BRICS RS-96-22 Aceto & Fokkink: An Equational Axiomatization for Multi-Exit Iteration

BRICS

Basic Research in Computer Science

An Equational Axiomatization for Multi-Exit Iteration

Luca Aceto Wan J. Fokkink

BRICS Report Series RS-96-22 ISSN 0909-0878 June 1996 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1996, BRICS, Department of Computer Science

University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent publications in the BRICS Report Series. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK - 8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@brics.dk

BRICS publications are in general accessible through WWW and anonymous FTP:

http://www.brics.dk/
ftp ftp.brics.dk (cd pub/BRICS)

An Equational Axiomatization for Multi-Exit Iteration

Luca Aceto^{∗} BRICS^{†} Department of Computer Science Aalborg University, Fr. Bajersvej 7E 9220 Aalborg Ø, Denmark

Wan Fokkink^{‡} Utrecht University, Department of Philosophy Heidelberglaan 8, 3584 CS Utrecht The Netherlands

Abstract

This paper presents an equational axiomatization of bisimulation equivalence over the language of Basic Process Algebra (BPA) with multi-exit iteration. Multiexit iteration is a generalization of the standard binary Kleene star operation that allows for the specification of agents that, up to bisimulation equivalence, are solutions of systems of recursion equations of the form

X_{1} = P_{1}X_{2} + Q_{1}
⋮
X_{n} = P_{n}X_{1} + Q_{n}

where n is a positive integer, and the P_{i} and the Q_{i} are process terms. The addition of multi-exit iteration to BPA yields a more expressive language than that obtained by augmenting BPA with the standard binary Kleene star (BPA^{∗}). As a consequence, the proof of completeness of the proposed equational axiomatization for this language, although standard in its general structure, is much more involved than that for BPA^{∗}. An expressiveness hierarchy for the family of k-exit iteration operators proposed by Bergstra, Bethke and Ponse is also offered.

AMS Subject Classification (1991): 08A70, 03C05, 68Q10, 68Q40, 68Q55, 68Q68, 68Q70. CR Subject Classification (1991): D.3.1, F.1.2, F.3.2. Keywords and Phrases: Concurrency, process algebra, Basic Process Algebra (BPA), multi-exit iteration, bisimulation, equational logic, complete axiomatizations.

∗On leave from the School of Cognitive and Computing Sciences, University of Sussex, Brighton BN1 9QH, UK. Partially supported by the Human Capital and Mobility cooperation project Express.

Email: luca@iesd.auc.dk.

†Basic Research in Computer Science, Centre of the Danish National Research Foundation.

‡Email: fokkink@phil.ruu.nl.

1 Introduction

One of the classic topics in the theory of computation is the study of axiomatic characterizations of equalities between variations on regular expressions. This field of research has been active since Kleene’s original paper [27], where regular expressions were first introduced, and has yielded a collection of very deep and beautiful mathematical results. (The interested reader is invited to consult, e.g., [38, 14, 35, 29, 28] for an overview of the results that have been obtained within this line of research.) According to the point of view of formal language theory, a regular expression denotes a regular language, and two regular expressions are equal exactly when they denote the same language. This notion of semantics for regular expressions is the natural one to choose when the finite automaton associated with a regular event by Kleene’s synthesis theorem (cf., e.g., [27, 38]) is viewed as accepting a language. However, as first observed by Milner [30], defining the semantics of an automaton as the language it accepts is inappropriate when one views it as a reactive system, i.e., as a system that computes by reacting to stimuli from its environment. For this reason, a wealth of notions of equivalence over processes that, to different degrees, capture their behaviour as reactive machines have been proposed in the literature on process theory. (The interested reader is invited to consult the references [22, 24] for more details.) Amongst these, the notion of bisimulation equivalence [34] has emerged as a fundamental semantic equivalence for reactive systems, and the development of its theory has by now reached a level of maturity that is comparable to that of the standard notions from the theory of formal languages. For example, the complete axiomatization of bisimulation equivalence for the regular fragment of CCS [32], provided by Milner in his classic paper [31], parallels those obtained by Salomaa for regular languages [37, 38], and have contributed to the realization that the notion of process is at least as elegant and mathematically tractable as that of language.

Despite these successes, process theory has traditionally lacked a systematic investigation of (equational) axiomatizations of process equivalences over regular expressions—a notable exception being Milner’s seminal paper [31], where an implicational proof system was proposed for bisimulation equivalence over regular events, and the problem of its completeness raised. (To the best of the authors’ knowledge, this problem of Milner’s is still awaiting a solution.)

The study of axiomatic questions for variations on the language of regular expressions from the perspective of process theory has received new impulse after the publication of [9]. In op. cit. the authors have investigated the expressive power of variations on standard process description languages in which infinite behaviours are defined by means of Kleene’s star operation [27, 15] rather than by means of systems of recursion equations, and have proposed an axiom system for bisimulation equivalence over the language of Basic Process Algebra [10] with the original binary version of the Kleene star operation (BPA^{∗}). The completeness of the axiom system proposed ibidem was proven by Fokkink and Zantema in [20, 17], and this result has been followed by a series of contributions in which several notions of process equivalence have been equationally axiomatized over languages incorporating variations on the Kleene star operation—see, e.g., [16, 3, 2, 1, 21, 18].

Interestingly, as already noted by Milner in [31, Sect. 6], not every process defined using finite-state systems of recursion equations can be described, up to bisimulation equivalence, using only regular expressions. (As shown in [9], any regular process can be specified in the axiom system ACP_{τ} [11] with Kleene star using handshake communication.) The limited expressive power of the Kleene star operation in denoting finite automata modulo bisimulation equivalence is highlighted in [8], where it is shown that the process described by the following recursion equation

(1)  X =^{def} a · (a · X + b) + a

cannot be expressed in the language BPA^{∗} modulo bisimulation equivalence. (Of course, a simple use of Arden’s lemma yields that the language denoted by X is the same associated with the regular expression (a · a)^{∗}(a · b + a). However, the process denoted by X above is not bisimulation equivalent to that associated with the BPA^{∗} term (a · a)^{∗}(a · b + a).)

In order to increase the expressive power of super-languages of BPA incorporating Kleene star-like operations, the use of k-exit iteration has been proposed in [8]. For every positive integer k, and process terms P_{i} and Q_{i} (1 ≤ i ≤ k), the process term (P_{1}, …, P_{k})^{∗}(Q_{1}, …, Q_{k}) denotes a solution to the following list of recursion equations:

X_{1} = P_{1}X_{2} + Q_{1}
⋮
X_{k} = P_{k}X_{1} + Q_{k}

For example, the term (a, a)^{∗}(a, b) uses 2-exit iteration, and the reader will immediately realize that, up to isomorphism, it denotes the finite automaton associated with the variable X in (1).

The aim of this paper is to present an equational axiomatization of bisimulation equivalence over the language obtained by augmenting Basic Process Algebra with the family of k-exit iteration operations. In fact, we shall consider a slight syntactic generalization of the family of k-exit iteration operations, in that we permit the construction of terms of the form (P_{1}, …, P_{m})^{∗}(Q_{1}, …, Q_{n}), with m and n two arbitrary positive integers. The result is a purely algebraic process language that is more expressive than BPA^{∗}.

Apart from the standard laws from the equational theory for BPA, and the adaptations of the three axioms for the binary Kleene star [20] to multi-exit iteration, the equational axiomatization that we propose contains the following axiom schemas for multi-exit iteration:

\begin{aligned}MEI4 & (x_{0}, x_{1}, v⃗)^{∗}(y, x_{2}(v⃗, x_{0}(x_{1} + x_{2}))^{∗}(w⃗, y), w⃗) & = & (x_{0}(x_{1} + x_{2}), v⃗)^{∗}(y, w⃗) \\ MEI5 & ((x, v⃗)^{m})^{∗}((y, w⃗)^{n}) & = & (x, v⃗)^{∗}(y, w⃗) \end{aligned}

where we use v⃗ and w⃗ to stand for arbitrary vectors of process variables, and n, m are positive integers. Typically, these two axioms deal with equalities between terms that have distinct exit degrees.

Our proof of the completeness of this axiom system with respect to bisimulation equivalence over BPA with multi-exit iteration uses an adaptation of a proof technique developed by the second author in [17]. The actual details of the completeness proof are, however, more delicate and intricate than those of the proof given ibidem. In particular, as the reader will realize, extra care need be taken in dealing with equalities whose equational deduction makes an essential use of the new laws MEI4–5.

As remarked above, Bergstra, Bethke and Ponse [8, 9] have shown that the process described by the recursion equation (1) cannot be specified in the language BPA^{∗} modulo bisimulation equivalence. In this paper, we generalize this result by showing that, in presence of a countably infinite set of actions, the family of k-exit iteration operations from [8] induces a strict expressiveness hierarchy of super-languages of BPA. More precisely, we prove that, for every positive integer k, the agent that corresponds to the solution of the following system of recursion equations (with X_{1} as the leading variable)

X_{1} = a_{1}X_{2} + a_{1}
⋮
X_{k+1} = a_{1}X_{1} + a_{k+1}

can only be specified, modulo bisimulation equivalence, with the use of multi-exit iterations of the form (P_{1}, …, P_{m})^{∗}(Q_{1}, …, Q_{n}) with n greater than k.

We conclude this introduction with a brief overview of the contents of this paper. We begin by introducing the language of Basic Process Algebra with multi-exit iteration and its operational semantics (Sects. 2.1–2.3). The equational axiomatization of bisimulation equivalence over Basic Process Algebra with multi-exit iteration is presented in Sect. 2.4. The whole of Sect. 3 is devoted to a detailed proof of the completeness of the proposed axiomatization. The proof we present consists of three steps. First we isolate a collection of basic process terms, which cover, up to bisimulation equivalence, the whole language of process terms, and whose structure will simplify the proof of the promised completeness theorem (Sect. 3.1). We then proceed to define a well-founded ordering over basic terms which will allow for an inductive proof of our main result, and study some of its properties (Sect. 3.2). Finally, we shall show that two bisimilar basic terms can be proven equal using the equations in the proposed axiom system (Sect. 3.4). The paper concludes with an expressiveness hierarchy for the family of k-exit iteration operations (Sect. 4).

2 BPA with Multi-Exit Iteration

We begin by presenting the language of Basic Process Algebra with multi-exit iteration and its semantics.

2.1 The Syntax

We assume a non-empty alphabet A of atomic actions, with typical elements a, b, and a countably infinite set Var of process variables, disjoint from A, with typical elements x, y, z. We shall use α, β to range over A ∪ Var.

The language (BPA^{me∗}(A)) of terms over Basic Process Algebra (BPA) with multiexit iteration is defined inductively as follows:

- each α ∈ A ∪ Var is a term;

- if P and Q are terms, then P + Q is a term;

- if P and Q are terms, then P · Q is a term;

- if P_{1}, ..., P_{m} and Q_{1}, ..., Q_{n} (m, n ≥ 1) are terms, then (P_{1}, ..., P_{m})^{∗}(Q_{1}, ..., Q_{n}) is a term.

The set of closed terms, i.e., terms that do not contain occurrences of process variables, is denoted by T(BPA^{me∗}(A)). We shall use P, Q, …, Y to range over (BPA^{me∗}(A)). In writing terms over the above syntax, we shall always assume that the operation · binds stronger than +. In the sequel the operation · will often be omitted, so P Q denotes P · Q. We shall use the symbol ≡ to stand for syntactic equality of terms. The size of a process term is the number of operations occurring in it. A (closed) substitution is a mapping from process variables to (closed) terms in the language (BPA^{me∗}(A)). For every term P and (closed) substitution σ, the (closed) term obtained by replacing every occurrence of a variable x in P with the (closed) term σ(x) will be written P σ.

Intuitively, closed terms stand for agents whose behaviour is completely specified, whereas terms containing occurrences of process variables denote agents with partially specified behaviour. For example, an atomic action a stands for a process that can only perform itself in one computational step and terminate in doing so; on the other hand, the term a + x denotes a partially specified process, whose behaviour depends in part on that of the process term that is substituted for the variable x.

Apart from actions and variables, the signature of the language (BPA^{me∗}(A)) includes the binary operations of alternative composition + and sequential composition · familiar from the theory of Basic Process Algebra [10, 7], and a variation on the original binary version of the Kleene star operation [27], that will be referred to as multi-exit iteration. For positive integers m and n, the process term (P_{1}, ..., P_{m})^{∗}(Q_{1}, ..., Q_{n}) stands for an agent whose behaviour is specified by the following defining equation:

(P_{1}, ..., P_{m})^{∗}(Q_{1}, ..., Q_{n}) = P_{1} · (P_{2}, ..., P_{m}, P_{1})^{∗}(Q_{2}, ..., Q_{n}, Q_{1}) + Q_{1} .

Multi-exit iteration is a mild syntactic generalization of the family of k-exit iteration operations introduced in [8]—the only difference being that in op. cit. the number of the P_{i} must always be equal to that of the Q_{j}. As we shall see, multi-exit iteration and the family of k-exit iteration operations have the same expressive power modulo bisimulation equivalence. (Cf. Sect. 4 for some remarks on the expressive power of the k-exit iteration operations.)

In order to simplify notation in the presentation of the operational semantics and of the axiomatization for (BPA^{me∗}(A)), we shall use the notion of ‘vectors of processes’. A vector of processes is a tuple (P_{1}, ..., P_{m}), where m ≥ 0. We shall use P⃗ , Q⃗, R⃗, S⃗ to denote such vectors of processes. In multi-exit iteration, the expressions at the left- and right-hand side of the star are non-empty vectors of processes.

In the sequel, (Q, P⃗) represents the vector that is obtained by concatenating the process term Q in front of vector P⃗, and (P⃗ , Q) represents the vector that is obtained by appending the process term Q at the rear of vector P⃗. Furthermore, we assume the following features for vectors:

- Multiplication with a process term: (P_{1}, ..., P_{m}) · Q equals (P_{1}Q, ..., P_{m}Q).

- Power of a vector: for a positive integer n, (P_{1}, ..., P_{m})^{n} equals

(\underbrace{P_{1}, ..., P_{m}, …, P_{1}, ..., P_{m}}_{n times})

Enclosing parentheses will always be omitted from vectors of length one, i.e., (P) will be written P.

2.2 Operational Semantics

The operational semantics for the language (BPA^{me∗}(A)) is given by the labelled transition system [26, 36]

( (BPA^{me∗}(A)), {→^{α}| α ∈ A ∪ Var}, {→^{α}✓ | α ∈ A ∪ Var})

where the transition relations →^{α} and the unary predicates →^{α}✓ are, respectively, the least subsets of (BPA^{me∗}(A)) × (BPA^{me∗}(A)) and (BPA^{me∗}(A)) satisfying the rules in Table 1. Intuitively, a transition P →^{a} Q means that the system represented by the term P can perform the action a, thereby evolving into Q, whereas P →^{x} P′ means that the initial behaviour of P may depend on the term that is substituted for the process variable x. The special symbol ✓ stands for (successful) termination; therefore the interpretation of the statement P →^{α}✓ is that the process term P can terminate by performing α, if α is an atomic action, or by executing to completion the term that is substituted for the process variable x, if α = x.

\overline{α →^{α}✓}

\frac{P →^{α}✓}{P + Q →^{α}✓}  \frac{Q →^{α}✓}{P + Q →^{α}✓}  \frac{P →^{α} P′}{P + Q →^{α} P′}  \frac{Q →^{α} Q′}{P + Q →^{α} Q′}

\frac{P →^{α}✓}{P · Q →^{α} Q}  \frac{P →^{α} P′}{P · Q →^{α} P′ · Q}

\frac{P →^{α}✓}{(P, Q⃗)^{∗}(R, S⃗) →^{α} (Q⃗, P)^{∗}(S⃗, R)}  \frac{P →^{α} P′}{(P, Q⃗)^{∗}(R, S⃗) →^{α} P′ · (Q⃗, P)^{∗}(S⃗, R)}

\frac{R →^{α}✓}{(P, Q⃗)^{∗}(R, S⃗) →^{α}✓}  \frac{R →^{α} R′}{(P, Q⃗)^{∗}(R, S⃗) →^{α} R′}

Table 1: Transition Rules

Definition 2.1 The term P′ is a derivative of P if P can evolve into P′ by zero or more transitions. A derivative P′ of P is proper if P can evolve into P′ by performing at least one transition.

The following basic fact can be easily shown by structural induction on terms:

Fact 2.2 For every P ∈ (BPA^{me∗}(A)), the set of derivatives of P is finite.

Process terms are considered modulo bisimulation equivalence from Park [34]. Intuitively, two process terms are bisimilar if they have the same branching structure.

Definition 2.3 Two process terms P and Q are bisimilar, denoted by P \underline{↔} Q, if there exists a symmetric binary relation B on process terms which relates P and Q, such that:

- if R B S and R →^{α} R′, then there is a transition S →^{α} S′ such that R′ B S′,
- if R B S and R →^{α}✓, then S →^{α}✓.

Such a relation B will be called a bisimulation (witnessing the equivalence P \underline{↔} Q). The relation \underline{↔} will be referred to as bisimulation equivalence.

Note that if P is bisimilar to Q, then every (proper) derivative of P is bisimilar to some (proper) derivative of Q, and vice versa.

The transition rules in Table 1 are in the ‘path’ format of Baeten and Verhoef [6]. Hence, bisimulation equivalence is a congruence with respect to all the operations in the signature of (BPA^{me∗}(A)). The interested reader is invited to consult [6] for the definition of the path format for operational rules, and for a proof of the aforementioned congruence result.

Remark: The proof of the congruence theorem for the path format presented in op. cit. uses the extra assumption that the rules are well-founded. Fokkink and van Glabbeek [19] have shown that this requirement, which is, however, met by the rules in Table 1, can be dropped.

The reader might have noticed that we have defined notions of operational semantics and bisimulation equivalence that apply to open terms directly, following [33, 23] for process algebra with abstraction, and [1] for process algebra with the prefix iteration operation from [16], which is a restricted version of the Kleene star. This approach deviates from the standard practice in process theory, which prescribes to define operational semantics and bisimulation equivalence for closed terms only, and to give meaning to open terms thus:

P \underline{↔} Q =^{Δ} P σ \underline{↔} Qσ for all closed substitutions σ : Var → T(BPA^{me∗}(A)).

(Note that this amounts to stipulating that two open terms are equivalent exactly when the equation P = Q holds in the algebra of closed terms modulo bisimulation equivalence.) The following result shows that both approaches yield the same notion of bisimulation equivalence over (BPA^{me∗}(A)), that is, in our setting, two open terms are bisimilar if and only if all their closed instantiations are.

Lemma 2.4 For every P, Q ∈ (BPA^{me∗}(A)),

P \underline{↔} Q ⇔ P σ \underline{↔} Qσ for all closed substitutions σ : Var → T(BPA^{me∗}(A)).

Proof: The result can be proven following the strategy that was employed in [1] for prefix iteration. We remark, however, that the technical details are considerably more complicated in the case of multi-exit iteration. In particular, in the proof of the ‘if implication’, the choice of a canonical closed substitution σ_{(P,Q)} with the property that

P σ_{(P,Q)} \underline{↔} Qσ_{(P,Q)} ⇒ P \underline{↔} Q

requires more care than in the aforementioned reference. The interested reader is invited to consult [39, Theorems 3 and 4], where this type of result is proven in the more general setting of a simply typed lambda calculus, which captures multi-exit iteration. □

Lemma 2.4 implies that any complete axiomatization of bisimulation equivalence over the language (BPA^{me∗}(A)) is also a complete axiomatization of the algebra of closed terms modulo bisimulation. Such an axiomatization will, a fortiori, be ω-complete in the sense of, e.g., [25].

2.3 Norm and L-value of Process Terms

Process terms in (BPA^{me∗}(A)) are normed, which means that they are able to terminate by embarking in a finite sequence of transitions. We call such a sequence a termination trace. The norm of a process term P, denoted by |P |, is the length of its shortest termination trace; this notion stems from [4]. Note that bisimilar process terms have the same norm. The following lemma, which is due to Caucal [13], is typical for normed processes. The interested reader is referred to [17] for its proof.

Lemma 2.5 Let P, Q, R, S ∈ (BPA^{me∗}(A)) be such that P Q \underline{↔} RS. Then the following statements hold:

- If |Q| = |S|, then P \underline{↔} R and Q \underline{↔} S.

- If |Q| < |S|, then there is a proper derivative P′ of P such that P \underline{↔} RP′ and

P′Q \underline{↔} S.

The notion of norm may be used as a measure of the complexity of terms which is useful in inductive proofs. (Cf., e.g., the proof of the above lemma in [17].) However, this measure of term complexity does not lend itself to use in completeness proofs like the one presented in op. cit. because it does not respect term size. For example, the term aa + a has smaller norm than its sub-term aa. For this reason, Fokkink and Zantema [20] introduced the notion of L-value, which does not have this drawback.

Definition 2.6 The L-value of a process term P, notation L(P), is defined thus:

L(P) =^{Δ} sup{|P′| | P′ a proper derivative of P } .

Note that, as the set of derivatives of P is finite for every term P ∈ (BPA^{me∗}(A)) (Fact 2.2), the L-value of a process term is a well-defined natural number. For example, L(α) = sup ∅ = 0.

The following basic properties of the notion of L-value will be useful in the technical developments to follow.

Lemma 2.7

1. If P \underline{↔} Q, then L(P) = L(Q);

2. L(P) < L(P Q);

3. L(P_{i}) < L((P_{1}, ..., P_{m})^{∗}(Q_{1}, ..., Q_{n})) for i = 1, ..., m.

Remark: Note that, in general, the L-values of Q and Q_{i} are not smaller than those of P Q and (P_{1}, ..., P_{m})^{∗}(Q_{1}, ..., Q_{n}), respectively. For instance, if P ≡ a and Q ≡ a + aa, then L(P Q) = L(Q) = 1. The reader will find the construction of a similar example for multi-exit iteration an easy exercise.

2.4 The Axiom System

Table 2 contains our axiom system E for (BPA^{me∗}(A)) modulo bisimulation equivalence. It consists of the standard axioms A1–5 from Basic Process Algebra (cf. [10, 7]) together with five axiom schemas MEI1–5 for multi-exit iteration. In these axiom schemas, v⃗ and w⃗ denote meta-variables which range over vectors of processes, and n, m range over the set of positive integers.

Remark: For the sake of clarity, we remark that a meta-variable v⃗ is just syntactic sugar for an arbitrary vector of process variables. Therefore each of the axiom schemas MEI1–5 stands for an infinite family of equations, viz. one for each instantion of the meta-variables ranging over vectors of process variables and of those ranging over positive integers.

Laws MEI1–3 are modifications of the standard axioms for the binary Kleene star which, together with A1–5, have been shown to be complete for bisimulation equivalence over the language BPA^{∗} in [20, 17]. In particular, axiom MEI3 is the multi-exit version of a law which originates from Troeger’s work [40]. Axioms MEI4 and MEI5 are, to the best of our knowledge, new.

Proposition 2.8 (Soundness) If E ⊢ P = Q, then P \underline{↔} Q.

Proof: Since bisimulation equivalence is a congruence, this can be verified by checking soundness for each axiom separately, which is left to the reader. □

Remark: The fact that multi-exit iteration and the family of k-exit iteration operations (k ≥ 1), as defined in [8], have the same expressive power modulo bisimulation equivalence is witnessed by the soundness of axiom MEI5. This axiom may be used to turn every instance of a multi-exit iteration into an equivalent one that uses k-exit iteration for an appropriate k.

In the proof of the completeness of the axiom system E for bisimulation equivalence over the language (BPA^{me∗}(A)), we shall find it useful to have more general variants of the axioms MEI3,4.

Let us assume that v⃗_{0} and w⃗_{0} are vectors of process variables of the same length. The following equation, which we shall refer to as MEI3′, can be derived easily from MEI3 using MEI1:

(v⃗_{0}, x_{1}, v⃗_{1})^{∗}(w⃗_{0}, y + x_{2}(v⃗_{1}, v⃗_{0}, x_{1} + x_{2})^{∗}(w⃗_{1}, w⃗_{0}, y), w⃗_{1}) = (v⃗_{0}, x_{1} + x_{2}, v⃗_{1})^{∗}(w⃗_{0}, y, w⃗_{1}) .

A1  x + y = y + x
A2  (x + y) + z = x + (y + z)
A3  x + x = x
A4  (x + y)z = xz + yz
A5  (xy)z = x(yz)
MEI1  x(v⃗, x)^{∗}(w⃗, y) + y = (x, v⃗)^{∗}(y, w⃗)
MEI2  (x, v⃗)^{∗}(y, w⃗)z = (x, v⃗)^{∗}(yz, w⃗z)
MEI3  (x_{1}, v⃗)^{∗}(y + x_{2}(v⃗, x_{1} + x_{2})^{∗}(w⃗, y), w⃗) = (x_{1} + x_{2}, v⃗)^{∗}(y, w⃗)
MEI4 (x_{0}, x_{1}, v⃗)^{∗}(y, x_{2}(v⃗, x_{0}(x_{1} + x_{2}))^{∗}(w⃗, y), w⃗) = (x_{0}(x_{1} + x_{2}), v⃗)^{∗}(y, w⃗)
MEI5  ((x, v⃗)^{m})^{∗}((y, w⃗)^{n}) = (x, v⃗)^{∗}(y, w⃗)

Table 2: The Axiom System E

Similarly, the following equation, which we shall refer to as MEI4′, can be derived easily from MEI4 using MEI1:

\begin{matrix}(v⃗_{0}, x_{0}, x_{1}, v⃗_{1})^{∗}(w⃗_{0}, y, x_{2}(v⃗_{1}, v⃗_{0}, x_{0}(x_{1} + x_{2}))^{∗}(w⃗_{1}, w⃗_{0}, y), w⃗_{1}) = \\ (v⃗_{0}, x_{0}(x_{1} + x_{2}), v⃗_{1})^{∗}(w⃗_{0}, y, w⃗_{1}) . \end{matrix}

Note that the soundness of these generalized versions of equations MEI3–4 depends crucially on the assumption that v⃗_{0} and w⃗_{0} are vectors of process variables of the same length, and their use in the proof of the completeness theorem will be restricted to situations in which this requirement is met.

Notation 2.9 For an axiom system T , we write T ⊢ P = Q iff the equation P = Q is provable from the axioms in T using the rules of equational logic. For a collection of equations X over the signature of (BPA^{me∗}(A)), we write P =^{X} Q as a short-hand for A1,A2,X ⊢ P = Q.

For I = {i_{1}, …, i_{n}} a finite, non-empty index set, we write ∑_{i∈I} P_{i} for P_{i_{1}} +⋯+P_{i_{n}}. For notational convenience, and in order to reduce the number of cases in the com-

pleteness proof, in what follows we shall identify a term P with the meta-notations ∑_{i∈∅} Q_{i} + P and (∑_{i∈∅} Q_{i})Q + P.

The collection of possible transitions of each process term P is non-empty and finite,

say {P →^{α_{i}} P_{i} | i = 1, ..., m} ∪ {P →^{β_{j}}✓ | j = 1, ..., n}. We call the term

∑_{i=1}^{m} α_{i}P_{i} + ∑_{j=1}^{n} β_{j}

the expansion of P. The terms α_{i}P_{i} and β_{j} will be referred to as the summands of P.

Lemma 2.10 Each process term is provably equal to its expansion.

Proof: Straightforward, by structural induction on terms, using axioms A4, A5 and MEI1. □

3 The Completeness Proof

The remainder of the paper is devoted to a proof of completeness of the axiom system E with respect to bisimulation equivalence over the language (BPA^{me∗}(A)). The proof of this result will be given by adapting a proof technique developed by the second author in [17]. A comparison between this proof technique and the one originally used in [20] to solve the completeness problem for bisimulation equivalence over Basic Process Algebra with binary Kleene star may be found in [17].

The proof we present consists of three steps. First we isolate a collection of basic process terms, which cover, up to bisimulation equivalence, the whole language of process terms, and whose structure will simplify the proof of the promised completeness theorem. We then proceed to define a well-founded ordering over basic terms which will allow for an inductive proof of our main result, and study some of its properties. Finally, we shall show that two bisimilar basic terms can be proven equal using the equations in E. This proof strategy will be familiar to readers acquainted with the literature on completeness results from process theory. The actual details of the proof that we now proceed to present are, however, rather challenging and novel.

3.1 Basic Terms

As a first stepping stone towards our main result, we now aim at constructing a collection of basic process terms, with the property that each process term is provably equal to a basic one. We shall then prove the completeness theorem by showing that bisimilar basic terms are provably equal.

Let 𝔾 denote the collection of process terms in (BPA^{me∗}(A)) which only use action prefixing, in the sense of Milner [32], in lieu of general sequential composition, and in which vectors at the left- and right-hand side of multi-exit iteration have the same length. That is, 𝔾 is defined inductively as follows:

- each α ∈ A ∪ Var is in 𝔾;

- if P and Q are in 𝔾, then P + Q is in 𝔾;

- if α ∈ A ∪ Var and P is in 𝔾, then αP is in 𝔾;

- if P_{1}, ..., P_{n} and Q_{1}, ..., Q_{n} (n ≥ 1) are in 𝔾, then (P_{1}, ..., P_{n})^{∗}(Q_{1}, ..., Q_{n}) is in 𝔾.

Lemma 3.1 Every process term can be proven equal to a term in 𝔾 using axioms A4,5 and MEI2,5.

The import of the above lemma is that, without loss of generality, we may restrict ourselves to considering terms in 𝔾. However, 𝔾 is not yet our desired set of basic terms. In fact, one of the most fundamental properties that we require of a collection of basic terms for use in the proof of the completeness theorem is that it be closed under transitions. This is a property that 𝔾 does not enjoy. For example, the term (a^{∗}a)^{∗}a is clearly in 𝔾, and

(a^{∗}a)^{∗}a →^{a} (a^{∗}a)((a^{∗}a)^{∗}a) .

However, the right-hand side of the above transition is a term that is not contained in 𝔾. In order to overcome this complication, we introduce the following collection ℍ of process terms:

- if a term (P_{1}, ..., P_{n})^{∗}(Q_{1}, ..., Q_{n}) is in 𝔾, then it is also in ℍ;

- if a term (P_{1}, ..., P_{n})^{∗}(Q_{1}, ..., Q_{n}) is in 𝔾, and if P′ is a proper derivative of P_{n},

then P′(P_{1}, ..., P_{n})^{∗}(Q_{1}, ..., Q_{n}) is in ℍ.

For example, the term (a^{∗}a)((a^{∗}a)^{∗}a) is included in ℍ because a^{∗}a is a proper derivative of itself.

The set 𝔹 of basic terms is the union of 𝔾 and ℍ.

Lemma 3.2 If P ∈ 𝔹 and P →^{α} P′, then P′ ∈ 𝔹.

Proof: Let P →^{α} P′. If P ∈ ℍ\𝔾, then it is easy to see that P′ ∈ ℍ. If P ∈ 𝔾, then a straightforward structural induction yields that P′ ∈ 𝔹. □

For later use, we now define an equivalence relation ≅ on ℍ as the least one satisfying axiom MEI5 and the equivalences

- (P_{1}, ..., P_{n})^{∗}(Q_{1}, ..., Q_{n}) ≅ (P_{2}, ..., P_{n}, P_{1})^{∗}(Q_{2}, ..., Q_{n}, Q_{1});

- (P_{n}, P_{1}, ..., P_{n−1})^{∗}(Q_{n}, Q_{1}, ..., Q_{n−1}) ≅ P′(P_{1}, ..., P_{n})^{∗}(Q_{1}, ..., Q_{n}) if P′ is a proper derivative of P_{n}.

The key properties of the relation ≅ needed in the technical developments to follow will be studied in the following section.

3.2 An Ordering on Terms

Having identified a set of basic terms closed under transitions, we now proceed to define a well-founded ordering on this set that will allow us to give an inductive proof of the main result of this paper.

Definition 3.3 We say that a term P is an exit derivative of a term Q iff P is a derivative of Q, but not vice versa.

Let ≺ denote the least transitive relation over the set of process terms satisfying:

- P ≺ Q if L(P) < L(Q),

- P ≺ Q if P is an exit derivative of Q.

Intuitively, if P ≺ Q, then either the set of derivatives of P is properly included in that of Q, or the L-value of P is strictly smaller than that of Q.

Lemma 3.4 ≺ is a well-founded ordering on (BPA^{me∗}(A)).

Proof: First of all, observe that if P ≺ Q then L(P) ≤ L(Q). This follows because if P is a derivative of Q, then L(P) ≤ L(Q) since all proper derivatives of P are also proper derivatives of Q.

Suppose now, towards a contradiction, that ≺ is not well-founded. This means that there exists an infinite descending chain P_{0} ≻ P_{1} ≻ P_{2} ≻ · · ·. As L(P_{n}) ≥ L(P_{n+1}) for all n, there is an N such that L(P_{N}) = L(P_{n}) for all n > N. Since P_{m} ≻ P_{n} for m, n > N with m < n, it follows that P_{n} is an exit derivative of P_{m} for each such m, n. By Fact 2.2, each process term has only finitely many derivatives, so there are m, n > N with m < n and P_{m} ≡ P_{n}. Then P_{m} ⊁ P_{n}, and we have found a contradiction. Hence, ≺ is well-founded. □

Following [17], we now proceed to study the interaction between the operational semantics of process terms and the above-defined ordering. A technical tool we shall use below is a weight function g that associates a natural number to each process term. This is defined thus:

g(α) =^{Δ} 0
g(P + Q) =^{Δ} max{g(P), g(Q)} + 1
g(P Q) =^{Δ} max{g(P), g(Q)}
g((P_{1}, ..., P_{m})^{∗}(Q_{1}, ..., Q_{n})) =^{Δ} max{g(P_{1}), ..., g(P_{m}), g(Q_{1}) + 1, ..., g(Q_{n}) + 1} .

The basic property of this weight function that we shall need is expressed in the lemma below, which follows by a straightforward structural induction.

Lemma 3.5 If P′ is a derivative of P, then g(P′) ≤ g(P). Moreover, if

- P ≡ P_{1} + P_{2} for some terms P_{1} and P_{2}, and P′ is a proper derivative of P, or

- P ≡ (P_{1}, ..., P_{m})^{∗}(Q_{1}, ..., Q_{n}), for some terms P_{i} (1 ≤ i ≤ m) and Q_{j} (1 ≤ j ≤ n), and P′ is a proper derivative of some Q_{j},

then g(P′) < g(P).

The following two lemmas will play a major rôle in the proof of the main result of this paper. The first states that, intuitively, escaping from a loop reduces the complexity of a process term, as measured by the above defined ordering. This is due to the fact that once a process term has exited a loop, it can never return to it.

Lemma 3.6 If Q′ is a proper derivative of Q_{i} for some i = 1, ..., n, then

Q′ ≺ (P_{1}, ..., P_{m})^{∗}(Q_{1}, ..., Q_{n}) .

Proof: If Q′ is a proper derivative of some Q_{i}, then Lem. 3.5 gives that

g(Q′) < g((P_{1}, ..., P_{m})^{∗}(Q_{1}, ..., Q_{n})) .

Again using Lem. 3.5, we infer from this inequality that (P_{1}, ..., P_{m})^{∗}(Q_{1}, ..., Q_{n}) is not a derivative of Q′. Since Q′ is a derivative of (P_{1}, ..., P_{m})^{∗}(Q_{1}, ..., Q_{n}), it follows that Q′ ≺ (P_{1}, ..., P_{m})^{∗}(Q_{1}, ..., Q_{n}). □

As witnessed by the proof of the above lemma, the exit derivatives of a term of the form (P_{1}, ..., P_{m})^{∗}(Q_{1}, ..., Q_{n}) are exactly the proper derivatives of the terms Q_{i}. As an immediate consequence of this observation, we note that:

Fact 3.7 If P, Q ∈ ℍ and P ≅ Q, then P and Q have the same L-value and exit derivatives.

The observations collected in the above result imply that ≅-equivalent basic terms dominate the same process terms with respect to the ordering ≺, i.e., that if P ≺ R ≅ S, then P ≺ S.

The following lemma is part of the crux of the proof of the completeness theorem; intuitively, it states that the only transitions between basic terms that do not decrease the complexity of terms, as measured by ≺, are those belonging to some loop.

Lemma 3.8 If P ∈ 𝔹 and P →^{α} P′, then either P′ ≺ P, or P, P′ ∈ ℍ and P ≅ P′.

Proof: We begin by establishing two facts that we shall use in the proof of the statement of the lemma.

A. If P ∈ 𝔹, P′ ∉ ℍ and P →^{α} P′, then P′ has smaller size than P. Proof. First of all, note that the claim is vacuously true if P ∈ ℍ\𝔾, because, in that case, it follows that P′ ∈ ℍ. That the claim holds for P ∈ 𝔾 can be shown by a simple structural induction on P.

B. If P ∈ ℍ and P →^{α} P′, then either g(P) > g(P′), or P′ ∈ ℍ and P ≅ P′. Proof. Since P ∈ ℍ, it follows that, for some terms P_{i} and Q_{i} (1 ≤ i ≤ n),

- either P ≡ (P_{1}, ..., P_{n})^{∗}(Q_{1}, ..., Q_{n}),

- or P ≡ P′_{n}(P_{1}, ..., P_{n})^{∗}(Q_{1}, ..., Q_{n}), for some proper derivative P′_{n} of P_{n}.

Hence, P′ can have one of the following three forms:

1. P′ ≡ (P_{2}, ..., P_{n}, P_{1})^{∗}(Q_{2}, ..., Q_{n}, Q_{1}),

2. P′ ≡ P′′_{n}(P_{1}, ..., P_{n})^{∗}(Q_{1}, ..., Q_{n}), for some proper derivative P′′_{n} of P_{n}, or

3. P′ ≡ Q′_{1}, for some proper derivative of Q_{1}.

In the first two cases P′ ∈ ℍ and P ≅ P′, and in the last case g(P′) = g(Q′_{1}) < g(P) (Lem. 3.5).

We are now in a position to prove the lemma. Assume that, for some basic term P, P →^{α} P′ and P′ ⊀ P. We prove that P, P′ ∈ ℍ and P ≅ P′.

To this end, note, first of all, that, since P′ is a proper derivative of P and P′ ⊀ P, it must be the case that P is a proper derivative of P′. So there exists a sequence of transitions

P_{0} →^{α_{1}} P_{1} →^{α_{2}} ⋯ →^{α_{n}} P_{n}, n ≥ 2,

where P_{0} ≡ P ≡ P_{n} and P_{1} ≡ P′. Note that each term P_{k}, 0 ≤ k ≤ n, is basic as P is (Lem. 3.2).

We claim that P_{l} ∈ ℍ for some 0 ≤ l ≤ n. In fact, assume, towards a contradiction, that P_{k} ∉ ℍ for all k. Then fact A implies that P_{k+1} has smaller size than P_{k} for k = 0, ..., n − 1. Therefore P has smaller size than itself, which is impossible.

Hence, P_{l} ∈ ℍ for some l. Since each P_{k} is a proper derivative of each P_{k′}, we have g(P_{k}) ≤ g(P_{k′}) for all k and k′ (Lem. 3.5). Therefore g(P_{k}) must be the same for all k. Now fact B and P_{l} ∈ ℍ imply that P_{k} ∈ ℍ for all k, and P_{0} ≅ P_{1} ≅ ⋯ ≅ P_{n}. □

Elements of 𝔹 × 𝔹 are considered modulo commutativity. The well-founded ordering ≺ on 𝔹 induces an ordering on 𝔹 × 𝔹 as the least transitive relation satisfying:

(P, Q) ⊏ (R, S) if P ≺ R and Q ≅ S .

It is immediate to see that the above-defined ordering on 𝔹 × 𝔹 is also well-founded.

3.3 A Lemma

In the proof of the completeness theorem to follow, we shall often need to analyze equivalences between terms of the form P′(P_{1}, ..., P_{m})^{∗}(Q_{1}, ..., Q_{m}). We now aim at establishing a lemma that will be a useful tool in the study of these equivalences.

Notation 3.9 For a term X ≡ (P_{1}, ..., P_{n})^{∗}(Q_{1}, ..., Q_{n}), the expression shift(X) stands for the term (P_{2}, ..., P_{n}, P_{1})^{∗}(Q_{2}, ..., Q_{n}, Q_{1}). For a non-negative integer k, shift^{k}(X) denotes the result of applying the function shift to the term X k times. Note that X \underline{↔} P_{1}shift(X) + Q_{1}.

The following lemma will be applied in the proof of Lem. 3.11.

Lemma 3.10 Let X ≡ (P_{1}, ..., P_{m})^{∗}(Q_{1}, ..., Q_{m}) and Y ≡ (R_{1}, ..., R_{n})^{∗}(S_{1}, ..., S_{n}). Assume that T X \underline{↔} UY for some T and U, and that Q_{1} does not have a proper derivative that is bisimilar to Y. Then we have the following two possibilities:

1. either T \underline{↔} U;

2. or T \underline{↔} U(V + W) for some terms V and W, whose proper derivatives are contained in those of T, such that V X \underline{↔} R_{1}shift(Y) and W X \underline{↔} S_{1}.

Proof: Lem. 2.5 applied to the equivalence T X \underline{↔} UY yields three possibilities:

A. either T \underline{↔} U and X \underline{↔} Y;

B. or T \underline{↔} UT′ and T′X \underline{↔} Y for some proper derivative T′ of T;

C. or T U′ \underline{↔} Y and X \underline{↔} U′Y for some proper derivative U′ of U.

Case A agrees with the first statement in the lemma.

If case B holds, then T′X \underline{↔} Y \underline{↔} R_{1}shift(Y) + S_{1}. Then clearly there exist terms V and W, whose proper derivatives are contained in those of T′, such that T′ \underline{↔} V +W, V X \underline{↔} R_{1}shift(Y), and W X \underline{↔} S_{1}. This agrees with the second statement in the lemma.

Finally, case C contradicts one of the assumptions. In fact, as X \underline{↔} U′Y implies P_{1}shift(X)+ Q_{1} \underline{↔} U′Y, in that case Q_{1} has a proper derivative that is bisimilar to Y. □

The following technical lemma will be used repeatedly in the proof of the promised completeness theorem.

Lemma 3.11 Let X ≡ (P_{1}, ..., P_{m})^{∗}(Q_{1}, ..., Q_{m}) and Y ≡ (R_{1}, ..., R_{n})^{∗}(S_{1}, ..., S_{n}). Assume that T_{1}X \underline{↔} R_{1}shift(Y) for some term T_{1}, and that Q_{1} has no proper derivative that is bisimilar to Y. Then we have the following two possibilities:

I. either there are terms U_{1}, ..., U_{n}, whose proper derivatives are contained in those of T_{1}, such that:

T_{1}  \underline{↔} R_{1}(R_{2}, ..., R_{n}, R_{1})^{∗}(U_{2}, ..., U_{n}, U_{1})
U_{i}X \underline{↔} S_{i}  i = 1, ..., n

II. or there is a k ∈ {1, ..., n} and there are terms T_{2}, ..., T_{k} and U_{2}, ..., U_{k}, whose proper derivatives are contained in those of T_{1}, such that:

T_{i}  \underline{↔} R_{i}(T_{i+1} + U_{i+1}) i = 1, ..., k − 1
T_{k}  \underline{↔} R_{k}
T_{i}X \underline{↔} R_{i}shift^{i}(Y)  i = 2, ..., k
U_{i}X \underline{↔} S_{i}  i = 2, ..., k .

Proof: Assume that the proviso of the lemma holds for some terms X, Y and T_{1} of the required form. Consider the following equivalence A_{i} for some i ≤ n:

A_{i} T_{i}X \underline{↔} R_{i}shift^{i}(Y).

Recall that we assumed that it holds for i = 1.

As Q_{1} has no proper derivative that is bisimilar to Y, and Y is a proper derivative of shift^{i}(Y) for every non-negative integer i, it follows that Q_{1} has no proper derivative that is bisimilar to shift^{i}(Y). Therefore we can apply Lem. 3.10 to equivalence A_{i} to obtain the following possibilities; either

B_{i} T_{i} \underline{↔} R_{i},

or, if i < n, then there exist terms T_{i+1} and U_{i+1}, whose proper derivatives are contained in those of T_{i}, such that

C_{i} T_{i} \underline{↔} R_{i}(T_{i+1} + U_{i+1}), T_{i+1}X \underline{↔} R_{i+1}shift^{i+1}(Y) and U_{i+1}X \underline{↔} S_{i+1},

or, if i = n, then there exist terms T_{n+1} and U_{1}, whose proper derivatives are contained in those of T_{n}, such that

C_{n} T_{n} \underline{↔} R_{n}(T_{n+1} + U_{1}), T_{n+1}X \underline{↔} R_{1}shift(Y) and U_{1}X \underline{↔} S_{1}.

Note that, by transitivity, the proper derivatives of the T_{i} and the U_{i} are all contained in those of T_{1}.

In light of the above discussion, Lem. 3.10 gives that condition A_{i} implies either B_{i} or C_{i} for i = 1, ..., n. Furthermore, C_{i} clearly implies A_{i+1} for i = 1, ..., n − 1. So, since we assumed that A_{1} holds, we can distinguish the following two cases:

I. either C_{1}, ..., C_{n} hold;

II. or there is a k ∈ {1, ..., n} such that C_{1}, ..., C_{k−1} and B_{k} hold.

We consider these two cases in turn.

I. Suppose that C_{1}, ..., C_{n} hold, so that:

T_{i} \underline{↔} R_{i}(T_{i+1} + U_{i+1}) i = 1, ..., n − 1
T_{n} \underline{↔} R_{n}(T_{n+1} + U_{1})
U_{i}X \underline{↔} S_{i}  i = 1, ..., n
T_{n+1}X \underline{↔} R_{1}shift(Y) .

By assumption T_{1}X \underline{↔} R_{1}shift(Y), so the last equivalence implies T_{n+1}X \underline{↔} T_{1}X. Then Lem. 2.5 yields T_{n+1} \underline{↔} T_{1}. To complete the proof for this case, it is sufficient to show that the equivalences

T_{i} \underline{↔} R_{i}(T_{i+1} + U_{i+1})  i = 1, ..., n − 1
T_{n} \underline{↔} R_{n}(T_{1} + U_{1})

together yield the following equivalence:

T_{1} \underline{↔} R_{1}(R_{2}, ..., R_{n}, R_{1})^{∗}(U_{2}, ..., U_{n}, U_{1}) .

The construction of the required bisimulation relation is not hard, and is left to the reader.

II. Suppose that there is a k ∈ {1, ..., n} such that C_{1}, ..., C_{k−1} and B_{k} hold. Then

T_{i} \underline{↔} R_{i}(T_{i+1} + U_{i+1}) i = 1, ..., k − 1
T_{k}  \underline{↔} R_{k}
T_{i}X \underline{↔} R_{i}shift^{i}(Y)  i = 2, ..., k
U_{i}X \underline{↔} S_{i}  i = 2, ..., k

and we are done.

The proof of the lemma is now complete. □

3.4 The Completeness Theorem

We are finally in a position to prove the desired completeness result.

Theorem 3.12 (Completeness) Let X, Y ∈ (BPA^{me∗}(A)). If X \underline{↔} Y, then E ⊢ X = Y.

Proof: First of all, note that, as each process term is provably equal to a basic term (Lem. 3.1), it is sufficient to show that bisimilar basic terms are provably equal. This we proceed to do by induction on the well-founded ordering ⊏ on 𝔹×𝔹. To this end, assume that X, Y are basic terms such that X \underline{↔} Y. Suppose furthermore, as inductive hypothesis that if two basic terms X′, Y′ with (X′, Y′) ⊏ (X, Y) are bisimilar, then E ⊢ X′ = Y′. We proceed to show that E ⊢ X = Y. For notational convenience, we shall write X = Y in lieu of E ⊢ X = Y. Throughout the proof, we shall use the fact that the collection of basic terms is closed under transitions (Lem. 3.2) without further mention. We prove the claim by considering the following two cases:

Case 1. X ∉ ℍ or Y ∉ ℍ;

Case 2. Both X and Y are in ℍ. We examine these two cases in turn.

• Case 1. Assume that X ∉ ℍ or Y ∉ ℍ. By symmetry, we may suppose that X ∉ ℍ. Since X \underline{↔} Y, by possibly using axiom A3 we can adapt the expansions of X and Y to the following forms:

X = ∑_{i=1}^{m} α_{i}X_{i} + ∑_{j=1}^{n} β_{j} Y = ∑_{i=1}^{m} α_{i}Y_{i} + ∑_{j=1}^{n} β_{j}

where X_{i} \underline{↔} Y_{i} for i = 1, ..., m. As X ∉ ℍ, Lem. 3.8 gives that X_{i} ≺ X for i = 1, ..., m. Furthermore, again using Lem. 3.8, we infer that, for i = 1, ..., m, either Y_{i} ≺ Y or Y_{i} ≅ Y. Therefore, for every index i, (X_{i}, Y_{i}) ⊏ (X, Y), and we may apply the inductive hypothesis to the equivalence X_{i} \underline{↔} Y_{i} to derive that X_{i} = Y_{i}. Hence, by substitutivity it follows that X = Y, and we are done.

• Case 2. Assume that X, Y ∈ ℍ. We proceed with the proof by considering the possible forms these bisimilar terms may take. By symmetry, it is sufficient to distinguish the following three cases:

Case 2.1. X ≡ (P_{1}, ..., P_{m})^{∗}(Q_{1}, ..., Q_{m}) and Y ≡ (R_{1}, ..., R_{n})^{∗}(S_{1}, ..., S_{n});

Case 2.2. X ≡ P′(P_{1}, ..., P_{m})^{∗}(Q_{1}, ..., Q_{m}) for some proper derivative P′ of P_{m}, and Y ≡ (R_{1}, ..., R_{n})^{∗}(S_{1}, ..., S_{n});

Case 2.3. X ≡ P′(P_{1}, ..., P_{m})^{∗}(Q_{1}, ..., Q_{m}) for some proper derivative P′ of P_{m}, and Y ≡ R′(R_{1}, ..., R_{n})^{∗}(S_{1}, ..., S_{n}) for some proper derivative R′ of R_{n}. We proceed by considering each of these cases in turn.

∗ Case 2.1. Let X ≡ (P_{1}, ..., P_{m})^{∗}(Q_{1}, ..., Q_{m}) and Y ≡ (R_{1}, ..., R_{n})^{∗}(S_{1}, ..., S_{n}). By symmetry, it is sufficient to consider the following two sub-cases:

Case 2.1.1. There exist a proper derivative Q′ of some Q_{i} with Q′ \underline{↔} Y, and a proper derivative S′ of some S_{j} with S′ \underline{↔} X;

Case 2.1.2. No proper derivative of any Q_{i} is bisimilar to Y. We consider these two sub-cases in turn.

∘ Case 2.1.1. Assume that there exist a proper derivative Q′ of some Q_{i} with Q′ \underline{↔} Y, and a proper derivative S′ of some S_{j} with S′ \underline{↔} X. Note that, by transitivity, we may infer that Q′ \underline{↔} S′. As Q′ ≺ X and S′ ≺ Y (Lem. 3.6), we may apply the inductive hypothesis to each of the aforementioned equivalences to derive that

X = S′ = Q′ = Y

and we are done.

∘ Case 2.1.2. Assume that no proper derivative of any Q_{i} is bisimilar to Y.

We begin the proof for this case by adapting X and Y.

Definition 3.13 For Z ≡ (T_{1}, ..., T_{j})^{∗}(U_{1}, ..., U_{j}), let K(Z) denote the number of i’s in \{1, ..., j\} for which shift^{i}(Z) \underline{↔} Z. Note that K(Z) ≥ 1, as shift^{j}(Z) ≡ Z.

Put

\begin{aligned}X_{0} & ≡ & ((P_{1}, ..., P_{m})^{K(Y)})^{∗}((Q_{1}, ..., Q_{m})^{K(Y)}) \\ Y_{0} & ≡ & ((R_{1}, ..., R_{n})^{K(X)})^{∗}((S_{1}, ..., S_{n})^{K(X)}) . \end{aligned}

It is not hard to see that, for every i ∈ {1, …, m} and k ∈ {0, …, K(Y) − 1},

shift^{i}(X) \underline{↔} shift^{i+km}(X_{0}) .

Similarly, for every j ∈ {1, …, n} and k ∈ {0, …, K(X) − 1},

shift^{j}(Y) \underline{↔} shift^{j+kn}(Y_{0}) .

Since X_{0} \underline{↔} X and Y_{0} \underline{↔} Y, it follows that both K(X_{0}) and K(Y_{0}) are equal to K(X) · K(Y). Owing to axiom MEI5, the equalities X = X_{0} and Y = Y_{0} are provable. The rest of the proof for this case will be devoted to proving X_{0} = Y_{0}. For notational convenience, put X_{0} ≡ (P_{1}, ..., P_{M})^{∗}(Q_{1}, ..., Q_{M}) and Y_{0} ≡ (R_{1}, ..., R_{N})^{∗}(S_{1}, ..., S_{N}). We shall now prove that there exists an increasing sequence of integers 0 = c_{0} < ⋯ < c_{M} = N such that for l = 0, ..., M:

A_{l} shift^{l}(X_{0}) \underline{↔} shift^{c_{l}}(Y_{0});

B_{l} shift^{i}(Y_{0}) \underline{↔} / Y_{0} for c_{l−1} < i < c_{l} (where, by convention, c_{−1} =^{Δ} 0);

C_{l} X_{0} = (R_{1}, ..., R_{c_{l}}, P_{l+1}, ..., P_{M})^{∗}(S_{1}, ..., S_{c_{l}}, Q_{l+1}, ..., Q_{M}).

In fact, we shall show that the conjunction of the statements A_{l}, B_{l} and C_{l} implies the conjunction of A_{l+1}, B_{l+1} and C_{l+1} for l < M. Since A_{0} (viz. X_{0} \underline{↔} Y_{0}), B_{0} (viz. a vacuous statement) and C_{0} (viz. X_{0} = X_{0}) hold, we can then conclude that C_{M} (viz. X_{0} = Y_{0}) holds, which is what we want to prove. Throughout the proof, we shall make use of the fact that, as X ≅ X_{0} and Y ≅ Y_{0}, these terms dominate the same basic terms with respect to the well-founded ordering ≺. This remark will allow us to apply the inductive hypothesis to all pairs (X′, Y′) of bisimilar terms such that (X′, Y′) ⊏ (X_{0}, Y_{0}), and will be used without further mention. Assume now that, for some l with 0 ≤ l < M, the statements A_{i}, B_{i} and C_{i} hold for all i ≤ l and some increasing sequence of integers 0 = c_{0} < ⋯ < c_{l} < N. We set out to deduce the statements A_{l+1}, B_{l+1} and C_{l+1} for some c_{l+1} with c_{l} < c_{l+1} ≤ N, where c_{l+1} equals N if and only if l + 1 = M. First, we spell out the expansions of P_{l+1} and R_{c_{l}+1}:

P_{l+1} = ∑_{i∈I} T_{i} R_{c_{l}+1} = ∑_{j∈J} U_{j}

where the summands T_{i} and U_{j} are of the form either αV or α.

As A_{l} holds, P_{l+1}shift^{l+1}(X_{0})+Q_{l+1} \underline{↔} R_{c_{l}+1}shift^{c_{l}+1}(Y_{0})+S_{c_{l}+1}. Hence, for every i ∈ I, either there exists an index j ∈ J such that

(2)  T_{i}shift^{l+1}(X_{0}) \underline{↔} U_{j}shift^{c_{l}+1}(Y_{0})

or there exists a summand αS′ of S_{c_{l}+1} such that

(3)  T_{i}shift^{l+1}(X_{0}) \underline{↔} αS′ .

Thus, I can be divided into the following, not necessarily disjoint, subsets:

I_{0} =^{Δ} {i ∈ I | ∃α, S′ : S_{c_{l}+1} →^{α} S′ and (3) holds}
I_{1} =^{Δ} {i ∈ I | ∃j ∈ J such that (2) holds} .

On the other hand, for every j ∈ J there exists an i ∈ I such that equivalence (2) holds. In fact, suppose, towards a contradiction, that for some j ∈ J this does not hold. Since P_{l+1}shift^{l+1}(X_{0})+Q_{l+1} \underline{↔} R_{c_{l}+1}shift^{c_{l}+1}(Y_{0})+S_{c_{l}+1}, it follows that for this j there exists a summand αQ′ of Q_{l+1} such that

αQ′ \underline{↔} U_{j}shift^{c_{l}+1}(Y_{0}) .

Since Y_{0} is a derivative of shift^{c_{l}+1}(Y_{0}), then there is a proper derivative of Q_{l+1} that is bisimilar to Y_{0}, and therefore to Y. This contradicts the assumption for case 2.1.2. Note that, by our previous reasoning, the index set I_{1} is non-empty; let V_{1} denote the term ∑_{i∈I_{1}} T_{i}. The following equation follows by possibly using axiom A3:

(4)  P_{l+1} = ∑_{i∈I_{0}} T_{i} + V_{1} .

Moreover, the following equivalence is an immediate consequence of the fact that for every j ∈ J there exists an i ∈ I such that equivalence (2) holds:

(5)  V_{1}shift^{l+1}(X_{0}) \underline{↔} R_{c_{l}+1}shift^{c_{l}+1}(Y_{0}) .

We proceed with the proof by deriving the following equality:

(6)  ∑_{i∈I_{0}} T_{i}shift^{l+1}(X_{0}) + Q_{l+1} = S_{c_{l}+1} .

Proof of Equation (6). We show that each summand of S_{c_{l}+1} is provably equal to a summand of the term at the left-hand side of the equation, and vice versa. Let αS′ be a summand of S_{c_{l}+1}; then the transition shift^{c_{l}}(Y_{0}) →^{α} S′ holds. As

P_{l+1}shift^{l+1}(X_{0}) + Q_{l+1} \underline{↔} shift^{c_{l}}(Y_{0})

by assumption A_{l}, either there exists an i ∈ I_{0} such that (3) holds, or there exists a summand αQ′ of Q_{l+1} such that

(7)  Q′ \underline{↔} S′ .

If there exists an i ∈ I_{0} such that (3) holds, then

1. either T_{i} ≡ αP′ for some proper derivative P′ of P_{l+1} such that P′shift^{l+1}(X_{0}) \underline{↔} S′,

2. or T_{i} ≡ α and shift^{l+1}(X_{0}) \underline{↔} S′.

As S′ ≺ Y_{0} (Lem. 3.6), P′shift^{l+1}(X_{0}) ≅ X_{0} and shift^{l+1}(X_{0}) ≅ X_{0}, in each of these two cases we may apply the inductive hypothesis and substitutivity to infer that

T_{i}shift^{l+1}(X_{0}) = αS′ .

If (7) holds, then Q′ ≺ X_{0} and S′ ≺ Y_{0} (Lem. 3.6), so that we may apply the inductive hypothesis and substitutivity to infer

αQ′ = αS′ .

If α is a summand of S_{c_{l}+1}, then α must also be a summand of Q_{l+1}, and therefore of the term on the left-hand side of the equation. Hence, every summand of S_{c_{l}+1} is provably equal to a summand of the term at the left-hand side of (6). By the symmetric argument it can be shown that every summand of the term at the left-hand side of (6) is provably equal to a summand of S_{c_{l}+1}. Namely, by definition of I_{0} each term T_{i}shift^{l+1}(X_{0}) for i ∈ I_{0} is bisimilar to a summand of S_{c_{l}+1}. Moreover, as P_{l+1}shift^{l+1}(X_{0}) + Q_{l+1} \underline{↔} R_{c_{l}+1}shift^{c_{l}+1}(Y_{0}) + S_{c_{l}+1}, Y_{0} is a derivative of shift(Y_{0}), and no derivative of Q_{l+1} is bisimilar to Y_{0}, every summand of Q_{l+1} must be bisimilar to a summand of S_{c_{l}+1}. End of Proof of Equation (6).

We now proceed with our argument by analyzing equivalence (5) using Lem. 3.11. According to this lemma two possibilities may arise, which we consider in turn.

- Case 2.1.2.1. If the first case of Lem. 3.11 holds with respect to equivalence (5), then, in particular, there exists a term W such that

W shift^{l+1}(X_{0}) \underline{↔} S_{c_{l}+1} .

Equality (6) implies the equivalence

W shift^{l+1}(X_{0}) \underline{↔} ∑_{i∈I_{0}} T_{i}shift(X_{0}) + Q_{l+1} .

Since X_{0} is a derivative of shift^{l+1}(X_{0}) and Y_{0} \underline{↔} X_{0}, it follows that there is a proper derivative of Q_{l+1} which is bisimilar to Y_{0}, and therefore to Y. This contradicts the assumption at the start of case 2.1.2.

- Case 2.1.2.2. In light of the previous discussion, we may assume that the second case of Lem. 3.11 holds with respect to equivalence (5). In this case, note, first of all, that, for every j, h ≥ 0,

shift^{j}(Y_{0}) ≡ shift^{j+hn}(Y_{0}) .

Therefore, by the second case of Lem. 3.11, there is an integer k ∈ {1, ..., n} and there exist terms V_{2}, ..., V_{k} and W_{2}, ..., W_{k}, whose proper derivatives are contained in those of V_{1}, such that:

(8)  V_{i} \underline{↔} R_{c_{l}+i}(V_{i+1} + W_{i+1})  i = 1, ..., k − 1
(9)  V_{k}  \underline{↔} R_{c_{l}+k}
(10)  V_{i}shift^{l+1}(X_{0}) \underline{↔} R_{c_{l}+i}shift^{c_{l}+i}(Y_{0})  i = 2, ..., k
(11)  W_{i}shift^{l+1}(X_{0}) \underline{↔} S_{c_{l}+i}  i = 2, ..., k .

Put c_{l+1} =^{Δ} c_{l} + k. We now show that A_{l+1}, B_{l+1} and C_{l+1} hold, and that c_{l+1} ≤ N, with c_{l+1} = N iff l + 1 = M. Equivalence (9) and the instance of (10) for i = k, together with Lem. 2.5, yield the equivalence

shift^{l+1}(X_{0}) \underline{↔} shift^{c_{l+1}}(Y_{0})

which corresponds to A_{l+1}. We now show that B_{l+1} holds. Suppose, towards a contradiction, that shift^{c_{l}+i}(Y_{0}) \underline{↔} Y_{0} for some i ∈ {1, ..., k − 1}. Equivalences (10) and (11), together with A4 and MEI1, imply that shift^{c_{l}+i}(Y_{0}) \underline{↔} (V_{i+1} + W_{i+1})shift^{l+1}(X_{0}). Therefore, as X_{0} \underline{↔} Y_{0},

P_{1}shift(X_{0}) + Q_{1} \underline{↔} Y_{0} \underline{↔} shift^{c_{l}+i}(Y_{0}) \underline{↔} (V_{i+1} + W_{i+1})shift^{l+1}(X_{0}) .

As X_{0} is a derivative of shift^{l+1}(X_{0}), and Y_{0} \underline{↔} X_{0}, it follows that Q_{1} has a derivative bisimilar to Y_{0}, and therefore to Y. This contradicts the assumption for case 2.1.2. So it must be the case that shift^{c_{l}+i}(Y_{0}) \underline{↔} / Y_{0} for i = 1, ..., k − 1, which corresponds to B_{l+1}. As c_{l} < N and B_{l+1} holds, it follows that c_{l} + i ≠ N for i = 1, ..., k − 1. Hence c_{l+1} ≤ N. We now show that c_{l+1} = N iff l + 1 = M. By definition of K(Z) (Def. 3.13) we have:

- c_{l+1} = N iff there are K(Y_{0}) indices i ∈ \{1, ..., c_{l+1}\} with shift^{i}(Y_{0}) \underline{↔} Y_{0};

- l + 1 = M iff there are K(X_{0}) indices j ∈ \{1, ..., l + 1\} with shift^{j}(X_{0}) \underline{↔} X_{0}.

Recall that X_{0} and Y_{0} where designed such that K(X_{0}) = K(Y_{0}). Furthermore, A_{i} and B_{i} for i ≤ l +1 imply that shift^{i}(Y_{0}) \underline{↔} Y_{0} for 1 ≤ i ≤ c_{l+1} iff i = c_{j} for some j ∈ \{1, ..., l +1\} with shift^{j}(X_{0}) \underline{↔} X_{0}. Hence, it follows that c_{l+1} = N iff l + 1 = M. It remains to prove that C_{l+1} holds. Equality (4) implies that L(V_{1}) ≤ L(P_{l+1}), so, by Lem. 2.7, L(V_{1}) < L(X_{0}). Since the proper derivatives of the terms V_{i} are contained in those of V_{1}, it follows that L(V_{i}) < L(X_{0}) for i = 2, ..., k. Now, invariance of L-value under bisimulation (Lem. 2.7), together with the equivalences X_{0} \underline{↔} Y_{0}, (8) and (9), yields

1. L(R_{c_{l}+i}(V_{i+1} + W_{i+1})) < L(Y_{0}) for i = 1, ..., k − 1 and

2. L(R_{c_{l+1}}) < L(Y_{0}).

It follows that

- V_{i} ≺ X_{0} for i = 1, ..., k,

- R_{i}(V_{i+1} + W_{i+1}) ≺ Y_{0} for i = 1, ..., k − 1 and

- R_{c_{l+1}} ≺ Y_{0}.

Thus we can apply induction to equivalences (8) and (9) to derive

(12)  V_{i} = R_{c_{l}+i}(V_{i+1} + W_{i+1})  i = 1, ..., k − 1
(13)  V_{k} = R_{c_{l+1}} .

Furthermore, since S′ ≺ Y_{0} for every proper derivative S′ of each term S_{c_{l}+i} (Lem. 3.6), and since each derivative in the expansion of W_{i}shift^{l+1}(X_{0}) is ≅-equivalent to X_{0}, we can apply the same reasoning used in the proof of (6) to equivalence (11) to obtain

(14)  W_{i}shift^{l+1}(X_{0}) = S_{c_{l}+i}  i = 2, ..., k .

The equations that we derived up to now can be used to prove

(15) X_{0} = (R_{1}, ..., R_{c_{l}+i−1}, V_{i}, P_{l+2}, ..., P_{M})^{∗}(S_{1}, ..., S_{c_{l}+i−1}, S_{c_{l}+i}, Q_{l+2}, ..., Q_{M})

for i = 1, ..., k − 1, and

(16)  X_{0} = (R_{1}, ..., R_{c_{l+1}}, P_{l+2}, ..., P_{M})^{∗}(S_{1}, ..., S_{c_{l+1}}, Q_{l+2}, ..., Q_{M}) .

In order to derive these equations, we apply induction on i. First, we deal with the case i = 1:

X_{0}  =^{C_{l}} (R_{1}, ..., R_{c_{l}}, P_{l+1}, ..., P_{M})^{∗}(S_{1}, ..., S_{c_{l}}, Q_{l+1}, ..., Q_{M})
=^{(4)} (R_{1}, ..., R_{c_{l}}, ∑_{i∈I_{0}} T_{i} + V_{1}, P_{l+2}, ..., P_{M})^{∗}(S_{1}, ..., S_{c_{l}}, Q_{l+1}, Q_{l+2}..., Q_{M})
=^{MEI3′} (R_{1}, ..., R_{c_{l}}, V_{1}, P_{l+2}, ..., P_{M})^{∗}(S_{1}, ..., S_{c_{l}}, ∑_{i∈I_{0}} T_{i}Z + Q_{l+1}, Q_{l+2}..., Q_{M})

where

Z =^{(4)} (P_{l+2}, ..., P_{M}, R_{1}, ..., R_{c_{l}}, P_{1})^{∗}(Q_{l+2}..., Q_{M}, S_{1}, ..., S_{c_{l}}, Q_{l+1}) .

Applying MEI1 to the right-hand side of the above equation for M − l − 1 times, followed by equation C_{l}, we obtain

Z = P_{l+2}(⋯ (P_{M}X_{0} + Q_{M}) ⋯) + Q_{l+2} .

Again applying MEI1 to the above equation, but this time from right to left, we deduce the equality Z = shift^{l+1}(X_{0}). Therefore:

X_{0} =

(R_{1}, ..., R_{c_{l}}, V_{1}, P_{l+2}, ..., P_{M})^{∗}(S_{1}, ..., S_{c_{l}}, ∑_{i∈I_{0}} T_{i}shift^{l+1}(X_{0}) + Q_{l+1}, Q_{l+2}..., Q_{M})

=^{(6)} (R_{1}, ..., R_{c_{l}}, V_{1}, P_{l+2}, ..., P_{M})^{∗}(S_{1}, ..., S_{c_{l}}, S_{c_{l}+1}, Q_{l+2}..., Q_{M}) .

If k > 1, then we have proven equation (15) for i = 1. If k = 1, then c_{l+1} = c_{l} + 1, and by equation (13) V_{1} = R_{c_{l+1}}, which proves (16). Next, suppose that we have proven equation (15) for i = j, where 1 ≤ j < k. We derive either equation (15) for i = j + 1, if k > j + 1, or equation (16), if k = j + 1. To this end, we reason as follows:

X_{0} =^{(15),(12)}

(R_{1}, ..., R_{c_{l}+j−1}, R_{c_{l}+j}(V_{j+1} + W_{j+1}), P_{l+2}, ..., P_{M})^{∗}(S_{1}, ..., S_{c_{l}+j}, Q_{l+2}, ..., Q_{M})

=^{MEI4′} (R_{1}, ..., R_{c_{l}+j}, V_{j+1}, P_{l+2}, ..., P_{M})^{∗}(S_{1}, ..., S_{c_{l}+j}, W_{j+1}Z, Q_{l+2}, ..., Q_{M})

where

Z =^{(12)} (P_{l+2}, ..., P_{M}, R_{1}, ..., R_{c_{l}+j−1}, V_{j})^{∗}(Q_{l+2}..., Q_{M}, S_{1}, ..., S_{c_{l}+j−1}, S_{c_{l}+j}) .

Applying MEI1 for M − l − 1 times, followed by equation (15), we obtain

Z = P_{l+2}(⋯ (P_{M}X_{0} + Q_{M}) ⋯) + Q_{l+2} .

Again using MEI1, we may now deduce the equality Z = shift^{l+1}(X_{0}). Therefore:

X_{0} = (R_{1}, ..., R_{c_{l}+j}, V_{j+1}, P_{l+2}, ..., P_{M})^{∗}(S_{1}, ..., S_{c_{l}+j}, W_{j+1}shift^{l+1}(X_{0}), Q_{l+2}, ..., Q_{M})

=^{(14)} (R_{1}, ..., R_{c_{l}+j}, V_{j+1}, P_{l+2}, ..., P_{M})^{∗}(S_{1}, ..., S_{c_{l}+j}, S_{c_{l}+j+1}, Q_{l+2}, ..., Q_{M}) .

If k > j + 1, then we have proven equation (15) for i = j + 1. If k = j + 1, then c_{l+1} = c_{l} + j + 1, and by equation (13) V_{j+1} = R_{c_{l+1}}, which proves equation (16). Equation (16) corresponds to C_{l+1}. Thus, we have completed the proof that the conjunction of A_{l}, B_{l} and C_{l} implies the conjunction of A_{l+1}, B_{l+1} and C_{l+1} for 0 ≤ l < M. Since A_{0}, B_{0} and C_{0} hold, we can then conclude C_{M}, that is, X_{0} = Y_{0}. By axiom MEI5, it follows that X = X_{0} and Y = Y_{0}. Therefore X = Y, which finishes the proof of this case.

∗ Case 2.2. Assume that X ≡ P′(P_{1}, ..., P_{m})^{∗}(Q_{1}, ..., Q_{m}) for some proper derivative P′ of P_{m}, and Y ≡ (R_{1}, ..., R_{n})^{∗}(S_{1}, ..., S_{n}). For notational convenience we put X′ ≡ (P_{1}, ..., P_{m})^{∗}(Q_{1}, ..., Q_{m}). We proceed with the proof by distinguishing two sub-cases, depending on whether any of the terms Q_{i} has a proper derivative that is bisimilar to Y or not.

∘ Case 2.2.1. Suppose that there is a proper derivative Q′ of some Q_{i}, for i = 1, ..., m, such that Q′ \underline{↔} Y. As P′X′ \underline{↔} R_{1}shift(Y) + S_{1}, and X is a derivative of X′, it follows that S_{1} has a proper derivative S′ that is bisimilar to X. Hence, transitivity yields X \underline{↔} S′ \underline{↔} Q′ \underline{↔} Y. Since S′ ≺ Y and Q′ ≺ X (Lem. 3.6), we can apply induction to these three equivalences to obtain

X = S′ = Q′ = Y .

∘ Case 2.2.2. Suppose that no proper derivative of any Q_{i} is bisimilar to Y.

As P′X′ \underline{↔} Y \underline{↔} R_{1}shift(Y) + S_{1}, there exist terms T_{1} and U_{1}, whose proper derivatives are contained in those of P′, such that:

(17)  P′ \underline{↔} T_{1} + U_{1}
(18)  T_{1}X′ \underline{↔} R_{1}shift(Y)
(19)  U_{1}X′ \underline{↔} S_{1} .

As L(P′) < L(X) (Lem. 2.7), in light of the equivalences X \underline{↔} Y and (17), invariance of L-value under bisimulation (Lem. 2.7) yields L(T_{1} + U_{1}) < L(Y). It follows that P′ ≺ X′ and T_{1} + U_{1} ≺ Y. Therefore, by induction, equivalence (17) can be proven:

(20)  P′ = T_{1} + U_{1} .

Furthermore, since S′ ≺ Y for every proper derivative S′ of S_{1} (Lem. 3.6), and since each derivative in the expansion of U_{1}X′ is ≅-equivalent to X, we can apply the same reasoning used in the proof of (6) to equivalence (19) to obtain

(21)  U_{1}X′ = S_{1} .

Finally, we can apply Lem. 3.11 to equivalence (18) to obtain the following two possibilities:

- Case 2.2.2.1. If case I of Lem. 3.11 holds, then there are terms V_{1}, ..., V_{n}, whose proper derivatives are contained in those of T_{1}, such that:

(22)  T_{1} \underline{↔} R_{1}(R_{2}, ..., R_{n}, R_{1})^{∗}(V_{2}, ..., V_{n}, V_{1})
(23)  V_{i}X′ \underline{↔} S_{i}  i = 1, ..., n .

By (17) and Lem. 2.7, it follows that L(T_{1}) ≤ L(P′) < L(X). In light of the equivalences X \underline{↔} Y and (22), invariance of L-value under bisimulation (Lem. 2.7), yields that

L(R_{1}(R_{2}, ..., R_{n}, R_{1})^{∗}(V_{2}, ..., V_{n}, V_{1})) < L(Y) .

Hence, we can apply induction to equivalence (22) to obtain

(24)  T_{1} = R_{1}(R_{2}, ..., R_{n}, R_{1})^{∗}(V_{2}, ..., V_{n}, V_{1}) .

Moreover, since S′ ≺ Y for every proper derivative S′ of S_{i} (Lem. 3.6), and since each derivative in the expansion of V_{i}X′ is ≅-equivalent to X, we can apply the same reasoning used in the proof of (6) to derive equivalence (23):

(25)  V_{i}X′ = S_{i}  i = 1, ..., n .

Hence, we may conclude the proof for this case thus:

X ≡ P′X′  =^{(20)}  (T_{1} + U_{1})X′
=^{A4,(24),(21)} R_{1}(R_{2}, ..., R_{n}, R_{1})^{∗}(V_{2}, ..., V_{n}, V_{1})X′ + S_{1}
=^{MEI2,(25)} R_{1}(R_{2}, ..., R_{n}, R_{1})^{∗}(S_{2}, ..., S_{n}, S_{1}) + S_{1}
=^{MEI1}  Y .

- Case 2.2.2.2. If case II of Lem. 3.11 holds, then there is a k ∈ {1, ..., n} and there are terms T_{2}, ..., T_{k} and U_{2}, ..., U_{k}, whose proper derivatives are contained in those of T_{1}, such that:

(26)  T_{i} \underline{↔} R_{i}(T_{i+1} + U_{i+1})  i = 1, ..., k − 1
(27)  T_{k}  \underline{↔} R_{k}
(28)  T_{k}X′ \underline{↔} R_{k}shift^{k}(Y)
(29)  U_{i}X′ \underline{↔} S_{i}  i = 2, ..., k .

By (17) and Lem. 2.7, it follows that L(T_{1}) ≤ L(P′) < L(X). Since the proper derivatives of the terms T_{i} are contained in those of T_{1}, it follows that L(T_{i}) < L(X) for i = 2, ..., k. In light of the equivalences X \underline{↔} Y and (26)–(27), invariance of L-value under bisimulation (Lem. 2.7) yields

- L(R_{i}(T_{i+1} + U_{i+1})) < L(Y) for i = 1, ..., k − 1 and

- L(R_{k}) < L(Y).

Hence, we may apply induction to equivalences (26) and (27) to infer that:

(30)  T_{i} = R_{i}(T_{i+1} + U_{i+1})  i = 1, ..., k − 1
(31)  T_{k} = R_{k} .

Reasoning as in the proof of (6), it is not hard to deduce equivalence (29):

(32)  U_{i}X′ = S_{i}  i = 2, ..., k .

Furthermore, equivalences (27), (28), and Lem. 2.5 imply that X′ \underline{↔} shift^{k}(Y). This equivalence can be deduced by case 2.1 of the proof:

(33)  X′ = shift^{k}(Y) .

We can now use these equalities to derive X = Y as follows:

X ≡ P′X′  =^{(20)}  (T_{1} + U_{1})X′
=^{A4,(30),(21)} R_{1}(T_{2} + U_{2})X′ + S_{1}
=^{(30),(32)} R_{1}(R_{2}(T_{3} + U_{3})X′ + S_{2}) + S_{1}
=^{(30),(32)} ⋯
=^{(31),(32)} R_{1}(R_{2}(⋯ (R_{k−1}(R_{k}X′ + S_{k}) + S_{k−1}) ⋯) + S_{2}) + S_{1}
=^{(33)}  R_{1}(R_{2}(⋯ (R_{k−1}(R_{k}shift^{k}(Y) + S_{k}) + S_{k−1}) ⋯) + S_{2}) + S_{1} .

Finally, since R_{i}shift^{i}(Y) + S_{i} =^{MEI1} shift^{i−1}(Y) for i = 1, ..., k, we can apply axiom MEI1 k times in order to reduce this last term to Y. This completes the proof for case 2.2.

∗ Case 2.3. Assume that X ≡ P′(P_{1}, ..., P_{m})^{∗}(Q_{1}, ..., Q_{m}) for some proper derivative P′ of P_{m}, and that Y ≡ R′(R_{1}, ..., R_{n})^{∗}(S_{1}, ..., S_{n}), for some proper derivative R′ of R_{n}. For convenience, put X′ ≡ (P_{1}, ..., P_{m})^{∗}(Q_{1}, ..., Q_{m}) and Y′ ≡ (R_{1}, ..., R_{n})^{∗}(S_{1}, ..., S_{n}). We proceed with the proof by analyzing the equivalence P′X′ \underline{↔} R′Y′ using Lem. 2.5. By symmetry, we may restrict ourselves to considering the following two sub-cases, depending on whether |X′| = |Y′| or |X′| < |Y′|, respectively.

∘ Case 2.3.1. Assume that |X′| = |Y′|. Then an application of Lem. 2.5 yields the equivalences P′ \underline{↔} R′ and X′ \underline{↔} Y′. As L(P′) < L(X) and L(R′) < L(Y) (Lem. 2.7), the inductive hypothesis yields P′ = R′. To conclude the proof for this case, it is therefore sufficient to note that the equality X′ = Y′ follows from X′ \underline{↔} Y′ by case 2.1 of the proof.

∘ Case 2.3.2. Assume that |X′| < |Y′|. Then an application of Lem. 2.5 yields a proper derivative P′′ of P′ such that

P′ \underline{↔} R′P′′
P′′X′ \underline{↔} Y′ .

As L(P′) < L(X) (Lem. 2.7), invariance of L-value under bisimulation (Lem. 2.7) yields L(R′P′′) < L(Y). Then we may apply the inductive hypothesis to deduce the equality P′ = R′P′′. Furthermore, P′′X′ = Y′ follows from the equivalence P′′X′ \underline{↔} Y′ by case 2.2 of the proof. Hence, P′X′ = R′P′′X′ = R′Y′. This completes the proof for case 2.3. As we have examined all the possible forms X, Y ∈ ℍ may take, the proof for case 2 is complete.

We have therefore shown the completeness theorem. □

In light of Lem. 2.4, Thm. 3.12 has the following corollary.

Corollary 3.14 The axiom system E is an ω-complete axiomatization of the algebra T(BPA^{me∗}(A)) modulo bisimulation equivalence.

4 An Expressiveness Hierarchy for Multi-Exit Iteration

As shown in [8], the addition of multi-exit iteration to BPA yields a language that, modulo bisimulation equivalence, is strictly more expressive than that obtained by augmenting BPA with the standard binary Kleene star. For example, if the set of actions A contains at least two elements, then the process (a, a)^{∗}(a, b) cannot be expressed, modulo bisimulation equivalence, in ACP [7], and a fortiori in BPA, enriched with the binary Kleene star (cf. Lem. 3.2.3 in op. cit.).

Let us say that a term of the form (P_{1}, …, P_{m})^{∗}(Q_{1}, …, Q_{n}) has n-exit iteration. By analogy with the aforementioned result from [8], we shall now argue that, in the presence of a countably infinite set of actions, the sequence of k-exit iteration operations induces a hierarchy of super-languages of BPA with a strictly increasing expressive power modulo bisimulation equivalence. To this end, we shall show that, for every positive integer k, there is a process over k + 1 distinct actions that can be specified using (k + 1)-exit iteration, but not using h-exit iteration with h ≤ k.

Before embarking in the proof of this fact, we introduce some notions that will be useful in our argument.

Definition 4.1 A non-empty sequence of transitions

P_{0} →^{α_{1}} P_{1} →^{α_{2}} P_{2} ⋯ →^{α_{n+1}} P_{n+1}

is called a loop from P iff P_{0} ≡ P_{n+1} ≡ P. The termination actions of a term P are those actions a such that P →^{a}✓. Finally, for every k ≥ 1, we write BPA^{k∗} for the set of terms in the language (BPA^{me∗}(A)) that may use h-exit iteration with h ≤ k.

The following lemma provides the key to our expressiveness result.

Lemma 4.2 Let k ≥ 1 and let P be a term in the language BPA^{k∗}. Then every loop from P traverses at most k terms with distinct, non-empty sets of termination actions.

Proof: By structural induction on P. We proceed by a case analysis on the form P may take. The case P ≡ α is obviously vacuous because actions and variables have no loop from them.

• Case: P ≡ Q + R. By Lem. 3.5, if P′ is a proper derivative of P ≡ Q + R, then g(P′) < g(P). Moreover, again by Lem. 3.5, the function g is non-increasing with respect to transitions. It follows that a term of the form Q + R has no loop from it. This case is therefore vacuous.

• Case: P ≡ QR. Consider a loop

P_{0} →^{α_{1}} P_{1} →^{α_{2}} P_{2} ⋯ →^{α_{n+1}} P_{n+1}

from P. Two possibilities may now arise:

1. there exists a loop

Q_{0} →^{α_{1}} Q_{1} →^{α_{2}} Q_{2} ⋯ →^{α_{n+1}} Q_{n+1}

from Q such that P_{i} ≡ Q_{i}R for every i = 0, …, n + 1, or 2. there exist l ∈ {1, …, n} and sequences of transitions

Q ≡ Q_{0} →^{α_{1}} Q_{1} →^{α_{2}} Q_{2} ⋯ Q_{l−1} →^{α_{l}}✓ and R ≡ P_{l} →^{α_{l+1}} P_{l+1} ⋯ →^{α_{n+1}} P_{n+1}

such that P_{i} ≡ Q_{i}R for i = 0, …, l − 1.

If the first possibility applies, then all the terms traversed by the loop from P have no termination actions. If the second applies, then the loop from P traverses exactly the same terms visited by the following loop from R:

R ≡ P_{l} →^{α_{l+1}} P_{l+1} ⋯ →^{α_{n+1}} P_{n+1} ≡ P →^{α_{1}} Q_{1}R →^{α_{2}} Q_{2}R ⋯ Q_{l−1}R →^{α_{l}} R

and the claim follows immediately by induction.

• Case: P ≡ (Q_{1}, …, Q_{m})^{∗}(R_{1}, …, R_{h}), where h ≤ k. Note, first of all, that no proper derivative of any of the terms R_{i} can be traversed by a loop from P (Lem. 3.5). Thus the only terms with non-empty sets of termination actions in loops from P are those of the form shift^{i}(P) for some non-negative integer i. There are at most h terms with this form that have distinct sets of termination actions.

□

As an immediate corollary of the above lemma, we now obtain the following result.

Corollary 4.3 Let k be a positive integer. If the set of actions A contains at least k +1 distinct actions a_{1}, …, a_{k+1}, then the process

a_{1}^{∗}(a_{1}, a_{2}, …, a_{k+1})

cannot be specified in the language BPA^{k∗} modulo bisimulation equivalence.

Proof: Immediate by Lem. 4.2, because the term under consideration has a loop that traverses k + 1 terms with distinct, non-empty sets of termination actions. □

Let now the set of actions A = {a_{1}, a_{2}, …} be countably infinite. By Cor. 4.3, it follows that, for every k ≥ 1, the process

a_{1}^{∗}(a_{1}, a_{2}, …, a_{k+1})

cannot be specified in the language BPA^{k∗} modulo bisimulation equivalence. Thus, for every k ≥ 1, the language BPA^{(k+1)∗} is strictly more expressive than BPA^{k∗} modulo bisimulation equivalence. This establishes the promised expressiveness hierarchy for the collection of languages BPA^{k∗} (k ≥ 1).

References

[1] L. Aceto, W. J. Fokkink, R. van Glabbeek, and A. Ingólfsdóttir, Axiomatizing prefix iteration with silent steps, Research Report RS–95–56, BRICS (Basic Research in Computer Science, Centre of the Danish National Research Foundation), Department of Mathematics and Computer Science, Aalborg University, November 1995. To appear in Information and Computation. Available by anonymous ftp at the address ftp.brics.aau.dk in the directory

    pub/BRICS/RS/95/56.

[2] L. Aceto and J. F. Groote, A complete equational axiomatization for MPA with string iteration, Research Report RS–95–28, BRICS (Basic Research in Computer Science, Centre of the Danish National Research Foundation), Department of Mathematics and Computer Science, Aalborg University, May 1995. Available by anonymous ftp at the address ftp.brics.aau.dk in the directory

pub/BRICS/RS/95/28.

[3] 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 National Research Foundation), Department of Mathematics and Computer Science, Aalborg University, Jan. 1995. To appear in the Proceedings of AMAST ’96. Available by anonymous ftp at the

address ftp.daimi.aau.dk in the directory pub/BRICS/95/5.

[4] J. Baeten, J. Bergstra, and J. Klop, Decidability of bisimulation equivalence for processes generating context-free languages, J. Assoc. Comput. Mach., 40 (1993), pp. 653–682.

[5] J. Baeten and J. Klop, eds., Proceedings CONCUR 90, Amsterdam, vol. 458 of Lecture Notes in Computer Science, Springer-Verlag, 1990.

[6] J. Baeten and C. Verhoef, A congruence theorem for structured operational semantics, in Best [12], pp. 477–492.

[7] J. Baeten and W. Weijland, Process Algebra, Cambridge Tracts in Theoretical Computer Science 18, Cambridge University Press, 1990.

[8] J. Bergstra, I. Bethke, and A. Ponse, Process algebra with iteration, Report CS-R9314, Programming Research Group, University of Amsterdam, 1993. Available by anonymous ftp at the address fwi.uva.nl as

pub/programming-research/reports/1993/P9314.ps.Z.

[9] , Process algebra with iteration and nesting, Computer Journal, 37 (1994), pp. 243–258.

[10] J. Bergstra and J. Klop, Fixed point semantics in process algebras, Report IW 206, Mathematisch Centrum, Amsterdam, 1982.

[11] , Algebra of communicating processes with abstraction, Theoretical Comput. Sci., 37 (1985), pp. 77–121.

[12] E. Best, ed., Proceedings CONCUR 93, Hildesheim, Germany, vol. 715 of Lecture Notes in Computer Science, Springer-Verlag, 1993.

[13] D. Caucal, Graphes canoniques de graphes algébriques, Theoretical Informatics and Applications, 24 (1990), pp. 339–352.

[14] J. H. Conway, Regular algebra and finite machines, Chapman and Hall, 1971.

[15] I. Copi, C. Elgot, and J. Wright, Realization of events by logical nets, J. Assoc. Comput. Mach., 5 (1958), pp. 181–196.

[16] W. J. Fokkink, A complete equational axiomatization for prefix iteration, Inf. Process. Lett., 52 (1994), pp. 333–337.

[17] , On the completeness of the equations for the Kleene star in bisimulation, Logic Group Preprint Series 141, Dept. of Philosophy, Utrecht University, Sept. 1995. To appear in the Proceedings of AMAST ’96. Available by anonymous ftp

from phil.ruu.nl as logic/PREPRINTS/preprint141.ps.

[18] , A complete axiomatization for prefix iteration in branching bisimulation, Fundamenta Informaticae, 26 (1996), pp. 103–113.

[19] W. J. Fokkink and R. van Glabbeek, Ntyft/ntyxt rules reduce to ntree rules, Information and Computation, 126 (1996), pp. 1–10.

[20] W. J. Fokkink and H. Zantema, Basic process algebra with iteration: Completeness of its equational axioms, Computer Journal, 37 (1994), pp. 259–267.

[21] , Prefix iteration in basic process algebra: applying termination techniques, in Proceedings ACP 95, Eindhoven, A. Ponse, C. Verhoef, and B. v. Vlijmen, eds., vol. Report CS-95-14, Eindhoven University of Technology, 1995, pp. 139–156.

[22] R. v. Glabbeek, The linear time – branching time spectrum, in Baeten and Klop [5], pp. 278–297.

[23] , A complete axiomatization for branching bisimulation congruence of finitestate behaviours, in Mathematical Foundations of Computer Science 1993, Gdansk, Poland, A. Borzyszkowski and S. Sokołowski, eds., vol. 711 of Lecture Notes in Computer Science, Springer-Verlag, 1993, pp. 473–484. Available by anonymous

ftp from Boole.stanford.edu.

[24] , The linear time – branching time spectrum II: the semantics of sequential processes with silent moves, in Best [12], pp. 66–81.

[25] J. F. Groote, A new strategy for proving ω–completeness with applications in process algebra, in Baeten and Klop [5], pp. 314–331.

[26] R. Keller, Formal verification of parallel programs, Comm. ACM, 19 (1976), pp. 371–384.

[27] S. Kleene, Representation of events in nerve nets and finite automata, in Automata Studies, C. Shannon and J. McCarthy, eds., Princeton University Press, 1956, pp. 3–41.

[28] D. Kozen, A completeness theorem for Kleene algebras and the algebra of regular events, Information and Computation, 110 (1994), pp. 366–390.

[29] D. Krob, Complete systems of B-rational identities, Theoretical Comput. Sci., 89 (1991), pp. 207–343.

[30] R. Milner, A Calculus of Communicating Systems, vol. 92 of Lecture Notes in Computer Science, Springer-Verlag, 1980.

[31] , A complete inference system for a class of regular behaviours, J. Comput. System Sci., 28 (1984), pp. 439–466.

[32] , Communication and Concurrency, Prentice-Hall International, Englewood Cliffs, 1989.

[33] , A complete axiomatisation for observational congruence of finite-state behaviors, Information and Computation, 81 (1989), pp. 227–247.

[34] D. Park, Concurrency and automata on infinite sequences, in 5^{th} GI Conference, Karlsruhe, Germany, P. Deussen, ed., vol. 104 of Lecture Notes in Computer Science, Springer-Verlag, 1981, pp. 167–183.

[35] D. Perrin, Finite automata, in Handbook of Theoretical Computer Science, J. van Leeuwen, ed., vol. B: Formal Models and Semantics, Elsevier Science Publishers B.V., 1990, ch. 1, pp. 1–57.

[36] G. Plotkin, A structural approach to operational semantics, Report DAIMI FN-19, Computer Science Department, Aarhus University, 1981.

[37] A. Salomaa, Two complete axiom systems for the algebra of regular events, J. Assoc. Comput. Mach., 13 (1966), pp. 158–169.

[38] , Theory of Automata, vol. 100 of International Series of Monographs in Pure and Applied Mathematics (I.N. Sneddon and M. Stark eds.), Pergamon Press, Oxford, 1969.

[39] P. Sewell, Bisimulation is not finitely (first order) equationally axiomatisable, in Proceedings 9^{th} Annual Symposium on Logic in Computer Science, Paris, France, IEEE Computer Society Press, 1994, pp. 62–70.

[40] D. Troeger, Step bisimulation is pomset equivalence on a parallel language without explicit internal choice, Mathematical Structures in Computer Science, 3 (1993), pp. 25–62.

Recent Publications in the BRICS Report Series

RS-96-22 Luca Aceto and Wan J. Fokkink. An Equational Axiomatization for Multi-Exit Iteration. June 1996. 30 pp.

RS-96-21 Dany Breslauer, Tao Jiang, and Zhigen Jiang. Rotation of Periodic Strings and Short Superstrings. June 1996. 14 pp.

RS-96-20 Olivier Danvy and Julia L. Lawall. Back to Direct Style II: First-Class Continuations. June 1996. 36 pp. A preliminary version of this paper appeared in the proceedings of the 1992 ACM Conference on Lisp and Functional Programming, William Clinger, editor, LISP Pointers, Vol. V, No. 1, pages 299�310, San Francisco, California, June 1992. ACM Press.

RS-96-19 John Hatcliff and Olivier Danvy. Thunks and the λ-Calculus. June 1996. 22 pp. To appear in Journal of Functional Programming.

RS-96-18 Thomas Troels Hildebrandt and Vladimiro Sassone. Comparing Transition Systems with Independence and Asynchronous Transition Systems. June 1996. 14 pp. To appear inConcurrency Theory: 7th International Conference, CONCUR ’96 Proceedings, LNCS, 1996.

RS-96-17 Olivier Danvy, Karoline Malmkj�r, and Jens Palsberg. Eta-Expansion Does The Trick (Revised Version). May 1996. 30 pp. To appear in ACM Transactions on Programming Languages and Systems (TOPLAS).

RS-96-16 Lisbeth Fajstrup and Martin Rau�en. Detecting Deadlocks in Concurrent Systems. May 1996. 10 pp.

RS-96-15 Olivier Danvy. Pragmatic Aspects of Type-Directed Partial Evaluation. May 1996. 27 pp.

RS-96-14 Olivier Danvy and Karoline Malmkj�r. On the Idempotence of the CPS Transformation. May 1996. 15 pp.

RS-96-13 Olivier Danvy and Ren� e Vestergaard. Semantics-Based Compiling: A Case Study in Type-Directed Partial Evaluation. May 1996. 28 pp.