The Algebra of Finite State Processes

Peter Michael Sewell

Doctor of Philosophy University of Edinburgh

1995

Graduation date: November 1995

Abstract

This thesis is concerned with the algebraic theory of finite state processes. The processes we focus on are those given by a signature with prefix, summation and recursion, considered modulo strong bisimulation. We investigate their equational and implicational theories.

We first consider the existence of finite equational axiomatisations. In order to express an interesting class of equational axioms we embed the processes into a simply typed lambda calculus, allowing equation schemes with metasubstitutions to be expressed by pure equations. Two equivalences over the lambda terms are defined, an extensional equality and a higher order bisimulation. Under a restriction to first order variables these are shown to coincide and an examination of the coincidence shows that no finite equational axiomatisation of strong bisimulation can exist. We then encode the processes of Basic Process Algebra with iteration and zero (BPA_{δ}^{∗}) into this lambda calculus and show that it too is not finitely equationally axiomatisable, in sharp contrast to the extant positive result for the fragment without zero.

For the implicational theory, we show the existence of finite computable complete sets of unifiers for finite sets of equations between processes (with zero order variables). It follows that the soundness of sequents over these is decidable.

Some applications to the theories of higher order process calculi and non-well-founded sets are made explicit.

Acknowledgements

I would like to thank my supervisor, Robin Milner, for his teaching in the practice and purpose of research, and for his patience and enthusiasm while this thesis mutated into its current form. Stuart Anderson provided intellectual support at an important time and also a period of educational employment. Section 2.3 was improved by discussions with Zoltán Ésik.

The Laboratory for the Foundations of Computer Science has provided a broad and stimulating environment in which to work. I thank particularly the members of the π and concurrency clubs.

This thesis was written with the aid of a voice recognition system, largely funded by the SERC. Thanks are also due to the Department and particularly to John Butler for providing the underlying hardware. I have been supported by SERC studentship 90311819 and the ESPRIT BRA 6454 (CONFER). Paul Taylor’s diagram and proof tree macro packages were used.

I have enjoyed my time in Scotland. This is partly due to the companionship of my long-suffering office mates Chen, Stephen and Luc, and Alex, Anthony, David, Dilip, Ian, John, Neil, Roberto, Savi and Steve.

Unfailing support has been provided by my parents and family.

Declaration

I declare that this thesis was composed by myself and that the work presented is my own except where otherwise stated. The main results of Chapter 3 and §4.1 have been reported in [Sew94 ].

Peter Sewell

This is a revised version, incorporating the suggestions of my examiners, Colin Stirling and David Walker.

Table of Contents

1. Introduction 1 1.1 Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 1.2 Notation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3

2. Background 5

2.1 Processes and Automata . . . . . . . . . . . . . . . . . . . . . . . . 5 2.1.1 Models . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 2.1.2 Syntax: μ-expressions . . . . . . . . . . . . . . . . . . . . . 8 2.1.3 Syntax: ∗-expressions . . . . . . . . . . . . . . . . . . . . . 10

2.2 Axiomatisation — some general remarks . . . . . . . . . . . . . . . 15 2.3 An overview of previous work . . . . . . . . . . . . . . . . . . . . . 20

2.3.1 Infinite systems for μ-expressions . . . . . . . . . . . . . . . 22 2.3.2 Finite impure horn clause systems . . . . . . . . . . . . . . 29 2.3.3 Finite pure horn clause systems . . . . . . . . . . . . . . . . 30 2.3.4 Systems for ∗-expressions . . . . . . . . . . . . . . . . . . . 31 2.3.5 Infinitary rules and Denotational models . . . . . . . . . . . 35

3. Axiomatisation over μ-expressions 37 3.1 Outline of chapter . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 Table of Contents v

3.2 Basic definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 3.3 Higher order bisimulation . . . . . . . . . . . . . . . . . . . . . . . 45 3.4 Finite state and decidability properties . . . . . . . . . . . . . . . . 48 3.5 The transition system of a substituted term . . . . . . . . . . . . . 53 3.6 The coincidence of ∼_{ext} and ∼_{ho} . . . . . . . . . . . . . . . . . . . 55 3.7 Loop properties . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59

4. A Miscellany 62

4.1 Axiomatisation over ∗-expressions . . . . . . . . . . . . . . . . . . 62 4.1.1 Axiomatisation with and without 0 . . . . . . . . . . . . . . 62 4.1.2 Axiomatisation with 1 . . . . . . . . . . . . . . . . . . . . . 65

4.2 Higher order process calculi . . . . . . . . . . . . . . . . . . . . . . 66 4.2.1 Syntax and transitions . . . . . . . . . . . . . . . . . . . . . 66 4.2.2 Normal bisimulation . . . . . . . . . . . . . . . . . . . . . . 68 4.2.3 The coincidence of ∼_{ho} and ∼_{Nr} . . . . . . . . . . . . . . . 69

4.3 Non-well-founded set theory . . . . . . . . . . . . . . . . . . . . . 71 4.4 Weak congruence: relative axiomatisability and at higher order . . 73

4.4.1 Weak higher order congruence . . . . . . . . . . . . . . . . 73 4.4.2 A finite axiomatisation of weak congruence relative to bisim-

ulation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 75

5. Implicational theory 80 5.1 The consequence relation and unification . . . . . . . . . . . . . . 81 5.2 Unification for charts . . . . . . . . . . . . . . . . . . . . . . . . . . 82 5.3 Minimal sets of unifiers . . . . . . . . . . . . . . . . . . . . . . . . 88

5.4 Unification for finite processes . . . . . . . . . . . . . . . . . . . . 89 6. Conclusion 91

6.1 Higher order bisimulation . . . . . . . . . . . . . . . . . . . . . . . 92 6.2 Axiomatisability . . . . . . . . . . . . . . . . . . . . . . . . . . . . 94 6.3 Unification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 99

A. Completeness proof 100 B. Loop properties 105 Bibliography 110 Index of Axioms 117 Index 119

Chapter 1

Introduction

Finite state machines have been the subject of a great deal of work in theoretical computer science, particularly by the language theory and process algebra communities. In their various formalisations they are the basis for models or specifications of many computational phenomena. A common formalisation is the labelled transition system consisting of a (finite) set equipped with an indexed family of binary relations over it. Typically the set is thought of as the possible states that a modelled system may be in, with the relations as the allowable changes of state. This is extremely general — for a particular application additional structure (such as a termination predicate on states) may be required and the model may be too fine, containing many states which should be identified. Many equivalences have been proposed, differing in their treatment of nondeterministic choice and termination. We shall largely be concerned with two, language equivalence and bisimulation, that are reasonably canonical among them. The introduction of an equivalence immediately raises a question of decidability. These are both decidable over finite state systems and indeed efficient decision procedures have been widely used in practice.

Direct presentations of finite state machines as sets and relations are awkward to work with. Accordingly, syntactic forms have been introduced to represent them, including a variety of process calculi and regular expressions. Any such raise questions of expressiveness, congruence and axiomatisability (all with respect to a chosen equivalence). The first two are generally straightforward. It is desirable for the syntax to be expressively complete, i.e. for all finite state machines to be representable up to the equivalence. If any manipulation of syntactic terms, such as equational reasoning, is to be done then the equivalence must also be a congruence and preferably also substitutive. There are several motivations for seeking axiomatisability results. The most obvious is that any sound system may be useful for human or machine manipulation of terms, particularly but not necessarily if it is complete. A number of nontrivial verification problems arising from practice can be addressed using such systems. For this thesis a more important motivation is that axiomatisability results (and especially their proofs) shed light on the nature of the equivalences involved and on their interaction with the syntax of axioms. If positive, axiomatisability results enable the semantic maps to be presented as the unique maps from term algebras, which is sometimes convenient. Lastly they permit a comparison of different equivalences and with the alternative view that takes a set of axioms as primary.

Given a syntax that admits substitution and a choice of equivalence there is a further natural question of the existence of solutions to (or unifiers for) equations between terms. The existence of finite computable complete sets of unifiers gives the decidability of implications between equations.

We will largely be concerned with a single equivalence — strong bisimulation — over the terms of a simple syntax — the μ-expressions, with prefix, summation and a binding operator for recursion. We consider the existence of finite axiomatisations and of finite computable complete sets of unifiers.

The existence of a finite axiomatisation obviously depends upon the strength of the metalanguage in which axioms are written. The weakest interesting choice is to consider equational axioms. For a syntax with binding there are further choices of the entities that variables in axioms may range over. We embed the μ-expressions into a fragment of a simply typed lambda calculus, allowing many non-trivial properties to be expressed as equations. Our first main result is that no finite set of these equations can be a complete axiomatisation. There are then almost immediate non-finite-axiomatisability results for bisimulation of certain regular expressions and for equality of certain non-well-founded set expressions. A key tool is a notion of higher order bisimulation which we relate to the normal bisimulation of the higher order π calculus.

Our second main result is the construction of finite complete sets of unifiers for finite sets of equations between μ-expressions.

1.1 Overview

In Chapter 2 the basic definitions of syntax and semantics are introduced and the problems of axiomatisability that arise are discussed, firstly in general terms with reference to their motivation and then with reference to some previous work in the field.

In Chapter 3 our main non-axiomatisability result, that there is no finite equational axiomatisation for bisimulation over μ-expressions, is formulated and proved.

Chapter 4 consists of a number of applications and developments of the theory of higher order bisimulation. We consider the axiomatisability of bisimulation over ∗-expressions, relate higher order bisimulation to the higher order π calculus and cast our results into the language of non-well-founded set theory. We also give a definition of weak higher order congruence and show that weak congruence is finitely axiomatisable relative to bisimulation.

In Chapter 5 there is an investigation of the implicational theory of finite state processes (up to bisimulation). We show the existence of finite computable complete sets of unifiers for sets of equations between μ-expressions and hence the decidability of implications.

There are only limited formal dependencies between chapters. The definitions in §2.1 are used throughout and the sections of Chapter 4 should be read after Chapter 3 (but are independent of each other).

1.2 Notation

The notation used is by and large standard, a few points are mentioned here for reference.

Theorems, propositions, lemmas and corollaries are numbered in two sequences, one of theorems and one of the others. The statements of a few lemmas are repeated in appendices with the original numbers. Subsidiary lemmas and definitions within proofs are sometimes indented.

If ⟶ is any binary relation on a set we write ⟶^{∗}, ⟶^{+}, ⟶^{n}, ⟶^{≤n} for its reflexive transitive closure, its transitive closure, the n-ary self composition and the union of ⟶^{m} for m ≤ n. We often work with a family ⟶^{a} | a ∈ Act of binary relations indexed by actions and write ⟶ for ∪_{a∈Act} ⟶^{a}. Universal quantifiers over actions are freely omitted.

Substitutions are written postfix with E[F/X] standing for E in which all occurrences of X are replaced by copies of F. The composition of substitutions ρ and ρ′ is written as ρ ∘ ρ′. The substitution which is as ρ except where overridden by ρ′ is written ρ ⊕ ρ′

Tuples are written with tildes, e.g. writing Ẽ for a tuple E_{1} … E_{n}, or in angle brackets, e.g. ⟨A, B, C⟩. Concatenation and append are both written simply as juxtapositions.

The set of natural numbers is written ω. We sometimes identify the number n with the set {0, …, n − 1}.

Background

In this chapter the basic definitions of syntax and semantics are introduced and the problems of axiomatisability that arise are discussed, firstly in general terms with reference to their motivation and then with reference to some previous work in the field.

2.1 Processes and Automata

The current applicability and history of the study of finite state machines are both too extensive to be treated here in any depth — a very brief historical sketch will be given. The basic notion is that of a finite discrete system together with an informal idea of its behaviour in discrete time. This is explicitly present in the work of Turing [Tur37] and of McCulloch and Pitts [MP43], although it may well have existed earlier. It is there applied respectively to the modelling of abstract (human) computation and concrete neural networks. In the first, machines (i.e. the finite state controls of Turing machines) are given by explicit descriptions of the sets of states and transition relations. In the second they are given structurally as networks of fundamental elements, with expressivity results relating structure and behaviour. A more syntactic description, the regular^{1} or ∗-expressions, was introduced by Kleene [Kle56] and later simplified by Copi, Elgot and Wright [CEW58].

1We avoid the use of ‘regular’. Most entities that we deal with could be qualified by it, to no useful end.

They have an explicit iteration operator together with sequential composition and summation. The paper of Kleene introduced in addition the study of the algebra of these expressions, giving some sound equations for his interpretation (which in the simplified formulation of [CEW58] is close to the standard language interpretation). Finer interpretations were apparently first introduced by Milner [Mil80] to give a more refined account of the interactions between a machine and an experimenter, leading to the bisimulation equivalence of Park [Par81]. To express all finite state machines up to bisimulation a richer syntax is required, such as the μ-expressions which have variables and an explicit recursion operator together with prefix and summation. The algebra of the four combinations of syntax and model has been the subject of a large body of work, some of which is discussed in §2.3. We first give precise definitions of the two models, followed by the definitions of syntax and the basic results. Detailed references and proofs are omitted — the latter are all either straightforward or essentially from [Kle56] or [Mil84].

2.1.1 Models

The models are parameterised by a set Act of atomic actions, ranged over by a, b. This is generally supposed to be nonempty but we require no other structure and do not require it to be infinite. The set of finite sequences of actions will be written Act^{∗} with the empty sequence as ϵ and concatenation as juxtaposition. Universal quantifiers over Act will generally be omitted.

We start not with labelled transition systems but with charts. These contain additional information in the form of a visibility predicate ▷ between states and a set Var of variables. This allows μ-expressions containing free variables to be modelled and permits a close tie-up between bisimulation and language equivalence of ∗-expressions. The definitions are justified by Proposition 11 below relating them to the closed term case. When dealing with μ-expressions we suppose Var to be infinite, to permit alpha conversion.

Definition A chart S is a tuple ⟨S, ⟶, ▷, s_{0}⟩ where S is a set of states, s_{0} ∈ S is an initial state, ⟶ ⊆ S × Act × S is a transition relation and ▷ ⊆ S × Var is a visibility predicate. We will sometimes ignore the initial state.

The finest equivalence on charts that we deal with is bisimulation, at the top of the linear-branching time hierarchy. It takes full account of the nondeterministic branching structure of the transition relations.

Definition A relation R ⊆ S × S over the state set of a chart is a bisimulation if s R t implies:

• If s⟶^{a}s′ then ∃t′ . t⟶^{a}t′ ∧ s′ R t′.

• If s ▷ X then t ▷ X.

and symmetrically. Two states are bisimilar, written s ∼ s′, if there exists a bisimulation relating them.

Proposition 1 The relation ∼ is itself a bisimulation.

At the bottom of the linear-branching time hierarchy are various forms of trace or language equivalence. The following definition allows the chart and language semantics of ∗-expressions to be closely related (by Proposition 12 below).

Definition The extended language of a state s of a chart is the subset of Act^{∗}×Var containing a_{1}, …, a_{n}, X iff there exist states s_{1}, …, s_{n} such that s⟶^{a_{1}}s_{1} … ⟶^{a_{n}}s_{n} ▷ X. Two states are language equivalent if they have the same extended languages.

The trace congruence of [Rab93] will also be referred to.

Definition The trace set of a state s is the subset of Act^{∗} containing a_{1}, …, a_{n} iff there exist states s_{1}, …, s_{n} such that s⟶^{a_{1}}s_{1} ⋯ ⟶^{a_{n}}s_{n}. Two states are trace congruent if they have the same trace sets and the same extended languages.

In many applications it is necessary to abstract from certain actions which are considered to take place ‘internally’. One equivalence that does this is the weak (or observational) congruence of [Mil89]. This is defined in terms of a distinguished action τ and the derived transition relations

⟹^{a} =^{def} ⟶^{τ}^{∗}⟶^{a}⟶^{τ}^{∗}
⟹^{â} =^{def} ⟶^{τ}^{∗}⟶^{a}⟶^{τ}^{∗}, if a ∈ Act − τ
=^{def} ⟶^{τ}^{∗},  if a = τ.

Definition A relation R ⊆ S×S over the state set of a chart is a weak bisimulation if s R t implies:

• If s⟶^{a}s′ then ∃t′ . t⟹^{â}t′ ∧ s′ R t′.

• If s ▷ X then t⟶^{τ}^{∗} ▷ X.

and symmetrically. Two states are weak bisimilar, written s ≈ s′, if there exists a bisimulation relating them. Two states are weak congruent, written s ≈^{c} s′, if there is a weak bisimulation R with s W(R) t, where s W(R) t if

• If s⟶^{a}s′ then ∃t′ . t⟹^{a}t′ ∧ s′ R t′.

• If s ▷ X then t⟶^{τ}^{∗} ▷ X.

and symmetrically.

Proposition 2 Bisimulation is strictly finer than weak congruence and trace congruence. The latter is strictly finer than language equivalence.

Bisimulation and the other equivalences are lifted to relations between charts by applying the above definitions to a disjoint union and considering the initial states.

2.1.2 Syntax: μ-expressions

Definition The μ-expressions are those of the grammar

E ::= 0 | X | aE | E + E | μXE

where X and a are drawn from sets Var, Act of variables and actions and μ is a binding operator. We adopt standard notions of free and bound variables, substitution and alpha conversion. The scope of a binder is generally as far to the right as possible. Sum is taken to have lower precedence than prefix so aE + F is (aE) + (F).

We will have occasion to refer to the infinite term equivalence =_{infinite term} induced by unwinding the recursions in μ-expressions to give finite or infinite trees. A formal definition will not be given, however.

Definition Take the relations ⟶^{a} | a ∈ Act and ▷ to be the least over μ-expressions such that

aE⟶^{a}E  X ▷ X

{E⟶^{a}E′ \atop E + F ⟶^{a}E′} and sym. {E ▷ X \atop E + F ▷ X} and sym.

{E⟶^{a}E′ \atop μY E⟶^{a}E′[μY E /Y]}  \begin{matrix}E ▷ X & X ≠ Y \\ μY E ▷ X \end{matrix} .

Any μ-expression E can thus be regarded as a chart, with initial state E itself. The rule for μ differs from the more usual

{E[μY E /Y]⟶^{a}E′ \atop μY E⟶^{a}E′}

but is slightly more convenient. We check that it is equipotent. Let ⇝^{a} be the least relation over μ-expressions satisfying the rules for prefix, sum and the second rule for μ.

Proposition 3 The relations ⟶^{a} and ⇝^{a} coincide.

Proof The following lemmas are used, both of which are provable by induction on derivations. Closely related properties will be heavily used later (see Lemmas 35 and 52).

Lemma 4 If E⇝^{a}F then E[G/Y]⇝^{a}F [G/Y].

Lemma 5 If E[F/Y]⟶^{a}G then either E⟶^{a}E′ and E′[F/Y] = G or E ▷ Y

and F ⟶^{a}G.

The proposition can now be proved by an induction on derivations for each direction. The only interesting cases are those in which the conclusion of a derivation is the relevant μ rule. Lemma 4 is required for the inclusion ⟶^{a} ⊆ ⇝^{a} and Lemma 5 for the converse. □

10 Chapter 2. Background The μ-expressions suffice to express all finite charts up to bisimulation and therefore also up to language equivalence. Definition A chart ⟨S, ⟶, ▷, s_{0}⟩ is finite if S, ⟶ and ▷ are all finite. Proposition 6 A chart is bisimilar to a finite chart iff it is bisimilar to some μexpression. The equivalences are congruences. Proposition 7 Bisimulation of μ-expressions is a congruence, i.e. it is an equivalence satisfying

{E ∼ F \atop aE ∼ aF} \begin{matrix}E ∼ E′ & F ∼ F′ \\ E + F ∼ E′ + F′ \end{matrix} {E ∼ F \atop μXE ∼ μXF}

and is substitutive, i.e. it satisfies

{E ∼ F \atop E[G/X] ∼ F [G/X]}.

Proposition 8 Language equivalence of μ-expressions is a substitutive congruence. Proposition 9 Trace congruence of μ-expressions is a substitutive congruence. Proposition 10 Weak congruence of μ-expressions is a substitutive congruence. In a given application one might well take as primary bisimulation over labelled transition systems or closed μ-expressions. The extension to open terms given above can be justified as the coarsest reasonable such. Proposition 11 Bisimulation of μ-expressions is the largest congruence that, when restricted to the closed μ-expressions, is at least as fine as bisimulation there.

2.1.3 Syntax: ∗-expressions

Finite state systems have also been described using calculi with a unary or binary iteration operator in place of explicit recursion, such as the ∗-expressions given by

E ::= a | 0 | 1 | E + E | E . E | E^{∗} | E^{⋆}E

where a ∈ Act. There are several points to note:

• Actions are now taken to be nullary and there is a sequential composition.

• Two iteration operators are included. A binary iteration E^{⋆}F represents zero or more iterations of E followed by one of F. This was introduced in [Kle56] and simplified in [CEW58] to the ubiquitous unary iteration, with E^{∗} representing zero or more iterations of E. In the presence of 1 they will be interdefinable in our semantics, with

E^{⋆}F = E^{∗} . F  and  E^{∗} = E^{⋆}1.

• Both a 0 and a 1 are included. In process calculus terms they will represent the unsuccessfully and successfully terminated processes respectively. Language theoretically, they will represent the empty language and the language containing only the empty word. In both cases they will be units and zeros for choice and sequential composition as below.

\begin{aligned}0 + E & = & E & = & E + 0 & 0 . E & = & 0 \\ 1 . E & = & E & = & E . 1 \end{aligned}

Language theoretically we will also have E . 0 = 0. In the presence of 0 and ∗ (but not 0 and ^{⋆} alone) 1 is definable with 1 = 0^{∗}. Calculi without 1 have recently been studied in the setting of ACP, where the interaction of 1 and the parallel operators may be subtle. Binary iteration has received renewed attention in these, for example in [BBP94].

We give chart semantics using an additional judgment √ to record successful termination. Formally we regard √ as a distinguished element of Var and write E√ as shorthand for E ▷ √. The previous definitions of bisimulation and language can therefore be applied.

Definition Take the relations ⟶^{a} | a ∈ Act and predicate √ to be the least over the ∗-expressions such that

a⟶^{a}1  1√
{E⟶^{a}E′ \atop E + F ⟶^{a}E′} and sym.  {E√ \atop E + F √} and sym.
{E⟶^{a}E′ \atop E . F ⟶^{a}E′ . F} \begin{matrix}E√ & F ⟶^{a}F′ \\ E . F ⟶^{a}F′ \end{matrix} \begin{matrix}E√ & F √ \\ E . F √ \end{matrix}
{E⟶^{a}E′ \atop E^{∗}⟶^{a}E′ . E^{∗}}  E^{∗}√
{E⟶^{a}E′ \atop E^{⋆}F ⟶^{a}E′ .(E^{⋆}F)} {F ⟶^{a}F′ \atop E^{⋆}F ⟶^{a}F′}  {F √ \atop E^{⋆}F √}.

Note that there are no rules for 0. The ∗-expressions are expressively complete for language equivalence. We first recall the standard definition of the language denoted by a regular expression. Definition The language denoted by a ∗-expression E is [[E]] where

[[a]] =^{def} {a}
[[0]] =^{def} {}
[[1]] =^{def} {ϵ}
[[E + F]] =^{def} [[E]] ∪ [[F]]
[[E . F]] =^{def} { st | s ∈ [[E]] ∧ t ∈ [[F]] }
[[E^{∗}]] =^{def} { s_{1} … s_{n} | n ≥ 0 ∧ ∀i ∈ 1..n . s_{i} ∈ [[E]] }
[[E^{⋆}F]] =^{def} { s_{1} … s_{n}t | t ∈ [[F]] ∧ n ≥ 0 ∧ ∀i ∈ 1..n . s_{i} ∈ [[E]] }.

This factors through the chart semantics. Proposition 12 A word w is in the language denoted by a ∗-expression iff w, √ is in the extended language of the chart associated with the expression. Proposition 13 A language L ⊆ Act^{∗} is denotable by a ∗-expression iff { w, √ | w ∈ L } is the extended language of a finite chart with Var = {√}.

Thus they are as expressive as the μ-expressions, up to language equivalence, however they express fewer bisimulation classes:

Proposition 14 There exists a finite chart with Var = {√} that is not bisimilar to any ∗-expression.

Both equivalences are congruences.

Proposition 15 Bisimulation of ∗-expressions is a congruence, i.e. it is an equivalence satisfying

\begin{matrix}E ∼ E′ & F ∼ F′ \\ E + F ∼ E′ + F′ \end{matrix}  \begin{matrix}E ∼ E′ & F ∼ F′ \\ E . F ∼ E′ . F′ \end{matrix}  {E ∼ F \atop E^{∗} ∼ F^{∗}}  \begin{matrix}E ∼ E′ & F ∼ F′ \\ E^{⋆}F ∼ E′ ^{⋆}F′ \end{matrix}

and is substitutive (w.r.t. substitution of terms for actions), i.e. it satisfies

{E ∼ F \atop E[G/a] ∼ F [G/a]}.

Proposition 16 Language equivalence of ∗-expressions is a substitutive congruence.

Note that the definition of the ∗-expressions does not include variables — actions play a dual role, appearing both in the definitions of the equivalences and in the substitution rule of axiomatisations. This is standard in the literature. It is shown to be innocuous by the previous two propositions.

A variety of subcalculi have been discussed in the literature with differing notation. For reference we include a little table:

a 0 1 + . ^{∗}  ^{⋆}
a Λ ∨ . ^{∗} [CEW58]
a 0 1 + . ^{∗}  [Con71,Koz94]
a ϕ  + . ^{∗}  [Sal66]
a  ϵ + .  BPA^{ϵ} as in [Mol89]
a  + .  ^{∗} BPA^{∗} as in [BBP94,FZ94]
a δ  + .  ^{∗} BPA_{δ}^{∗} as in [BBP94,FZ94,Fok94]

The cited work is variously concerned with algebras satisfying certain axioms or with particular models. We therefore need to state carefully exactly what the above correspondences are. For the first three lines the common expressions denote the same language in the standard interpretation, except that in [CEW58] E^{∗} does not necessarily contain the empty word. For the last three lines bisimulation as defined below agrees with the definitions in the cited work, as follows.

For terms of {1, a, +, .} bisimulation is that of [Mol89, §6.3.1] for BPA^{ϵ} (identifying 1 and ϵ). As discussed there it differs from the original BPA^{ϵ} semantics of [Vra86]. Our transition system differs also from the semantics of [BBP94,FZ94] for terms of {0, a, +, ., ^{⋆}}. There the rules above involving 1, ^{∗} or √ are replaced by the following

a⟶^{a}√

{E⟶^{a}√ \atop E + F ⟶^{a}√} and sym.

{E⟶^{a}√ \atop E . F ⟶^{a}√}

{E⟶^{a}√ \atop E^{⋆}F ⟶^{a}E^{⋆}F}  {F ⟶^{a}√ \atop E^{⋆}F ⟶^{a}√}

with the bisimulation ↔ defined by replacing the condition

• If E′ ▷ √ then F′ ▷ √.

by

• If E′⟶^{a}√ then F′⟶^{a}√.

The bisimulations coincide, however.

Proposition 17 For terms of {0, a, +, ., ^{⋆}} bisimulation ∼ coincides with bisimulation ↔ over BPA_{δ}^{∗} (identifying 0 and δ) as defined in [BBP94].

Proof Let P, Q range over terms of {0, a, +, ., ^{⋆}} and E, F, G range over terms of {1, 0, a, +, ., ^{⋆}}. If =_{1} is the least equivalence over the latter such that 1 . E =_{1} E and

{E =_{1} F \atop E . G =_{1} F . G}

then it is straightforward to show that

{ P, Q | ∃E, F . P =_{1} E ∼ F =_{1} Q }

is contained in ↔ and that

{ E, F | ∃P, Q . E =_{1} P ↔ Q =_{1} F } ∪ { E, F | E =_{1} 1 =_{1} F }

is contained in ∼. □

2.2 Axiomatisation — some general remarks

The bulk of this thesis addresses questions of axiomatisability of equivalences over the μ- and ∗-expressions. As it stands these questions are poorly defined — there is a range of possible definitions of what an axiomatisation is and the motivation of Chapter 1 does not provide technical criteria that pick out a unique one. In general the insight gained from an axiomatisation is inversely related to the expressiveness of the metalanguage in which the axioms and rules are presented. We briefly discuss the possible spectrum. Detailed references to and discussion of previous work are left to the next section.

We first consider infinite equational axiomatisations. The sets of all equivalent pairs of expressions are trivially complete (and indeed also recursive, as bisimulation and language equivalence of finite charts are decidable). More interesting are sets generated in a uniform way from a small number of schemata (using some ad hoc metanotation) such as the group or commutative identities reproduced in §2.3, or the axioms C_{mn} of §2.3.4. These expose some of the structure of the equivalence concerned. They are compelling if they do this well and are simple — an informal criterion. Tighter questions can be asked about the existence of finite axiomatisations. To make these precise and in particular to state nonexistence results we must define classes of allowable axiomatisations. We give a variety of notions of ‘pure’ system, i.e. systems in which all terms that appear are of the object language.

For an object language without binding operators, such as the ∗-expressions, the situation is unproblematic. We take a finite pure equational axiomatisation to consist of a finite set A of pairs of object language terms together with the rules in Figure 2–1 for congruence and the following:

E = F E = F ∈ A {E = F \atop E[G/a] = F [G/a]}.

Moving to a richer logic, a finite pure horn clause axiomatisation consists of a finite set of expressions of the form

E_{1} = F_{1} ∧ ⋯ ∧ E_{m} = F_{m} → E′ = F′

E = E ref

{E = F \atop F = E} sym  \begin{matrix}E = F & F = G \\ E = G \end{matrix} tran

\begin{matrix}E = F & E′ = F′ \\ E + E′ = F + F′ \end{matrix} +cong \begin{matrix}E = F & E′ = F′ \\ E . E′ = F . F′ \end{matrix} ^{. cong}

{E = F \atop E^{∗} = F^{∗}} ∗cong  \begin{matrix}E = F & E′ = F′ \\ E^{⋆}E′ = F ^{⋆}F′ \end{matrix} ^{^{⋆}cong}

Figure 2–1: Congruence rules for ∗-expressions

or

E_{1} = F_{1} ∧ ⋯ ∧ E_{m} = F_{m} →⊥,

where E, F are object language terms and m ≥ 0, together with rules for congruence, instantiation and manipulation of ∧, → and ⊥.

In the presence of binding operators the situation is not quite so simple, as equations between object language terms are then very inexpressive. For example alpha conversion or the unfolding of recursions would each require an infinite set of equations. Instead one might write down schemata such as

E[μXE /X] = μXE
μY E[Y/X] = μXE , if Y not free in μXE,

expressing unfolding and alpha conversion. It would be possible to give a definition (perhaps several) of a natural class of such schemata and, by formalising the manner in which they are instantiated, a definition of a class of axiomatisations containing a finite set of them. We do not because it would be rather complex — the schemata above contain metavariables over both object variables (X, Y) and terms (E), substitutions and a simple side condition. Instead we embed the μ-expressions into a fragment of the simply typed lambda calculus. This is described in detail in Chapter 3. For now we note only that it lets us take a finite pure equational axiomatisation to be simply a finite set of pairs of lambda terms (of appropriate types) together with standard rules for βη equality. The first schema above can be written simply as

e: P → P ▷ fix e = e(fix e) : P

and the second is subsumed by lambda calculus alpha conversion. A finite pure horn clause axiomatisation would then be as before except that E, F now range over typed lambda terms.

A number of finite horn clause axiomatisations have been given which are essentially impure in that they contain rules which cannot be put into this form. We mention two, deferring full definitions of the notation involved to later in this chapter. Firstly the unique fixed point rule schema from [Mil84]:

E = F [E/X] ∧ X guarded in F → E = μXF

in which the ‘guarded’ condition is not equational and secondly the functorial implication from [BÉ94]:

∀i ∈ m . E_{i}[Y_{ρ(j)}/X_{j}]_{j∈m} = F_{ρ(i)} → ∀i ∈ m . μ̃_{i}X̃ Ẽ = μ̃_{ρ(i)}Ỹ F̃

which has an instance for each pair m, n ≥ 1 of natural numbers and surjective function ρ: m → n.

In summary, for both ∗-expressions and μ-expressions we have a hierarchy of classes of axiomatisations:

• Infinite (but elegant) equational

• Finite impure horn clause

• Finite pure horn clause

• Finite pure equational

of which the first two are not formally defined. For μ-expressions the last two will be further subdivided by placing restrictions on the types allowable in axioms.

We now return to the general motivation for axiomatisability results of Chapter 1 and discuss it with respect to this hierarchy.

Human and Machine reasoning

Sound systems are in principle useful for reasoning about the equivalence of expressions. In practice, however, they are only useful for human reasoning about relatively small expressions. For that there is no advantage in restricting to a weak metalanguage — indeed it may be useful to apply (say) both unique fixed point reasoning from the system of [Mil84] and the schema from the infinite system of §2.3.1 in the same work. For larger expressions model-based techniques which apply directly to the chart denoted by an expression seem to be preferable, as efficient algorithms have been found. We should note that for more expressive calculi the situation may be very different. There it may be possible to use (human) understanding of the (term) structure in a particular equivalence problem to quickly find a good proof in a suitable formal system. It may also be possible to orient the equations of an equational axiomatisation to give a useful term rewriting system.

Insight

As stated in Chapter 1 a more important motivation for this work is the insight gained from proofs — of positive (completeness) or negative (non-axiomatisability) results. In general we would like positive results as far down the hierarchy as possible since an inexpressive metalanguage requires a better understanding. (In the extreme case of a strong logic the definitions of the equivalences could be directly but pointlessly written down.) Conversely, negative results should be as far up as possible although obviously their statements require formal definitions of classes of axioms.

Expressivity and Comparison

Positive results can be used to compare different equivalences, particularly if there is a clean extension of an axiomatisation for one which is complete for another. A more general approach is to consider questions of relative axiomatisability, i.e. to consider whether an equivalence ∼_{1} is axiomatisable in one of the senses above augmented with a rule

E ∼_{2} F → E = F

for another equivalence ∼_{2}. A different form of comparison is to keep the equivalence fixed and vary the expressions. The existence of an axiomatisation can be seen as depending on the metalanguage being expressive with respect to the object language. This can be investigated by looking for axiomatisable sub-languages of a non-axiomatisable object language.

Other models

Throughout this section and in the greater part of the thesis we have considered axiomatisation of the equivalences induced by a few particular, intended, models of the expressions. An alternative approach is to consider the category of all models equipped with suitable homomorphisms. Pure equational and horn clause axiomatisations (not necessarily finite) are desirable in that they permit the results of universal algebra to be applied. For the ∗-expressions the notion of model is standard and the results (from [MT92], say) are immediately applicable. In particular any pure equational (resp. horn clause) axiomatisation defines a variety (resp. quasi variety) containing an initial model. For the μ-expressions there are several possible notions of model. Two, the preiteration algebras and strong preiteration algebras, are given in [BÉ94] together with an analogue of the variety theorem. They are specialized from work on iteration theories. These provide a general setting for the investigation of the equational logic of fixed point operators. We cannot do justice to the work here, but instead refer the reader to [BÉ93b].

One can also look for axiomatisations which are sound in several intended models, as is done for example in [Koz94] for the ∗-expressions. In particular, axioms involving a ‘guarded’ condition tend not to be valid in coarser models.

Domain theoretic models of the μ-expressions will be briefly discussed in §2.3.5 along with the infinitary rules of ω-induction and the approximation induction principle.

Completeness and ω-completeness

We have several times referred in an ambiguous way to completeness results. There can be a significant difference between completeness for closed and open terms, as shown for example in [Mol89] for a calculus with parallel composition. We recall the definitions from §2.3.2 of that work.

Typically one might have an equivalence ≃ defined over closed terms and a proof system deriving judgments ⊢ E = F between arbitrary terms. The proof system is then said to be complete if

• for all closed E, F if E ≃ F then ⊢ E = F,

and ω-complete if

• for all E and F, if Eρ ≃ F ρ for all closed substitutions ρ then ⊢ E = F.

For μ-expressions ω-completeness does not seem to be a problem. The negative result of Chapter 3 (Theorem 6) shows that there is no complete system and so immediately that there is no ω-complete system. The positive results mentioned in the next section (Theorems 1, 2, 3 and 4) are all with respect to all μ-expressions and so could be considered as ω-completeness results.

On the other hand, one could take the pure axiomatisations obtained from the first two and last of these by embedding into the lambda calculus. They might then be considered to be ω-complete iff all the sound identities between terms containing higher type variables are derivable (i.e., with notation from Chapter 3: iff they are complete for ∼_{ext} over T_{ω}^{P}, not just over T_{0}^{P}). We do not have a completeness result over T_{ω}^{P}, or even over T_{1}^{P} — such a result would be of some limited interest.

2.3 An overview of previous work

There is a substantial literature dealing with axiomatisation of equivalences over calculi denoting finite state machines. A part of it is summarised in Figure 2– 2, classified by the equivalence, calculus and strength of logic addressed and labelled √ (resp. ×) if finite complete systems are given (resp. shown not to exist). Results labelled [Sew] are contained in this thesis and have also been announced in [Sew94 ]. Care must be taken when interpreting the figure as there are differ-

√[Mil84](impure)

√[BÉ94]
[figure]

horn clause √[Sal66](impure) √[AG87] √[Bof90, Kro91] √[Koz94]

√[Rab93](impure)

×[Sew] ; √[FZ94] ; √[Fok94]  ×[Sew]  bisimulation
[figure]

equational ×[Red64] ×[Con71] √[Yan](for events ≥ 1)

language or trace

∗-expressions  μ-expressions

Figure 2–2: Finite axiomatisability results

ing definitions, in particular of the syntax of the ∗-expressions and of language equivalence over μ-expressions.

The figure is not intended to imply that all vertices have equal interest — in fact the expressivity results of Propositions 6, 13, 14 suggest that the language/∗- expression and bisimulation/μ-expression edges are more significant than the others. Further, there are many interesting equivalences which are not shown. There are trivial implications only along the logic (vertical) axis — relative axiomatisability results would give implications along the equivalence axis but we have none applicable.

We will first discuss the μ-expression problems in some detail, not attempting to be exhaustive or historical but rather focusing on the techniques used to show completeness. We then discuss the ∗-expression work more briefly and finally mention some more distantly related work. Soundness proofs will be omitted.

In the absence of recursion there is no difficulty. The axioms

\begin{aligned}A1 & E + (F + G) & = & (E + F) + G \\ A2 & E + F & = & F + E \\ A3 & E + 0 & = & E \\ A4 & E + E & = & E \end{aligned}

together with rules for congruence are complete for bisimulation over the expressions given by

E ::= 0 | aE | E + E

(from [HM80]) and adding P 1 or P 1, P 2

\begin{aligned}P 1 & aE + aF & = & a(E + F) \\ P 2 & a0 & = & 0 \end{aligned}

gives completeness for trace congruence or language equivalence respectively. (We present these and subsequent axioms informally using metavariables E, F. They could easily be put in a pure form in a lambda calculus similar to that of Chapter 3.) Axiomatisations for a number of equivalences in the linear-branching time spectrum are collected in [Gla90]. Bisimulation over arbitrary well-founded GSOS systems is finitely axiomatised in [ABV92].

2.3.1 Infinite systems for μ-expressions

We now give an infinite system for bisimulation over all μ-expressions. That this is possible is of course trivial and indeed the completeness proof, although new, is not terribly difficult. It is included for several reasons. Firstly, it provides some insight and suggests interesting conjectures about the completeness of subsystems. Indeed the nonexistence proof of Chapter 3 arose from considering whether restrictions of a closely related system were complete. Secondly the proof is closely related to those for certain finite impure horn clause systems considered in the next section. Finally the result gives a relative axiomatisability result as an immediate corollary and may be useful for completeness proofs of other systems — e.g. the pure horn clause system of §2.3.3 — as it is only necessary to show that all instances of these equations are derivable.

Together with A1–4 there are axioms for alpha conversion, recursion unfolding, absorbing unguarded variables and a form of Bekič’s lemma.

A5  μY E[Y/X] = μXE , if Y not free in μXE
B1  E[μXE /X] = μXE
B2  μXX + E = μXE
B3  μXE[μY F /Y] = μXE[μY F [μXE /X] /Y]

In addition we have a set of axioms C_{mn} indexed by pairs of non-zero natural numbers. Loosely, C_{mn} expresses the equality of any m-state transition system with one in which each state has been split into n bisimilar states. To state these precisely we need some additional notation.

A natural number, say n, will be identified with the set {0, …, n − 1}. We introduce sequences of formal equations, i.e. nonempty sequences of pairs of a variable (all of which must be distinct) and a μ-expression. A variety of notations will be used — the following all denote the same sequence.

[figure: \begin{matrix}⟨X_{0} = E_{0}, …, X_{n−1} = E_{n−1}⟩ \\ ⟨X_{i} = E_{i} | i ∈ n⟩ \\ ⟨X̃ = Ẽ⟩ \end{matrix}; X_{0} = E_{0} ; ⋮ ; X_{n−1} = E_{n−1}]

The fixed point of a sequence is a μ-expression defined by induction:

μ ⟨X = E⟩ =^{def} μXE
μ ⟨X̃ = Ẽ, X = E⟩ =^{def} μ ⟨X̃ = Ẽ[μXE /X]⟩.

The simultaneous substitution of n expressions E_{i} | i ∈ n for n distinct variables X_{i} | i ∈ n will be written as [E_{i}/X_{i}]_{i∈n}. We let i and k range over m, j over n and f over the functions from n to n. Pairs of numbers are given the product ordering. Finally, the axiom is

C_{mn} \begin{aligned}& μ ⟨X_{i} = E_{i}[X_{k}/Z_{kf}]_{k∈m,f∈n^{n}} | i ∈ m⟩ \\ = & μ ⟨Y_{ij} = E_{i}[Y_{k,f(j)}/Z_{kf}]_{k∈m,f∈n^{n}} | i ∈ m, j ∈ n⟩, \end{aligned}

in which we suppose that none of the X_{k} or Y_{kj} appear in any of the expressions E_{i}. Note that the substitutions appearing have as domain all mn^{n} of the Z_{kf}.

The idea is rather simpler than the notation. Consider a non-binding occurrence of a variable (say X_{k}) in a sequence of m equations. If each state is split into n, giving a sequence of mn equations, it becomes n occurrences. Each might be any of the Y_{kj} | j ∈ n. To allow for any such ‘behaviour’ of the original occurrence we begin with n^{n} formal variables Z_{kf} for each X_{k}.

For example here is C_{12}, omitting the first index of the Y ’s (which is always 0):

μ ⟨ X_{0} = E_{0}[X_{0}X_{0}X_{0}X_{0}] ⟩ = μ ⟨ \begin{matrix}Y_{0} = E_{0}[Y_{0}Y_{0}Y_{1}Y_{1}] \\ Y_{1} = E_{0}[Y_{0}Y_{1}Y_{0}Y_{1}] \end{matrix} ⟩

and C_{22}:

μ ⟨ \begin{matrix}X_{0} = E_{0}[X_{0}X_{0}X_{0}X_{0}X_{1}X_{1}X_{1}X_{1}] \\ X_{1} = E_{1}[X_{0}X_{0}X_{0}X_{0}X_{1}X_{1}X_{1}X_{1}] \end{matrix} ⟩ = μ [figure] \begin{matrix}Y_{00} =E_{0}[Y_{00}Y_{00}Y_{01}Y_{01}Y_{10}Y_{10}Y_{11}Y_{11}] \\ Y_{01} =E_{0}[Y_{00}Y_{01}Y_{00}Y_{01}Y_{10}Y_{11}Y_{10}Y_{11}] \\ Y_{10} =E_{1}[Y_{00}Y_{00}Y_{01}Y_{01}Y_{10}Y_{10}Y_{11}Y_{11}] \\ Y_{11} =E_{1}[Y_{00}Y_{01}Y_{00}Y_{01}Y_{10}Y_{11}Y_{10}Y_{11}] \end{matrix} [figure].

We show how these axioms can be used to derive the equation

μXaX = μXa^{n}X

(for any n ≥ 1) in a simple way. Given n, consider the instance of C_{1n} obtained by taking E_{0} = aZ_{0,f} where f : n → n is defined by

f(x) =^{def} (x + 1) mod n.

This instance of C_{1n} is

μX_{0}aX_{0} = μY_{0}aμY_{1}a … μY_{n−1}aY_{0}

from which the equation follows by use of B1 and A5.

The completeness of these axioms is reasonably straightforward. We show that any expression is provably equal (using axioms A, B only) to the fixed point of a sequence of equations in a standard form. Given such sequences for two bisimilar expressions we construct a ‘product’ sequence of equations and use instances of C to show that all three fixed points are provably equal. The proofs of Lemmas 18, 19, 20 and 21 are banished to Appendix A.

Notation If E = F is provable from the axioms Q together with A1–5 and rules for congruence then we write Q ⊢ E = F. We work up to the equivalence induced by A1–5 throughout.

First we give two simple results. Provable equality lifts from expressions to the fixed points of sequences and the binary B3 implies an m-ary form (palliating the occasional ambiguity in the order of sequences).

Lemma 18 For axioms Q, if Q ⊢ E_{i} = F_{i} for all i then Q ⊢ μ ⟨X̃ = Ẽ⟩ = μ ⟨X̃ = F̃⟩.

Lemma 19 If π: m → m is a permutation with π(0) = 0 then B3 ⊢ μ ⟨X_{i} = E_{i} | i ∈ m⟩ = μ ⟨X_{π(i)} = E_{π(i)} | i ∈ m⟩.

Expressions are provably equal to the fixed point of a sequence of equations that is in a standard form.

Definition A sequence of equations ⟨X_{i} = E_{i} | i ∈ m⟩ is standard if each E_{i} is of the form

E ::= 0 | W | aX | E + E

(where X ranges over { X_{i} | i ∈ m } and W ranges over all other variables) and does not contain a free occurrence of X_{0}. A standard sequence ⟨X_{i} = E_{i} | i ∈ m⟩ can be regarded as a finite chart with states m, transitions i⟶^{a}j iff aX_{j} is a summand of E_{i}, visibilities i ▷ W iff W is a summand of E_{i} and initial state 0. It is accessible if ∀i ∈ m . 0⟶^{∗}i.

Lemma 20 For any μ-expression E there is a standard accessible sequence ⟨X̃ = Ẽ⟩ such that B ⊢ E = μ ⟨X̃ = Ẽ⟩.

Lemma 21 If ⟨X̃ = Ẽ⟩ is standard then ⟨X̃ = Ẽ⟩ ∼ μ ⟨X̃ = Ẽ⟩.

There is a natural ‘product’ definable over bisimilar standard sequences.

Definition If ⟨X_{i} = E_{i} | i ∈ m⟩, ⟨Y_{j} = F_{j} | j ∈ n⟩ are standard, accessible and bisimilar then we define a standard accessible sequence ⟨X̃ = Ẽ⟩ ⊗ ⟨Ỹ = F̃⟩ as follows. Let R ⊆ m × n be the largest bisimulation between the sequences considered as charts. It is clear that if i R j then

• if W is a summand of E_{i} then W is a summand of F_{j},

• if aX_{i′} is a summand of E_{i} then there is some j′ such that aY_{j′} is a summand of F_{j} and i′ R j′

(and symmetrically) and further that dom(R) = m, ran(R) = n and 0 R 0. Now

⟨X̃ = Ẽ⟩ ⊗ ⟨Ỹ = F̃⟩ =^{def} ⟨Y_{ij} = G_{ij} | i R j⟩,

where

G_{ij} =^{def}  ∑{ W | W is a summand of E_{i} and F_{j} }
+ ∑{ aY_{i′j′} | aX_{i′} is a summand of E_{i}, aY_{j′} is a summand of F_{j}
and i′ R j′ }.

Lemma 22 If ⟨X̃ = Ẽ⟩, ⟨Ỹ = F̃⟩ are standard, accessible and bisimilar then C ⊢ μ ⟨X̃ = Ẽ⟩ = μ (⟨X̃ = Ẽ⟩ ⊗ ⟨Ỹ = F̃⟩) and symmetrically.

Proof We show C ⊢ μ ⟨X̃ = Ẽ⟩ = μ ⟨Y_{ij} = G_{ij} | i R j⟩, with notation as in the previous definition. Take E′_{i} | i ∈ m to be

E′_{i} =^{def}  ∑{ W | W is a summand of E_{i} }
+ ∑{ aZ_{i′f} | ∀j . i R j ⇒ aY_{i′f(j)} is a summand of G_{ij} }.

It is straightforward to check that the equalities

E_{i} = E′_{i}[X_{k}/Z_{kf}]_{k∈m,f∈n^{n}}
G_{ij} = E′_{i}[Y_{k,f(j)}/Z_{kf}]_{k∈m,f∈n^{n}}

are provable from A1–5 so by Lemma 18 so are

μ ⟨X̃ = Ẽ⟩ = μ ⟨X̃ = Ẽ′[X_{k}/Z_{kf}]_{k∈m,f∈n^{n}}⟩
μ ⟨Y_{ij} = G_{ij} | i R j⟩ = μ ⟨Y_{ij} = E′_{i}[Y_{k,f(j)}/Z_{kf}]_{k∈m,f∈n^{n}} | i R j⟩.

It remains to note that

C ⊢ μ ⟨X̃ = Ẽ′[X_{k}/Z_{kf}]_{k∈m,f∈n^{n}}⟩ = μ ⟨Y_{ij} = E′_{i}[Y_{k,f(j)}/Z_{kf}]_{k∈m,f∈n^{n}} | i R j⟩.
□

Theorem 1 The axioms A1–5, B1–3 and { C_{mn} | m, n ∈ ω × ω } are sound and complete for bisimulation over μ-expressions.

Proof Completeness is immediate from Lemmas 20, 21 and 22. □

Complete subsets

This theorem can be sharpened somewhat. In the presence of C_{12} and A1–5 axiom B1 can be simplified to the following.

B1′  μXE = E , if X not free in E.

Further, it is clear that if m′ > m and n′ > n then any instance of C_{mn} is an instance of C_{m′n′} so it suffices to take enough instances of C_{mn} to cover ω × ω (with respect to the product ordering). One can then ask whether this is a necessary condition. We conjecture that it is but we know only that instances with arbitrarily large n are required (from the results of Chapter 3).

Relative axiomatisability

The axioms C_{mn} (and also A5, B1, B3) are all sound for infinite term equality of μ-expressions. It is therefore an immediate corollary of Theorem 1 that bisimulation is finitely equationally axiomatisable relative to infinite term equality, i.e. that A1–4, B2 and the implication

E =_{infinite term} F → E = F

are complete for bisimulation. In §4.4 we show that weak congruence is finitely equationally axiomatisable relative to bisimulation, and hence also relative to infinite term equality.

One could ask whether adding P 1 gives completeness for trace congruence. We conjecture that it does not. More generally one could ask whether it or any other equivalence in the linear-branching time spectrum is finitely equationally axiomatisable relative to infinite term equality. Answers to these questions would perhaps be of technical interest. Positive results would isolate the ‘non-finitely-equational’ part of the equivalences to the C_{mn}. Negative results would of course be stronger than simple non-finite-axiomatisability results for the same equivalence. They might nonetheless be easier to prove, being rather more focussed.

The commutative identities

A closely related infinite system has been given by Bloom and Ésik in [BÉ94]. We will simply state the result here, without doing justice to the bulk of their work (which is in a more general setting). We first need to define another n-ary fixed point operator.

Definition If X̃, Ẽ are n-tuples of variables and terms then μ̃X̃ Ẽ is an n-tuple of terms defined inductively:

μ̃XE =^{def} μXE
μ̃X̃X ẼE =^{def} (μ̃X̃Ẽ[μXH /X]), μXH

where H =^{def} E[μ̃X̃Ẽ /X̃]. The ith component of the tuple μ̃X̃Ẽ will be written μ̃_{i}X̃Ẽ.

There is a commutative identity for each m, n ≥ 1 and family of functions ρ_{ij}: n → n | i ∈ m, j ∈ n. As before, each identity loosely expresses the equality of an mstate transition system with one in which each state has been split into n bisimilar states. We let i, i′, k range over m and j, j′, l range over n. The commutative identity is then

\begin{matrix}∀i′ ∈ m, j′ ∈ n . & μ̃_{i′} ⟨X_{i} = E_{i}[X_{k}/Z_{kl}]_{k∈m,l∈n} | i ∈ m⟩ \\ = & μ̃_{i′j′} ⟨Y_{ij} = E_{i}[Y_{k,ρ_{ij}(l)}/Z_{kl}]_{k∈m,l∈n} | i ∈ m, j ∈ n⟩ \end{matrix}

in which the variables X_{k} and Y_{kl} are presumed not to occur free in any of the terms E_{i}. For the reader familiar with [BÉ94] this is just

μx.(t ∥ [R/x]) = (μy.t[y_{ρ}/x])_{ρ}

in notation which may be easier to understand at first sight, although perhaps harder to work with.

The following two axioms are also required. For the first it is assumed that Z does not occur free in E.

\begin{aligned}E1 & μZE[ZZ/XY] & = & μXμY E \\ E2 & μXE[F/X] & = & E[μXF [E/X] /X] \end{aligned}

These are the double iteration identity and the composition identity.

Theorem 2 ([BÉ94, Theorem 6.6]) The commutative identities together with axioms A1–5,B2,E1–2 are sound and complete for bisimulation over μ-expressions.

We conjecture that in the presence of a finite number of axioms (e.g. A5,B1– 3,E1–2) the commutative identities for m, n^{n} imply all the consequences of C_{mn}, which in turn imply all the consequences of the commutative identities for m, n.

2.3.2 Finite impure horn clause systems

A number of complete systems have been given that contain an impure horn clause expressing the fact that certain equations have unique solutions (together with a finite set of equational axioms). The first seems to be that for language equivalence of ∗-expressions by Salomaa [Sal66]. For μ-expressions there are complete systems for bisimulation [Mil84], weak congruence [Mil89], branching bisimulation congruence [Gla93a], divergence bisimulation [Gla93b] and trace congruence [Rab93]. We will reproduce the system of [Mil84] for bisimulation and sketch a completeness proof.

The axioms are A1–5,B1–2 together with rules for congruence, substitution and D:

D  E = F [E/X] ∧ X guarded in F → E = μXF

where X is guarded in F if every free occurrence of X in F is contained in a subexpression aG. We write ⊢ E = F if E = F is provable from these axioms.

The completeness proof below is a minor rearrangement of that given in [Mil84]. It is similar in structure to that of the previous subsection (in fact the latter was based on this). The definitions of standard sequences of equations and of the product of two bisimilar standard sequences are common. Now, however, instead of showing that expressions are provably equal to the fixed points of standard sequences they are shown to be provable solutions of standard sequences. The axiom D is then shown to imply an m-ary form, that certain sequences have provably unique solutions (this is the only place where D is required).

Definition A expression E is a provable solution of the equations ⟨X_{i} = E_{i} | i ∈ m⟩ if there exist expressions G_{i} | i ∈ m such that ⊢ E = G_{0} and ∀i ∈ m . ⊢ G_{i} = E_{i}[G̃/X̃]. It is a provably unique solution if for any E′ that is also a provable solution ⊢ E = E′.

Lemma 23 ([Mil84, Theorem 5.9]) For any expression E there is a standard accessible sequence ⟨X̃ = Ẽ⟩ for which E is a provable solution.

Lemma 24 If E is a provable solution of a standard ⟨X̃ = Ẽ⟩ then E ∼ ⟨X̃ = Ẽ⟩.

Proof Straightforward. □

Lemma 25 ([Mil84, Proof of Theorem 5.10]) If ⟨X̃ = Ẽ⟩, ⟨Ỹ = F̃⟩ are standard, accessible and bisimilar with provable solutions E, F then E, F are both provable solutions of ⟨X̃ = Ẽ⟩ ⊗ ⟨Ỹ = F̃⟩.

Definition A sequence of equations ⟨X_{i} = E_{i} | i ∈ m⟩ is guarded if each X_{i} is guarded in all the E_{j}. Clearly any standard sequence is guarded.

Lemma 26 ([Mil84, Theorem 5.7]) Any guarded sequence of equations has a provably unique solution.

Theorem 3 ([Mil84, Theorem 5.10]) The axioms A1–5, B1, B2, D are sound and complete for bisimulation over μ-expressions.

Proof Completeness is immediate from the above lemmas. □

2.3.3 Finite pure horn clause systems

The previously cited [BÉ94] by Bloom and Ésik also contains a finite pure horn clause system. We present a minor variant which has axioms A1–5, B2 and E1–3 together with rules for congruence and substitution. E3, also known as the GA implication, is given below. It is assumed that Z is not free in E or F.

E3 μZE[ZZ/XY] = μZF [ZZ/XY] → μZE[ZZ/XY] = μXF [μY E /Y]

We will give an outline of the completeness proof. It uses another implication — the functorial implication — which cannot be written as a single pure horn clause.

Definition The functorial implicationfor a surjective function ρ: m → n, where m, n ≥ 1, is

∀i ∈ m . E_{i}[Y_{ρ(j)}/X_{j}]_{j∈m} = F_{ρ(i)} → ∀i ∈ m . μ̃_{i}X̃ Ẽ = μ̃_{ρ(i)}Ỹ F̃

where X̃, Ẽ (resp. Ỹ , F̃) are m-tuples (resp. n-tuples) of variables and terms and it is supposed that no Y_{k} is free in any E_{i}.

The core of the completeness proof is Lemma 28 below which can be shown by induction on n.

Lemma 27 ([BÉ94, Lemma 7.5]) The axioms A5, E1–3 imply all instances of the functorial implication for functions ρ: m → 1.

Lemma 28 ([BÉ94, Lemma 7.4]) The axioms A5, E1–2 and the functorial implication for all ρ: m → 1 (m ≥ 1) imply all instances of the functorial implication for surjective ρ: m → n.

Lemma 29 ([BÉ94, Proof of Prop 7.1]) The axioms A5, E1–2 and the functorial implication for all ρ: m → n imply all instances of the commutative identity.

Theorem 4 ([BÉ94, Theorem 6.6]) The axioms A1–5, B2, E1–3 are sound and complete for bisimulation over μ-expressions.

Proof Completeness is immediate from the above lemmas and Theorem 2. □

We conjecture that E3 is also sound for weak congruence. If so then it follows that the axioms F 1–3, which are introduced in §4.4.1 in our proof that weak congruence is equational relative to bisimulation, are, together with A1–5, B1–3, E1–3, a finite pure horn clause axiomatisation of weak congruence over μ-expressions.

2.3.4 Systems for ∗-expressions

Unless stated otherwise all work mentioned in this subsection is with respect to language equivalence.

It has been shown that language equivalence of ∗-expressions is not finitely equational. Three proofs of this are sketched in [Con71]. The first was apparently given by Redko [Red64] and Salomaa in an incomplete form and later completed by Pilling. We will reproduce a sketch of the second, from [Con71, p.106], here to permit an easy comparison with our proof that bisimulation of μ-expressions is not finitely equational. Both intuitively say that any finite set of equations does not permit the introduction of arbitrary prime factors into the lengths of loops or iterates. Whether this can be made precise by giving a single proof for both cases is an interesting open question.

Theorem 5 (from [Con71 ]) Language equivalence of ∗-expressions is not finitely equationally axiomatisable.

\begin{aligned}C1 & A + 0 & = & A & C8 & A .(B + C) & = & (A . B) + (A . C) \\ C2 & A + B & = & B + A & C9 & (B + C) . A & = & (B . A) + (C . A) \\ C3 & (A + B) + C & = & A + (B + C) & C10 & (A . B) . C & = & A .(B . C) \\ C4 & A . 0 & = & 0 & C11 & (A + B)^{∗} & = & (A^{∗} . B)^{∗} . A^{∗} \\ C5 & 0 . A & = & 0 & C12 & (A . B)^{∗} & = & 1 + A .(B . A)^{∗} . B \\ C6 & A . 1 & = & A & C13 & (A^{∗})^{∗} & = & A^{∗} \\ C7 & 1 . A & = & A \end{aligned}

Figure 2–3: Axioms C1–13

Proof For any prime p there is a model A_{p} of the ∗-expressions in which all tautologies of less than a certain size are satisfied but others are not. The underlying set of the model is a set of 2^{p}+1 ∗-expressions over a distinguished action x ∈ Act:

|A_{p}| =^{def} {∑_{i∈I} x^{i} | I ⊆ {0, …, p − 1}} ∪ {x^{∗}} .

Using axioms C1–13 as in Figure 2–3 and the assumption x^{p} = 1 it can be shown that any ∗-expression over x is provably equal to a unique element of |A_{p}|, defining the operations of A_{p}. If σ is an environment, i.e. a function σ: Act → |A_{p}|, then we write [[E]]σ for the interpretation of a term E in A_{p}.

Let ≡ be the equivalence relation over |A_{p}| that identifies x^{∗} and ∑_{i∈p} x^{i}. It can be shown that ≡ is a congruence and that A_{p}/≡ satisfies all tautologies. On the other hand A_{p} clearly does not satisfy the tautology

C14.p  A^{∗} = (A^{p})^{∗} . ∑_{i∈p} A^{i}

at A = x. It remains to find, for any finite set of tautologies, a prime p such that all are satisfied by A_{p}.

Let the canonical ∗-expressions be the sums of terms, each of which is 0, 1 or contains no occurrence of 0, 1 or +. The length of such is the number of nonzero subterms. Any ∗-expression is provably equal to a canonical one, using C1–13. Further, any expression obtained from a canonical one by replacing actions by 0 or 1 is provably equal to a canonical one of the same or smaller length.

We show that any tautology E = F with E, F both canonical and of length less than p holds in A_{p}. Suppose not (for a contradiction), i.e. for some σ: Act → |A_{p}| that [[E]]σ ≠ [[F]]σ. We can assume w.l.g. that for all actions y occurring in E, F that σ(y) ∉ {0, 1} and further that [[E]]σ = ∑_{i∈p} x^{i} and [[F]]σ = x^{∗} (as A_{p}/ ≡ satisfies all tautologies). By soundness any action y occurring under a ∗ in E or F must occur under a ∗ in both. σ(y) must then be a single power x^{i}, otherwise [[E]]σ = x^{∗}. Let E′, F′ be E, F with all variables that do not occur under a ∗ replaced by 1. It can be shown that [[E′]]σ ≠ x^{∗} = [[F′]]σ so [[E′]]σ = ∑_{i∈p} x^{i}. There must therefore be p subterms of E′ (as each is a single power) which is a contradiction. □

Note that C14.p is not in general sound for bisimulation, so this proof cannot be trivially adapted to show the non-axiomatisability of bisimulation over ∗-expressions.

Turning to positive results, complete infinite systems have been given by Krob in [Kro91] and Bloom and Ésik in [BÉ93a].

The latter contains another set of commutative identities which are slightly awkward to state without introducing a lot of specialized notation. We need to consider matrices of ∗-expressions, defining sequential composition in the obvious fashion and the ∗ of a square matrix inductively on its size:

[ \begin{matrix}A & B \\ C & D \end{matrix} ]^{∗} =^{def} [ \begin{matrix}(A + B . D^{∗} . C)^{∗} & (A + B . D^{∗} . C)^{∗} . B . D^{∗} \\ (D + C . A^{∗} . B)^{∗} . C . A^{∗} & (D + C . A^{∗} . B)^{∗} \end{matrix} ] .

There is a commutative identity for each m ≥ n ≥ 1, surjective function ρ: m → n, family of functions ρ_{i}: m → m | i ∈ m that respect ρ, i.e. satisfy

∀i, j ∈ m . ρ(j) = ρ(ρ_{i}(j)),

and n × m matrix A of expressions A_{pi} | p ∈ n, i ∈ m. We first define an m × m matrix B by

B_{ij} =^{def} ∑_{k∈ρ_{i}^{−1}(j)} A_{ρ(i),k}

and an n × n matrix C by

C_{pq} =^{def} ∑_{k∈ρ^{−1}(q)} A_{pk}.

Viewing ρ as an m × n matrix with

ρ_{ip} = 1 , if ρ(i) = p
= 0 , otherwise,

the commutative identity is the n × m equations of

B^{∗} . ρ = ρ . C^{∗}.

Bloom and Ésik showed that the axiom

1^{∗} = 1

together with the two axioms above, the commutative identities, their duals (in a sense we leave undefined) and the semiring axioms C1–10 are complete.

The former contains the group identities proposed in [Con71]. For each finite group ⟨G, ∘, ^{−1}, I⟩ there is an identity over variables X_{g} | g ∈ G. Suppose G = {0, …, m − 1} and I = 0. We define an m × m matrix M by

M_{ij} =^{def} X_{i^{−1}∘j}.

The identity is then

[ 1 0 ⋯ 0 ] . M^{∗} . [ 1 ⋮ 1 ] = (∑_{g∈G} X_{g})^{∗} ,

which is the first equation of the commutative identity for n = 1, ρ(i) = 0, ρ_{i}(j) = i ∘ j, A_{1i} = X_{i}.

Krob showed that these identities for all finite groups G together with the axioms C1–13 and

(X . Y)^{∗} = 1 + X .(Y . X)^{∗} . Y
(X + Y)^{∗} = (X^{∗} . Y)^{∗} . X^{∗}

are complete.

They are not all sound for bisimulation — taking G to be the two element group {1, −1} with multiplication gives the identity

(a + b . a^{∗} . b)^{∗} + a^{∗} . b .(a + b . a^{∗} . b)^{∗} = (a + b)^{∗},

the left hand side of which can evolve via ⟶^{b} to a state which is not successfully terminated, which the right hand side cannot.

A finite equational system has been given by Yanov [Con71, p.108] that is complete for ∗-expressions E such that E = E + 1. Returning to bisimulation for a moment, a finite equational system has been given by Fokkink and Zantema [FZ94] for ∗-expressions of the form

E ::= a | 1 | E + E | E . E | E^{⋆}E.

It will be discussed in Chapter 4. It is not clear whether there is any precise connection between these results.

Two finite impure horn clause systems have been given by Salomaa in [Sal66], one of which has already been discussed. Finally, finite pure horn clause systems have been given by Arkhangelskii and Gorshkov [AG87], Boffa and Krob [Bof90, Kro91] and Kozen [Koz94]. Sample rules from these are

(E_{1} + E_{2})^{∗} . E_{3} = (F_{1} + F_{2})^{∗} . F_{3}
→
(E_{1} + E_{2})^{∗} . E_{3} = (F_{2} + F_{1} . E_{1}^{∗} . E_{2})^{∗} .(F_{3} + F_{1} . E_{1}^{∗} . E_{3})
E . E = E → E^{∗} = 1 + E
E . F + F = F → E^{∗} . F + F = F

respectively.

2.3.5 Infinitary rules and Denotational models

There is a large body of other work involving axiomatisations over process calculi, some of which is mentioned here for completeness. Firstly there is work (e.g. [BBK87,BW90]) on ACP using the Approximation Induction Principle. A family of unary operators π_{n} | n ∈ ω is introduced with transitions

{E⟶^{a}F \atop π_{n+1}(E)⟶^{a}π_{n}(F)}.

The AIP is then the implication

(∀n ∈ ω . π_{n}(E) = π_{n}(F)) → E = F.

It is sound for bisimulation over finitely branching labelled transition systems and can be used to give finite complete axiomatisations for a large class of process calculi, e.g. those that are GSOS definable [ABV92]. Being infinitary it does not fit in any of the classes of axiomatisation considered in §2.2. In [BK84] there is a variant of Milner’s system from [Mil84] (reproduced in §2.3.2) for a syntax close to our sequences of formal equations.

A number of axiomatisations for calculi of infinite state processes have been presented in a sequent style, for example in [CHM94,CHM93,Chr93,HS91,Hüt91]. It is not clear whether corresponding horn clause axiomatisations can be given, even allowing additional predicates such as ‘guardedness’ conditions.

In this thesis we are only concerned with axiomatising equivalences. Partial orders over processes have been introduced for several reasons — to match a notion of effective testing [Mil81], to allow for divergent [Wal88] and under-specified [CS90] processes and to allow a CPO-based denotational semantics [HP80,Hen81, Hen88,AH88,Abr91]. Walker gives in [Wal88] a complete system using a variant of the unique fixed point rule of [Mil84]. The CPO models admit infinitary rules such as ω-induction. We recall a definition from [Hen88] for term models which requires a definition of the syntactic approximants to a recursive term:

E^{0} =^{def} ⊥
X^{n+1} =^{def} X
(aE)^{n+1} =^{def} aE^{n+1}
(E + F)^{n+1} =^{def} E^{n+1} + F^{n+1}
(μXE)^{n+1} =^{def} E^{n+1}[(μXE)^{n}/X]

It is then

(∀n ∈ ω . E^{n} ≤ F) → E ≤ F

which again does not fit into any of the classes of axiomatisation considered in §2.2.

I expect that the following is known in the folklore but is perhaps worth pointing out in print. Bisimulation preorders such as those appearing in the above references work well for strong bisimulation but less so when one abstracts from certain actions. In particular any CPO equipped with continuous functions for a, b, c, τ and + that satisfies axioms A1–4 and ττX = τX will identify μ-expressions that are not even weak-completed-trace equivalent, e.g. writing τ^{ω} for μX τX and the standard semantic function as [[ ]]

[[aτ^{ω} + aτbτcτ^{ω}]] = [[aτ^{ω} + aτbτ^{ω} + aτbτcτ^{ω}]],

so when using such a model divergence can only be regarded as catastrophic.

Axiomatisation over μ-expressions

In this chapter we formulate and prove our main non-axiomatisability result, that there is no finite equational axiomatisation for bisimulation over μ-expressions.

To state the result a precise definition of the admissible equational axiomatisations is required, preferably as large as possible. For a syntax with variable binding, such as the μ-expressions, there does not seem to be a canonical definition. Consider for example the following three rules from [Mil84].

A4  E + E = E
B1  μXE = E[μXE /X]
D  E = F [E/X] ∧ X guarded in F → E = μXF

The last involves an implication and an additional predicate symbol — for either reason we would not call it an equational axiom. The first is formally an equation scheme, standing for the infinite set of equations obtained by replacing E by each μ-expression. Its schematic nature is harmless, however, as it could be replaced by the equation

X + X = X

38 Chapter 3. Axiomatisation over μ-expressions

with a standard inference rule of substitution. The second is again schematic but is not equivalent to any equation within the syntax of μ-expressions. Indeed, to equationally express anything of interest about fixed points, such as the simple properties below, some notation for substitution is required.

μXE = μXE[E/X]
B1  μXE = E[μXE /X]
E2  μXE[F/X] = E[μXF [E/X] /X]
C_{12} μX E[X, X, X, X] = μX E[X, X, μY E[X, Y, X, Y], μY E[X, Y, X, Y]]

To express these directly we could allow axioms containing substitutions and metavariables over terms (E, F) and variables (X, Y), together with a rather complicated rule for their instantiation. It would be awkward to characterise the sound axioms of this form, however, so instead we will embed the μ-expressions in a simply typed lambda calculus and work up to βη equality. Axioms such as the above can be written as equations containing variables of higher type rather than as equation schemes, with substitution appearing only in the rules defining βη equality. This simplifies the technical development and also gives added significance to some of the intermediate results as the terms of higher type can be viewed as a fragment of a higher order process calculus.

The main theorem, stated in §3.2, asserts the nonexistence of finite axiomatisations containing at most first order variables. These axiomatisations may contain (the translations of) schemes such as those above. Generalising the result to axiomatisations containing variables of arbitrary type is discussed in Chapter 6.

3.1 Outline of chapter

The proof rests on the fact that finite axiomatisations only provide bisimulations of certain ‘widths’, which we illustrate for the first axiom above. Writing a^{n} for \overbrace{a … a}^{n times}, repeated use of μXE = μXE[E/X] can change the length of a loop only by factors of 2, i.e. it can derive the ‘internal’ unfolding

μXa^{n}X = μXa^{2^{k}n}X

for any k ≥ 0 but not

μXa^{n}X = μXa^{pn}X

for any prime p > 2. We show that for any finite set of axioms there is some bound corresponding to this ‘2’.

The details are somewhat lengthy (occupying the remainder of this chapter) but may be of some independent interest. In particular, notions of higher order transition system and bisimulation are given which might be interesting when considering richer higher order calculi. We show a finite-state property and hence decidability of higher order bisimulation at arbitrary type.

The intermediate results can be applied to give an easy proof of the nonexistence of finite axiomatisations of bisimulation over calculi of ∗-expressions containing a zero process. This is done in Chapter 4, where it is related to the positive result of [FZ94] for BPA^{∗} (which has no zero).

In the next section we define the lambda calculus used and state the nonexistence result precisely. We then define an extensional equivalence ∼_{ext} over open terms that contains all sound equations and give a useful alternative characterisation of it. In §3.3 higher order transition systems and higher order bisimulation are defined and in §3.4 we show that all processes are ‘finite state’ in the appropriate sense and hence that higher order bisimulation is decidable. An inductive characterisation of the transitions of a substituted term is given in §3.5. In §3.6 higher order bisimulation and ∼_{ext} are shown to coincide over the base type terms containing first order variables (the T_{1}^{P} defined in the next section) — hence all sound axioms lie within finite higher order bisimulations. Finally in §3.7 we construct from these bisimulations an equivalence over terms which is preserved by all proofs. A pair of bisimilar but inequivalent terms is then picked out.

3.2 Basic definitions

From now on we shall be considering terms of a simply typed lambda calculus with a single base type P of processes and the following constants:

0 : P

a: P → P for each a ∈ Act
+ : P → P → P
fix :(P → P) → P

We will usually work up to βη equality, using abstraction to allow parameterised equations. This is in contrast to taking β-reduction to be of comparable computational interest to the labelled transitions, e.g. in the work of Nielson [Nie89].

Notation and definitions will be taken from [Mit90]. In particular we write typing judgements and typed equations as Γ ▷ E: σ and Γ ▷ E = F : σ, where E, F are terms, σ is a type, Γ an assignment of types to a finite set of variables. The inference rules for typing and βη equality are reproduced in Figure 3–1. It is presumed wherever Γ, x: α appears that x does not occur in Γ and further that the terms appearing in a typed equation Γ ▷ E = F : σ are both typable with type σ in Γ. There is an unfortunate clash of notation between the ▷ of typing judgments and the visibility predicate ▷. As both are standard we make only a small typographical distinction — it should be clear from context which is intended. If E a set of typed equations we write E ⊢ Γ ▷ E = F : σ to mean that Γ ▷ E = F : σ is derivable from E using the rules in Figure 3–1 — formally, that it is derivable by those rules augmented by

Γ ▷ E = F : σ (Γ ▷ E = F : σ) ∈ E.

We sometimes elide existentially quantified Γ.

The order of a type is as usual:

order(P) = 0
order(σ → τ) = max{1 + order(σ), order(τ)}.

We take some type assignment K with a countable infinity of variables at each type. For k ∈ ω ∪ {ω} we write T_{k}^{σ} for the set of terms E for which there is some finite Γ ⊆ K, containing only variables of order ≤ k, such that Γ ▷ E: σ. In particular T_{0}^{σ} contains terms of type σ whose only free variables are of type P.

There is an obvious bijection between the μ-expressions and the long βη normal forms in T_{0}^{P} with for example

μXaY + X ↔ fix λx: P. + (ay) (x).

For any equivalence over μ-expressions this induces an equivalence over T_{0}^{P}, closing under βη equality.

Definition An axiomatisation for an equivalence ∼ over μ-expressions is a set E of typed equalities that is sound, i.e.

∀E, F ∈ T_{0}^{P} . E ⊢ E = F : P ⇒ E ∼ F

x: σ ▷ x: σ var  {} ▷ c: σ cst

{Γ ▷ M : σ \atop Γ, x: τ ▷ M : σ} addhyp

{Γ, x: σ ▷ M : τ \atop Γ ▷(λx: σ. M) : σ → τ} → Intro  \begin{matrix}Γ ▷ M : σ → τ & Γ ▷ N : σ \\ Γ ▷ MN : τ \end{matrix} → Elim

{Γ ▷ M = N : σ \atop Γ, x: τ ▷ M = N : σ} addhyp  Γ ▷ M = M : σ ref

{Γ ▷ M = N : σ \atop Γ ▷ N = M : σ} sym  \begin{matrix}Γ ▷ L = M : σ & Γ ▷ M = N : σ \\ Γ ▷ L = N : σ \end{matrix} tran

{Γ, x: σ ▷ M = N : τ \atop Γ ▷(λx: σ. M) = (λx: σ. N) : σ → τ} ξ \begin{matrix}Γ ▷ M = M′: σ → τ & Γ ▷ N = N′: σ \\ Γ ▷ MN = M′N′: τ \end{matrix} μ

{y ∉ F V (M) \atop Γ ▷ λx: σ. M = λy: σ. M[y/x] : σ → τ} α

Γ ▷(λx: σ. M)N = M[N/x] : τ β  {x ∉ F V (M) \atop Γ ▷ λx: σ. (Mx) = M : σ → τ} η

Figure 3–1: Lambda calculus and complete, i.e.

∀E, F ∈ T_{0}^{P} . E ⊢ E = F : P ⇐ E ∼ F.

We assume w.l.g. that E contains only equalities at type P (otherwise they can be applied to new variables of appropriate types).

Note that if ∼ is not both a congruence for a, +, μX and substitutive (i.e. E ∼ F ⇒ E[G/x] ∼ F [G/x]) then there can be no axiomatisation in this sense. Further, bisimulation is a substitutive congruence.

Some candidate axioms (corresponding to the axiom schemes given earlier) are given below, taking Γ = {e: P → P, f : P → P, z: P → P → P → P → P }.

Γ ▷ fix e = fix λx: P. e(ex) : P
B1 Γ ▷ fix e = e(fix e) : P
E2 Γ ▷ fix λx: P. e(fx) = e(fix λx: P. f(e(x))) : P
C_{12} Γ ▷ fix λx: P. zxxxx = fix λx: P. zxx(fix λy: P. zxyxy)(fix λy: P. zxyxy) : P

They can all be shown sound for bisimulation by using Theorem 8 below. Clearly any of the axioms of the infinite system given in §2.3.1 could be written in this form.

We define the order of a finite set of typed equalities to be the maximum order of any variable (free or bound) therein. The main theorem can now be stated.

Theorem 6 If Act is non-empty there is no finite axiomatisation of order ≤ 1 for any substitutive congruence ∼ finer than (or identical to) bisimulation that for all n ≥ 1 satisfies

μXaX ∼ μXa^{n}X.

The restriction to axioms of order ≤ 1 simplifies the problem considerably, as we will discuss later. We have yet to prove the result without it but note that the candidate axioms above are all of order 1, supporting the view that it admits an interestingly rich class of axioms.

In the rest of this section we characterise the sound axioms.

Definition If ρ is a substitution with a finite domain that includes the free variables of E_{1}, E_{2}, … and for all x: σ in its domain ρ(x) ∈ T_{0}^{σ} then we say that ρ is a substitution for E_{1}, E_{2}, . . ..

Definition If ∼ is a substitutive congruence over μ-expressions the relation ∼_{ext} over T_{ω}^{P} is given by

E ∼_{ext} F iff for all substitutions ρ for E, F we have Eρ ∼ F ρ.

Sound axioms clearly lie within ∼_{ext}. For the converse we give another characterisation.

Definition If E = { Γ_{i} ▷ M_{i} = N_{i}: P | i ∈ I } is a set of typed equations then the relation =_{E} over T_{0}^{P} is the smallest equivalence such that:

• If ρ is a substitution for M_{i}, N_{i} then M_{i}ρ =_{E} N_{i}ρ.

• =_{E} is a congruence for contexts of the form

C ::= | x | 0 | aC | C + C | fix λx: P. C.

• =_{E} is closed under βη equivalence.

Proposition 30 If M, N ∈ T_{0}^{P} then E ⊢ M = N : P iff M =_{E} N.

Corollary 31 If ∼ is a substitutive congruence over μ-expressions then a set of typed equations E is sound for ∼ iff E ⊆∼_{ext}.

Proof (of Proposition 30)

We need two facts about derivations of typing and typed equality judgements:

Lemma 32 If E ⊢ Γ ▷ M = N : σ then there is a derivation in which all instances of μ have an instance of ref as one premise and all rules below an instance of tran are themselves instances of tran.

Proof We write derivations of typed equalities in a linear syntax, using the rule names, not in tree form. The proof is via two rewrite systems over derivations of typed equalities. The first, generated by the rule

μ(d, e) ↦ tran(μ(d, ref ()), μ(ref (), e)), if d ≠ ref () ≠ e

clearly terminates as it reduces the number of redexes and the normal forms satisfy the first condition. The second, generated by the rules

μ(tran(d, e), ref ()) ↦ tran(μ(d, ref ()), μ(e, ref ()))
μ(ref (), tran(d, e)) ↦ tran(μ(ref (), d), μ(ref (), e))
add hyp(tran(d, e)) ↦ tran(add hyp(d), add hyp(e))
sym(tran(d, e)) ↦ tran(sym(d), sym(e))
ξ(tran(d, e)) ↦ tran(ξ(d), ξ(e)),

terminates as it reduces the total number of rules below each instance of tran. It introduces no redexes of the first so the normal forms satisfy both conditions of the lemma. □

Lemma 33 If Γ, z: σ ▷ G: τ, {} ▷ M : σ and {} ▷ N : σ then there exists some n and G_{j} | j ∈ 1..n such that:

• Γ, z: σ ▷ G_{j}: τ.

• G_{j} is in long βη normal form and contains at most one free occurrence of z.

• G[M/z] =_{βη} G_{1}[M/z], G_{n}[N/z] =_{βη} G[N/z] and ∀j ∈ 1..n − 1 . G_{j}[N/z] =_{βη} G_{j+1}[M/z].

Proof Let H_{1} be the normal form of G and define H_{k+1} by substituting N for the leftmost occurrence of z in H_{k} and taking the normal form. Let n be the least such that H_{n} has at most one occurrence of z (n must exist as otherwise G[N/z] is not strongly normalising) and for i ∈ 1..n substitute M for all except the leftmost occurrence of z in H_{i} and let G_{i} be the normal form thereof. □

Now we can prove Proposition 30. The right-to-left implication is trivial. For the left-to-right we suppose that d is a derivation of E ⊢ Γ ▷ M = N : P in the form of Lemma 32 and show M =_{E} N by induction on d. Either the bottom rule in d is an instance of tran and the induction hypothesis can be used or d contains no instances of tran. The unique top rule in d is then either one of ref , α, β, η in which case M =_{βη} N and so M =_{E} N, or an axiom Γ_{i} ▷ M_{i} = N_{i}: P. Suppose Γ_{i} = x_{1} : σ_{1}, …, x_{n}: σ_{n}. There is a term G and new variable z such that

Γ, z: σ_{1} → ⋯ σ_{n} → P ▷ G: P

G[λx_{1} : σ_{1}. · · · λx_{n}: σ_{n}. M_{i} /z] =_{βη} M
G[λx_{1} : σ_{1}. · · · λx_{n}: σ_{n}. N_{i} /z] =_{βη} N.

It now suffices to use Lemma 33 and note that G_{j}[λx_{1} : σ_{1}. · · · λx_{n}: σ_{n}. M_{i} /z] =_{E} G_{j}[λx_{1} : σ_{1}. · · · λx_{n}: σ_{n}. N_{i} /z]. □

We note that, taking ∼ to be bisimulation, ∼_{ext} is a congruence in the following sense.

Proposition 34 If E ∼_{ext} F and E′ ∼_{ext} F′ then aE ∼_{ext} aF, +EE′ ∼_{ext} +F F′ and fix λx: P. E ∼_{ext} fix λx: P. F.

Proof Straightforward, using the analogous properties of ∼ from Proposition 7.

□

3.3 Higher order bisimulation

To show a non-axiomatisability result we need to capture some limitation of any finite set of sound axioms. To do this a more intensional characterisation of ∼_{ext}, without its quantification over all substitutions, is required. A suitable equivalence is defined below in two steps. Firstly a notion of higher order transition system is given and then higher order bisimulation (written ∼_{ho}) is defined over it. We generalise the definition of bisimulation over open μ-expressions in [Mil84], reproduced in §2.1.1. There (where variables are all of ‘type P ’) an extended transition system is defined over μ-expressions consisting of the usual labelled transitions together with predicates E ▷ X (pronounced ‘E sees X’ or ‘X is visible in E’). An extended bisimulation then requires matching of visibilities at each state, as well as transitions, and can be shown equal to the relevant special case of ∼_{ext}. The essential fact about these visibility predicates is that the transitions of a μ-expression E[F/X] can be calculated from the visibilities of E and the transitions of E and F. In this work variables may be of higher type and so applied to arguments (which may themselves be of higher type), so we need a more sophisticated visibility predicate to get an analogous result. The restriction to low order variables is not yet needed so this is all still over terms with free variables of arbitrary type, i.e. the terms T_{ω}^{P}.

Notation From now on we take all terms mentioned to be in normal form unless stated otherwise and work up to alpha equivalence when convenient. We write + infix except when emphasizing the distinction between lambda calculus terms and others. Bisimulation over T_{0}^{P} will be written ∼.

Definition Take the relations ⟶^{a} | a ∈ Act and ▷ to be the least over normal forms in T_{ω}^{P} such that

aE⟶^{a}E  E ▷ E

{E⟶^{a}E′ \atop E + F ⟶^{a}E′} and sym.  {E ▷ E′ \atop E + F ▷ E′} and sym.

{E⟶^{a}E′ \atop fix λy: P. E⟶^{a}E′[fix λy: P. E /y]} {E ▷ E′ \atop fix λy: P. E ▷ E′[fix λy: P. E /y]}

We will usually only be concerned with visibility judgments of the form E ▷ xF̃. For example consider the term

E =^{def} fix λy: P. by + x(zx + y)

with {x: P → P, z:(P → P) → P } ▷ E: P. We have

\begin{aligned}& E⟶^{b}E \\ and & E ▷ x(zx + E). \end{aligned}

There are a number of simple properties of the transition and visibility relations that will be used without comment.

Lemma 35 For all E, F, G ∈ T_{ω}^{P} and substitutions ρ:

• If E⟶^{a}F then Eρ⟶^{a}F ρ.

• If E ▷ F then Eρ ▷ F ρ.

• If E ▷ F ⟶^{a}G then E⟶^{a}G.

• If E ▷ F ▷ G then E ▷ G.

3.3. Higher order bisimulation 47

• If E⟶^{a}F then F V (F) ⊆ F V (E).

• If E ▷ F then F V (F) ⊆ F V (E). Proof Straightforward inductions on the derivations of the judgments. □ Higher order bisimulation is defined using this transition system. Definition If R is a relation on T_{ω}^{P} then the typed relations R̂^{σ} over T_{ω}^{σ} are given by

• R̂^{P} = R

• E R̂^{σ → τ} F iff for all x: σ ∈ K, if x is not free in E, F then Ex R̂^{τ} F x. Note that we are writing Ex for its normal form, according to the convention above. Notation We abbreviate the application ((xE_{1}) …)E_{n} by xẼ, in which x is typically assumed to be of a type σ_{1} → … σ_{n} → P. Definition A relation R over T_{ω}^{P} is a higher order bisimulation if E R F implies

• If E⟶^{a}E′ then ∃F′ . F ⟶^{a}F′ ∧ E′ R F′.

• If E ▷ xẼ then ∃F̃ . F ▷ xF̃ ∧ ∀i . E_{i} R̂^{σ_{i}} F_{i}. and symmetrically. We write ∼_{ho} for the union of all higher order bisimulations and ∼_{ho}^{σ} for ˆ ∼_{ho}^{σ}. Proposition 36 ∼_{ho} is a higher order bisimulation and is an equivalence relation. Proof Straightforward except for transitivity where Proposition 38 is needed. □ For example, if

E =^{def} fix λx: P. y(yx)
F =^{def} fix λx: P. yx,

then E ∼_{ho} F is shown by taking a relation {⟨E, F ⟩, ⟨yE, F ⟩}, the only relevant visibilities or transitions being

\begin{matrix}E ▷ y(y(E)) & F ▷ yF \\ yE ▷ yE & F ▷ yF. \end{matrix}

The terms in the T_{ω}^{σ} can be viewed as a small fragment of the higher order π calculus of [San93], taking a single object sort s ↦ () and the agents without parallel composition, restriction, infinitary sum, matching, variables of sorts containing s or infinitely many/higher order defined constants. This is discussed further in §4.2.

3.4 Finite state and decidability properties

As we are working with a mild generalization of finite state processes it is to be expected that all higher order bisimulations between them are in some sense finitely generated. In the sequel we need only the following result for terms in T_{1}^{P}.

Definition The derivatives of a term E ∈ T_{1}^{P} are der(E) =^{def} { F ∈ T_{1}^{P} | E⇝^{∗}F }, where ⇝ is the least relation over T_{1}^{P} such that

E⟶E′ ⇒ E⇝E′
E ▷ xẼ ⇒ ∀i . E⇝E_{i}.

This generalises the standard definition for transition systems.

Lemma 37 If E ∈ T_{1}^{P} then der(E) is finite. Further if E ∼_{ho} F then there is a higher order bisimulation contained in der(E) × der(F) relating them.

Proof This is a special case of Corollary 46 and Proposition 47 below. □

In the rest of this section we show a generalization of this result for terms in T_{ω}^{P} containing free variables of arbitrary types and hence the decidability of higher order bisimulation for arbitrary terms. This is slightly subtle as any higher order bisimulation between non-trivial terms in T_{ω}^{P} must be infinite. We will need to know that higher order bisimulation preserves sets of free variables.

Proposition 38 If E ∼_{ho} F then F V (E) = F V (F).

Proof We show that free variables are accessible via the transition system in a sense that is preserved by higher order bisimulation.

Notation V ranges over sets of variables such that each V^{σ} and K^{σ} − V^{σ} is infinite.

Definition For a set V of variables ⇝_{V} is the least relation over normal forms in T_{ω}^{P} such that

E⟶E′ ⇒ E⇝_{V}E′
E ▷ xẼ ∧ z̃ ∩ (F V (E_{i}) ∪ V) = {} ⇒ E⇝_{V}E_{i}z̃.

Lemma 39 If E⇝_{V}F then for all terms G, variables w ∈ V^{P} and substitutions ρ with dom(ρ)∪ran(ρ) ⊆ K−V there exists ρ′ with dom(ρ′)∪ran(ρ′) ⊆ K − V such that Eρ[G/w]⇝_{V}F ρ′[G/w].

Proof If E⟶^{a}F we can take ρ′ = ρ, otherwise E ▷ yẼ and F = E_{i}z̃ with z̃ ∩ (F V (E_{i}) ∪ V) = {}. Take some z̃′ such that z̃′ ∩ (F V (E_{i}) ∪ V ∪ F V (E_{i}ρ[G/w]) ∪ dom(ρ)) = {} and put ρ′ = [z̃′/z̃] ∘ ρ. □

Corollary 40 If E⇝_{V}^{n} ▷ xẼ, x ∈ V and ρ is a substitution with dom(ρ) ∪ ran(ρ) ⊆ K − V then there exists Ẽ′ such that Eρ⇝_{V}^{n} ▷ xẼ′.

Corollary 41 If E⇝_{V}^{∗} ▷ xẼ and {x, y} ⊆ V then there exists Ẽ′ such that fix λy: P. E⇝_{V}^{∗} ▷ xẼ′.

Proof Both are simple inductions along ⇝_{V}^{n}. □

Lemma 42 x ∈ F V (E) iff ∀V . x ∈ V ⇒ ∃Ẽ . E⇝_{V}^{∗} ▷ xẼ.

Proof ⇒: By induction on E, using Corollary 41 for the fix case. ⇐: If E⇝_{V}^{∗}F then the free variables of F are either present in E or not in V. □

Suppose x ∈ F V (E). Take any V containing F V (E) ∪ F V (F). By Lemma 42 E⇝_{V}^{n} ▷ xẼ. By induction on n we can show F ⇝_{V}^{n} ▷ xF̃ (using Corollary 40) then by Lemma 42 x ∈ F V (F). □

We give an alternative definition of higher order bisimulation that is not necessarily infinite.

Definition If R is a relation on T_{ω}^{P} then the typed relations \overline{R}^{σ} over T_{ω}^{σ} are given by

• \overline{R}^{P} = R

• E \overline{R}^{σ → τ} F iff there exists x: σ ∈ K that is not free in E, F such that Ex \overline{R}^{τ} F x.

Definition Such an R is a loose higher order bisimulation if E R F implies

• If E⟶^{a}E′ then ∃F′ . F ⟶^{a}F′ ∧ E′ R F′.

• If E ▷ xẼ then ∃F̃ . F ▷ xF̃ ∧ ∀i . E_{i} \overline{R}^{σ_{i}} F_{i}.

and symmetrically.

A loose higher order bisimulation generates a higher order bisimulation as follows.

Definition If R is a relation on T_{ω}^{P} then E Cl(R) F iff there exists an injective type-respecting substitution ρ: F V (E, F) → K such that Eρ R F ρ.

Proposition 43 If R is a loose higher order bisimulation then Cl(R) is a higher order bisimulation.

Proof

Lemma 44 If E \overline{R}^{σ} F then for all injective ρ: F V (E, F) → K we have

Eρ { \atop Cl(R)}^{σ} F ρ.

Proof By induction on the type σ. □

We now check that Cl(R) is a higher order bisimulation. Suppose E Cl(R) F, i.e. for some ρ that Eρ R F ρ. If E⟶^{a}E′ then Eρ⟶^{a}E′ρ so (as R a loose higher order bisimulation) there is some B such that F ρ⟶^{a}B R^{−1} E′ρ. Now ρ is invertible so

F = F ρρ^{−1}⟶^{a}Bρ^{−1} and moreover E′ Cl(R) Bρ^{−1}.

Suppose E ▷ xẼ, then Eρ ▷ ρ(x)(Ẽρ) so F ρ ▷ ρ(x)B̃ with ∀i . E_{i}ρ \overline{R}^{σ_{i}} B_{i}. Now

F ▷ x(B̃ρ^{−1}) and by Lemma 44 ∀i . E_{i} { \atop Cl(R)}^{σ_{i}} B_{i}ρ^{−1}. □

Given terms E, F and a higher order bisimulation R with E R F we shall now show that it is possible to make particular choices of their derivatives such that these are finite and R restricted to them is a loose higher order bisimulation.

We suppose some total order, isomorphic to the naturals, on each K^{σ} and that V ⊆ K is a set of variables with each V^{σ} and K^{σ} − V^{σ} infinite. We let f range over computable type-respecting partial functions K → P_{fin}K with finite and computable domain. They are extended to total functions f : P_{fin}K → P_{fin}K by

f(A) =^{def} (A − dom(f)) ∪ ⋃{ f(a) | a ∈ A ∩ dom(f) }.

The function with empty domain will be written {}. These functions will be used to calculate the free variables of subterms in their original contexts.

Definition The full application of a term is given by

E ∗_{f} =^{def} E for E: P
E ∗_{f} =^{def} (Ex) ∗_{f} for E: σ → τ,

where x is the first variable in (K^{σ} − V^{σ}) − f(F V (E)).

Definition The f-derivatives of a term E ∈ T_{ω}^{P} are der_{f}(E) =^{def} { F ∈ T_{ω}^{P} | E⇝_{f}^{∗}F } where ⇝_{f} is the least relation over T_{ω}^{P} such that

E⟶E′ ⇒ E⇝_{f}E′
E ▷ xẼ ⇒ ∀i . E⇝_{f}E_{i} ∗_{f} .

The proper f-derivatives of E are der_{f}^{+}(E) =^{def} { F ∈ T_{ω}^{P} | E⇝_{f}^{+}F }.

Proposition 45 If R is a higher order bisimulation with E R F then Q =^{def} R ∩ (der_{{}} E × der_{{}} F) is a loose higher order bisimulation.

Proof We can show E R̂^{σ} F ⇒ E ∗_{\{\}} R F ∗_{\{\}} and E ∗_{\{\}} Q F ∗_{\{\}} ⇒ E \overline{Q}^{σ} F by induction on types using Proposition 38. The result is then straightforward. □

Corollary 46 E ∼_{ho} F iff there is a loose higher order bisimulation contained in der_{{}} E × der_{{}} F.

52 Chapter 3. Axiomatisation over μ-expressions Proof Immediate from Propositions 43 and 45. □ Proposition 47 The set of f-derivatives der_{f}(E) of a term is finite and computable. Proof

Lemma 48 If x ∈ V then ∀F ∈ T_{ω}^{σ} . F ∗_{f⊕x↦f(F V (E)−{x})}[fix λx: P. E /x] = F [fix λx: P. E /x] ∗_{f}. Proof Induction on σ. □ Lemma 49 If x ∈ V then ∀n . E[fix λx: P. E /x]⇝_{f}^{≤n}F ⟺ ∃E′ . E⇝_{f⊕x↦f(F V (E)−{x})}^{≤n}E′ ∧ E′[fix λx: P. E /x] = F. Proof Induction on n. □

It is now straightforward to show by induction on E that ∀f . der_{f}^{+}(E) is finite and computable. □ Corollary 50 ∼_{ho} is decidable. Proof By Corollary 46, to decide E ∼_{ho} F we need only consider the set of relations contained in der_{{}} E × der_{{}} F. This set is finite and computable and moreover it is clearly decidable whether any element of it is a loose higher order bisimulation. □ We note that ∼_{ho} is also a congruence in a limited sense, although this fact will not be used until Chapter 6. Proposition 51

1. If E ∼_{ho} F and E′ ∼_{ho} F′ then aE ∼_{ho} aF, +EE′ ∼_{ho} +F F′ and fix λx: P. E ∼_{ho} fix λx: P. F.

2. If E ∼_{ho}^{τ} F and x: σ then λx: σ. E ∼_{ho}^{σ → τ} λx: σ. F.

3. If E ∼_{ho}^{σ} F and x: σ → τ then xE ∼_{ho}^{τ} xF.

4. If E ∼_{ho}^{σ → τ} F and x: σ ∉ F V (E) ∪ F V (F) then Ex ∼_{ho}^{τ} F x.

Proof The only interesting part is the fix case of 1, for which it suffices to check that

{ E[fix λx: P. G /x], F [fix λx: P. G /x] | E, F, G ∈ T_{ω}^{P} and E ∼_{ho} F }

is a loose higher order bisimulation. □

3.5 The transition system of a substituted term

In this section we consider the transitions of a substituted term such as Eρ. The transition and visibility predicates are related by the following.

Lemma 52 If E ∈ T_{ω}^{P}, ρ is a substitution for E and Eρ⟶^{a}A then either E⟶^{a}E′

and E′ρ = A or E ▷ xẼ and ρ(x)(Ẽρ)⟶^{a}A.

Proof Induction on the derivation of Eρ⟶^{a}A. □

In general there will be a complex pattern of β reduction involved in reducing the ρ(x)(Ẽρ) term appearing above to normal form. If E ∈ T_{1}^{P} and E and ran(ρ) are all in normal form, however, it is simple, allowing a direct inductive characterisation of the transitions of Eρ. The rest of this section is devoted to giving that characterisation.

For the remainder of the chapter we consider only terms in T_{1}^{P}, i.e. terms of type P containing at most first order variables. We discuss whether this restriction can be removed in §6.1.

We consider a substitution ρ with a finite domain containing at most first order variables and a range with variables only of type P. We suppose that dom(ρ) ∩ F V (ran(ρ)) = {}. We further suppose w.l.g. that there is a set Z ⊆ K of variables disjoint from dom(ρ) and F V (ran(ρ)) and for all y: \underbrace{P → ⋯ → P}_{n times} → P ∈ dom(ρ)

that ρ(y) is of the form

λz_{1} : P. · · · λz_{n}: P. H_{y}

for a term H_{y}, with each z_{i} ∈ Z.

In the sequel y ranges over dom(ρ), z over Z^{P} and x over K^{P} − dom(ρ) − Z.

54 Chapter 3. Axiomatisation over μ-expressions Definition The relation ▷_{ρ} ⊆ T_{1}^{P} × (K^{P} − dom(ρ) − Z) is the least such that

1. E ▷ x ⇒ E ▷_{ρ} x

2. E ▷ yẼ ∧ H_{y} ▷ x ⇒ E ▷_{ρ} x

3. E ▷ yẼ ∧ H_{y} ▷ z_{j} ∧ E_{j} ▷_{ρ} x ⇒ E ▷_{ρ} x. For a ∈ Act let ⟶_{ρ}^{a} ⊆ T_{1}^{P} × T_{1}^{P} be the least relation such that

1. E⟶^{a}F ⇒ E⟶_{ρ}^{a}F

2. E ▷ yẼ ∧ H_{y}⟶^{a}H′ ⇒ E⟶_{ρ}^{a}H′[Ẽ/z̃]

3. E ▷ yẼ ∧ H_{y} ▷ z_{j} ∧ E_{j}⟶_{ρ}^{a}B ⇒ E⟶_{ρ}^{a}B.

Proposition 53 These relations agree with the transition system, i.e.

Eρ ▷ x ⟺ E ▷_{ρ} x
Eρ⟶^{a}B ⟺ ∃F . E⟶_{ρ}^{a}F ∧ F ρ = B.

Proof The right-to-left implications are straightforward inductions. To show the others we first pick out a controlled sub-relation of the β reduction of Eρ.

Definition Let the relation ⟶_{β} ⊆ T_{1}^{P} × T_{1}^{P} be the least relation such that

1. yẼ ⟶_{β} H_{y}[Ẽ/z̃]

2. E ⟶_{β} F ⇒ fix λw: P. E ⟶_{β} fix λw: P. F

3. (E_{j} ⟶_{β} E′_{j} ∧ ∀i ≠ j . E_{i} = E′_{i}) ⇒ cẼ ⟶_{β} cẼ′ for any constant or

variable c. This is related to βη equality by the following. Lemma 54 For all E there is some F such that E ⟶_{β}^{∗} F and F V (F) ∩ dom(ρ) = {}. Proof One can show that otherwise Eρ has an infinite sequence of β reductions. □

3.6. The coincidence of ∼_{ext} and ∼_{ho} 55

Lemma 55 If E ⟶_{β} F then Eρ = F ρ.

Proof Induction on E ⟶_{β} F. □

It is related to the transition relation by

Lemma 56 If E ⟶_{β} F ⟶_{ρ}^{a}H then for some G E⟶_{ρ}^{a}G ⟶_{β}^{∗} H. Further, if E ⟶_{β} F ▷_{ρ} x then E ▷_{ρ} x.

Proof By somewhat tedious inductions on derivations of ⟶_{β}. □

Now suppose Eρ⟶^{a}B. By Lemmas 54 and 55 there is an F such that E ⟶_{β}^{∗} F and Eρ = F ⟶^{a}B. By the definition of ⟶_{ρ}^{a} we have F ⟶_{ρ}^{a}B so using Lemma 56 we have E⟶_{ρ}^{a}A ⟶_{β}^{∗} B for some A. Finally by Lemma 55 we have Aρ = B.

Suppose Eρ ▷ x. As before there is an F such that E ⟶_{β}^{∗} F and Eρ = F ▷ x. By the definition of ▷_{ρ} we have F ▷_{ρ} x so using Lemma 56 we have E ▷_{ρ} x. □

3.6 The coincidence of ∼_{ext} and ∼_{ho}

We now show that over T_{1}^{P} the equivalences ∼_{ext} and ∼_{ho} coincide.

Theorem 7 If Act is nonempty and E ∼_{ext} F then E ∼_{ho} F.

Proof Suppose there is some action a ∈ Act. By Lemma 37 there is a largest N such that some derivative of E or F is higher order bisimilar to a^{N}0 (take N = 0 if there are none such). Using this we construct a substitution ρ for E, F. For

y: \underbrace{P → ⋯ → P}_{m times} → P put

ρ(y) =^{def} λz_{1} : P. · · · λz_{m}: P. aA_{y}
A_{y} =^{def} a0 + a^{N+3+y}0 + ∑_{i∈1..m} aB_{i}
B_{i} =^{def} a^{2i}0 + a^{2i+1}z_{i}

(eliding some injective function from variables to the naturals). The following three lemmas show that ρ is sufficiently discriminating.

Lemma 57 If E′ ∈ der(E) ∪ der(F) then ∀G̃ . E′ρ ≁_{ho} A_{y}[G̃ρ /z̃].

Proof Suppose not, then E′ρ⟶^{a} ∼_{ho} P =^{def} a^{N+2+y}0. By Lemma 52

either E′⟶^{a}E′′ ∧ E′′ρ ∼_{ho} P or E′ ▷ y′Ẽ ∧ A_{y′}[Ẽρ /z̃] ∼_{ho} P. Both

contradict the definition of ρ. □

Lemma 58 If y ≠ y′then ∀Ẽ, F̃ . A_{y}[Ẽ/z̃] ≁_{ho} A_{y′}[F̃/z̃].

Proof The transition to a^{N+2+y}0 of the left hand side cannot be matched by the right. □

Lemma 59 If A_{y}[Ẽ/z̃] ∼_{ho} A_{y}[F̃/z̃] then ∀i . E_{i} ∼_{ho} F_{i}.

Proof Straightforward, by consideration of the ways in which a transition A_{y}[Ẽ/z̃]⟶^{a}B_{i}[Ẽ/z̃] can be matched. □

We can now check that

R =^{def} { E′, F′ | E′ ∈ der(E), F′ ∈ der(F) and E′ρ ∼_{ho} F′ρ }

is a higher order bisimulation. Consider E′ R F′ and suppose E′⟶^{b}E′′. By

Lemma 35 E′ρ⟶^{b}E′′ρ so F′ρ⟶^{b} ∼ E′′ρ. By Lemma 52 either F′⟶^{b}F′′ ∧ F′′ρ ∼

E′′ρ — then E′′ R F′′ — or F′ ▷ yF̃ ∧ b = a ∧ A_{y}[F̃ρ /z̃] ∼ E′′ρ — contradicting Lemma 57. Now suppose E′ ▷ yẼ. We have E′ρ⟶^{a}A_{y}[Ẽρ /z̃] so F′ρ⟶^{a} ∼ A_{y}[Ẽρ /z̃]. By Lemma 52 either F′⟶^{a}F′′ ∧ F′′ρ ∼ A_{y}[Ẽρ /z̃] — contradicting Lemma 57 — or F′ ▷ y′F̃ ∧ A_{y′}[F̃ρ /z̃] ∼ A_{y}[Ẽρ /z̃] — in which case by Lemma 58 y = y′ and by Lemma 59 ∀i . E_{i}ρ ∼ F_{i}ρ so ∀i . E_{i} R F_{i}. □

Remark The presence of + is essential for this theorem. Consider a variable y: P → P → P. The +-free normal forms in T_{0}^{P → P → P} are of the form λx_{1} : P. λx_{2} : P. E for E of

E ::= 0 | aE | x | fix λx: P. E

and so must ignore one or both of their arguments. The appropriate definition of ∼_{ext} is ∼_{ext}^{+free} where A ∼_{ext}^{+free} B iff for all substitutions for A, B with +-free range Aρ ∼ Bρ. Taking the terms A =^{def} y 0 (y a0 0) and B =^{def} y 0 (y aa0 0) we have A ∼_{ext}^{+free} B but A ≁_{ho} B. This prevents a cheap proof of non-finite-axiomatisability over the +-free fragment. For the even simpler +-free fragment with a single action we conjecture that there is a finite equational axiomatisation using the axiom

{f : P → P, g: P → P } ▷ fix λx: P. f(gx) = fix λx: P. f(g(g(x)) : P,

which is sound only because this fragment is so inexpressive.

Theorem 8 If E ∼_{ho} F then E ∼_{ext} F.

Proof Given E ∼_{ho} F we must show for all substitutions ρ for E, F that Eρ ∼_{ho} F ρ. This is done indirectly. We construct below transition systems E⋆ρ, F ⋆ρ and show in the next two lemmas that

Eρ ∼_{ho} E⋆ρ ∼_{ho} F ⋆ρ ∼_{ho} Eρ.
□

The (straightforward) direct proof is not given as in the next section information relating the ‘loop structure’ of Eρ and F ρ is extracted from these bisimulations.

The transition system E⋆ρ differs from Eρ in that states that might be identified by the non-injectivity of ρ are split apart. For example if

E =^{def} y + aE′
E′ =^{def} fix λx: P. a(z + ax)
ρ(y) =^{def} ρ(z) =^{def} 0

then

Eρ [figure: a; \underline{a}] E′ρ

whereas E⋆ρ is

[figure: ⟨E⟩; a; ⟨E′⟩; a; \underline{a}; ⟨z + aE′⟩]

To define E⋆ρ the inference system of §3.3 is extended to one for inferring transitions labelled by nonempty finite sequences of actions, with the rules

{E⟶^{a}F \atop E⟶^{aϵ}F} single  \begin{matrix}E⟶^{a}F & F ⟶^{l}G \\ E⟶^{al}G \end{matrix} cons.

If d is an inference tree of this system with conclusion E⟶^{l}F we write d: E⟶^{l}F.

Definition Given a substitution ρ for E_{0} with ρ and notation as in §3.5 the transition system E_{0}⋆ρ has states

S =^{def} { ⟨E⟩ | E ∈ der(E_{0}) }
⊎ {⟨H′[Ẽ/z̃], yẼ, d⟩ | d: H_{y}⟶^{l}H′
and ∃E ∈ der(E_{0}) . E ▷ yẼ}

58 Chapter 3. Axiomatisation over μ-expressions with root ⟨E_{0}⟩. The transition relation ⇝^{a} of E_{0}⋆ρ is the least relation such that

1. E⟶^{a}F ⇒ ⟨E⟩⇝^{a}⟨F ⟩

2. E ▷ yẼ ∧ d: H_{y}⟶^{a}H′ ⇒ ⟨E⟩⇝^{a}⟨H′[Ẽ/z̃], yẼ, single(d)⟩

3. E ▷ yẼ ∧ H_{y} ▷ z_{i} ∧ ⟨E_{i}⟩⇝^{a}s ⇒ ⟨E⟩⇝^{a}s

4. (∃E ∈ der(E_{0}) . E ▷ yẼ) ∧ d: H_{y}⟶^{l}H′ ∧ d′: H′⟶^{a}H′′ ⇒

⟨H′[Ẽ/z̃], yẼ, d⟩⇝^{a}⟨H′′[Ẽ/z̃], yẼ, cons(d, d′)⟩

5. (∃E ∈ der(E_{0}) . E ▷ yẼ) ∧ d: H_{y}⟶^{l}H′ ∧ H′ ▷ z_{i} ∧ ⟨E⟩⇝^{a}s ⇒

⟨H′[Ẽ/z̃], yẼ, d⟩⇝^{a}s.

The visibilities ▷′ of E_{0}⋆ρ are given by 1. (There is no corresponding case.)

2. E ▷ yẼ ∧ H_{y} ▷ x ⇒ ⟨E⟩ ▷′ x

3. E ▷ yẼ ∧ H_{y} ▷ z_{i} ∧ ⟨E_{i}⟩ ▷′ x ⇒ ⟨E⟩ ▷′ x

4. (∃E ∈ der(E_{0}) . E ▷ yẼ) ∧ d: H_{y}⟶^{l}H′ ∧ H′ ▷ x ⇒

⟨H′[Ẽ/z̃], yẼ, d⟩ ▷′ x

5. (∃E ∈ der(E_{0}) . E ▷ yẼ) ∧ d: H_{y}⟶^{l}H′ ∧ H′ ▷ z_{i} ∧ ⟨E⟩ ▷′ x ⇒

⟨H′[Ẽ/z̃], yẼ, d⟩ ▷′ x. Lemma 60 If ρ is a substitution for E then Eρ ∼_{ho} E⋆ρ. Proof One can check that

{ Aρ, ⟨A⟩ | ⟨A⟩ is a state of E⋆ρ }

∪ { Aρ, ⟨A, F, d⟩ | ⟨A, F, d⟩ is a state of E⋆ρ }

is a higher order bisimulation, using induction on the transition derivations. □ Lemma 61 If E ∼_{ho} F and ρ is a substitution for E, F then E⋆ρ ∼_{ho} F ⋆ρ.

Proof By Lemma 37 there is a finite higher order bisimulation R with E R F. Let the relation Q between the states of E⋆ρ and F ⋆ρ be

Q =^{def} { ⟨E′⟩, ⟨F′⟩ | E′ R F′ }
∪ { ⟨H′[Ẽ/z̃], yẼ, d⟩, ⟨H′[F̃/z̃], yF̃, d⟩ | there exist E′ ∈ der(E) and

F′ ∈ der(F) such that E′ ▷ yẼ, F′ ▷ yF̃,

∀j . E_{j} R F_{j} and d: H_{y}⟶^{l}H′ }.

One can check that Q is a higher order bisimulation betwixt E⋆ρ and F ⋆ρ, using induction on the transition derivations. □

3.7 Loop properties

The instantiations Eρ, F ρ of a higher order bisimilar E, F are uniform in a sense captured by the following definition and theorem.

Definition For u ≥ 1 take the predicate L_{u} and equivalence relation ≡_{u} over states in a transition system to be:

• L_{u}s iff s has a loop with no prime factor ≥ u, i.e. s⟶^{∗}s′⟶^{n}s′ for some s′ and n with no prime factor ≥ u.

• s ≡_{u} s′ iff ∀v ≥ u . L_{v}s ⇔ L_{v}s′.

Theorem 9 If E ∼_{ho} F then there is some u ≥ 1 such that for all substitutions ρ for E, F Eρ ≡_{u} F ρ.

Proof This follows from the following two lemmas. □

Lemma 62 If ρ is a substitution for E then ∀u ≥ 1 . Eρ ≡_{u} E⋆ρ.

Proof See Appendix B. □

Definition For a finite relation U ⊆ A × B say the width of U is

width(U) =^{def} max{max_{a∈A} #{ b | a U b }, max_{b∈B} #{ a | a U b }}.

Lemma 63 If E ∼_{ho} F then there is some u ≥ 1 such that for all substitutions ρ for E, F E⋆ρ ≡_{u} F ⋆ρ.

Proof Consider the R and Q in the proof of Lemma 61. We first give a u ≥ 1, dependent on R but not on ρ, strictly greater than the width of Q. Let R′ ⊆ T_{1}^{P} × T_{1}^{P} be

yẼ R′ yF̃ ⟺ ∃E′ ∈ der(E), F′ ∈ der(F) . E′ ▷ yẼ ∧ F′ ▷ yF̃ ∧ ∀i . E_{i} R F_{i}

and put u =^{def} 1 + max{width(R), width(R′)}. To see that E⋆ρ ≡_{u} F ⋆ρ suppose that s Q t, v ≥ u and L_{v}s, i.e. for some s′ and some n ≥ 1 with no prime factors ≥ v that s⟶^{∗}s′⟶^{n}s′. As Q is a higher order bisimulation there exist t_{i} | i ≥ 0 such that

s′  s′  s′ ⋯
Q  Q  Q ⋯
t ⟶^{∗} t_{0} ⟶^{n} t_{1} ⟶^{n} t_{2} ⋯

but #{ t_{i} | i ≥ 0 } < u so for some k ∈ 1..u − 1 we have t⟶^{∗}t′⟶^{kn}t′. Further, kn has no prime factors ≥ v. □

The equivalences ≡_{u} have the following congruence property.

Lemma 64 For M, N ∈ T_{0}^{P} and C[ ] a context from

C ::= | x | 0 | aC | C + C | fix λx: P. C

(where x: P ∈ K), if M ∼_{ho} N and M ≡_{u} N then C[M] ≡_{u} C[N].

Proof By induction on contexts using the following lemma. □

Definition loops E =^{def} { k | ∃E′ . E⟶^{∗}E′⟶^{k}E′ }

Lemma 65

loops aE = loops E
loops E + F = loops E ∪ loops F
loops fix λx: P. E = loops E ∪ {∑_{i∈I} k_{i} | ∀i ∈ I . E⟶^{k_{i}} ▷ x}

where I ranges over finite sets.

Proof Straightforward. □

The following is included for later use.

Lemma 66 If E⟶^{∗}F ⟶^{l}F then there exist a term fix λx: P. G, a finite set I and k_{i} ≥ 1 | i ∈ I such that E⟶^{∗} ▷ fix λx: P. G, ∑_{I} k_{i} = l and ∀i . G⟶^{k_{i}} ▷ x.

Proof Induction on E using Lemma 65. □

Finally we can put together the results of this chapter.

Lemma 67 If E is a finite set of typed equalities that is sound for bisimulation and of order ≤ 1 then there is some u ≥ 1 such that for all M, N ∈ T_{0}^{P} if E ⊢ M = N : P then M ≡_{u} N.

Proof We assume w.l.g. that E contains only equalities at type P. By Corollary 31 each equation lies within ∼_{ext} and so by Theorem 7 within ∼_{ho}. Take u to be the largest of those given by Theorem 9 applied to each equation. By Proposition 30 M =_{E} N. An induction on a derivation of this then suffices, using Lemma 64 in the inductive steps and Theorem 9 at the uses of axioms. □

Proof (of Theorem 6) The main theorem follows by noting that if E is sound for an equivalence finer than bisimulation then it is sound for bisimulation and that, if q is the smallest prime strictly greater than the u given by the previous lemma, then

fix λx: P. ax ≢_{u} fix λx: P. a^{q}x.
□

A Miscellany

In this chapter we include a number of applications and developments of the theory of higher order bisimulation. We consider the axiomatisability of bisimulation over ∗-expressions, relate higher order bisimulation to the higher order π calculus and cast our results into the language of non-well-founded set theory. We also give a definition of weak higher order congruence and show that weak congruence is finitely axiomatisable relative to bisimulation. The sections may be read in any order.

4.1 Axiomatisation over ∗-expressions

Bisimulation equivalence of ∗-expressions has recently received attention in [BBP94], where the addition of operators that suffice to express the regular processes is considered. The results of the previous chapter can be used to give an easy proof of a non-axiomatisability result for the basic calculus.

4.1.1 Axiomatisation with and without 0

To discuss axioms over ∗-expressions we find it convenient to introduce a set of variables disjoint from Act. An axiomatisation will be a set of pairs of open terms together with rules for equivalence, congruence and instantiation of variables. This differs slightly from the usual setup in which instantiation of actions is permitted.

4.1. Axiomatisation over ∗-expressions 63

Fokkink and Zantema have given (in [FZ94]) a complete axiomatisation for the ∗-expressions that do not contain 0, 1 or the unary ∗.

Theorem 10 (Fokkink and Zantema) The axioms below are sound and complete for bisimulation over BPA^{∗}, i.e. over expressions of {a, +, ., ^{⋆} }.

x + y = y + x
(x + y) + z = x + (y + z)
x + x = x
(x + y) . z = x . z + y . z
(x . y) . z = x .(y . z)
x .(x^{⋆}y) + y = x^{⋆}y
x^{⋆}(y . z) = (x^{⋆}y) . z
x^{⋆}(y .((x + y)^{⋆}z) + z) = (x + y)^{⋆}z

Proof This is immediate from the result of [FZ94] and Proposition 17. □

If the zero process is added, however, there can be no finite axiomatisation.

Theorem 11 There is no finite axiomatisation for bisimulation over any set of ∗- expressions closed under {0, a, +, .} and one of { ^{∗}, ^{⋆} }.

This can be shown using the results of Chapter 3. We first note that the ∗-expressions (and axioms over them) can be faithfully encoded into our lambda calculus, encoding sequential composition using function composition at type P → P.

Definition Take the map [[ ]] from ∗-expressions to lambda calculus terms of type P → P to be

[[x]] =^{def} x where we suppose x: P → P ∈ K
[[a]] =^{def} a
[[0]] =^{def} λy: P. 0
[[1]] =^{def} λy: P. y
[[E + F]] =^{def} λy: P. + ([[E]]y)([[F]]y)
[[E . F]] =^{def} λy: P. [[E]]([[F]]y)
[[E^{∗}]] =^{def} λy: P. fix λz: P. + (y)([[E]]z)

[[E^{⋆}F]] =^{def} λy: P. fix λz: P. + ([[F]]y)([[E]]z)

Lemma 68 If y: P ∈ K then

E ∼ F ⟺ [[E]]y ∼_{ho} [[F]]y.

Proof It is straightforward to check that E√ ⟺ [[E]]y ▷ y, E⟶^{a}E′ ⇒ [[E]]y⟶^{a}[[E′]]y

and [[E]]y⟶^{a}A ⇒ ∃E′ . E⟶^{a}E′ ∧ [[E′]]y = A. □

Proof (of Theorem 11) To prove the theorem we consider a sound finite set A of axioms. The encodings of these must be higher order bisimilar (as the terms constructed in the proof of Theorem 7 are all expressible) so [[A]] is a sound set in our earlier sense. By Lemma 67 there is some u such that if M, N ∈ T_{0}^{P} and [[A]] ⊢ M = N : P then M ≡_{u} N. Now consider the relevant pair of terms below, where q is the smallest prime strictly greater than u.

E =^{def} a^{∗} . 0  E =^{def} a^{⋆}0
F =^{def} (\overbrace{a . . . . . a}^{q times})^{∗} . 0 F =^{def} (\overbrace{a . . . . . a}^{q times})^{⋆}0

In each case [[E]]y ≢_{u} [[F]]y so [[A]] ⊬ [[E]]y = [[F]]y: P so A ⊬ E = F but E ∼ F. □

The addition of other operators does not affect the result, so long as their semantics are expressible by an encoding into lambda terms as above.

In [Fok94] Fokkink introduced a subcalculus of the ∗-expressions that contains a zero process but for which bisimulation is nonetheless finitely equationally axiomatisable. Denoted MPA_{δ}^{∗} (for Minimal Process Algebra) it is obtained by requiring the first operand of sequential compositions and of binary iterations to be single actions, i.e. in our notation the terms of

E ::= 0 | a . E | E + E | a^{⋆}E.

Aceto and Ingólfsdóttir have recently given (in [AI95]) an extension of that axiomatisation that is complete for observation congruence. These positive axiomatisability results, for BPA^{∗} and MPA_{δ}^{∗}, can be seen as depending on the inexpressiveness of the calculi, in that the processes required in the proof of Theorem 11 cannot be expressed.

4.1.2 Axiomatisation with 1

In the light of the previous subsection it is natural to question whether bisimulation over expressions of the signature {a, 1, +, ., ^{∗}} is axiomatisable. Unfortunately a naive application of the same idea does not show non-axiomatisability. For a proof analogous to that of Theorem 11 we would need a term G such that G^{∗} and (G^{q})^{∗} are bisimilar but not provably equal. By the following lemma any such G must be successfully terminated.

Lemma 69 For q ≥ 2, if G^{∗} ∼ (G^{q})^{∗} then either G√ or ∄H . G⟶^{∗}H√.

Proof Suppose for a contradiction that ¬G√ and G⟶^{+}√. Writing n(E) for the smallest non-zero natural such that E⟶^{n}√ we have n(G^{∗}) = n(G) ≥ 1 and n((G^{q})^{∗}) = q n(G^{∗}) > n(G^{∗}), hence G^{∗} ≁ (G^{q})^{∗}. □

Taking the simplest nontrivial example G =^{def} a + 1 it is easy to see that for any n there is a bisimulation of width 2 relating ((a + 1)^{n})^{∗} and ((a + 1)^{n+1})^{∗}, namely

R =^{def} {((a + 1)^{n})^{∗}, ((a + 1)^{n+1})^{∗}}
∪ { C_{m}^{n}, C_{m+1}^{n+1} | 0 ≤ m ≤ n − 1 }
∪ {C_{n−1}^{n}, C_{0}^{n+1}}

where

C_{0}^{n} =^{def} 1 .((a + 1)^{n})^{∗}
C_{m}^{n} =^{def} (1 .(a + 1)^{m}) .((a + 1)^{n})^{∗} , for m ≥ 1.

The technique of Chapter 3 therefore cannot be used to show that (a + 1)^{∗} and ((a+1)^{q})^{∗} are not provably equal. The question of axiomatisability over {a, 1, +, ., ^{∗}} remains open.

4.2 Higher order process calculi

The lambda calculus of §3.2 was introduced to allow a clean definition of interesting classes of equational axioms over the μ-expressions, not involving ad hoc metanotation. It is, however, of additional interest when viewed as a simple fragment of a higher order process calculus such as the higher order π calculus of Sangiorgi [San93,San94]. In particular the theory of strong higher order bisimulation is not well understood even for this fragment (the work of Sangiorgi is concerned only with the weak case). We will give a precise connection between higher order bisimulation (as defined in Chapter 3) and normal bisimulation as defined in [San94] for the strictly higher order fragment of the higher order π calculus. This confirms the intuition that, in both, the equivalence of abstractions is checked by applying them to simple ‘new’ terms (new variables and triggers respectively).

4.2.1 Syntax and transitions

The basic version of the higher order π calculus of [San94] has guarded summation, parallel composition, restriction and the application of a variable or constant:

P ::= ∑_{i∈I} α_{i}.P_{i} | P_{1} | P_{2} | νaP | Y ⟨Ã⟩ | D⟨Ã⟩

where prefixes α are inputs or outputs:

α ::= a(X̃) | \overline{a}⟨Ã⟩

(with a ≠ τ) and agents A are abstractions:

A ::= (X̃)P.

Here X̃ and Ã range over (possibly empty) tuples. It is assumed that all terms obey a suitable sorting discipline. There is an evident bijection between the lambda terms in T_{ω}^{P} (in normal form, containing only guarded summation and modulo axioms A1–4) and the higher order π terms in which there is no parallel composition, restriction or infinitary summation, the only defined constant is

FIX =^{def} (X)X⟨FIX⟨X⟩⟩

\overline{a}⟨Ã⟩.P ⟶^{\overline{a}⟨Ã⟩}P out a(X̃).P ⟶^{a⟨Ã⟩}P [Ã/X̃] inp

{P ⟶^{μ}P′ \atop P | Q⟶^{μ}P′ | Q} par \begin{matrix}P ⟶^{\overline{a}⟨Ã⟩}P′ & Q⟶^{a⟨Ã⟩}Q′ \\ P | Q⟶^{τ}P′ | Q′ \end{matrix} com

{P ⟶^{μ}P′ \atop P + Q⟶^{μ}P′} sum  {P |!P ⟶^{μ}P′ \atop !P ⟶^{μ}P′} rep

Figure 4–1: Higher order π transition system

and all names appear only as inputs with a nullary sort — i.e. the terms of

P ::= ∑_{i∈I} a_{i}⟨⟩.P_{i} | Y ⟨Ã⟩ | FIX⟨A⟩.

We define higher order bisimulation (∼_{ho}) over these terms via the bijection. Unfortunately the definition of normal bisimulation and the results of [San94] are in terms of a slightly different calculus — with replication in place of constants and with unary variables and names, i.e. variables only of types from

σ ::= P | σ → P

and names that carry single values of these types. We will therefore only obtain a result for lambda terms that do not contain fix , however the definition will be generalised to allow arbitrary types. We take a fragment of the higher order π calculus that is just large enough to contain the terms of

P ::= ∑_{i∈I} a_{i}⟨⟩.P_{i} | Y ⟨Ã⟩ †

and to admit a definition of normal bisimulation. The terms are those of

P ::= ∑_{i∈I} α_{i}.P_{i} | P_{1} | P_{2} | Y ⟨Ã⟩ |!P. ‡

The labelled transition system semantics for this is given in Figure 4–1, in which μ ranges over all action labels and the symmetric counterparts of par, com and sum are omitted. For the sub-fragment with only unary variables and names the transition system coincides with that of [San94]. Our omission of restriction is therefore harmless in that normal bisimulation (as defined in the next section) over this sub-fragment coincides with normal bisimulation over the whole calculus of [San94]. A similar coincidence presumably holds between normal bisimulation over the latter and normal bisimulation over the ‘reduced higher order π calculus’ of [San93], which allows name passing in addition to process passing.

4.2.2 Normal bisimulation

Three equivalences over the higher order π calculus are defined and shown equal in [San93] — context bisimulation, barbed congruence and normal bisimulation. The idea behind the latter is that to check the input case of the equivalence of two processes it suffices to consider inputs of a particular form, the triggers. A trigger is an agent of the form

Tr_{m_{i}} =^{def} (X̃)\overline{m}_{i}⟨X̃⟩.0

for a name m_{i} of suitable sort. Similarly to check the equivalence of processes with free variables it suffices to substitute triggers on new, distinct names for the variables and then check equivalence.

Definition A symmetric relation R over closed terms of ‡ is a normal bisimulation if for any P R Q and distinct m̃ not in the free names of P, Q:

• If P ⟶^{a⟨Tr_{m_{1}},...,Tr_{mn}⟩}P′ then ∃Q′ . Q ⟹^{a⟨Tr_{m_{1}},...,Tr_{mn}⟩}Q′ and P′ R Q′.

• If P ⟶^{\overline{a}⟨A_{1},...,A_{n}⟩}P′ then ∃Q′, B̃ . Q ⟹^{\overline{a}⟨B_{1},...,B_{n}⟩}Q′ and

P′ |!m_{1}(X̃_{1}).A_{1}⟨X̃_{1}⟩ | ⋯ |!m_{n}(X̃_{n}).A_{n}⟨X̃_{n}⟩
R
Q′ |!m_{1}(X̃_{1}).B_{1}⟨X̃_{1}⟩ | ⋯ |!m_{n}(X̃_{n}).B_{n}⟨X̃_{n}⟩.

• If P ⟶^{τ}P′ then ∃Q′ . Q⟹Q′ and P′ R Q′.

(Here ⟹^{α} =^{def} ⟶^{τ}^{∗}⟶^{α}⟶^{τ}^{∗} and ⟹ =^{def} ⟶^{τ}^{∗}, as usual.) The union of all normal bisimulations is written ∼_{Nr}. It is lifted to open terms P, Q with free variables X, Y, … by

P ∼_{Nr} Q iff P ρ ∼_{Nr} Qρ

where ρ is a substitution [Tr_{m_{X}}/X, Tr_{m_{Y}} /Y, …] for some new distinct names m_{X}, m_{Y} , . . ..

This is the natural generalisation of the definition of [San94] to processes with free variables of arbitrary type, but without restriction.

4.2.3 The coincidence of ∼_{ho} and ∼_{Nr}

Proposition 70 If P, Q are terms of †, i.e. of

P ::= ∑_{i∈I} a_{i}⟨⟩.P_{i} | Y ⟨Ã⟩

then P ∼_{ho} Q iff P ∼_{Nr} Q.

Proof In the following we assume that the set of names is the disjoint union of Act (ranged over by a) and a set M (ranged over by m). E and F range over abstractions (X̃)P of the above processes. We work up to the associativity, commutativity and 0-absorbtion of | and the law !P = P |!P. A trigger substitution ρ is a substitution of distinct triggers for all free variables in terms to which it is applied. For the right-to-left direction we let

R =^{def} { E, F | Eρ ∼_{Nr} F ρ and ρ is a trigger substitution}

and check that this is a higher order bisimulation.

Suppose E R F and E ▷ yẼ. Clearly Eρ ⟶^{\overline{m}_{y}⟨Ẽρ⟩}0 so there is some B̃ such that

F ρ ⟹^{\overline{m}_{y}⟨B̃⟩}0 and for any new m̃ and X̃_{i} | i ∈ 1..n

!m_{1}(X̃_{1}).E_{1}ρ⟨X̃_{1}⟩ | ⋯ |!m_{n}(X̃_{n}).E_{n}ρ⟨X̃_{n}⟩
∼_{Nr}
!m_{1}(X̃_{1}).B_{1}⟨X̃_{1}⟩ | ⋯ |!m_{n}(X̃_{n}).B_{n}⟨X̃_{n}⟩.

Hence there is some F̃ such that F ▷ yF̃ and F̃ρ = B̃. Further, by the definition of normal bisimulation, for any i and new m̃_{i}

(E_{i}⟨X̃_{i}⟩)ρ ⊕ [Tr_{m_{i1}}/X_{i1}, …] ∼_{Nr} (F_{i}⟨X̃_{i}⟩)ρ ⊕ [Tr_{m_{i1}}/X_{i1}, …]

so (E_{i}⟨X̃_{i}⟩) R (F_{i}⟨X̃_{i}⟩) and E_{i} R̂^{σ_{i}} F_{i}.

The reasoning for E⟶^{a}E′ is straightforward.

For the left-to-right direction we take

R_{0} =^{def} { Eρ, F ρ | E ∼_{ho}^{P} F and ρ is a trigger substitution}
∪ {!m(X̃).Eρ⟨X̃⟩,!m(X̃).F ρ⟨X̃⟩ | E ∼_{ho}^{σ_{1}···σ_{n} → P} F

ρ is a trigger substitution X̃ are not free in E, F m does not occur in ran(ρ) }

and close up under certain parallel compositions. Let R be the smallest relation containing R_{0} such that if P R Q, P′ R Q′ and no name occurs both in input and output positions in P | P′ or Q | Q′ then P | P′ R Q | Q′. We check that R is a normal bisimulation. No communication can occur in any process in dom(R) ∪ ran(R) so the only transitions that need be considered are the following, in which P R Q, E ∼_{ho}^{σ} F and m̃, X̃ are new:

• P | Eρ⟶^{a⟨⟩}P | E′ρ as E⟶^{a}E′
R
Q | F ρ
• P |!m(X̃).Eρ⟨X̃⟩ ⟶^{m⟨Tr_{m_{1}},...,Tr_{mn}⟩}P |!m(X̃).Eρ⟨X̃⟩ | Eρ⟨Tr_{m_{1}}, …, Tr_{m_{n}}⟩
R
Q |!m(X̃).F ρ⟨X̃⟩
• P | Eρ ⟶^{\overline{m}_{y}⟨Ẽρ⟩}P | 0 as E ▷ yẼ
R
Q | F ρ

For the first, F ⟶^{a}F′ ∼_{ho} E′ so (Q | F ρ)⟶^{a⟨⟩}(Q | F′ρ) R (P | E′ρ).

For the second

Q |!m(X̃).F ρ⟨X̃⟩ ⟶^{m⟨Tr_{m_{1}},...,Tr_{mn}⟩} Q |!m(X̃).F ρ⟨X̃⟩ | F ρ⟨Tr_{m_{1}}, …, Tr_{m_{n}}⟩.

We have E⟨X̃⟩ ∼_{ho}^{P} F ⟨X̃⟩ so E⟨X̃⟩ρ ⊕ [Tr_{m_{1}}/X_{1}, …] R_{0} F ⟨X̃⟩ρ ⊕ [Tr_{m_{1}}/X_{1}, …], hence Eρ⟨Tr_{m_{1}}, …, Tr_{m_{n}}⟩ R_{0} F ρ⟨Tr_{m_{1}}, …, Tr_{m_{n}}⟩ and the targets of the transitions are related by R.

For the third there exists some F̃ such that F ▷ yF̃ and ∀i . E_{i} ∼_{ho}^{σ_{i}} F_{i}. It follows that

Q | F ρ ⟶^{\overline{m}_{y}⟨F̃ρ⟩} Q | 0.

Further, for all i and new X̃_{i}

!m_{i}(X̃_{i}).E_{i}ρ⟨X̃_{i}⟩ R_{0} !m_{i}(X̃_{i}).F_{i}ρ⟨X̃_{i}⟩

so

(P |!m_{1}(X̃_{1}).E_{1}ρ⟨X̃_{1}⟩ | ⋯) R (Q |!m_{1}(X̃_{1}).F_{1}ρ⟨X̃_{1}⟩ | ⋯).
□

We expect that this proposition could be generalised to all lambda terms, i.e. to

P ::= ∑_{i∈I} a_{i}⟨⟩.P_{i} | Y ⟨Ã⟩ | FIX⟨A⟩,

without difficulty, although the statement would require a higher order π calculus with both replication and constants.

The definitions of barbed congruence and context bisimulation both involve quantification over higher order π contexts and so cannot be easily related to ∼_{ho} or ∼_{ext} (except via the above proposition, of course). This prevents us making use of Sangiorgi’s results to obtain a cheap proof of the equality of ∼_{ho} and ∼_{ext}.

4.3 Non-well-founded set theory

In the usual conception of set theory the membership relation is required to be well-founded — there is, for example, no set which is a member of itself. The Zermelo-Fraenkel axiomatisation expresses this by the axiom of Foundation:

FA: Any non-empty set X has an element Y such that X ∩ Y = {}.

In [Acz88] Aczel discusses a number of alternative axioms that admit non-well-founded sets. He focuses on the axioms of ZFC with an axiom AFA (of Anti-Foundation) replacing FA. We recall its statement.

Definition A graph is a set of nodes together with a set of edges, i.e. ordered pairs of the nodes. A decoration of a graph is an assignment of a set to each of its nodes such that the elements of the set assigned to a node are the sets assigned to the children of that node.

AFA: Any graph has a unique decoration.

Pointed graphs can therefore be taken to denote unique sets of ZFC−FA+AFA. To say when they denote the same set we define bisimulation between pointed graphs in the obvious way.

Definition A bisimulation between pointed graphs ⟨N, ⟶, n_{0}⟩ and ⟨N′, ⟶′, n′_{0}⟩ is a relation R ⊆ N × N′ such that n_{0} R n′_{0} and if n R n′ then:

• If n⟶n_{1} then ∃n′_{1} . n′⟶′n′_{1} ∧ n_{1} R n′_{1}.

• If n′⟶′n′_{1} then ∃n_{1} . n⟶n_{1} ∧ n_{1} R n′_{1}.

Proposition 71 (Aczel) Two pointed graphs denote the same set iff they are bisimilar.

These definitions of pointed graphs and bisimulation are almost identical to those of §2.1.1 of charts, taking a single action and no variables, and bisimulation thereof. (They differ only in that the sets involved are non-well-founded and standard, respectively, which we gloss over.) We can therefore take the closed μ-expressions over a single action to denote non-well-founded sets. For more intuitive notation one could write 0 as {}, the single action as an outfix { }, + as ∪ and {A_{1}, …, A_{n}} as an abbreviation for {A_{1}} ∪ ⋯ ∪ {A_{n}}, with for example

μX {X} = μX {{X}}
μX {{}, X} = μX {{}, {{}, X}}.

The collection of non-well-founded sets denotable by μ-expressions is reasonably large. It coincides with the hereditarily finite sets of [Acz88, Ch.1]. In [Acz88] particular non-well-founded sets are described using either pictures of pointed graphs or pointed sets of guarded equations. We expect that the simpler syntax of μ-expressions is sometimes more convenient, just as it is for process algebra.

We trivially have the following corollary of Theorem 6.

Corollary 72 There is no finite axiomatisation of order ≤ 1 for non-well-founded set equality of μ-expressions over a single action.

4.4 Weak congruence: relative axiomatisability and

at higher order

In this section we show that weak congruence of μ-expressions is finitely equationally axiomatisable relative to bisimulation. We also give a definition of weak higher order congruence. This enables us to prove the soundness of the new axioms simply by exhibiting some small weak higher order bisimulations.

4.4.1 Weak higher order congruence

The adaption of the definition of higher order bisimulation to the weak case is straightforward. The only subtlety involved is that we must require the arguments of a variable to be weak (higher order) congruent, not merely weak (higher order) bisimilar. For example, taking x: P → P, the terms x (a0) and x (τa0) cannot be identified as substituting the identity for x would give non-congruent terms.

Definition Let R, S be relations over T_{ω}^{P}. The relation R(R, S) over T_{ω}^{P} is defined by E R(R, S) F iff

• If E⟶^{a}E′ then ∃F′ . F ⟹^{a}F′ ∧ E′ S F′.

• If E ▷ xẼ then ∃F̃ . F ⟶^{τ}^{∗} ▷ xF̃ ∧ ∀i . E_{i} R̂^{σ_{i}} F_{i}.

and symmetrically. The relation S(R, S) over T_{ω}^{P} is defined by E S(R, S) F iff

• If E⟶^{a}E′ then ∃F′ . F ⟹^{â}F′ ∧ E′ S F′.

• If E ▷ xẼ then ∃F̃ . F ⟶^{τ}^{∗} ▷ xF̃ ∧ ∀i . E_{i} R̂^{σ_{i}} F_{i}.

and symmetrically. For E, F ∈ T_{ω}^{P} we say E is weak higher order congruent to F, written E ≈_{ho}^{c} F, if there exist R, S such that R ⊆ R(R, S), S ⊆ S(R, S) and E R F.

The sound axioms can be characterised as before.

Definition The relation ≈_{ext}^{c} over T_{ω}^{P} is given by

E ≈_{ext}^{c} F iff for all substitutions ρ for E, F we have Eρ ≈^{c} F ρ.

By Corollary 31 an axiom E = F is sound for ≈^{c} precisely if E ≈_{ext}^{c} F.

In the rest of this section we again consider only terms in T_{1}^{P}, i.e. terms of type P containing at most first order variables. We show an analogue of Theorem 8, that any weak higher order congruent pairs of terms are sound.

Theorem 12 If E ≈_{ho}^{c} F then E ≈_{ext}^{c} F.

Proof Given E ≈_{ho}^{c} F and a substitution ρ for E, F we must show that Eρ ≈^{c} F ρ. We are not going to show a non-axiomatisability result for ≈^{c} (although one might well) and so do not need to factor this through the derived transition systems E⋆ρ, F ⋆ρ. We adopt conditions on variables as in §3.5, in particular taking ρ(y) to be of the form λz_{1} : P. · · · λz_{n}: P. H_{y}. Suppose that R ⊆ R(R, S), S ⊆ S(R, S), E R F and that R and S relate only terms contained in der(E), der(F). We let

Q =^{def} { E′ρ, F′ρ | E′ (R ∪ S) F′ }
∪ { H′[Ẽρ/z̃], H′[F̃ ρ/z̃] | there exist E′ ∈ der(E), F′ ∈ der(F) such that
E′ ▷ yẼ, F′ ▷ yF̃,
∀j . E_{j} R F_{j} and H_{y}⟶^{+}H′ }.

It is straightforward to check that Q is a weak bisimulation, using Proposition 53 and induction on the definitions of ⟶_{ρ}^{a}, ▷_{ρ}. Moreover, if E′ R F′ then E′ρ W(Q) F′ρ. □

We have no immediate application for the converse, that E ≈_{ext}^{c} F implies E ≈_{ho}^{c} F, and so leave it and other investigation of the weak case to future work.

4.4.2 A finite axiomatisation of weak congruence relative to bisimulation

The new axioms are F 1–3, which presented as schemas are:

\begin{aligned}F 1 & μ ⟨ \begin{matrix}X = E + aY \\ Y = F + τG \end{matrix} ⟩ & = & μ ⟨ \begin{matrix}X = E + aY + aG \\ Y = F + τG \end{matrix} ⟩ \\ F 2 & μ ⟨ \begin{matrix}X = E + τY \\ Y = F + G \end{matrix} ⟩ & = & μ ⟨ \begin{matrix}X = E + τY + G \\ Y = F + G \end{matrix} ⟩ \\ F 3 & aμXE & = & aμXE + τX. \end{aligned}

We show below that these suffice to saturate (the fixed point of) any standard equation sequence. Over saturated charts weak congruence and bisimulation coincide so the relative axiomatisability result follows immediately, i.e. F 1–3 together with a rule

F 4  E ∼ F → E = F

are complete for ≈^{c}.

Axiom schemas F 1–3 can be written as a set of pure equations between lambda terms. Unfortunately F 1 and F 3 involve variables (a) ranging over Act so strictly speaking an infinite set of such equations is required. Taking Γ = {e: P → P → P, f : P → P → P, g: P → P → P, h: P → P } and an arbitrary constant a: P → P:

F 1′_{a} Γ ▷ fix λx: P. (exA_{1}) + (aA_{1}) = (exA_{1}) + (aA_{1}) + (a(gxA_{1})) : P
where A_{1} =^{def} fix λy: P. (fxy) + (τ(gxy))
F 2′ Γ ▷ fix λx: P. (exA_{2}) + (τA_{2}) = (exA_{2}) + (τA_{2}) + (gxA_{2}) : P
where A_{2} =^{def} fix λy: P. (fxy) + (gxy)
F 3′_{a} Γ ▷ a fix λx: P. hx = a fix λx: P. (hx) + (τx) : P

all instances of F 1′_{a} and F 3′_{a} for a ∈ Act are required. One could take a modified signature which has base types P and A and constants

0 : P

a: A for each a ∈ Act (including τ) .: A → P → P + : P → P → P fix :(P → P) → P.

The equations F 3′_{a} | a ∈ Act could then be expressed by a single equation

F 3′′ {α: A, h: P → P } ▷ α.fix λx: P. hx = α.fix λx: P. (hx) + (τ.x) : P,

and similarly for F 1′_{a} | a ∈ Act. One could then obtain a precise finite axiomatisability result. We do not do this because the definitions (e.g. of weak higher order congruence) would become somewhat more complex and no more enlightening. The completeness proof will be presented in terms of the schematic forms F 1–3. The soundness proof shows that all instances of F 1′_{a}, F 2′ and F 3′_{a} are sound. It would presumably be straightforward to carry out both for the modified signature.

Lemma 73 For any a ∈ Act the axioms F 1′_{a}, F 2′ and F 3′_{a} are sound.

Proof By Theorem 12 and Corollary 31 we need only show that the terms in each equation are weak higher order congruent. For F 1′_{a} let B, C be the left and right hand terms of the equation respectively and let

R =^{def} {⟨B, C⟩, ⟨A_{1}[B/x], A_{1}[C/x]⟩, ⟨gB(A_{1}[B/x]), gC(A_{1}[C/x])⟩}.

It is routine to check that R ⊆ R(R, R) (and hence R ⊆ S(R, R)) so B ≈_{ho}^{c} C. The reasoning for the other axioms is similar. □

Definition A chart S = ⟨S, ⟶, ▷, s_{0}⟩ is root-unwound if ¬∃s . s⟶^{a}s_{0}. It is saturated if it is root-unwound, accessible and:

1. s⟹^{a}s′ ⇒ s⟶^{a}s′

2. s⟶^{τ}^{∗} ▷ X ⇒ s ▷ X

3. s ≠ s_{0} ⇒ s⟶^{τ}s.

Note that any standard sequence is, when viewed as a chart, root-unwound.

Lemma 74 For saturated charts S, T, if S ≈^{c} T then S ∼ T.

Proof It is routine to check that ≈, restricted to (S − s_{0}) × (T − t_{0}), is a strong bisimulation and then that s_{0} ∼ t_{0}. □

Lemma 75 If for all substitutions ρ with X, X′ ∉ dom(ρ) we have ⊢ A = B, where

A =^{def} μ ⟨ \begin{matrix}X = Eρ \\ X′ = E′ρ \end{matrix} ⟩ and B =^{def} μ ⟨ \begin{matrix}X = E′′ρ \\ X′ = E′ρ \end{matrix} ⟩ ,

then for all (possibly empty) sequences ⟨Ỹ = F̃⟩, ⟨Z̃ = G̃⟩ we have ⊢ L = R, where

L =^{def} μ [figure] \begin{matrix}Ỹ = F̃ \\ X = E \\ X′ = E′ \\ Z̃ = G̃ \end{matrix} [figure] and R =^{def} μ [figure] \begin{matrix}Ỹ = F̃ \\ X = E′′ \\ X′ = E′ \\ Z̃ = G̃ \end{matrix} [figure].

Proof By the definition of the fixed point of a sequence there is a substitution ρ with domain Z̃ such that

L = μ⟨Ỹ = F̃ρ[μX′E′ρ /X′][A/X]⟩
R = μ⟨Ỹ = F̃ρ[μX′E′ρ /X′][B/X]⟩.

By the premise and congruence rules, for all i

⊢ F_{i}ρ[μX′E′ρ /X′][A/X] = F_{i}ρ[μX′E′ρ /X′][B/X]

so by Lemma 18 ⊢ L = R. □

Lemma 76 For any standard sequence ⟨X_{i} = E_{i} | i ∈ m⟩ there is a saturated standard sequence ⟨X_{i} = F_{i} | i ∈ m⟩ such that A1–5,B3,F 1–3 ⊢ μ⟨X_{i} = E_{i} | i ∈ m⟩ = μ⟨X_{i} = F_{i} | i ∈ m⟩.

Proof For a standard sequence ⟨Z_{i} = G_{i} | i ∈ m⟩, considered as a chart, let the measure f ⟨Z_{i} = G_{i} | i ∈ m⟩ be the pair

⟨#{ i, a, j | i⟹^{a}j ∧ ¬i⟶^{a}j }, #{ i, W | i⟶^{τ}^{∗} ▷ W ∧ ¬i ▷ W }⟩.

We show by induction on f ⟨X̃ = Ẽ⟩ (with the product ordering) that there exists a provably equal ⟨X̃ = F̃⟩ satisfying conditions 1 and 2 of the definition of a saturated chart. The base case, f ⟨X̃ = Ẽ⟩ = ⟨0, 0⟩, is trivial. Suppose f ⟨X̃ = Ẽ⟩ = ⟨p + 1, q⟩.

Definition For n ≥ 0 and states s, s′ of a chart say s⟹^{a}_{n}s′ if there exist n_{1}, n_{2} ≥ 0 such that s⟶^{τ}^{n_{1}} ⟶^{a}⟶^{τ}^{n_{2}}s′, n_{1} + n_{2} = n and further that n_{1} + n_{2} is minimal amongst the n′_{1} + n′_{2} such that s⟶^{τ}^{n′_{1}} ⟶^{a}⟶^{τ}^{n′_{2}}s′.

Clearly there exist i, a, j, n ≥ 1 such that i⟹^{a}_{n}j. In fact there exist i, a, j such that i⟹^{a}_{1}j, as otherwise we can pick a non-minimal subsequence of the transitions in i⟹^{a}_{n}j. It follows that ¬(i⟶^{a}j) and that there is some k such that either (1) i⟶^{τ}k⟶^{a}j or (2) i⟶^{a}k⟶^{τ}j. Suppose (1). Then

E_{i} = E_{i} + τX_{k}
E_{k} = E_{k} + aX_{j}.

By ⟨X̃ = Ẽ⟩ standard we know that k ≠ 0 ≠ j and by Lemma 19 w.l.g. k = i + 1, so ⟨X̃ = Ẽ⟩ is

[figure: \begin{matrix}Ỹ = F̃ \\ X_{i} = E_{i} + τX_{k} \\ X_{k} = E_{k} + aX_{j} \\ Z̃ = G̃ \end{matrix}]

for some (possibly empty) Ỹ = F̃ and Z̃ = G̃. By Lemma 75 this is provably equal, using F 2, to

[figure] \begin{matrix}Ỹ = F̃ \\ X_{i} = E_{i} + τX_{k} + aX_{j} \\ X_{k} = E_{k} + aX_{j} \\ Z̃ = G̃ \end{matrix} [figure],

which has measure ⟨p, q⟩. The case for (2) is similar but using F 1.

Suppose f ⟨X̃ = Ẽ⟩ = ⟨p, q + 1⟩. This is similar to (1) above but instantiating the ‘G’ of F 2 by a variable rather than by a term aX_{j}.

This completes the induction. It remains only to add τ loops to ensure that condition 3 holds. This is straightforward using F 3. □

Theorem 13 The axioms F 1–4 are sound and complete for weak congruence (≈^{c}).

Proof Soundness is immediate from Lemma 73 and the fact that ∼⊆≈^{c}. For completeness suppose that E ≈^{c} F. By Lemma 20 there are standard accessible sequences ⟨X̃ = Ẽ⟩, ⟨Ỹ = F̃⟩ such that

AB ⊢ E = μ⟨X̃ = Ẽ⟩
AB ⊢ F = μ⟨Ỹ = F̃⟩

(here AB denotes the axioms A1–5,B1–3 introduced in §2.3). By Lemma 76 there are saturated sequences ⟨X̃ = Ẽ′⟩, ⟨Ỹ = F̃′⟩ such that

ABF 1–3 ⊢ μ⟨X̃ = Ẽ⟩ = μ⟨X̃ = Ẽ′⟩
ABF 1–3 ⊢ μ⟨Ỹ = F̃⟩ = μ⟨Ỹ = F̃′⟩.

By soundness and Lemma 21 ⟨X̃ = Ẽ′⟩ ≈^{c} ⟨Ỹ = F̃′⟩ so by Lemma 74 ⟨X̃ = Ẽ′⟩ ∼ ⟨Ỹ = F̃′⟩. By Lemma 21 again μ⟨X̃ = Ẽ′⟩ ∼ μ⟨Ỹ = F̃′⟩ so using F 4 ⊢ μ⟨X̃ = Ẽ′⟩ = μ⟨Ỹ = F̃′⟩. Finally, all uses of axioms from A and B can, as these are sound for bisimulation, be replaced by uses of F 4. □

It follows that, if the pure implication E3 (from §2.3.3) could be shown sound for ≈^{c}, the axioms A1–5, B1–3, E1–3, F 1–3 would be a finite pure horn clause axiomatisation for ≈^{c}. This would be as good a positive result for ≈^{c} as could be expected, as we expect that the proof of Chapter 3 could, with some added complexity, be adapted to show that there is no finite equational axiomatisation for ≈^{c}.

Implicational theory

In this chapter we investigate the implicational theory of finite state processes up to bisimulation. We consider sequents

E_{1} = F_{1} ∧ ⋯ ∧ E_{m} = F_{m} ⊢ G_{1} = H_{1} ∨ ⋯ ∨ G_{n} = H_{n}

over μ-expressions (for m, n ≥ 0). The first two sections are devoted to showing that unification problems over μ-expressions have finite computable complete sets of unifiers. The decidability of ⊢ is an easy corollary. These results carry over to the case of finite processes. By taking a singleton set of actions we then have finite complete sets of unifiers for certain set and non-well-founded set problems, generalising the result of [BB88]. We do not, however, have a good characterisation of the minimal complete sets of unifiers — some coarse cardinality bounds thereof are given.

These sequents do not appear to provide enough power to finitely axiomatise bisimulation (we do not give a proof of this). It was shown by Bloom andÉsik that sequents over expressions containing first order variables suffice (see §2.3.3). The decidability of such sequents is left for future work.

For a richer signature, sequents such as the above may be regarded as interesting implicit process specifications, with unification results providing automated implementation. The solving of equations between CCS expressions involving parallel composition has been studied in some depth. We refer the reader to [Liu93] in which Liu reviews previous work and shows that rather severe restrictions on the forms of equations are required for decidability (of the existence of solutions).

We note that closely related work has been done (independently) by Drost, who in [Dro94] gives a rule based unification algorithm, a proof of its correctness and a complexity analysis. We have not investigated how the sets of unifiers produced are related to those described here.

5.1 The consequence relation and unification

Definition E_{1} = F_{1} ∧ ⋯ ∧ E_{m} = F_{m} ⊢ G_{1} = H_{1} ∨ ⋯ ∨ G_{n} = H_{n} holds iff for all substitutions ρ if ∀i ∈ 1..m . E_{i}ρ ∼ F_{i}ρ then ∃j ∈ 1..n . G_{j}ρ ∼ H_{j}ρ.

The following is immediate from the definition.

Proposition 77 ⊢ is a regular, ordinary consequence relation as defined in [Avr91], i.e. the rules below for reflexivity, cut and weakening are sound and multiplicity can be neglected. Letting A and Γ, Δ, Θ range over equations and finite sets of equations respectively:

A ⊢ A refl
Γ_{1} ⊢ Δ_{1}, A A, Γ_{2} ⊢ Δ_{2}

Γ_{1}, Γ_{2} ⊢ Δ_{1}, Δ_{2} cut

{Γ ⊢ Δ \atop Θ, Γ ⊢ Δ} w − l  {Γ ⊢ Δ \atop Γ ⊢ Δ, Θ} w − r

We recall some standard definitions from [BS93], instantiating them to the setting of bisimulation over μ-expressions.

Definition A unification problem is a finite set {E_{1} = F_{1}, …, E_{n} = F_{n}} of equations between μ-expressions. A unifier for this is a substitution ρ satisfying all the equations up to bisimulation, i.e. such that ∀i ∈ 1..n . E_{i}ρ ∼ F_{i}ρ. The set U of all unifiers can be ordered by σ < θ iff there exists a substitution λ such that for all variables x free in the problem σ(x)λ ∼ θ(x). (This is clearly a preorder.) A complete set C ⊆ U of unifiers is one such that ∀θ ∈ U . ∃σ ∈ C . σ < θ. A minimal complete set is a complete set for which < is a discrete order.

Lemma 78 If for any unification problem there is a finite computable complete set of unifiers then the consequence relation is decidable.

Proof Consider the sequent

E_{1} = F_{1} ∧ ⋯ ∧ E_{m} = F_{m} ⊢ G_{1} = H_{1} ∨ ⋯ ∨ G_{n} = H_{n}

and let C be a finite complete set of unifiers for the problem {E_{1} = F_{1}, …, E_{m} = F_{m}}. We show that the sequent holds iff ∀σ ∈ C . ∃j ∈ 1..n . G_{j}σ ∼ H_{j}σ. The left to right direction is immediate from the definitions. For the other, consider an arbitrary substitution ρ such that ∀i ∈ 1..m . E_{i}ρ ∼ F_{i}ρ. By definition ρ is a unifier so there is some σ ∈ C . σ < ρ, i.e. ∃λ . ∀x . ρ(x) ∼ σ(x)λ. By the premise ∃j ∈ 1..n . G_{j}σ ∼ H_{j}σ but bisimulation is substitutive so G_{j}σλ ∼ H_{j}σλ. □

5.2 Unification for charts

It is convenient to work with transition systems rather than directly with μ-expressions. Accordingly we define charts and chart substitution. These are essentially as in §2.1.1, differing only in that for this chapter charts have no start state.

Definition A chart is a tuple ⟨S, ⟶, ▷⟩ where S is a set of states, ⟶ ⊆ S × Act × S is a transition relation and ▷ ⊆ S × Var is a visibility predicate.

Except where otherwise stated we consider only finite state charts, i.e. those for which all three components are finite. Substitution over charts is as expected — we give an explicit definition for concreteness.

Definition A chart substitution τ is a chart (say T) together with a function τ from a finite subset A of Var to the state set of T. The result of a substitution Sτ is a chart with states S ⊎ T and the least transition and visibility relations satisfying the following clauses.

{s⟶^{a}s′ \atop inl(s)⟶^{a}inl(s′)} {t⟶^{a}t′ \atop inr(t)⟶^{a}inr(t′)} \begin{matrix}s ▷ y & y ∈ A & τ(y)⟶^{a}t′ \\ inl(s)⟶^{a}inr(t′) \end{matrix}
{s ▷ x ∉ A \atop inl(s) ▷ x}  {t ▷ x \atop inr(t) ▷ x}  \begin{matrix}s ▷ y ∈ A & τ(y) ▷ x \\ inl(s) ▷ x \end{matrix}

Notation We will often omit the injections into disjoint unions. If s is a state of a chart S then sσ is the corresponding state in Sσ.

Definition If S is a chart ⟨S, ⟶, ▷⟩ then Var(S) is the range of ▷, i.e. the set of variables visible to any state within it and Act(S) is the set of actions occurring in it. If s is a state of a chart then vis(s) =^{def} { x | s ▷ x }.

Definition A unification problem is a finite set { s_{i} = s′_{i} | i ∈ I } of pairs of states within a chart. A unifier for such is a substitution θ with domain Var(S) such that ∀i ∈ I . s_{i}θ ∼ s′_{i}θ.

Notation From now on we fix a unification problem as above. We let R range over pairs of a symmetric relation R ⊆ S × S and a relation ⟶_{R} ⊆ Var(S) × Act × S.

Definition For any R we define a substitution σ_{R} as follows. First, we introduce new variables V_{A} indexed by nonempty sets A of the variables occurring in S and put

V_{R} =^{def} { V_{A} | ∀s, s′ ∈ S . s R s′ ⇒ ((A ∩ vis(s) ≠ {}) ⟺ (A ∩ vis(s′) ≠ {})) }.

We define a chart S_{2} =^{def} ⟨S ⊎ Var(S), ⟶ ∪ ▷ ⟶_{R} ∪ ⟶_{R}, ▷_{R}⟩ where

s ▷_{R} V_{A} ⟺ V_{A} ∈ V_{R} ∧ ∃x . s ▷ x ∈ A
x ▷_{R} V_{A} ⟺ V_{A} ∈ V_{R} ∧ x ∈ A.

The substitution σ_{R} takes a variable x ∈ Var(S) to the state x of S_{2}.

Definition R is a solution bisimulation if:

1. R is a bisimulation on the chart ⟨S, ⟶ ∪ ▷ ⟶_{R}, {}⟩.

2. ∀i ∈ I . s_{i} R s′_{i}.

Lemma 79 The set of solution bisimulations is finite and computable.

Proof There are a bounded number of relations R, ⟶_{R} and it is decidable whether each is a solution bisimulation. □

Lemma 80 For any solution bisimulation R, the substitution σ_{R} is a unifier.

Proof The chart Sσ_{R} has states S⊎(S⊎Var(S)). We let inl(s), inr(s), x range over these components respectively. Letting α, β range over {l, r} it is straightforward to show that it has the transitions generated by

s⟶^{a}s′ ⇒ inα(s)⟶^{a}inα(s′)
s ▷ ⟶^{a}_{R}s′ ⇒ inα(s)⟶^{a}inr(s′)
x⟶^{a}_{R}s′ ⇒ x⟶^{a}inr(s′)

and the visibilities generated by

s ▷_{R} V_{A} ⇒ inα(s) ▷ V_{A}
x ▷_{R} V_{A} ⇒ x ▷ V_{A}.

It is then straightforward to check that

Q =^{def} { inα(s), inβ(s′) | s R s′ }

is a bisimulation with ∀i ∈ I . inl(s_{i}) Q inl(s′_{i}). □

This gives us a finite computable set of unifiers:

{ σ_{R} | R is a solution bisimulation }.

It remains to show that this is complete.

Definition A substitution θ with domain Var(S) satisfies an R (which is not necessarily a solution bisimulation) if:

3. ∀s, t ∈ S . s R t ⇒ sθ ∼ tθ.

4. ∀x ∈ Var(S), s ∈ S . x⟶^{a}_{R}s ⟺ θ(x)⟶^{a} ∼ sθ.

Lemma 81 If θ is a substitution with domain Var(S) that satisfies R then θ factors through the substitution σ_{R}.

Proof

Definition Given a finite set P of processes let their intersection ⋂ P be some minimal member of the bisimulation class of

∑{ a.q | ∀p ∈ P . p⟶^{a} ∼ q } + ∑{ x | ∀p ∈ P . p ▷ x }.

If all elements of P are finite state then ⋂ P is also finite state.

5.2. Unification for charts 85 Definition The substitution λ has range V_{R} as defined above and for V_{A} ∈ V_{R}

λ(V_{A}) =^{def} ⋂{ θ(x) | x ∈ A }.

We will show for all x ∈ Var(S) that θ(x) ∼ σ_{R}(x)λ. First we give two lemmas exploiting the structure of the set V_{R} of variables.

Lemma 82 If θ(x)⟶^{a}p and ¬∃s ∈ S . sθ ∼ p then ∃V_{A} ∈ V_{R} . x ∈ A ∧

∀y ∈ A . θ(y)⟶^{a} ∼ p.

Lemma 83 If θ(x) ▷ z then ∃V_{A} ∈ V_{R} . x ∈ A ∧ ∀y ∈ A . θ(y) ▷ z. Proof Only the first is given here — the other is similar. We show that there exists a strictly increasing sequence of sets A_{k} ⊆ Var(S) with A_{0} =^{def} {x} all of which satisfy

∀y ∈ A_{k} . θ(y)⟶^{a} ∼ p.

Suppose V_{A_{k}} ∉ V_{R}, otherwise we are done. There are then some s, s′ ∈ S and y such that

s R s′
y ∈ A_{k} ∩ vis(s)
{} = A_{k} ∩ vis(s′).

By induction θ(y)⟶^{a} ∼ p so sθ⟶^{a} ∼ p. By clause 3 s′θ⟶^{a} ∼ p so either • s′⟶^{a}s′′ ∧ s′′θ ∼ p, contradicting the premise, or

• ∃y′ ∈ vis(s′) − A_{k} . θ(y′)⟶^{a} ∼ p, in which case we put A_{k+1} =^{def}

A_{k} ∪ {y′}.

□

It is useful to use a simple ‘bisimulation up to’ technique.

Definition If ⟨S, ⟶_{S}, ▷_{S}⟩, ⟨T, ⟶_{T} , ▷_{T} ⟩ are charts then Q ⊆ S × T is a bisimulation up to ∼ if s Q t implies

• s⟶^{a}s′ ⇒ ∃t′ . t⟶^{a}t′ ∧ s′ (∼ ∪ ∼ Q ∼) t′

• s ▷_{S} x ⇒ t ▷_{T} x and symmetrically.

Proposition 84 If Q is a bisimulation up to ∼ then ∼ ∪ ∼ Q ∼ is a bisimulation.

Proof Straightforward. □

Now let

S_{1} =^{def} ⟨S ∪ Var(S), ⟶, ▷ ∪ id_{Var(S)}⟩
S_{2} =^{def} ⟨S ∪ Var(S), ⟶ ∪ ▷ ⟶_{R} ∪ ⟶_{R}, ▷_{R}⟩
Q =^{def} id_{S∪Var(S)}.

We check below that Q is a bisimulation up to ∼ between S_{1}θ and S_{2}λ. The result follows by noting that the state x of S_{1} is bisimilar to the one state chart ‘x’ and that the state x of S_{2} is σ_{R}(x) by definition.

We give only the transition part for pairs ⟨s, s⟩ ∈ Q — the rest is similar. There are two cases for transitions of sθ:

• s⟶^{a}s′ ∧ sθ⟶^{a}s′θ. Then sλ⟶^{a}s′λ.

• s ▷ x ∧ θ(x)⟶^{a}p ∧ sθ⟶^{a}p. Suppose ∃s′ ∈ S.s′θ ∼ p. Then by 4⇐ x⟶^{a}_{R}s′

so s⟶^{a}_{S_{2}}s′ and sλ⟶^{a}s′λ Q^{−1} s′θ ∼ p. Now suppose not. Then by Lemma

82 ∃V_{A} ∈ V . x ∈ A ∧ λ(V_{A})⟶^{a} ∼ p so s ▷_{R} V_{A} and sλ⟶^{a} ∼ p.

For transitions of sλ there are three cases:

• s⟶^{a}s′ ∧ sλ⟶^{a}s′λ. Then sθ⟶^{a}s′θ.

• s ▷ x⟶^{a}_{R}s′ ∧ sλ⟶^{a}s′λ. Then by 4 ⇒ θ(x)⟶^{a} ∼ s′θ so sθ⟶^{a} ∼ s′θ Q s′λ.

• s ▷_{R} V_{A} ∧ λ(V_{A})⟶^{a}q ∧ sλ⟶^{a}q. Then by the definitions of ▷_{R} and λ sθ⟶^{a} ∼

q.

□

Remark It is not the case that for any solution bisimulation σ_{R} satisfies R — the right-to-left implication of 4 may fail, essentially because ⟶_{R} is too small. For example take S =^{def} ⟨{1, 2, 3}, {}, {⟨1, x⟩}⟩, the problem {2 = 3}, R =^{def} {⟨2, 3⟩, ⟨3, 2⟩} and ⟶_{R} =^{def} {x⟶^{a}2}. Here V_{R} = {V_{{x}}} and σ_{R}(x) = V_{{x}} + a0. We have

σ_{R}(x)⟶^{a} ∼ (3σ_{R}) but ¬(x⟶^{a}_{R}3).

Lemma 85 If θ is a unifier then there is a solution bisimulation R(θ) that is satisfied by it.

Proof Define R, ⟶_{R} by:

3. ∀s, t ∈ S . s R t ⟺ sθ ∼ tθ.

4. ∀x ∈ Var(S), s ∈ S . x⟶^{a}_{R}s ⟺ θ(x)⟶^{a} ∼ sθ.

Trivially, R is symmetric (and reflexive), is satisfied by θ and ∀i ∈ I . s_{i} R s′_{i}. It remains to check that R is a bisimulation on ⟨S, ⟶ ∪ ▷ ⟶_{R}, {}⟩. Suppose sθ ∼ tθ. There are two possible transitions:

• s⟶^{a}s′, in which case sθ⟶^{a}s′θ.

• s ▷ y⟶^{a}_{R}s′, in which case θ(y)⟶^{a} ∼ s′θ so sθ⟶^{a} ∼ s′θ.

In either case tθ⟶^{a} ∼ s′θ and one of the following holds.

• t⟶^{a}t′ ∧ t′θ ∼ s′θ. Then t (⟶^{a} ∪ ▷ ⟶^{a}_{R}) t′ R s′.

• t ▷ y ∧ θ(y)⟶^{a} ∼ s′θ. Then y⟶^{a}_{R}s′ so t (⟶^{a} ∪ ▷ ⟶^{a}_{R}) s′ R s′.

□

Theorem 14 The set { σ_{R} | R is a solution bisimulation} is a finite computable complete set of unifiers.

Proof It is finite and computable by Lemma 79 and contains only unifiers by Lemma 80. For completeness suppose θ is an arbitrary unifier. By Lemma 85 there is a solution bisimulation R satisfied by it, then by Lemma 81 θ factors through σ_{R}. □

Corollary 86 The consequence relation ⊢ over sets of equations between μ-expressions is decidable.

Proof By Lemma 78. □

Remark The conjunction can be internalised, i.e.

E_{1} = F_{1} ∧ ⋯ ∧ E_{m} = F_{m} ⊢ G_{1} = H_{1} ∨ ⋯ ∨ G_{n} = H_{n}

holds iff

( ∑_{i∈1..m} a_{i}E_{i} = ∑_{i∈1..m} a_{i}F_{i}) ⊢ G_{1} = H_{1} ∨ ⋯ ∨ G_{n} = H_{n}

does.

5.3 Minimal sets of unifiers

The complete sets of the previous section can be reduced somewhat, as follows.

Corollary 87 The set of all σ_{R,⟶_{R}} where

• R, ⟶_{R} is a solution bisimulation.

• R is an equivalence relation containing bisimulation over S.

• R, ⟶_{R} is minimal with respect to set inclusion among the R′, ⟶_{R} satisfying the above.

is a complete set of unifiers.

Proof From Theorem 14 and the observations that for ⟨R, ⟶_{R}⟩, ⟨R′, ⟶_{R}⟩ if R ⊆ R′ then σ_{R} < σ_{R′} and if R′ is the reflexive symmetric transitive closure of R then σ_{R} = σ_{R′}. □

These may still not be minimal. For example the set for the problem a0+x = a0+x contains both x ↦ V_{{x}} and x ↦ a0+V_{{x}}. We do not have a nice characterisation of the minimal sets (in contrast to that of [BB88] for certain set equations) but coarse bounds on their size can be easily given. An upper bound from counting the number of relations R, ⟶_{R} is

2^{|S|×|S|} × 2^{|Var(S)|×|Act(S)|×|S|}.

For an exponential lower bound, the problem

a0 = a0 + ∑_{i∈1..n} x_{i}

has 2^{n} incomparable unifiers.

5.4 Unification for finite processes

Theorem 14 further implies the existence of finite complete sets of unifiers for the finite process expressions, i.e. those given by

E ::= 0 | X | aE | E + E.

The reasoning is general and may well be known. We suppose ∼ is a substitutive congruence and consider a subset T of terms satisfying the following (allowing E, F to range over all μ-expressions).

• Var ⊆ T

• E, F ∈ T ⇒ E[F/x] ∈ T

• E[F/x] ∼∈ T ⇒ ∃E′ ∈ T . E ∼ E′

• E[F/x] ∼∈ T ∧ x ∈ F V (E) ⇒ ∃F′ ∈ T . F ∼ F′ ∧ F V (F′) ⊆ F V (F)

The finite process expressions and bisimulation clearly satisfy these conditions.

Definition A T -unification problem is a finite set {E_{1} = F_{1}, …, E_{n} = F_{n}} of equations between members of T. A T -unifier for this is a substitution ρ with range in T satisfying all the equations up to bisimulation, i.e. such that ∀i ∈ 1..n . E_{i}ρ ∼ F_{i}ρ. The set U_{T} of all T -unifiers can be ordered by σ <_{T} θ iff there exists a substitution λ with range in T such that for all variables x free in the problem σ(x)λ ∼ θ(x). (This is clearly a preorder.) A T -complete set C ⊆ U_{T} of T -unifiers is one such that ∀θ ∈ U_{T} . ∃σ ∈ C . σ_{T} <_{T} θ.

Proposition 88 If C is complete for a T -problem and satisfies

∀σ ∈ C . ∀E ∈ ran(σ) . E ∼∈ T ⇒ E ∈ T

then C ∩ U_{T} is T -complete for it.

Proof The last two conditions above imply their vector forms, i.e.

• E[F̃/x̃] ∼∈ T ⇒ ∃E′ ∈ T . E ∼ E′ • Ẽ[F̃/x̃] ∼∈ T^{m} ∧ x̃ ⊆ F V (Ẽ) ⇒ ∃F̃′ ∈ T^{n} . ∀i . F_{i} ∼ F′_{i} ∧ F V (F′_{i}) ⊆

F V (F_{i})

by induction on the length of x̃. Now suppose θ is a T -unifier. By C complete there is a substitution λ such that ∀x.σ(x)λ ∼ θ(x). By the second and first vector forms we can find λ′ and σ′ with ranges in T. The premise then implies that the range of σ is also in T and we have σ <_{T} θ. □

Corollary 89 There are finite computable complete sets of unifiers for problems over the finite process expressions.

Proof It remains only to note that if ∃E′ ∈ T . E′ ∼ E then such an E′ can be constructed. □

Remark The consequence relation ⊢_{f} obtained by restricting to finite process expressions is strictly larger than ⊢. The inclusion is trivial and for example ax = x ⊢_{f} a0 = 0 but ax = x ⊬ a0 = 0.

Remark Lemmas 81 and 85 hold for infinite state unifiers θ (of finite state problems) so the set of unifiers given in Theorem 14 is also complete for such and the consequence relation ⊢_{i} obtained by allowing arbitrary charts coincides with ⊢ over the finite state problems.

Conclusion

The main contributions of the thesis are, briefly, as follows.

In Chapter 2 a conceptually simple (albeit notationally complex) infinite set of equation schemes over μ-expressions was given and shown to be complete for bisimulation. This gave rise to conjectures about the completeness of various subsets, one of which led to the result of Chapter 3.

In Chapter 3 a simply typed lambda calculus was introduced in which a large class of equation schemes over μ-expressions can be expressed as equations. A higher order bisimulation was defined over the lambda terms, shown to be decidable and (when restricted to terms with first order variables) to coincide with a more extensional equality. Examination of the coincidence showed that equational axioms preserve certain loop properties and hence that no finite, equational, first order axiomatisation for bisimulation over the μ-expressions can exist.

In Chapter 4 it was shown that no finite equational axiomatisation for bisimulation over sets of ∗-expressions containing a zero process can exist, in sharp contrast to the extant positive result for BPA^{∗}. The lambda terms were viewed as a fragment of the higher order π calculus and higher order bisimulation was shown to coincide with the normal bisimulation of Sangiorgi. The work was related to the theory of non-well-founded sets. Finally, a finite equational axiomatisation of weak congruence relative to bisimulation was given. The soundness proof made use of a definition of weak higher order congruence.

In Chapter 5 it was shown that unification problems over μ-expressions have finite computable complete sets of unifiers and hence that certain sequents over μ-expressions are decidable.

In the rest of this chapter we discuss possible future work, including the several problems that have been left open.

6.1 Higher order bisimulation

In Chapter 3 we were able to show the coincidence of ∼_{ho} and ∼_{ext} only for terms containing variables of at most first order types. We conjecture that the coincidence holds for all terms but have been unable to prove either inclusion. Our proof for the first order case depended on an inductive characterisation of the transitions of a substituted term Eρ (Proposition 53) which in turn depended on a tight relationship between β-reduction and transitions (Lemma 56). These cannot be simply generalized to the general case, for which we expect that a more sophisticated induction (corresponding to a normalisation proof for general β reduction) is required. It is natural to consider the lifting of ∼_{ho} and ∼_{ext} to logical relations over terms of all types (containing variables of arbitrary types). This enables a number of related conjectures to be stated.

We recall from [Mit90] the definition of logical relation over the typed applicative structure of terms in the T_{ω}^{σ}.

Definition If ∼ is a relation over T_{ω}^{P} then

∼^{LR}^{P} =^{def} ∼
E ∼^{LR}^{σ → τ} F =^{def} ∀E′, F′ ∈ T_{ω}^{σ} . E′ ∼^{LR}^{σ} F′ ⇒ EE′ ∼^{LR}^{τ} F F′.

The relations ∼^{LR}^{σ} are a logical relation if for each constant c: σ (here with c one of 0, a, +, fix ) we have c ∼^{LR}^{σ} c.

It is immediate from Propositions 34 and 51 that ∼^{LR}_{ext}^{σ} and ∼^{LR}_{ho}^{σ} are logical partial equivalence relations. The conjectures can now be stated, in each of which the types σ and τ are universally quantified.

Conjecture 90

1. ∼^{LR}_{ext}^{σ} is reflexive.

2. ∼^{LR}_{ho}^{σ} is reflexive.

3. If E ∼_{ho}^{σ} F and G: τ then E[G/x] ∼_{ho}^{σ} F [G/x].

4. ∼_{ho}^{σ} = ∼^{LR}_{ho}^{σ}.

5. ∼_{ho} ⊆ ∼_{ext}.

6. ∼_{ho} = ∼_{ext}.

7. ∼_{ho}^{σ} = ∼^{LR}_{ext}^{σ}.

There are a number of implications between these, mostly trivial. We note that using Proposition 51 clause 3 can be shown to be equivalent to the congruence of ∼_{ho}^{σ} for application on the left or right. Further, clause 3 implies clause 5 and is implied by clause 6. We note also that clause 4 is equivalent to the conjunction of clauses 2 and 3, using straightforward inductions on types.

A possible starting point for the inclusion ∼_{ho}⊆∼_{ext} is therefore the proof by Sangiorgi that context bisimulation is a congruence for application [San94, Appendix B]. The work in [Sta82], in which βη equality is reduced to βη equality at a particular type, may also be relevant.

For the inclusion ∼_{ext}⊆∼_{ho} a simple proof would need, for any E ∼_{ext} F, a substitution ρ for E, F such that a higher order bisimulation relating E and F can be extracted from a bisimulation relating Eρ and F ρ. A sample problematic case is the pair of terms

E =^{def} x (λw: P. x (λu: P. cw + du))
F =^{def} x (λw: P. x (λu: P. cu + dw)),

where x:(P → P) → P, which are not higher order bisimilar. This rules out substitutions of the form

ρ(x) =^{def} λy: P → P. a_{x}(y G),

with y not free in G, as for these Eρ ∼ F ρ.

There are three other obvious developments of higher order bisimulation.

In §3.4 higher order bisimulation was shown to be decidable by the exponential technique of checking whether any relation over a given set is a loose bisimulation. One could look for a tighter complexity result, based on the partition refinement algorithm of Paige and Tarjan [PT87].

For higher order process calculi one is interested in equivalences that abstract from internal actions. In §4.4 we defined a weak higher order congruence, ≈_{ho}^{c}, that does this. One could develop the theory of ≈_{ho}^{c}, in particular by showing a converse to Theorem 12, i.e. showing that ≈_{ext}^{c}⊆≈_{ho}^{c}, and exhibiting a tight connection between ≈_{ho}^{c} and the equivalences over the higher order π calculus. The literature contains many different equivalences over transition systems that abstract from internal actions. There is at least as much scope for different higher order equivalences, and even less understanding of the criteria for choosing between them.

Throughout this thesis we have considered only sequential nondeterministic processes from very simple signatures. For these it is possible to characterise the extensional equality ∼_{ext} over open terms by a bisimulation involving visibility judgments, resting on results such as

E[F/X]⟶^{a}A iff (E⟶^{a}E′ ∧ E′[F/X] = A) ∨ (E ▷ X ∧ F ⟶^{a}A)

for the μ-expressions and Proposition 53 for lambda terms with first order variables. There does not appear to be an analogous result for terms involving parallel composition (although formulating a precise result to that effect is nontrivial). One could investigate the class of GSOS-definable (say) operators for which there are analogues of the visibility judgment and higher order bisimulation — perhaps something like those for which the target of any transition depends only on the ‘near future’ behaviour of all except one argument.

6.2 Axiomatisability

The space of possible finite axiomatisability results is very large. They can be classified along three main dimensions.

Syntax: we have considered μ-expressions and several classes of ∗-expressions.

Equivalence: this can be loosely subdivided into a linear-branching time dimension and a dimension of abstraction from internal actions. We have considered infinite term equality, (strong) bisimulation, weak congruence and (strong) language/trace congruence.

Logic: we have considered equational and horn clause (both pure and impure) axiomatisations.

For axiomatisations over μ-expressions there are further dimensions, namely the orders of free variables that may occur in axioms and whether variables over actions are admitted. We have generally considered only the first order case.

Some of the known results were summarised in Figure 2–2, page 21. It is reproduced below, omitting references. The results shown are for strong equivalences, that do not abstract from internal actions, and the results for μ-expressions are for axioms with at most first order variables and without variables over actions.

\begin{matrix}√ & (impure) \\ √ \end{matrix}

[figure]
horn clause \begin{matrix}√ & (impure) \\ √ \end{matrix}  √(impure)
× √  × bisimulation
[figure]

equational

×
√(for events ≥ 1)

language or trace

∗-expressions  μ-expressions

There are a great many conjectures suggested by this and by the multi-dimensional diagram of which it is a slice. A few of these seem to have some compelling interest, albeit largely technical. They are discussed below. It should be noted that bisimulation of μ-expressions is very close to infinite term equality of terms from an arbitrary first order signature with recursion. Some of these questions could be posed in that more general setting.

In the diagrams below conjectures are indicated by ‘?’, sometimes annotated by √ or × if we expect a positive or negative result. Relative axiomatisability results are indicated by double arrows ⇒.

With variables of arbitrary order

arbitrary order  ?×  ?×

first order ×(Thm. 6) \overline{⇐}  ×(Thm. 6)
bisimulation  infinite term equality

μ-expressions strong equational

We would like to generalise Theorem 6 to allow variables of arbitrary order, not simply those of first order. A proof would presumably depend on a proof of the coincidence of ∼_{ho} and ∼_{ext} for all terms, as discussed in the previous section. For simplicity one could first consider infinite term equality. In the first order case this might enable the (somewhat complex) proof of Theorem 6 to be simplified and in the arbitrary order case be a useful stepping stone towards the result for bisimulation.

A further question is the existence of good (possibly infinitary) ω-complete axiomatisations for bisimulation, i.e. axiomatisations complete for ∼_{ext} over T_{ω}^{P} or T_{1}^{P}, not just over T_{0}^{P}.

Abstracting from τ

horn clause

√[BÉ94]

?√

√[Mil89](impure)

equational ×(Thm. 6) \overline{⇒ (Thm. 13)} ?×
bisimulation  weak congruence

μ-expressions branching time first order with and without action variables

The left edge is the back right edge of the cube. As discussed in §4.4.2, to express interesting axioms about weak congruence as pure typed equations we need to modify the signature slightly, adding a base type A of actions and taking constants

0 : P

a: A for each a ∈ Act (including τ) .: A → P → P + : P → P → P fix :(P → P) → P.

We conjecture that the proof of Theorem 6 could be adapted to this signature without difficulty and to weak congruence at the cost of some uninteresting complications. A more interesting result would be to show that axiom E3, used in the pure horn clause axiomatisation of bisimulation in [BÉ94] and reproduced in §2.3.3, is sound for weak congruence. Together with the result of [BÉ94] and Theorem 13 (the relative axiomatisation of weak congruence over bisimulation) this would give a pure horn clause axiomatisation for weak congruence.

Linear time

horn clause ?√ √[Rab93](impure)

√[BÉ94]

equational  ?×  \overline{? ⇐}  ×(Thm. 6)
trace congruence  bisimulation

μ-expressions

strong first order with and without action variables

This is the right hand face of the cube. The non-axiomatisability proof of Theorem 6 for bisimulation of μ-expressions and that reproduced in §2.3.4 from [Con71] for language equivalence of ∗-expressions are based on similar intuitions, that a finite set of axioms cannot introduce an arbitrary prime factor into the length of a recursion or iteration. We would like to make this precise, e.g. by giving a non-axiomatisability proof for all equivalences, finer than or equal to trace congruence, over μ-expressions and hence over ∗-expressions.

Another interesting question about trace congruence is whether it is equationally axiomatisable relative to bisimulation. A negative result would immediately give non-axiomatisability. A positive result could be combined with the result of [BÉ94], if E3 is sound for trace congruence, to give a pure horn clause axiomatisation.

Bisimulation of ∗-expressions

×{0, 1, a, +, ., ^{⋆} }(Thm. 11)
[figure]
×{0, a, +, ., ^{⋆} }(Thm. 11)  ?{1, a, +, ., ^{⋆} }
[figure]
√{0, a . , +, a^{⋆} }[Fok94]  √{a, +, ., ^{⋆} }[FZ94]

∗-expressions bisimulation strong equational

This expands the lower back left corner of the cube. The lines indicate signature inclusions. As discussed in §4.1.2 we would like to know whether bisimulation over the expressions of {1, a, +, ., ^{⋆} } is equationally axiomatisable and cannot use a simple adaption of the proof of Theorem 11, depending only on the widths of axioms, to show that it is not. One could also investigate whether the axiomatisation of weak congruence over {0, a . , +, a^{⋆} } given in [AI95] can be adapted to {a, +, ., ^{⋆} }, possibly using ideas from the proof of Theorem 13 that over μexpressions weak congruence is axiomatisable relative to bisimulation.

Incompleteness of axiomatisations with unbounded width

The proof of Theorem 6 is somewhat crude in that it ignores all information about putative axiomatisations except for the widths of the bisimulations that they provide. We conjectured in §2.3.4 that there are subsets of the axioms C_{mn} of unbounded width that are incomplete even together with any finite set of other axioms. One might begin by generalising Proposition 92 below.

Definition For n ≥ 1 an n-lts is a finite transition system over n actions, each state having exactly one outgoing transition on each action (and no visibilities). For k ≥ 1 we write ∼^{k} for the transitive closure of the union of all bisimulations of width ≤ k.

The 1-lts’ are particularly simple, enabling us to give a precise characterisation of ∼^{k}.

Proposition 91 For any 1-lts S there exist m ≥ 0, n ≥ 1 such that S ∼^{1} S_{n,m} =^{def} a^{m+n−1}μXa^{n}X.

Proposition 92 If m, m′ ≥ 0, n, n′ ≥ 1 and k ≥ 2 then S_{n,m} ∼^{k} S_{n′,m′} iff for all primes p, if n and n′ have different numbers of factors of p then p ≤ k.

Proof Straightforward, along the lines of the proof of Lemma 63. □

6.3 Unification

In Chapter 5 we showed that for unification problems over μ-expressions (equivalently, over lambda terms containing only zero order variables) there exist finite computable complete sets of unifiers up to bisimulation. It remains, however, to characterise the minimal such sets.

It follows from their existence that the soundness of sequents over μ-expressions is decidable. We would like to have a decidability result for sequents over lambda terms containing first order variables, particularly as these suffice to express the axiomatisation of Bloom and Ésik.

Appendix A

Completeness proof

This appendix contains the deferred parts of the proof of Theorem 1, i.e. completeness for the infinite system of §2.3. First we give a little technical result.

Lemma 93 If z_{j} is not free in F̃ for any j and z_{j} is not free in E for non-zero j then

⊢ μ ⟨X = E, Ỹ = F̃, Z̃ = G̃⟩ = μ ⟨X = E[μ ⟨Z̃ = G̃⟩/Z_{0}], Ỹ = F̃⟩.

Proof We show the two sides are alpha equivalent by induction on the size of Z̃. The base case is trivial. For the inductive step:

μ ⟨X = E, Ỹ = F̃, Z̃ = G̃, Z = G⟩
= μ ⟨X = E[μZG /Z], Ỹ = F̃[μZG /Z], Z̃ = G̃[μZG /Z]⟩ by def μ
=  μ ⟨X = E, Ỹ = F̃, Z̃ = G̃[μZG /Z]⟩  by premise
=  μ ⟨X = E[μ ⟨Z̃ = G̃[μZG /Z]⟩ /Z_{0}], Ỹ = F̃⟩  by ind. hyp.
=  μ ⟨X = E[μ ⟨Z̃ = G̃, Z = G⟩ /Z_{0}], Ỹ = F̃⟩  by def μ.
□

Lemma 18 For axioms Q, if Q ⊢ E_{i} = F_{i} for all i then Q ⊢ μ ⟨X̃ = Ẽ⟩ = μ ⟨X̃ = F̃⟩.

Proof By induction in the length of X̃. The base case is just μ-congruence. For the inductive step we need to know that if Q ⊢ E = F then Q ⊢ E[G/X] = F [G/X] which can be shown by induction on proofs, noting that none of the axioms constrain the forms of instantiations of metavariables (up to alpha conversion). □

Lemma 19 If π: n → n is a permutation with π(0) = 0 then B3 ⊢ μ ⟨X_{i} = E_{i} | i ∈ n⟩ = μ ⟨X_{π(i)} = E_{π(i)} | i ∈ n⟩.

Proof We show the result for permutations which simply exchange two values, which suffices. Here Ỹ = F̃ may be the empty sequence.

μ ⟨X̃ = Ẽ, X = E, Y = F, Ỹ = F̃⟩
= μ ⟨X̃ = Ẽρ, X = Eρ, Y = F ρ⟩  by def μ for some ρ with domain Ỹ
= μ ⟨X̃ = Ẽρ [ \begin{matrix}μY F ρ[μXEρ[μY F ρ /Y] /X] & / & Y \\ μXEρ[μY F ρ /Y] & / & X \end{matrix} ]⟩ by def μ
= μ ⟨X̃ = Ẽρ [ \begin{matrix}μY F ρ[μXEρ /X] & / & Y \\ μXEρ[μY F ρ[μXEρ /X] /Y] & / & X \end{matrix} ]⟩ by B3 and Lem. 18
= μ ⟨X̃ = Ẽ, Y = F, X = E, Ỹ = F̃⟩  by def μ
□

Lemma 20 For any μ-expression E there is a standard accessible sequence ⟨X̃ = Ẽ⟩ such that B ⊢ E = μ ⟨X̃ = Ẽ⟩.

Proof This is immediate from Lemmas 94 and 96 following. □

Definition A sequence of equations ⟨X̃ = Ẽ⟩ is almost standard if each E_{i} is of the form

E ::= 0 | X | aX | E + E

(where X ranges over all variables) and does not contain a free occurrence of X_{0}.

Lemma 94 For any expression E there is an almost standard sequence ⟨X̃ = Ẽ⟩ such that B ⊢ E = μ ⟨X̃ = Ẽ⟩.

Proof It is straightforward to show that for any E there is an expression μY F such that:

1. B ⊢ E = μY F.

2. Y does not occur in F.

3. F is of the form F ::= 0 | X | aμXF | μXF | F + F.

4. The bound variables of μY F are distinct from each other and from the free variables.

5. μY F has no subexpressions of the form μZZ + G.

We define a sequence of equations μ^{−1}(μY F) for any μY F that satisfies 3–5 as follows.

μ^{−1} (μY ∑_{0}^{l−1} a_{i}μX_{i}F_{i} + ∑_{l}^{l+m−1} μX_{i}F_{i} + ∑_{0}^{n} Y_{k})

=^{def}

[figure: \begin{matrix}Y = ∑_{0}^{l−1} a_{i}X_{i} + ∑_{l}^{l+m−1} X_{i} + ∑_{0}^{n} Y_{k} \\ μ^{−1}(μX_{i}F_{i}) | i ∈ l + m \end{matrix}]

Conditions 3,5 ensure that it is possible to write F in the form appearing in the left hand side. Condition 4 ensures that the result is a well defined equation sequence. Conditions 2,3 ensure that it is almost standard. It therefore suffices to show that B ⊢ μμ^{−1}(μY F) = μY F, which we do by induction on F. The inductive step requires the following.

Lemma 95 If:

• The sets of bound variables of μX_{i}F_{i} are disjoint for distinct i ∈ n.

• The bound variables of μX_{i}F_{i} and free variables of μX_{j}F_{j} are disjoint for i ≠ j.

• The bound variables of μX_{i}F_{i} and free variables of E are disjoint apart from X_{i}.

then

B ⊢ μ ⟨ \begin{matrix}Y = E \\ μ^{−1}(μX_{i}F_{i}) | i ∈ n \end{matrix} ⟩ = μY E[μX_{i}F_{i} /X_{i}]_{i∈n}.

Proof By induction on n. For n = 0 it is simply the definition of μ. For

n + 1 :

μ [figure] \begin{matrix}Y = E \\ μ^{−1}(μX_{i}F_{i}) | i ∈ n \\ μ^{−1}(μX_{n}F_{n}) \end{matrix} [figure]

= μ ⟨ \begin{matrix}Y = E[μμ^{−1}(μX_{n}F_{n}) /X_{n}] \\ μ^{−1}(μX_{i}F_{i}) | i ∈ n \end{matrix} ⟩ by Lemma 93
= μ ⟨ \begin{matrix}Y = E[μX_{n}F_{n} /X_{n}] \\ μ^{−1}(μX_{i}F_{i}) | i ∈ n \end{matrix} ⟩  by outer induction
= μY E[μX_{n}F_{n} /X_{n}][μX_{i}F_{i} /X_{i}]_{i∈n} by inner induction
= μY E[μX_{i}F_{i} /X_{i}]_{i∈n+1}.
□
□

Lemma 96 For any almost standard sequence ⟨X̃ = Ẽ⟩ there is a standard accessible sequence ⟨X̃ = F̃⟩ such that B ⊢ μ ⟨X̃ = Ẽ⟩ = μ ⟨X̃ = F̃⟩.

Proof Using Lemma 19, B2 and Lemma 18 we can ensure that no E_{i} is of the form X_{i} + G. We proceed by induction on the size of

{ X_{i} | X_{i} is a summand of some E_{j} }.

Using Lemma 19, if this set is not empty then we can assume it contains X_{n−1}. Let F̃, F be Ẽ with each occurrence of X_{n−1} as a summand of some E_{j} replaced by a new variable W. These occurrences of X_{n−1} can be provably replaced with E_{n−1} as follows (writing Ỹ , Y for X̃).

μ ⟨Ỹ = F̃[Y/W], Y = F ⟩
= μ ⟨Ỹ = F̃[Y/W][μY F /Y]⟩  by def μ
= μ ⟨Ỹ = F̃ [ \begin{matrix}μY F /W \\ μY F /Y \end{matrix} ]⟩
= μ ⟨Ỹ = F̃ [ \begin{matrix}F [μY F /W] /W \\ μY F /Y \end{matrix} ]⟩ by B1 and Lemma 18
= μ ⟨Ỹ = F̃[F/W][μY F /Y]⟩
= μ ⟨Ỹ = F̃[F/W], Y = F ⟩  by def μ.

Establishing accessibility is straightforward. □

Lemma 21 If ⟨X̃ = Ẽ⟩ is standard then ⟨X̃ = Ẽ⟩ ∼ μ ⟨X̃ = Ẽ⟩.

104 Appendix A. Completeness proof Proof Straightforward. □

Appendix B

Loop properties

In this appendix we relate the loop structures of the transition systems Eρ and E⋆ρ, showing that loops in one can be matched ‘on the nose’ by loops in the other instead of merely ‘up to bisimulation’. We show the following:

Lemma 97 If ρ is a substitution for E_{r} then loops(E_{r}ρ) = loops(E_{r}⋆ρ).

It is then straightforward to show Lemma 62 of section 3.6. The interesting direction is the inclusion ⊆. It does not follow from the bisimilarity of E_{r}ρ and E_{r}⋆ρ as the action of ρ may be non-injective — we may have

E_{r}ρ⟶^{∗}Eρ⟶^{l}E′ρ

with Eρ = E′ρ but E ≠ E′. We show below that for any loop of E_{r}ρ there is another with the same length headed by an instance of fix and then that any such can be matched in E_{r}⋆ρ.

Notation We write S for the set of states of E⋆ρ and for s ∈ S write fst(s) for the underlying term of s, i.e.

fst(⟨E⟩) =^{def} E
fst(⟨E, yẼ, d⟩) =^{def} E.

We adopt the assumptions on ρ from §3.5, letting y range over dom(ρ), z, Z over Z^{P} and w over K−dom(ρ)−F V (ran(ρ))−Z (which we assume contains infinitely many variables at type P).

Intuitively if s ∈ S and fst(s)ρ ▷ fix M then this instance of fix comes either from the term fst(s) or from the substitution ρ. To capture this we define new visibility predicates:

106 Appendix B. Loop properties Definition Let ▷′, ▷′′ ⊆ S×T_{1}^{P} be the least relations satisfying the clauses below. The numbering of clauses matches that in the definition of E⋆ρ in §3.6.

1. E ▷ F ⇒ ⟨E⟩ ▷′ F

2. n/a.

3. E ▷ yẼ ∧ H_{y} ▷ z_{j} ∧ ⟨E_{j}⟩ ▷′ F ⇒ ⟨E⟩ ▷′ F

4. n/a.

5. E ▷ yẼ ∧ d: H_{y}⟶^{l}H′ ∧ H′ ▷ z_{j} ∧ ⟨E_{j}⟩ ▷′ F ⇒ ⟨H′[Ẽ/z̃], yẼ, d⟩ ▷′ F

1. n/a.

2. E ▷ yẼ ∧ H_{y} ▷ H′ ⇒ ⟨E⟩ ▷′′ H′

3. E ▷ yẼ ∧ H_{y} ▷ z_{j} ∧ ⟨E_{j}⟩ ▷′′ F ⇒ ⟨E⟩ ▷′′ F

4. E ▷ yẼ ∧ d: H_{y}⟶^{l}H′ ∧ H′ ▷ H′′ ⇒ ⟨H′[Ẽ/z̃], yẼ, d⟩ ▷′′ H′′

5. E ▷ yẼ ∧ d: H_{y}⟶^{l}H′ ∧ H′ ▷ z_{j} ∧ ⟨E_{j}⟩ ▷′′ F ⇒ ⟨H′[Ẽ/z̃], yẼ, d⟩ ▷′′ F

These relations are complementary. Lemma 98 If fst(s)ρ ▷ fix λw: P. A then one of the following holds.

1. ∃E_{0} . s ▷′ fix λw: P. E_{0} ∧ E_{0}ρ = A

2. ∃H_{0}, Ẽ . s ▷′′ fix λw: P. H_{0} ∧ H_{0}[Ẽρ /z̃] = A Proof First suppose s = ⟨E⟩ and show the result by induction on Eρ ▷ fix λw: P. A using Proposition 53. The result for s not of this form is then a simple case analysis. □ Transitions of Eρ can be matched in E⋆ρ. Lemma 99 If one of

1. s =^{def} ⟨E[fix λw: P. F /w]⟩ and Eρ⟶^{a}A

2. s =^{def} ⟨H′[Ẽ[fix λw: P. F /w] /Z̃], yẼ[fix λw: P. F /w], d⟩ ∈ S and

H′[Ẽ/Z̃]ρ⟶^{a}A

hold then there exists t ∈ S such that s⟶^{a}t and either there exists E′ such that

t = ⟨E′[fix λw: P. F /w]⟩ and A = E′ρ

or there exists y′, Ẽ′, H′′, d′ such that

t = ⟨H′′[Ẽ′[fix λw: P. F /w] /Z̃′], y′Ẽ′[fix λw: P. F /w], d′⟩ and A = H′′[Ẽ′/Z̃′]ρ.

Proof Suppose 1. By Proposition 53 there exists E_{1} such that E⟶_{ρ}^{a}E_{1} and E_{1}ρ = A. The conclusion can be shown by induction on the definition of ⟶_{ρ}^{a}. Now suppose 2. By the assumptions on variables H′[Ẽ/Z̃]ρ = H′[Ẽρ /Z̃]

so H′[Ẽρ /Z̃]⟶^{a}A and either H′⟶^{a}H′′ ∧ H′′[Ẽρ /Z̃] = A or H′ ▷ Z_{j} ∧ E_{j}ρ⟶^{a}A.

The first case is trivial, the second follows from part 1. □

Transitions of Eρ that are headed by an instance of fix can be matched in E⋆ρ by transitions which have a destination state that is somewhat independent of their start state.

Lemma 100 If ⟨E⟩ ∈ S, E ▷ fix λw: P. F and F ρ⟶^{a}A then there exists t ∈ S such that

∀⟨E′′⟩ ∈ S . E′′ ▷ fix λw: P. F ⇒ ⟨E′′⟩⟶^{a}t

and either there exists E′ such that

t = ⟨E′[fix λw: P. F /w]⟩ and A = E′ρ

or there exists y′, Ẽ′, H′′, d′ such that

t = ⟨H′′[Ẽ′[fix λw: P. F /w] /Z̃′], y′Ẽ′[fix λw: P. F /w], d′⟩ and A = H′′[Ẽ′/Z̃′]ρ.

Proof By Proposition 53 there exists F′ such that F ⟶_{ρ}^{a}F′ and F′ρ = A. The result follows by considering cases of the definition of ⟶_{ρ}^{a}, using Lemma 99 for case 3. □

This can be strengthened to deal with all states of E⋆ρ.

Lemma 101 If s ∈ S, s ▷′ fix λw: P. F and F ρ⟶^{a}A then there exists t ∈ S such that

∀s′ ∈ S . s′ ▷′ fix λw: P. F ⇒ s′⟶^{a}t

and either there exists E′ such that

t = ⟨E′[fix λw: P. F /w]⟩ and A = E′ρ

or there exists y′, Ẽ′, H′′, d′ such that

t = ⟨H′′[Ẽ′[fix λw: P. F /w] /Z̃′], y′Ẽ′[fix λw: P. F /w], d′⟩ and A = H′′[Ẽ′/Z̃′]ρ.

Proof By an easy induction there exists ⟨E⟩ ∈ S such that E ▷ fix λw: P. F. By Lemma 100 there exists t ∈ S such that

∀⟨E′′⟩ ∈ S . E′′ ▷ fix λw: P. F ⇒ ⟨E′′⟩⟶^{a}t

and the second clause of the conclusion holds. It remains to check by induction on ▷′ that

∀s′ ∈ S . s′ ▷′ fix λw: P. F ⇒ s′⟶^{a}t.

□

Lemma 102 If one of

1. s =^{def} ⟨E[fix λw: P. F /w]⟩ and Eρ ▷ w

2. s =^{def} ⟨H′[Ẽ[fix λw: P. F /w] /Z̃], yẼ[fix λw: P. F /w], d⟩ ∈ S and

H′[Ẽ/Z̃]ρ ▷ w

hold then s ▷′ fix λw: P. F.

Proof Suppose 1. By Proposition 53 E ▷_{ρ} w. The conclusion can be shown by induction on the definition of ▷_{ρ}. The result for 2 is then straightforward. □

Finally we can prove:

Lemma 97 If ρ is a substitution for E_{r} then loops(E_{r}ρ) = loops(E_{r}⋆ρ).

Proof ⊇: Suppose ⟨E_{r}⟩⟶^{∗}s⟶^{l}s. By tracking transitions along the higher order bisimulation in the proof of Lemma 60 we can see that

E_{r}ρ⟶^{∗} fst(s)ρ⟶^{l} fst(s)ρ.

⊆: Suppose E_{r}ρ⟶^{∗}A⟶^{l}A. By Lemma 66 there exists a term fix λw: P. B, a finite set I and k_{i} ≥ 1 | i ∈ I such that E_{r}ρ⟶^{∗} ▷ fix λw: P. B, ∑_{I} k_{i} = l and ∀i . B⟶^{k_{i}} ▷ w.

By tracking transitions along the higher order bisimulation of Lemma 60 we have ⟨E_{r}⟩⟶^{∗}s for some s with fst(s)ρ ▷ fix λw: P. B. By Lemma 98 one of the following holds.

1. s ▷′ fix λw: P. F ∧ F ρ = B.

By induction on n if F ρ⟶^{n}A then there exist t ∈ S such that

∀s′ ∈ S . s′ ▷′ fix λw: P. F ⇒ s′⟶^{n}t

and either there exists E′ such that

t = ⟨E′[fix λw: P. F /w]⟩ and A = E′ρ

or there exists y′, Ẽ′, H′′, d′ such that

t = ⟨H′′[Ẽ′[fix λw: P. F /w] /Z̃′], y′Ẽ′[fix λw: P. F /w], d′⟩ and A = H′′[Ẽ′/Z̃′]ρ, using Lemma 101 for the base case and Lemma 99 for the inductive step. Finally, by Lemma 102, for all i ∈ I, if s′ ▷′ fix λw: P. F then

s′⟶^{k_{i}} ▷′ fix λw: P. F

so s (and hence ⟨E_{r}⟩) has a loop of length l.

2. s ▷′′ fix λw: P. H_{0} ∧ H_{0}[Ẽρ /z̃] = B.

We know that w is not free in Ẽρ so must have for each i that

H_{0}⟶H_{i}⟶^{k_{i}−1} ▷ w.

By induction on s ▷′′ fix λw: P. H_{0} there is some yẼ, d such that

s⟶⟨H_{i}[fix λw: P. H_{0} /w][Ẽ/z̃], yẼ, d⟩.

Further, this state has a loop of length l.

□

Bibliography

[Abr91] Samson Abramsky. A domain equation for bisimulation. Information and Control, 92,2:161–218, 1991.

[ABV92] Luca Aceto, Bard Bloom, and Frits Vaandrager. Turning SOS rules into equations. Technical Report CS-R9218, CWI, June 1992. To appear in the LICS ’92 special issue of Information and Computation.

[Acz88] Peter Aczel. Non-well-founded Sets, volume 14 of CSLI Lecture Notes. CSLI, 1988.

[AG87] K. B. Arkhangelskii and P. V. Gorshkov. Implicational axioms for the algebra of regular languages. Doklady Akad. Nauk, USSR, ser A., 10:67– 69, 1987. (in Russian).

[AH88] L. Aceto and M. Hennessy. Termination, deadlock and divergence. Technical Report 6/88, Sussex University, 1988.

[AI95] L. Aceto and A. Ingólfsdóttir. A complete equational axiomatization for prefix iteration with silent steps. Research Report RS–95–5, BRICS (Basic Research in Computer Science, Centre of the Danish Research Foundation), Department of Mathematics and Computer Science, Aalborg University, January 1995.

[Avr91] Arnon Avron. Simple consequence relations. Information and Computation, 92:105–139, 1991.

[BB88] Franz Baader and Wolfram Büttner. Unification in commutative idempotent monoids. Theoretical Computer Science, 56:345–353, 1988.

[BBK87] J. C. M. Baeten, J. A. Bergstra, and J. W. Klop. On the consistency of Koomen’s fair abstraction rule. Theoretical Computer Science, 51:129– 176, 1987.

[BBP94] J. A. Bergstra, I. Bethke, and A. Ponse. Process algebra with iteration. The Computer Journal, 37(4):243–258, 1994. Also as University of Amsterdam Programming Research Group report P9314.

[BÉ93a] Stephen L. Bloom and Zoltán Ésik. Equational axioms for regular sets. Math. Struct. in Comp. Science, 3:1–24, 1993.

[BÉ93b] Stephen L. Bloom and Zoltán Ésik. Iteration Theories: The Equational Logic of Iterative Processes. EATCS Monographs on Theoretical Computer Science. Springer-Verlag, 1993.

[BÉ94] Stephen L. Bloom and Zoltán Ésik. Iteration algebras of finite state process behaviors. Draft, February 1994.

[BK84] J. A. Bergstra and J. W. Klop. A complete inference system for regular processes with silent moves. Technical Report CS-R8420, CWI, 1984.

[Bof90] M. Boffa. Une remarque sur les systèmes complets d’identités rationelles. Theoret. Inform. Applic., 24(4):419–423, 1990.

[BS93] Franz Baader and Jörg H. Siekmann. Handbook of Logic in Artificial Intelligence and Logic Programming, chapter ‘Unification Theory’. Oxford University Press, 1993.

[BW90] J. C. M. Baeten and W. P. Weijland. Process Algebra. Cambridge Tracts in Theoretical Computer Science 18. Cambridge University Press, 1990.

[CEW58] Irving M. Copi, Calvin C. Elgot, and Jesse B. Wright. Realization of events by logical nets. Journal of the ACM, 5(2):181–196, April 1958.

[CHM93] Søren Christensen, Yoram Hirshfeld, and Faron Moller. Decomposability, decidability and axiomatisability for bisimulation equivalence on basic parallel processes. In Proc. 8th IEEE Symposium on Logic in Computer Science, pages 386–396, New York, 1993. IEEE Computer Society Press.

[CHM94] Søren Christensen, Yoram Hirshfeld, and Faron Moller. Decidable subsets of CCS. The Computer Journal, 37(4):233–242, 1994.

[Chr93] Søren Christensen. Decidability and Decomposition in Process Algebras. PhD thesis, University of Edinburgh, 1993. Also as CST–105–93.

[Con71] J. H. Conway. Regular Algebra and Finite Machines. Chapman and Hall, 1971.

[CS90] Rance Cleveland and Bernhard Steffen. A preorder for partial process specifications. In CONCUR 90, pages 141–151, 1990.

[Dro94] N. J. Drost. Unification in an algebra with choice and action prefix. Technical Report P9321, Programming Research Group, University of Amsterdam, July 1994.

[Fok94] W. J. Fokkink. A complete equational axiomatisation for prefix iteration. Information Processing Letters, 52(6):333–337, December 1994. Also as CWI report CS-R9415.

[FZ94] Wan Fokkink and Hans Zantema. Basic process algebra with iteration: Completeness of its equational axioms. The Computer Journal, 37(4):259–267, 1994. Also as CWI report CS–R9368.

[Gla90] R. J. van Glabeek. The linear time — branching time spectrum. In J. C. M. Baeten and J. W. Klop, editors, Proceedings CONCUR 90, Amsterdam, LNCS 458, pages 278–297, 1990.

[Gla93a] R. J. van Glabeek. A complete axiomatization for branching bisimulation congruence of finite-state behaviours. In Andrzej M. Borzyszkowski and Stefan Sokolowski, editors, Proceedings 18th MFCS, LNCS 711, pages 473–484, 1993.

[Gla93b] R. J. van Glabeek. Divergence bisimulation. Personal communication, 1993.

[Hen81] Matthew Hennessy. A term model for synchronous processes. Information and Control, 51:58–75, 1981.

[Hen88] Matthew Hennessy. Algebraic Theory of Processes. The MIT Press, 1988.

[HM80] Matthew Hennessy and Robin Milner. On observing nondeterminism and concurrency. In J. W. de Bakker and J. van Leeuwen, editors, Proceedings 7th Colloquium on Automata, Languages and Programming, LNCS 85, pages 299–309. Springer-Verlag, 1980.

[HP80] M. C. B. Hennessy and G. D. Plotkin. A term model for CCS. In Proceedings 9th MFCS, LNCS 88, 1980.

[HS91] H. Hüttel and C. Stirling. Actions speak louder than words: proving bisimilarity for context-free processes. In Proc. 6th IEEE Symposium on Logic in Computer Science, pages 376–386, New York, 1991. IEEE Computer Society Press.

[Hüt91] H. Hüttel. Decidability, Behavioural Equivalences and Infinite Transition Graphs. PhD thesis, University of Edinburgh, 1991. CST–86–91.

[Kle56] S. C. Kleene. Representation of events in nerve nets and finite automata. In C. E. Shannon and J. McCarthy, editors, Automata Studies, pages 3–41. Princeton University Press, 1956. Annals of Mathematics Studies 34.

[Koz94] Dexter Kozen. A completeness theorem for Kleene algebras and the algebra of regular events. Information and Computation, 110:366–390, 1994. Also in LICS ’91.

[Kro91] Daniel Krob. Complete systems of B-rational identities. Theoretical Computer Science, 89:207–343, 1991.

[Liu93] Xinxin Liu. On decidability and small model property of process equations. Technical Report 93:10, School of Cognitive and Computing Sciences, University of Sussex, 1993.

[Mil80] Robin Milner. A Calculus of Communicating Systems, LNCS 92. Springer-Verlag, 1980. Also published as LFCS report ECS-LFCS-86-7.

[Mil81] Robin Milner. A modal characterisation of observable machinebehaviour. In Proceedings CAAP ’81, LNCS 112, pages 25–34, 1981.

[Mil84] Robin Milner. A complete inference system for a class of regular behaviours. Journal of Computer and System Sciences, 28(3):439–466, 1984.

[Mil89] Robin Milner. A complete axiomatisation for observational congruence of finite state behaviours. Information and Computation, 81:227– 247, 1989.

[Mit90] John C. Mitchell. Type systems for programming languages. In The Handbook of Theoretical Computer Science, chapter 8. Elsevier Science, 1990.

[Mol89] Faron Moller. Axioms for Concurrency. PhD thesis, University of Edinburgh, 1989.

[MP43] Warren S. McCulloch and Walter Pitts. A logical calculus of the ideas immanent in nervous activity. Bulletin of Mathematical Biophysics, 5:115–133, 1943.

[MT92] K. Meinke and J. V. Tucker. Handbook of Logic in Computer Science, volume 1, chapter ‘Universal Algebra’, pages 189–411. Clarendon press, Oxford, 1992.

[Nie89] Flemming Nielson. The typed λ-calculus with first-class processes. In Proc. PARLE ’89, LNCS 366. Springer-Verlag, 1989.

[Par81] D. M. R. Park. Concurrency and automata on infinite sequences. In Proc. 5th G.I. Conference, LNCS 104. Springer-Verlag, 1981.

[PT87] R. Paige and R. Tarjan. Three partition refinement algorithms. SIAM Journal on Computing, 16(6):973–989, 1987.

[Rab93] Alexander Rabinovich. A complete axiomatisation for trace congruence of finite state behaviors. In Austin and Main, editors, Proceedings of Mathematical Foundations of Programming Semantics (IX), LNCS, 1993. (to appear).

[Red64] V. N. Redko. On defining relations for the algebra of regular events. Ukrain. Mat. Zh., 16:120–126, 1964. (in Russian).

[Sal66] Arto Salomaa. Two complete axiom systems for the algebra of regular events. Journal of the ACM, 13(1):158–169, January 1966.

[San93] Davide Sangiorgi. Expressing Mobility in Process Algebras: First-Order and Higher-Order Paradigms. PhD thesis, University of Edinburgh, 1993.

[San94] Davide Sangiorgi. Bisimulation in higher-order process calculi. In Proceedings of the IFIP Working Conference on Programming Concepts, Methods and Calculi (PROCOMET ’94), pages 207–224, 1994.

[Sew94] Peter Sewell. Bisimulation is not finitely (first-order) equationally axiomatisable. In Proc. 9th IEEE Symposium on Logic in Computer Science, pages 62–70. IEEE, 1994.

[Sta82] R. Statman. Completeness, invariance and λ-definability. The Journal of Symbolic Logic, 47(1):17–26, March 1982.

[Tur37] A. M. Turing. On computable numbers, with an application to the entscheidungsproblem. Proceedings of the London Mathematical Society (second series), 42:230–265, 1937.

[Vra86] J. L. M. Vrancken. The algebra of communicating processes with empty process. Technical Report FVI 86-01, University of Amsterdam, Department of Computer Science, 1986.

[Wal88] D. J. Walker. Bisimulations and divergence. In Proc. 3rd IEEE Symposium on Logic in Computer Science, pages 186–192, 1988.

[Yan] Yanov. See [Con71, p. 108].

Index of axioms

A1  E + (F + G) = (E + F) + G  22
A2  E + F = F + E  22
A3  E + 0 = E  22
A4  E + E = E  22
A5  μY E[Y/X] = μXE , if Y not free in μXE 23

B1  E[μXE /X] = μXE  23
B1′  μXE = E , if X not free in E.  26
B2  μXX + E = μXE  23
B3  μXE[μY F /Y] = μXE[μY F [μXE /X] /Y]  23

C_{mn}  \begin{aligned}& μ ⟨X_{i} = E_{i}[X_{k}/Z_{kf}]_{k∈m,f∈n^{n}} | i ∈ m⟩ \\ = & μ ⟨Y_{ij} = E_{i}[Y_{k,f(j)}/Z_{kf}]_{k∈m,f∈n^{n}} | i ∈ m, j ∈ n⟩ \end{aligned}  23

C1–13  ⋯  32
C14.p  A^{∗} = (A^{p})^{∗} . ∑_{i∈p} A^{i}  32

D  E = F [E/X] ∧ X guarded in F → E = μXF  29

E1 (double iteration) μZE[ZZ/XY] = μXμY E  28
E2 (composition)  μXE[F/X] = E[μXF [E/X] /X]  28
E3 (GA implication) \begin{aligned}& μZE[ZZ/XY] = μZF [ZZ/XY] \\ → & μZE[ZZ/XY] = μXF [μY E /Y] \end{aligned}  30

F 1  μ ⟨ \begin{matrix}X = E + aY \\ Y = F + τG \end{matrix} ⟩ = μ ⟨ \begin{matrix}X = E + aY + aG \\ Y = F + τG \end{matrix} ⟩  75

F 2  μ ⟨ \begin{matrix}X = E + τY \\ Y = F + G \end{matrix} ⟩ = μ ⟨ \begin{matrix}X = E + τY + G \\ Y = F + G \end{matrix} ⟩  75
F 3  aμXE = aμXE + τX.  75
F 4  E ∼ F → E = F  75

P 1  aE + aF = a(E + F)  22
P 2  a0 = 0  22

commutative identity for μ-expressions

\begin{aligned}& μ̃_{i′} ⟨X_{i} = E_{i}[X_{k}/Z_{kl}]_{k∈m,l∈n} | i ∈ m⟩ \\ = & μ̃_{i′j′} ⟨Y_{ij} = E_{i}[Y_{k,ρ_{ij}(l)}/Z_{kl}]_{k∈m,l∈n} | i ∈ m, j ∈ n⟩ \end{aligned}  27

commutative identity for ∗-expressions

B^{∗} . ρ = ρ . C^{∗}  33

functorial implication

\begin{aligned}& ∀i ∈ m . E_{i}[Y_{ρ(j)}/X_{j}]_{j∈m} = F_{ρ(i)} \\ → & ∀i ∈ m . μ̃_{i}X̃ Ẽ = μ̃_{ρ(i)}Ỹ F̃ \end{aligned}  30

group identity

[ 1 0 ⋯ 0 ] . M^{∗} . [ 1 ⋮ 1 ] = (∑_{g∈G} X_{g})^{∗}  34

Index

≡_{u}, 59

axiomatisation, 40 ω-complete, 19 complete, 42 pure equational, 15, 16 pure horn clause, 15, 17 sound, 40

bisimulation, 7 higher order ∼_{ho}, 47 loose higher order, 50 normal ∼_{Nr}, 68 of pointed graphs, 72 solution, 83 weak ≈, 8

chart, 6, 82 finite, 10 root-unwound, 76 saturated, 76

chart substitution, 82 commutative identity, 27, 33 composition identity (E2), 28

decoration, 71 der( ) or derivatives, 48 double iteration identity (E1), 28

equation sequence, 23 accessible, 25 almost standard, 101 fixed point of, 23 guarded, 30 product of, 25 provable solution, 29 standard, 25

expressions ∗-, 10

μ-, 8

extensional equality ∼_{ext}, 43

functorial implication, 30

GA implication (E3), 30

graph, 71

group identity, 34

higher order π calculus, 66

infinite term equivalence =_{infinite term},

9 iteration theories, 19

lambda calculus, 39, 41

language

of ∗-expressions, 12 language equivalence, 7 loops, 60 L_{u}, 59

n-lts, 98

order( ), 40

relative axiomatisability, 18, 21, 27, 73 substitution for ..., 42 substitutive, 10, 13, 42

T -unification problem, 89 T -unifier, 89 T_{k}^{σ}, 40 trace congruence, 7 transition system

E⋆ρ, 57

higher order, 46

of a standard sequence, 25 of the ∗-expressions, 11 of the μ-expressions, 9

unification problem, 81, 83 unifier, 81, 83

visibility predicate ▷, 6

W(R), 8 weak congruence ≈^{c}, 8 weak extensional equality ≈_{ext}^{c}, 74 weak higher order congruence ≈_{ho}^{c}, 73 width( ), 59