BRICS

Basic Research in Computer Science

A Finite Equational Base for CCS with Left Merge and Communication Merge

Luca Aceto Willem Jan Fokkink Anna Ingólfsdóttir Bas Luttik

BRICS Report Series RS-06-6

ISSN 0909-0878 March 2006 BRICS RS-06-6 Aceto et al.: A Finite Equational Base for CCS with Left Merge and Communication Merge Copyright \begin{matrix}c \\ ◯ \end{matrix} 2006, Luca Aceto & Willem Jan Fokkink & Anna

Ingólfsdóttir & Bas Luttik. 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 BRICS Report Series publications. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus IT-parken, Aabogade 34 DK–8200 Aarhus N Denmark

Telephone: +45 8942 9300
Telefax: +45 8942 5601
Internet: BRICS@brics.dk

BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:

http://www.brics.dk
ftp://ftp.brics.dk

This document in subdirectory RS/06/6/

A finite equational base for CCS with left merge and communication merge

Luca Aceto^{1,4}, Wan Fokkink^{2,5}, Anna Ingolfsdottir^{1,4}, and Bas Luttik^{3,5}

1 Department of Computer Science, Reykjavík University, Iceland, luca@ru.is,annai@ru.is

2 Department of Computer Science, Vrije Universiteit Amsterdam, The Netherlands,

                                    wanf@cs.vu.nl

3 Department of Mathematics and Computer Science, Technische Universiteit Eindhoven,

                          The Netherlands, s.p.luttik@tue.nl

4 BRICS, Department of Computer Science, Aalborg University, Denmark 5 Department of Software Engineering, CWI, The Netherlands

Abstract. Using the left merge and communication merge from ACP, we present an equational base for the fragment of CCS without restriction and relabelling. Our equational base is finite if the set of actions is finite.

1 Introduction

One of the first detailed studies of the equational theory of a process algebra was performed by Hennessy and Milner [9]. They considered the equational theory of the process algebra that arises from the recursion-free fragment of CCS (see [11]), and presented a set of equational axioms that is complete in the sense that all valid closed equations (i.e., equations in which no variables occur) are derivable from it in equational logic [15]. For the elimination of parallel composition from closed terms, Hennessy and Milner proposed the well-known Expansion Law, an axiom schema that generates infinitely many axioms. Thus, the question arose whether a finite complete set of axioms exists. With their axiom system ACP, Bergstra and Klop demonstrated in [3] that it does exist if two auxiliary operators are used: the left merge and the communication merge. It was later proved by Moller [13] that without using at least one auxiliary operator a finite complete set of axioms does not exist.

The aforementioned results pertain to the closed fragments of the equational theories discussed, i.e., to the subsets consisting of the closed valid equations only. Many valid equations such as, e.g., the equation (x ∥ y) ∥ z ≈ x ∥ (y ∥ z) expressing that parallel composition is associative, are not derivable (by means of equational logic) from the axioms in [3] or [9]. In this paper we shall not neglect the variables and contribute to the study of full equational theories of process algebras. We take the fragment of CCS without recursion, restriction and relabelling, and consider the full equational theory of the process algebra that is obtained by taking the syntax modulo bisimilarity [14]. Our goal is then to present an equational base (i.e., a set of valid equations from which every other valid equation can be derived) for it, which is finite if the set of actions is finite. Obviously, Moller’s result about the unavoidability of the use of auxiliary operations in a finite complete axiomatisation of the closed fragment of the equational theory of CCS a fortiori implies that auxiliary operations are needed to achieve our goal. So we add left merge and communication merge from the start.

Moller [12] considers the equational theory of the same fragment of CCS, except that his parallel operator implements pure interleaving instead of CCS-communi-cation and the communication merge is omitted. He presents a set of valid axiom schemata and proves that it generates an equational base if the set of actions is infinite. Groote [6] does consider the fragment including communication merge, but, instead of the CCS-communication mechanism, he assumes an uninterpreted communication function. His axiom schemata also generate an equational base provided that the set of actions is infinite. We improve on these results by considering the communication mechanism present in CCS, and by proving that our axiom schemata generate an equational base also if the set of actions is finite. Moreover, our axiom schemata generate a finite equational base if the set of actions is finite.

Our equational base consists of axioms that are mostly well-known. For parallel composition (∥), left merge (∥ ) and communication merge (|) we adapt the axioms of ACP, adding from Bergstra and Tucker [4] a selection of the axioms for standard concurrency and the axiom (x | y) | z ≈ 0, which expresses that the communication mechanism is a form of handshaking communication.

Our proof follows the classic two-step approach: first identify a set of normal forms such that every process term has a provably equal normal form, and then demonstrate that for distinct normal forms there is a distinguishing valuation that proves that they should not be equated. (We refer to the survey [2] for a discussion of proof techniques and an overview of results and open problems in the area. We remark in passing that one of our main results in this paper, viz. Corollary 34, solves the open problem mentioned in [2, p. 362].) Since both associating a normal form with a process term and determining a distinguishing valuation for two distinct normal forms are easily seen to be computable, as a corollary to our proof we get the decidability of the equational theory. Another consequence of our result is that our equational base is complete for the set of valid closed equations as well as ω-complete [7].

The positive result that we obtain in Corollary 34 of this paper stands in contrast with the negative result that we have obtained in [1]. In that article we proved that there does not exist a finite equational base for CCS if the auxiliary operation |^{/} of Hennessy [8] is added instead of Bergstra and Klop’s left merge and communication merge. Furthermore, we conjecture that a finite equational base fails to exist if the unary action prefixes are replaced by binary sequential composition. (We refer to [2] for an infinite family of valid equations that we believe cannot all be derivable from a single finite set of valid equations.)

The paper is organised as follows. In Sect. 2 we introduce a class of algebras of processes arising from a process calculus à la CCS, present a set of equations that is valid in all of them, and establish a few general properties needed in the remainder of the paper. Our class of process algebras is parametrised by a communication function. It is beneficial to proceed in this generality, because it allows us to first consider the simpler case of a process algebra with pure interleaving (i.e., no communication at all) instead of CCS-like parallel composition. In Sect. 3 we prove that an equational base for the process algebra with pure interleaving is obtained by simply adding the axiom x | y ≈ 0 to the set of equations introduced in Sect. 2. The proof in Sect. 3 extends nicely to a proof that for the more complicated case of CCS-communication it is enough to replace x | y ≈ 0 by x | (y | z) ≈ 0; this is discussed in Sect. 4.

2 Algebras of processes

We fix a set A of actions, and declare a special action τ that we assume is not in A. We denote by A_{τ} the set A ∪ {τ}. Generally, we let a and b range over A and α over A_{τ}. We also fix a countably infinite set V of variables. The set P of process terms is generated by the following grammar:

P ::= x | 0 | α.P | P + P | P ∥ P | P | P | P ∥ P ,

with x ∈ V, and α ∈ A_{τ}. We shall frequently simply write α instead of α.0. Furthermore, to be able to omit some parentheses when writing terms, we adopt the convention that α. binds stronger, and + binds weaker, than all the other operations.

Table 1. The operational semantics.

\overline{α.P ⟶^{α} P} \frac{P ⟶^{α} P′}{P + Q ⟶^{α} P′}  \frac{Q ⟶^{α} Q′}{P + Q ⟶^{α} Q′}

\frac{P ⟶^{α} P′}{P ∥ Q ⟶^{α} P′ ∥ Q} \frac{P ⟶^{α} P′}{P ∥ Q ⟶^{α} P′ ∥ Q} \frac{Q ⟶^{α} Q′}{P ∥ Q ⟶^{α} P ∥ Q′}

\frac{P ⟶^{a} P′, Q ⟶^{b} Q′, γ(a, b)↓}{P | Q ⟶^{γ(a,b)} P′ ∥ Q′}  \frac{P ⟶^{a} P′, Q ⟶^{b} Q′, γ(a, b)↓}{P ∥ Q ⟶^{γ(a,b)} P′ ∥ Q′}

A process term is closed if it does not contain variables; we denote the set of all closed process terms by P_{0}. We define on P_{0} binary relations ⟶^{α} (α ∈ A_{τ}) by means of the transition system specification in Table 1. The last two rules in Table 1 refer to a communication function γ, i.e., a commutative and associative partial binary function γ : A × A ⇀ A_{τ}. We shall abbreviate the statement ‘γ(a, b) is defined’ by γ(a, b)↓ and the statement ‘γ(a, b) is undefined’ by γ(a, b)↑. In the remainder of this paper we shall in particular consider the following communication functions:

1. The trivial communication function is the partial function f : A × A ⇀ A_{τ} such that f(a, b)↑ for all a, b ∈ A.

2. The CCS communication function h : A × A ⇀ A_{τ} presupposes a bijection ¯. on A such that \overline{\overline{a}} = a and \overline{a} ≠ a for all a ∈ A, and is then defined by h(a, b) = τ if \overline{a} = b and undefined otherwise.

Definition 1. A bisimulation is a symmetric binary relation R on P_{0} such that P R Q implies

if P ⟶^{α} P′, then there exists Q′ ∈ P_{0} such that Q ⟶^{α} Q′ and P′ R Q′.  (1)

Closed process terms P, Q ∈ P_{0} are said to be bisimilar (notation: P \underline{↔}_{γ} Q) if there exists a bisimulation R such that P R Q.

The relation \underline{↔}_{γ} is an equivalence relation on P_{0}; we denote the equivalence class containing P by [P], i.e.,

[P] = \{Q ∈ P_{0} : P \underline{↔}_{γ} Q\} .

The rules in Table 1 are all in de Simone’s format [5] if P, P′, Q and Q′ are treated as variables ranging over closed process terms, and if the last two rules are treated as rule schemata generating a rule for every a, b such that γ(a, b)↓. Hence, \underline{↔}_{γ} has the substitution property for the syntactic constructs of our language of closed process terms, and therefore the constructs induce an algebraic structure on P_{0}/\underline{↔}_{γ}, with a constant 0, unary operations α. (α ∈ A_{τ}) and four binary operations +, ∥ , | and ∥ defined by

0 = [0]  [P] ∥ [Q] = [P ∥ Q]
α.[P] = [α.P]  [P] | [Q] = [P | Q]
[P] + [Q] = [P + Q]  [P] ∥ [Q] = [P ∥ Q] .

Henceforth, we denote by P_{γ} (for γ an arbitrary communication function) the algebra obtained by dividing out \underline{↔}_{γ} on P_{0} with constant 0 and operations α. (α ∈ A_{τ}), +, ∥ , |, and ∥ as defined above. The elements of P_{γ} are called processes, and will be ranged over by p, q and r.

2.1 Equational reasoning

We can use the full language of process expressions to reason about the elements of P_{γ}. A valuation is a mapping ν : V → P_{γ}; it induces an evaluation mapping

[[ ]]_{ν} : P → P_{γ}

inductively defined by

[[x]]_{ν} = ν(x)  [[P ∥ Q]]_{ν} = [[P]]_{ν} ∥ [[Q]]_{ν}
[[0]]_{ν} = 0  [[P | Q]]_{ν} = [[P]]_{ν} | [[Q]]_{ν}
[[α.P]]_{ν} = α.[[P]]_{ν}  [[P ∥ Q]]_{ν} = [[P]]_{ν} ∥ [[Q]]_{ν}

[[P + Q]]_{ν} = [[P]]_{ν} + [[Q]]_{ν}.

A process equation is a formula P ≈ Q with P and Q process terms; it is said to be valid (in P_{γ}) if [[P]]_{ν} = [[Q]]_{ν} for all ν : V → P_{γ}. If P ≈ Q is valid in P_{γ}, then we shall also write P \underline{↔}_{γ} Q. The equational theory of the algebra P_{γ} is the set of all valid process equations, i.e.,

EqTh(P_{γ}) = {P ≈ Q : [[P]]_{ν} = [[Q]]_{ν} for all ν : V → P_{γ}} .

The precise contents of the set EqTh(P_{γ}) depend to some extent on the choice of γ. For instance, the process equation x | y ≈ 0 is only valid in P_{γ} if γ is the trivial communication function f; if γ is the CCS communication function h, then P_{γ} satisfies the weaker equation x | (y | z) ≈ 0.

Table 2. Process equations valid in every P_{γ}.

A1 x + y  ≈ y + x
A2 (x + y) + z ≈ x + (y + z)
A3 x + x  ≈ x
A4 x + 0  ≈ x
L1 0 ∥ x  ≈ 0
L2 α.x ∥ y  ≈ α.(x ∥ y)
L3 (x + y) ∥ z ≈ x ∥ z + y ∥ z
L4 (x ∥ y) ∥ z ≈ x ∥ (y ∥ z)
L5 x ∥ 0  ≈ x

C1 0 | x  ≈ 0
C2 a.x | b.y ≈ γ(a, b).(x ∥ y) if γ(a, b)↓
C3 a.x | b.y ≈ 0  if γ(a, b)↑
C4 (x + y) | z ≈ x | z + y | z
C5 x | y  ≈ y | x
C6 (x | y) | z ≈ x | (y | z)
C7 (x ∥ y) | z ≈ (x | z) ∥ y
P1 x ∥ y  ≈ (x ∥ y + y ∥ x) + x | y

Table 2 lists process equations that are valid in P_{γ} independently of the choice of γ. (The equations L2, C2 and C3 are actually axiom schemata; they generate an axiom for all a, b ∈ A. Note that if A is finite, then these axiom schemata generate finitely many axioms.) Henceforth whenever we write an equation P ≈ Q, we shall mean that it is derivable from the axioms in Table 2 by means of equational logic. It is well-known that the rules of equational logic preserve validity. We therefore obtain the following result.

Proposition 2. For all process terms P and Q, if P ≈ Q, then P \underline{↔}_{γ} Q.

In the following lemma we give an example of a valid equation that can be derived from Table 2 using the rules of equational logic.

Lemma 3. The following equation is derivable from the axioms in Table 2:

C8 (x ∥ y) | (z ∥ u) ≈ (x | z) ∥ (y ∥ u) .

Proof. The lemma is proved with the derivation:

(x ∥ y) | (z ∥ u) ≈ (z ∥ u) | (x ∥ y)  (by C5)
≈ (z | (x ∥ y)) ∥ u  (by C7)
≈ ((x ∥ y) | z) ∥ u  (by C5)
≈ ((x | z) ∥ y) ∥ u  (by C7)
≈ (x | z) ∥ (y ∥ u)  (by L4).
⊓ ⊔

A set of valid process equations is an equational base for P_{γ} if all other valid process equations are derivable from it by means of equational logic. Clearly, P_{γ} has EqTh(P_{γ}) as an equational base, but it is infinite, and offers little insight into the nature of the equations valid in P_{γ}. The purpose of this paper is to prove that if we add to the equations in Table 2 the equation x | y ≈ 0 we obtain an equational base for P_{f}, and if, instead, we add x | (y | z) ≈ 0 we obtain an equational base for P_{h}. Both these equational bases are finite, if the set of actions A is finite.

Definition 4. Let P be a process term. We define the height of a process term P, denoted h(P), inductively as follows:

\begin{matrix}h(0) = 0 , \\ h(x) = 1 , \\ h(α.P) = h(P) + 1 , \\ h(P + Q) = max(h(P), h(Q)) . \end{matrix}  \begin{matrix}h(P ∥ Q) = h(P) + h(Q) , \\ h(P | Q) = h(P) + h(Q) , \\ h(P ∥ Q) = h(P) + h(Q) , \end{matrix}

Definition 5. We call a process term simple if it is not 0 and not an alternative composition.

Lemma 6. For every process term P there exists a sequence of simple process terms S_{1}, …, S_{n} (n ≥ 0) such that h(P) ≥ h(S_{i}) for all i = 1, …, n and

P ≈ ∑_{i=1}^{n} S_{i} (by A1, A2 and A4).

We postulate that the summation of an empty sequence of terms denotes 0. The terms S_{i} will be called syntactic summands of P.

2.2 General properties of P_{γ}

We collect some general properties of the algebras P_{γ} that we shall need in the remainder of the paper.

The binary transition relations ⟶^{α} (α ∈ A_{τ}) on P_{0}, which were used to associate an operational semantics with closed process terms, will play an important rôle in the remainder of the paper. They induce binary relations on P_{γ}, also denoted by ⟶^{α}, and defined as the least relations such that P ⟶^{α} P′ implies [P] ⟶^{α} [P′]. Note that we then get, directly from the definition of bisimulation, that for all P, P′ ∈ P_{0}:

[P] ⟶^{α} [P′] iff for all Q ∈ [P] there exists Q′ ∈ [P′] such that Q ⟶^{α} Q′.

Proposition 7. For all p, q, r ∈ P_{γ}:

(a) p = 0 iff there do not exist p′ ∈ P_{γ} and α ∈ A_{τ} such that p ⟶^{α} p′;

(b) α.p ⟶^{β} r iff α = β and r = p;

(c) p + q ⟶^{α} r iff p ⟶^{α} r or q ⟶^{α} r;

(d) p ∥ q ⟶^{α} r iff there exists p′ ∈ P_{γ} such that p ⟶^{α} p′ and r = p′ ∥ q; and

(e) p | q ⟶^{α} r iff there exist actions a, b ∈ A and processes p′, q′ ∈ P_{γ} such that

α = γ(a, b), p ⟶^{a} p′, q ⟶^{b} q′, and r = p′ ∥ q′; and

(f) p ∥ q ⟶^{α} r iff p ∥ q ⟶^{α} r or q ∥ p ⟶^{α} r or p | q ⟶^{α} r.

Let p, p′ ∈ P_{γ}; we write p → p′ if p ⟶^{α} p′ for some α ∈ A_{τ}. We denote by →^{∗} the reflexive-transitive closure of →. If p and p′ are processes such that p → p′, then we call p′ a residual of p.

It is easy to see from Table 1 that if P ⟶^{α} P′, then P′ has fewer symbols than P. Consequently, the length of a transition sequence starting with a process [P] is bounded from above by the number of symbols in P.

Definition 8. The depth |p| of an element p ∈ P_{γ} is defined as

|p| = max{n ≥ 0 : ∃p_{n}, …, p_{0} ∈ P_{γ} s.t. p = p_{n} → ⋯ → p_{0}}.

The branching degree bdeg(p) of an element p ∈ P_{γ} is defined as

bdeg(p) = |{(α, p′) : p ⟶^{α} p′}| .

For the remainder of this section, we focus on properties of parallel composition on P_{γ}. The depth of a parallel composition is the sum of the depths of its components.

Lemma 9. For all p, q ∈ P_{γ}, |p ∥ q| = |p| + |q|.

Proof. If p = p_{m} → ⋯ → p_{0} and q = q_{n} → ⋯ → q_{0}, then

p ∥ q = p_{m} ∥ q → ⋯ → p_{0} ∥ q = p_{0} ∥ q_{n} → ⋯ → p_{0} ∥ q_{0} ,

so clearly |p ∥ q| ≥ |p| + |q|.

It remains to prove that |p| + |q| ≥ |p ∥ q|. We proceed by induction on the depth of p ∥ q. If |p ∥ q| = 0, then (p ∥ q)↛, so p↛ and q↛; hence |p| = 0 and |q| = 0, and it follows that |p ∥ q| = |p| + |q|. Suppose that |p ∥ q| = n + 1. Then there exist r_{n+1}, …, r_{0} ∈ P_{γ} such that

p ∥ q = r_{n+1} → r_{n} → ⋯ → r_{0} .

Note that |r_{i}| = i for all 0 ≤ i ≤ n + 1. Further note that the transition r_{n+1} → r_{n} cannot be the result r_{n+1} ⟶^{γ(a,b)} r_{n} of communication between a transition p ⟶^{a} p′ and a transition q ⟶^{b} q′; for then there would exist a longer transition sequence from p ∥ q, obtained by replacing the single transition r_{n+1} → r_{n} by two transitions r_{n+1} = p ∥ q → p′ ∥ q → p′ ∥ q′ = r_{n}, contradicting our assumption that |p ∥ q| = n + 1. Hence, either r_{n} = p′ ∥ q with p → p′, or r_{n} = p ∥ q′ with q → q′. In the first case it follows by the induction hypothesis that |p′| + |q| ≥ |p′ ∥ q| = n, so |p| + |q| ≥ |p′| + |q| + 1 ≥ n + 1 = |p ∥ q|. In the second case the proof is similar. ⊓ ⊔

According to the following lemma and Proposition 2, P_{γ} is a commutative monoid with respect to ∥, with 0 as the identity element.

Lemma 10. The following equations are derivable from the axioms in Table 2:

\begin{matrix}P2 & (x ∥ y) ∥ z ≈ & x ∥ (y ∥ z) \\ P3 & x ∥ y  ≈ & y ∥ x \\ P4 & x ∥ 0  ≈ & x . \end{matrix}

An element p ∈ P_{γ} is parallel prime if p ≠ 0, and p = q ∥ r implies q = 0 or r = 0. Suppose that p is an arbitrary element of P_{γ}; a parallel decomposition of p is a finite multiset [p_{1}, …, p_{n}] of parallel primes such that p = p_{1} ∥ ⋯ ∥ p_{n}. (The process 0 has as decomposition the empty multiset, and a parallel prime process p has as decomposition the singleton multiset [p].) The following theorem is a straightforward consequence of the main result in [10].

Theorem 11. Every element of P_{γ} has a unique parallel decomposition.

Proof. In a similar way as in [10, Sect. 4] it can be established that the inverse of →^{∗} is a decomposition order on the commutative monoid P_{γ} with respect to parallel composition; it then follows from [10, Theorem 32] that this commutative monoid has unique decomposition. ⊓ ⊔

The following corollary is a straightforward consequence of the above unique decomposition result.

Corollary 12 (Cancellation). Let p, q, r ∈ P_{γ}. If p ∥ q = p ∥ r, then q = r.

The branching degree of a parallel composition is at least the branching degree of its components.

Lemma 13. For all p, q ∈ P_{γ}, bdeg(p ∥ q) ≥ bdeg(p), bdeg(q).

Proof. First we prove that bdeg(p ∥ q) ≥ bdeg(q). By Proposition 7, if q ⟶^{α} q′, then p ∥ q ⟶^{α} p ∥ q′. Suppose that q_{1} and q_{2} are distinct processes such that q ⟶^{α} q_{1}

and q ⟶^{α} q_{2}. Then p ∥ q ⟶^{α} p ∥ q_{1} and p ∥ q ⟶^{α} p ∥ q_{2}. Since p ∥ q_{1} = p ∥ q_{2} would

imply q_{1} = q_{2} by Corollary 12, it follows that p ∥ q′ and p ∥ q′′ are distinct. Hence bdeg(p ∥ q) ≥ bdeg(q).

By commutativity of ∥, it also follows that bdeg(p ∥ q) ≥ bdeg(p). ⊓ ⊔

We define a sequence of parallel prime processes with special properties that make them very suitable as tools in our proofs in the remainder of the paper:

φ_{i} = τ.0 + ⋯ + τ^{i}.0  (i ≥ 1)  (2)

(with τ^{i}.0 recursively defined by τ^{i}.0 = 0 if i = 0, and τ.τ^{i−1}.0 if i > 0).

Lemma 14. (i) For all i ≥ 1, the processes φ_{i} are parallel prime. (ii) The processes φ_{i} are all distinct, i.e., φ_{k} = φ_{l} implies that k = l. (iii) For all i ≥ 1, the process φ_{i} has branching degree i.

Proof. (i) Clearly φ_{i} ≠ 0. Suppose φ_{i} = p ∥ q; to prove that φ_{i} is parallel prime, we need to establish that either p = 0 or q = 0. Note that p ∥ q ⟶^{τ} 0. There do not exist actions a and b and processes p′ and q′ such that γ(a, b) = τ and p′ ∥ q′, for then also p ∥ q ⟶^{a} p′ ∥ q, quod non. Therefore, according to Proposition 7, there are only two cases to consider:

(a) If there exists p′ such that p ⟶^{τ} p′ and p′ ∥ q = 0, then it follows by Lemma 9 that |q| = 0, and hence q = 0.

(b) If there exists q′ such that q ⟶^{τ} q′ and p ∥ q′ = 0, then it follows by Lemma 9

that |p| = 0, and hence p = 0. (ii) If φ_{k} = φ_{l}, then k = |φ_{k}| = |φ_{l}| = l. (iii) On the one hand, φ_{i} ⟶^{τ} τ^{j}.0 for all 0 ≤ j < i and τ^{k}.0 = τ^{l}.0 implies k = l

for all 0 ≤ k, l < i, so bdeg(φ_{i}) is at least i. On the other hand, if φ_{i} ⟶^{α} p, then α = τ and p = τ^{j}.0 for some 0 ≤ j < i, so bdeg(φ_{i}) is at most i. ⊓ ⊔

3 An equational base for P_{f}

In this section, we prove that an equational base for P_{f} is obtained if we add the axiom

F x | y ≈ 0

to the set of axioms generated by the axiom schemata in Table 2. The resulting equational base is finite if A is finite.

Henceforth, whenever we write P ≈_{F} Q, we shall mean that the equation P ≈ Q is derivable from the axioms in Table 2 and the axiom F.

Proposition 15. For all process terms P and Q, if P ≈_{F} Q, then P \underline{↔}_{f} Q.

To prove that adding F to the axioms in Table 2 suffices to obtain an equational base for P_{f}, we need to establish that P \underline{↔}_{f} Q implies P ≈_{F} Q for all process terms P and Q. We adopt the classic two step approach [2]:

1. In the first step we identify a set of normal forms N_{F}, and prove that every process term P can be rewritten to a normal form by means of the axioms.

2. In the second step we prove that bisimilar normal forms are identical modulo applications of the axioms A1–A4. This is done by associating with every pair of normal forms a so-called distinguishing valuation, i.e., a valuation that proves that the normal forms are not bisimilar unless they are provably equal modulo the axioms A1–A4.

Definition 16. The set N_{F} of F-normal forms is generated by the following grammar:

N ::= 0 | N + N | α.N | x ∥ N ,

with x ∈ V, and α ∈ A_{τ}.

Note that the set of simple F-normal forms (see Definition 5) is generated by the grammar

S ::= α.N | x ∥ N ,

with x ∈ V, α ∈ A_{τ}, and N ∈ N_{F}.

Lemma 17. For every process term P there is an F-normal form N such that P ≈_{F} N and h(P) ≥ h(N).

Proof. Recall that h(P) denotes the height of P (see Definition 4). In this proof we also use another syntactic measure on P: the length of P, denoted ℓ(P), is the number of symbols occurring in P. Define a partial order ≺ on process terms by P ≺ Q if the pair (h(P), ℓ(P)) is less than the pair (h(Q), ℓ(Q)) in the lexicographical order on ω ×ω; i.e., P ≺ Q if h(P) < h(Q) or h(P) = h(Q) and ℓ(P) < ℓ(Q). It is well-known that the lexicographical order on ω × ω, and hence the order ≺ on process terms, is well-founded; so we may use ≺-induction.

The remainder of the proof consists of a case distinction on the syntactic forms that P may take.

1. If P is a variable, say P = x, then P ≈ x ∥ 0 by L5; the process term x ∥ 0 is an F-normal form and h(P) = h(x) = h(x) + 0 = h(x ∥ 0).

2. If P = 0, then P is an F-normal form.

3. If P = α.P′, then, since h(P′) < h(P), it holds that P′ ≺ P, and hence by the induction hypothesis there exists an F-normal form N such that P′ ≈_{F} N and h(P′) ≥ h(N). Then α.N is an F-normal form such that P ≈_{F} α.N and h(P) ≥ h(α.N).

4. If P = P_{1} + P_{2}, then, since h(P_{1}), h(P_{2}) ≤ h(P) and ℓ(P_{1}), ℓ(P_{2}) < ℓ(P), it holds that P_{1}, P_{2} ≺ P, and hence by the induction hypothesis there exist Fnormal forms N_{1} and N_{2} such that P_{1} ≈_{F} N_{1}, P_{2} ≈_{F} N_{2}, h(P_{1}) ≥ h(N_{1}) and h(P_{2}) ≥ h(N_{2}). Then N_{1} + N_{2} is an F-normal form such that P ≈_{F} N_{1} + N_{2} and h(P) ≥ h(N_{1} + N_{2}).

5. If P = Q ∥ R, then, since h(Q) ≤ h(P) and ℓ(Q) < ℓ(P), it holds that Q ≺ P, and hence by the induction hypothesis and Lemma 6 there exists a sequence S_{1}, …, S_{n} of simple F-normal forms such that Q ≈_{F} ∑_{i=1}^{n} S_{i} and h(Q) ≥ h(S_{i}) for all i = 1, …, n. If n = 0, then P ≈_{F} 0∥ R ≈ 0 by L1, and clearly h(P) ≥ h(0). Otherwise, by L3

P ≈_{F} ∑_{i=1}^{n}(S_{i} ∥ R) .

So it remains to show, for all i = 1, …, n, that S_{i} ∥ R is provably equal to an appropriate F-normal form. We distinguish cases according to the syntactic form of S_{i}:

(a) If S_{i} = α.N′_{i}, with N′_{i} an F-normal form, then by L2

S_{i} ∥ R ≈ α.(N′_{i} ∥ R) .

Since h(N′_{i}) < h(S_{i}) ≤ h(Q), it holds that N′_{i} ∥ R ≺ P and hence by the induction hypothesis there exists an F-normal form N_{i} such that N′_{i} ∥ R ≈_{F} N_{i} and h(N′_{i} ∥ R) ≥ h(N_{i}). Clearly, α.N_{i} is an F-normal form such that S_{i} ∥ R ≈_{F} α.N_{i} and h(S_{i} ∥ R) ≥ h(α.N_{i}).

(b) If S_{i} = x ∥ N′_{i}, with N′_{i} an F-normal form, then by L4

(x ∥ N′_{i}) ∥ R ≈ x ∥ (N′_{i} ∥ R) .

Note that h(x) = 1, so h(N′_{i}) < h(S_{i}) ≤ h(Q). It follows that N′_{i} ∥ R ≺ P, and hence by the induction hypothesis there exists an F-normal form N_{i} such that N′_{i} ∥ R ≈_{F} N_{i} and h(N′_{i} ∥ R) ≥ h(N_{i}). Clearly, x ∥ N_{i} is an F-normal form such that S_{i} ∥ R ≈_{F} x ∥ N_{i} and h(S_{i} ∥ R) ≥ h(x ∥ N_{i}).

6. If P = Q | R, then P ≈_{F} 0 according to the axiom F and clearly h(P) ≥ h(0).

7. If P = Q∥ R, then P ≈ (Q∥ R+R∥ Q)+Q| R ≈_{F} Q∥ R+R∥ Q by the axioms P1, F and A4. We can now proceed as in case 5 to show that for Q∥ R and R∥ Q there exist F-normal forms N_{1} and N_{2}, respectively, such that Q ∥ R ≈_{F} N_{1}, R ∥ Q ≈_{F} N_{2}, h(Q ∥ R) ≥ h(N_{1}) and h(R ∥ Q) ≥ h(N_{2}). Then N_{1} + N_{2} is an F-normal form such that P ≈_{F} N_{1} + N_{2} and h(P) ≥ h(N_{1} + N_{2}). ⊓ ⊔

It remains to prove that for every two F-normal forms N_{1} and N_{2} there exists a distinguishing valuation, i.e., a valuation ∗ such that if N_{1} and N_{2} are not provably equal, then the ∗-interpretations of N_{1} and N_{2} are distinct. Stating it contrapositively, for every two F-normal forms N_{1} and N_{2}, it suffices to establish the existence of a valuation ∗ : V → P_{γ} such that

if [[N_{1}]]_{∗} = [[N_{2}]]_{∗}, then N_{1} ≈_{F} N_{2}. (3)

The valuation ∗ : V → P_{f} that we are going to define below will depend on N_{1} and N_{2}. The idea is that ∗ assigns processes to variables in such a way that much of the original syntactic structure of N_{1} and N_{2} can be recovered by analysing the behaviour of [[N_{1}]]_{∗} and [[N_{2}]]_{∗}. To recognize variables, we shall use the special processes φ_{i} (i ≥ 1) defined in Eqn. (2) on p. 8. Recall that the processes φ_{i} have branching degree i. We are going to assign to every variable a distinct process φ_{i}. By choosing i larger than the maximal ‘branching degrees’ occurring in N_{1} and N_{2}, the behaviour contributed by an instantiated variable is distinguished from behaviour already present in the F-normal forms themselves.

Definition 18. We define the width w(N) of an F-normal form N as follows:

(i) if N = 0, then w(N) = 0; (ii) if N = N_{1} + N_{2}, then w(N) = w(N_{1}) + w(N_{2}); (iii) if N = α.N′, then w(N) = max(w(N′), 1); (iv) if N = x ∥ N′, then w(N) = max(w(N′), 1).

We now fix a natural number W and use it to define a valuation ∗ that satisfies Eqn. (3) for all F-normal forms N_{1} and N_{2} such that w(N_{1}), w(N_{2}) ≤ W (as we shall prove in Theorem 22 below). Note that, since we are allowed to choose a different W for each pair of F-normal forms N_{1} and N_{2}, it follows that for each such pair there indeed exists a distinguishing valuation.

Let ⌜⌝ denote an injective function

⌜⌝ : V → {n ∈ ω : n > W }

that associates with every variable a unique natural number greater than W. We define the valuation ∗ : V → P_{γ} for all x ∈ V by

∗(x) = τ.φ_{⌜x⌝} .

The τ-prefix is to ensure the following property for all normal forms (not just N_{1} and N_{2}).

Lemma 19. For every F-normal form N, the branching degree of [[N]]_{∗} is at most w(N).

Proof. Structural induction on N. ⊓ ⊔

Lemma 20. Let S be a simple F-normal form, let α ∈ A_{τ}, and let p be a process such that [[S]]_{∗} ⟶^{α} p. Then the following statements hold:

(i) if S = β.N, then α = β and p = [[N]]_{∗}; (ii) if S = x ∥ N, then α = τ and p = φ_{⌜x⌝} ∥ [[N]]_{∗}.

An important property of ∗ is that it allows us to distinguish the different types of simple F-normal forms by classifying their residuals according to the number of parallel components with a branching degree that exceeds W. Let us say that a process p is of type n (n ≥ 0) if its unique parallel decomposition contains precisely n parallel prime components with a branching degree > W.

Corollary 21. Let S be a simple F-normal form such that w(S) ≤ W.

(i) If S = α.N, then the unique residual [[N]]_{∗} of [[S]]_{∗} is of type 0. (ii) If S = x ∥ N, then the unique residual φ_{⌜x⌝} ∥ [[N]]_{∗} of [[S]]_{∗} is of type 1.

Proof. On the one hand, by Lemma 19, in both cases [[N]]_{∗} has a branching degree of at most w(N) ≤ w(S) ≤ W, and hence, by Lemma 13, its unique parallel decomposition cannot contain parallel prime components with a branching degree that exceeds W. On the other hand, by Lemmas 14(i) and 14(iii), the process φ_{⌜x⌝} is parallel prime and has a branching degree that exceeds W. So [[N]]_{∗} is of type 0, and φ_{⌜x⌝} ∥ [[N]]_{∗} is of type 1. ⊓ ⊔

Theorem 22. For every two F-normal forms N_{1}, N_{2} such that w(N_{1}), w(N_{2}) ≤ W it holds that [[N_{1}]]_{∗} = [[N_{2}]]_{∗} only if N_{1} ≈ N_{2} modulo A1–A4.

Proof. By Lemma 6 we may assume that N_{1} and N_{2} are summations of sequences of simple F-normal forms. We assume [[N_{1}]]_{∗} = [[N_{2}]]_{∗} and prove that then N_{1} ≈ N_{2} modulo A1–A4, by induction on the sum of the heights of N_{1} and N_{2}.

We first prove that for every syntactic summand S_{1} of N_{1} there is a syntactic summand S_{2} of N_{2} such that S_{1} ≈ S_{2} modulo A1–A4. To this end, let S_{1} be an arbitrary syntactic summand of N_{1}; we distinguish cases according to the syntactic form of S_{1}.

1. Suppose S_{1} = α.N′_{1}; then [[S_{1}]]_{∗} ⟶^{α} [[N′_{1}]]_{∗}. Hence, since [[N_{1}]]_{∗} = [[N_{2}]]_{∗}, there exists a syntactic summand S_{2} of N_{2} such that [[S_{2}]]_{∗} ⟶^{α} [[N′_{1}]]_{∗}. By Lemma 19 the branching degree of [[N′_{1}]]_{∗} does not exceed W, so [[S_{2}]]_{∗} has a residual of type 0, and therefore, by Corollary 21, there exist β ∈ A_{τ} and a normal form N′_{2} such that S_{2} = β.N′_{2}. Moreover, since [[S_{2}]]_{∗} ⟶^{α} [[N′_{1}]]_{∗}, it follows by Lemma 20(i) that α = β and [[N′_{1}]]_{∗} = [[N′_{2}]]_{∗}. Hence, by the induction hypothesis, we conclude that N′_{1} ≈ N′_{2} modulo A1–A4, so S_{1} = α.N′_{1} ≈ β.N′_{2} = S_{2}.

2. Suppose S_{1} = x ∥ N′_{1}; then [[S_{1}]]_{∗} ⟶^{τ} φ_{⌜x⌝} ∥ [[N′_{1}]]_{∗}. Hence, since [[N_{1}]]_{∗} = [[N_{2}]]_{∗}, there exists a summand S_{2} of N_{2} such that [[S_{2}]]_{∗} ⟶^{τ} φ_{⌜x⌝} ∥ [[N′_{1}]]_{∗}. Since S_{2} has a residual of type 1, by Corollary 21 there exist a variable y and a normal form N′_{2} such that S_{2} = y∥ N′_{2}. Now, since [[S_{2}]]_{∗}⟶^{τ}φ_{⌜x⌝}∥[[N′_{1}]]_{∗}, it follows by Lemma 20(ii) that

φ_{⌜x⌝} ∥ [[N′_{1}]]_{∗} = φ_{⌜y⌝} ∥ [[N′_{2}]]_{∗} . (4)

Since [[N′_{1}]]_{∗} and [[N′_{2}]]_{∗} are of type 0, we have that the unique decomposition of [[N′_{1}]]_{∗} (see Theorem 11) does not contain φ_{⌜y⌝} and the unique decomposition of [[N′_{2}]]_{∗} does not contain φ_{⌜x⌝}. Hence, from (4) it follows that φ_{⌜x⌝} = φ_{⌜y⌝} and [[N′_{1}]]_{∗} = [[N′_{2}]]_{∗}. From the former we conclude, by Lemma 14(ii) and the injectivity of ⌜.⌝, that x = y and from the latter we conclude by the induction hypothesis that N′_{1} ≈ N′_{2} modulo A1–A4. So S_{1} = x ∥ N′_{1} ≈ y ∥ N′_{2} = S_{2}.

We have established that every syntactic summand of N_{1} is provably equal to a syntactic summand of N_{2}. Similarly, it follows that every syntactic summand of N_{2} is provably equal to a syntactic summand of N_{2}. Hence, modulo A1–A4, N_{1} ≈ N_{1} + N_{2} ≈ N_{2}, so the proof of the theorem is complete. ⊓ ⊔

Corollary 23. For all process terms P and Q, P ≈_{F} Q if, and only if, P \underline{↔}_{f} Q, and hence the axioms generated by the schemata in Table 2 together with the axiom F consitute an equational base for P_{f}.

Proof. The implication from left to right is Proposition 15. To prove the implication from right to left, suppose P \underline{↔}_{f} Q. Then, by Lemma 17 there exist normal forms N_{1} and N_{2} such that P ≈_{F} N_{1} and Q ≈_{F} N_{2}; from P \underline{↔}_{f} Q we conclude by Proposition 15 that N_{1} \underline{↔}_{f} N_{2}. Now choose W large enough such that w(N_{1}), w(N_{2}) ≤ W. From N_{1} \underline{↔}_{f} N_{2} it follows that [[N_{1}]]_{∗} = [[N_{2}]]_{∗}, and hence, by Theorem 22 N_{1} ≈ N_{2}. We may therefore conclude that P ≈_{F} N_{1} ≈ N_{2} ≈_{F} Q. ⊓ ⊔

Corollary 24. The equational theory of P_{f} is decidable.

Proof. From the proof of Lemma 17 it is easy to see that there exists an effective procedure that associates with every process term a provably equivalent F-normal. Furthermore, from Definition 18 it is clear that every F-normal form has an effectively computable width. We now sketch an effective procedure that decides whether a process equation P ≈ Q is valid:

1. Compute F-normal forms N_{1} and N_{2} such that P ≈_{F} N_{1} and Q ≈_{F} N_{2}.

2. Compute w(N_{1}) and w(N_{2}) and define W as their maximum.

3. Determine the (finite) set V′ of variables occurring in N_{1} and N_{2}; define an injection ⌜.⌝ : V′ → {n ∈ ω : n > W }, and a substitution ∗ : V′ → P_{0} that assigns to a variable x in V′ the closed process term τ.φ_{⌜x⌝}. (We may interpret Eqn. 2 as defining a sequence of closed process terms instead of a sequence of processes.)

4. Let N_{1}^{∗} and N_{2}^{∗} be the results from applying ∗ to N_{1} and N_{2}, respectively.

5. Determine if the closed process terms N_{1}^{∗} and N_{2}^{∗} are bisimilar; if they are, then the process equation P ≈ Q is valid in P_{f}, and otherwise it is not. ⊓ ⊔

4 An equational base for P_{h}

We now consider the algebra P_{h}. Note that if A happens to be the empty set, then P_{h} satisfies the axiom F, and it is clear from the proof in the previous section that the axioms generated by the axiom schemata in Table 2 together with F in fact constitute a finite equational base for P_{h}. We therefore proceed with the assumption that A is nonempty, and prove that an equational base for P_{h} is then obtained if we add the axiom

H x | (y | z) ≈ 0

to the set of axioms generated by the axiom schemata in Table 2. Again, the resulting equational base is finite if the set A is finite.

Henceforth, whenever we write P ≈_{H} Q, we shall mean that the equation P ≈ Q is derivable from the axioms in Table 2 and the axiom H.

Proposition 25. For all process terms P and Q, if P ≈_{H} Q, then P \underline{↔}_{h} Q.

We proceed to adapt the proof presented in the previous section to establish the converse of Proposition 25. Naturally, with H instead of F not every occurrence of | can be eliminated from process terms; we therefore need to adapt the notion of normal form.

Definition 26. The set N_{H} of H-normal forms is generated by the following grammar:

N ::= 0 | N + N | α.N | x ∥ N | (x | a) ∥ N | (x | y) ∥ N ,

with x, y ∈ V, α ∈ A_{τ} and a ∈ A.

Note that the set of simple H-normal forms (see Definition 5) is generated by the grammar

S ::= α.N | x ∥ N | (x | a) ∥ N | (x | y) ∥ N ,

with x, y ∈ V, α ∈ A_{τ}, a ∈ A, and N ranging over H-normal forms.

In the proof that every process term is provably equal to an H-normal form, we use the following derivable equation.

Lemma 27. The following equation is derivable from the axioms in Table 2 and the axiom H:

C9 τ.x | y ≈_{H} 0 .

Proof. Let a ∈ A; then

τ.x | y ≈_{H} τ.(x ∥ 0) | y by P4 (see Lemma 10)
≈_{H} (a.x | \overline{a}.0) | y by C2
≈_{H} 0  by H.
⊓ ⊔

Lemma 28. For every process term P there exists an H-normal form N such that P ≈_{H} N and h(P) ≥ h(N).

Proof. As in the proof of Lemma 17 we proceed by ≺-induction and do a case distinction on the syntactic form of P. For the first four cases (P is a variable, P = 0, P = α.P′ and P = P_{1} + P_{2}) the proofs are identical to those in Lemma 17, so they are omitted.

5. If P = Q ∥ R, then, since h(Q) ≤ h(P) and ℓ(Q) < ℓ(P), it holds that Q ≺ P, and hence by the induction hypothesis and Lemma 6 there exists a sequence S_{1}, …, S_{n} of simple H-normal forms such that Q ≈_{H} ∑_{i=1}^{n} S_{i} and h(Q) ≥ h(S_{i}) for all i = 1, …, n. If n = 0, then P ≈_{H} 0∥ R ≈ 0 by L1, and clearly h(P) ≥ h(0). Otherwise, by L3

P ≈_{H} ∑_{i=1}^{n}(S_{i} ∥ R) ,

so it remains to show, for all i = 1, …, n, that S_{i} ∥ R is provably equal to an appropriate H-normal form. We distinguish cases according to the syntactic form of S_{i}:

(a) If S_{i} = α.N′_{i} (with N′_{i} an H-normal form), then by L2

S_{i} ∥ R ≈_{H} α.(N′_{i} ∥ R) .

Since h(N′_{i}) < h(S_{i}) ≤ h(Q), it holds that N′_{i} ∥ R ≺ P and hence by the induction hypothesis there exists an H-normal form N such that N′_{i} ∥ R ≈_{H} N and h(N′_{i} ∥ R) ≥ h(N). Clearly, α.N is an H-normal form such that S_{i} ∥ R ≈_{H} α.N and h(S_{i} ∥ R) ≥ h(α.N).

(b) If S_{i} = S′_{i} ∥ N′′_{i} with S′_{i} = x, S′_{i} = (x | a) or S′_{i} = (x | y), and N′′_{i} an H-normal form, then by L4

S_{i} ∥ R ≈_{H} S′_{i} ∥ (N′′_{i} ∥ R) .

Note that h(S′_{i}) > 0, so h(N′′_{i}) < h(S_{i}) ≤ h(Q). It follows that N′′_{i} ∥ R ≺ P, and hence by the induction hypothesis there exists an H-normal form N such that N′′_{i} ∥ R ≈_{H} N and h(N′′_{i} ∥ R) ≥ h(N). Clearly, S′_{i} ∥ N is an H-normal form such that S_{i} ∥ R ≈_{H} S′_{i} ∥ N and h(S_{i} ∥ R) ≥ h(S′_{i} ∥ N).

6. If P = Q|R, then, since h(Q) ≤ h(P) and ℓ(Q) < ℓ(P), it holds that Q ≺ P, and, for similar reasons, R ≺ P. Hence, by the induction hypothesis and Lemma 6 there exist sequences S_{1}, …, S_{m} and T_{1}, …, T_{n} of simple H-normal forms such that Q ≈_{H} ∑_{i=1}^{m} S_{i}, R ≈_{H} ∑_{j=1}^{n} T_{j}, h(Q) ≥ h(S_{i}) for all i = 1, …, m, and h(R) ≥ h(T_{j}) for all j = 1, …, n. Note that if m = 0, then P ≈_{H} 0 | R ≈ 0 by C1, and if n = 0, then P ≈_{H} Q | 0 ≈_{H} 0 | Q ≈_{H} 0 by C5 and C1, and clearly h(P) ≥ h(0). Otherwise, by C4 and C5

P ≈_{H} ∑_{i=1}^{m} ∑_{j=1}^{n}(S_{i} | T_{j}) ,

and it remains to show, for all i = 1, …, m and j = 1, …, n, that S_{i} | T_{j} is provably equal to an appropriate H-normal form. We distinguish cases according to the syntactic forms that S_{i} and T_{j} may take:

(a) Suppose S_{i} = τ.S′_{i}; then S_{i} | T_{j} ≈_{H} 0 by Lemma 27, and clearly h(S_{i} | T_{j}) ≥ 0.

(b) Suppose T_{j} = τ.T′_{j}; then we apply C5 and proceed as in the previous case.

(c) Suppose S_{i} = S′_{i} ∥ S′′_{i} with S′_{i} = x | a or S′_{i} = x | y; then by C7, C6, H, and L1

S_{i} | T_{j} ≈ (S′_{i} | T_{j}) ∥ S′′_{i} ≈_{H} 0 ∥ S′′_{i} ≈ 0 ,

and clearly h(S_{i} | T_{j}) ≥ h(0).

(d) Suppose T_{j} = T′_{j} ∥ T′′_{j} with T′_{j} = x | a or T′_{j} = x | y; then S_{i} | T_{j} ≈ T_{j} | S_{i} by C5 and we can proceed as in the previous case.

(e) Suppose S_{i} = a.S′_{i} and T_{j} = b.T′_{j}.

If b ≠ \overline{a}, then S_{i} | T_{j} ≈ 0 by C3 and h(S_{i} | T_{j}) ≥ h(0). On the other hand, if b = \overline{a}, then S_{i} | T_{j} ≈ τ.(S′_{i} ∥ T′_{j}), and, since h(S′_{i}) < h(S_{i}) ≤ h(Q) and h(T′_{j}) < h(T_{i}) ≤ h(R), it follows that S′_{i}∥T′_{j} ≺ P. So, by the induction hypothesis there exists an H-normal form N such that S′_{i}∥T′_{j} ≈_{H} N and h(S′_{i} ∥ T′_{j}) ≥ h(N). Then clearly τ.N is an H-normal form such that S_{i} | T_{j} ≈_{H} τ.N and h(S_{i} | T_{j}) ≥ h(τ.N).

(f) Suppose S_{i} = a.S′_{i} and T_{j} = x ∥ T′_{j}. Then

a.S′_{i} | (x ∥ T′_{j}) ≈ a.(0 ∥ S′_{i}) | (x ∥ T′_{j})  (by P4, P3 in Lemma 10)
≈ (a ∥ S′_{i}) | (x ∥ T′_{j})  (by L2)
≈ (x | a) ∥ (S′_{i} ∥ T′_{j})  (by Lemma 3 and C5).

Since h(S′_{i}) < h(S_{i}) ≤ h(Q) and h(T′_{j}) < h(T_{i}) ≤ h(R), it follows that S′_{i} ∥ T′_{j} ≺ P, and hence by the induction hypothesis there exists an H-normal form N such that S′_{i}∥T′_{j} ≈_{H} N and h(S′_{i}∥T′_{j}) ≥ h(N). Then clearly (x|a)∥ N is an H-normal form such that S_{i} | T_{j} ≈_{H} (x | a) ∥ N and h(S_{i} | T_{j}) ≥ h((x | a) ∥ N).

(g) If S_{i} = x ∥ S′_{i} and T_{j} = a.T′_{j}, then the proof is analogous to the previous case.

(h) Suppose S_{i} = x ∥ S′_{i} and T_{j} = y ∥ T′_{j}. Then, by the derived equation C8 (see Lemma 3)

S_{i} | T_{j} ≈ (x | y) ∥ (S′_{i} ∥ T′_{j}) .

Since h(S′_{i}) < h(S_{i}) ≤ h(Q) and h(T′_{j}) < h(T_{i}) ≤ h(R), it follows that S′_{i} ∥ T′_{j} ≺ P, and hence by the induction hypothesis there exists an H-normal form N such that S′_{i}∥T′_{j} ≈_{H} N and h(S′_{i}∥T′_{j}) ≥ h(N). Then clearly (x|y)∥ N is an H-normal form such that S_{i} | T_{j} ≈_{H} (x | y) ∥ N and h(S_{i} | T_{j}) ≥ h((x | y) ∥ N).

7. If P = Q ∥ R, then P ≈ Q ∥ R + R ∥ Q + Q | R. We can now proceed as in case 5 to show that for Q ∥ R and R ∥ Q there exist H-normal forms N_{1} and N_{2}, respectively, such that Q ∥ R ≈_{H} N_{1}, R ∥ Q ≈_{H} N_{2}, h(Q ∥ R) ≥ h(N_{1}) and h(R∥ Q) ≥ h(N_{2}). Furthermore, we can proceed as in case 6 to show that for Q|R there exists an H-normal form N_{3} such that Q | R ≈_{H} N_{3} and h(Q | R) ≥ h(N_{3}). Then N_{1} + N_{2} + N_{3} is an H-normal form such that P ≈_{H} N_{1} + N_{2} + N_{3} and h(P) ≥ h(N_{1} + N_{2} + N_{3}). ⊓ ⊔

We proceed to establish that for every two H-normal forms N_{1} and N_{2} there exists a valuation ∗ : V → P_{γ} such that

if [[N_{1}]]_{∗} = [[N_{2}]]_{∗}, then N_{1} ≈_{H} N_{2}. (5)

The distinguishing valuations ∗ will have a slightly more complicated definition than before, because of the more complicated notion of normal form.

As in the previous section, for the definition of ∗ we fix a natural number W. Since | may occur in H-normal forms, we now also need to make sure that whatever process ∗ assigns to variables has sufficient communication abilities. To achieve this, we fix a finite subset A′ = {a_{1}, …, a_{n}} of A that is closed under the bijection ¯. on A. (Note that every finite subset of A has a finite superset with the aforementioned property.) Based on W and A′ we define the valuation ∗ : V → P_{γ} by

∗(x) = a_{1}.φ_{(1·⌜x⌝)} + ⋯ + a_{n}.φ_{(n·⌜x⌝)} .

We shall prove that ∗ satisfies Eqn. (5) provided that the actions occurring in N_{1} and N_{2} are in A′ ∪ {τ} and the width of N_{1} and N_{2}, defined below, does not exceed W. We must also be careful to define the injection ⌜⌝ in such a way that the extra factors 1, …, n in the definition of ∗ do not interfere with the numbers assigned to variables; we let ⌜⌝ denote an injection

⌜⌝ : V → {m : m a prime number such that m > n and m > W }

that associates with every variable a prime number greater than the cardinality of A′ and greater than W.

The definition of width also needs to take into account the cardinality of A′ to maintain the property that the branching degree of [[N]]_{∗} does not exceed w(N).

Definition 29. We define the width w(N) of an H-normal form N as follows:

(i) if N = 0, then w(N) = 0; (ii) if N = N_{1} + N_{2}, then w(N) = w(N_{1}) + w(N_{2}); (iii) if N = α.N′, then w(N) = max(w(N′), 1); (iv) if N = x ∥ N′, then w(N) = max(w(N′), |A′|);

(v) if N = (x | α) ∥ N′, then w(N) = max(w(N′), 1); and (vi) if N = (x | y) ∥ N′, then w(N) = max(w(N′), |A′|).

Lemma 30. For every H-normal form N, the branching degree of [[N]]_{∗} is at most w(N).

Proof. Structural induction on N. ⊓ ⊔

Lemma 31. Let S be a simple H-normal form, let α ∈ A_{τ}, and let p be a process such that [[S]]_{∗} ⟶^{α} p. Then the following statements hold:

(i) if S = β.N, then α = β and p = [[N]]_{∗}; (ii) if S = x ∥ N, then α = a_{i} and p = φ_{i·⌜x⌝} ∥ [[N]]_{∗} for some i ∈ {1, …, n}; (iii) if S = (x | a) ∥ N, then α = τ and p = φ_{i·⌜x⌝} ∥ [[N]]_{∗} for the unique i ∈ {1, …, n}

such that \overline{a} = a_{i}; and (iv) if S = (x|y)∥ N, then α = τ and p = φ_{i·⌜x⌝}∥φ_{j·⌜y⌝}∥[[N]]_{∗} for some i, j ∈ {1, …, n}

such that \overline{a_{i}} = a_{j}.

As in the previous section, we distinguish H-normal forms by classifying their residuals according to the number of parallel components with a branching degree that exceeds W. Again, we say that a process p is of type n (n ≥ 0) if its unique parallel decomposition contains precisely n parallel prime components with a branching degree > W.

Corollary 32. Let S be a simple H-normal form such that w(S) ≤ W and such that the actions occurring in S are included in A′ ∪ {τ}.

(i) If S = α.N, then the unique residual of [[S]]_{∗} is of type 0. (ii) If S = x ∥ N, then all residuals of [[S]]_{∗} are of type 1. (iii) If S = (x | a) ∥ N, then the unique residual of [[S]]_{∗} is of type 1. (iv) If S = (x | y) ∥ N, then all residuals of [[S]]_{∗} are of type 2.

Proof. On the one hand, by Lemma 30, in each case [[N]]_{∗} has a branching degree of at most w(N) ≤ w(S) ≤ W, and hence, by Lemma 13, its unique parallel decomposition cannot contain parallel prime components with a branching degree that exceeds W. On the other hand, by Lemmas 14(i) and 14(iii), the processes φ_{i·⌜x⌝} and φ_{j·⌜y⌝} are parallel prime and have a branching degree that exceeds W. Using these observations it is straightforward to establish the corollary as a consequence of Lemma 31. ⊓ ⊔

Theorem 33. For every two H-normal forms N_{1}, N_{2} such that w(N_{1}), w(N_{2}) ≤ W and such that the actions occurring in N_{1} and N_{2} are included in A′ ∪ {τ} it holds that [[N_{1}]]_{∗} = [[N_{2}]]_{∗} only if N_{1} ≈ N_{2} modulo A1–A4, C5.

Proof. By Lemma 6 we may assume that N_{1} and N_{2} are summations of sequences of simple H-normal forms. We assume [[N_{1}]]_{∗} = [[N_{2}]]_{∗} and prove that then N_{1} ≈ N_{2} modulo A1–A4, C5, by induction on the sum of the heights of N_{1} and N_{2}.

We first prove that for every syntactic summand S_{1} of N_{1} there is a syntactic summand S_{2} of N_{2} such that S_{1} ≈ S_{2} modulo A1–A4, C5. To this end, let S_{1} be an arbitrary syntactic summand of N_{1}; we distinguish cases according to the syntactic form of S_{1}.

1. Suppose S_{1} = α.N′_{1}; then [[S_{1}]]_{∗} ⟶^{α} [[N′_{1}]]_{∗}. Hence, since [[N_{1}]]_{∗} = [[N_{2}]]_{∗}, there exists a syntactic summand S_{2} of N_{2} such that [[S_{2}]]_{∗} ⟶^{α} [[N′_{1}]]_{∗}. By Lemma 30 the branching degree of [[N′_{1}]]_{∗} does not exceed W, so [[S_{2}]]_{∗} has a residual of type 0, and therefore, by Corollary 32, there exist β ∈ A_{τ} and an H-normal form N′_{2} such that S_{2} = β.N′_{2}. Moreover, since [[S_{2}]]_{∗} ⟶^{α} [[N′_{1}]]_{∗} it follows by Lemma 31(i) that α = β and [[N′_{1}]]_{∗} = [[N′_{2}]]_{∗}. Hence, by the induction hypothesis, we conclude that N′_{1} ≈ N′_{2} modulo A1–A4, C5. So S_{1} = α.N′_{1} ≈ β.N′_{2} = S_{2}.

2. Suppose S_{1} = x ∥ N′_{1}; then [[S_{1}]]_{∗} ⟶^{a_{1}} φ_{⌜x⌝} ∥ [[N′_{1}]]_{∗}. Hence, since [[N_{1}]]_{∗} = [[N_{2}]]_{∗}, there exists a summand S_{2} of N_{2} such that [[S_{2}]]_{∗} ⟶^{a_{1}} φ_{⌜x⌝} ∥ [[N′_{1}]]_{∗}. Since S_{2} has a residual of type 1, by Corollary 32(i, iv) it is not of the form α.N′_{2} for some α ∈ A_{τ} and H-normal form N′_{2}, or of the form (y | z) ∥ N′_{2} for some y, z ∈ V and H-normal form N′_{2}. Moreover, S_{2} cannot be of the form (y | a) ∥ N′_{2} for some y ∈ V and a ∈ A, for then by Lemma 31(iii) [[S_{2}]]_{∗} ⟶^{α} p would imply α = τ ≠ a_{1}. So, there exists a variable y and an H-normal form N′_{2} such that S_{2} = y ∥ N′_{2}. Now, since [[S_{2}]]_{∗} ⟶^{a_{1}} φ_{⌜x⌝} ∥ [[N′_{1}]]_{∗}, it follows by Lemma 31(ii) that

φ_{⌜x⌝} ∥ [[N′_{1}]]_{∗} = φ_{⌜y⌝} ∥ [[N′_{2}]]_{∗} . (6)

Since [[N′_{1}]]_{∗} and [[N′_{2}]]_{∗} are of type 0, we conclude that the unique decomposition of [[N′_{1}]]_{∗} does not contain φ_{⌜y⌝} and the unique decomposition of [[N′_{2}]]_{∗} does not contain φ_{⌜x⌝}. Hence, from (6) it follows that φ_{⌜x⌝} = φ_{⌜y⌝} and [[N′_{1}]]_{∗} = [[N′_{2}]]_{∗}. From the former we conclude by the injectivity of ⌜.⌝ that x = y, and from the latter we conclude by the induction hypothesis that N′_{1} ≈ N′_{2} modulo A1–A4, C5. So S_{1} = x ∥ N′_{1} ≈ y ∥ N′_{2} = S_{2}.

3. Suppose S_{1} = (x | a) ∥ N′_{1}, and let i be such that \overline{a} = a_{i}. Then [[S_{1}]]_{∗} ⟶^{τ} φ_{i·⌜x⌝} ∥ [[N′_{1}]]_{∗}. Hence, since [[N_{1}]]_{∗} = [[N_{2}]]_{∗}, there exists a summand S_{2} of N_{2} such that

[[S_{2}]]_{∗} ⟶^{τ} φ_{i·⌜x⌝} ∥ [[N′_{1}]]_{∗} .

Since S_{2} has a residual of type 1, by Corollary 32(i, iv) it is not of the form α.N′_{2} for some α ∈ A_{τ} and H-normal form N′_{2}, or of the form (y | z) ∥ N′_{2} for some y, z ∈ V and H-normal form N′_{2}. Moreover, S_{2} cannot be of the form y ∥ N′_{2} for some y ∈ V, for then by Lemma 31(ii) [[S_{2}]]_{∗} ⟶^{α} p would imply α = a_{k} ≠ τ for some k ∈ {1, …, n}. So, there exist a variable y, action b ∈ A′ and an H-normal form N′_{2} such that S_{2} = (y | b) ∥ N′_{2}. Now, since [[S_{2}]]_{∗} ⟶^{τ} φ_{i·⌜x⌝} ∥ [[N′_{1}]]_{∗}, it follows by Lemma 31(iii) that

φ_{i·⌜x⌝} ∥ [[N′_{1}]]_{∗} = φ_{j·⌜y⌝} ∥ [[N′_{2}]]_{∗} , (7) with j ∈ \{1, …, n\} such that \overline{b} = a_{j}. By Lemma 14(i, iii) the processes φ_{i·⌜x⌝} and φ_{j·⌜y⌝} are parallel prime and have branching degrees that, since ⌜x⌝ > W and ⌜y⌝ > W, exceed W. Therefore, since [[N′_{1}]]_{∗} and [[N′_{2}]]_{∗} are of type 0, it follows that the unique decomposition of [[N′_{1}]]_{∗} does not contain φ_{j·⌜y⌝} and the unique decomposition of [[N′_{2}]]_{∗} does not contain φ_{i·⌜x⌝}. Hence, by (7) we have that φ_{i·⌜x⌝} = φ_{j·⌜y⌝} and [[N′_{1}]]_{∗} = [[N′_{2}]]_{∗}. From φ_{i·⌜x⌝} = φ_{j·⌜y⌝}, by Lemma 14(ii) we infer that i · ⌜x⌝ = j · ⌜y⌝. Since ⌜x⌝ and ⌜y⌝ are prime numbers greater than i and j, it follows that i = j, whence a = b, and ⌜x⌝ = ⌜y⌝, whence x = y by the injectivity of ⌜.⌝. From [[N′_{1}]]_{∗} = [[N′_{2}]]_{∗} we conclude by the induction hypothesis that N′_{1} ≈ N′_{2} modulo A1–A4, C5. So S_{1} = (x | a) ∥ N′_{1} ≈ (y | b) ∥ N′_{2} = S_{2}.

4. Suppose S_{1} = (x|y)∥ N′_{1}. Then [[S_{1}]]_{∗}⟶^{τ}φ_{i·⌜x⌝}∥φ_{j·⌜y⌝}∥[[N′_{1}]]_{∗} with i, j ∈ {1, …, n}

such that \overline{a_{i}} = a_{j}. Hence, since [[N_{1}]]_{∗} = [[N_{2}]]_{∗}, there exists a summand S_{2} of N_{2} such that

[[S_{2}]]_{∗} ⟶^{τ} φ_{i·⌜x⌝} ∥ φ_{j·⌜y⌝} ∥ [[N′_{1}]]_{∗} .

Since S_{2} has a residual of type 2, by Corollary 32 there exist x′, y′ ∈ V and an H-normal form N′_{2} such that S_{2} = (x′ | y′) ∥ N′_{2}. Now, since [[S_{2}]]_{∗} ⟶^{τ} φ_{i·⌜x⌝} ∥ φ_{j·⌜y⌝} ∥ [[N′_{1}]]_{∗} it follows by Lemma 31(iv) that for some k, l ∈ {1, …, n} such that \overline{a_{k}} = a_{l}

φ_{i·⌜x⌝} ∥ φ_{j·⌜y⌝} ∥ [[N′_{1}]]_{∗} = φ_{k·⌜x′⌝} ∥ φ_{l·⌜y′⌝} ∥ [[N′_{2}]]_{∗} . (8)

By Lemma 14(i, iii) the processes φ_{i·⌜x⌝}, φ_{j·⌜y⌝}, φ_{k·⌜x′⌝} and φ_{l·⌜y′⌝} are parallel prime and have branching degrees that exceed W. Therefore, since [[N′_{1}]]_{∗} and [[N′_{2}]]_{∗} are of type 0, it follows that the unique decomposition of [[N′_{1}]]_{∗} does not contain φ_{k·⌜x′⌝} and φ_{l·⌜y′⌝}, and the unique decomposition of [[N′_{2}]]_{∗} does not contain φ_{i·⌜x⌝} and φ_{j·⌜y⌝}. Hence, from (8) we infer that [[N′_{1}]]_{∗} = [[N′_{2}]]_{∗} and either φ_{i·⌜x⌝} = φ_{k·⌜x′⌝} and φ_{j·⌜y⌝} = φ_{l·⌜y′⌝}, or φ_{i·⌜x⌝} = φ_{l·⌜y′⌝} and φ_{j·⌜y⌝} = φ_{k·⌜x′⌝}. From the former we conclude by the induction hypothesis that N′_{1} ≈ N′_{2} modulo A1–A4, C5; from the latter it follows reasoning as in case 3 that either x = x′ and y = y′, or x = y′ and y = x′. In both cases, S_{1} = (x | y) ∥ N′_{1} ≈ (x′ | y′) ∥ N′_{2} = S_{2}.

We have established that every syntactic summand of N_{1} is provably equal to a syntactic summand of N_{2}. Similarly, it follows that every syntactic summand of N_{2} is provably equal to a syntactic summand of N_{2}. Hence, modulo A1–A4, C5 N_{1} ≈ N_{1} + N_{2} ≈ N_{2}, and the proof of the theorem is complete. ⊓ ⊔

Corollary 34. For all process terms P and Q, P ≈_{H} Q if, and only if, P \underline{↔}_{h} Q, and hence the axioms generated by the schemata in Table 2 together with the axiom H consitute an equational base for P_{h}.

Proof. The implication from left to right is Proposition 25. To prove the implication from right to left, suppose P \underline{↔}_{h} Q. Then, by Lemma 28 there exist H-normal forms N_{1} and N_{2} such that P ≈_{H} N_{1} and Q ≈_{H} N_{2}; from P \underline{↔}_{h} Q we conclude by Proposition 25 that N_{1} \underline{↔}_{h} N_{2}. Now choose W large enough such that w(N_{1}), w(N_{2}) ≤ W, and pick a finite set A′ that is closed under ¯. and includes all of the actions occurring in N_{1} and N_{2}. From N_{1} \underline{↔}_{h} N_{2} it follows that [[N_{1}]]_{∗} = [[N_{2}]]_{∗}, and hence, by Theorem 33 N_{1} ≈ N_{2}. We can therefore conclude P ≈_{H} N_{1} ≈ N_{2} ≈_{H} Q. ⊓ ⊔ Corollary 35. The equational theory of P_{h} is decidable.

Proof. From the proof of Lemma 28 it is easy to see that there exists an effective procedure that associates with every process term a provably equivalent H-normal. Furthermore, from Definition 29 it is clear that, given a set A′, every H-normal form has a effectively computable width. We now sketch an effective procedure that decides whether a process equation P ≈ Q is valid:

1. Compute H-normal forms N_{1} and N_{2} such that P ≈_{H} N_{1} and Q ≈_{H} N_{2}.

2. Determine the least set A′ = {a_{1}, …, a_{n}} of actions that is closed under ¯. and contains the actions in A occurring in N_{1} and N_{2}.

3. Compute w(N_{1}) and w(N_{2}) given A′ and define W as their maximum.

4. Determine the (finite) set V′ of variables occurring in N_{1} and N_{2}; define an injection

⌜.⌝ : V′ → {m ∈ ω : m a prime number such that m > n and m > W } ,

and a substitution ∗ : V′ → P_{0} that assigns to a variable x in V′ the closed process term

a_{1}.φ_{1·⌜x⌝} + ⋯ + a_{n}.φ_{n·⌜x⌝} .

(Again, we interpret Eqn. 2 as defining a sequence of closed process terms instead of a sequence of processes.)

5. Let N_{1}^{∗} and N_{2}^{∗} be the results from applying ∗ to N_{1} and N_{2}, respectively.

6. Determine if the closed process terms N_{1}^{∗} and N_{2}^{∗} are bisimilar; if they are, then the process equation P ≈ Q is valid in P_{h}, and otherwise it is not. ⊓ ⊔

References

1. L. Aceto, W. J. Fokkink, A. Ingolfsdottir, and B. Luttik. CCS with Hennessy’s merge has no finite equational axiomatization. Theor. Comput. Sci., 330(3):377–405, 2005.

2. L. Aceto, W. J. Fokkink, A. Ingolfsdottir, and B. Luttik. Finite equational bases in process algebra: Results and open questions. In A. Middeldorp, V. van Oostrom, F. van Raamsdonk, and R. C. de Vrijer, editors, Processes, Terms and Cycles: Steps on the Road to Infinity, LNCS 3838, pages 338–367. Springer, 2005.

3. J. A. Bergstra and J. W. Klop. Process algebra for synchronous communication. Inform. and Control, 60(1-3):109–137, 1984.

4. J. A. Bergstra and J. V. Tucker. Top-down design and the algebra of communicating processes. Sci. Comput. Programming, 5(2):171–199, 1985.

5. R. de Simone. Higher-level synchronising devices in Meije-SCCS. Theor. Comput. Sci., 37:245– 267, 1985.

6. J. F. Groote. A new strategy for proving omega-completeness applied to process algebra. In J. C. M. Baeten and J. W. Klop, editors, Proceedings of CONCUR’90, LNCS 458, pages 314–331. Springer, 1990.

7. J. Heering. Partial evaluation and ω-completeness of algebraic specifications. Theoret. Comput. Sci., 43(2-3):149–167, 1986.

8. M. Hennessy. Axiomatising finite concurrent processes. SIAM J. Comput., 17(5):997–1017, 1988.

9. M. Hennessy and R. Milner. Algebraic laws for nondeterminism and concurrency. J. ACM, 32(1):137–161, January 1985.

10. B. Luttik and V. van Oostrom. Decomposition orders—another proof of the fundamental theorem of arithmetic. Theor. Comput. Sci., 335(2–3):147–186, 2005.

11. R. Milner. Communication and Concurrency. Prentice-Hall International, 1989.

12. F. Moller. Axioms for Concurrency. PhD thesis, University of Edinburgh, 1989.

13. F. Moller. The nonexistence of finite axiomatisations for CCS congruences. In Proceedings of LICS’90, pages 142–153. IEEE Computer Society Press, 1990.

14. D. M. R. Park. Concurrency and automata on infinite sequences. In P. Deussen, editor, 5^{th} GI Conference, LNCS 104, pages 167–183. Springer, 1981.

15. W. Taylor. Equational logic. Houston J. Math., (Survey), 1979.

Recent BRICS Report Series Publications

RS-06-6 Luca Aceto, Willem Jan Fokkink, Anna Ingólfsdóttir, and Bas Luttik. A Finite Equational Base for CCS with Left Merge and Communication Merge. March 2006. 22 pp.

RS-06-5 Kristian Støvring. Extending the Extensional Lambda Calculus with Surjective Pairing is Conservative. March 2006. 18 pp. To appear in Logical Methods in Computer Science. Supersedes RS-05-35.

RS-06-4 Olivier Danvy and Kevin Millikin. A Rational Deconstruction of Landin’s J Operator. 2006.

RS-06-3 Ma�gorzata Biernacka and Olivier Danvy. A Concrete Framework for Environment Machines. February 2006. ii+29 pp. To appear in the ACM Transactions on Computational Logic. Supersedes BRICS RS-05-15.

RS-06-2 Mikkel Baun Kjærgaard and Jonathan Bunde-Pedersen. A Formal Model for Context-Awareness. February 2006. 26 pp.

RS-06-1 Luca Aceto, Taolue Chen, Willem Jan Fokkink, and Anna Ingólfsdóttir. On the Axiomatizability of Priority. January 2006. 25 pp.

RS-05-38 Ma�gorzata Biernacka and Olivier Danvy. A Syntactic Correspondence between Context-Sensitive Calculi and Abstract Machines. December 2005. iii+39 pp. Revised version of BRICS RS-05-22.

RS-05-37 Gerth Stølting Brodal, Kanela Kaligosi, Irit Katriel, and Martin Kutz. Faster Algorithms for Computing Longest Common Increasing Subsequences. December 2005. 16 pp.

RS-05-36 Dariusz Biernacki, Olivier Danvy, and Chung-chieh Shan. On the Static and Dynamic Extents of Delimited Continuations. December 2005. ii+33 pp. To appear in the journal Science of Computer Programming. Supersedes BRICS RS-05-13.

RS-05-35 Kristian Støvring. Extending the Extensional Lambda Calculus with Surjective Pairing is Conservative. November 2005. 19 pp.

RS-05-34 Henning Korsholm Rohde. Formal Aspects of Polyvariant Specialization. November 2005. 27 pp.