On Cool Congruence Formats for Weak Bisimulations

(extended abstract)

Rob van Glabbeek

National ICT Australia and School of Computer Science and Engineering The University of New South Wales

                           rvg@cs.stanford.edu

Abstract. In TCS 146, Bard Bloom presented rule formats for four main notions of bisimulation with silent moves. He proved that weak bisimulation equivalence is a congruence for any process algebra defined by WB cool rules, and established similar results for rooted weak bisimulation (Milner’s “observational congruence”), branching bisimulation and rooted branching bisimulation. This study reformulates Bloom’s results in a more accessible form and contributes (trivial) analogues for (rooted) η-bisimulation and (rooted) delay bisimulation. Moreover, finite equational axiomatisations of rooted weak bisimulation equivalence are provided that are sound and complete for finite processes in any RWB cool process algebra. These require the introduction of auxiliary operators with lookahead. Finally, a challenge is presented for which Bloom’s formats fall short and further improvement is called for.

Introduction

Structural Operational Semantics [8, 10] is one of the main methods for defining the meaning of operators in system description languages like CCS [8]. A system behaviour, or process, is represented by a closed term built from a collection of operators, and the behaviour of a process is given by its collection of (outgoing) transitions, each specifying the action the process performs by taking this transition, and the process that results after doing so. For each n-ary operator f in the language, a number of transition rules are specified that generate the transitions of a term f(p_{1}, …, p_{n}) from the transitions (or the absence thereof) of its arguments p_{1}, …, p_{n}.

For purposes of representation and verification, several behavioural equivalence relations have been defined on processes, of which the most well-known is strong bisimulation equivalence [8], and its variants weak and branching bisimulation equivalence [8, 7], that feature abstraction from internal actions. In order to allow compositional system verification, such equivalence relations need to be congruences for the operators under consideration, meaning that the equivalence class of an n-ary operator f applied to arguments p_{1}, …, p_{n} is completely determined by the equivalence classes of these arguments. Although strong bisimulation equivalence is a congruence for the operators of CCS and many other languages found in the literature, weak bisimulation equivalence fails to be a congruence for the choice or alternative composition operator + of CCS. To bypass this problem one uses the coarsest congruence relation for + that is finer than weak bisimulation equivalence, characterised as rooted weak bisimulation equivalence [8, 3], which turns out to be a minor variation of weak bisimulation equivalence, and a congruence for all of CCS and many other languages. Analogously, rooted branching bisimulation is the coarsest congruence for CCS and many other languages that is finer than branching bisimulation equivalence [7].

In order to streamline the process of proving that a certain equivalence is a congruence for certain operators, and to guide sensible language definitions, syntactic criteria (rule formats) for the transition rules in structural operational semantics have been developed, ensuring that the equivalence is a congruence for any operator specified by rules that meet these criteria. One of these is the GSOS format of Bloom, Istrail & Meyer [5], generalising an earlier format by De Simone [11]. When adhering to this format, all processes are computably finitely branching, and strong bisimulation equivalence is a congruence [5]. Bloom [4] defines congruence formats for (rooted) weak and branching bisimulation equivalence by imposing additional restrictions on the GSOS format. As is customary in this field, finer equivalences have wider formats, so Bloom’s BB cool GSOS format, which guarantees that branching bisimulation equivalence is a congruence, is more general than his WB cool GSOS format, which suits weak bisimulation equivalence; also his RWB cool GSOS format, suiting rooted weak bisimulation, is more general than the WB cool GSOS format, and his RBB cool GSOS format, guaranteeing that rooted branching bisimulation equivalence is a congruence, is the finest of all. The prime motivating example for these formats is the structural operational semantics of CCS [8]. All CCS operators are RWB cool, and the CCS operators other than the + are even WB cool.

Bloom’s formats involve a fast bookkeeping effort of names of variables, used to precisely formulate the bifurcation rules that his formats require. To make his work more accessible, Bloom also presents simpler but less general versions of his formats, obtained by imposing an additional syntactic restriction. This restriction makes it possible to simplify the bifurcation rules to patience rules, which do not require such an extensive bookkeeping. Fokkink [6] generalises Bloom’s simply RBB cool format to a format he calls RBB safe, and writes “The definition of bifurcation rules is deplorably complicated, and we do not know of any examples from the literature that are RBB cool but not simply RBB cool. Therefore, we refrain from this generalisation here.” Ulidowski [12–14] studies congruence formats for variations of the semantic equivalences mentioned above with a different treatment of divergence. Ulidowski’s formats form the counterparts of Bloom’s simply cool formats only.

The main aim of the present study is to simplify and further clarify Bloom’s work, so as to make it more accessible for the development of applications, variations and extensions. In passing, analogous results are obtained for two equivalences, and their rooted variants, that bridge the gap between weak and branching bisimulation. Moreover, the method of Aceto, Bloom & Vaandrager [1] to extract from any GSOS language a finite equational axiomatisation that is sound and complete for strong bisimulation equivalence on finite processes, is adapted to rooted weak bisimulation equivalence. In the construction fresh function symbols may need be added whose transition rules have lookahead and thereby fall outside the GSOS format.

One of the simplifications of Bloom’s formats presented here stems from the observation that the operators in any of the cool formats can be partitioned in principal operators and abbreviations, such that the abbreviations can be regarded as syntactic sugar, adding nothing that could not be expressed with principal operators. For any abbreviation f there exists a principal operator f^{⋆} that typically takes more arguments. For instance, f(x_{1}, x_{2}) could be an abbreviation of f^{⋆}(x_{1}, x_{1}, x_{2}). The rules for the abbreviations are completely determined by the rules for the principal operators, and for principal operators patience rules suffice, i.e. one does not need the full generality of bifurcation rules. Moreover, the simply cool formats can be characterised by the requirement that all operators are principal. These observations make it possible to define the cool formats of Bloom without mentioning bifurcation rules altogether. It also enables a drastic simplification of the congruence proofs, namely by establishing the congruence results for the simply cool formats first, and reducing the general case to the simple case by means of some general insights in abbreviation expansion.

Even though any operation that fits the cool formats can also be defined using merely the simply cool formats, in practice it may be handy to work with the full generality of the cool formats. The unary copying operator cp of [5] (page 257) for instance does not fit the cool formats directly, but can be made to fit by adding an auxiliary binary copying operator to the language, of which the unary one is an abbreviation. Dumping the abbreviation from the language would appear unnatural here, as the unary operator motivates the rules for both itself and its binary expansion, the latter being needed merely to make it work.

Another simplification contributed here is in the description of the RWB cool format. Bloom requires for every operational rule with target t the existence of two terms t_{1} and t_{2}, and seven types of derived operational rules. I show that without limitation of generality it is always possible to choose t_{2} = t, thereby making four of those seven types of rules redundant. Thus, the same format is obtained by requiring only t_{1} and two types of derived rules (the third being a patience rule, that was already required for its own sake).

After defining the basic concepts in Section 1, I present the simply cool congruence formats in Section 2. Section 3 presents the theory of abbreviations that lifts the results from the simple to the general formats, and Sect. 4 deals with the rooted congruence formats. Section 5 compares my definitions of the cool formats with the ones of Bloom. Section 6 recapitulates the method of [1] to provide finite equational axiomatisations of strong bisimulation equivalence that are sound and complete for finite processes on an augmentation of any given GSOS language, and Sect. 7 extends this work to the rooted weak equivalences. Finally, Sect. 8 presents a fairly intuitive GSOS language for which the existing congruence formats fall short and further improvement is called for.

Acknowledgement. My thanks to Simone Tini for inspiration.

1 Preliminaries

In this paper V = {x_{1}, x_{2}, …} and Act are two sets of variables and actions.

Definition 1. A signature is a collection Σ of function symbols f ∉ V equipped with a function ar : Σ → IN. The set T T(Σ) of terms over a signature Σ is defined recursively by:

• V ⊆ T T(Σ),

• if f ∈ Σ and t_{1}, …, t_{ar(f)} ∈ T T(Σ) then f(t_{1}, …, t_{ar(f)}) ∈ T T(Σ).

A term c() is abbreviated as c. For t ∈ T T(Σ), var(t) denotes the set of variables that occur in t. T (Σ) is the set of closed terms over Σ, i.e. the terms p ∈ T T(Σ) with var(p) = ∅. A Σ-substitution σ is a partial function from V to T T(Σ). If σ is a substitution and S is any syntactic object, then σ(S) denotes the object obtained from S by replacing, for x in the domain of σ, every occurrence of x in S by σ(x). In that case σ(S) is called a substitution instance of S. A Σ-substitution is closed if it is a total function from V to T (Σ).

Definition 2. Let Σ be a signature. A positive Σ-literal is an expression t ⟶^{a} t′ and a negative Σ-literal an expression t −̸→^{a} with t, t′ ∈ T T(Σ) and a ∈ Act. A transition rule over Σ is an expression of the form \frac{H}{α} with H a set of Σliterals (the premises of the rule) and α a positive Σ-literal (the conclusion). The left- and right-hand side of α are called the source and the target of the rule, respectively. A rule \frac{H}{α} with H = ∅ is also written α. A transition system specification (TSS), written (Σ, R), consists of a signature Σ and a set R of transition rules over Σ. A TSS is positive if the premises of its rules are positive.

Definition 3. [5] A GSOS rule is a transition rule such that

• its source has the form f(x_{1}, …, x_{ar(f)}) with f ∈ Σ and x_{i} ∈ V,

• the left-hand sides of its premises are variables x_{i} with 1 ≤ i ≤ ar(f),

• the right-hand sides of its positive premises are variables that that are all distinct, and that do not occur in its source,

• its target only contains variables that also occur in its source or premises.

A GSOS language, or TSS in GSOS format, is a TSS whose rules are GSOS rules.

Definition 4. A transition over a signature Σ is a closed positive Σ-literal. With structural recursion on p one defines when a GSOS language L generates a transition p ⟶^{a} p′ (notation p ⟶^{a}_{L} p′):

f(p_{1}, …, p_{n}) ⟶^{a}_{L} q iff L has a transition rule _{\frac{H}{f(x_{1},...,x_{n})⟶^{a}t}} and there is a

closed substitution σ with σ(x_{i}) = p_{i} for i = 1, ..., n and σ(t) = q, such that

p_{i} ⟶^{c}_{L} σ(y) for (x_{i} ⟶^{c} y) ∈ H and ¬∃r(p_{i} ⟶^{c}_{L} r) for (x_{i} −̸→^{c}) ∈ H.

Henceforth a GSOS language L over a signature Σ is assumed, and closed Σterms will be called processes. The subscript L will often be suppressed. Moreover, Act = A ._{∪} {τ} with τ the silent move or hidden action.

Definition 5. Two processes t and u are weak bisimulation equivalent or weakly bisimilar (t\underline{↔}_{w} u) if tRu for a symmetric binary relation R on processes (a weak bisimulation) satisfying, for a ∈ Act,

if pRq and p ⟶^{a} p′ then ∃q_{1}, q_{2}, q′ such that q ⟹ q_{1} ⟶^{(a)} q_{2} ⟹ q′ ∧ p′Rq′. (*)

Here p ⟹ p′ abbreviates p = p_{0} ⟶^{τ} p_{1} ⟶^{τ} ⋯ ⟶^{τ} p_{n} = p′ for some n ≥ 0, whereas p ⟶^{(a)} p′ abbreviates (p ⟶^{a} p′) ∨ (a = τ ∧ p = p′).

t and u are η-bisimilar (t\underline{↔}_{η} u) if in (*) one additionally requires pRq_{1}; t and u are delay bisimilar (t\underline{↔}_{d} u) if in (*) one additionally requires q_{2} = q′; t and u are branching bisimilar (t\underline{↔}_{b} u) if in (*) one requires both; t and u are strongly bisimilar (t\underline{↔} u) if in (*) one simply requires q ⟶^{a} q′.

Two processes t and u are rooted weak bisimulation equivalent (t\underline{↔}_{rw} u), if they satisfy

if t ⟶^{a} t′ then ∃u_{1}, u_{2}, u such that u ⟹ u_{1} ⟶^{a} u_{2} ⟹ u′ and t′ \underline{↔}_{w} u′, and

if u ⟶^{a} u′ then ∃t_{1}, t_{2}, t such that t ⟹ t_{1} ⟶^{a} t_{2} ⟹ t′ and t′ \underline{↔}_{w} u′.

They are rooted η-bisimilar (t \underline{↔}_{rη} u) if above one additionally requires u_{1} = u, t_{1} = t, and t′ \underline{↔}_{η} u′, they are rooted delay bisimilar (t \underline{↔}_{rd} u) if one requires u_{2} = u′, t_{2} = t′ and t′ \underline{↔}_{d} u′, and they are rooted branching bisimilar (t\underline{↔}_{rb} u) if one requires u_{1} = u, u_{2} = u′, t_{1} = t, t_{2} = t′ and t′ \underline{↔}_{b} u′.

It is well known and easy to check that the nine relations on processes defined above are equivalence relations indeed [2, 7], and that, for x ∈ {weak, η, delay, branching, strong}, x-bisimulation equivalence is the largest x-bisimulation relation on processes. Moreover, p\underline{↔}_{rx} q implies p\underline{↔}_{x} q.

Definition 6. An equivalence relation ∼ on processes is a congruence if

p_{i} ∼ q_{i} for i = 1, …, ar(f) ⇒ f(p_{1}, …, p_{ar(f)}) ∼ f(q_{1}, …, q_{ar(f)})

for all f ∈ Σ. This is equivalent to the requirement that for all t ∈ T T(Σ) and closed substitutions σ, ν : V → T (Σ)

σ(x) = ν(x) for x ∈ var(t) ⇒ σ(t) = ν(t).

This note, and Bloom [4], deal with syntactic conditions on GSOS languages that guarantee that the equivalence notions of Definition 5 are congruences.

2 Simply Cool GSOS Languages

In this section I define simply XB cool rule formats, for X∈ {W,D,H,B}, such that on XB cool GSOS languages, X-bisimulation equivalence is a congruence. In [5] it is shown that strong bisimulation equivalence is a congruence on any GSOS language. The proof is pretty straightforward; it consists of showing that the congruence-closure of \underline{↔} is a bisimulation. The same idea can be applied almost verbatim to \underline{↔}_{w}, \underline{↔}_{d}, \underline{↔}_{η} and \underline{↔}_{b}, once we have lemmas like Lemma 1 below. The simply XB cool formats contain the simplest syntactic requirements that guarantee these lemmas to hold.

Definition 7. Let L be a positive GSOS language. For an operator f in L, the rules of f are the rules in L with source f(x_{1}, ..., x_{ar(f)}).

• An operator in L is straight if it has no rules in which a variable occurs multiple times in the left-hand side of its premises. An operator is smooth if moreover it has no rules in which a variable occurs both in the target and in the left-hand side of a premise.

• An argument i ∈ IN of an operator f is active if f has a rule in which x_{i} appears as left-hand side of a premise.

• A variable x occurring in a term t is receiving in t if t is the target of a rule in L in which x is the right-hand side of a premise. An argument i ∈ IN of an operator f is receiving if a variable x is receiving in a term t that has a subterm f(t_{1}, …, t_{n}) with x occurring in t_{i}.

• A rule of the form \frac{x_{i} ⟶^{τ} y}{f(x_{1}, …, x_{n}) ⟶^{τ} f(x_{1}, …, x_{n})[y/x_{i}]} with 1 ≤ i ≤ n is

called a patience rule for the i^{th} argument of f. Here t[y/x] denotes term t with all occurrences of x replaced by y.

Definition 8. A GSOS language L is simply WB cool if it is positive and

1. all operators in L are straight,

2. patience rules are the only rules in L with τ-premises,

3. every active argument of an operator has a patience rule,

4. every receiving argument of an operator has a patience rule,

5. all operators in L are smooth.

The formats simply DB cool, simply HB cool and simply BB cool are defined likewise, but skipping Clause 4 for DB and BB, and Clause 5 for HB and BB.

The simply WB and BB cool formats above coincide with the ones of [4], whereas the simply DB cool format coincides with the eb format of [13].

Lemma 1. Let L be simply WB cool, let \frac{H}{s⟶^{a}t} be a rule in L, and let ν be a closed substitution such that ν(x)⟹⟶^{(c)}⟹ν(y) for each premise x⟶^{c}y in H.

Then ν(s) ⟹⟶^{(a)}⟹ ν(t).

Similar lemmas can be obtained for the other three formats, and these yield the following congruence results. The proofs are in the full version of this paper.

Theorem 1. On any simply WB cool GSOS language, \underline{↔}_{w} is a congruence. On any simply DB cool GSOS language, \underline{↔}_{d} is a congruence. On any simply HB cool GSOS language, \underline{↔}_{η} is a congruence. On any simply BB cool GSOS language, \underline{↔}_{b} is a congruence.

3 Cool GSOS Languages

In this section I will extend the simply XB cool rule formats to XB cool rule formats and establish the associated congruence theorems (X∈ {W,D,H,B}).

Definition 9. A GSOS language is two-tiered if its operators are partitioned into abbreviations and principal operators, and for every abbreviation f a principal operator f^{⋆} is specified, together with a substitution σ_{f} : {x_{1}, …, x_{ar(f^{⋆})}} → {x_{1}, …, x_{ar(f)}}, such that the rules of f are

\{\frac{σ_{f}(H)}{f(x_{1}, …, x_{ar(f)}) ⟶^{a} σ_{f}(t)} | \frac{H}{f^{⋆}(x_{1}, …, x_{ar(f^{∗})}) ⟶^{a} t} is a rule of f^{⋆} \} .

Write f(i) for the j such that σ_{f}(x_{i}) = x_{j}; take f^{⋆} = f and f(i) = i in case f is a principal operator.

Trivially, any positive GSOS language can be extended (straightened) to a twotiered GSOS language whose principal operators are straight and smooth [1].

Example 1. Let L have an operator f with rule \frac{x_{1} ⟶^{a} y, x_{1} ⟶^{b} z}{f(x_{1}, x_{2}) ⟶^{a} f(x_{1}, (f(y, x_{2}))}.

L is straightened by adding a operator f^{⋆} with

\frac{x_{1} ⟶^{a} y, x_{2} ⟶^{b} z}{f^{⋆}(x_{1}, x_{2}, x_{3}, x_{4}) ⟶^{a} f(x_{3}, f(y, x_{4}))}.

In this case σ_{f}(x_{1}) = σ_{f}(x_{2}) = σ_{f}(x_{3}) = x_{1} and σ_{f}(x_{4}) = x_{2}.

Equally trivial, f^{⋆}(p_{f(1)}, ..., p_{f(n)}) ⟶^{a} t iff f(p_{1}, ..., p_{n}) ⟶^{a} t;

so f^{⋆}(p_{f(1)}, ..., p_{f(n)})\underline{↔} f(p_{1}, ..., p_{n}).

Definition 10. A two-tiered GSOS language L is WB cool if it is positive and

1. all principal operators in L are straight,

2. patience rules are the only rules of principal operators with τ-premises,

3. every active argument of a principal operator has a patience rule,

4. if argument f(i) of f is receiving, then argument i of f^{⋆} has a patience rule,

5. all principal operators in L are smooth.

The formats DB cool, HB cool and BB cool are defined likewise, but skipping Clause 4 for DB and BB, and Clause 5 for HB and BB. Clause 4 may be weakened slightly; see Sect. 3.1.

Note that the simply cool formats defined before are exactly the cool formats with the extra restriction that all operators are principal.

Theorem 2. On any WB cool GSOS language, \underline{↔}_{w} is a congruence. On any DB cool GSOS language, \underline{↔}_{d} is a congruence. On any HB cool GSOS language, \underline{↔}_{η} is a congruence. On any BB cool GSOS language, \underline{↔}_{b} is a congruence.

Given that the cool GSOS languages differ from the simply cool GSOS language only by the addition of operators that can be regarded as syntactic sugar, the theorems above are a simple consequence of the corresponding theorems for simply cool GSOS languages. Details are in the full version of this paper.

3.1 A Small Extension

Say that an argument i of an operator f is ignored if f^{⋆} has no argument k with f(k) = i. In that case there can be no rule with source f(x_{1}, …, x_{ar(f)}) with x_{i} in its premises or in its target. A subterm u of a term t is irrelevant if occurs within an ignored argument t_{i} of a subterm f(t_{1}, …, t_{ar(f)}) of t. Now Definition 7 of an argument of an operator being receiving may be strengthened by replacing “a subterm f(t_{1}, …, t_{n}) with x occurring in t_{i}” by “a relevant subterm f(t_{1}, …, t_{n}) with x a relevant subterm of t_{i}”. This yields a slight weakening of Clause 4 in Definition 10, still sufficient to obtain Theorem 2.

Example 2. Let L have a rule \frac{x_{1} ⟶^{a} y}{g(x_{1}) ⟶^{a} f(h(f(x_{1}, y)), k(y))}. By Definition 7

both the arguments of h and k are receiving, so Clause 4 in Definition 10 demands patience rules for both h^{⋆} and k^{⋆}. Now suppose that h^{⋆} = h, k^{⋆} = k, ar(f^{⋆}) = 1 and σ_{f}(x_{1}) = x_{1}. This means that f(x_{1}, x_{2}) is an abbreviation for f^{⋆}(x_{1}) and the second argument of f is ignored. In such a case f(p, q)\underline{↔} f(p, r) for all closed terms p, q and r. Now the weakened Clause 4 does not demand a patience rule for either h^{⋆} or k^{⋆}, since the arguments of h and k are no longer receiving.

4 Rooted Cool GSOS Languages

In this section I will define the (simply) RWB, RDB, RHB and RBB cool rule formats and establish the associated congruence theorems. In order to formulate the requirements for the RWB and RDB cool GSOS languages I need the concept of a ruloid, this being a kind of derived GSOS rule.

Definition 11. For r transition rule, let RHS(r) denote the set of right-hand sides of its premises. Let L be a positive GSOS language. The class of L-ruloids is the smallest set of rules such that

• \frac{x⟶^{a}y}{x⟶^{a}y} is an L-ruloid, for every x, y ∈ V and a ∈ Act;

• if σ is a substitution, L has a rule \frac{H}{s⟶^{a}t}, and for every premise x ⟶^{c} y in H there is an L-ruloid r_{y} = \frac{H_{y}}{σ(x)⟶^{c}σ(y)} such that the sets RHS(r_{y}) are pairwise

disjoint and each RHS(r_{y}) is disjoint with var(σ(s)), then ^{\frac{⋃_{y∈H} H_{y}}{σ(s)⟶^{a}σ(t)}} is an L-ruloid.

Note that a transition α, seen as a rule \frac{∅}{α}, is an L-ruloid iff it is generated by L in the sense of Definition 4. The left-hand sides of premises of a ruloid are variables that occur in its source, and the right-hand sides are variables that are all distinct and do not occur in its source. Its target only contains variables that also occur elsewhere in the rule.

Example 3. Let L contain the rule \frac{x_{1} ⟶^{a} y_{1} x_{2} ⟶^{b} y_{2}}{f(x_{1}, x_{2}) ⟶^{a} g(x_{1}, y_{1})}. Then L has ruloids

\frac{x ⟶^{a} x′ y ⟶^{b} y′}{f(x, y) ⟶^{a} g(x, x′)} and \frac{x ⟶^{a} x′ y ⟶^{b} y′ z ⟶^{b} z′}{f(f(x, y), z) ⟶^{a} g(f(x, y), g(x, x′))}.

Definition 12. A GSOS language L is RWB cool if the operators can be partitioned in tame and wild ones, such that

1. the target of every rule contains only tame operations;

2. the sublanguage L^{tame} of tame operators in L is WB cool;

3. L is positive, and for each rule \frac{H}{s⟶^{a}t} there is a term u and a substitution σ : var(u) → var(s) such that

– there is an L-ruloid \frac{K}{u⟶^{a}v} with σ(K) = H and σ(v) = t,

– and for every premise x ⟶^{c} y in K, L has a rule \frac{σ(x)⟶^{τ}y}{s⟶^{τ}σ(u[y/x])};

(4. if argument f(i) of f is receiving, then argument i of f^{⋆} has a patience rule.)

The formats RDB cool, RHB cool and RBB cool are defined likewise, adapting “WB cool” in the second clause appropriately, but skipping the third clause for RHB and RBB, and the last one for RDB and RBB. The last clause cannot be skipped for RHB. The simply RXB cool rule formats (X∈ {W,D,H,B}) are obtained by requiring the sublanguage of tame operators to be simply XB cool.

Note that in the third clause, u, σ and the ruloid can always be chosen in such a way that v = t. The instance of this clause with s = f(x_{1}, …, x_{ar(f)}) for a tame operator f is (in the full version of this paper) easily seen to be redundant.

The last clause above appeared before as Clause 4 in Definition 10 of the WB and HB cool formats. Given that a term with a receiving variable cannot contain wild operators, this clause is almost implied by Clause 2 above. All it adds, is that the requirement of Clause 4 for the sublanguage of tame operators applies to “receiving in L” instead of merely “receiving in L^{tame} ”. Thus, the rules for the wild operators help determine which variables in a term t count as receiving. The following results are obtained in the full version of this paper.

Proposition 1. In the definition of RWB cool above, Clause 4 is redundant.

Theorem 3. On any RWB cool GSOS language, \underline{↔}_{rw} is a congruence. On any RDB cool GSOS language, \underline{↔}_{rd} is a congruence. On any RHB cool GSOS language, \underline{↔}_{rη} is a congruence. On any RBB cool GSOS language, \underline{↔}_{rb} is a congruence.

Example 4. The following fragment of CCS has the constant 0, unary operators a. , binary operators + and ∥, and instances of the GSOS rules below. Here a ranges over Act = N ._{∪} \overline{N} ._{∪} \{τ\} with N a set of names and \overline{N} = \{\overline{a} | a ∈ N \} the set of co-names. The function \overline{·} extends to N ∪ \overline{N} (but not to Act) by \overline{\overline{a}} = a.

\begin{matrix}\frac{x_{1} ⟶^{a} y_{1}}{x_{1} + x_{2} ⟶^{a} y_{1}} \frac{x_{2} ⟶^{a} y_{2}}{x_{1} + x_{2} ⟶^{a} y_{2}} a.x_{1} ⟶^{a} x_{1} \\ \frac{x_{1} ⟶^{a} y_{1}}{x_{1}∥x_{2} ⟶^{a} y_{1}∥x_{2}} & \frac{x_{2} ⟶^{a} y_{2}}{x_{1}∥x_{2} ⟶^{a} x_{1}∥y_{2}} & \frac{x_{1} ⟶^{a} y_{1} x_{2} ⟶^{\overline{a}} y_{2}}{x_{1}∥x_{2} ⟶^{τ} y_{1}∥y_{2}} \end{matrix}

The sublanguage without the + is simply WB cool, and the entire GSOS language is simply RWB cool. Clause 3 of Definition 12 applied to the i^{th} rule for the + is satisfied by taking u = x, σ(x) = x_{i}, and the ruloid \frac{x⟶^{a}y_{i}}{x⟶^{a}y_{i}}.

5 Comparison with Bloom’s Formats

Bloom’s definitions of the cool formats differ in five ways from mine.

First of all Bloom requires bifurcation rules for all operators in L^{tame}, whereas I merely require patience rules for the principal operators. As principal operators in L^{tame} are straight, and bifurcation rules for straight operators are exactly patience rules, the difference is that I dropped the bifurcation requirement for abbreviations (non-principal operators). This is possible, because by Definition 9, which corresponds to Definition 3.5.5 in [4], the rules for the abbreviations are completely determined by the rules for their straightenings, and it turns out that a bifurcation rule of an abbreviation f is exactly what is determined by the corresponding patience rule for its straightening f^{⋆}.

Bloom requires the existence of bifurcation/patience ruloids for receiving variables in any term, whereas I require them for receiving arguments of operators, which is a more syntactic and easy to check requirement. The two approaches are shown equivalent in the full version of this paper when using the extension of my formats of Sect. 3.1, this being the reason behind that extension.

Bloom’s WB and RWB cool formats use a so-called ε-presentation. This entails that rules may have premises of the form x ⟶^{ε} y. In terms of Definition 4, the meaning of such premises is given by the requirement that σ(x) = σ(y) for (x ⟶^{ε} y) ∈ H. By using ε-premises, any rule can be given a form in which the target is a univariate term, having no variables in common with the source. This allows a simplification of the statement of the bifurcation ruloids. Any εpresented GSOS language can be converted to ε-free form by substitution, in each rule r, x for y for every premise x ⟶^{ε} y of r. I believe that my conventions for naming variables improve the ones of [4].

Bloom’s rendering of the RWB cool format doesn’t feature Clause 4 (and in view of Prop. 1, neither does mine), but Clause 3 is much more involved. For every rule with conclusion s ⟶^{a} t Bloom requires the existence of two terms t_{1} and t_{2} and seven types of derived operational rules, such that the diagram on the right commutes. My

s  t t_{1}  t_{2} a a a a τ  τ τ  τ

Clause 3 stems from the observation that, given Bloom’s other restrictions, t necessarily has the rules required for t_{2}, so that one may always choose t_{2} = t. This leaves only t_{1} (called u in Definition 12) and three types of rules, one of which (the t_{1}-loop in the diagram above) is in fact a bifurcation rule whose existence is already implied by the requirements of Definition 10.

In Clause 3 of Definition 12, Bloom requires that

var(u) = \{y′ | y ∈var(t)\} and σ(y′) = \begin{cases}x if H contains a premise x ⟶^{c} y \\ y otherwise. \end{cases} (1)

In order to match Bloom’s format I could have done the same, but this condition is not needed in the proof and reduces the generality of the format.

Proposition 2. A GSOS language is WB cool, respectively RWB, BB or RBB cool, as defined here, with the extension of Sect. 3.1 and the restriction (1) above, iff it is WB cool, resp. RWB, BB or RBB cool, as defined in Bloom [4].

Moreover, my proofs that cool languages are compositional for bisimulation equivalences greatly simplify the ones of Bloom [4] by using a reduction of the general case to the simple case, instead of treating the general formats directly.

6 Turning GSOS Rules into Equations

This section recapitulates the method of [1] to provide finite equational axiomatisations of \underline{↔} on an augmentation of any given GSOS language.

Definition 13. A process p, being a closed term in a GSOS language, is finite if there are only finitely many sequences of transitions p ⟶^{a_{1}} p_{1} ⟶^{a_{2}} ⋯ ⟶^{a_{n}} p_{n}. The length n of the longest sequence of this form is called the depth of p.

Definition 14. An equational axiomatisation Ax over a signature Σ is a set of equations t = u, called axioms, with t, u ∈ T T(Σ). It respects an equivalence relation ∼ on T (Σ) if σ(t) ∼ σ(u) for any closed substitution σ : V → T (Σ).

An instance of axiom t = u is an equation σ(C[t/x]) = σ(C[u/x]) where σ is a substitution and C a term with var(C)={x}, and x occurring only once in C. An equation p = q is derivable from Ax, notation p =_{Ax} q, if there is a sequence p_{0}, …, p_{n} of terms with n ≥ 0 such that p = p_{0}, q = p_{n} and for i = 1, …, n the equation p_{i−1} = p_{i} is an instance of one of the axioms.

Ax is sound for ∼ if p =_{Ax} q implies p ∼ q for p, q ∈ T (Σ). Ax is complete for ∼ on finite processes if p ∼ q implies p =_{Ax} q for finite processes p and q.

Note that Ax is sound for ∼ iff Ax respects ∼ and ∼ is a congruence.

Definition 15. A GSOS language L extends BCCS (basic CCS) if it contains the operators 0, a. and + of Example 4. A basic process is a closed term build from the operators mentioned above only. A head normal form is a closed term of the form 0+a_{1}.p_{1} +⋯+a_{n}.p_{n} for n ≥ 0. An axiomatisation on L is head normalising if any term f(p_{1}, …, p_{ar(f)}) with the p_{i} basic processes can be converted into head normal form.

Proposition 3. Let L be a GSOS language extending BCCS, and Ax a head normalising equational axiomatisation, respecting \underline{↔}, and containing the axioms A1–4 of Table 1. Then Ax is sound and complete for \underline{↔} on finite processes.

x + (y + z) = (x + y) + z A1  x∥y = x∥−y + y∥−x + x|y CM1
x + y = y + x  A2  a.x∥−y = a.(x∥y)  CM2
x + x = x  A3  0∥−y = 0  CM3
x + 0 = x  A4  (x + y)∥−z = x∥−z + y∥−z  CM4
a.x|\overline{a}.y = τ.(x∥y)  CM5
a.(τ.(x + y) + x) = a.(x + y) T1  a.x|b.y = 0  (if b ≠ \overline{a}) CM6
τ.x + x = τ.x  T2  0|x = x|0 = 0  CM7
a.(τ.x + y) + a.x = a.(τ.x + y) T3  (x + y)|z = x|z + y|z  CM8
x|(y + z) = x|y + x|z  CM9

Table 1. Complete equational axiomatisations of BCCS and the parallel composition

Proof. Using induction on the depth of p and a nested structural induction, the axioms can convert any finite process p into a basic process. Here one uses that strongly bisimilar processes have the same depth. Now apply the well-known fact that the axioms A1–4 are sound and complete for \underline{↔} on basic processes [8].

For the parallel composition operator ∥ of CCS no finite equational head normalising axiomatisation respecting strong bisimulation equivalence exists [9]. However, Bergstra & Klop [3] gave such an axiomatisation on the language obtained by adding two auxiliary operators, the left merge ∥− and the communi-

cation merge |, with rules \frac{x_{1} ⟶^{a} y_{1}}{x_{1}∥−x_{2} ⟶^{a} y_{1}∥x_{2}} and \frac{x_{1} ⟶^{a} y_{1} x_{2} ⟶^{\overline{a}} y_{2}}{x_{1}|x_{2} ⟶^{τ} y_{1}∥y_{2}} , provided

the alphabet Act of actions is finite. The axioms are CM1–9 of Table 1, in which + binds weakest and a. strongest, and a, b range over Act.

Aceto, Bloom & Vaandrager [1] generalise this idea to arbitrary GSOS languages with finitely many rules, each with finitely many premises, and assuming a finite alphabet Act. I recapitulate their method for positive languages only.

A smooth operator (Definition 7) only has rules of the form \frac{\{x_{i} ⟶^{c_{i}} y_{i} | i∈I\}}{f(x_{1}, …, x_{n}) ⟶^{a} t}.

The trigger of such a rule is the partial function ↑_{r}: {i, …, n} ⇀ Act given by ↑_{r} (i) = c_{i} if i∈I, and ↑_{r} (i) is undefined otherwise.

Definition 16. [1] A smooth GSOS operator f is distinctive, if no two rules of f have the same trigger, and the triggers of all rules of f have the same domain.

All operators of CCS, as well as ∥− and |, are smooth. The operators 0, a. , ∥− and | are distinctive, but ∥ is not. Its triggers have domains {1}, {2} and {1, 2}.

For every smooth and distinctive operator f, Aceto, Bloom & Vaandrager declare four types of axioms. First of all, for every rule r as above there is an axiom f(σ(x_{1}), …, σ(x_{n})) = a.σ(t), where σ : {x_{1}, …, x_{n}} → T T(Σ) is the substitution given by σ(x_{i}) = c_{i}.y_{i} for i ∈ I and σ(x_{i}) = x_{i} for i ∉ I. Such an axiom is called an action law. Examples are CM2 and CM5 in Table 1.

Secondly, whenever I is the set of active arguments of f, but f has no rule of the form above (where the name of the variables y_{i} is of no importance), there is an axiom f(σ(x_{1}), …, σ(x_{n})) = 0, with σ as above (for an arbitrary choice of distinct variables y_{i}). Such an axiom is an inaction law. An example is CM6. If f has k active arguments, in total there are |Act|^{k} action and inaction laws for f, one for every conceivable trigger with as domain the active arguments of f.

Finally, for any active argument i of f, there are laws

f(x_{1}, … x_{i−1}, 0, x_{i+1}, …, x_{n}) = 0 and f(x_{1}, …, x_{i} + x′_{i}, …, x_{n}) = f(x_{1}, …, x_{i}, …, x_{n}) + f(x_{1}, …, x′_{i}, …, x_{n}).

Examples for the second type of inaction law are CM3 and CM7, and examples of distributivity laws are CM4, CM8 and CM9.

It is not hard to see that all axioms above respect \underline{↔} and that together they bring any term f(p_{1}, …, p_{ar(f)}) with the p_{i} basic processes in head normal form.

The method of [1] makes three types of additions to a given finite GSOS language L, and provides an equational head normalising axiomatisation on the resulting language, that respects strong bisimulation.

First of all, the operators 0, a. and + are added, if not already there. The corresponding axioms are A1–4 of Table 1. If all other operators are smooth and distinctive, for each of them the axioms just described are taken, which finishes the job. (In the presence of negative premises, this step is slightly more complex.)

In case there are operators f that are smooth but not distinctive, the set of operational rules of f is partitioned into subsets D such that no two rules in D have the same trigger, and the triggers of all rules in D have the same domain. Note that such a partition can always be found—possibly by taking exactly one rule in each subset D. Now for any subset D in the partition, an operator f_{D} with ar(f_{D}) = ar(f) is added to the language, whose rules are exactly the rules in that subset, but with f_{D} in the source. By definition, f_{D} is distinctive. Now add an axiom f(x_{1}, …, x_{ar(f)}) = ∑ f_{D}(x_{1}, …, x_{ar(f)}), where the sum is taken over all subsets in the partition, and apply the method above to the operators f_{D}. Again, it is trivial to check that the axioms respect \underline{↔} and are head normalising. Applied to the ∥ of CCS, this technique yields the left merge and communication merge as auxiliary operators, as well as a right merge, and the axiom CM1.

In case of operators f that are not smooth, a smooth operator f^{⋆} is added to L, of which f is an abbreviation in the sense of Definition 9 (cf. Example 1). The treatment of f^{⋆} proceeds as above, and the project is finished by the axiom

f(p_{1}, ..., p_{n}) = f^{⋆}(p_{f(1)}, ..., p_{f(n)}).

Besides completeness for finite processes, using an infinitary induction principle the method of [1] even yields completeness for arbitrary processes. I will not treat this here, as it does not generalise to weak equivalences.

7 Turning Cool GSOS Rules into Equations

The method of [1] does not apply to \underline{↔}_{w}, \underline{↔}_{d}, \underline{↔}_{η}, and \underline{↔}_{b}, because these equivalences fail to be congruences for the +. However, Bloom [4] shows that the method applies more or less verbatim to \underline{↔}_{rb}. This section observes that the same holds for \underline{↔}_{rη}, and finds an adaptation to yield finite equational axiomatisations of \underline{↔}_{rw} (resp. \underline{↔}_{rd}) that are sound and complete for finite processes on an augmentation of any RWB cool (resp. RDB cool) GSOS language.

On basic processes, the axioms A1–4 together with T1–T3 are complete for \underline{↔}_{rw} [8], whereas complete axiomatisations for \underline{↔}_{rd}, \underline{↔}_{rη} and \underline{↔}_{rb} are obtained by dropping T3, T2 or both, respectively [7]. So in order to get axiomatisations of these equivalences that are complete for finite processes, all that is needed is head normalisation. The simplest approach is to use the same head normalising axioms as in the previous section, reasoning that axioms that respect \underline{↔} surely respect a coarser equivalence like \underline{↔}_{rb} or \underline{↔}_{rw}. The only way this approach could fail is when the auxiliary operators generated by [1] fail to be congruences for the equivalence relation at hand. The operators 0, a. and + are WB cool, and thus unproblematic. As observed in [4], for any RBB cool GSOS language, the augmented language is also RBB cool. Namely, the new operators do not show up in targets of new rules, so classifying all auxiliary operators as wild is sufficient. Since the auxiliary operators do not increase the collection of receiving arguments of operators either, it follows likewise that for any RHB cool GSOS language, the augmented language is also RHB cool. Hence one obtains

Proposition 4. The method of [1], together with axiom T1 (and T3), yields finite equational axiomatisations of \underline{↔}_{rb} (resp. \underline{↔}_{rη}) that are sound and complete for finite processes on an augmentation of any RBB cool (resp. RHB cool) GSOS language.

For \underline{↔}_{rw} and \underline{↔}_{rd} this approach fails. In particular, these equivalences fail to be congruences for the communication merge: one has τ.a.0\underline{↔}_{rd} τ.a.0 + a.0 but

0\underline{↔} (τ.a.0|\overline{a}.b.0)\underline{↮}_{rd} ((τ.a.0 + a.0)|\overline{a}.b.0)\underline{↔} τ.b.0.

Conjecture. There exists no GSOS language including the parallel composition of CCS and ≥2 visible actions that admits a finite equational axiomatisation of weak bisimulation equivalence that is sound and complete for finite processes.

Nevertheless, such an axiomatisation was found by Bergstra & Klop [3], using a variant of the communication merge that is not a GSOS operator. Their axiomatisation of ∥ is obtained from the one in Table 1 by requiring a, b ≠ τ in CM6, and adding the axioms τ.x|y = x|τ.y = x|y. Here I generalise their approach to arbitrary RWB cool (or RDB cool) GSOS languages.

The RWB cool format can be extended by allowing wild operators f, besides GSOS rules satisfying Clause 3 of Definition 12, also to have rules of which all premises have the form x ⟹⟶^{c} y with c ∈ A. For such rules Clause 3 is not required, but in fulfilling Clause 4, they do count in determining which arguments are receiving. A similar extension applies to the RDB cool format.

Theorem 4. On any extended-RWB cool TSS, \underline{↔}_{rw} is a congruence. On any extended-RDB cool TSS, \underline{↔}_{rd} is a congruence.

In an RWB (or RDB) cool language, the smooth operators f^{⋆} that are needed to axiomatise a non-smooth operator f are unproblematic. For tame operators f, they are already in the language, and for a wild f it is not hard to define them in such a way that the augmented language remains RWB (or RDB) cool. Of the operators f_{D} needed to axiomatise a non-distinctive operator f, those that have exactly one active argument can be made to satisfy Clause 3 of Definition 12 by including the relevant τ-rule in D. All operators f_{D} with another number of active arguments cannot have τ-premises, by Definitions 12 and 10. These operators f_{D} are replaced by counterparts f′_{D}, obtained by replacing each premise x ⟶^{c} y in a rule for f_{D} by x ⟹⟶^{c} y. By Theorem 4, \underline{↔}_{rw} (or \underline{↔}_{rd}) is a congruence for f′_{D}. Furthermore, f(x_{1}, …, x_{ar(f)}) \underline{↔}_{rw} ∑ f′_{D}(x_{1}, …, x_{ar(f)}). Now the required axiomatisation is obtained by omitting all inaction laws for the modified operators f′_{D} with σ(x_{i}) = τ.y_{i} for some active argument i, and instead adding τ-laws f′_{D}(x_{1}, …, τ.x_{i}, …, x_{n}) = f′_{D}(x_{1}, …, x_{i}, …, x_{n}).

8 A Challenge

All equivalences of Definition 5 are congruences of the GSOS language with rules

\frac{x_{1} ⟶^{a} y}{f(x_{1}) ⟶^{a} g(y)} \frac{x_{1} ⟶^{τ} y}{g(x_{1}) ⟶^{τ} g(y)} g(x_{1}) ⟶^{τ}!x_{1}

\frac{x_{1} ⟶^{a} y}{!x_{1} ⟶^{a} y∥!x_{1}}  \frac{x_{1} ⟶^{a} y_{1}}{x_{1}∥x_{2} ⟶^{a} y_{1}∥x_{2}}  \frac{x_{2} ⟶^{a} y_{2}}{x_{1}∥x_{2} ⟶^{a} x_{1}∥y_{2}}

for a∈Act. Here, the operator !x can be understood as a parallel composition of infinitely many copies of x. The rules for f, g and ∥ are WB cool, but the one for ! is not. It is not even RBB safe in the sense of [6].

Open problem. Find a congruence format that includes the language above.

References

1. L. Aceto, B. Bloom & F.W. Vaandrager (1994): Turning SOS rules into equations. Information and Computation 111(1), pp. 1–52.

2. T. Basten (1996): Branching bisimulation is an equivalence indeed! Information Processing Letters 58(3), pp. 141–147.

3. J.A. Bergstra & J.W. Klop (1985): Algebra of communicating processes with abstraction. Theoretical Computer Science 37(1), pp. 77–121.

4. B. Bloom (1995): Structural operational semantics for weak bisimulations. Theoretical Computer Science 146, pp. 25–68.

5. B. Bloom, S. Istrail & A.R. Meyer (1995): Bisimulation can’t be traced. Journal of the ACM 42(1), pp. 232–268.

6. W.J. Fokkink (2000): Rooted branching bisimulation as a congruence. Journal of Computer and System Sciences 60(1), pp. 13–37.

7. R.J. van Glabbeek & W.P. Weijland (1996): Branching time and abstraction in bisimulation semantics. Journal of the ACM 43(3), pp. 555–600.

8. R. Milner (1990): Operational and algebraic semantics of concurrent processes. In J. van Leeuwen, editor: Handbook of Theoretical Computer Science, chapter 19, Elsevier Science Publishers B.V. (North-Holland), pp. 1201–1242. Alternatively see Communication and Concurrency, Prentice-Hall International, Englewood Cliffs, 1989, or A Calculus of Communicating Systems, LNCS 92, Springer-Verlag, 1980.

9. F. Moller (1990): The nonexistence of finite axiomatisations for CCS congruences. In Proceedings 5^{th} Annual Symposium on Logic in Computer Science, Philadelphia, USA, IEEE Computer Society Press, pp. 142–153.

10. G.D. Plotkin (2004): A structural approach to operational semantics. The Journal of Logic and Algebraic Programming 60–61, pp. 17–139. First appeared in 1981.

11. R. de Simone (1985): Higher-level synchronising devices in Meije-SCCS. Theoretical Computer Science 37, pp. 245–267.

12. I. Ulidowski (1992): Equivalences on observable processes. In Proceedings 7^{th} Annual Symposium on Logic in Computer Science, Santa Cruz, California, IEEE Computer Society Press, pp. 148–159.

13. I. Ulidowski & I. Phillips (2002): Ordered SOS rules and process languages for branching and eager bisimulations. Information & Computation 178, pp. 180–213.

14. I. Ulidowski & S. Yuen (2000): Process languages for rooted eager bisimulation. In C. Palamidessi, editor: Proceedings of the 11th International Conference on Concurrency Theory, CONCUR 2000, LNCS 1877, Springer, pp. 275–289.

Appendix for Referees

A The congruence proofs for the simply cool rule formats

In this appendix I first prove the result from [5] that strong bisimulation equivalence is a congruence for all GSOS operators. Then I change this proof in minimal ways so as to obtain the congruence results for the simply cool GSOS languages. In doing so, for each simply cool GSOS format I state a lemma that tells exactly what is needed to make the congruence proof work.

Theorem 5 ([5]). On any GSOS language, strong bisimulation equivalence is a congruence.

Proof. Let R be the smallest relation on processes satisfying

• if p\underline{↔} q then pRq, and

• if p_{i}Rq_{i} for i = 1, …, ar(f) then f(p_{1}, …, p_{ar(f)})Rf(q_{1}, …, q_{ar(f)}).

It suffices to show that R is a strong bisimulation, because this implies that R equals \underline{↔}, and by construction R is a congruence. Because \underline{↔} is symmetric, so is R. So it remains to show that

if pRq and p ⟶^{a} p′, with a ∈ Act, then ∃q′ such that q ⟶^{a} q′ and p′Rq′.

This I will do with induction on the number of applications of the second clause in the definition of R above in establishing that pRq. Note that this number is the same for qRp.

Base case: Let p \underline{↔} q and p ⟶^{a} p′. Using that \underline{↔} is a strong bisimulation, there must be a process q′ such that q ⟶^{a} q′ and p′ \underline{↔} q′, hence p′Rq′.

Induction step: Let p = f(p_{1}, …, p_{n}) and q = f(q_{1}, …, q_{n}) where p_{i}Rq_{i} for i = 1, …, n, and p_{i}Rq_{i} is established in less applications of the second step than pRq. By induction, one may assume

if p_{i} ⟶^{c} p′ then there is a q′ such that q_{i} ⟶^{c} q′ and p′Rq′  (2)
if q_{i} ⟶^{c} q′ then there is a p′ such that p_{i} ⟶^{c} p′ and p′Rq′  (3)

for i = 1, ..., n and c ∈ Act. Let p ⟶^{a} p′. By Definition 4, there must be a rule \frac{H}{f(x_{1},...,x_{n})⟶^{a}t} in L and a closed substitution σ with σ(x_{i}) = p_{i} for i = 1, ..., n

and σ(t) = p′, such that p_{i} ⟶^{c} σ(y) for (x_{i} ⟶^{c} y) ∈ H and ¬∃r(p_{i} ⟶^{c} r) for

(x_{i} −̸→^{c}) ∈ H.

For (x_{i} ⟶^{c} y) ∈ H, using that p_{i} ⟶^{c} σ(y), by (2) there is a q_{y} such that

q_{i} ⟶^{c} q_{y} and σ(y)Rq_{y}.

For (x_{i} −̸→^{c}) ∈ H, using that ¬∃r(p_{i} ⟶^{c} r), by (3) there can not be a s ∈ T (Σ) with q_{i} ⟶^{c} s. Let ν be a substitution with ν(x_{i}) = q_{i} for i = 1, …, n and ν(y) = q_{y} if y is the right-hand side of a premise in H, taking ν(z) = σ(z) for all other variables z; by the last clause of Definition 3 such a substitution ν does indeed exist. I now have σ(x)Rν(x) for all x ∈ V, and hence σ(t)Rν(t) by the definition of R. Take q′ = ν(t). So p′Rq′. Moreover, q_{i} ⟶^{c} ν(y) for (x_{i} ⟶^{c} y) ∈ H and ¬∃r(q_{i} ⟶^{c} r) for (x_{i} −̸→^{c}) ∈ H. Thus, by Definition 4,

q = f(q_{1}, …, q_{n}) ⟶^{a} ν(t) = q′. ⊓ ⊔

20  Rob van Glabbeek

Lemma WB Let L be simply WB cool, let \frac{H}{s⟶^{a}t} be a rule in L, and let ν be a closed substitution. If for each premise x⟶^{c}y in H one has ν(x)⟹⟶^{(c)}⟹ν(y),

then ν(s) ⟹⟶^{(a)}⟹ ν(t).

Lemma RWB Let L be simply RWB cool, let \frac{H}{s⟶^{a}t} be a rule in L, and let ν be a closed substitution. If for each premise x ⟶^{c} y in H one has

ν(x) ⟹⟶^{c}⟹ ν(y), then ν(s) ⟹⟶^{a}⟹ ν(t).

Lemma DB Let L be simply DB cool, let \frac{H}{s⟶^{a}t} be a rule in L, and let ν be a closed substitution. If for each premise x ⟶^{c} y in H one has ν(x) ⟹⟶^{(c)} ν(y),

then ν(s) ⟹⟶^{(a)} ν(t).

Lemma RDB Let L be simply RDB cool, let \frac{H}{s⟶^{a}t} be a rule in L, and let ν be a closed substitution. If for each premise x ⟶^{c} y in H one has ν(x) ⟹⟶^{c} ν(y),

then ν(s) ⟹⟶^{a} ν(t).

Lemma HB Let L be simply HB cool, let \frac{\{x_{i}⟶^{c_{i}}y_{i}|i∈I\}}{f(x_{1},...,x_{n})⟶^{a}t} be a rule in L, and let ρ, ν be closed substitutions satisfying ρ(x_{i}) ⟹ ν(x_{i}) ⟶^{(c_{i})}⟹ ν(y_{i}) for i∈I and

ρ(x_{i}) = ν(x_{i}) for i∉I. Then ρ(f(x_{1}, ..., x_{n})) ⟹ ν(f(x_{1}, ..., x_{n})) ⟶^{(a)}⟹ ν(t).

Lemma RHB Let L be simply RHB cool, let \frac{H}{s⟶^{a}t} be a rule in L, and let ν be a closed substitution such that ν(x) ⟶^{c}⟹ ν(y) for each positive premise x ⟶^{c} y in H and ¬∃r (ν(x) −̸→^{c} r) for each negative premise x −̸→^{c} in H. Then

ν(s) ⟶^{a}⟹ ν(t).

Lemma BB Let L be simply BB cool, let \frac{\{x_{i}⟶^{c_{i}}y_{i}|i∈I\}}{f(x_{1},...,x_{n})⟶^{a}t} be a rule in L, and let ρ, ν be closed substitutions satisfying ρ(x_{i}) ⟹ ν(x_{i}) ⟶^{(c_{i})} ν(y_{i}) for i∈I and

ρ(x_{i}) = ν(x_{i}) for i∉I. Then ρ(f(x_{1}, ..., x_{n})) ⟹ ν(f(x_{1}, ..., x_{n})) ⟶^{(a)} ν(t).

Lemma RBB Let L be simply RBB cool, let \frac{H}{s⟶^{a}t} be a rule in L, and let ν be a closed substitution such that ν(x) ⟶^{c} ν(y) for each positive premise x ⟶^{c} y in H and ¬∃r (ν(x) −̸→^{c} r) for each negative premise x −̸→^{c} in H. Then

ν(s) ⟶^{a} ν(t).

By Definition 4, the last lemma holds trivially. The others will be obtained in Appendices B and D. With these lemmas the congruence proofs are easy. I will only present the representative cases of (rooted) weak and branching bisimulation equivalence.

Theorem 1WB On any simply WB cool GSOS language, \underline{↔}_{w} is a congruence.

Proof. Let R be the smallest relation on processes satisfying

• if p\underline{↔}_{w} q then pRq, and

• if p_{i}Rq_{i} for i = 1, …, ar(f) then f(p_{1}, …, p_{ar(f)})Rf(q_{1}, …, q_{ar(f)}).

It suffices to show that R is a weak bisimulation, because this implies that R equals \underline{↔}_{w}, and by construction R is a congruence. Because \underline{↔}_{w} is symmetric, so is R. So it remains to show that

if pRq and p ⟶^{a} p′, then there is a q′ such that q ⟹⟶^{(a)}⟹ q′ and p′Rq′.

This I will do with induction on the number of applications of the second clause in the definition of R above in establishing pRq.

Base case: Let p\underline{↔}_{w} q and p ⟶^{a} p′. Using that \underline{↔}_{w} is a weak bisimulation, there must be a process q′ such that q ⟹⟶^{(a)}⟹ q′ and p′ \underline{↔}_{w} q′, hence p′Rq′.

Induction step: Let p = f(p_{1}, …, p_{n}) and q = f(q_{1}, …, q_{n}) where p_{i}Rq_{i} for i = 1, …, n, and p_{i}Rq_{i} is established in less applications of the second step than pRq. By induction, one may assume

if p_{i} ⟶^{c_{i}} p′_{i} then there is a q′_{i} such that q_{i} ⟹⟶^{(c_{i})}⟹ q′_{i} and p′_{i}Rq′_{i} (4)

for i = 1, ..., n and c_{i} ∈ Act. Let p ⟶^{a} p′. By Definition 4, there must be a rule

\frac{\{x_{i}⟶^{c_{i}}y_{i}|i∈I\}}{f(x_{1},...,x_{n})⟶^{a}t} in L and a closed substitution σ with σ(x_{i}) = p_{i} for i = 1, …, n

and σ(t) = p′, such that p_{i} ⟶^{c_{i}} σ(y_{i}) for i ∈ I. So by (4), for i ∈ I there is a q′_{i} such that q_{i} ⟹⟶^{(c_{i})}⟹ q′_{i} and σ(y_{i})Rq′_{i}. Let ν be a substitution with ν(x_{i}) = q_{i} for i = 1, …, n and ν(y_{i}) = q′_{i} for i ∈ I, taking ν(z) = σ(z) for all other variables z. I now have σ(x)Rν(x) for all x ∈ V, and hence σ(t)Rν(t) by the definition of R. Take q′ = ν(t). Then p′Rq′. Moreover, ν(x_{i}) ⟹⟶^{(c_{i})}⟹ ν(y_{i}) for each i ∈ I. Thus, by Lemma WB, q = ν(f(x_{1}, …, x_{n})) ⟹⟶^{(a)}⟹ ν(t) = q′. ⊓ ⊔

Theorem 1RWB On any simply RWB cool GSOS language, \underline{↔}_{rw} is a congruence.

Proof. Let f be an operator of arity n, and let p_{i} \underline{↔}_{rw} q_{i} for i = 1, …, n. I

have to show that f(p_{1}, …, p_{n}) \underline{↔}_{rw} f(q_{1}, …, q_{n}). Let f(p_{1}, …, p_{n}) ⟶^{a} p′. By

Definition 4, there must be a rule _{\frac{H}{f(x_{1},...,x_{n})⟶^{a}t}} in L and a closed substitution

σ with σ(x_{i}) = p_{i} for i = 1, ..., n and σ(t) = p′, such that p_{i} ⟶^{c} σ(y) for (x_{i} ⟶^{c} y) ∈ H. For any (x_{i} ⟶^{c} y) ∈ H, using that p_{i} \underline{↔}_{rw} q_{i}, there is a q_{y} such that q_{i} ⟹⟶^{c}⟹ q_{y} and σ(y) \underline{↔}_{w} q_{y}. Let ν be a substitution with ν(x_{i}) = q_{i} for i = 1, …, n and ν(y) = q_{y} if y is the right-hand side of a premise in H, taking ν(z) = σ(z) for all other variables z; by the last clause of Definition 3 such a substitution ν does indeed exist. I now have σ(x) \underline{↔}_{w} ν(x) for all x ∈ V, and hence σ(t) \underline{↔}_{w} ν(t) by Theorem 1WB. Take q′ = ν(t). So p′ \underline{↔}_{w} q′. Moreover, ν(x_{i}) ⟹⟶^{c}⟹ ν(y) for each premise (x_{i} ⟶^{c} y) ∈ H. Thus, by Lemma RWB,

f(q_{1}, …, q_{n}) = ν(f(x_{1}, …, x_{n})) ⟹⟶^{a}⟹ ν(t) = q′.

The case assuming f(q_{1}, …, q_{n}) ⟶^{a} q′ follows by symmetry. ⊓ ⊔ Theorem 1BB On any simply BB cool GSOS language, \underline{↔}_{b} is a congruence.

Proof. Let R be the smallest relation on processes satisfying

• if p\underline{↔}_{b} q then pRq, and

• if p_{i}Rq_{i} for i = 1, …, ar(f) then f(p_{1}, …, p_{ar(f)})Rf(q_{1}, …, q_{ar(f)}).

It suffices to show that R is a branching bisimulation, because this implies that R equals \underline{↔}_{b}, and by construction R is a congruence. Because \underline{↔}_{b} is symmetric, so is R. So it remains to show that

if pRq and p ⟶^{a} p′ then ∃q^{pre}, q′ with q ⟹ q^{pre} ⟶^{(a)} q′, pRq^{pre} and p′Rq′.

This I will do with induction on the number of applications of the second clause in the definition of R above in establishing pRq.

Base case: Let p \underline{↔}_{b} q and p ⟶^{a} p′. Using that \underline{↔}_{b} is a branching bisimulation, there must be processes q^{pre}, q′ such that q ⟹ q^{pre} ⟶^{(a)} q′, p \underline{↔}_{b} q^{pre} and p′ \underline{↔}_{b} q′, hence pRq^{pre} and p′Rq′.

Induction step: Let p = f(p_{1}, …, p_{n}) and q = f(q_{1}, …, q_{n}) where p_{i}Rq_{i} for i = 1, …, n, and p_{i}Rq_{i} is established in less applications of the second step than pRq. By induction, one may assume

if p_{i} ⟶^{c_{i}} p′_{i} then ∃q_{i}^{pre}, q′_{i} such that q_{i} ⟹ q_{i}^{pre} ⟶^{(c_{i})} q′_{i}, p_{i}Rq_{i}^{pre} and p′_{i}Rq′_{i} (5)

for i = 1, ..., n and c_{i} ∈ Act. Let p ⟶^{a} p′. By Definition 4, there must be a

rule \frac{\{x_{i}⟶^{c_{i}}y_{i}|i∈I\}}{f(x_{1},...,x_{n})⟶^{a}t} in L and a closed substitution σ with σ(x_{i}) = p_{i} for i =

1, …, n and σ(t) = p′, such that p_{i} ⟶^{c_{i}} σ(y_{i}) for i ∈ I. So by (5), for i ∈ I

there are q_{i}^{pre}, q′_{i} such that q_{i} ⟹ q_{i}^{pre} ⟶^{(c_{i})} q′_{i}, p_{i}Rq_{i}^{pre} and σ(y_{i})Rq′_{i}. Let ν be a

substitution with ν(x_{i}) = q_{i}^{pre} and ν(y_{i}) = q′_{i} for i ∈ I and ν(x_{i}) = q_{i} for i ∉ I, taking ν(z) = σ(z) for all other variables z. I now have σ(x)Rν(x) for all x ∈ V, and hence σ(t)Rν(t) and σ(f(x_{1}, …, x_{n})Rν(f(x_{1}, …, x_{n}) by the definition of R. Take q^{pre} = ν(f(x_{1}, …, x_{n})) and q′ = ν(t). So pRq^{pre} and p′Rq′. Moreover, q_{i} ⟹ ν(x_{i}) ⟶^{(c_{i})} ν(y) for each i ∈ I. Thus Lemma BB, taking ρ to be a closed substitution with ρ(x_{i}) = q_{i}, yields q ⟹ q^{pre} ⟶^{(a)} q′. ⊓ ⊔

Theorem 1RBB On any simply RBB cool GSOS language, \underline{↔}_{rb} is a congruence.

Proof. Let f be an operator of arity n, and let p_{i} \underline{↔}_{rb} q_{i} for i = 1, …, n. I

have to show that f(p_{1}, …, p_{n}) \underline{↔}_{rb} f(q_{1}, …, q_{n}). Let f(p_{1}, …, p_{n}) ⟶^{a} p′. By

Definition 4, there must be a rule _{\frac{H}{f(x_{1},...,x_{n})⟶^{a}t}} in L and a closed substitution

σ with σ(x_{i}) = p_{i} for i = 1, ..., n and σ(t) = p′, such that p_{i} ⟶^{c} σ(y) for

(x_{i} ⟶^{c} y) ∈ H and ¬∃r(p_{i} ⟶^{c} r) for (x_{i} −̸→^{c}) ∈ H.

For any (x_{i} ⟶^{c} y) ∈ H, using that p_{i} \underline{↔}_{rb} q_{i}, there is a q_{y} such that q_{i} ⟶^{c} q_{y} and σ(y)\underline{↔}_{b} q_{y}.

For any (x_{i} −̸→^{c}) ∈ H, using that p_{i} \underline{↔}_{rb} q_{i}, there can not be a s ∈ T (Σ) with

q_{i} ⟶^{c} s.

Let ν be a substitution with ν(x_{i}) = q_{i} for i = 1, …, n and ν(y) = q_{y} if y is the right-hand side of a premise in H, taking ν(z) = σ(z) for all other variables z; by the last clause of Definition 3 such a substitution ν does indeed exist. I now have σ(x)\underline{↔}_{b} ν(x) for all x ∈ V, and hence σ(t)\underline{↔}_{b} ν(t) by Theorem 1BB. Take q′ = ν(t). So p′ \underline{↔}_{b} q′. Moreover, ν(x_{i}) ⟶^{c} ν(y) for each premise x_{i} ⟶^{c} y in H and ¬∃r(ν(x_{i}) ⟶^{c} r) for each premise x_{i} −̸→^{c} in H. Thus, by Lemma RBB, or

Definition 4, f(q_{1}, …, q_{n}) = ν(f(x_{1}, …, x_{n})) ⟶^{a} ν(t) = q′.

The case assuming f(q_{1}, …, q_{n}) ⟶^{a} q′ follows by symmetry. ⊓ ⊔

B Proofs of Lemmas WB–BB

Lemma 2. Suppose L satisfies Clause 4 in Definition 8 of simply WB cool, and let μ, ν be closed substitutions. If μ(y) ⟹ ν(y) for every y ∈ var(t) that is receiving in t, and μ(x) = ν(x) for every x ∈ var(t) that is not receiving in t, then μ(t) ⟹ ν(t).

Proof. By structural induction on t. If t is a variable, the statement follows by assumption. Otherwise, t = f(t_{1}, …, t_{n}). It suffices to show that for i = 1, …, n one has

f(ν(t_{1}), ..., ν(t_{i−1}), μ(t_{i}), μ(t_{i+1}), ..., μ(t_{n})) ⟹
f(ν(t_{1}), ..., ν(t_{i−1}), ν(t_{i}), μ(t_{i+1}), ..., μ(t_{n})).  (6)

If t_{i} contains no variable that is receiving in t, then μ(t_{i}) = ν(t_{i}) by assumption, which yields (6). If t_{i} does contains such a variable, then, by definition, i is a receiving argument of g. By induction, μ(t_{i}) ⟹ ν(t_{i}), and the patience rule for the i^{th} argument of g yields (6).

Proof of Lemma WB: Let L be simply WB cool, let r = \frac{\{x_{i} ⟶^{c_{i}} y_{i} | i ∈ I\}}{f(x_{1}, …, x_{n}) ⟶^{a} t} be a rule in L and let μ, ν be closed substitutions such that

• ν(x_{i}) ⟹ μ(x_{i}) ⟶^{(c_{i})} μ(y_{i}) ⟹ ν(y_{i}) for i∈I,

• ν(x) = μ(x) for all variables x that do not occur in the premises of r.

I need to show that ν(f(x_{1}, …, x_{n})) ⟹⟶^{(a)}⟹ ν(t).

In case r is a patience rule—so I = {k}, c_{k} = τ and t = f(x_{1}, …, x_{n})[y/x_{k}]

with 1 ≤ k ≤ n—one has ν(f(x_{1}, ..., x_{n})) ⟹ μ(f(x_{1}, ..., x_{n})) ⟶^{(τ)}

μ(f(x_{1}, ..., x_{n})[y/x_{k}]) ⟹ ν(f(x_{1}, ..., x_{n})[y/x_{k}]) by repeated application of r.

Otherwise, ⟶^{(c)} = ⟶^{c} by Clause 2 of Definition 8. Now ν(f(x_{1}, …, x_{n})) ⟹ μ(f(x_{1}, …, x_{n})) by Clause 3, and μ(f(x_{1}, …, x_{n})) ⟶^{a} μ(t) by application of r. Clause 5 yields that μ(x) = ν(x) for all variables x ∈ var(t) that are not receiving in t, so μ(t) ⟹ ν(t) by Lemma 2. ⊓ ⊔

The Proof of Lemma DB proceeds likewise, but taking μ(x) = ν(x) for all variables x that do not occur in the left-hand side of premises. Clause 5 now implies that μ(t) = ν(t). ⊓ ⊔ Proof of Lemma HB: Let L be simply HB cool, let r = \frac{\{x_{i} ⟶^{c_{i}} y_{i} | i ∈ I\}}{f(x_{1}, …, x_{n}) ⟶^{a} t} be a rule in L and let ρ, μ, ν be closed substitutions such that

• ρ(x_{i}) ⟹ ν(x_{i}) ⟶^{(c_{i})} μ(y_{i}) ⟹ ν(y_{i}) for i∈I,

• ρ(x_{i}) = ν(x_{i}) = μ(x_{i}) for i∉I, and

• ν(x) = μ(x) for all variables x that do not occur as right-hand sides of premises in H.

I need to show that ρ(f(x_{1}, …, x_{n})) ⟹ ν(f(x_{1}, …, x_{n})) ⟶^{(a)}⟹ ν(t).

Note that ν(f(x_{1}, …, x_{n})) = μ(f(x_{1}, …, x_{n})).

In case r is a patience rule—so I = {k}, c_{k} = τ and t = f(x_{1}, …, x_{n})[y/x_{k}]

with 1 ≤ k ≤ n—one has ρ(f(x_{1}, ..., x_{n})) ⟹ ν(f(x_{1}, ..., x_{n})) ⟶^{(τ)}

μ(f(x_{1}, ..., x_{n})[y/x_{k}]) ⟹ ν(f(x_{1}, ..., x_{n})[y/x_{k}]) by repeated application of r.

Otherwise, ⟶^{(c)} = ⟶^{c} by Clause 2 of Definition 8. Now ρ(f(x_{1}, …, x_{n})) ⟹ ν(f(x_{1}, …, x_{n})) by Clause 3, ν(f(x_{1}, …, x_{n})) ⟶^{a} μ(t) by application of r; and μ(t) ⟹ ν(t) by Lemma 2. ⊓ ⊔

The Proof of Lemma BB proceeds likewise, but omitting μ. ⊓ ⊔

C Cool GSOS languages

Given that the cool GSOS languages differ from the simply cool GSOS language only by the addition of operators that can be regarded as syntactic sugar, the Theorem 2 is a simple consequence of the corresponding theorems for simply cool GSOS languages. Below I go through the details.

Definition 17. Let L be a two-tiered GSOS language, with signature Σ. Let Σ^{⋆} be the subcollection of principal operators in Σ, and Σ^{∗} = {f^{∗} | f ∈ Σ^{⋆}} be a collection of fresh names for the latter. For f ∈ Σ an abbreviation, write f^{∗} for (f^{⋆})^{∗}. Define the translation ^{∗} : T (Σ) → T (Σ^{∗}) recursively by x^{∗} = x for x ∈ V and (f(t_{1}, …, t_{n}))^{∗} = f^{∗}(t_{f(1)}^{∗}, …, t_{f(n)}^{∗}). Let L^{∗} be the GSOS

language with signature Σ^{∗} and rules \frac{H}{f^{∗}(x_{1}, …, x_{ar(f)}) ⟶^{a} t^{∗}} for f ∈ Σ^{⋆} and

\frac{H}{f(x_{1}, …, x_{ar(f)}) ⟶^{a} t} a rule of L.

Observation 1. Let L be XB cool, with X∈ {W,D,H,B}. Then L^{∗} is simply XB cool.

Any equivalence relation ∼ on processes defined in terms of the transitions between them, naturally extends to an equivalence relation on the disjoint union of T (Σ) and T (Σ^{∗}), with L generating the transitions between processes from T (Σ) and L^{∗} generating the transitions between processes from T (Σ)^{∗} (see Definition 4).

Lemma 3. Let L be a two-tiered GSOS language.

Then p^{∗} ⟶^{a}_{L^{∗}} p′ iff ∃p_{1}(p′ = p_{1}^{∗} ∧ p ⟶^{a}_{L} p_{1}).

Proof. By structural induction on p ∈ T (Σ), using that t^{∗}[u^{∗}/x] = (t[u/x])^{∗}. ⊓ ⊔

Corollary 1. Let L be a two-tired GSOS language, and ∼ be any equivalence relation on processes satisfying p \underline{↔} q ⇒ p ∼ q. Then p^{∗} ∼ q^{∗} iff p ∼ q.

Proof. We have p\underline{↔} p^{∗} for all p ∈ T (Σ), because \{(p, p^{∗}), (p^{∗}, p) | p ∈ T (Σ)\} is a strong bisimulation by Lemma 3. Hence if p ∼ q then p^{∗} \underline{↔} p ∼ q \underline{↔} q∗, implying p^{∗} ∼ q^{∗}, and if p^{∗} ∼ q^{∗} then p\underline{↔} p^{∗} ∼ q^{∗} \underline{↔} q, implying p ∼ q. ⊓ ⊔

Corollary 2. Let L be a two-tiered GSOS language such that ∼ is a congruence on L^{∗}, for ∼ an equivalence relation satisfying p \underline{↔} q ⇒ p ∼ q. Then ∼ is a congruence on L.

Proof. Let ar(f) = n. Suppose p_{i} ∼ q_{i} for i = 1, ..., n. By Cor. 1, p_{i}^{∗} ∼ q_{i}^{∗} for i = 1, ..., n. By assumption, (f(p_{1}, ..., p_{n}))^{∗} ∼ (f(q_{1}, ..., q_{n}))^{∗}. Thus, by Cor. 1, f(p_{1}, ..., p_{n}) ∼ f(q_{1}, ..., q_{n}). ⊓ ⊔

Proof of Theorem 2: Let L be XB cool, with X∈ {W,D,H,B}. By Obs. 1, L^{∗} is simply XB cool. So by Theorem 1, \underline{↔}_{X} is a congruence on L^{∗}. Apply Cor. 2.

⊓ ⊔

D Rooted cool GSOS languages

Lemma 4. Suppose an L-ruloid has a premise with right-hand side x and a target t containing a subterm f(t_{1}, …, t_{n}) with x ∈ var(t_{i}). Then i is a receiving argument of f.

Proof. By Definition 11 there must be terms w_{1}, …, w_{n}, variables y_{1}, …, y_{n}, and substitutions σ_{1}, …, σ_{n}, such that t = σ_{1}(w_{1}), y_{i} is receiving in w_{i} (i = 1, ..., n), σ_{i}(y_{i})=σ_{i+1}(w_{i+1}) (i=1, ..., n − 1), and σ(y_{n}) = x; and moreover one of the w_{k} has a subterm f(w_{k}^{1}, …, w_{k}^{n}) with y_{k} ∈ var(w_{k}^{i}). It follows that i is an receiving argument of f. ⊓ ⊔

Proposition 5. In Definition 12 of the RWB cool format above, the Clause 4 is redundant.

Proof. Let argument i of operator f be L-receiving. I will show that it is already L^{tame}-receiving. Let t be a term with a subterm f(t_{1}, …, t_{n}) such that y ∈ var(t_{i}) and y is L-receiving in t. So there is a rule r = _{\frac{H}{f(x_{1},...,x_{n})⟶^{a}t}} in L with

y occurring as the right-hand side of a premise in H. Let u and σ be the term and substitution that must exists for r by the third clause of Definition 12. Definition 12 implies that the operators in u are tame, and there is an L-ruloid, hence an L^{tame}-ruloid, \frac{K}{u⟶^{a}v} with σ(K) = H and σ(v) = t. Let f(v_{1}, …, v_{n}) be the subterm of v with σ(v_{i}) = t_{i} for i = 1, …, n. By the last clause of Definition 3, y ∉ range(σ). Hence, as y ∈ var(σ(v_{i})), y ∈ var(v_{i}). Given that dom(σ) = var(u), σ does not effect the right-hand sides of K, so y is the righthand side of a premise in K. By Lemma 4, i is an L^{tame}-receiving argument of f. ⊓ ⊔

When working with the slightly stronger definition of receiving contemplated in Section 3.1, the proof above remains valid with trivial adaptations.

Now I will prove the remaining lemmas of Section A, thereby completing the proofs of the simply cool congruence results.

Proof of Lemma RHB: Let L be simply RHB cool, let r = \frac{H}{s⟶^{a}t} be a rule

in L, and let ν be a closed substitution such that ν(x) ⟶^{c}⟹ ν(y) for each positive premise x ⟶^{c} y in H and ¬∃r (ν(x) −̸→^{c} r) for each negative premise x −̸→^{c} in H. I need to show that ν(s) ⟶^{a}⟹ ν(t). By assumption, there is a closed substitution μ such that

• ν(x) ⟶^{c} μ(y) ⟹ ν(y) for each premise x ⟶^{c} y in H, and

• ν(x) = μ(x) for all variables x that do not occur as right-hand sides of premises in H.

Thus ν(s) = μ(s) ⟶^{a} μ(t) by application of r, and μ(t) ⟹ ν(t) by Lemma 2.

Lemma 5. Let L be simply WB cool, let r = \frac{H}{s⟶^{a}t} be an L-ruloid, and let ν be a

closed substitution. If for each premise x⟶^{c}y in H one has ν(x)⟹⟶^{c}⟹ν(y),

then ν(s) ⟹⟶^{a}⟹ ν(t).

Proof. The case that r is a rule in L is proven exactly as in Lemma WB, just writing a for (a), etc. The general case now follows by a straightforward structural induction on s. ⊓ ⊔

Proof of Lemma RWB: Let L be simply RWB cool, let r = \frac{H}{s⟶^{a}t} be a rule

in L, and let ν be a closed substitution such that ν(x) ⟹⟶^{c}⟹ ν(y) for each premise x ⟶^{c} y in H. I need to show that ν(s) ⟹⟶^{a}⟹ ν(t). Case 1: Suppose that there is a closed substitution μ such that

• ν(x) ⟶^{c} μ(y) ⟹ ν(y) for each premise x ⟶^{c} y in H, and

• ν(x) = μ(x) for all variables x that do not occur as right-hand sides of premises in H.

Then ν(s) = μ(s) ⟶^{a} μ(t) by application of r, and μ(t) ⟹ ν(t) by Lemma 2. Case 2: Suppose that there is a premise x^{0} ⟶^{c} y^{0} in H such that ν(x^{0}) ⟶^{τ} p ⟹⟶^{c}⟹ ν(y^{0}) for a closed term p. Let u, σ and r′ = \frac{K}{u⟶^{a}v} be the term, substitution and ruloid that exists for r by the third clause of Definition 12, and let x^{1} be the unique variable in u such that K has a premise x^{1} ⟶^{c} y^{0} (using that σ(y^{0}) = y^{0})). Hence σ(x^{1}) = x^{0}. Let μ be the closed substitution with μ(y^{0}) = p and μ(z) = ν(z) for all variables z ≠ y^{0}. Now μ(σ(x^{1})) = μ(x^{0}) =

ν(x^{0}) ⟶^{τ} μ(y^{0}). By Clause 3 of Definition 12, L has a rule \frac{σ(x^{1})⟶^{τ}y^{0}}{s⟶^{τ}σ(u[y^{0}/x^{1}])}; hence

ν(s) = μ(s) ⟶^{τ} μ(σ(u[y^{0}/x^{1}])). Let ρ be the closed substitution with ρ(x^{1}) = p and ρ(z) = ν(σ(z)) for all variables z ≠ x^{1}. Then μ(σ(u[y^{0}/x^{1}]) = ρ(u), the operators in u are tame, and ρ(x) ⟹⟶^{c}⟹ ρ(y) for each premise x ⟶^{c} y in K. Lemma 5 yields ρ(u) ⟹⟶^{a}⟹ ρ(v). By Clause 5 of Definition 8, x^{1} ∉ var(v), so ρ(v) = ν(σ(v)) = ν(t). Thus ν(s) = μ(s) ⟶^{τ} μ(σ(u[y^{0}/x^{1}])) =

ρ(u) ⟹⟶^{a}⟹ ρ(v) = ν(t). ⊓ ⊔

The Proof of Lemma RDB proceeds likewise, using a DB cool counterpart of Lemma 5. ⊓ ⊔

Theorem 6. On any RWB cool GSOS language, \underline{↔}_{rw} is a congruence. On any RDB cool GSOS language, \underline{↔}_{rd} is a congruence. On any RHB cool GSOS language, \underline{↔}_{rη} is a congruence. On any RBB cool GSOS language, \underline{↔}_{rb} is a congruence.

Proof. Let L be RBB cool. Regard L as a two-tiered GSOS languages by classifying all wild operators as principal ones. The GSOS language L^{∗} constructed in Definition 17 is simply RBB cool, by Obs. 1, so by Theorem 1RBB \underline{↔}_{rb} is a congruence on L^{∗}. Apply Cor. 2.

The other cases go likewise, except that in checking that L^{∗} is simply RWB or RDB cool, one has to check that Clause 3 of Definition 12 is satisfied. Let u and σ be a term and substitution that satisfy Clause 3 for a rule _{\frac{H}{f(x_{1},...,x_{n})⟶^{a}t}} with f

wild. I claim that u^{∗} and σ are appropriate for the rule _{\frac{H}{f(x_{1},...,x_{n})⟶^{a}t^{∗}}}, existing

in L^{∗}. Namely, by a straightforward structural induction on u, if \frac{K}{u⟶^{a}v} is an L-ruloid then \frac{K}{u^{∗}⟶^{a}v^{∗}} is an L^{∗}-ruloid. Moreover, σ(v) = t implies σ(v^{∗}) = t^{∗}. By

construction, for every premise x ⟶^{c} y in K, L^{∗} has a rule \frac{σ(x)⟶^{τ}y}{f(x_{1},...,x_{n})⟶^{τ}σ(u^{∗}[y/x])}.

E Comparison with Bloom’s formats

I reformulate the weakened version from Section 3.1 of Clause 4 of Definition 10 in such a way that it resembles the corresponding requirement in Bloom [4].

Definition 18. A term u ∈ T T(Σ) is univariate if no variable occurs more than once in u.

Trivially, any term can be written as σ(u) with u a univariate term and σ: V →V.

Proposition 6. In the definition of WB and HB cool GSOS languages, the weakening of Clause 4 of Definition 10 proposed in Section 3.1 is equivalent to

4′. if x ∈ vat(t) is receiving in t, u is a univariate term, y ∈ var(u), and σ : V → V is a substitution such that σ(u) = t^{⋆} with σ(y) = x, then there is

an L-ruloid \frac{y⟶^{τ}z}{u⟶^{τ}u[z/y]}.

Proof. 4 ⇒ 4′: Suppose L satisfies Clause 4, x ∈ var(t) is receiving in t, u is a univariate term, y ∈ var(u), and σ : V → V is a substitution such that σ(u) = t^{⋆} with σ(y) = x. With structural induction on subterms w of u that contain y, I show that there is an L-ruloid \frac{y⟶^{τ}z}{w⟶^{τ}w[z/y]}. For every such w there is a subterm v of t that contains x, with σ(w) = v^{⋆}.

Base case: w = y. By definition, there is a ruloid \frac{y⟶^{τ}z}{y⟶^{τ}z}.

Induction step: Let v = f(v_{1}, …, v_{ar(f)}) and w = f^{⋆}(w_{1}, …, w_{n}), and let i ∈ {1, …, n} be the unique argument of f^{⋆} with y ∈ var(w_{i}). Then σ(w_{i}) = v_{f(i)}^{⋆}, so x ∈ var(v_{f(i)}^{⋆}) ⊆ var(v_{f(i)}). Thus f(i) is a receiving argument of f, and L

must have a patience rule \frac{x_{i}⟶^{τ}z′}{f^{⋆}(x_{1},...,x_{n})⟶^{τ}f^{⋆}(x_{1},...,x_{n})[z′/x_{i}]}. By induction, there is

an L-ruloid \frac{y⟶^{τ}z}{w_{i}⟶^{τ}w_{i}[z/y]}, so by Definition 11 one obtains the required L-ruloid

\frac{y⟶^{τ}z}{f^{⋆}(w_{1},...,w_{n})⟶^{τ}f^{⋆}(w_{1},...,w_{n})[z/y]}.

4′ ⇒ 4: Suppose L satisfies Clause 4′, and argument f(i) of operator f is receiving. Then there must be a term t with a subterm v = f(v_{1}, …, v_{ar(f)}) such that v^{⋆} is a subterm of t^{⋆} and variable x ∈ var(v_{f(i)}^{⋆}) is receiving in t. Let u be a univariate term, and σ : V → V a substitution such that σ(u) = t^{⋆}. Let w = f^{⋆}(w_{1}, …, w_{n}) be the subterm of u with σ(w) = v^{⋆}. Then σ(w_{i}) = v_{f(i)}^{⋆}, and w_{i} (and hence u) must contain a variable y with σ(y) = x. By Clause 4′

there is an L-ruloid \frac{y⟶^{τ}z}{u⟶^{τ}u[z/y]}. By Clause 2 of Definition 10, patience rules are

the only rules for the operators of u with τ-premises. Hence, by Definition 11, this ruloid can only be obtained by stacking patience rules. As u is univariate, its subterm w_{i} contains the only occurrence of y in u, so one of the patience rules applied must be the one for argument i of f. ⊓ ⊔

F Equational axiomatisations

The proof of Theorem 4 is pretty straightforward and will be supplied in the full version of this paper. It involves a variant of Lemma 1.