Bisimulation equivalence is decidable for normed Process Algebra

Yoram Hirshfeld^{∗} School of Mathematical Sciences Tel Aviv University Israel

Mark Jerrum^{†} Department of Computer Science University of Edinburgh United Kingdom.

May, 1998

Abstract We present a procedure for deciding whether two normed PA terms are bisimilar. The procedure is “elementary,” having doubly exponential nondeterministic time complexity.

∗The first author was supported in part by EPSRC Visiting Research Fellowships GR/K83243 and GR/M06468. Address for correspondence: School of Mathematical Sciences, The Raymond and Beverly Sackler Faculty of Exact Sciences, Tel Aviv University, Ramat Aviv, Tel Aviv 69978, Israel.

†The second author is supported in part by Esprit Working Group No. 21726, “RAND2.” Address for correspondence: Department of Computer Science, University of Edinburgh, The King’s Buildings, Edinburgh EH9 3JZ, United Kingdom.

1 Discussion

Let Atom be a finite set of atomic processes or atoms, Act a finite set of actions, and Π a collection of productions of the form X )^{a} Y, where X, Y ∈ Atom and a ∈ Act. Regarding the atoms as states of a system, we can think of the production X )^{a} Y as specifying a possible evolution, or derivation of the system from state X to Y via action a. What we have is nothing more than a finite state automaton, familiar from formal language theory.

We can generalise this situation somewhat by allowing both the states and the right hand sides of productions to be terms constructed from atoms using an associative, non-commutative operator “ · ” that we think of as “sequential composition.” The productions specify the derivations available to atoms, and hence, by extension, to terms: the derivations available to a general term P = X_{1} · · · · · X_{n} are precisely those of the form

P )^{a} X′_{1} · X_{2} · · · · · X_{n},

where X_{1} )^{a} X′_{1} is a derivation of the atom X_{1}. (Note that X′_{1} is not in general an atom, and may be ε, the empty term.) The non-commutativity of the sequential composition operator is reflected in the restriction that productions can be applied only to the leftmost atom.

By way of example, if Atom = {X}, Act = {a, b}, and the available productions are

X )^{a} X · X and X )^{b} ε,

then the states reachable (by some sequence of derivations) from X are ε, X, X · X, X · X · X, …, and the available action-sequences from state X to itself are ε, ab, abab, aabb, ababab, …, i.e., all “balanced parenthesis sequences.”

In the field of concurrency theory, systems defined by sets of productions of the form just described are known as “context-free” or “Basic Process Algebra” (BPA) processes. (What we have been terming “states” are commonly referred to as processes in concurrency theory.) In language-theoretic terms, a BPA process is equivalent to a pushdown automaton with one state. However, concurrency theory is distinguished from formal language theory in having a different set of concerns: given two BPA processes P and Q we are interested not in whether the action-sequences available to the P and Q are equal as sets (a static notion), but in whether P and Q are “behaviourally equivalent” in a dynamical sense.

What is the “correct” notion of behavioural equivalence for concurrent processes? A popular and mathematically fruitful answer is the relation of bisimilarity: two processes are bisimilar, or bisimulation equivalent, if, roughly, they may evolve together in such a way that whenever the first process performs a certain action, the second process is able to respond by performing the same action, and vice versa. (Precise definitions of this and other terms appearing in this section will be given in Section 2.) The notion of bisimulation equivalence was introduced by Park [11] around 1980, and has been intensively studied since. Bisimilarity plays an important role in algebraic theories of concurrency, such as that based on Milner’s CCS [9].

As we have already seen, a BPA process may have infinitely many states, so it is by no means clear, a priori, that there is an effective procedure for deciding whether two BPA processes P and Q are bisimilar. The first such procedure was presented by Christensen, Hüttel and Stirling [6], though no upper bound on complexity could be offered at the time. Subsequently, Burkart, Caucal and Steffen showed the decision problem to be “elementary,” i.e., to have timecomplexity bounded by some constant-height tower of exponentials [3].

With an eye to modelling concurrent systems, we may introduce an associative, commutative operator “ | ” representing “parallel composition.” Basic Parallel Processes (BPP) are terms constructed from atoms using just this parallel composition operator. Derivations on atoms may be defined, as in BPA, by a finite set of productions, and then extended to terms in the natural way. The commutativity of the parallel composition operator expresses itself in the ability of a process P | Q | R, say, to evolve through any of P, Q or R undergoing a derivation. Bisimilarity of pairs of BPPs was shown to be decidable by Christensen, Hirshfeld and Moller [5], but is not known to be elementary.

Is is natural to consider processes built from atoms using both sequential and parallel composition operators. As before, derivations on atoms may be defined by a grammar, the productions of which have atoms on the left hand side, and arbitrary terms on the right. The derivation relation extends to terms in the natural way, respecting the commutativity of parallel composition; so that, for example, if U, X, Y, Z ∈ Atom and U )^{a} U′, X )^{a} X′, Y )^{a} Y′ and Z )^{a} Z′ are possible derivations, then (adopting the convention that “ · ” binds more tightly than “ | ”), the process (U | X) · Y | Z has all of

(U′ | X) · Y | Z, (U | X′) · Y | Z and (U | X) · Y | Z′

as possible derivatives (via action a), but not (U | X) · Y′ | Z. This set-up can be viewed as a fragment of the process algebra ACP, the Algebra of Communicating Processes of Bergstra and Klop [2]; we refer to this fragment as PA. As a model for concurrent systems, PA still lacks the important element of synchronisation (the “C” in “ACP”), but at least it represents step towards the the kind of expressivity that would be required to describe realistic concurrent systems.

An open problem of some years’ standing is whether bisimilarity of PA processes is decidable and, if so, how great is its computational complexity. We are not able to provide a complete answer to this question. However, we are able to present a decision procedure for the subclass of “normed” PA processes. The property of being normed applies to processes generally, independently of how they are described (in BPA, BPP, PA, or whatever). A process P is said to be normed if, for all P^{∗} that can be reached from P via some sequence of derivations, there is a further sequence of derivations that reduces P^{∗} to ε. For processes described in BPA, BPP or PA, a sufficient condition for being normed is that all atoms X ∈ Atom can be reduced to ε via some derivation sequence.

The assumption of normedness seems innocuous; nevertheless, experience suggests that normed processes are easier to cope with than arbitrary ones. For both BPA and BPP, bisimilarity was shown first shown to be decidable for normed processes: in the case of BPA by Baeten, Bergstra and Klop [1], and in the case of BPP by Christensen, Hirshfeld and Moller [4]. Furthermore, Hirshfeld, Jerrum and Moller have presented polynomial-time algorithms for deciding bisimilarity for both normed BPA [7] and normed BPP [8]. The same phenomenon now reappears in the context of PA.

At the core of the problem of deciding bisimilarity of PA processes lies the surprising complexity of interactions that can occur between sequential and parallel composition. In particular, there are situations in which the sequential composition of two processes P_{1}·P_{2} may be equivalent to a parallel composition Q_{1} | Q_{2} of two other processes. A trivial example is given by Atom = {X}, Act = {a, b} and productions

X )^{a} X | X and X )^{b} ε,

which system is equivalent to the example using sequential composition given earlier. But this is just the simplest case, and the equivalence P_{1} · P_{2} ∼ Q_{1} | Q_{2} in fact has an infinite set of solutions of apparently unbounded complexity.

The key to our approach is to develop a structure theory for PA that completely classifies the situations in which a sequential composition of two processes can be bisimilar to a parallel composition. Fortunately, the infinite collection of examples mentioned earlier can be covered using a small number of patterns (applied recursively). As a consequence of the classification we obtain a decision procedure for bisimilarity in normed PA. Unfortunately, the structure theory we develop relies crucially on unique decomposition of processes into sequential and parallel prime components, which in turn relies of normedness, so there seems little hope of a direct extension to the general (un-normed) case.

It is a chastening thought that we have absolutely no information concerning the complexity of deciding bisimilarity for general (un-normed) PA: the two extremes—that bisimilarity is in the class P, or that it is undecidable—are perfectly consistent with our current lack of knowledge.

2 Notation and Basic facts about PA

Here, we collect together many definitions that are standard in the area. Because they are numerous and routine, we shall not explicitly flag definitions as such in this section.

Recall that Atom is a finite set of atomic processes or atoms, and Act Atoms, actions

and processes.

a finite set of actions. We let U, X, Y, Z stand for generic atoms, and a, b, c for generic actions; other naming conventions will be introduced as and when convenient. The set Proc of processes contains all terms in the free algebra over Atom generated by the non-commutative associative operator “ · ” of sequential composition, and the commutative associative operator “ | ” of parallel composition.

A PA process is defined by a finite set Π of productions, each of the form

PA process, derivation, immediate derivative.

X )^{a} P,  (1)

where X ∈ Atom, a ∈ Act and P ∈ Proc. A production such as (1) specifies a derivation available to X: atomic process X undergoes action a to become process P. The notion of derivation may be extended to arbitrary processes P ∈ Proc in the natural way:

• if P )^{a} P′ then P · Q )^{a} P′ · Q;

• if P )^{a} P′ then P | Q )^{a} P′ | Q;

• if Q )^{a} Q′ then P | Q )^{a} P | Q′.

(The last rule adds nothing new, but is included to emphasise the commutative nature of parallel composition.) If P )^{a} Q for some action a we say that Q is an immediate derivative of P. We drop the label a from the derivation P )^{a} Q in cases where the associated action a is unimportant.

Derivative, We write P ⇝ P^{∗}—and say that P^{∗} is a derivative of P—if there is some

labelled transition system.

sequence of processes P_{0}, P_{1}, …, P_{l} such that

P = P_{0} ) P_{1} ) ⋯) P_{l−1} ) P_{l} = P^{∗};

the number l is the length of the derivation sequence. Note that an immediate derivative corresponds to the special case l = 1. We shall typically use P′ to denote an immediate derivative of P, and P^{∗} to denote a (general) derivative. The collection of all derivations defines a structure known as a labelled transition system: formally, this is just a labelled directed multigraph on vertex set Proc, in which there is an edge labelled a from P to P′ precisely when P )^{a} P′. Note that the finite set of productions Π may define an infinite labelled transition system.

Notational When writing PA processes we adopt a couple of conventions: sequential

conventions.

composition binds more tightly than parallel composition, and exponentiation is used to denote a parallel composition of several copies of a process, thus

P^{k} = \underbrace{P | … | P}_{k copies}.

Norm, reduction, The norm ||P|| of a process P ∈ Proc is the length of a shortest derivation

immediate reduct, reduct.

sequence P ⇝ ε if such a sequence exists, and otherwise. A process P is said to be normed if every derivative P^{∗} of P has finite norm. Note that if all atoms X ∈ Act have finite norm, than all processes P ∈ Proc will be normed. A reduction is a derivation P )^{a} P′ that reduces norm, i.e., ||P′|| < ||P||; we say that P′ is an immediate reduct of P. Note that if P )^{a} P′ is any reduction then ||P′|| = ||P|| − 1. A (general) reduct of P is any process P^{∗} that can be reached from P via a sequence of reductions.

Observation 2.1 If P and Q have finite norm, then ||P · Q|| = ||P | Q|| = ||P|| + ||Q||.

A binary relation ℛ on Proc is a bisimulation if the following conditions Bisimulation

relation,

bisimilarity (or bisimulation equivalence).

are satisfied:

• for all P, Q, P′ ∈ Proc and a ∈ Act such that P ℛ Q and P )^{a} P′, there exists Q′ ∈ Proc such that Q )^{a} Q′ and P′ ℛ Q′; and

• for all P, Q, Q′ ∈ Proc and a ∈ Act such that P ℛ Q and Q )^{a} Q′, there exists P′ ∈ Proc such that P )^{a} P′ and P′ ℛ Q′.

The property of being a bisimulation is closed under union, so there is a unique maximal bisimulation that we shall denote by “ ∼ ”. Two processes P, Q such that P ∼ Q are said to be bisimilar or bisimulation equivalent. Note that bisimilarity is well defined for PA, being invariant under rearrangement of terms, using associativity of sequential composition and associativity and commutativity of parallel composition.

By way of example, suppose Atom = {H, K, X}, Act = {a, b, c}, and Π is the An example of a

pair of bisimilar processes.

set of productions

\begin{matrix}X & )^{a} & X^{2}, & K & )^{c} & X, & H & )^{c} & K | X^{2} \\ X & )^{b} & ε, & K & )^{c} & K | X, & H & )^{c} & H | X \end{matrix}

Then

H · X ∼ K · X | K · X,  (2)

as can be verified by explicit construction of a bisimulation R containing the pair ⟨H · X, K · X | K · X⟩:

R = {⟨(H | X^{i+j}) · X, (K | X^{i}) · X | (K | X^{j}) · X⟩ : i, j ∈ ℕ}
∪ {⟨(K | X^{i+j+1} ) · X, (K | X^{i}) · X | X^{j} · X⟩ : i, j ∈ ℕ}
∪ {⟨(K | X^{i+j}) · X, (K | X^{i}) · X | X^{j}⟩ : i, j ∈ ℕ}
∪ {⟨X^{i+j+1} · X, X^{i} · X | X^{j} · X⟩ : i, j ∈ ℕ}
∪ {⟨X^{i+j} · X, X^{i} · X | X^{j}⟩ : i, j ∈ ℕ}
∪ {⟨X^{i} · X, X^{i+1}⟩ : i ∈ ℕ}.

It is a routine exercise to check that R satisfies the definition of a bisimulation.

This relatively simple example hints at the technical difficulties that lie at the heart of the problem of deciding bisimilarity of PA processes: observe that an equation such as (2) may hold even though the l.h.s. is formally a sequential composition and the r.h.s. a parallel composition, and even though both sides are infinite state (i.e., the set of processes reachable from either side is infinite).

The bisimulation relation on PA processes possesses algebraic structure which is crucial to our decision procedure.

Bisimilarity is a Observation 2.2 Bisimulation equivalence is a congruence under sequential

congruence.

and parallel composition. That is,

P · R ∼ Q · R, R · P ∼ R · Q and P | R ∼ Q | R,

for all P, Q, R satisfying P ∼ Q.

Note that Observation 2.2 holds even if the some of the processes involved have infinite norm.

Sequential and For normed processes the situation is even better. We say that a normed

parallel primes.

process P is a sequential prime (respectively a parallel prime) if it is not bisimilar to any process of the form P_{1} · P_{2} (respectively P_{1} | P_{2}) with ||P_{1}||, ||P_{2}|| > 0. The use of the term “prime” here is justified by the following facts.

Unique sequential Proposition 2.3 Suppose

decomposition.

P_{1} · P_{2} · · · · · P_{n} ∼ Q_{1} · Q_{2} · · · · · Q_{m},

where the processes P_{i} and Q_{j} are sequential primes of finite norm. Then n = m, and P_{i} ∼ Q_{i}, for all 1 ≤ i ≤ n.

Proof. See, for example, Hirshfeld et al. [7].

Unique parallel Proposition 2.4 Suppose

decomposition.

P_{1} | P_{2} | … | P_{n} ∼ Q_{1} | Q_{2} | … | Q_{m},

where the processes P_{i} and Q_{j} are parallel primes of finite norm. Then n = m, and there exists a permutation π of the integers {1, 2, …, n} such that P_{i} ∼ Q_{π(i)} , for all 1 ≤ i ≤ n.

Proof. See, for example, Christensen et al. [4].

(The phenomenon of unique decomposability of processes was first noted by Milner and Moller [10].) Note that Propositions 2.3 and 2.4 require the component processes to have finite norm. It is because we make extensive use of unique decomposition that our decision procedure is restricted to normed processes.

Note also that Propositions 2.3 and 2.4 imply a converse to Observation 2.2,

Cancellation which allows cancellation of like components. Thus, if P, Q, R are normed and

rules.

P · R ∼ Q · R, then P ∼ Q. In fact, the cancelled processes do not need to be equal, merely bisimilar. Similar cancellation rules can be formulated for the other two cases in Observation 2.2. Cancellation fails for general (possibly infinite norm) processes.

3 Outline of the decidability proof

The full proof of decidability is long and technically involved, so we offer in this section a rough guide to its main features.

To motivate the approach, let us attempt to build a (non-deterministic) decision procedure directly from the definition of bisimilarity. Given a pair or processes ⟨P, Q⟩, we wish to decide whether P ∼ Q. We try all derivations P )^{a} P′ (note that there are finitely many) and for each one guess a matching derivation Q )^{a} Q′. (By “matching” derivation we mean one for which P′ ∼ Q′.) Symmetrically, for each derivation Q )^{a} Q′ we guess a matching derivation P )^{a} P′. Let us call the process of generating all pairs ⟨P′, Q′⟩ derived from ⟨P, Q⟩ an “expansion step.” If there exists a derivation P )^{a} P′ that is not matched by any derivation Q )^{a} Q′ (i.e., Q is incapable of performing action a), we say the expansion step fails; in this case, we immediately halt and reject.

Otherwise we consider all the derived pairs of processes ⟨P′, Q′⟩ and apply the expansion step to them to build a second level of derived processes, and then a third, and so on. If P ∼ Q then the nondeterministic choices can be made so that no expansion step fails. Conversely, if P / ∼ Q then, eventually, some expansion step must fail, whatever nondeterministic choices are made.

The main (and only) objection to the above approach is that the derived processes can grow without limit, so that the procedure will not in general terminate in the case P ∼ Q. We counter this objection by combining the expansion step with a complementary simplification step that cuts in when the norm of P and Q becomes larger than the norm of any atom. In this situation, P and Q must either be sequential or parallel compositions. If P and Q are of the same kind—both sequential or both parallel—the simplification step is straightforward. For example, if P = P_{1}·P_{2} and Q = Q_{1}·Q_{2} with ||P_{1}|| ≥ ||Q_{1}||, then we guess a process R with norm ||R|| = ||P_{1}|| − ||Q_{1}||; then we replace the pair ⟨P, Q⟩ by the two smaller pairs ⟨P_{1}, Q_{1} · R⟩ and ⟨R · P_{2}, Q_{2}⟩. This is an appropriate action, since, by unique factorisation,

P ∼ Q {} ∃R [P_{1} ∼ Q_{1} · R ∧ R · P_{2} ∼ Q_{2}].

A similar simplification step is available when P and Q are both parallel compositions.

The difficult case for simplification is when (say) P is a sequential composition, and Q a parallel composition, leading to a so-called “mixed equation.” For this case we develop a structure theory that classifies the situations when P ∼ Q. The range of possible mixed equations is remarkably rich, and it is this fact that leads to the technical complexities of the proof. Nevertheless, the classification can be described with sufficient precision to allow the simplification step described above to be extended to mixed equations.

An overview of the structure theory is presented in Figure 1. For the few readers who wish to brave the full proof presented in later sections, we hope Fig-Mixed equation: F · G ∼ P_{1} | … | P_{n} (choose F to have smallest possible norm, so that F is not a sequential composition).

Monomorphic equation: F · (T | (F · T)^{n−1} ) ∼ (F · T)^{n}, where F is a “monomorphic atom” and T is any term (see Theorem 5.2).

F·X^{m} ∼ A_{1}·X^{m} | … | A_{n} ·X^{m} | X^{l}

(see Theorem 4.2(c)).

Mixed equation with a “series-parallel tail” (see Section 6).

Mixed equation with a non-series-parallel tail: F is an atom (see Theorem 8.6).

(T | X^{i}) · X^{m} ∼ T · X^{m} | X^{i}, where T is any term (see Lemma 6.7).

Pumpable equation: (F_{1} | H) · X^{m} ∼ (V | H) · X^{m} | R where F_{1} is a parallel prime, R = K^{e_{1}} · X^{m} | … | K^{e_{n−1}} · X^{m}, K is an “X-monomorphic term” and H is a product of “generalised K-primes” (see Theorem 7.18).

G / ∼ X^{m} G ∼ X^{m}

X · X ∼ X | X X · X / ∼ X | X

n = 1 n > 1

Figure 1: Outline of the structure theory for mixed equations ure 1 will provide a useful map; for the majority, Figure 1, taken in conjunction with the referenced theorems and Section 9, will probably prove sufficient.

4 Mixed equations: preliminaries and normal form

Our procedure for deciding bisimilarity in PA relies on having a complete classification of the circumstances in which a sequential composition of two processes can be bisimilar to a parallel composition.

Definition 4.1 A mixed equation is an equivalence of the form Mixed equation,

minimal mixed equation, unit.

F · G ∼ P_{1} | ⋯ | P_{n},  (3)

where P_{1}, …, P_{n} are parallel primes, and n ≥ 2. We say that (3) is a minimal mixed equation if ||F|| = 1; in this case, F is necessarily an atom of norm one, or unit. We reserve the letters X, Y and Z to stand for units.

Our basic normal-form theorem for mixed equations follows after technical lemma.

Lemma 4.1 Let T = P_{1} | P_{2} | ⋯ | P_{n} be a decomposition of a process T into parallel primes. If all the immediate reducts of T are bisimilar to each other then P_{1} ∼ P_{2} ∼ ⋯ ∼ P_{n} ∼ P, i.e., T ∼ P^{n} is a (parallel) power. Furthermore, P has a unique immediate reduct (up to bisimulation).

Proof. Let T′ be the unique immediate reduct on the l.h.s., so that T ) T′ with ||T′|| < ||T||. Let P_{i} and P_{j} be two factors on the r.h.s., and P ) P′_{i}, P ) P′_{j} be two immediate reducts. By assumption,

P_{1} | ⋯ | P′_{i} | ⋯ | P_{j} | ⋯ | P_{n} ∼ P_{1} | ⋯ | P_{i} | ⋯ | P′_{j} | ⋯ | P_{n},

and, by unique decomposition, P′_{i} | P_{j} ∼ P_{i} | P′_{j}. The prime process P_{i} is either bisimilar to the prime P_{j} or to a component of P′_{i}, and, since ||P′_{i}|| < ||P_{i}||, we must conclude the former. The final part of the lemma is again an easy consequence of unique factorisation.

Theorem 4.2 (a) In a minimal mixed equation, all the components on the Normal-form

theorem for mixed equations.

r.h.s. are bisimilar to each other:

Y · G ∼ P^{n} and G ∼ P′ | P^{n−1} ,  (4)

where P′ is the unique reduct of P.

(b) Every mixed equation can be reduced to a minimal mixed equation, which is unique up to bisimilarity.

(c) If ||F|| > 1 then there is a unit X such that G ∼ X^{m}, and each component P_{i} is bisimilar either to X or to a sequential composition of the form A · X^{m} (the same m as in the decomposition of G). Thus the normal form for mixed equations with ||F|| > 1 is

F · X^{m} ∼ A_{1} · X^{m} | ⋯ | A_{n} · X^{m} | X^{l}.  (5)

(d) The minimal equation obtained by reducing equation (5) is

Y · X^{m} ∼ X^{m+1} ,  (6)

where Y is a unit.

(e) Every immediate derivative of X is bisimilar either to some power of X, or to a sequential composition B · X^{m} (the same m as in the decomposition of G). In particular, if m ≥ max{||X′|| : X ) X′}, then every derivative of X is bisimilar to a power of X.

Proof. If ||F|| = 1 in equation (3) then F · G has a unique immediate reduct. By Lemma 4.1, the r.h.s. of equation (3) is a power. This gives part (a) of the lemma.

If ||F|| > 1 then reduce the r.h.s. for ||F|| − 1 steps, always selecting a component of largest norm. No component will disappear before they are all of norm 1, so that by the time the l.h.s. becomes Y · G, with Y a unit, the r.h.s. is still a parallel composition. Since the only immediate reduct on the l.h.s. is G, we conclude from Lemma 4.1 that the r.h.s. is a power:

Y · G ∼ Q^{n} and G ∼ Q′ | Q^{n−1} .  (7)

If an alternative derivation sequence leads to Ŷ· G on the l.h.s. and a parallel composition on the r.h.s., where Ŷ is a unit, then, for the same reasons,

Ŷ· G ∼ Q̂n̂ and G ∼ Q̂′ | Q̂^{n̂−1}.

Comparing the two expressions for G we see that Q ∼ Q̂ and n = n̂, since Q and Q̂ are both parallel primes. But then Y ∼ Ŷ also, by unique sequential decomposition of Q^{n} ∼ Q̂n̂ . This proves (b).

If ||F|| > 1, then in reducing F to Y the final step was F^{∗} ) Y, so that the original equation evolved into

F^{∗} · G ∼ Q_{1} | Q_{2} | ⋯ | Q_{r},  (8)

where we assume that the r.h.s. is fully factorised. Note that r ≥ 2, since the reduction was done in such a way as to preserve the parallel composition. By part (b), any reduction on the r.h.s. of (8) that retains its parallel form leads to minimal equation (7). Without loss of generality, we assume that Q_{1} ) Q′_{1} reduces (8) to the minimal equation, so that

Q′_{1} | Q_{2} | ⋯ | Q_{r} ∼ Q^{n}.

Hence Q_{2} ∼ Q. We shall show that ||Q|| = 1. Assume to the contrary that ||Q|| > 1. Then reducing Q_{2} in equation (8) also retains the parallel form on the r.h.s., so that also

Q_{1} | Q′_{2} | ⋯ | Q_{r} ∼ Q^{n},

which is impossible, since ||Q′_{2}|| < ||Q|| and Q is a parallel prime. Thus Q is a unit and we denote it by X. Clearly, G ∼ X^{m}, where m = ||G|| and the original equation (3) becomes

F · X^{m} ∼ P_{1} | ⋯ | P_{n}.

For each P_{i} we may eliminate on the right all the components except P_{i}. If ||P_{i}|| ≤ m we end up with X^{k} ∼ P_{i}, for some k ≤ m; and if ||P_{i}|| > m with F^{∗} · X^{m} ∼ P_{i}. This proves (c), with the component X^{l} accumulating all the components P_{i} with ||P_{i}|| ≤ m.

Part (d) is an easy exercise: reduce each A_{i} on the r.h.s. to ε, and then reduce X’s as necessary.

Finally, starting with equation (6), we analyse the possible derivatives of X. Assume that X ) X′, so that X^{m+1} ) X′ | X^{m} on the r.h.s. of (6). The l.h.s. follows with Y · X^{m} ) Y′ · X^{m}. Hence Y′ · X^{m} ∼ X′ | X^{m}. Now eliminate the X^{m} on the right to obtain either Y^{∗} · X^{m} ∼ X′ or X^{k} ∼ X′, for some k ≤ m. This completes part (e), and the proof of the lemma.

5 Monomorphic equations

The analysis of mixed equations of form (5), in which G is a power of a unit, requires considerable work, which we leave to later sections. In this section we analyse the complementary case, which turns out to be much more tractable. By Theorem 4.2(c), we already know that ||F|| = 1; however, more can be said.

Definition 5.1 We say that an atom is monomorphic if Y ) Y′ implies Monomorphic

atom. Y′ ∼ Y or Y′ ∼ ε.

Since Y is normed, ||Y|| = 1, so that only units may have this property.

Observation 5.1 It is easy to decide if an atom is monomorphic, and if two monomorphic atoms are bisimilar. For convenience, we may modify the productions, keeping only one atom from each equivalence class (under bisimilarity) of monomorphic atoms, so that the only derivatives of a monomorphic atom Y are Y and ε.

If Y is monomorphic then, for every term T and every n ≥ 2, the following mixed equation holds:

Y · (T | (Y · T)^{n−1} ) ∼ (Y · T)^{n}.  (9)

Definition 5.2 An equation of the form (9), with Y a monomorphic atom, Monomorphic

equation.

is called a monomorphic equation.

We shall see that this family includes all instances of mixed equations that are not of the form (5).

Sufficient Theorem 5.2 If G is not bisimilar to the power of a unit, then the mixed

condition for an equation to be monomorphic.

equation F · G ∼ P_{1} | ⋯ | P_{n} must be monomorphic: F is a monomorphic atom, P_{i} ∼ P ∼ F · T for some fixed T, and G ∼ T | (F · T)^{n−1} .

Proof. Since G is not the power of a unit, we know from Theorem 4.2(c) that ||F|| = 1, and from Theorem 4.2(a) that the r.h.s. is a power of some parallel prime P, i.e., F · G ∼ P^{n}. Moreover, P has a unique reduction P ) P′, leading to G ∼ P′ | P^{n−1} . Assume that F ) F̂ / ∼ ε, so that F · G ) F̂· G. The r.h.s. of the mixed equation responds with P ) P̂, leading to

F̂· G ∼ P̂| P^{n−1} .

Since this is again a mixed equation, and G is still not a power of an atom, we again conclude that ||F̂|| = 1, and the r.h.s. is a power with ||P̂|| = ||P||. Necessarily, P̂∼ P, so that the r.h.s., and hence the l.h.s., remains the same, up to bisimilarity. Thus F̂∼ F, and F is monomorphic. Note that our analysis also showed that if F ) F then P ) P, and if F ) ε then P ) P′; and since F has no other move, P has no other move. It is therefore easy to see that P ∼ F · P′. Thus every mixed equation is either of form (5) or (9).

As a corollary, we have a result that helps us analyse the situation when F in equation (5) is a sequential composition. (The bulk of the structure theory is concerned with the case of a parallel composition.)

Structure of Corollary 5.3 Consider the mixed equation

mixed equations with a sequential composition on the l.h.s.

(F_{1} · F_{2}) · X^{m} ∼ A_{1} · X^{m} | ⋯ | A_{n} · X^{m} | X^{l},  (10)

where the r.h.s. is a non-trivial (n + l ≥ 2) parallel prime decomposition. One of the following two situations obtains:

• F_{2}·X^{m} ∼ X^{m+k} and A_{i} ·X^{m} ∼ B_{i} ·X^{m+k} (with appropriately chosen B_{i} ), so equation (10) is equivalent to

F_{1} · X^{m+k} ∼ B_{1} · X^{m+k} | ⋯ | B_{n} · X^{m+k} | X^{l};

• equation (10) is monomorphic, i.e.,

F_{1} · (F_{2} · X^{m}) ∼ (A · X^{m})^{n},

where F_{1} is a monomorphic atom, A ∼ F_{1}·A′ (where A′ is the unique reduct of A), and

F_{2} · X^{m} ∼ A′ · X^{m} | (A · X^{m})^{n−1} .

Proof. Setting G = F_{2} · X^{m}, equation (10) becomes

F_{1} · G ∼ A_{1} · X^{m} | ⋯ | A_{n} · X^{m} | X^{l}.  (11)

If G is bisimilar to a power of a unit, say G ∼ Y^{m+k} where k = ||F_{2}||, then after some reductions, we discover that Y ∼ X. Starting with F_{1} · X^{m+k} on the l.h.s. and eliminating all but A_{i} · X^{m} on the r.h.s., we get F_{1}^{∗} · X^{m+k} ∼ A_{i} · X^{m}. (Note that ||F_{1}^{∗}|| > 0 since A_{i} · X^{m} is a parallel prime.) This deals with the first possibility.

If G is not bisimilar to a power of a unit, then equation (11) is a monomorphic equation by Theorem 5.2. Necessarily, A_{i} ·X^{m} is the P of Theorem 5.2, and F_{1} the F of that theorem.

6 Mixed equations with a series-parallel tail

If X is monomorphic then X · X ∼ X | X. This equation may also arise when X is not monomorphic, e.g., if X is defined by the transition rules

X )^{a} ε, X )^{b} X · X, and X )^{c} X | X.

This breeds some more mixed equations, such as

(A | X) · X^{3} ∼ A · X^{3} | X,

where A is any term.

Before classifying such equations, we shall present some useful alternative formulations of the “series-parallel” property X · X ∼ X | X.

Definition 6.1 For any atom X, an X-term is a term built from the atom X X-term, extended

X-term.

using the operations of sequential and parallel composition. An extended X-term is a term that is bisimilar to an X-term.

For any term T and action a ∈ Act, denote by δ_{a}(T) the set

δ_{a}(T) = {k : there exists T′ such that T )^{a} T′ and ||T′|| − ||T|| = k }. (12)

Lemma 6.1 Let T ≠ ε be an extended X-term. Then:

(a) δ_{a}(T) = δ_{a}(X), for all a ∈ Act;

(b) if all the immediate derivatives of X are extended X-terms, then all the immediate derivatives of T are extended X-terms.

Proof. For T an X-term, the claims are proved by structural induction. For T an extended X-term, part (a) holds because bisimulation preserves norm, and part (b) follows immediately from the definition of extended X-term.

Lemma 6.2 Let X be an atom. The following are equivalent statements of the series-parallel property:

(i) X · X ∼ X | X;

(ii) every derivative of X is an extended X-term;

(iii) two (extended) X-terms are bisimilar iff they have the same norm;

(iv) X satisfies a mixed equation

F · X^{m} ∼ A_{1} · X^{m} | ⋯ | A_{n} · X^{m} | X^{l},

(n may be 0), where m is bigger than the norm of any immediate derivative of X.

Proof. The equivalence of (i)–(iv) follows from the sequence of entailments:

(i) } (ii), (ii) } (iii), (iii) } (i), (iii) } (iv) and (iv) } (ii).

(i) } (ii): Assume to the contrary that X ⇝ T, where T is the derivative with smallest norm that is not an extended X-term. The sequence of moves X | X ⇝ X | T on the r.h.s. is matched on the l.h.s. by a sequence of moves X ⇝ S such that S · X ∼ X | T. (Note that the first X on the l.h.s. cannot disappear.) We now eliminate X to get S′ · X ∼ T. Since X ⇝ S′ and ||S′|| < ||T|| we conclude that S′ is an extended X-term. But then so is S′ · X and hence T, a contradiction.

(ii) } (iii): Observe that, by Lemma 6.1, the relation

{⟨T, S⟩ : ||T|| = ||S||, and T and S are both extended X-terms}

is a bisimulation.

(iii) } (i): This entailment is immediate.

(iii) } (iv): This follows from the equation X^{m} · X^{m} ∼ X^{m} | X^{m}, which holds for arbitrarily high m.

(iv) } (ii): This is just Theorem 4.2(e).

Corollary 6.3 Suppose X is a series-parallel atom, so that X · X ∼ X | X. Then:

(a) if T is an extended X-term then T ∼ X^{||T||};

(b) every subterm of an extended X-term is an extended X-term.

Proof. Part (a) is a special case of the equivalence of (i) and (iii) in Lemma 6.2.

Suppose that T is a minimal counterexample to part (b). If T = T_{1} · T_{2} then by the equivalence of (i) and (iii) in Lemma 6.2,

T ∼ \underbrace{X · X · · · · · X}_{||T|| copies},

so by unique sequential decomposition,

T_{1} ∼ \underbrace{X · X · · · · · X}_{||T_{1}|| copies} and T_{2} ∼ \underbrace{X · X · · · · · X}_{||T_{2}|| copies}:

Step 1: Let 𝒜(X) be the set of all atoms occurring as subterms in derivatives of X. Compute 𝒜(X) by forming the transitive closure of the following binary relation on atoms:

{⟨U, U′⟩ : U′ is a subterm in an immediate derivative of U}.

Step 2: Test, for all atoms U ∈ 𝒜(X) and all actions a ∈ Act, whether

δ_{a}(U) = δ_{a}(X),  (13)

where δ_{a} is as defined in (12); accept if equality (13) holds for all choices of U and a, and reject otherwise.

Figure 2: A procedure for deciding X · X ∼ X | X.

a contradiction to minimality. Similarly, if T = T_{1} | T_{2} then T ∼ X^{||T||} and hence, by unique parallel decomposition, T_{1} ∼ X^{||T_{1}||} and T_{2} ∼ X^{||T_{2}||}: again a contradiction.

In the light of Lemma 6.2 and Corollary 6.3, the series-parallel property ought to be easy to test. This is indeed so, and Figure 2 presents a decision procedure.

Lemma 6.4 The algorithm in Figure 2 correctly decides X · X ∼ X | X.

Proof. First suppose X is series-parallel, i.e., X · X ∼ X | X. For every U ∈ 𝒜(X) there is, by definition, some derivative T of X which contains U as a subterm. By the equivalence of (i) and (ii) in Lemma 6.2, T is an extended X-term, and hence, by Corollary 6.3, U ∼ X^{||U||}. Thus equality (13) is satisfied for all U ∈ 𝒜(X) and a ∈ Act, and the procedure accepts.

Conversely, suppose that the procedure accepts, so that equality (13) holds for all U ∈ 𝒜(X) and a ∈ Act. It is easy to check that the relation

{⟨T, X^{||T||}⟩ : T is a term such that X ⇝ T}

is a bisimulation. Thus X is series-parallel by the equivalence of (i) and (ii) in Lemma 6.2.

Definition 6.2 Let T be a term. The X-norm ||T||_{X} of T is the length of the X-norm,

X-reduction, X-reduct.

shortest norm-reducing sequence T ⇝ S, where S is an extended X-term. (Note that every step in the sequence is required to reduce the usual norm.) An (immediate) X-reduction of a term T is an (immediate) derivation T ) S that decreases both the (usual) norm and the X-norm, i.e., ||S|| < ||T|| and ||S||_{X} < ||T||_{X}. In this case, we say that S is an (immediate) X-reduct of T.

Note that if T is an extended X-term then ||T||_{X} = 0; otherwise, T has finite Xnorm ||T||_{X} ≤ ||T|| and there is at least one X-reduction of T. (The X-reduction necessarily reduces both norms by 1.)

Properties of Observation 6.5 The X-norm has similar properties to the norm:

X-norm.

(a) if T ∼ S then ||T||_{X} = ||S||_{X};

(b) ||T | S||_{X} = ||T||_{X} + ||S||_{X};

(c) ||T · S||_{X} ≥ ||T||_{X} + ||S||_{X};

(d) ||T · S||_{X} = ||T||_{X} if S is an X-term; in particular, in the equation

F · X^{m} ∼ A_{1} · X^{m} | ⋯ | A_{n} · X^{m} | X^{l}

we have ||F||_{X} = ||A_{1}||_{X} + ⋯ + ||A_{n}||_{X}.

X-unit, X-free. Definition 6.3 If ||K||_{X} = 1 we say that K is an X-unit. A term T is Xfree if its decomposition into parallel primes does not contain a component bisimilar to X, i.e., T cannot be expressed in the form T ∼ S | X for some S. We reserve the letter K (possibly subscripted) to stand for an X-unit.

Note that an X-unit may have norm greater than one, and is not in general an atom. The following lemma is a major tool in our analysis.

Lemma 6.6 Suppose X is series-parallel, i.e., X · X ∼ X | X.

(a) If K is an X-unit then it has a unique (up to bisimilarity) X-reduct K′; necessarily K′ is an X-term and hence K′ ∼ X^{||K||−1}.

(b) Suppose T ∼ P_{1} | P_{2} | ⋯ | P_{n} is a decomposition of a process T into parallel primes. If T is X-free and has a unique X-reduction (up to bisimilarity) then P_{1} ∼ P_{2} ∼ ⋯ ∼ P_{n}.

Proof. To see part (a), observe that all the X-reductions of K lead to an extended X-term with norm ||K|| − 1; by Corollary 6.3, all such terms are bisimilar to X^{||K||−1} and hence to each other.

For (b), note that each P_{i} has positive X-norm and a (unique) X-reduct P′_{i}. By assumption,

P′_{1} | ⋯ | P_{i} | ⋯ | P_{n} ∼ P_{1} | ⋯ | P′_{i} | ⋯ | P_{n},

for all i. By unique decomposition, P′_{1} | P_{i} ∼ P_{1} | P′_{i}, and P_{1} is a parallel component of P′_{1} | P_{i}. Since ||P_{1}|| > ||P′_{1}|| and P_{1} and P_{i} are prime, P_{1} ∼ P_{i}.

The sample mixed equation that opened the section is a special case of a general pattern.

Lemma 6.7 Suppose X is series-parallel. For every term T, and every i and m:

(T | X^{i}) · X^{m} ∼ T · X^{m} | X^{i}.  (14)

Proof. If S is an X-term then S·X^{m} ∼ X^{m} | S, by the equivalence of (i) and (iii) in Lemma 6.2. Hence the relation

{⟨(T | S) · X^{m}, T · X^{m} | S⟩ : S is an X-term and T is an arbitrary term}

is a bisimulation.

7 Pumpable equations

In this section we explore the series-parallel case further. Recall that, in the generic mixed equation (5), n stands for the number of components with positive X-norm on the r.h.s., and F denotes the first (sequential) component on the l.h.s. Lemma 6.7 gives a potentially infinite family of mixed equations with n = 1; as we shall see, there may be other infinite families of mixed equations with n ≥ 2.

Since Corollary 5.3 enables us to handle the cases where F is a sequential composition, we concentrate in this section on classifying the situations in which F is a parallel composition. It turns out that equations of this kind—the “pumpable equations” of the section title—have a rich and interesting structure.

Definition 7.1 Suppose X is series-parallel. A pumpable equation is a mixed

Pumpable equation.

equation of the form

(F_{1} | ⋯ | F_{r}) · X^{m} ∼ A_{1} · X^{m} | ⋯ | A_{n} · X^{m} | X^{l},  (15)

where r ≥ 2, n + l ≥ 2, and F_{i} and A_{j} are X-free for 1 ≤ i ≤ r and 1 ≤ j ≤ n.

The appropriateness of the terminology “pumpable equation” will become apparent towards the end of the section. Note that the assumption that F_{i} and A_{j} are X-free is harmless: by Lemma 6.7, if A_{j} ∼ Â_{j} | X then the factor X can be pulled out and incorporated into the X^{l} component. Similarly, if F_{i} ∼ F̂_{i} | X then, again by Lemma 6.7, X can be pulled out and cancelled with an X on the right (which must exist by unique decomposition).

In retrospect, the r.h.s. of (15) is a little too general, as X cannot in fact occur as a factor. For suppose l > 0; then we may apply the reduction X ) ε to the r.h.s., which, without loss of generality, is matched by F_{1} ) F′_{1} on the l.h.s.:

(F′_{1} | ⋯ | F_{r}) · X^{m} ∼ A_{1} · X^{m} | ⋯ | A_{n} · X^{m} | X^{l−1},

Then (parallel) composing both sides with X, and applying Lemma 6.7:

((F′_{1} | X) | F_{2} | ⋯ | F_{r}) · X^{m} ∼ A_{1} · X^{m} | ⋯ | A_{n} · X^{m} | X^{l}

By unique factorisation, F_{1} ∼ F′_{1} | X, contradicting X-freeness of F_{1}. We record this information for future reference.

Observation 7.1 In a pumpable equation, n (the number of parallel components with positive X-norm on the r.h.s.) is at least two, and l (the number of occurrences of X as a factor) is zero.

7.1 Basic facts

With the ultimate aim of brevity in mind, we slightly extend one of our earlier definitions.

X-simplification Definition 7.2 Suppose T is an X-free term. We say that an X-free term

of a term or equation, minimal pumpable equation, X-valence of a term.

S is an X-simplification of T, and write T )_{X} S, if there is an X-reduction T ) T′ ∼ S | X^{i} for some i (possibly zero). An X-simplification of an equation T_{1} ∼ T_{2} is a second equation S_{1} ∼ S_{2} obtained by applying bisimilaritypreserving X-simplifications T_{1} )_{X} S_{1} and T_{2} )_{X} S_{2} to the two sides. A pumpable equation is minimal if no X-simplification of it is a pumpable equation. The X-valence of a term T is the number of distinct (up to bisimulation equivalence) X-simplifications of T.

In operational terms an X-simplification of a pumpable equation may be achieved in three steps: (i) apply X-reductions to both sides, (ii) pull any parallel X components to the outer level using Lemma 6.7, and (iii) cancel any parallel X components that are common to the two sides.

Lemma 7.2 The form of pumpable equations is constrained as follows.

(a) There are no pumpable equations with X-norm less than three.

(b) There are no pumpable equations with a product of X-units on the l.h.s., i.e., with ||F_{i}||_{X} = 1, for all 1 ≤ i ≤ r.

(c) Every pumpable equation may be transformed by a series of X-simpli-fications to a minimal pumpable equation of X-norm three. This minimal equation is necessarily of the form

(F | K) · X^{m} ∼ K^{2} · X^{m} | K · X^{m},  (16)

with ||F||_{X} = 2 and ||K||_{X} = 1.

Proof. A pumpable equation trivially has X-norm at least two. To achieve this value, the equation would need to have the form

(F_{1} | F_{2}) · X^{m} ∼ A_{1} · X^{m} | A_{2} · X^{m},  (17)

with ||F_{1}||_{X} = ||F_{2}||_{X} = ||A_{1}||_{X} = ||A_{2}||_{X} = 1. Suppose, without loss of generality, that the X-simplification of equation (17) annihilating F_{1} on the l.h.s. also annihilates A_{1} on the r.h.s., so that

F_{2} · X^{m} ∼ A_{2} · X^{m},

and hence

F_{2} ∼ A_{2}.  (18)

In a similar fashion, by employing an X-simplification annihilating F_{2}, we deduce

F_{1} ∼ A_{1} or F_{1} ∼ A_{2},  (19)

and by annihilating A_{2},

F_{1} ∼ A_{1} or F_{2} ∼ A_{1}.  (20)

It follows easily from assertions (18–20) that F_{1} ∼ A_{1} and F_{2} ∼ A_{2}. But this is impossible, since the (usual) norm of the r.h.s. of equation (17) would then exceed that of the l.h.s. by m > 0. This deals with part (a).

Suppose, contrary to part (b) that

(F_{1} | ⋯ | F_{r}) · X^{m} ∼ A_{1} · X^{m} | ⋯ | A_{n} · X^{m},

where ||F_{i}||_{X} = 1 for 1 ≤ i ≤ r. Perform r − 2 X-simplifications, taking care to maintain at least two components of positive X-norm on the r.h.s. Note that this procedure maintains pumpability, but the X-norm of the resulting equation is just two, contradicting part (a).

Finally to part (c). A minimum pumpable equation must have the form

(F | K) · X^{m} ∼ A_{1} · X^{m} | A_{2} · X^{m},  (21)

with ||K||_{X} = ||A_{2}||_{X} = 1 and ||F||_{X} = ||A_{1}||_{X} ≥ 2, otherwise an X-simplification would be available. (If either side had three parallel components with positive X-norm, or two components of X-norm at least two, then we could X-reduce the component of largest X-norm on the other side.) Moreover, again by minimality, X-simplifications of F must be answered by A_{2}, and hence there is only one such (up to bisimilarity); and X-simplifications of A_{1} must be answered by K. We must show that ||F||_{X} = 2, A_{1} ∼ K^{2} and A_{2} ∼ K.

Applying the X-simplification that annihilates A_{2} and reduces F )_{X} F′ with ||F′||_{X} = ||F||_{X} − 1, we obtain

(F′ | K) · X^{m} ∼ A_{1} · X^{m},

and consequently A_{1} ∼ F′ | K. Now A_{1} has a unique X-simplification, so, by Lemma 6.6(b), A_{1} ∼ K^{t} and F′ ∼ K^{t−1}; moreover, t ≥ 2 by part (a) of this lemma.

Applying to equation (21) the X-simplification that annihilates K and reduces A_{1} )_{X} K^{t−1}, we obtain

F · X^{m} ∼ K^{t−1} · X^{m} | A_{2} · X^{m}.

Now a further X-simplification, annihilating a K on the r.h.s. and reducing F )_{X} F′ ∼ K^{t−1} on the l.h.s., yields

K^{t−1} · X^{m} ∼ K^{t−2} · X^{m} | A_{2} · X^{m}

if t > 2, and

K · X^{m} ∼ A_{2} · X^{m}

otherwise. By part (b) of this lemma, the former is impossible, and we must conclude that ||F||_{X} = ||A_{1}||_{X} = t = 2, A_{1} ∼ K^{2} and A_{2} ∼ K.

Uniqueness of Lemma 7.3 Let X-units.

(F_{1} | ⋯ | F_{r}) · X^{m} ∼ A_{1} · X^{m} | ⋯ | A_{n} · X^{m}

be a pumpable equation. All the ( X-free) X-units reachable by (iterated) X-simplification from F_{1}, …, F_{r} and A_{1}, …, A_{n} are bisimilar to some fixed X-unit, say K.

Proof. Throughout the proof, X-units will always be X-free. Suppose K is an X-unit reachable from some F_{i}. Perform repeated X-simplifications on the l.h.s. until only K · X^{m} remains; the r.h.s. must respond, so K must also reachable from some A_{j}. A similar argument applies in the other direction, so the set of X-units reachable from the l.h.s. is equal to the set reachable from the r.h.s. Call an equation heterogeneous if this set contains more than one element. We start by assuming that heterogeneous pumpable equations exist, and obtain a contradiction.

Consider a heterogeneous equation of minimum X-norm. Assume the F_{i} are ordered so that ||F_{1}||_{X} ≥ ||F_{2}||_{X} ≥ ⋯ ≥ ||F_{r}||_{X} and similarly for the A_{j}. Observe that r = 2 and ||F_{2}||_{X} = 1, otherwise we can perform an X-simplification on the r.h.s. that preserves heterogeneity and automatically retains the parallel form of the l.h.s. By an exactly similar argument, n = 2 (we know by Observation 7.1 that n ≥ 2) and ||A_{2}||_{X} = 1. So, with some renaming, the minimal counterexample must look like

(F | K) · X^{m} ∼ A · X^{m} | K̂· X^{m},  (22)

where K and K̂ are X-units, and ||F||_{X} = ||A||_{X} ≥ 2 by Lemma 7.2(a).

Consider an X-simplification F )_{X} F′ that preserves heterogeneity, i.e., F′ ⇝ K̃ where K̃ / ∼ K is an X-unit. By minimality, this X-simplification must be matched on the r.h.s. by K̂, and hence F′ is unique (up to bisimilarity). Now perform this X-simplification to obtain

(F′ | K) · X^{m} ∼ A · X^{m},

and hence A ∼ F′ | K. Write F′ ∼ H | K^{i} with i maximal (possibly zero), so that H does not contain K as a parallel component. Then

A ∼ H | K^{i+1}  (23)

We distinguish two cases, depending on whether or not K is bisimilar to K̂.

If K / ∼ K̂, then any X-simplification A )_{X} A′ that preserves parallel composition on the l.h.s. would contradict minimality, since preservation of heterogeneity is automatic. Thus there is a unique X-simplification to A′, which is answered by K. If H ≠ ε then equation (23) would formally have at least two X-simplifications: to H | K^{i} and to H′ | K^{i+1}, where H )_{X} H′ is any X-simplification of H. But these two are both bisimilar to A′ and hence to each other, i.e.,

H | K^{i} ∼ H′ | K^{i+1},

which is impossible since H does not contain K as a factor. Thus we conclude that H = ε and F′ ∼ K^{i}. But this is a contradiction, as F′ was chosen to preserve heterogeneity.

Finally suppose K̂∼ K, so that equation (22) becomes

(F | K) · X^{m} ∼ A · X^{m} | K · X^{m}.  (24)

There must exist an X-simplification A )_{X} A′ that preserves heterogeneity, i.e., A′ ⇝ K̃ with K̃ / ∼ K. Any such X-simplification that preserved the parallel form on the l.h.s. would contradict minimality, so there is a unique such reduction, which is matched by K on the l.h.s. Now return to equation (23). We know that ||H||_{X} ≥ 1, otherwise the only X-unit reachable from the r.h.s. is K, contradicting heterogeneity. If ||H||_{X} ≥ 2 then there is an X-simplification H )_{X} H′ ⇝ K̃ of H preserving reachability of K̃. In that case, the r.h.s. of equation (23) formally has at least two X-simplifications preserving reachability of K̃, namely H | K^{i} and to H′ | K^{i+1}. These two are both bisimilar to A′ and hence to each other, implying, as before, that H contains K as a parallel factor, contrary to its definition. The only remaining possibility is that ||H||_{X} = 1, which is equivalent to H ∼ K̃. Equation (24) then specialises to

(F | K) · X^{m} ∼ (K̃| K^{i+1}) · X^{m} | K · X^{m}.  (25)

The possibility i = 0 is ruled out by Lemma 7.2(c), so we may suppose i ≥ 1. Observe that there are three distinct (up to bisimulation equivalence) Xsimplifications on the r.h.s., induced by K̃)_{X} ε, K^{i+1} )_{X} K^{i} and K·X^{m} )_{X} ε. (In checking this observation, note that K^{i+1} · X^{m} and (K̃ | K^{i}) · X^{m} are both parallel primes by Lemma 7.2(b).) In other words, the r.h.s. of equation (25) has X-valence three, and so must the l.h.s. The X-simplification K^{i+1} )_{X} K^{i} applied to the r.h.s. of equation (25) preserves the X-valence of the r.h.s., and so cannot be matched by K )_{X} ε on the l.h.s., which reduces the X-valence from three to two. So we have an X-simplification that preserves heterogeneity, contradicting minimality of equation (22).

Lemma 7.3 associates a privileged X-unit K with each pumpable equation. This X-unit plays an important role in the structure theory, and we need to examine its properties further.

X-monomorphic Definition 7.3 An X-unit K is X-monomorphic if all derivations of K are

term.

of one of the two forms K ) K | X^{k} or K ) X^{k} (where k may be zero).

X-units do not Lemma 7.4 Let K be the privileged X-unit associated with some pumpable

grow.

equation. Then K has no X-norm-increasing moves. As an immediate consequence, K is X-monomorphic.

Proof. Consider the minimal equation (16), which we choose to write

(K_{(2)} | K) · X^{m} ∼ K^{2} · X^{m} | K · X^{m}.  (26)

We shall see in due course that the notation K_{(2)} is an instance of a general naming convention for a potentially infinite sequence of terms derived from K; the notation is introduced here only for consistency with later proofs, and the nature of the convention itself need not concern us for the moment. Suppose that some X-norm-increasing immediate derivative K ) H exists. There are two possible responses on the r.h.s. to applying K ) H to the l.h.s. of (26):

(K_{(2)} | H) · X^{m} ∼ K^{2} · X^{m} | Ĥ · X^{m}  (27)

and

(K_{(2)} | H) · X^{m} ∼ (K | Ĥ) · X^{m} | K · X^{m}.  (28)

We analyse these two possibilities in turn.

In case (27), apply the X-simplification K_{(2)} )_{X} K to the l.h.s., yielding a pumpable equation with (K | H) · X^{m} as its l.h.s. (Note that the r.h.s. must remain a parallel composition.) Now, by Lemma 8, the minimal form (26) may be regained by iterated X-simplification. The factor K_{(2)} on the l.h.s. can only have come from H, so there must be a derivation K ⇝ K_{(2)}, and consequently

K · X^{m} ⇝ K_{(2)} · X^{m} ∼ (K · X^{m})^{2}.  (29)

Therefore, for any n, starting with K·X^{m} and applying an appropriate sequence of derivations, we can get to a term that is syntactically of the form F · X^{m} but bisimilar to (K · X^{m})^{n}:

F · X^{m} ∼ (K · X^{m})^{n}.  (30)

If F is formally a sequential composition, then write F ∼ F_{1} · F_{2} with F_{1} a sequential prime. By Corollary 5.3, F_{2} ∼ X^{k} and K ∼ K̂· X^{k} for some k, and we may reformulate equation (30) be redefining F to be F_{1}, K to be K̂, and m to be m + k. (Note that the second possibility allowed by Corollary 5.3—that equation (30) is monomorphic—can be ruled out, as it is inconsistent with the assumption that K has X-norm-increasing moves.) We can therefore proceed under the assumption that F is not a formal sequential composition.

Can F be a formal parallel composition? If so, it would have to be the power of a parallel prime, since the X-valence of the r.h.s. of (30) is clearly one. By Lemma 7.2(b), the prime in question must have X-norm at least two. But then there is no X-simplification of the l.h.s. of (30) that preserves the property of having X-valence one, a contradiction.

The only remaining possibility is that F is an atom, but this too can be ruled out by choosing n sufficiently large (larger than the X-norm of any atom). This completes the analysis of case (27).

In case (28), apply the X-simplification K | Ĥ )_{X} Ĥ to the r.h.s., to obtain a pumpable equation with r.h.s. Ĥ · X^{m} | K · X^{m}. (Note that the parallel product on the l.h.s. must survive.) By Lemma 7.2(c), this r.h.s. is reducible, via a series of X-simplifications, to K^{2} · X^{m} | K · X^{m}. Since K^{2} · X^{m} is a parallel prime, it must be possible to reduce Ĥ · X^{m} ⇝ K^{2} · X^{m}, and hence Ĥ ⇝ K^{2}, again by a series of X-simplifications. Applying the pattern K ) Ĥ ⇝ K^{2} of derivations repeatedly to the r.h.s. of equation (26) yields an equation of the form

F · X^{m} ∼ (K^{n} · X^{m})^{2}.  (31)

for arbitrarily large n. As before, by adjusting F, K and m as necessary, we may assume that F is not a formal sequential composition.

Can F be a formal parallel composition? Again, it would have to be the power of a parallel prime, since the X-valence of the r.h.s. of (31) is one. Moreover the power would have to be a square, as the r.h.s. of (31) is able to regain the property of having valence one after just two X-simplifications:

(K^{n} · X^{m})^{2} )_{X} K^{n} · X^{m} | K^{n−1} · X^{m} )_{X} (K^{n−1} · X^{m})^{2}.  (32)

(Recall that by Lemma 7.2(b) the parallel prime of which the l.h.s. is a power has X-norm at least two.) By applying balanced X-simplifications of the form (32) repeatedly to the r.h.s. we arrive eventually at an equation of the form

P^{2} · X^{m} ∼ (K^{2} · X^{m})^{2},

which in one further step yields

(P | K) · X^{m} ∼ K^{2} · X^{m} | K · X^{m},

which we recognise as the minimal equation (26). Thus P ∼ K_{(2)}, and

K_{(2)}^{2} · X^{m} ∼ (K^{2} · X^{m})^{2}.

But this equation is incompatible with

K_{(2)} · X^{m} ∼ (K · X^{m})^{2}.

on (ordinary) norm grounds, as together they imply m = 0.

Finally, by taking n sufficiently large, we may rule out the remaining possibility, that F is an atom. This completes the analysis of case (28), and the proof.

Starting with an X-monomorphic X-unit K, we identify a sequence K_{(1)}, K_{(2)}, K_{(3)}, … of terms of increasing X-norm, of which K itself is the first element. When K is the privileged X-unit associated with some pumpable equation, the associated sequence plays a key role in elucidating the structure the equation.

Definition 7.4 Suppose X is a series-parallel atom, K an X-monomorphic

Generalised ; K-prime.

term, and m a positive integer. A term K_{(j)} of X-norm j is a generalised K-prime if it satisfies the equation

K_{(j)} · X^{m} ∼ (K · X^{m})^{j}.  (33)

Note that for sufficiently large j the term K_{(j)} may not be expressible in our language of terms; however, if K_{(j)} is expressible then it is unique (up to bisimilarity) by unique factorisation. Thus we may speak of “the” jth generalised K-prime K_{(j)}.

Our notation for generalised K-primes omits reference to m, since this number will always be clear from the context. We shall turn to the question of expressibility (or constructibility) of generalised K-primes after reviewing some of their elementary properties.

Observation 7.5 Let K be an X-monomorphic term, and K_{(j)} an associated generalised K-prime satisfying (33). Then:

(a) the unique X-simplification of K_{(j)} is K_{(j)} )_{X} K_{(j−1)};

(b) K_{(j)} is a parallel prime.

Proof. Glancing at (33), we see that the unique X-simplification of K_{(j)} · X^{m} is

K_{(j)} · X^{m} )_{X} (K_{(j)})′ · X^{m} ∼ (K · X^{m})^{j−1} ∼ K_{(j−1)} · X^{m}.

By unique factorisation, (K_{(j)})′ ∼ K_{(j−1)}, establishing (a).

Suppose K_{(j)} is not a parallel prime. Then, since K_{(j)} and K_{(j−1)} both have unique X-simplifications, K_{(j)} must be the power of some X-unit, say K_{(j)} ∼ K̂^{j}. Indeed, by performing j − 1 X-simplifications starting from (33) we find that K̂ ∼ K_{(1)} = K and, one step before that, K^{2} · X^{m} ∼ (K · X^{m})^{2}. But this is not possible on (ordinary) norm grounds, establishing (b).

Observation 7.5(b) justifies to some extent our chosen terminology. Concerning expressibility of generalised K-primes, Observation 7.5(a) allows two apparent possibilities: for a given X-monomorphic term K, either all generalised K-primes K_{(j)} are expressible, or there exists a k such that K_{(j)} is expressible if j ≤ k, and not otherwise. Both possibilities can in fact occur.

Lemma 7.6 Let K be an X-monomorphic term.

(a) If K ∼ Y · X^{i} for some monomorphic atom Y and integer i, then all generalised K-primes may be explicitly expressed using the recurrence K_{(1)} = Y · X^{i}, and K_{(j)} = Y · (K_{(j−1)} | X^{i+m} ) for all j ≥ 2.

(b) Otherwise, there is a maximum integer j for which K_{(j)} is expressible. This maximum j is bounded by the maximum norm of any atom.

Proof. Consider equation (33). If K_{(j)} is a formal sequential composition, then, by Corollary 5.3, either equation (33) is monomorphic, or K_{(j)} = F_{1} · F_{2}, where F_{2} ∼ X^{i}. Part (a) of the lemma covers the former case, and part (b) the latter.

In the monomorphic case, K has only the derivations K ) K and K ) X^{i}, where i = ||K|| − 1, and hence K ∼ Y · X^{i} for some monomorphic Y. The claimed expressions for K_{(j)} in terms of Y and X may be verified by explicit construction of the bisimulation relation: simply take all pairs

⟨⟨K_{(j)} · X^{m} | X^{l}, (K · X^{m})^{j} | X^{l}⟩ : j, l ∈ ℕ⟩

and all pairs that can be derived from these by applying Lemma 6.7. This deals with part (a).

In the non-monomorphic case, we may, by taking F_{1} as small as possible, assume that F_{1} is not a sequential composition. By Corollary 5.3, F_{2} ∼ X^{i} where i = ||F_{2}||, and F_{1} is a generalised K̂-prime satisfying

F_{1} · Xm̂ ∼ (K̂· Xm̂)^{j},

where K̂· X^{i} ∼ K and m̂ = i + m. Now F_{1} is not a sequential composition by construction, and not a parallel composition by Observation 7.5. Hence F_{1} is an atom, and its X-norm (and hence the X-norm of K_{(j)}) is bounded by the largest X-norm (and hence the largest norm) of any atom. This deals with part (b).

When we turn to algorithmic issues, we shall sidestep the question of expressibility of generalised K-primes by explicitly constructing them; that is, we shall add new atoms to represent the terms K_{(j)}, and new productions to represent their derivations. Lemma 7.6 assures that the number of new atoms we need to add is bounded.

Definition 7.5 Suppose X is a series-parallel atom and K an X-

Generalised ; K-term (of ; degree j).

monomorphic term. Let j be such that K_{(j)} is expressible. Then

ΠK_{(≤j)} = {K_{(j)}^{e_{j}} | K_{(j−1)}^{e_{j−1}} | ⋯ | K_{(1)}^{e_{1}} : (e_{j}, …, e_{1}) ∈ ℕ^{j} and e_{j} ≥ 1},

is the set of generalised K-terms of degree j, and

ΠK_{(∗)} = ⋃_{j}ΠK_{(≤j)}

where the union is over j for which K_{(j)} is expressible, is the set of generalised K-terms.

7.2 The left-hand side

The goal of this subsection is to show (Theorem 7.9) that the l.h.s. of a pumpable equation is necessarily of a certain form. In rough terms, the l.h.s. is of the form F · X^{m}, where F is “nearly” a generalised K-term. Our approach is via the study of equations in which F is precisely a generalised K-term, which are characterised in Lemma 7.8. First of all, though, a technical lemma.

Lemma 7.7 Let K be the privileged X-unit associated with some pumpable equation, and let K_{(1)} (= K), K_{(2)}, K_{(3)}, … be as in Definition 7.4. Suppose H is an X-free term that does not contain K_{(j′)} as a parallel component for any j′ < j. If (H | K_{(j)}) · X^{m} is a parallel composite (i.e., non-prime), then so is (H | K_{(j−1)}) · X^{m}. (Interpret K_{(0)} as ε here.)

Proof. Consider the prime decomposition ∏ _{i=1}^{n} A_{i} · X^{m} of (H | K_{(j)}) · X^{m}, ordered so that ||A_{1}||_{X} ≥ ||A_{2}||_{X} ≥ ⋯ ≥ ||A_{n}||_{X}. For (H | K_{(j−1)}) · X^{m} to be a parallel prime, we must have n = 2 and ||A_{2}||_{X} = 1, i.e., A_{2} ∼ K. Thus

(H | K_{(j)}) · X^{m} ∼ A_{1} · X^{m} | K · X^{m},  (34)

and the X-simplification K )_{X} ε on the r.h.s. is matched by K_{(j)} )_{X} K_{(j−1)} on the l.h.s. So A_{1} ∼ H | K_{(j−1)}, and by substitution into equation (34),

(H | K_{(j)}) · X^{m} ∼ (H | K_{(j−1)}) · X^{m} | K · X^{m}.  (35)

On (ordinary) norm grounds, j = 1 is not possible, so we may assume j ≥ 2. Since H does not contain K_{(j−1)} as a factor, the X-valence of (H | K_{(j−1)}) is at least as large as that of (H | K_{(j)}). So the X-simplification that annihilates the factor K · X^{m} on the r.h.s. of equation (35) must be a duplicate; i.e., a term bisimulation equivalent to (H | K_{(j−1)}) · X^{m} can be obtained by two formally distinct X-simplifications on the r.h.s. of (35), and one of these is an explicit parallel composition. But (H | K_{(j−1)}) · X^{m} ∼ A_{1} · X^{m}, which is supposed to be a parallel prime.

So provided we reduce the K_{(j)} factors on the l.h.s. of a pumpable equation in the correct order (smallest first), we guarantee to preserve parallel compositeness of the r.h.s.

Lemma 7.8 Let K be the privileged X-unit associated with some pumpable equation, and let ΠK_{(∗)} = ⋃_{j} ΠK_{(≤j)} be the corresponding set of generalised K-terms. Suppose F ∈ ΠK_{(≤j)}, and write F = K_{(j)}^{e} | H, where e ≥ 1, H ∈ ΠK_{(≤h)} and h < j.

(a) If e ≥ 2 then F · X^{m} is a parallel prime.

(b) If e = 1 then

F · X^{m} = (K_{(j)} | H) · X^{m} ∼ (K_{(j−1)} | H) · X^{m} | K · X^{m}.

(Note that if h < j − 1, the r.h.s. will factorise further.)

Proof. We start with the easier part (b). It is routine to verify that if we add the set of pairs

⟨⟨(K_{(j)} | H | X^{l}) · X^{m}, (K_{(j−1)} | H) · X^{m} | K · X^{m} | X^{l}⟩ : H ∈ ΠK_{(≤h)} and h < j⟩,

to the maximum bisimulation relation, the result is still a bisimulation (obviously the maximum one). The only interesting case is when K_{(j−1)} ) K_{(j−2)} | X^{k} on the r.h.s. If h < j − 1 then there is a valid response on the l.h.s., namely K_{(j)} ) K_{(j−1)} | X^{k}; otherwise, we finesse by instead applying the derivation K_{(j−1)} ) K_{(j−2)} | X^{k} to one of the copies of K_{(j−1)} that we know to exist within H (instead of the explicit K_{(j−1)} component), and matching that derivation by a similar one in the H on the l.h.s. This deals with part (b).

Part (a) is proved by contradiction. Suppose F = K_{(j)}^{e} | H provides a minimum (X-norm) counterexample, so that F · X^{m} is composite and e ≥ 2. In the light of Lemma 7.7, minimality of F implies H = ε and e = 2. So we must have

K_{(j)}^{2} · X^{m} ∼ ∏_{i=1}^{n} A_{i} · X^{m},

where n ≥ 2. The X-valence of the l.h.s. is one, so the r.h.s. is a prime-power:

K_{(j)}^{2} · X^{m} ∼ (A · X^{m})^{n}.  (36)

Letting A )_{X} A′ be the unique X-simplification of A, we have

(K_{(j)} | K_{(j−1)}) · X^{m} ∼ | \begin{matrix}(A · X^{m})^{n−1} , & if ||A||_{X} = 1; \\ (A · X^{m})^{n−1} | A′ · X^{m}, & otherwise. \end{matrix}

By minimality, K_{(j−1)}^{2} · X^{m} is a parallel prime, so either ||A||_{X} = 1 and n ≤ 3, or ||A||_{X} = 2 and n = 2. Equation (36) must be of one of two forms:

K^{2} · X^{m} ∼ (A · X^{m})^{2}

which is impossible by Lemma 7.2(b), or

K_{(2)}^{2} · X^{m} ∼ (A · X^{m})^{2},  (37)

which leads after one X-simplification to

(K_{(2)} | K) · X^{m} ∼ A · X^{m} | A′ · X^{m},

and after another to

K^{2} · X^{m} ∼ A · X^{m}.  (38)

(K_{(2)} )_{X} K on the l.h.s. must be matched by A′ )_{X} ε on the r.h.s., since we know that K^{2} · X^{m} is a parallel prime.) Substituting (38) into (37) yields

K_{(2)}^{2} · X^{m} ∼ (K^{2} · X^{m})^{2},

which, as we saw in the proof of Lemma 7.4, is impossible on (ordinary) norm grounds.

We are now in a position to state and prove the main theorem of the section, which gives rather precise information about the form of the l.h.s. of any pumpable equation.

General form of Theorem 7.9 Suppose

the l.h.s. of a pumpable equation.

(F_{1} | ⋯ | F_{r}) · X^{m} ∼ A_{1} · X^{m} | ⋯ | A_{n} · X^{m}

is a pumpable equation. Let K be the privileged X-unit associated with the equation, and let ΠK_{(∗)} = ⋃_{j} ΠK_{(≤j)} be the corresponding set of generalised K-terms, as in Definition 7.4. Assume that both sides of the equation are completely factored (so that, in particular, each F_{i} is a parallel prime) and that the factors are listed in order of non-increasing X-norm, ||F_{1}||_{X} ≥ ||F_{2}||_{X} ≥ ⋯ ≥ ||F_{r}||_{X}. Then ||F_{1}||_{X} > ||F_{2}||_{X} (i.e., F_{1} is the unique factor on the l.h.s. of largest X-norm), and F_{2} | ⋯ | F_{r} ∼ H ∈ ΠK_{(∗)} (i.e., each factor with the possible exception of the largest is bisimilar to K_{(j)} for some j).

Exceptional Proof. Call a factor F_{i} exceptional if it is not bisimilar to K_{(j)} for some j. The

factor, l.h.s.

proof is in two stages: (i) show that there can be at most one exceptional factor on the l.h.s., and then (ii) show that the exceptional factor, if it exists, must have strictly larger X-norm than all the others. This is enough to establish the theorem, since the case where all factors F_{i} are non-exceptional is covered by Lemma 7.8(b).

To prove first claim—that there can be at most one exceptional factor— we postulate a minimum X-norm counterexample and derive a contradiction. Minimality implies that the counterexample must have the form

(F_{1} | F_{2}) · X^{m} ∼ A_{1} · X^{m} | ⋯ | A_{n} · X^{m},  (39)

i.e., there are precisely two factors (both exceptional) on the l.h.s. (If there are additional exceptional factors, perform any X-simplification on the r.h.s. that preserves the parallel composition; if there are additional factors of the form K_{(j)}, apply an X-simplification to the smallest of them and appeal to Lemma 7.7.) We distinguish three cases.

Case I. Assume n ≥ 3, or n = 2 and ||A_{1}||_{X}, ||A_{2}||_{X} ≥ 2. In this case, any X-simplification on the l.h.s. of (39) preserves the parallel product on the r.h.s., and thus must destroy one of the exceptional factors on the l.h.s. Without loss of generality, assume that F_{1} )_{X} F′_{1} ∈ ΠK_{(≤j_{1})} and F_{2} )_{X} F′_{2} ∈ ΠK_{(≤j_{2})}, where j_{1} ≥ j_{2}. (Reverse the roles of F_{1} and F_{2} if necessary to obtain the inequality.) As we have observed, (F′_{1} | F_{2}) · X^{m} is a (parallel) composite, and the same must be true of (K_{(j_{2})} | F_{2}) · X^{m} by Lemma 7.7. In contrast, we know from Lemma 7.8(a) that (K_{(j_{2})} | F′_{2}) · X^{m} is a parallel prime, since K_{(j_{2})} occurs with exponent at least two. We conclude that

(K_{(j_{2})} | F_{2}) · X^{m} ∼ (K_{(j_{2})} | F′_{2}) · X^{m} | K · X^{m},

and further, by Lemma 7.8(b) and unique factorisation,

K_{(j_{2})} | F_{2} ∼ K_{(j_{2}+1)} | F′_{2}.

But the last equation contradicts the assumption that F_{2} is exceptional.

Case II. Assume that n = 2 and A_{2} ∼ K. (Note that this is the complement to Case I.) The form of the counterexample is now

(F_{1} | F_{2}) · X^{m} ∼ A · X^{m} | K · X^{m}.  (40)

We consider two complementary subcases.

Case IIa. To the Case II assumptions, add the further assumption F_{1} ∼ F_{2} ∼ F. Applying an X-simplification to A on the r.h.s. of (40) yields

(F | F′) · X^{m} ∼ A′ · X^{m} | K · X^{m},

where, by minimality, F′ ∈ ΠK_{(≤j)} for some j. In contrast, by Lemma 7.8(a), (F′ | F′) · X^{m} is a parallel prime. We conclude that

(F | F′) · X^{m} ∼ (F′ | F′) · X^{m} | K · X^{m}.

In the light of Lemma 7.8(b) and unique factorisation, the last equation contradicts the assumption that F_{2} is exceptional, just as in Case I.

Case IIb. To the Case II assumptions, add the further assumption F_{1} / ∼ F_{2}. Apply an X-simplification to the factor K·X^{m} on the r.h.s. of (40), and suppose, without loss of generality, that the response on the l.h.s. is F_{1} )_{X} F′_{1}, yielding

(F′_{1} | F_{2}) · X^{m} ∼ A · X^{m}.  (41)

Note that any X-simplification F_{2} )_{X} F′_{2} on the l.h.s. of (40) is matched on the r.h.s. by A, and hence the parallel composition on the r.h.s. is preserved. Minimality then implies F′_{2} ∈ ΠK_{(≤j_{2})} for some integer j_{2}.

If F_{1} has some other X-simplification F_{1} )_{X} F_{1}^{†} with F_{1}^{†} / ∼ F′_{1}, then the r.h.s. must respond with an X-simplification of A, again preserving the parallel composition on the r.h.s. Minimality then implies F_{1}^{†} ∈ ΠK_{(≤j_{1})} for some j_{1}, a situation we already ruled out in Case I. We conclude that the X-simplification F_{1} )_{X} F′_{1} is unique, up to bisimilarity.

Between equations (40) and (41) the X-valence of the r.h.s. (and hence of the l.h.s.) has decreased. This observation, combined with the fact that F_{1} has a unique X-simplification, implies F′_{1} ∼ F_{2}^{k} for some k ≥ 1. Thus, noting (41) and substituting for A in (40),

(F_{1} | F_{2}) · X^{m} ∼ F_{2}^{k+1} · X^{m} | K · X^{m},

which leads after one X-simplification to

(F_{1} | F′_{2}) · X^{m} ∼ (F_{2}^{k} | F_{2}^{†}) · X^{m} | K · X^{m},  (42)

where F_{2}^{†} ∈ ΠK_{(∗)}. (Recall that every X-simplification of F_{2} leads to a generalised K-term.) In k X-simplifications, the r.h.s. of (42) becomes

(F_{2}^{†})^{k+1} · X^{m} | K · X^{m},

which by Lemma 7.8(b) is bisimilar to H · X^{m} with H ∈ ΠK_{(∗)}. But the l.h.s. of (42) requires a sequence of at least k + 1 X-simplifications to achieve the same form. This contradiction eliminates the final case (Case IIb).

We have established that the l.h.s. of any pumpable equation contains at most one exceptional factor. In the second stage of the proof, we must show that the unique exceptional factor, if it exists, has larger X-norm than all the others. As in the first stage, we consider a minimum X-norm counterexample and obtain a contradiction. By Lemma 7.7 we know the minimum counterexample is of the form

(F | K_{(j)}) · X^{m} ∼ A_{1} · X^{m} | ⋯ | A_{n} · X^{m},  (43)

where F is a parallel prime that is not bisimilar to any K_{(j′)}, and has X-norm at most j. We distinguish two cases.

First, suppose that there is an X-simplification of F, say F )_{X} F′, that preserves the parallel composition on the r.h.s. of (43). Minimality entails F′ ∈ ΠK_{(≤j′)} for some j′ < j. Now reduce K_{(j)} to K_{(j′)} by a series of Xsimplifications; by Lemma 7.7, the parallel composition on the r.h.s. of (43) is preserved. On the other hand, one further X-simplification, that of F )_{X} F′, destroys the parallel composition on the r.h.s., by Lemma 7.8(a). Therefore, we must have

(F | K_{(j′)}) · X^{m} ∼ A · X^{m} | K · X^{m},  (44)

reducing in one X-simplification to

(F′ | K_{(j′)}) · X^{m} ∼ A · X^{m}.

By unique factorisation, A ∼ F′ | K_{(j′)}, and we may substitute for A in equation (44) to obtain

(F | K_{(j′)}) · X^{m} ∼ (F′ | K_{(j′)}) · X^{m} | K · X^{m}.

But this would imply, in the light of Lemma 7.8(b), that F ∈ ΠK_{(∗)}, a contradiction.

Finally suppose that there is no X-simplification of F that preserves the parallel composition on the r.h.s. of (43). Then F has a unique X-simplification, say F )_{X} F′, and we must have

(F | K_{(j)}) · X^{m} ∼ A · X^{m} | K · X^{m},

reducing in one X-simplification to

(F′ | K_{(j)}) · X^{m} ∼ A · X^{m}.

Thus, A ∼ F′ | K_{(j)} and

(F | K_{(j)}) · X^{m} ∼ (K_{(j)} | F′) · X^{m} | K · X^{m}.  (45)

The l.h.s. of (45) has X-valence two, whereas the r.h.s. has X-valence at least three, a contradiction. To verify the latter claim, note that, by Lemma 7.8(b), F′ / ∼ K_{(j)}, so that there must be at least two distinct X-simplifications of K_{(j)} | F′. The X-simplification of K on the r.h.s. of (45) leads to an outcome clearly distinct from either of these, since it leaves the r.h.s. as a parallel prime.

7.3 The right-hand side

The goal of this subsection is to show (Theorem 7.12) that the r.h.s. of a pumpable equation is necessarily of a certain form. In rough terms, the r.h.s. is “nearly” a parallel composition of terms of the form K^{t} · X^{m}. The approach is similar that adopted in the previous section: namely, we initially aim to characterise (in Lemma 7.11) those equations in which the r.h.s. is precisely a product of such terms. We start with a technical lemma. Call a component A · X^{m} on the r.h.s. of a pumpable equation exceptional if A ∉ ΠK_{(≤1)}, i.e., if Exceptional

factor, r.h.s.

it is not of the form K^{t} · X^{m} for some t.

Lemma 7.10 Let

(F_{1} | ⋯ | F_{r}) · X^{m} ∼ A_{1} · X^{m} | ⋯ | A_{n−1} · X^{m} | K^{t} · X^{m}

be a pumpable equation which has K^{t} · X^{m} as its smallest non-exceptional component on the r.h.s. (I.e., every A_{i} · X^{m} is either exceptional or is bisimilar to K^{s} · X^{m} with s ≥ t.) Suppose that the X-simplification K^{t} )_{X} K^{t−1} is applied to the r.h.s. The response on the l.h.s. satisfies the following condition: if the l.h.s. had a component F_{i} bisimilar to K before the X-simplification then it continues to have one after. As a consequence: (a) the parallel composition on the l.h.s. is preserved, that is, the new l.h.s. is of the form (F′_{1} | ⋯ | F′_{r′}) · X^{m} with r′ ≥ 2, and (b) at least one of the new prime components F′_{1} | ⋯ | F′_{r′} is bisimilar to K_{(j)} for some positive j. (Note that (b) holds even if n = 2 and t = 1 so that the parallel composition on the r.h.s. is destroyed).

Proof. If there are at least two components F_{i} bisimilar to K then the result is immediate. So suppose that F_{r} ∼ K and ||F_{r−1}||_{X} ≥ 2. (Assume that the components F_{i} are listed in order of non-increasing X-norm.) The X-simplification K^{t} )_{X} K^{t−1} on the r.h.s. cannot be matched by K ) ε on the l.h.s.: on the one hand, if t ≥ 2, the X-valence of the r.h.s. does not decrease, whereas the X-valence of the l.h.s. certainly does; on the other hand, if t = 1, the (ordinary) norm of the r.h.s. decreases by more (in fact an additive term m) than the norm of the l.h.s.

Rider (a) is immediate, since the destruction of the parallel composition on the l.h.s. would necessitate the annihilation of a unique factor bisimilar to K. Rider (b) is almost as easy. By Theorem 7.9 we know that the l.h.s. of the initial equation has at least one component bisimilar to K_{(j)} for some j. If j ≥ 2 then there is a component K_{(j)} or K_{(j−1)} after X-simplification; if j = 1 then at least one component bisimilar to K_{(1)} ∼ K must survive.

Lemma 7.11 Suppose

(F_{1} | ⋯ | F_{r}) · X^{m} ∼ ∏_{i=1}^{n} K^{e_{i}} · X^{m}  (46)

is a pumpable equation in which both sides are fully factored (i.e., F_{1}, …, F_{r} are all parallel primes), the F_{k} are in listed in order of non-increasing X-norm ||F_{1}||_{X} ≥ ||F_{2}||_{X} ≥ ⋯ ≥ ||F_{r}||_{X}, and the exponents e_{i} are also in nonincreasing order e_{1} ≥ e_{2} ≥ ⋯ ≥ e_{n}. Then r = e_{1} − e_{2} + 1 (in particular, e_{1} > e_{2}),

F_{1} · X^{m} ∼ (K^{e_{2}} · X^{m})^{2} | K^{e_{3}} · X^{m} | ⋯ | K^{e_{n}} · X^{m}.

and F_{2} ∼ F_{3} ∼ ⋯ ∼ F_{r} ∼ K. Moreover, for all e > e_{2} (and not just for e = e_{1}) it is the case that

(F_{1} | K^{e−e_{2}} ) · X^{m} ∼ K^{e} · X^{m} | K^{e_{2}} · X^{m} | K^{e_{3}} · X^{m} | ⋯ | K^{e_{n}} · X^{m}.

Proof. Consider the equation obtained from (46) by applying a sequence of e_{1} − e_{2} X-simplifications to the largest component K^{e_{1}} on the l.h.s.:

F̂· X^{m} ∼ (K^{e_{2}} · X^{m})^{2} | K^{e_{3}} · X^{m} | ⋯ | K^{e_{n}} · X^{m}.  (47)

We claim that F̂ is a parallel prime. (Later we shall argue that F̂ is in fact F_{1}.) Suppose to the contrary that F̂ is a (parallel) composite. Then, by repeated application of Lemma 7.10,

F̃· X^{m} ∼ (K^{e_{2}} · X^{m})^{2},

where F̃ is still a composite. The X-valence of the r.h.s. is one, so F̃ ∼ F^{s} for some parallel prime F and some exponent s ≥ 2. Furthermore, by Theorem 7.9, F ∼ K_{(j)} for some j. But this is impossible by Lemma 7.8(a).

Denote by ℱ the finite set of all non-increasing sequences of positive numbers f_{1} ≥ f_{2} ≥ ⋯ ≥ f_{ν} such that

K^{f_{1}} · X^{m} | K^{f_{2}} · X^{m} | ⋯ | K^{f_{ν}} · X^{m}

is reachable from the r.h.s. of (47) via some sequence of X-simplifications. For all (f_{1}, …, f_{ν}) ∈ ℱ denote by F[f_{1}, …, f_{ν}] the term satisfying

F[f_{1}, …, f_{ν}] · X^{m} ∼ K^{f_{1}} · X^{m} | K^{f_{2}} · X^{m} | ⋯ | K^{f_{ν}} · X^{m}.

(c.f., equation (47)). Note that F[f_{1}, …, f_{ν}] is well defined (up to bisimilarity) for any sequence (f_{1}, …, f_{ν}) ∈ ℱ. It is routine to verify—recall Lemma 7.4 at this point—that if we add the set of pairs

⟨⟨(F[f_{1}, …, f_{ν}] | K^{s}) · X^{m}, K^{f_{1}+s} · X^{m} | K^{f_{2}} · X^{m} | ⋯ | K^{f_{n}} · X^{m}⟩ :
s ∈ ℕ and (f_{1}, …, f_{ν}) ∈ ℱ⟩

to the maximum bisimulation relation, the result is still a bisimulation (obviously the maximum one). Now set ν = n, s = e_{1} − e_{2}, f_{1} = e_{2}, and f_{2} = e_{2}, …, f_{n} = e_{n}.

Now for the main result of the section, which provides a rather precise characterisation of the general form of the r.h.s. of a pumpable equation.

Theorem 7.12 Suppose General form of

the r.h.s. of a pumpable equation.

(F_{1} | ⋯ | F_{r}) · X^{m} ∼ A_{1} · X^{m} | ⋯ | A_{n} · X^{m}

is a pumpable equation, and let K be the privileged X-unit associated with the equation. Assume that both sides of the equation are completely factored (so that, in particular, each A_{i} · X^{m} is a parallel prime) and that the factors are listed in order of non-increasing X-norm, ||A_{1}||_{X} ≥ ||A_{2}||_{X} ≥ ⋯ ≥ ||A_{n}||_{X}. Then ||A_{1}||_{X} > ||A_{2}||_{X} (i.e., A_{1}·X^{m} is the unique factor on the r.h.s. of largest X-norm), and A_{2}, …, A_{n} ∈ ΠK_{(≤1)} (i.e., each factor with the possible exception of the largest is bisimilar to K^{t} · X^{m} for some t).

Proof. As with Theorem 7.9, the proof is in two stages. In the first stage, we prove by contradiction that the r.h.s. of a pumpable equation contains at most one exceptional factor. Consider a minimal (X-norm) counterexample to this claim. The number of exceptional factors cannot be greater than two, otherwise we could perform an X-simplification on the l.h.s. and obtain a smaller counterexample. Furthermore, there cannot be any non-exceptional factors by Lemma 7.10. So the minimum counterexample has the form

(F_{1} | ⋯ | F_{r}) · X^{m} ∼ A · X^{m} | B · X^{m}  (48)

where A · X^{m} and B · X^{m} are parallel primes, and A, B ∉ ΠK_{(≤1)}. Note in particular that ||A||_{X}, ||B||_{X} ≥ 2.

Apply some X-simplification to the l.h.s. of (48) that preserves the parallel composition on the l.h.s. Without loss of generality, the r.h.s. responds with A )_{X} A′. By minimality, one of the exceptional components on the r.h.s. must disappear, and so

A′ · X^{m} ∼ ∏_{i} K^{e_{i}} · X^{m}  (49)

for some finite sequence (e_{i}) of positive integers (possibly of length one). By Lemma 7.7, we may reduce A′ · X^{m} ⇝ ε via some sequence of X-simplifications that preserves the parallel composition on the l.h.s. Referring to equation (48), we have annihilated the component A · X^{m} on the r.h.s. while retaining the parallel composition on the l.h.s.; it follows by unique factorisation that B is a (parallel) composite. We distinguish three cases.

Case I. Assume r ≥ 3, or r = 2 and ||F_{r}||_{X} ≥ 2. In this case, any Xsimplification of B )_{X} B′ on the r.h.s. of (48) preserves the parallel product on the l.h.s., and by minimality must destroy one of the exceptional factors on the r.h.s. Thus

B′ · X^{m} ∼ ∏_{i} K^{f_{i}} · X^{m}  (50)

for some sequence (f_{i}). By Lemma 7.11,

B′ ∼ B̂ | K^{t} or B′ ∼ K^{t}  (51)

where B̂ is a parallel prime with ||B̂||_{X} ≥ 2.

Consider the (parallel) prime decomposition of B. (Recall that B is composite.) If the prime decomposition of B contains K as a factor, then it can contain at most one non-K factor, otherwise the X-simplification of B induced by K )_{X} ε will lead to a term B′ that is not of the form (51). Furthermore, if the prime decomposition of B does not contain K as a factor, then it must contain exactly two prime factors by similar reasoning. In this case, at least one of the two factors must be bisimilar to K_{(2)}, by Lemma 7.10. (There must be a factor bisimilar to K_{(j)}, for some j; and j must be two, otherwise there exists an X-simplification B )_{X} B′ with B′ not of the form (51)). These considerations reduce the possibilities for B to just two:

B ∼ B̃ | K_{(2)}  (52)

and

B ∼ B̃ | K^{s},  (53)

where s ≥ 1 and B̃ is a parallel prime not bisimilar to K. (In the case of (52) this claim follows from primality of B · X^{m} and Lemma 7.8; in the case of (53) from the assumption that B · X^{m} is exceptional.)

The second possibility (53) is easy to rule out. Consider the X-simplification B ∼ B̃ | K^{s} )_{X} B̃ | K^{s−1} ∼ B′. The term B′ · X^{m} ∼ (B̃ | K^{s−1}) · X^{m} must factor (non-trivially) as specified in (50). But then, by Lemma 7.11, (B′ | K) · X^{m} ∼ (B̃ | K^{s}) · X^{m} ∼ B · X^{m} would factor non-trivially. However, B · X^{m} is assumed to be a parallel prime.

With a little more work, the other possibility (52) may also be ruled out. Since any X-simplification B )_{X} B′ of B ∼ B̃ | K_{(2)} must lead to a term B′ of the form (51), it follows that there is a unique X-simplification of B̃, which is of the form B̃ )_{X} K^{u} for some u ≥ 1. Now consider the sequence of X-simplifications

B · X^{m} ∼ (B̃ | K_{(2)}) · X^{m})_{X} (B̃ | K) · X^{m} ∼ B′ · X^{m}  (54)
)_{X} (K^{u} | K) · X^{m} ∼ K^{u+1} · X^{m}.  (55)

The outcome (54) of the first X-simplification is a (non-trivial) parallel composition as specified in (50), whereas the outcome (55) of the second is manifestly a parallel prime (recall Lemma 7.8(a)). The only way this can occur is for

(B̃ | K) · X^{m} ∼ B′ · X^{m} ∼ K^{u+1} · X^{m} | K · X^{m}.

But, by Lemma 7.8,

K^{u+1} · X^{m} | K · X^{m} ∼ (K_{(2)} | K^{u}) · X^{m},

which implies B̃ ∼ K_{(2)} and u = 1. Thus B ∼ K_{(2)}^{2}. The same argument applies equally to A, yielding A ∼ K_{(2)}^{2}. Substituting A ∼ B ∼ K_{(2)}^{2} into (48), we obtain

F^{k} · X^{m} ∼ K_{(2)}^{2} · X^{m} | K_{(2)}^{2} · X^{m},

where ||F||_{X} ≥ 2 (by Lemma 7.2(b)) and k ≥ 2. (The r.h.s. has X-valence one, so all the components F_{i} on the l.h.s. must be bisimilar to each other.) But it is impossible for all F_{i} to have the same X-norm, by Theorem 7.9. This completes the analysis of Case I.

Case II. Assume that n = 2 and F_{2} ∼ K. (Note that this is the complement to Case I.) The form of the counterexample is now

(F | K) · X^{m} ∼ A · X^{m} | B · X^{m},  (56)

where F a prime with ||F||_{X} ≥ 2. We consider two complementary subcases.

Case IIa. To the Case II assumptions, add the further assumption A ∼ B, so that (56) becomes

(F | K) · X^{m} ∼ A · X^{m} | A · X^{m}.

The X-simplification K )_{X} ε reduces the X-valence of the l.h.s. but increases that of the r.h.s.

Case IIb. To the Case II assumptions, add the further assumption A / ∼ B. Without loss of generality assume that the X-simplification K )_{X} ε on the l.h.s. is matched by B on the r.h.s. Then there is an X-simplification A )_{X} A′ (in fact any one will do) which when applied to the r.h.s. preserves the parallel composition on the l.h.s.. As we argued at the outset of the proof, this fact implies B is a parallel composition. (By minimality, the prime factorisation of A′ · X^{m} contains no exceptional components; now annihilate these components one by one using Lemma 7.10.) But this time, we have a little more: by observation (b) in Lemma 7.10, B must contain K as a parallel component. Since B · X^{m} is exceptional, it must also contain a parallel component not bisimilar to K. So B has at least two X-simplifications, and one of these preserves the parallel composition on the l.h.s. So the argument we just applied to B applies equally to A: the (parallel) prime decomposition of A contains at least one component bisimilar to K, and at least one not bisimilar to K.

By minimality, every X-simplification A )_{X} A′ yields an A′ such that the prime decomposition of A′ · X^{m} contains no exceptional factors. (We use the assumption A / ∼ B here.) By Lemma 7.11, it follows that A ∼ Ã | K^{s}, where s ≥ 1 and Ã is a parallel prime not bisimilar to K. Now consider the particular X-simplification

A · X^{m} ∼ (Ã | K^{s}) · X^{m} )_{X} (Ã | K^{s−1}) · X^{m} ∼ ∏_{i} K^{e_{i}} · X^{m},

where the product at the far right is non-trivial. By Lemma 7.11,

A · X^{m} ∼ (Â | K^{s}) · X^{m} ∼ K^{e_{1}+1} · X^{m} | ∏_{i≥2} K^{e_{i}} · X^{m},

contradicting the assumption that A · X^{m} is a parallel prime. This completes Case II, and the first stage of the proof: we now know that there is at most one exceptional component on the r.h.s.

Now to the second stage. If there are no exceptional factors on the r.h.s. then, by Lemma 7.11, ||A_{1} · X^{m}||_{X} > ||A_{2} · X^{m}||_{X}. We know from the first stage that there is at most one exceptional factor. So it only remains to show that the exceptional factor, if it exists, has strictly larger X-norm than all the others. As usual, we consider a minimal (X-norm) counterexample and derive a contradiction. By Lemma 7.10, a minimal counterexample is necessarily of the form

(F_{1} | ⋯ | F_{r}) · X^{m} ∼ K^{t} · X^{m} | A · X^{m},  (57)

where A ∉ ΠK_{(≤1)}, and t = ||A||_{X}.

We distinguish two cases. First suppose that A has at least one Xsimplification, say A )_{X} A′ that preserves the parallel composition on the l.h.s. of (57). By minimality, A′ · X^{m} is a parallel composition (possibly trivial) of non-exceptional components—refer to equation (49)—in which the highest power of K is e_{1} < t. Using a sequence of X-simplifications, reduce K^{t} · X^{m} on the r.h.s. of equation (57) to K^{e_{1}} ·X^{m}. By Lemma 7.10, the response on the l.h.s. preserves the parallel composition. However, one further X-simplification on the l.h.s., namely A )_{X} A′, destroys the parallel composition, by Lemma 7.11. Therefore, at the penultimate step we must have

(F | K) · X^{m} ∼ K^{e_{1}} · X^{m} | A · X^{m},  (58)

reducing in the final X-simplification to

F · X^{m} ∼ (K^{e_{1}} · X^{m})^{2} | ∏_{i≥2} K^{e_{i}} · X^{m}.

But then, by Lemma 7.11,

(F | K) · X^{m} ∼ K^{e_{1}+1} · X^{m} | K^{e_{1}} · X^{m} | ∏_{i≥2} K^{e_{i}} · X^{m}.  (59)

Comparing equations (58) and (59), we see that A · X^{m} is non-exceptional, counter to assumption.

The second case—all X-simplifications of A in (57) destroy the parallel composition on the l.h.s.—is simpler to handle. Note that the X-simplification A )_{X} A′ is unique (up to bisimilarity). So the situation is

(F | K) · X^{m} ∼ K^{t} · X^{m} | A · X^{m},  (60)

reducing in one X-simplification to

F · X^{m} ∼ K^{t} · X^{m} | A′ · X^{m}.  (61)

The r.h.s. of equation (60) has X-valence two, which implies that the l.h.s. of (60) also has X-valence two, which in turn implies that the l.h.s. of (61) has X-valence one. This can only happen if the r.h.s. of (61) is a square, i.e., A′ ∼ K^{t}. But this is impossible on X-norm grounds, since ||A′||_{X} < ||A||_{X} = t.

7.4 The left hand knows what the right is doing

The previous two sections provided considerable information about the l.h.s. and r.h.s. of pumpable equations, considered in isolation. We now consider how derivations on the two sides are coordinated. This will lead to an effective inductive classification of all pumpable equations.

Lemma 7.13 Let The large

component on the l.h.s. responds to the small ones on the r.h.s.

(F_{1} | ⋯ | F_{r}) · X^{m} ∼ A_{1} · X^{m} | ⋯ | A_{n} · X^{m}  (62)

be any pumpable equation in completely factored form with components arranged in non-increasing order of X-norm. We know from Theorems 7.9 and 7.12 that F_{1} and A_{1} are the unique components of largest X-norm on the l.h.s. and r.h.s., respectively. Then any X-simplification of one of the n − 1 smallest components A_{j} · X^{m} on the r.h.s. is matched by an Xsimplification F_{1} )_{X} F′_{1} of the largest component on the l.h.s. Moreover, provided n ≥ 3 or ||A_{n}||_{X} ≥ 2, i.e., the parallel composition on the r.h.s. is preserved, the new largest component on the l.h.s. is to be found within the parallel components of F′_{1}.

Proof. First we demonstrate that the largest component F_{1} on the l.h.s. always responds to an X-simplification of any of the n−1 smallest components A_{j}·X^{m} on the r.h.s. Recall (Theorem 7.12) that each A_{j} for 2 ≤ j ≤ n is bisimilar to K^{t} for some t. Consider a counterexample of smallest X-norm:

(F_{1} | H) · X^{m} ∼ W · X^{m} | K^{t} · X^{m},  (63)

where H = F_{2} | ⋯ | F_{r} ∈ ΠK_{(∗)} and the X-simplification K^{t} )_{X} K^{t−1} on the r.h.s. is matched by H )_{X} H′ on the l.h.s. (To see that it is possible to collect together the remaining n−1 components on the r.h.s. of 62 into the one term W · X^{m}, simply annihilate A_{j} · X^{m} ∼ K^{t} · X^{m} on the r.h.s. via a sequence of X-simplifications, and observe the response on the l.h.s.) We distinguish two cases.

If t = 1 then equation (63) specialises to

(F_{1} | H) · X^{m} ∼ W · X^{m} | K · X^{m}.  (64)

In one X-simplification we reach

(F_{1} | H′) · X^{m} ∼ W · X^{m}

(H responds because (64) is a counterexample), implying W ∼ F_{1} | H′. Note that by Lemma 7.10(a) ||H′||_{X} ≥ 1, and hence ||H||_{X} ≥ 2; moreover, we have the option of applying a further X-simplification H′ )_{X} H′′ to H′. Substituting for W in (64) yields

(F_{1} | H) · X^{m} ∼ (F_{1} | H′) · X^{m} | K · X^{m}.  (65)

Now apply the sequence of X-simplifications

(F_{1} | H′) · X^{m} | K · X^{m} )_{X} (F_{1} | H′′) · X^{m} | K · X^{m} )_{X} (F_{1} | H′′) · X^{m}

to the r.h.s. of (65). Since ||F_{1}||_{X}, ||H||_{X} ≥ 2, the l.h.s. after the first Xsimplification is a parallel composition; moreover its largest component has X-norm at most ||F_{1}||_{X}. By Lemma 7.10(a), the l.h.s. after the second Xsimplification is also a parallel composition, and by minimality of the counterexample, its largest component has X-norm strictly less than ||F_{1}||_{X}. But this is inconsistent with the r.h.s. being (F_{1} | H′′) · X^{m}.

If t ≥ 2, then write H as Ĥ | K^{s} with s maximal (so that Ĥ does not contain K as a parallel component). Because (63) is a counterexample, the X-simplification K^{t} )_{X} K^{t−1} on the r.h.s. is matched by H )_{X} H′ on the l.h.s. By considering the change in ordinary norm, we see that it is K^{s} that responds and not Ĥ. (When j ≥ 2, the X-simplification K_{(j)} )_{X} K_{(j−1)} reduces the ordinary norm by ||K|| + m.) So starting at

(F_{1} | Ĥ | K^{s}) · X^{m} ∼ W · X^{m} | K^{t} · X^{m},  (66)

we reach, after one X-simplification,

(F_{1} | Ĥ | K^{s−1}) · X^{m} ∼ W · X^{m} | K^{t−1} · X^{m}.  (67)

By minimality of the counterexample, a further X-simplification yields

(F′_{1} | Ĥ | K^{s−1}) · X^{m} ∼ W · X^{m} | K^{t−2} · X^{m}.  (68)

Consider what happens if the order of the X-simplifications on the l.h.s. is reversed, so that F_{1} )_{X} F′_{1} is applied first and K^{s} )_{X} K^{s−1} second. The order of events on the l.h.s. is now

(F_{1} | Ĥ | K^{s}) · X^{m} )_{X} (F′_{1} | Ĥ | K^{s}) · X^{m} )_{X} (F′_{1} | Ĥ | K^{s−1}) · X^{m}.

The end result is of course equation (68). Note, however, that the l.h.s. at the intermediate stage differs according to the order of the X-simplifications, since

F_{1} | Ĥ | K^{s−1} / ∼ F′_{1} | Ĥ | K^{s}.  (69)

(The component F_{1} on the l.h.s. has strictly greater X-norm than any appearing on the r.h.s.) Consider how the r.h.s. must respond. Since (68) has fewer copies of K^{t} · X^{m} on the r.h.s. than (66), at least one of the two X-simplifications on the r.h.s. in passing from (66) to (68) must be K^{t} · X^{m} )_{X} K^{t−1} · X^{m}. It cannot be the first, by (69), nor the second, by minimality of the counterexample: a contradiction.

We have shown that in one X-simplification from equation (63) we reach

(F′_{1} | H) · X^{m} ∼ W · X^{m} | K^{t−1} · X^{m};  (70)

it remains to show that F′_{1} continues to contain the largest component on the l.h.s., provided the parallel composition on the r.h.s. remains non-trivial. Assume that this is not the case, i.e., that H contains a component of strictly larger X-norm than any in F′_{1}. By Theorem 7.9, F′_{1} ∈ ΠK_{(∗)}, and hence F′_{1} | H ∈ ΠK_{(∗)}; thus equation (70) is covered by Lemma 7.8.

Suppose first that t ≥ 2. Since the unique largest component is now contained within H, we have, after one further X-simplification,

(F′_{1} | H′) · X^{m} ∼ W · X^{m} | K^{t−2} · X^{m}.

Consider what happens when the X-simplifications on the l.h.s. of (63) are performed in the reverse order

(F_{1} | H) · X^{m} )_{X} (F_{1} | H′) · X^{m} )_{X} (F′_{1} | H′) · X^{m}.

As we observed earlier, the intermediate stage differs according to the order of X-simplifications, since F_{1} | H′ / ∼ F′_{1} | H. The r.h.s. cannot evolve in the same way as before, and the only alternative is that there is a component K^{t−1} · X^{m} on the r.h.s. of (63), and that K^{t−1} · X^{m} )_{X} K^{t−2} · X^{m} is performed first and then K^{t} · X^{m} )_{X} K^{t−1} · X^{m}. But this is impossible, as the X-simplification K^{t−1} · X^{m} )_{X} K^{t−2} · X^{m} must be matched by F_{1}.

Finally suppose t = 1. Then W ∼ F′_{1} | H ∈ ΠK_{(∗)} and

(F_{1} | H) · X^{m} ∼ W · X^{m} | K · X^{m}.

Matching this equation against Lemma 7.8 we see that F_{1} | H ∈ ΠK_{(∗)}. In particular, F_{1} is a generalised K-prime with a unique X-simplification F_{1} )_{X} F′_{1} to another generalised K-prime F′_{1} whose X-norm is at least as large as any component of H, contradicting our assumption that the largest component has passed to H.

To continue our investigations of the coordination of the two sides of a pumpable equation, it is convenient to work with a form of the equation in which the two sides of the equation are not necessarily fully factored:

(F | H) · X^{m} ∼ W · X^{m} | R,  (71)

where

R = ∏_{i} K^{e_{1}} · X^{m}.  (72)

and H ∈ ΠK_{(∗)}. The components F on the l.h.s. and W · X^{m} on the r.h.s. are in general parallel composites, but we insist that the factorisation of F contains the unique largest component on the l.h.s., and W · X^{m} the unique largest component on the r.h.s.

Lemma 7.14 Consider any pumpable equation in partially factored form (71), where F and W · X^{m} contain, as factors, the unique largest components on the l.h.s. and r.h.s., respectively. Then W contains H as a factor, so that W ∼ V | H for some V, and equation (71) can be rewritten as

(F | H) · X^{m} ∼ (V | H) · X^{m} | R.  (73)

Proof. Apply any X-simplification to R on the r.h.s. of (71); by Lemma 7.13, it is F on the l.h.s. that responds. Furthermore, by the same lemma, the new largest component is contained in the derivative of F, provided R does not vanish. Repeating this argument ||R||_{X} times we see that H remains unscathed, giving (F^{∗} | H) · X^{m} ∼ W · X^{m}.

Lemma 7.15 Consider a partially factored pumpable equation in the form

Deflating a pumpable equation.

(73). Let H )_{X} H′ be any X-simplification of H. Then

(F | H′) · X^{m} ∼ (V | H′) · X^{m} | R.  (74)

Moreover, provided ||H||_{X} ≥ 2, the largest component on the r.h.s. remains in (V | H′) · X^{m}.

Proof. Recall (Theorem 7.9) that H ∈ ΠK_{(∗)}. We first show that any Xsimplification H )_{X} H′ applied to one side of (73) is matched by the same X-simplification on the other. Suppose (73) is a minimum X-norm counterexample: more precisely, there is a generalised K-prime K_{(j)} occurring in H such that the X-simplifications K_{(j)} )_{X} K_{(j−1)} applied to H on the two sides of (73) do not match, as required by (74).

Re-express equation (74) as

(S | K_{(j)}^{s}) · X^{m} ∼ (T | K_{(j)}^{t}) · X^{m} | R,  (75)

where S | K_{(j)}^{s} ∼ F | H, T | K_{(j)}^{t} ∼ V | H, and S and T do not contain K_{(j)} as a factor. Note that t ≥ s, by Lemma 7.14. In one X-simplification from (75) we arrive at

(S | K_{(j)}^{s−1} | K_{(j−1)}) · X^{m} ∼ (T′ | K_{(j)}^{t}) · X^{m} | R

(K_{(j)}^{t} does not respond, since (75) is a counterexample, and R does not respond by Lemma 7.13), and in one further X-simplification we arrive at one of two possibilities:

(S | K_{(j)}^{s−2} | K_{(j−1)}^{2}) · X^{m} ∼ (T′ | K_{(j)}^{t−1} | K_{(j−1)}) · X^{m} | R  (76)

(the counterexample was minimal). Alternatively, starting at (75), we may arrive in one X-simplification at

(S′ | K_{(j)}^{s}) · X^{m} ∼ (T | K_{(j)}^{t−1} | K_{(j−1)}) · X^{m} | R  (77)

(again, because (75) is a counterexample), and in one further X-simplification at

\begin{matrix}(S′′ | K_{(j)}^{s}) · X^{m} \\ (S′ | K_{(j)}^{s−1} | K_{(j−1)}) · X^{m} \end{matrix}\ ∼ (T′ | K_{(j)}^{t−1} | K_{(j−1)}) · X^{m} | R.  (78)

Now compare equations (76) and (78), and note that the r.h.s’s are identical. However, whichever variant of equation (78) is taken, the l.h.s. of (78) has at least one more copy of K_{(j)} than the l.h.s. of (76), a contradiction.

Finally, we need to show, under the assumption ||H||_{X} ≥ 2, that the largest component on the r.h.s. stays with (V | H′) · X^{m} and does not pass to R. Suppose to the contrary that the largest (X-norm) component of (V | H′) · X^{m} is no bigger than the largest component of R. Then, by Theorem 7.12, the r.h.s. of (74) consists only of non-exceptional factors, so that

(V | H′) · X^{m} ∼ ∏_{k} K^{f_{k}} · X^{m},

for some non-increasing sequence (f_{k}), and R is as in (72) with (e_{i}) nonincreasing. Note that f_{1} ≤ e_{1}. Starting with (73), apply a sequence of Xsimplifications to R to yield a parallel composition R^{∗} of non-exceptional factors, whose largest factor has X-norm f_{1}. By Lemma 7.13, it is F that responds on the l.h.s.:

(F^{∗} | H) · X^{m} ∼ (V | H) · X^{m} | R^{∗}.

Now apply the X-simplification H )_{X} H′ to the r.h.s.; the largest factor on the r.h.s. occurs to a power at least two, so, by Lemma 7.11, the l.h.s. is a parallel prime. But this is not possible, as ||F^{∗}||_{X}, ||H||_{X} ≥ 2.

Lemma 7.16 Consider a pumpable equation in the form (73), where H ∈ ΠK_{(≤h)} Suppose H^{∗} is any generalised K-term reachable via some sequence of X-simplifications from H. Then

(F | H^{∗}) · X^{m} ∼ (V | H^{∗}) · X^{m} | R;

in particular,

(F | K_{(h)}) · X^{m}∼ (V | K_{(h)}) · X^{m} | R,

and

F · X^{m} ∼ V · X^{m} | R.

Proof. Apply Lemma 7.15 repeatedly.

7.5 The general form

We now show that Lemma 7.16 has a kind of converse; this will allow us to deduce that any pumpable equation, however complex, may be obtained from a relatively simple base equation by adding generalised K-primes evenly to the two sides. This construction justifies the choice of the name “pumpable” for this class of mixed equation.

Lemma 7.17 Consider a pumpable equation in the form (73), specialised

Inflating a pumpable equation.

to the case when H is a generalised K-prime:

(F | K_{(h)}) · X^{m} ∼ (V | K_{(h)}) · X^{m} | R.  (79)

Note that the equation is not necessarily completely factored, but that the unique largest prime components on the l.h.s. and r.h.s. are contained in F and (V | K_{(h)}) · X^{m}, respectively. Then, for any H ∈ ΠK_{(≤h)},

(F | H) · X^{m} ∼ (V | H) · X^{m} | R.  (80)

Furthermore, bisimulation preserving derivations of (80) are independent of H: thus if F makes a derivation on the l.h.s. (or one of V or H makes a derivation on the r.h.s.) then the response on the other side is independent of H.

Proof. Fix the X-monomorphic term K. We claim that if we add the set of pairs

𝒫 = ⟨⟨(F | H) · X^{m}, (V | H) · X^{m} | R⟩ : h ∈ ℕ^{+}, H ∈ ΠK_{(≤h)},
and F, V, R satisfy (F | K_{(h)}) · X^{m} ∼ (V | K_{(h)}) · X^{m} | R⟩

to the maximum bisimulation relation, the result is still a bisimulation (obviously the maximum one). It is to be understood that the equation

(F | K_{(h)}) · X^{m} ∼ (V | K_{(h)}) · X^{m} | R

appearing in the definition of 𝒫 is of the form (73); specifically, F and (V | K_{(h)}) · X^{m} satisfy the conditions placed upon them in the statement of the lemma. We need to check that for each pair ⟨P, Q⟩ ∈ 𝒫 and each derivation P ) P′ there is a derivation Q ) Q′ such that (P′, Q′) ∈ 𝒫 ∪ ∼, and similarly with the roles of P and Q reversed.

Take a typical pair

⟨(F | H) · X^{m}, (V | H) · X^{m} | R⟩ ∈ 𝒫,  (81)

corresponding to a bisimilar base pair

(F | K_{(h)}) · X^{m} ∼ (V | K_{(h)}) · X^{m} | R.  (82)

Case R. Consider first a derivation R ) R′ applied to the r.h.s. of (81). Recall that, by Theorem 7.12, R is a parallel composition of non-exceptional factors of the form K^{t}·X^{m}. The only interesting derivations for us are X-norm decreasing ones (the others leave the r.h.s. unchanged modulo the creation or destruction of powers of X). Suppose, then that R )_{X} R′ is some X-simplification of R. By Lemma 7.13, this X-simplification applied to the r.h.s. of (82) is matched on the l.h.s. by F )_{X} F′:

(F′ | K_{(h)}) · X^{m} ∼ (V | K_{(h)}) · X^{m} | R′.

Then, by definition of 𝒫,

⟨(F′ | H) · X^{m}, (V | H) · X^{m} | R′⟩ ∈ 𝒫.

Case H. Next consider a derivation H ) H′ applied to the r.h.s. of (81). Again, the only interesting case is the X-norm decreasing one. Suppose then that H )_{X} H′ is some X-simplification of H. If H′ ∈ ΠK_{(≤h)} then it is immediate from (82) and the definition of 𝒫 that

⟨(F | H′) · X^{m}, (V | H′) · X^{m} | R⟩ ∈ 𝒫.  (83)

Otherwise, H′ ∈ ΠK_{(≤h−1)}; but then, by Lemma 7.15, we have

(F | K_{(h−1)} ) · X^{m} ∼ (V | K_{(h−1)} ) · X^{m} | R,

leading once more to (83).

Case V. Now consider a derivation V ) V′ applied to the r.h.s. of (81). Recall that V may be a parallel composite. If the derivation V ) V′ induces a reduction of an instance of K_{(h)} in V, then finesse by using the copy of K_{(h)} in H in place of the one in V. This reduces us to Case H. Otherwise, by Lemma 7.15, the derivation V ) V′ on the r.h.s. of (82) is matched by F ) F′ on the l.h.s., yielding

(F′ | K_{(h)}) · X^{m} ∼ (V′ | K_{(h)}) · X^{m} | R.  (84)

Provided we can assure ourselves that the largest components on the l.h.s. and r.h.s. remain with F′ and (V′ | K_{(h)}) · X^{m},

⟨(F′ | H) · X^{m}, (V′ | H) · X^{m} | R⟩ ∈ 𝒫

will follow from the definition of 𝒫. It is easy to see that the largest component on the l.h.s. remains with F. For if not, the l.h.s. would be composed entirely of generalised K-primes (Theorem 7.9); but then (Lemma 7.8) the r.h.s. cannot contain an occurrence of K_{(h)}.

As for the r.h.s. suppose to the contrary that the largest (X-norm) component of (V′ | K_{(h)}) · X^{m} is no bigger than the largest component of R. Then, by Theorem 7.12, the r.h.s. of (84) consists only of non-exceptional factors, so that

(V′ | K_{(h)}) · X^{m} ∼ ∏_{k} K^{f_{k}} · X^{m},

for some non-increasing sequence (f_{k}), and R is as in (72) with (e_{i}) nonincreasing. Note that f_{1} ≤ e_{1}. We proceed as in the proof of Lemma 7.15. Starting with (82), apply a sequence of X-simplifications to R to yield a parallel composition R^{∗} of non-exceptional factors, whose largest factor has X-norm f_{1}. By Lemma 7.13, it is F that responds on the l.h.s.:

(F^{∗} | K_{(h)}) · X^{m} ∼ (V | K_{(h)}) · X^{m} | R^{∗};

moreover, ||F^{∗}||_{X} > h ≥ 1. Now apply the X-simplification V )_{X} V′ to the r.h.s.; as this is matched by F^{∗}, which has norm at least two, the parallel composition on the l.h.s. is preserved. However, the largest factor on the r.h.s. occurs to a power at least two, so, by Lemma 7.11, the l.h.s. is a parallel prime, a contradiction.

Case F. The situations that occur as a result of the derivation F ) F′ have already been analysed under Case R and Case V.

Case F exhausts the possibilities and concludes the proof.

Ideally we would like a stronger version of Lemma 7.17 in which the basis equation (79) is replaced by the the simpler equation

F_{1} · X^{m} ∼ V · X^{m} | R;  (85)

but such a strengthening would not be valid unless complex side conditions were placed on V. Nevertheless, the classification of pumpable equations that follows from Lemmas 7.16 and 7.17 will prove adequate, if we exercise care.

General form of a Theorem 7.18 The general form of pumpable equation is

pumpable

equation. (F | H) · X^{m} ∼ (V | H) · X^{m} | R  (86)

where H ∈ ΠK_{(≤h)} for some h, and R is a product (72) of non-exceptional components; furthermore, the largest parallel prime factor of F has norm greater than h and the other factors of F (if any) are generalised Kprimes; finally, the term (V | H) · X^{m} contains the largest parallel prime factor on the r.h.s. The terms F, V and R satisfy

(F | K_{(h)}) · X^{m} ∼ (V | K_{(h)}) · X^{m} | R,  (87)

and equation (86) holds for all H ∈ ΠK_{(≤h)}. Furthermore, bisimulation preserving derivations of (80) are independent of H, as in Lemma 7.17.

Proof. Equations (87) follows from (86) by Lemma 7.16. Then equation (86) for general H ∈ ΠK_{(≤h)} follows from (87) by Lemma 7.17. (Note that the largest factor on the r.h.s. of (87) remains with (V | K_{(h)}) · X^{m} by Lemma 7.15.)

The key feature of Theorem 7.18 is that it allows us to represent the infinite family of equations of the form (86)—with F, V and R fixed, and H ranging over ΠK_{(≤h)}—by a single “schema” with “contexts” on either side into which an arbitrary term H ∈ ΠK_{(≤h)} may be slotted. (Details will be supplied when we come to the decision procedure itself.) In general, the schema will be much more compact than the pumpable equation itself. However, will still be too large if the component F is.

We know that F is not a parallel composition (or more accurately need not be a parallel composition, otherwise we could absorb extra factors into H); furthermore, we are not too concerned if F is an atom, since the norm of the equation will then be bounded. However, it is important for us to be able to deal with the situation in which F is a sequential composition. Such an equation might be monomorphic, in which case its structure is simple enough to analyse using Theorem 5.2. Otherwise, Corollary 5.3 tells us that F factors as F ∼ F̂· X^{m′} , in which case (85) hides an underlying pumpable equation with “tail” X^{m+m′} . The final theorem shows that this underlying equation has a restricted form—all parallel factors of R have X-norm one—allowing further simplification to take place.

Theorem 7.19 Let When one

pumpable

equation is built on top of another

(F | K_{(h)}) · X^{m} ∼ (V | K_{(h)}) · X^{m} | R  (88)

be a pumpable equation in the usual not-fully-factored form (74), and suppose F ∼ F̂· X^{m′} for some F̂ and m′ ≥ 1, and suppose further that F̂ is a parallel composition. Then R is a power of K · X^{m}, and h = 1. Moreover, V ∼ V̂· X^{m′} and K ∼ K̂· X^{m′} for some V̂ and K̂, yielding the new pumpable equation

F̂· X^{m+m′} ∼ V̂ · X^{m+m′} | R.  (89)

Conversely, suppose K is an X-unit and

F · X^{m} ∼ V · X^{m} | R  (90)

is an equation where R is a power of K · X^{m}. Suppose further that V has the property that V ⇝ V^{∗} and ||V^{∗}||_{X} = 1 entails V^{∗} ∼ K | X^{j} for some j. Then

(F | K) · X^{m} ∼ (V | K) · X^{m} | R,  (91)

i.e., noting h = 1, we recover (88).

Proof. Annihilating K_{(h)} from the two sides of (88), using Lemma 7.15, yields the new pumpable equation

F̂· X^{m′} · X^{m} ∼ V · X^{m} | R;  (92)

then, by Corollary 5.3, V ∼ V̂ · X^{m′} and (89) follows. Also by Corollary 5.3, every (parallel) prime factor in R is bisimilar to a term of the form A · X^{m+m′} . Consider a typical prime factor K^{j} · X^{m} of R. Then K^{j} · X^{m} ∼ A · X^{m+m′} ∼ A · X^{m′} · X^{m}, entailing

A · X^{m′} ∼ K^{j}.  (93)

Now A cannot be a parallel composition, otherwise (93) would be a pumpable equation with only X-units on the r.h.s., which is impossible by Lemma 7.11. But A·X^{m+m′} is a factor on the r.h.s. of a pumpable equation, namely (89), and the only such factors for which A is a parallel prime are those of X-norm one. It follows that j = 1. Thus R is a power of K·X^{m}. Note that K·X^{m} ∼ K̂·X^{m+m′} by Corollary 5.3.

We now show that h = 1. Suppose to the contrary that h ≥ 2. Construct a generalised K̂-prime K̂_{(h)} satisfying

K̂_{(h)} · X^{m+m′} ∼ (K̂· X^{m+m′} )^{h} ∼ (K · X^{m})^{h} ∼ K_{(h)} · X^{m},

and note that K ∼ K̂· X^{m′} . Since V̂ · X^{m+m′} contains the largest factor on the r.h.s. of a pumpable equation, V̂ is a parallel composition. Thus, it is possible to reduce V̂ · X^{m′} to ε in such a way that at any intermediate stage

V̂ · X^{m′} ⇝ V̂^{∗}· X^{m′} ⇝ ε,  (94)

with ||V̂^{∗}||_{X} ≥ 2, we have that V̂^{∗} is a parallel composition. Consider any such intermediate term. Certainly V̂^{∗} · X^{m′} / ∼ K̂_{(h)} · X^{m′} , since K̂_{(h)} is a parallel prime (Observation 7.5). Neither can V̂^{∗}· X^{m′} contain K̂_{(h)} · X^{m′} as a (proper, parallel) factor, for then we would obtain a pumpable equation of the form

V̂^{∗}· X^{m′} ∼ K̂_{(h)} · X^{m′} | S,

which again contradicts primality of K̂_{(h)}. So at no intermediate step in the reduction sequence (94) does V̂^{∗}· X^{m′} contain K̂_{(h)} · X^{m′} as a factor.

Now rewrite (88) as

(F̂· X^{m′} | K̂_{(h)} · X^{m′} ) · X^{m} ∼ (V̂ · X^{m′} | K̂_{(h)} · X^{m′} ) · X^{m} | R,

and annihilate V̂ · X^{m′} using a sequence of the type just described. Note that the response on the l.h.s. is always by F̂, so we end up with a pumpable equation of the form

(F̂^{∗}· X^{m′} | K̂_{(h)} · X^{m′} ) · X^{m} ∼ K̂_{(h)} · X^{m′} · X^{m} | R ∼ (K · X^{m})^{n}

for some n, again contradicting Lemma 7.11. We must conclude that h = 1, and K_{(h)} = K.

Finally, starting with (90) we need to deduce (91). By assumption, any (X-free) X-unit reachable from V is bisimilar to K. Armed with this fact, we may effectively construct a bisimulation relation containing (91) by mimicking the assumed bisimulation relation containing (90), as in Lemma 7.17. The only misfortune that can befall us is if V reaches ε before K^{i} does: but this need not occur because in a previous step some reduct of V would be bisimilar to K, and we could have selected the explicit K instead.

8 Mixed equations with a non-series-parallel tail

Theorem 7.18 provides an effective characterisation of pumpable equations, i.e., mixed equations whose “tail” is the power of a unit X that satisfies X·X ∼ X | X. We now need to characterise equations in which X · X / ∼ X | X. Fortunately, this turns out to be an easier task.

Suppose we have a mixed equation

F · X^{m} ∼ A_{1} · X^{m} | ⋯ | A_{n} · X^{m} | X^{l},  (95)

where the unit X satisfies X · X / ∼ X | X. By Theorem 4.2(e), the exponent m is bounded by the maximum norm of an immediate derivative of X, and, by Lemma 6.2, there is at least one immediate derivation X ) A · X^{m}, for which A·X^{m} is not bisimilar to a power of X. We shall show, eventually, that m = 1, X is finite state, and F is not a parallel composition. Theorem 8.6 will summarise the remaining possibilities, which almost amount to F being atomic.

Definition 8.1 For a term T, the internal parallelism IP(T) of T is the Internal

parallelism of a term.

maximum, over all subterms of T with the form S · (T_{1} | T_{2}), of the norm ||T_{1} | T_{2}|| of T_{1} | T_{2}. Here, S is assumed to be non-trivial. If there are no subterms of the prescribed form, IP(T) = 0.

Lemma 8.1 Let

d = max{||S|| : Y ) S and Y is an atom }.

If T ) T′ then IP(T′) ≤ max{IP(T), d}.

Proof. Structural induction on terms.

Lemma 8.2 For any mixed equation (95) with X · X / ∼ X | X: The tail contains

just one X.

(a) m = 1;

(b) if X ⇝ T then T / ∼ X^{2}.

Proof. If m > 1 then, by Lemma 6.2, X ) A · X^{m} ⇝ X^{2}. Hence (a) follows from (b). We shall assume that (b) is false, i.e., X ⇝ X^{2}, and obtain a contradiction.

We assume that m is as large as possible—the maximum of m is well defined by Theorem 4.2(e)—and start with the corresponding minimal mixed equation

Y · X^{m} ∼ X^{m+1} .  (96)

(Refer to Theorem 4.2(d).) Since X ⇝ X^{2} ⇝ X^{3} ⇝ …, an equation of the form

F · X^{m} ∼ X^{n}  (97)

holds for arbitrary n > m. For sufficiently large n, the component F is not atomic. Can F be a sequential composition? By Corollary 5.3, equation (97) would have to be monomorphic, otherwise F could be factored to yield a mixed equation with a higher power of X on the l.h.s., contradicting maximality of m. But equation (97) cannot be monomorphic, since X, and hence F, has normincreasing derivations.

The only remaining possibility is that F is a parallel composition; since the r.h.s. of (97) has valence one, F must be a prime power. By the same reasoning, the unique reduct F′ of F is also a power. It follows that F is a power of units, and, in light of (96),

Y^{n−m} · X^{m} ∼ X^{n},  (98)

for arbitrarily large n, and hence (by reduction) for all n > m.

Let A be a term such that (i) X ⇝ A · X^{m}, (ii) A · X^{m} is not itself a power of X, but (iii) any reduct of A · X^{m} is a power of X. Starting with (97) and n a large prime number, transform the r.h.s. to (A · X^{m})^{n}. The l.h.s. responds with F ⇝ F^{∗}, giving

F^{∗} · X^{m} ∼ (A · X^{m})^{n}.  (99)

The term F^{∗} is too big to be an atom. We shall see that F^{∗} cannot be a sequential composition. Suppose to the contrary that it is; then, by Corollary 5.3 and maximality of m, equation (99) is monomorphic, so that F^{∗} ∼ Z · F^{†}, where Z is a monomorphic atom. Again, F^{†} is too large to be an atom, and cannot be a sequential composition, by maximality of m. If F^{†} is a parallel composition, then IP(F^{∗}) ≥ ||F^{†}|| = ||F^{∗}|| − 1, which is inconsistent with Lemma 8.1 when n is sufficiently large. We a forced to conclude that F^{∗} is a parallel composition.

The r.h.s. of (99) has valence one (all reducts of A · X^{m} are bisimilar to a certain power of X), so the term F^{∗} is in fact a power, say

E^{k} · X^{m} ∼ (A · X^{m})^{n},  (100)

where k ≥ 2. In the light of (98), the length of a shortest sequence of reductions that transforms the r.h.s. of (100) to (a term bisimilar to) a power of X is equal to that of the shortest such sequence that transforms the l.h.s. to a power of Y. On the r.h.s. that minimum length is n, and on the l.h.s. it is a multiple of k. Since k ≥ 2 and n is prime, n = k. But then in (100) the norm of the l.h.s. is congruent to m (mod n), while the norm of the r.h.s. is congruent to zero.

Lemma 8.3 Suppose X ⇝ A · X and

(F_{1} | F_{2} | … | F_{r}) · X ∼ (A · X)^{2},  (101)

where F_{i} are parallel primes, and X · X / ∼ X | X. Suppose also that the two reductions A · X ) A′ · X applied in sequence on the r.h.s. are answered by different components on the l.h.s.:

(F′_{1} | F′_{2} | … | F_{r}) · X ∼ (A′ · X)^{2}.  (102)

Then F_{1} ∼ F_{2} and F′_{1} ∼ F′_{2}.

Proof. Suppose F_{1} ) F′_{1} is the response to the first reduction A · X ) A′ · X:

(F′_{1} | F_{2} | … | F_{r}) · X ∼ A′ · X | A · X,  (103)

and F_{2} ) F′_{2} the response to the second. Consider what happens if the order of the two reductions is reversed, i.e., the reduction F_{2} ) F′_{2} is performed first and F_{1} ) F′_{1} second. We shall show that the first reduction F_{2} ) F′_{2} on the l.h.s. must be matched by A · X ) A′ · X on the r.h.s., just as before. Assume to the contrary that F_{2} ) F′_{2} is matched by A · X ) A_{1} · X, with A_{1} / ∼ A′:

(F_{1} | F′_{2} | … | F_{r}) · X ∼ A_{1} · X | A · X.  (104)

Now apply the reduction F_{1} ) F′_{1} to the l.h.s.; the response on the r.h.s. is either of the form A · X ) A_{2} · X or A_{1} · X ) A′_{1} · X. Since the end result is still (102), we have

(A′ · X)^{2} ∼ | \begin{matrix}A_{1} · X | A_{2} · X, & or \\ A′_{1} · X | A · X. \end{matrix}

In either case we see that A′ ·X cannot be parallel prime (in the first because of our assumption that A′ · X / ∼ A_{1} · X; in the second because ||A′_{1} · X|| < ||A′ · X||). So A′ · X is the l.h.s. of some mixed equation

A′ · X ∼ ∏_{i} B_{i} · X,

and

X ⇝ A · X ) A′ · X ∼ ∏_{i} B_{i} · X ⇝ X^{2},

in contradiction to Lemma 8.2. Hence our initial assumption that A_{1} / ∼ A′ was incorrect, and the r.h.s’s of (103) and (104) are in fact bisimilar, entailing F′_{1} | F_{2} ∼ F_{1} | F′_{2}. Since ||F′_{1}|| < ||F_{1}||, and F_{1} and F_{2} are primes, F_{1} ∼ F_{2}; but then F′_{1} ∼ F′_{2}.

Lemma 8.4 Suppose X ⇝ A · X, X · X / ∼ X | X and F · X ∼ (A · X)^{2}. Then

(a) F is not a parallel composition;

(b) X is finite state.

Proof. To prove (a), we assume that equation (101) is a minimal counterexample and obtain a contradiction. Suppose first that ||A|| ≥ 2, so that ||F|| ≥ 5 where F = F_{1} | … | F_{r}. We could then obtain a smaller counterexample: perform a reduction F_{1} ) F′_{1} (to the largest prime) on the l.h.s., which is matched by A ) A′ on the r.h.s.; and then a further reduction A ) A′ on the r.h.s. that is answered by the l.h.s. (If r ≥ 3, or r = 2 and F_{1} ∼ F_{2}, then is is clear that the l.h.s. remains a parallel composition; if r = 2 and F_{1} / ∼ F_{2}, then F_{1} cannot be annihilated in two steps because it has norm at least three, and F_{2} cannot be touched by Lemma 8.3.)

We are left with the case ||A|| = 1. The r.h.s. (A · X)^{2} has valence one (since A has a unique reduction) and so must the l.h.s. It follows that F must be a power F ∼ E^{k}, and since ||F · X|| = 4 we must have E^{3} · X ∼ (A · X)^{2} and ||E|| = 1. Annihilating A · X on the r.h.s. we obtain E · X ∼ A · X, while annihilating two As we obtain E · X ∼ X | X. Hence X ⇝ A · X ∼ X^{2}, which is not possible by Lemma 8.2. This establishes (a).

For (b), start with the minimal equation Y · X ∼ X | X. If X is infinite state then it has arbitrarily large derivatives; in particular we may find an arbitrarily large term A such that X ⇝ A · X and A has a norm-increasing immediate derivation. Applying this sequence of derivations to the l.h.s. of the minimal equation, the r.h.s. is forced to follow:

F · X ∼ (A · X)^{2},  (105)

with ||F|| arbitrarily large. The term F is too big to be atomic, and equation (105) cannot be monomorphic since A has a norm-increasing derivative. Thus, by Corollary 5.3, F cannot be a sequential composition. Finally, F is not a parallel composition by part (a).

L.h.s. is not a Lemma 8.5 Suppose

parallel

composition. F · X ∼ A_{1} · X | … | A_{n} · X | X^{l},  (106)

is a mixed equation with X · X / ∼ X | X; then the term F is not a parallel composition.

Proof. We assume that (106) is a minimal counterexample and obtain a contradiction. Suppose first that the counterexample has norm three (the smallest possible). If the r.h.s. is X^{3} then the l.h.s. has valence one, and must be of the form Y^{2} · X. Thus

Y^{2} · X ∼ X^{3} leading to Y · X ∼ X^{2};  (107)

and X, and hence Y, is finite state by Lemma 8.4. Let x and y denote the lengths of the longest sequences of norm-increasing derivations available to X and Y, respectively. Then equations (107) give 2y = 3x and y = 2x which imply x = 0. However, we know that X has at least one norm-increasing derivation.

Staying with norm three, the other possibility is

(A | Y) · X ∼ A · X | X leading to Y · X ∼ X^{2}.  (108)

Again, X and Y are finite state. First, suppose A is finite state, and let a denote the length of the longest sequence of norm-increasing derivations available to A. Then equations (108) give a + y = a + x and y = 2x, again entailing x = 0. Next, suppose that A ⇝ A^{∗} where A^{∗} ≠ ε is finite state. Choose A^{∗} firstly to minimise the number of derivations required to reach A^{∗} from A, and secondly to maximise the length a^{∗} of a sequence of norm-increasing transitions starting at A^{∗}. Then, applying A ⇝ A^{∗} on the l.h.s., using a minimum-length sequence of derivations, we reach

(A^{∗} | Y) · X ∼ Â · X | X,

where Â is finite state. Thus a^{∗} + y = â + x ≤ a^{∗} + x, where â is the length of a longest sequence of norm-increasing derivations available to Â. Thus y ≤ x, which together with y = 2x entails x = 0, a contradiction. Finally, suppose that the only finite state term reachable from A is ε. Starting with the left equation in (108), apply norm-increasing derivations to Y until A responds for the first time:

(A | Y^{∗}) · X ∼ A′ · X | X^{∗}.

(A must eventually respond because y = 2x and x > 0.) Now reduce A ⇝ ε on the l.h.s. via a sequence of ||A|| < ||A′|| reductions; the l.h.s. is now finite state, whereas the r.h.s. is still infinite state. This eliminates the possibility of a norm-three counterexample.

A minimum counterexample of norm greater than three must, as we have seen on previous occasions, have the form

(F | Z) · X ∼ A · X | X,  (109)

with ||Z|| = 1. (If either side had more than two components, or had no components of norm one, we could easily obtain a smaller-norm counterexample.) Moreover, again by minimality, F has a unique reduction F ) F′ matching X ) ε and A has a unique reduction A ) A′ matching Z ) ε. Reducing X, we obtain (F′ | Z) · X ∼ A · X, and hence F′ | Z ∼ A. Since A has a unique reduction, A ∼ Z^{t} and F′ ∼ Z^{t−1} where t ≥ 2. Substituting for A, equation (109) may be rewritten as

(F | Z) · X ∼ Z^{t} · X | X.  (110)

On the other hand, applying the reduction Z^{t} ) Z^{t−1} to the r.h.s. of (110) yields

F · X ∼ Z^{t−1} · X | X,

and since the l.h.s. has a unique reduction,

Z^{t−1} · X ∼ X^{t}.  (111)

Since X has a norm-increasing derivation, so must Z; let Z ) Ẑ be one such. Applying this derivation to the l.h.s. of (110) leads to one of two equations:

(F | Ẑ) · X ∼ | \begin{matrix}(Z̃ | Z^{t−1}) · X | X, & or \\ Z^{t} · X | B̂· X. \end{matrix}  (112)

where Z ) Z̃ and X ) B̂ · X are norm-increasing derivations. In the former instance, let X ) B̃· X be the norm-increasing derivation induced when Z ) Z̃ is applied to the l.h.s. of (111), yielding

(Z̃ | Z^{t−2}) · X ∼ B̃· X | X^{t−1}.  (113)

Applying the reduction Z ) ε to the r.h.s’s of (112) preserves the parallel composition on the l.h.s.—note that ||F||, ||Ẑ|| ≥ 2—and leads to

(parallel composition) · X ∼ | \begin{matrix}(Z̃ | Z^{t−2}) · X | X, & or \\ Z^{t−1} · X | B̂· X. \end{matrix}

Comparing with (111) and (113), we see that both possibilities have the form

(parallel composition) · X ∼ B · X | X^{t},

where B stands for either B̂ or B̃. (Note that in either case, X ) B · X is a possible derivation.) Now reduce the r.h.s. from B · X | X^{t} to B · X | X, via a sequence of t − 1 reductions; the valence of the r.h.s. remains constant during this process, and hence the parallel composition on the l.h.s. is still preserved:

(parallel composition) · X ∼ B · X | X.

Finally apply the norm-increasing derivation X ) B · X to the r.h.s. and appeal to Lemma 8.4 to obtain the desired contradiction.

General form of a Theorem 8.6 The general form of a mixed equation which is neither mono-

mixed equation with X · X / ∼ X | X.

morphic nor pumpable is

F · X ∼ A_{1} · X | … | A_{n} · X | X^{l}

where F is an atom, and X is a unit satisfying X · X / ∼ X | X; moreover X is finite state.

Proof. The term F is not a sequential composition by Corollary 5.3 and Lemma 8.2, and is not a parallel composition by Lemma 8.5. The unit X occurs to the power one on the l.h.s. by Lemma 8.2. Finally, by first reducing to the minimal mixed equation Y · X ∼ X | X, and then applying matched normincreasing derivations X ) A·X to the r.h.s. we place ourselves in the situation of Lemma 8.2; hence X is finite state.

9 The decision procedure

Subsection 9.1 will provide a high-level description of the Decision Procedure; Subsections 9.2 and 9.3 will present its main component procedures—expansion and simplification—along with an informal commentary; finally, Subsection 9.4 will justify correctness.

9.1 Overview

Figure 3 presents a high-level view of the proposed procedure for deciding whether a given terms P_{0} and Q_{0} of terms is bisimilar. The procedure maintains two sets, ℬ and 𝒫, whose elements are pairs of terms; ℬ initially contains just the pair ⟨P_{0}, Q_{0}⟩, while 𝒫 is empty. Roughly, our strategy is to augment the set ℬ until either (a) ℬ becomes a finite basis (in some sense) for a bisimulation that includes the pair ⟨P_{0}, Q_{0}⟩, or (b) some inconsistency is detected. The set 𝒫, which at all times satisfies the inclusion 𝒫 ⊆ ℬ, may be interpreted as the set of “processed” pairs.

The computation proceeds via a sequence of nondeterministic steps, in which a pair ⟨P, Q⟩ ∈ ℬ \ 𝒫 is selected, processed, and added to 𝒫. The type of processing—“expansion” or “simplification”— depends on whether ||P|| exceeds some bound b. This bound must be chosen sufficiently large; it suffices to take b to be twice the largest norm of any atom. As a result of processing ⟨P, Q⟩, a number of new pairs may be added to ℬ; however, we are able to bound the norm of these processes, and hence deduce that the procedure must eventually halt. If P_{0} ∼ Q_{0}, the nondeterministic choices can be made so that only bisimilar pairs are ever added to ℬ; in this case, the Step 3 always succeeds, and the procedure accepts when all pairs in ℬ have been processed. Conversely, if P_{0} / ∼ Q_{0}, then every nondeterministic branch will arrive at an inconsistency, which will manifest itself in Step 3 failing during an “expansion.” Note that, even if P_{0} ∼ Q_{0}, many nondeterministic branches will fail; the point is that at least one must succeed.

The elements of the set ℬ are, in fact, slightly more general than has so far Definition of

schema; norm of a schema.

been admitted. In addition to simple pairs of terms, we also allow schemas of the form

⟨(F | [ ]_{h}) · X^{m}, (V | [ ]_{h}) · X^{m} | R⟩,  (114)

where R is an explicit parallel composition of terms of the form K^{j} · X^{m} (i.e., non-exceptional factors). The notation [ ]_{h} stands for a context into which can be substituted any generalised K-term H ∈ ΠK_{(≤h)} (the same term H on the two sides of the schema). The schema (114) is intended to stand for the infinite set of pairs of processes that can be obtained by such substitutions. So the set ℬ, though itself finite, represents a potentially infinite set of putatively bisimilar pairs of processes. The norm of a schema is the norm of the l.h.s. (which should be equal to the norm of the r.h.s.) with the context erased.

The input is a pair of terms ⟨P_{0}, Q_{0}⟩; we are required to decide if P_{0} ∼ Q_{0}.

Step 1: If ||P_{0}|| ≠ ||Q_{0}|| then reject.

Step 2: Set ℬ := {⟨P_{0}, Q_{0}⟩} and 𝒫 := ∅. (The set ℬ is used to accumulate basis pairs; the set 𝒫 ⊆ ℬ is the set of basis pairs that have been “processed.”)

Step 3: While 𝒫 ⊂ ℬ choose a pair ⟨P, Q⟩ ∈ ℬ \ 𝒫, and process ⟨P, Q⟩ as

follows.

• If ||P|| = ||Q|| ≤ b then attempt to expand ⟨P, Q⟩ (refer to Figure 4 and Section 9.2); if the expansion fails then reject.

• Otherwise (||P|| = ||Q|| > b) apply the simplification step (refer to

Figure 5 and Section 9.3) to ⟨P, Q⟩.

Step 4: Accept. (At this point, 𝒫 = ℬ, and ℬ is a basis for a bisimulation containing ⟨P, Q⟩.)

Figure 3: A high-level view of the Decision Procedure.

In order to understand the decision procedure in greater depth, it is necessary to introduce the notion of finite approximation (from above) to the maximum bisimulation relation ∼.

Finite Definition 9.1 The sequence of binary relations (∼_{k}: k ∈ ℕ) on Proc is

approximants ∼_{k} to the maximum bisimulation ∼.

defined as follows. For all P, Q ∈ Proc: (i) P ∼_{0} Q, and (ii) P ∼_{k+1} Q iff

• for all P′ ∈ Proc and a ∈ Act such that P )^{a} P′, there exists Q′ ∈ Proc such that Q )^{a} Q′ and P′ ∼_{k} Q′; and

• for all Q′ ∈ Proc and a ∈ Act such that Q )^{a} Q′, there exists P′ ∈ Proc such that P )^{a} P′ and P′ ∼_{k} Q′.

∼ is a limit of the Proposition 9.1 P ∼ Q iff P ∼_{k} Q for all k ∈ ℕ.

sequence (∼_{k}).

Proof. Since ∼ ⊆ ∼_{k}, for all k, the forward implication is immediate. For the reverse implication, take any pair P, Q ∈ Proc satisfying P ∼_{k} Q for all k. For any derivation P )^{a} P′ there is a sequence of responses Q )^{a} Q′_{k} such that P′ ∼_{k} Q′_{k} for all k. But the sequence (Q′_{k}) contains only finitely many distinct processes—this is the “image-finiteness” property of PA—so some process Q′ must occur infinitely often. This process has the property that P′ ∼_{k} Q′ for all k. Thus the binary relation ⋂_{k} ∼_{k} satisfies the condition for a bisimulation relation, and hence is contained in ∼.

The input is a pair of terms or a schema ⟨P, Q⟩ to be expanded. If ⟨P, Q⟩ is a pair of simple terms, go to Case TT; if it is a schema, go to Case Sa.

Case TT: For each derivation P )^{a} P′ nondeterministically guess a derivation Q )^{a} Q′ and set ℬ := ℬ + ⟨P′, Q′⟩; if no derivation Q )^{a} Q′ exists, halt and report failure. Repeat this procedure with the roles of P and Q reversed. If responses were proposed for all possible derivations, then halt and report success.

Case Sa: (Refer to Theorem 7.18.) Suppose P = (F | [ ]_{h}) · X^{m} and Q = (V | [ ]_{h}) · X^{m} | R.

(a) For each derivation F )^{a} F′ nondeterministically guess a derivation

V )^{a} V′ or R )^{a} R′ and set

ℬ := ℬ + ⟨(F′ | [ ]_{h}) · X^{m}, (V′ | [ ]_{h}) · X^{m} | R⟩, or (115)
ℬ := ℬ + ⟨(F′ | [ ]_{h}) · X^{m}, (V | [ ]_{h}) · X^{m} | R′⟩,  (116)

as appropriate. If no such derivation can be found, halt and report failure.

(b) For each derivation R )^{a} R′, nondeterministically guess a derivation F )^{a} F′ and perform assignment (116). If no such derivation can be found, halt and report failure.

(c) For each derivation V )^{a} V′, either

• nondeterministically guess a derivation F )^{a} F′ and perform assignment (115), or

• provided K_{h} )^{a} K_{h−1} | X^{i},

ℬ := ℬ + ⟨(F̂| [ ]_{h}) · X^{m}, (V̂ | [ ]_{h}) · X^{m} | R⟩, and(117)
ℬ := ℬ + ⟨(F̂| [ ]_{h−1}) · X^{m}, (V̂ | [ ]_{h−1}) · X^{m} | R⟩, (118)

where F̂ = F | K_{h−1} | X^{i} and V̂ = V′ | K_{h}. If there is no reduction of K_{h} via action a, halt and report failure.

(d) Set ℬ := ℬ + ⟨(F | [ ]_{h−1}) · X^{m}, (V | [ ]_{h−1}) · X^{m} | R⟩. (If h = 1, the result is no longer a schema, just a pair of processes.)

If responses were proposed for all possible derivations, then halt and report success.

Figure 4: The Expansion Procedure.

9.2 Expansion

The Expansion Procedure is presented in Figure 4. In certain steps of this and subsequent procedures the reader is referred Theorems or Lemmas which justify those steps. The proof of correctness is an inductive argument that uses the cited results to provide the inductive steps. The Expansion Procedure is easy to appreciate at an abstract level. Given a pair ⟨P, Q⟩ ∈ ℬ \ 𝒫 we would like to test whether P ∼ Q. Since ⟨P, Q⟩ may be a schema, we have to make clear what we mean by bisimilarity in this case. For a schema ⟨P, Q⟩ we write P ∼ Q (respectively P ∼_{k} Q) if the two side of the schema are bisimilar (respectively, bisimilar up to k steps) for all valid substitutions into the context.

If indeed it is the case that P ∼ Q, then for each derivation P )^{a} P′ there will be a matching derivation Q )^{a} Q′ with P′ ∼ Q′ (and vice versa). (What is meant by derivation in the case of a schema is made explicit in Figure 4; note the importance here of uniformity of bisimulation-preserving derivations, as assured by Theorem 7.18.) Provided the Expansion Procedure makes the correct nondeterministic choices at every step, only bisimilar pairs will ever be added to ℬ. On the other hand, if P / ∼ Q then there is an integer k such that P / ∼_{k} Q; consider the minimal such k. Whatever non-deterministic choices are made by the Expansion Procedure, it will be forced at some point to add a pair ⟨P′, Q′⟩ to ℬ for which P′ / ∼_{k−1} Q′.

Consider the set \overline{ℬ} of bisimilar pairs ⟨P, Q⟩ reachable from ⟨P_{0}, Q_{0}⟩ by some sequence of expansion steps. If we knew an a priori upper bound b on the norm of (pairs of) processes contained in \overline{ℬ}, we would be done. For suppose P_{0} ∼ Q_{0}. Then, provided the correct nondeterministic choices are always made, only bisimilar pairs will be added to ℬ. Eventually ℬ = \overline{ℬ}, at which point the Decision Procedure halts and accepts. On the other hand, suppose P_{0} / ∼ Q_{0}. The the Decision Procedure is doomed to add pairs ⟨P, Q⟩ to ℬ such that P / ∼_{k} Q for smaller and smaller values of k. Eventually, a pair will be added such that P / ∼_{0} Q; when this pair is processed the expansion step will fail, and the Decision Procedure will halt and reject.

In reality, of course, there is no such bound b, so we must somehow control the norm of (pairs of) processes entering ℬ: this is the role of the Simplification Procedure, described in the following subsection. Although the details of the Expansion Procedure are mostly routine, the assignments (117) and (118) and the circumstances in which they are invoked may appear mystifying. At first sight, this step of the procedure may appear unnecessary, since Lemma 7.16 assures us that derivations involving generalised K-primes on the r.h.s. are matched by similar derivations on the l.h.s. However, we must remember that V may contain K_{h} as a factor when F does not; in this case, as in the Proof of Lemma 7.17, we may need to “steal” a K_{h} from the generalised K-term sitting in the context [ ]_{h}. After stealing from [ ]_{h} there may or may not be any K_{h} remaining, leading to the two possibilities represented by (117) and (118).

The input is a pair ⟨P, Q⟩. Go to Case Sa if ⟨P, Q⟩ is a schema; otherwise, go to Case SS if P and Q are both (formal) sequential compositions, Case PP if they are both parallel, and case SP if (after possible relabelling) P is sequential and Q is parallel.

Case SS: (Refer to Lemma 9.2.) Let P = P_{1} · P_{2} and Q = Q_{1} · Q_{2}, and assume, without loss of generality, that ||P_{1}|| > ||Q_{1}||. Nondeterministically guess R with ||R|| = ||P_{1}|| − ||Q_{1}||, and set

ℬ := ℬ + ⟨P_{1}, Q_{1} · R⟩ + ⟨R · P_{2}, Q_{2}⟩.

Case PP: (Refer to Lemma 9.2.) Let P = P_{1} | P_{2} and Q = Q_{1} | Q_{2}. Nondeterministically guess R_{1}, S_{1}, R_{2}, S_{2} with ||R_{1}|| + ||S_{1}|| = ||P_{1}|| and

||R_{2}|| + ||S_{2}|| = ||P_{2}||. Then

ℬ := ℬ + ⟨P_{1}, R_{1} | S_{1}⟩ + ⟨P_{2}, R_{2} | S_{2}⟩ + ⟨R_{2} | S_{1}, Q_{1}⟩ + ⟨R_{1} | S_{2}, Q_{2}⟩.

Case SP: Refer to Figure 6.

Case Sa: Refer to Figure 7.

Finally set 𝒫 := 𝒫 + ⟨P, Q⟩, recording the processing of the pair ⟨P, Q⟩.

Figure 5: The Simplification Procedure.

9.3 Simplification

The Simplification Procedure presented in Figures 5, 6 and 7 is invoked whenever a pair ⟨P, Q⟩ is processed whose constituent processes exceed, in norm, a certain bound b. The bound b is set larger than the norm of any atom, so we are guaranteed that P and Q are (explicit) sequential or parallel compositions. If P and Q are either both sequential (Case SS) or both parallel (Case PP) compositions, then the simplification step is straightforward: the unique sequential (respectively, parallel) decomposition theorem allows ⟨P, Q⟩ to be replaced by two (respectively, four) equivalent pairs of strictly smaller norm. In Case SS, for example, P = P_{1} · P_{2} ∼ Q_{1} · Q_{2} = Q if and only if there exists a term R, of the appropriate norm, such that both P_{1} ∼ Q_{1} · R and R · P_{2} ∼ Q_{2}.

Next, Case SP covers the situation where P or Q is a sequential composition and the other is parallel; suppose, without loss of generality that it is P that is sequential. We use the structure theory developed in Sections 4–8 to replace the pair ⟨P, Q⟩ by a number of equivalent pairs of lesser or equal norm. Note that this time the norm does not necessarily decrease; however, if the norm remains that same, the new pair will be of sequential-sequential or parallel-Case SP: Let P = P_{1} · P_{2} and Q = Q_{1} | Q_{2}. Nondeterministically select

and perform one of options (a)–(c) below.

(a) (Refer to Theorem 5.2.) Nondeterministically guess a monomorphic atom Y, a term T and a positive integer n satisfying n(||T|| + 1) = ||P||; then set

ℬ := ℬ + ⟨P_{1} · P_{2}, Y · (T | (Y · T)^{n−1} )⟩ + ⟨Q_{1} | Q_{2}, (Y · T)^{n}⟩.

(b) (Refer to Lemma 6.7.) Nondeterministically guess a series-parallel atom X, a term T and positive integers m and i such that ||T|| + m + i = ||P||; then set

ℬ := ℬ + ⟨P_{1} · P_{2}, (T | X^{i}) · X^{m}⟩ + ⟨Q_{1} | Q_{2}, T · X^{m} | X^{i}⟩.

(c) (Refer to Theorem 7.18 and Lemma 7.6.) Nondeterministically guess a series-parallel unit X, an X-monomorphic X-unit K, positive integers h and m, and a system of generalised K-primes K = K_{(1)}, K_{(2)}, …, K_{(h)}. Now guess terms F and V, a generalised K-term H ∈ ΠK_{(≤h)}, and a parallel product R of non-exceptional factors (terms of the form K^{j} · X^{m}), all subject to the constraint

||F|| + ||H|| + m ||X|| = ||V|| + ||H|| + m + ||R|| = ||P|| = ||Q||.

Then set

ℬ := ℬ + ⟨P_{1} · P_{2}, (F | H) · X^{m}⟩
+ ⟨Q_{1} | Q_{2}, (V | H) · X^{m} | R⟩
+ ⟨(F | [ ]_{h}) · X^{m}, (V | [ ]_{h}) · X^{m} | R⟩.

Figure 6: The Simplification Procedure (continued).

Case Sa: The input is a schema ⟨(F | [ ]_{h}) · X^{m}, (V | [ ]_{h}) · X^{m} | R⟩ whose norm exceeds the bound b. There are two possibilities: F is either a parallel (SubCase P) or sequential (SubCase S) composition (its norm is too large for it to be an atom). SubCase P: (Refer to Theorem 7.18.) Nondeterministically guess a number h′ in the range 1 ≤ h′ ≤ h, and terms F̂, V̂, and H ∈ ΠK_{(≤h′)}, satisfying the norm conditions ||F̂|| + ||H|| = ||F|| and ||V̂|| + ||H|| = ||V||. Then set

ℬ := ℬ + ⟨F, F̂| H⟩ + ⟨V, V̂ | H⟩ + ⟨(F̂| [ ]_{h}) · X^{m}, (V̂ | [ ]_{h}) · X^{m} | R⟩.

SubCase S: (Refer to Theorem 7.19 and Lemma 9.3.) Verify that h = 1, R = (K · X^{m})^{i} for some i ≥ 1, and V has the property that V ⇝ V^{∗} and ||V^{∗}||_{X} = 1 entails V^{∗} ∼ K | X^{j} for some j. (For a procedure to check the latter last condition, see Figure 8.) If any of these three conditions fail, halt and reject. Otherwise, set

ℬ := ℬ + ⟨F · X^{m}, V · X^{m} | R⟩.

Figure 7: The Simplification Procedure (concluded).

parallel type, so its norm will be decreased at a subsequent simplification step. The generalised K-primes used here are constructed using Lemma 7.6.

By setting the bound b larger than the norm of any atom, we avoid matching ⟨P, Q⟩ against a mixed equation with a non-series-parallel tail; for by Theorem 8.6, such an equation has l.h.s. F · X where F is atomic. This leaves three possibilities (assuming P ∼ Q):

(a) The pair ⟨P, Q⟩ matches (its components are bisimilar to the two sides of) a monomorphic equation (see Theorem 5.2).

(b) The pair ⟨P, Q⟩ matches a trivial mixed equation of the form described in Theorem 6.7.

(c) The pair ⟨P, Q⟩ matches a pumpable equation (see Theorem 7.18).

These four possibilities are picked up by the correspondingly labelled options in Case SP of the simplification procedure (refer to Figure 6).

Finally, Case Sa deals with the possibility that ⟨P, Q⟩ is a schema. The term F is too large in norm to be an atom, so it must be either a parallel or sequential composition. In the former case, F must have accumulated some generalised Kfactors which must now be shipped into the context, where they belong. In the latter case, the schema must hide a pumpable equation with a longer tail (higher Search (T · X^{i}):

This recursive procedure takes a term T, explicitly given in the form T · X^{i}. It searches systematically through all derivatives T ⇝ T^{∗} with ||T^{∗}||_{X} = 1, and verifies that all such T^{∗} satisfy T^{∗} · X^{i} ∼ K | X^{j}, for some j. The top level call to the procedure has i = 0.

(a) Has the parameter T ·X^{i} been processed before by this procedure? If so, return immediately.

(b) Is T a formal parallel composition T = T_{1} | T_{2}? If so, perform the following:

• if ||T_{1}||_{X} > 0, call Search (T_{1} · X^{i});

• if ||T_{2}||_{X} > 0, call Search (T_{2} · X^{i});

and return.

(c) Is T a formal sequential composition T = T_{1} · T_{2}? If so, perform the following:

• if ||T_{2}||_{X} > 0, call Search (T_{2} · X^{i}) and return; else

• [ ||T_{2}||_{X} = 0] if ||T_{2}|| + i ≥ ||K||, halt and reject; else

• [ ||T_{2}||_{X} = 0 and i′ = ||T_{2}|| + i < ||K||] call Search (T_{1} · X^{i′}), and

return.

(d) Otherwise T is an atom.

• If ||T||_{X} > 1 then, for all derivations T ) T′, call Search (T′ · X^{i}); else

• [ ||T||_{X} = 1] if T does not satisfy T · X^{i} ∼ K | X^{j} for some i, halt and reject. (Refer to Figure 9 for a procedure to decide the latter condition.)

Figure 8: Searching derivatives of X-norm one.

value of m), which must now be revealed. This is the situation described in Theorem 7.19. The one algorithmically non-trivial premise of Theorem 7.19 is handled by procedure Search of Figure 8, and its attendant procedure K-Bisim of Figure 9. Both are conceptually quite straightforward: the former is just a closure operation, while the later only has to deal with bisimilarity of X-units.

9.4 Correctness

Recall that ⟨P_{0}, Q_{0}⟩ is the input to the Decision Procedure, the pair of processes we wish to test for bisimilarity. We show separately that: if P_{0} ∼ Q_{0} then the procedure halts and accepts its input, and if P_{0} / ∼ Q_{0}, it halts and rejects. The former implication is the easier: we just need to check that the procedure K-Bisim (T · X^{i}, K | X^{j}):

This non-deterministic, recursive procedure tests bisimilarity of two X-units.

(a) Have these parameters been processed before by this procedure? If so, return immediately.

(b) Is T a formal parallel composition T = T_{1} | T_{2}? If so, perform the following (without loss of generality assume ||T_{2}||_{X} = 0):

• if j′ = j − ||T_{2}|| < 0, halt and reject; else,

• call K-Bisim (T_{1} · X^{i}, K | X^{j′}).

(c) Is T a formal sequential composition T = T_{1} · T_{2}? If so, perform the following:

• if ||T_{2}||_{X} > 0, halt and reject; else,

• [ ||T_{2}||_{X} = 0] if ||T_{2}|| + i ≥ ||K||, halt and reject; else

• [ ||T_{2}||_{X} = 0 and i′ = ||T_{2}|| + i < ||K||] call K-Bisim (T_{1} · X^{i′}, K |

X^{j}) and return.

(d) Otherwise T is an atom. For all derivations T ) T′, so the following: derivation K ) K | X^{j′} or K ) X^{j′}. Then:

• if ||T′||_{X} = 0, verify that there is a matching derivation K ) X^{j′} with ||T′ · X^{i}|| = ||X^{j′}|| (halt and reject if none exist); else • if ||T′||_{X} = 1, non-deterministically guess a matching derivation K ) K | X^{j′} with matching norm (halt and reject if none exist), and call K-Bisim (T′ · X^{i}, K | X^{j′}); else

• [ ||T′||_{X} > 1] halt and reject.

Figure 9: Testing whether an X-unit is bisimilar to K.

is always able to keep the set ℬ free from non-bisimilar pairs. For the latter implication, we rely on the following simple fact.

Lemma 9.2 For all k, the relation ∼_{k} is a congruence with respect to sequential and parallel composition; that is, ∼_{k} is an equivalence relation on terms that satisfies

P · Q ∼_{k} P̂· Q̂ and P | Q ∼_{k} P̂| Q̂,

for any terms P, P̂, Q and Q̂, with P ∼_{k} P̂ and Q ∼_{k} Q̂.

This fact will be applied in the contrapositive form: e.g., if P | Q / ∼_{k} P̂| Q̂ then either P / ∼_{k} P̂ or Q / ∼_{k} Q̂. We also need a level-k approximation version of the “lifting” part of Theorem 7.19.

Lemma 9.3 Let K be an X-unit, and suppose

F · X^{m} ∼_{k} V · X^{m} | R,

where R is a power of K · X^{m}. Suppose further that V has the property that V ⇝ V^{∗} and ||V^{∗}||_{X} = 1 entails V^{∗} ∼ K | X^{j} for some j. Then

(F | K^{i}) · X^{m} ∼_{k} (V | K^{i}) · X^{m} | R,

for all i.

All the machinery is in place for the main result.

Theorem 9.4 The procedure presented in Figure 3 correctly decides bisimilarity of PA terms in doubly exponential nondeterministic time.

Proof. The Simplification Procedure never produces terms whose norm is larger than the norm of its input. The Expansion Procedure can only produce terms reachable in one derivation from a term of norm at most b. Thus the set ℬ contains only terms whose norm is bounded by B = max{||P_{0}||, b + i}, where i is the maximum of ||Z′|| − ||Z|| over all atoms Z and derivations Z ) Z′. Since there are only a finite number of terms with norm bounded by B, the procedure must terminate.

It is straightforward to check that if P_{0} ∼ Q_{0} then there is some sequence of non-deterministic choices that causes the procedure to accept its input ⟨P_{0}, Q_{0}⟩. Specifically, one checks that whenever a new pair ⟨P, Q⟩ is added to ℬ, the procedure has the flexibility to choose processes P and Q with P ∼ Q. Thus the set ℬ only contains bisimilar pairs, and the procedure terminates only when 𝒫 = ℬ.

Finally suppose P_{0} / ∼ Q_{0}. We need to verify that the procedure rejects its input ⟨P_{0}, Q_{0}⟩ whatever non-deterministic choices are made. For terms P, Q define κ(P, Q) to be

κ(P, Q) = | \begin{matrix}min\{k : P / ∼_{k} Q\} & if P / ∼ Q; \\ & otherwise. \end{matrix}

Note that κ is well defined by the “image finiteness” property of PA, viz, that any PA term has only finitely many (immediate) derivatives. Image finiteness implies P ∼ Q iff P ∼_{k} Q for all k. Applying the Expansion Procedure to any pair ⟨P, Q⟩ with κ(P, Q) = k < is bound to produce at least one pair ⟨P′, Q′⟩ for which κ(P′, Q′). If we can prove that applying the Simplification Procedure to any pair ⟨P, Q⟩ with κ(P, Q) = k < will produce at least one pair ⟨P̃, Q̃⟩ with κ(P, Q) ≤ k and ||P̃|| < ||P||, then we are done: the Decision Procedure will halt and reject by induction on lexicographic ordering on pairs (κ(P, Q), ||P||). (Actually, this situation does not quite obtain: one may have ||P̃|| = ||P||, but in that case the original simplification step is immediately followed by another that does reduce the norm.)

To verify that the Simplification Procedure satisfies this property, it is necessary to assess each of the cases in the light of Lemma 9.2 (or for SubCase S of Figure 7, in the light of Lemma 9.3). Take, as an example, the Case SS of the Figure 5, i.e., the first case. If κ(P_{1}, Q_{1} · R) ≥ k and κ(R · P_{2}, Q_{2}) ≥ k, then P_{1} ∼_{k} Q_{1}·R and R·P_{2}, ∼_{k} Q_{2}. Then, by Lemma 9.2, P_{1}·P_{2} ∼_{k} Q_{1}·R·P_{2} ∼_{k} Q_{1}·Q_{2}, and hence κ(P_{1} · P_{2}, Q_{1} · Q_{2}) ≥ k. Equivalently, if κ(P_{1} · P_{2}, Q_{1} · Q_{2}) = k then either κ(P_{1}, Q_{1} · R) ≤ k or κ(R · P_{2}, Q_{2}) ≤ k. Either way, the norm is reduced. The other cases may be argued similarly.

The (syntactic) size of processes in ℬ is bounded by B, which in turn is exponential in the size of the (syntactic description) of the set of productions describing derivations, which we take to be the input size. Thus the cardinality of ℬ is doubly exponential in the input size. The non-deterministic timecomplexity of the decision procedure is thus doubly exponential.

Acknowledgement

The authors thank Colin Stirling for useful discussions on the structure of mixed equations.

References

[1] J. C. M. Baeten, J. A. Bergstra and J. W. Klop, Decidability of bisimulation equivalence for processes generating context-free languages, Journal of the ACM 40 (1993), 653–682.

[2] J. A. Bergstra and J. W. Klop, Algebra of communicating processes with abstraction. Theoretical Computer Science 37(1), 77–121.

[3] Olaf Burkart, Didier Caucal and Bernhard Steffen, An elementary bisimulation decision procedure for arbitrary context-free processes. Proceedings of MFCS ’95: 20th International Symposium on Mathematical Foundations of Computer Science, Lecture Notes in Computer Science 969, Springer-Verlag, 1995, 423–433.

[4] Søren Christensen, Yoram Hirshfeld, and Faron Moller, Decomposability, decidability and axiomatisability for bisimulation equivalence on basic parallel processes. Proceedings of the Eighth Annual IEEE Symposium on Logic in Computer Science (LICS 93), IEEE Computer Society Press, 1993, 386-396.

[5] Søren Christensen, Yoram Hirshfeld, and Faron Moller, Bisimulation equivalence is decidable for basic parallel processes. Proceedings of CONCUR 93: Fourth International Conference on Concurrency Theory, Lecture Notes in Computer Science 715 Springer-Verlag, 1993, 143–157.

[6] Søren Christensen, Hans Hüttel and Colin Stirling, Bisimulation equivalence is decidable for all context-free processes, Information and Computation 121 (1995), 143–148.

[7] Yoram Hirshfeld, Mark Jerrum and Faron Moller, A polynomial algorithm for deciding bisimilarity of normed context-free processes, Theoretical Computer Science 158 (1996), 143–159.

[8] Yoram Hirshfeld, Mark Jerrum and Faron Moller, A polynomial algorithm for deciding bisimulation equivalence of normed Basic Parallel Processes, Mathematical Structures in Computer Science 6 (1996), 251– 259.

[9] Robin Milner, Communication and Concurrency, Prentice Hall, 1989.

[10] Robin Milner and Faron Moller, Unique decomposition of processes, Theoretical Computer Science 107 (1993), 357–363.

[11] D. M. R. Park, Concurrency and Automata on Infinite Sequences. Theoretical Computer Science: Fifth GI-Conference, Lecture Notes in Computer Science 104, Springer Verlag, 1981, 167–183.