Lean and Full Congruence Formats for Recursion
Rob van Glabbeek

TL;DR
This paper distinguishes between lean and full congruence formats for recursion in process semantics, proving bisimilarity's congruence properties in various structural operational semantics formats.
Contribution
It introduces a formal distinction between lean and full congruence formats and proves bisimilarity's congruence properties within these frameworks.
Findings
Bisimilarity is a lean congruence for recursion in ntyft/ntyxt formats.
Bisimilarity is a full congruence in tyft/tyxt formats.
The paper clarifies the conditions under which bisimilarity preserves process equivalence.
Abstract
In this paper I distinguish two (pre)congruence requirements for semantic equivalences and preorders on processes given as closed terms in a system description language with a recursion construct. A lean congruence preserves equivalence when replacing closed subexpressions of a process by equivalent alternatives. A full congruence moreover allows replacement within a recursive specification of subexpressions that may contain recursion variables bound outside of these subexpressions. I establish that bisimilarity is a lean (pre)congruence for recursion for all languages with a structural operational semantics in the ntyft/ntyxt format. Additionally, it is a full congruence for the tyft/tyxt format.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsAdvanced Software Engineering Methodologies · Logic, programming, and type systems · Service-Oriented Architecture and Web Services
Lean and Full Congruence Formats for Recursion
Data61, CSIRO, Sydney, Australia
School of Computer Science & Engineering, University of New South Wales, Sydney, Australia
Rob van Glabbeek
Abstract
In this paper I distinguish two (pre)congruence requirements for semantic equivalences and preorders on processes given as closed terms in a system description language with a recursion construct. A lean congruence preserves equivalence when replacing closed subexpressions of a process by equivalent alternatives. A full congruence moreover allows replacement within a recursive specification of subexpressions that may contain recursion variables bound outside of these subexpressions.
I establish that bisimilarity is a lean (pre)congruence for recursion for all languages with a structural operational semantics in the ntyft/ntyxt format. Additionally, it is a full congruence for the tyft/tyxt format.
I Introduction
Structural Operational Semantics [45, 47] is one of the main methods for defining the meaning of system description languages like CCS [45]. A system or process is represented by a closed term built from a collection of operators, process variables and usually a recursion construct, 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. The transitions between states are obtained from a set of proof rules called transition rules.
For purposes of representation and verification, several behavioural equivalence relations have been defined on processes, of which the most well-known is (strong) bisimilarity [45]. To allow compositional system verification, such equivalences need to be congruences for the operators under consideration, meaning that the equivalence class of an -ary operator applied to arguments is completely determined by the equivalence classes of these arguments.
Equally important is that the chosen equivalence relation is a congruence for recursion. Recursion allows the specification of a process as a canonical solution of an equation .111The particular solution supplied by structural operational semantics is the one whose transitions are determined by the transition rules. Here is an expression that may contain the variable . If is the collection of other variables occurring in , not bound by the recursive specification, then the canonical solution of is a -ary function that returns a process for each valuation of these variables as processes. I call a lean congruence for recursion if each such operator satisfies the above-mentioned congruence requirement.
Take for example to be in the language CCS of Milner [45]. Then . Let be bisimilarity, so that [45]. Now the lean congruence requirement for insists that the selected solutions of the recursive equations and , obtained from by substituting each of these bisimilar processes for , are again bisimilar.
The lean congruence requirement plays a key rôle in the study of expressiveness of system description languages [34]. There, correct translations of one language into another up to a semantic equivalence are defined; and expressiveness hierarchies—one for each choice of —are defined in terms of those translations. However, a correct translation can exist only when is a lean congruence for the source language, as well as for the source’s image within the target language.
If is an expression like , for simplicity assuming that neither contains variables other than , and regardless which process is substituted for the variable , then the full congruence property demands that the selected solutions of the equations and are again equivalent. As a CCS example, suppose that a process is given as the solution of the equation . Using the idempotence of under bisimilarity, one can now proceed to think of the same process, up to bisimilarity, as the solution of . This type of reasoning is a central component in system verification by equivalence checking [8, 18, 7, 38], as applied in successful verification toolsets such as CADP [25] and mCRL2 [38]. Yet it is valid only if bisimilarity is a full congruence for recursion.
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 (congruence 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. The first of these was proposed by Robert de Simone in [49, 50] and is now called the De Simone format. A generalisation featuring transition rules with negative premises is the GSOS format of Bloom, Istrail & Meyer [12], and a generalisation with lookahead is the tyft/tyxt format of Groote & Vaandrager [40]. The ntyft/ntyxt format of Groote [37] allows both negative premises and lookahead and generalises the GSOS as well as the tyft/tyxt format. All this work provides congruence formats for (strong) bisimilarity. Congruence formats for other strong semantic equivalences—treating the internal action like any other action—appear in [11, 22].222These congruence formats also apply to behavioural preorders, and then ensure that such a preorder is a precongruence. Formats for weak semantics—abstracting from internal activity—can be found, e.g., in [51, 10, 19, 52, 53, 33, 24, 21].
Extensions to probabilistic systems appear for instance in [9, 42, 41, 26, 44, 6, 17]. Rule formats ensuring properties of operators other than being a (pre)congruence appear in [46] (commutativity), [16] (associativity), [3] (zero and unit elements), [4] (distributivity) and [2] (idempotence). Overviews on work on congruence formats and other rule formats, with many more references, can be found in [5, 39].
Yet, to the best of my knowledge, no one has proposed a congruence format for recursion. This hiatus is addressed here. I establish that bisimilarity is a lean congruence for recursion for all languages with a structural operational semantics in the ntyft/ntyxt format.333Some of those languages have a 3-valued transition system semantics, where bisimilarity becomes an asymmetric preorder. Here I establish that it is a precongruence. I did not succeed in showing that it is even a full congruence for all ntyft/ntyxt languages; nor did I find a counterexample. Even for GSOS languages this remains an open question. However, I show that bisimilarity is a full congruence for recursion for all tyft/tyxt languages.
My proof strategy follows the traditional method of [12, 40, 13]. However, for this to work smoothly, I present a new formulation—better fitted to my application—of the well-founded semantics of transition system specifications with negative premises, and show its consistency with previous formulations.
I could not establish the full congruence result directly, without using the lean congruence result as an intermediate step, even when restricting the latter to the tyft/tyxt format. Thus, I see no way around a sequence of two proofs with a large overlap.
The method of modal decomposition [23] yields alternative congruence proofs for operators specified in the tyft/tyxt and GSOS formats [23]. Extending this method to deal with recursion might be a way to extend my full congruence result to transition rules with negative premises.
Providing (lean and full) congruence formats for recursion for equivalences and preorders other than bisimilarity, as well as for weak versions of bisimilarity [45, 36]—supporting abstraction from internal actions—remains an important open problem.
II Transition system specifications and their meaning
In this paper and are two sets of variables and actions. Many concepts that will appear are parameterised by the choice of and , but as in this paper this choice is fixed, a corresponding index is suppressed.
Definition 1** **(Signatures)
A function declaration is a pair of a function symbol and an arity .444This work generalises seamlessly to operators with infinitely many arguments. Such operators occur, for instance, in [14, Appendix A.2]. Hence one may take to be any ordinal. An operator, like the summation or choice of CCS [45], that actually takes any set of arguments, needs to be simulated by a family of operators with a sequence of arguments (but yielding the same value upon reshuffling of the arguments), one for each cardinality of this set. A function declaration is also called a constant declaration. A signature is a set of function declarations. The set of terms with recursion over a signature is defined inductively by:
- •
,
- •
if and then ,
- •
If , and , then \raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!X|S!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}}\in\mbox{\bbb T}(\Sigma).
A term is abbreviated as . A function as appears in the last clause is called a recursive specification. A recursive specification is often displayed as . An occurrence of a variable in a term is free if it does not occur in a subterm of of the form \stackrel{{\scriptstyle\mbox{\tiny/}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny\backslash}}}\!\!X|S\!\!\stackrel{{\scriptstyle\mbox{\tiny\backslash}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny/}}} with . Let denote the set of variables occurring free in a term , and let be the set of terms over with . is set of closed terms over .
Example 1
Let contain three unary functions , and , and one infix-written binary function . Let . Then is a recursive specification, so \raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!X|S!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}}\mathbin{\in}\mbox{\bbb T}(\Sigma). Since , the only variable that occurs free in this term is .
As illustrated here, I often choose upper case letters for bound variables (the ones occurring in a set ) and lower case ones for variables occurring free; this is a convention only.
A recursive specification is meant to denote a -tuple (in the example above a pair) of processes that—when filled in for the variables in —forms a solution to the equations in .555When contains free variables from a set , this solution is parameterised by the choice of a valuation of these variables as processes, thereby becoming a -ary function. The term \stackrel{{\scriptstyle\mbox{\tiny/}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny\backslash}}}\!\!X|S\!\!\stackrel{{\scriptstyle\mbox{\tiny\backslash}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny/}}} denotes the -component of such a tuple.
Definition 2** **(Substitution)
A -substitution is a partial function from to ; it is closed if it is a total function from to . If is a substitution and any syntactic object, then denotes the object obtained from by replacing, for in the domain of , every free occurrence of in by , while renaming bound variables if necessary to prevent name-clashes. In that case is called a substitution instance of . A substitution instance where is given by for is denoted as , and for a recursive specification \stackrel{{\scriptstyle\mbox{\tiny/}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny\backslash}}}\!\!t|S\!\!\stackrel{{\scriptstyle\mbox{\tiny\backslash}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny/}}} abbreviates t[\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!Y|S!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}}/Y]_{Y\in V_{S}}.
Example 2
Extend from Ex. 1 with a constant . Then \raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!X|S!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}}[b.c/z]=\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!X|{X{=}(a.X)|(b.Y),;Y{=}(d.Y)|(X|b.c)}!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}}, \raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!X|S!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}}[X/z]=\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!Z|{Z{=}(a.Z)|(b.Y),\quad Y{=}(d.Y)|(Z|X)}!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}} and \raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!X|S!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}}[b.c/Y]=\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!X|S!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}}.
Structural operational semantics [47] defines the meaning of system description languages whose syntax is given by a signature . It generates a transition system in which the states, or processes, are the closed terms over —representing the remaining system behaviour from that state—and transitions between processes are supplied with labels. The transitions between processes are obtained from a transition system specification, which consists of a set of transition rules.
Definition 3** **(Transition system specifications)
Let be a signature. A positive -literal is an expression t\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt\hskip 2.5pt}\hfil}}}}}t^{\prime} and a negative -literal an expression t{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\mathord{-}\mkern-6.0mu\cleaders\hbox{\mkern-2.0mu\mathord{-}\mkern-2.0mu}\hfill\mkern-6.0mu\mathord{\not}\mkern-2.0mu\mathord{\rightarrow}}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt\hskip 2.5pt}\hfil}}}}} with and . For the literals t\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt\hskip 2.5pt}\hfil}}}}}t^{\prime} and t{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\mathord{-}\mkern-6.0mu\cleaders\hbox{\mkern-2.0mu\mathord{-}\mkern-2.0mu}\hfill\mkern-6.0mu\mathord{\not}\mkern-2.0mu\mathord{\rightarrow}}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt\hskip 2.5pt}\hfil}}}}} are said to deny each other. A transition rule over is an expression of the form with a set of -literals (the premises or antecedents of the rule) and a positive -literal (the conclusion). The terms at the left- and right-hand side of are the source and target of the rule. A rule with is also written . A literal or transition rule is closed if it contains no free variables. A transition system specification (TSS) is a pair with a signature and a set of transition rules over ; it is positive if all antecedents of its rules are positive.
The concept of a (positive) TSS presented above was introduced in Groote & Vaandrager [40]; the negative premises t{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\mathord{-}\mkern-6.0mu\cleaders\hbox{\mkern-2.0mu\mathord{-}\mkern-2.0mu}\hfill\mkern-6.0mu\mathord{\not}\mkern-2.0mu\mathord{\rightarrow}}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt\hskip 2.5pt}\hfil}}}}} were added in Groote [37]. The notion generalises the GSOS rule systems of [12] and constitutes the first formalisation of Plotkin’s Structural Operational Semantics (SOS) [47] that is sufficiently general to cover many of its applications.
The following definition (from [28]) tells when a transition is provable from a TSS. It generalises the standard definition (see e.g. [40]) by (also) allowing the derivation of transition rules. The derivation of a transition t\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt\hskip 2.5pt}\hfil}}}}}t^{\prime} corresponds to the derivation of the transition rule with . The case corresponds to the derivation of t\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt\hskip 2.5pt}\hfil}}}}}t^{\prime} under the assumptions .
Definition 4** **(Proof)
Let be a TSS. A proof of a transition rule from is a well-founded, upwardly branching tree of which the nodes are labelled by -literals, such that:
- •
the root is labelled by , and
- •
if is the label of a node and is the set of labels of the nodes directly above , then
- –
either and ,
- –
or is a substitution instance of a rule from .
If a proof of from exists, then is provable from , notation .
A TSS is meant to specify an LTS in which the transitions are closed positive literals. A positive TSS specifies a transition relation in a straightforward way as the set of all provable transitions.666Readers interested only in the restriction of my results to TSSs without negative premises—giving rise to 2-valued transition relations—can safely skip the remainder of this section, and identify p\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}p^{\prime} with . In the proofs of Prop. 3 and Thm. 2 also p\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}_{\lambda}p^{\prime} and equal , for any ; so the induction on can be skipped, as well as the auxiliary Claims 3 and 1, and the proof proceeds directly by induction on . But as pointed out in Groote [37], it is not so easy to associate a transition relation to a TSS with negative premises. In [32] several solutions to this problem were reviewed and evaluated. Arguably, the best method to assign a meaning to all TSSs is the well-founded semantics of Van Gelder, Ross & Schlipf [27], which in general yields a 3-valued transition relation . I present such a relation as a pair \stackrel{{\scriptstyle\mbox{\tiny/}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny\backslash}}}\!\!CT,PT\!\!\stackrel{{\scriptstyle\mbox{\tiny\backslash}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny/}}} of 2-valued transition relations—the sets of certain and possible transitions—with . When insisting on 2-valued transition relations, the best method is the same, declaring meaningful only those TSSs whose well-founded semantics is 2-valued, meaning that .
Below I give a new presentation of the well-founded semantics, strongly inspired by previous accounts in [48, 13, 32]. As Def. 4 does not allow the derivation of negative literals, to arrive at an approximation of the set of transitions that are in the transition relation intended by a TSS , one could start from an approximation of the closed negative literals that ought to be generated, and define as the set of closed positive literals provable from under the hypotheses . Intuitively,
if is an under- (resp. over-)approximation of the closed negative literals that “really” hold, then will be an under- (resp. over-)approximation of the intended (2-valued) transition relation, and 2. 2.
if is an under- (resp. over-)approximation of the intended transition relation, then the set of all closed negative literals that do not deny any literal in is an over- (resp. under-)approximation of the closed negative literals that agree with the intended transition relation.
Definition 5** **(Over- and underappr. of transition relations)
Let be a TSS. For ordinals the sets and of closed positive literals, and , of closed negative literals are defined inductively by:
is the set of literals
that do not deny any
with
iff .
is the set of literals
that do not deny any
iff .
Intuitively, is an underapproximation of the set of transitions that should be in the transition relation specified by , and an overapproximation. Likewise, is an underapproximation of the set of closed negative literals that should hold, and an overapproximation. The approximations get better with increasing . To understand this inductively, note that is the set of all closed negative literals, and thus surely an overapproximation. The induction step is given by considerations 1 and 2 above.
Lemma 1
and for .
Proof.
Let . The definition of immediately yields . From this, applying Def. 5, one obtains , and , respectively. The remaining claims follow by induction on .
As is the universal relation, certainly , so .
Let be a limit ordinal. Then . For any one has by induction. Namely if , and if . Hence for any , and hence . With Def. 5 this implies and hence .
Now let . By induction . With Def. 5 this implies , and hence . With Def. 5 this implies and hence . ∎∎
Since the closed literals over form a proper set, there must be an ordinal such that for all , and hence also , and .
Definition 6
Such an ordinal is called closure ordinal. Let , , and .
Remark 1
, taking the intersection over all ordinals. Likewise, , and .
Remark 2
is the set of literals that do not deny any literal in , and likewise for and . Moreover, and .
Definition 7** **(Well-founded semantics)
The 3-valued transition relation \stackrel{{\scriptstyle\mbox{\tiny/}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny\backslash}}}\!\!CT^{+}\!,PT^{+}\!\!\stackrel{{\scriptstyle\mbox{\tiny\backslash}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny/}}} constitutes the well-founded semantics of .
Below I show that the above account of the well-founded semantics is consistent with the one in [32], and thereby with the ones in [13, 48, 27].
Definition 8** **(Well-supported proof [32])
Let be a TSS. A well-supported proof from of a closed literal is a well-founded tree with the nodes labelled by closed literals, such that the root is labelled by , and if is the label of a node and is the set of labels of the children of this node, then:
- •
either is positive and is a substitution instance of a rule in ;
- •
or is negative and for each set of closed negative literals with for a closed positive literal denying , a literal in denies one in .
denotes that a well-supported proof from of exists.
Proposition 1
Let be a TSS. Then P\vdash_{\it ws}p\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt\hskip 2.5pt}\hfil}}}}}q iff (p\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt\hskip 2.5pt}\hfil}}}}}q)\in CT^{+}, and P\vdash_{\it ws}p{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\mathord{-}\mkern-6.0mu\cleaders\hbox{\mkern-2.0mu\mathord{-}\mkern-2.0mu}\hfill\mkern-6.0mu\mathord{\not}\mkern-2.0mu\mathord{\rightarrow}}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt\hskip 2.5pt}\hfil}}}}} iff (p{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\mathord{-}\mkern-6.0mu\cleaders\hbox{\mkern-2.0mu\mathord{-}\mkern-2.0mu}\hfill\mkern-6.0mu\mathord{\not}\mkern-2.0mu\mathord{\rightarrow}}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt\hskip 2.5pt}\hfil}}}}})\in CT^{-}.
Proof.
: Let be a well-supported proof of a closed literal . By consistently applying the same closed substitution to all literals occurring in , one can assume, without loss of generality, that all literals in are closed. With structural induction on I show that .
Suppose is positive and is the closed substitution instance of the rule of applied at the root of . Then for each the literal is ws-provable from by means of a strict subproof of . By induction . As is for some ordinal , it is closed under deduction. Hence .
Suppose is negative. Let be closed positive literal denying . By Def. 8, each set of closed negative literals with contains a literal denying a literal that is ws-provable from by means of a strict subproof of . By induction . Hence . Consequently . Hence .
: Suppose . With induction on I show that . First suppose . Let be a set of closed negative literals with for a closed positive literal denying . Assume that . Then would be in , contradicting the definition of . So contains a literal that is not in , i.e., denies a literal in for some . By induction, . It follows that .
Now suppose . Then . By the case above for each . Hence . ∎∎
The above result, together with Theorem 1 in [32], and the observation in [32] that literals t\mathrel{{\mathrel{\hbox{\mathop{\hbox to30.41106pt{\mathord{-}\mkern-6.0mu\cleaders\hbox{\mkern-2.0mu\mathord{-}\mkern-2.0mu}\hfill\mkern-6.0mu\mathord{\not}\mkern-2.0mu\mathord{\rightarrow}}}\limits^{\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt\hskip 2.5pt}}}}}}{a}t^{\prime} can be eliminated from consideration (as done here), implies that the well-founded semantics given above agrees with the one from [32].
In [32] it was shown that is consistent, in the sense that no TSS admits well-supported proofs of two literals that deny each other. This also follows directly from the material above. A TSS is called complete [32] if for each and , either P\vdash_{\it ws}p{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\mathord{-}\mkern-6.0mu\cleaders\hbox{\mkern-2.0mu\mathord{-}\mkern-2.0mu}\hfill\mkern-6.0mu\mathord{\not}\mkern-2.0mu\mathord{\rightarrow}}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt\hskip 2.5pt}\hfil}}}}} or P\vdash_{\it ws}p\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt\hskip 2.5pt}\hfil}}}}}q for some . This implies that is exactly the set of closed negative literals that do not deny any literal in . Hence and thus . So the 3-valued transition system associated to a complete TSS is 2-valued.
Below I write for , P\vdash p\mbox{,,,\not!!!\stackrel{{\scriptstyle a~{}}}{{\longrightarrow}}}_{\lambda} for (p\mbox{,,,\not!!!\stackrel{{\scriptstyle a~{}}}{{\longrightarrow}}})\mathbin{\in}CT^{-}_{\lambda}, P\vdash p\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}_{\lambda}q for and P\vdash p\mbox{,,,,\not!!!!\stackrel{{\scriptstyle a~{}}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{}}}}_{\lambda} for (p\mbox{,,,\not!!!\stackrel{{\scriptstyle a~{}}}{{\longrightarrow}}})\in PT^{-}_{\lambda}. Moreover, , resp. p\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}q, will abbreviate , resp. p\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}_{\kappa}q, where is the closure ordinal of Def. 6.
In my forthcoming lean congruence proof I will apply structural induction on “the proof of a transition or p\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}_{\lambda}q from ”. There I will mean the proofs of and , respectively, as this is what constitutes the evidence for the statement P\vdash p\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt\hskip 2.5pt}\hfil}}}}}_{\lambda}q, resp. P\vdash p\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}_{\lambda}q.
III The bisimulation preorder
The goal of this paper is to show that bisimilarity is a congruence for recursion for all languages with a structural operational semantics in the ntyft/ntyxt format. Traditionally [45], bisimilarity is defined on 2-valued transition systems only, whereas the structural operational semantics of a language specified by a TSS can be 3-valued. Rather than limit my results to languages specified by complete TSSs, I use an extension of the notion of bisimilarity to 3-valued transition systems. Such an extension, called modal refinement, is provided in [43]. There, 3-valued transition systems are called modal transition systems.
Definition 9** **(Bisimilarity)
Let be a TSS. A bisimulation is a binary relation on the states of such that, for and ,
- •
if and , then there is a with and ,
- •
if and P\vdash q\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}q^{\prime}, then there is a with P\vdash p\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}p^{\prime} and .
A process is a modal refinement of , notation , if there exists a bisimulation with . I call the bisimulation preorder, or bisimilarity. The kernel of , given by , is bisimulation equivalence.
Clearly, modal refinement is reflexive and transitive, and hence a preorder. The underlying idea is that a process with a 3-valued transition relation \stackrel{{\scriptstyle\mbox{\tiny/}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny\backslash}}}\!\!CT,PT\!\!\stackrel{{\scriptstyle\mbox{\tiny\backslash}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny/}}} is a specification of a process with a 2-valued transition relation, in which the presence or absence of certain transitions is left open. contains the transitions that are required by the specification, and the ones that are allowed. If , then may be closer to the eventual implementation, in the sense that some of the undetermined transitions have been resolved to present or absent. The requirements of Def. 9 now say that any transition that is required by should be (matched by a transition) required by , whereas any transition allowed by , should certainly be (matched by a transition) allowed by .
In case and are 2-valued (i.e. implementations) the modal refinement relation is just the traditional notion of bisimilarity [45] (and thus symmetric).
While achieving a higher degree of generality of my lean congruence theorem by interpreting incomplete TSSs as modal transition systems, I do not propose incomplete TSSs as a tool for the specification of modal transition systems.
IV Congruence properties
In the presence of recursion, two sensible notions of precongruence come to mind. Let be a preorder on the set of closed terms over . For closed substitutions write iff for each .
Definition 10** **(Lean precongruence)
A preorder is a lean precongruence iff for any term and any closed substitutions and with .
Definition 11** **(Full precongruence)
A preorder is a full precongruence iff it satisfies
[TABLE]
[TABLE]
for all functions , closed terms , and recursive specifications with .
A lean (resp. full) precongruence that is symmetric (i.e. an equivalence relation) is called a lean (resp. full) congruence. Clearly, each full (pre)congruence is also a lean (pre)congruence, and each lean (pre)congruence satisfies (1) above. Both implications are strict, as the following examples illustrate.
Example 3
Consider the TSS given by the rules
[TABLE]
where ranges over , and the recursion rule from Def. 13 below. An infinite trace of a process is a sequence such that there are processes with . Let iff for each infinite trace of there is an infinite trace of that has a suffix in common with . This is a preorder indeed. It is not hard to check that is a precongruence for both action prefixing and parallel composition , in the sense that (1) holds. However, it fails to be a lean congruence, because a.\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!X|X{=}c.X!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}}\equiv b.\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!X|X{=}c.X!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}}, yet when filled in for in \stackrel{{\scriptstyle\mbox{\tiny/}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny\backslash}}}\!\!Z|Z{=}Y\|Z\!\!\stackrel{{\scriptstyle\mbox{\tiny\backslash}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny/}}} (which can be seen as , an infinite parallel composition of copies of ) the two are no longer equivalent.
I did not find a pair of a TSS and a preorder known from the literature showing the same. This suggests that most common preorders that are (pre)congruences for a selection of common operators are also lean (pre)congruences for recursion.
Example 4
Consider the TSS with a constant and action prefixing, and only the rules for recursion from Def. 13 and for , with the internal action. Consider any semantic equivalence satisfying , and such that divergence \stackrel{{\scriptstyle\mbox{\tiny/}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny\backslash}}}\!\!X|X{=}\tau.X\!\!\stackrel{{\scriptstyle\mbox{\tiny\backslash}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny/}}} differs from deadlock or inaction . Such semantic equivalences are abound in the literature and include the failures semantics of CSP [15, 29] and branching bisimilarity with explicit divergence [35, 29]. They are all lean congruences (at least when no other operators are present). Yet, since 0\sim\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!X|X{=}X!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}}\not\sim\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!X|X{=}\tau.X!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}}, they fail to be full congruences.
A lean congruence is required for treating processes as equivalence classes of closed terms rather than as the closed terms themselves, in such a way that each term with free variables drawn from the set models a -ary operator on such processes. As explained in the introduction, this notion of congruence facilitates a formal comparison of the expressive power of system description languages [34]. However, it does not allow equivalence preserving modifications of recursive specifications themselves, as contemplated in the introduction. That requires a full congruence.
V The pure ntyxt/ntyft format with recursion
Definition 12** **(ntytt, ntyft, ntyxt, nxytt rules)
An ntytt rule is a rule in which the right-hand sides of positive premises are variables that are all distinct, and that do not occur in the source. An ntytt rule is an ntyxt rule if its source is a variable, an ntyft rule if its source contains exactly one function symbol and no multiple occurrences of variables, and an nxytt rule if the left-hand sides of its premises are variables.
The idea behind the names of the rules is that the ‘n’ in front refers to the presence of negative premises, and the following four letters refer to the allowed forms of left- and right-hand sides of premises and of the conclusion, respectively. For example, ntyft means a rule with negative premises (n), where left-hand sides of premises are general terms (t), right-hand sides of positive premises are variables (y), the source contains exactly one function symbol (f), and the target is a general term (t).
Definition 13
A TSS is in the ntyft/ntyxt format with recursion if for every recursive specification and it has a rule
[TABLE]
and all of its other rules are ntyft or ntyxt rules.
Definition 14** **(Well-founded and pure rules; distance)
The dependency graph of an ntytt rule with \{t_{i}\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt\hskip 2.5pt}\hfil}}}}}y_{i}\mid i\mathbin{\in}I\} as set of positive premises is the directed graph with edges . A ntytt rule is well-founded if each backward chain of edges in its dependency graph is finite. A variable in a rule is free if it occurs neither in the source nor in the right-hand sides of the premises of this rule. A rule is pure if it is well-founded and does not contain free variables. A TSS is well-founded, resp. pure, if all of its rules are.
Let be a pure ntytt rule. The distance of a variable to the source of is the ordinal number given by
[TABLE]
Bol & Groote show that bisimilarity is a congruence for any language specified by a complete TSS in the well-founded ntyft/ntyxt format (without recursion) [13]. This generalises a result by Groote [37], showing the same for stratified TSSs in the well-founded ntyft/ntyxt format; here stratified is a more restrictive criterion than completeness, guaranteeing that a TSS has a well-defined meaning as a 2-valued transition relation. That result, in turn, generalises the congruence formats of Groote & Vaandrager [40] for the well-founded tyft/tyxt format (obtained by leaving out negative premises) and for the GSOS format of Bloom, Istrail & Meyer [12]. Both of these generalise the De Simone format [49, 50].
Fokkink and van Glabbeek show that for any complete TSS in tyft/tyxt (resp. ntyft/ntyxt) format there exists a pure (and thus well-founded) complete TSS in tyft (resp. ntyft) format that generates the same transition relation [20]. From this it follows that the restriction to well-founded TSSs can be dropped from the congruence formats of [13] and [40]. The result of [20] generalises straightforwardly to incomplete TSSs, and to formats with recursion.
Theorem 1
For each TSS in the tyft/tyxt (resp. ntyft/ntyxt) format with recursion there exists a pure TSS in the tyft (resp. ntyft) format with recursion, generating the same (3-valued) transition relation.
Proof.
[20, Theorem 5.4] shows that for each TSS in ntyft/ntyxt format there exists a TSS in pure ntyft format, such that for any closed transition rule with only negative premises, one has . This result generalises seamlessly to TSS in the ntyft/ntyxt format with recursion; I leave it to the reader to check that recursion causes no new complications in the proof.
[20] obtains the quoted result for complete TSSs from Thm. 5.4 by means of an application of [20, Prop. 5.2], which says that if and are TSSs such that for any closed transition rule with only negative premises, then is complete iff is, and in that case they determine the same transition relation. This Prop. 5.2 was taken verbatim from [31, Prop. 29].
In [32], the journal version of [31], Prop. 29 was extended to also conclude, under the same assumption, that and determine the same 3-valued transition relation according to the well-founded semantics. Using this version of Prop. 29 instead of Prop. 5.2 yields the required result. ∎∎
The next two propositions (not used in the rest of the paper) tell that any language specified by TSS in the ntyft/ntyxt format with recursion satisfies two sanity requirements from [30]. The first is that, up to , the meaning of a closed term \stackrel{{\scriptstyle\mbox{\tiny/}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny\backslash}}}\!\!X|S\!\!\stackrel{{\scriptstyle\mbox{\tiny\backslash}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny/}}} is the -component of a solution of :
Proposition 2
Let be a TSS in the ntyft/ntyxt format with recursion and a recursive specification with . Then \raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!X|S!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}}\equiv_{B}\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!S_{X}|S!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}}.
Proof.
P\vdash\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!X|S!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}}\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt\hskip 2.5pt}\hfil}}}}}q for some and iff P\vdash\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!S_{X}|S!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}}\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt\hskip 2.5pt}\hfil}}}}}q. ∎∎
For the second, invariance under -conversion, write t\mathrel{\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\alpha}}{{=}}}}u if the terms differ only in the names of their bound variables (the variables from within a subexpression of the form \stackrel{{\scriptstyle\mbox{\tiny/}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny\backslash}}}\!\!X|S\!\!\stackrel{{\scriptstyle\mbox{\tiny\backslash}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny/}}}).
Proposition 3
Let be a TSS in the ntyft/ntyxt format with recursion. Then p\mathrel{\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\alpha}}{{=}}}}q\Rightarrow p\equiv_{B}q for all .
Proof.
By Thm. 1 I may assume, without loss of generality, that is in the pure ntyft format with recursion. I show that \mathrel{\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\alpha}}{{=}}}} is a bisimulation on —since \mathrel{\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\alpha}}{{=}}}} is also symmetric, this yields the required result.
Thus I need to show that, for and ,
- •
if p\mathrel{\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\alpha}}{{=}}}}q and , then there is a with and p^{\prime}\mathrel{\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\alpha}}{{=}}}}q^{\prime},
- •
if p\mathrel{\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\alpha}}{{=}}}}q and P\vdash q\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}q^{\prime}, then there is a with P\vdash p\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}p^{\prime} and p^{\prime}\mathrel{\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\alpha}}{{=}}}}q^{\prime}.
To this end it suffices to establish, for all ordinals , that
if p\mathrel{\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\alpha}}{{=}}}}q and , then there is a with and p^{\prime}\mathrel{\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\alpha}}{{=}}}}q^{\prime}, 2. 2.
if p\mathrel{\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\alpha}}{{=}}}}q and P\vdash q\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}q^{\prime}, then there is a with P\vdash p\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}_{\lambda}p^{\prime} and p^{\prime}\mathrel{\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\alpha}}{{=}}}}q^{\prime}.
The desired result is then obtained by taking to be the closure ordinal of Def. 6. This I will do by induction on , at the same time establishing that
if p\mathrel{\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\alpha}}{{=}}}}q and P\vdash p\mbox{,,,\not!!!\stackrel{{\scriptstyle a~{}}}{{\longrightarrow}}}_{\lambda}, then P\vdash q\mbox{,,,\not!!!\stackrel{{\scriptstyle a~{}}}{{\longrightarrow}}}, 2. 1.
if p\mathrel{\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\alpha}}{{=}}}}q and P\vdash q\mbox{,,,,\not!!!!\stackrel{{\scriptstyle a~{}}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{}}}}, then P\vdash p\mbox{,,,,\not!!!!\stackrel{{\scriptstyle a~{}}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{}}}}_{\lambda}.
So assume Claims 1–4 have been established for all .
Suppose p\mathrel{\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\alpha}}{{=}}}}q and P\vdash q\mbox{,,,,\not!!!!\stackrel{{\scriptstyle a~{}}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{}}}}. By Remark 2 there is no with . So by induction, using Claim 4 above, there is no with for some . By Def. 5 P\vdash p\mbox{,,,,\not!!!!\stackrel{{\scriptstyle a~{}}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{}}}}_{\lambda}. This yields Claim 1.
Now suppose p\mathrel{\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\alpha}}{{=}}}}q and P\vdash q\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}q^{\prime}. I need to find a with P\vdash q\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}_{\lambda}q^{\prime} and p^{\prime}\mathrel{\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\alpha}}{{=}}}}q^{\prime}. This I will do by structural induction on the proof of p\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}p^{\prime} from , making a case distinction based on the shape of .
- •
Let . Then where p_{i}\mathrel{\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\alpha}}{{=}}}}q_{i} for . Let be a proof of P\vdash q\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}q^{\prime} from . By Defs. 4 and 13, there must be a pure ntyft rule in and a closed substitution with for and , such that for each (t_{y}\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt\hskip 2.5pt}\hfil}}}}}y)\in H the transition P\vdash t_{y}[\nu]\mathbin{\stackrel{{\scriptstyle c}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}\nu(y) is provable from by means of a strict subproof of , and P\vdash u[\nu]\mbox{,,,,\not!!!!\stackrel{{\scriptstyle c~{}}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{}}}} for each (u{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\mathord{-}\mkern-6.0mu\cleaders\hbox{\mkern-2.0mu\mathord{-}\mkern-2.0mu}\hfill\mkern-6.0mu\mathord{\not}\mkern-2.0mu\mathord{\rightarrow}}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt\hskip 2.5pt}\hfil}}}}})\in H. Next, I define a substitution such that
- (i)
for , 2. (ii)
\sigma(y)\mathrel{\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\alpha}}{{=}}}}\nu(y) for each , 3. (iii)
P\vdash t_{y}[\sigma]\mathbin{\stackrel{{\scriptstyle c}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}_{\lambda}\sigma(y) for each (t_{y}\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt\hskip 2.5pt}\hfil}}}}}y)\in H.
The definition of and the inference of (i)–(iii) above proceed with induction on the distance of from the source of ,
Base case: Let for , so that Property (i) is satisfied. Regarding Property (ii), \sigma(x_{i})\mathrel{\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\alpha}}{{=}}}}\nu(x_{i}) for .
Induction step: When defining for some with (t_{y}\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt\hskip 2.5pt}\hfil}}}}}y)\in H, by induction has been defined already for all , so I may assume that \sigma(x)\mathrel{\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\alpha}}{{=}}}}\nu(x) for all and hence t_{y}[\sigma]\mathrel{\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\alpha}}{{=}}}}t_{y}[\nu].
By induction on , there is a with P\vdash t_{y}[\sigma]\mathbin{\stackrel{{\scriptstyle c}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}_{\lambda}p_{y} and p_{y}\mathrel{\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\alpha}}{{=}}}}\nu(y). Define . Properties (ii) and (iii) now hold for .
Take . So p^{\prime}\mathbin{=}t[\sigma]\mathrel{\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\alpha}}{{=}}}}t[\nu]\mathbin{=}q^{\prime} by Property (ii) of . For each premise (u{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\mathord{-}\mkern-6.0mu\cleaders\hbox{\mkern-2.0mu\mathord{-}\mkern-2.0mu}\hfill\mkern-6.0mu\mathord{\not}\mkern-2.0mu\mathord{\rightarrow}}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt\hskip 2.5pt}\hfil}}}}})\in H one has u[\sigma]\mathrel{\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\alpha}}{{=}}}}u[\nu] by Property (ii) of . So P\vdash u[\sigma]\mbox{,,,,\not!!!!\stackrel{{\scriptstyle c~{}}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{}}}}_{\lambda} by Claim 1. By Defs. 4 and 13, together with Property (iii) of , this implies P\vdash p=f(p_{1},\ldots,p_{n})\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}_{\lambda}t[\sigma]=p^{\prime}.
- •
Let p=\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!X|S!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}}. Then q=\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!\alpha(X)|S^{\prime}[\alpha]!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}} for some recursive specification with S_{Y}\mathrel{\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\alpha}}{{=}}}}S^{\prime}_{Y} for all , and an injective substitution such that the range of contains no variables occurring free in \stackrel{{\scriptstyle\mbox{\tiny/}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny\backslash}}}\!\!S^{\prime}_{Y}|S\!\!\stackrel{{\scriptstyle\mbox{\tiny\backslash}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny/}}} for some . Now \raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!S_{X}|S!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}}\mathrel{\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\alpha}}{{=}}}}\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!S_{X}|S^{\prime}!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}}\mathrel{\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\alpha}}{{=}}}}\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!S^{\prime}{\alpha(X)}|S^{\prime}[\alpha]!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}}. Let be a proof of P\vdash q\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}q^{\prime} from . By Defs. 4 and 13 P\vdash\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!S^{\prime}{\alpha(X)}|S^{\prime}[\alpha]!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}}\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}q^{\prime} is provable from by means of a strict subproof of . So by induction there is a such that P\vdash\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!S_{X}|S!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}}\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}_{\lambda}p^{\prime} and p^{\prime}\mathrel{\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\alpha}}{{=}}}}q^{\prime}. By Defs. 4 and 13, P\vdash p=\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!X|S!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}}\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}_{\lambda}p^{\prime}.
This establishes Claim 2.
Next, suppose that p\mathrel{\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\alpha}}{{=}}}}q and P\vdash p\mbox{,,,\not!!!\stackrel{{\scriptstyle a~{}}}{{\longrightarrow}}}_{\lambda}. By Def. 5 there is no with P\vdash p\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}_{\lambda}p^{\prime}. Using Claim 2, there is no with P\vdash q\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}q^{\prime}. By Remark 2, P\vdash q\mbox{,,,\not!!!\stackrel{{\scriptstyle a~{}}}{{\longrightarrow}}}. This yields Claim 3.
Claim 4 follows by structural induction on the proof of p\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt\hskip 2.5pt}\hfil}}}}}_{\lambda}p^{\prime} from , pretty much in the same way as Claim 2 above. ∎∎
Prop. 3 could be classified as “self-evident”. One reason to spell out the proof above is to obtain a template for bisimilarity proofs in the setting of the well-founded semantics. I will use this template in the forthcoming lean congruence proof.
VI A lean congruence result
The following congruence proof is strongly inspired by the one in [13].
Theorem 2
Bisimilarity is a lean precongruence for any language specified by a TSS in the ntyft/ntyxt format with recursion.
- Proof:
By Thm. 1 I may assume, without loss of generality, that is a TSS in the pure ntyft format with recursion. Let be the smallest lean precongruence containing bisimilarity, i.e., is the smallest relation on processes satisfying
- –
if then ,
- –
if and for all , then ,
- –
and if with , and satisfy for all , then \raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!Z|S!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}}[\rho]\mathrel{\cal R}\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!Z|S!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}}[\nu].
**A trivial structural induction on , using the last two clauses, shows that if satisfy for all , then . (*)
As \raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!_|S!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}}[\rho]:V_{S}\rightarrow{\rm T}(\Sigma) and \raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!_|S!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}}[\nu]:V_{S}\rightarrow{\rm T}(\Sigma), this implies that in the last clause one even has \raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!t|S!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}}[\rho]\mathrel{\cal R}\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!t|S!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}}[\nu] for all terms . ($)**
It suffices to show that is a bisimulation, because this implies , so that equals , and (*) says that is a lean precongruence. Thus I need to show that, for and ,
- –
if and , then there is a with and p^{\prime}\mathrel{\color[rgb]{0,0,1}\cal R}q^{\prime},
- –
if and P\vdash q\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}q^{\prime}, then there is a with P\vdash p\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}p^{\prime} and p^{\prime}\mathrel{\color[rgb]{1,0,0}\mathrel{\cal R}}q^{\prime}.
To this end it suffices to establish, for all ordinals , that
if and , then there is a with and p^{\prime}\mathrel{\color[rgb]{0,0,1}\cal R}q^{\prime},** ** 2. 2.
if and P\vdash q\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}q^{\prime}, then there is a with P\vdash p\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}_{\lambda}p^{\prime} and p^{\prime}\mathrel{\color[rgb]{1,0,0}\mathrel{\cal R}}q^{\prime}.
The desired result is then obtained by taking to be the closure ordinal of Def. 6. This I will do by induction on , at the same time establishing that
if and P\vdash p\mbox{,,,\not!!!\stackrel{{\scriptstyle a~{}}}{{\longrightarrow}}}_{\lambda}, then P\vdash q\mbox{,,,\not!!!\stackrel{{\scriptstyle a~{}}}{{\longrightarrow}}}, 2. 1.
if and P\vdash q\mbox{,,,,\not!!!!\stackrel{{\scriptstyle a~{}}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{}}}}, then P\vdash p\mbox{,,,,\not!!!!\stackrel{{\scriptstyle a~{}}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{}}}}_{\lambda}.
So assume Claims 1–4 have been established for all .
Suppose and P\vdash q\mbox{,,,,\not!!!!\stackrel{{\scriptstyle a~{}}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{}}}}. By Remark 2 there is no with . So by induction, using Claim 4 above, there is no with for some . By Def. 5 P\vdash p\mbox{,,,,\not!!!!\stackrel{{\scriptstyle a~{}}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{}}}}_{\lambda}. This yields Claim 1.
Now suppose and P\vdash q\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}q^{\prime}. I need to find a with P\vdash p\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}_{\lambda}p^{\prime} and . This I will do by structural induction on the proof of q\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}q^{\prime} from . I make a case distinction based on the derivation of .
- –
Let . Using that is a bisimulation, there must be a process such that P\vdash p\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}p^{\prime} and , hence . Since P\vdash p\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}p^{\prime}, certainly P\vdash p\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}_{\lambda}p^{\prime}, by Remark 1.
- –
Let and where for . Let be a proof of q\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}q^{\prime} from . By Defs. 4 and 13, there must be a pure ntyft rule in and a closed substitution with for and , such that for each (t_{y}\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt\hskip 2.5pt}\hfil}}}}}y)\in H the transition t_{y}[\nu]\mathbin{\stackrel{{\scriptstyle c}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}\nu(y) is provable from by means of a strict subproof of , and P\vdash u[\nu]\mbox{,,,,\not!!!!\stackrel{{\scriptstyle c~{}}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{}}}} for each (u{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\mathord{-}\mkern-6.0mu\cleaders\hbox{\mkern-2.0mu\mathord{-}\mkern-2.0mu}\hfill\mkern-6.0mu\mathord{\not}\mkern-2.0mu\mathord{\rightarrow}}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt\hskip 2.5pt}\hfil}}}}})\in H. Next, I define a substitution such that
- (i)
** for ,** 2. (ii)
** for each ,** 3. (iii)
P\vdash t_{y}[\sigma]\mathbin{\stackrel{{\scriptstyle c}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}_{\lambda}\sigma(y)** for each (t_{y}\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt\hskip 2.5pt}\hfil}}}}}y)\in H.**
The definition of and the inference of (i)–(iii) above proceed with induction on the distance of from the source of ,
Base case:** Let for , so that Property (i) is satisfied. Regarding Property (ii), for .**
Induction step:** When defining for some with (t_{y}\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt\hskip 2.5pt}\hfil}}}}}y)\in H, by induction has been defined already for all , so I may assume that for all and hence by (*******).
By induction on , there is a with P\vdash t_{y}[\sigma]\mathbin{\stackrel{{\scriptstyle c}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}_{\lambda}p_{y} and . Define . Properties (ii) and (iii) now hold for .
Take . So by (***) and Property (ii) of . For each premise (u{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\mathord{-}\mkern-6.0mu\cleaders\hbox{\mkern-2.0mu\mathord{-}\mkern-2.0mu}\hfill\mkern-6.0mu\mathord{\not}\mkern-2.0mu\mathord{\rightarrow}}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt\hskip 2.5pt}\hfil}}}}})\in H one has by (*******) and Property (ii) of . So P\vdash u[\sigma]\mbox{,,,,\not!!!!\stackrel{{\scriptstyle c~{}}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{}}}}_{\lambda} by Claim 1. By Defs. 4 and 13, together with Property (iii) of , this implies
P\vdash p=f(p_{1},\ldots,p_{n})\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}_{\lambda}t[\sigma]=p^{\prime}****.
- –
Let p\mathbin{=}\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!Z|S!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}}[\rho]\mathbin{=}\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!Z|S[\rho]!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}} and q\mathbin{=}\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!Z|S!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}}[\sigma]\mathbin{=}\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!Z|S[\sigma]!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}} where with , , and for all one has . Let be a proof of q\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}q^{\prime} from . By Defs. 4 and 13 \raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!S_{Z}|S[\sigma]!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}}\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}q^{\prime} is provable from by means of a strict subproof of . By (\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny/}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny\backslash}}}\!\!S_{Z}|S[\rho]\!\!\stackrel{{\scriptstyle\mbox{\tiny\backslash}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny/}}}}\mathrel{\cal R}\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny/}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny\backslash}}}\!\!S_{Z}|S[\sigma]\!\!\stackrel{{\scriptstyle\mbox{\tiny\backslash}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny/}}}}p^{\prime}P\vdash\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny/}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny\backslash}}}\!\!S_{Z}|S[\rho]\!\!\stackrel{{\scriptstyle\mbox{\tiny\backslash}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny/}}}}\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{}}}}{\lambda}p^{\prime}p^{\prime}\mathrel{\cal R}q^{\prime}P\vdash p=\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny/}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny\backslash}}}\!\!Z|S[\sigma]\!\!\stackrel{{\scriptstyle\mbox{\tiny\backslash}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny/}}}}\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{}}}}{\lambda}p^{\prime}$.**
Next, suppose that and P\vdash p\mbox{,,,\not!!!\stackrel{{\scriptstyle a~{}}}{{\longrightarrow}}}_{\lambda}. By Def. 5 there is no with P\vdash p\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}_{\lambda}p^{\prime}. Using Claim 2, there is no with P\vdash q\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}q^{\prime}. By Remark 2, P\vdash q\mbox{,,,\not!!!\stackrel{{\scriptstyle a~{}}}{{\longrightarrow}}}. This yields Claim 3.
Finally, suppose and . I need to find a with and p^{\prime}\mathrel{\color[rgb]{0,0,1}\cal R}q^{\prime}. This I will do by structural induction on the proof of p\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt\hskip 2.5pt}\hfil}}}}}_{\lambda}p^{\prime} from . I make a case distinction based on the derivation of .
- –
Let . Since , certainly , by Remark 1. Using that is a bisimulation, there must be a process such that P\vdash q\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt\hskip 2.5pt}\hfil}}}}}q^{\prime} and , hence p^{\prime}\mathrel{\color[rgb]{0,0,1}\cal R}q^{\prime}.
- –
Let and where for . Let be a proof of p\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt\hskip 2.5pt}\hfil}}}}}_{\lambda}p^{\prime} from . By Defs. 4, 5 and 13, there must be a pure ntyft rule in and a closed substitution with for and , such that for each (t_{y}\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt\hskip 2.5pt}\hfil}}}}}y)\in H the transition t_{y}[\sigma]\mathbin{\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt\hskip 2.5pt}\hfil}}}}}_{\lambda}}\sigma(y) is provable from by means of a strict subproof of , and P\vdash u[\sigma]{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\mathord{-}\mkern-6.0mu\cleaders\hbox{\mkern-2.0mu\mathord{-}\mkern-2.0mu}\hfill\mkern-6.0mu\mathord{\not}\mkern-2.0mu\mathord{\rightarrow}}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt\hskip 2.5pt}\hfil}}}}}_{\lambda} for each (u{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\mathord{-}\mkern-6.0mu\cleaders\hbox{\mkern-2.0mu\mathord{-}\mkern-2.0mu}\hfill\mkern-6.0mu\mathord{\not}\mkern-2.0mu\mathord{\rightarrow}}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt\hskip 2.5pt}\hfil}}}}})\in H. Next, I define a substitution such that
- (i)
** for ,** 2. (ii)
\sigma(y)\mathrel{\color[rgb]{0,0,1}\cal R}\nu(y)** for each ,** 3. (iii)
P\vdash t_{y}[\nu]\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt\hskip 2.5pt}\hfil}}}}}\nu(y)** for each (t_{y}\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt\hskip 2.5pt}\hfil}}}}}y)\in H.**
The definition of and the inference of (i)–(iii) above proceed with induction on the distance of from the source of ,
Base case:** Let for , so that Property (i) is satisfied. Regarding Property (ii), for .**
Induction step:** When defining for some with (t_{y}\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt\hskip 2.5pt}\hfil}}}}}y)\in H, by induction has been defined already for all , so I may assume that \sigma(x)\mathrel{\color[rgb]{0,0,1}\cal R}\nu(x) for all *and hence t_{y}[\sigma]\mathrel{\color[rgb]{0,0,1}\cal R}t_{y}[\nu] by ().
By induction on , there is a with P\vdash t_{y}[\nu]\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt\hskip 2.5pt}\hfil}}}}}q_{y} and \sigma(y)\mathrel{\color[rgb]{0,0,1}\cal R}q_{y}. Define . Properties (ii) and (iii) now hold for .
Take . So p^{\prime}\mathbin{=}t[\sigma]\mathrel{\color[rgb]{0,0,1}\cal R}t[\nu]\mathbin{=}q^{\prime} by () and Property (ii) of . For each premise (u{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\mathord{-}\mkern-6.0mu\cleaders\hbox{\mkern-2.0mu\mathord{-}\mkern-2.0mu}\hfill\mkern-6.0mu\mathord{\not}\mkern-2.0mu\mathord{\rightarrow}}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt\hskip 2.5pt}\hfil}}}}})\in H one has u[\sigma]\mathrel{\color[rgb]{0,0,1}\cal R}u[\nu] by (****) and Property (ii) of . So P\vdash u[\nu]{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\mathord{-}\mkern-6.0mu\cleaders\hbox{\mkern-2.0mu\mathord{-}\mkern-2.0mu}\hfill\mkern-6.0mu\mathord{\not}\mkern-2.0mu\mathord{\rightarrow}}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt\hskip 2.5pt}\hfil}}}}} by Claim 3. Since is closed under deduction, together with Property (iii) of this implies P\vdash q=f(q_{1},\ldots,q_{n})\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt\hskip 2.5pt}\hfil}}}}}t[\nu]=q^{\prime}.
- –
Let p\mathbin{=}\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!Z|S!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}}[\rho]\mathbin{=}\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!Z|S[\rho]!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}} and q\mathbin{=}\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!Z|S!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}}[\nu]\mathbin{=}\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!Z|S[\nu]!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}} where with , , and for all one has . Let be a proof of p\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt\hskip 2.5pt}\hfil}}}}}_{\lambda}p^{\prime} from . By Defs. 4, 5 and 13 \raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!S_{Z}|S[\rho]!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}}\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt\hskip 2.5pt}\hfil}}}}}_{\lambda}p^{\prime} is provable from by means of a strict subproof of . By (\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny/}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny\backslash}}}\!\!S_{Z}|S[\rho]\!\!\stackrel{{\scriptstyle\mbox{\tiny\backslash}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny/}}}}\mathrel{\cal R}\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny/}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny\backslash}}}\!\!S_{Z}|S[\nu]\!\!\stackrel{{\scriptstyle\mbox{\tiny\backslash}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny/}}}}q^{\prime}P\vdash\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny/}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny\backslash}}}\!\!S_{Z}|S[\nu]\!\!\stackrel{{\scriptstyle\mbox{\tiny\backslash}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny/}}}}\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt\scriptstyle a\hskip 2.5pt}\hfil}}}}}q^{\prime}p^{\prime}\mathrel{\color[rgb]{0,0,1}\cal R}q^{\prime}P\vdash q=\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny/}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny\backslash}}}\!\!Z|S[\nu]\!\!\stackrel{{\scriptstyle\mbox{\tiny\backslash}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny/}}}}\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt\scriptstyle a\hskip 2.5pt}\hfil}}}}}q^{\prime}$.**
This yields Claim 4.
The above result implies that any ntyft/ntyxt language with recursion satisfies congruence requirement (1) up to , but is not strong enough to yield (2).
VII A full congruence result
In this section I deal with positive TSSs only. Here the relations \mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}_{\lambda} and for ordinals and all coincide, and . The following auxiliary concept was used in [45] to show that CCS satisfies Condition (2) of Def. 11.
Definition 15
A symmetric relation is a bisimulation up to if and imply that there is a with and , for all . Here .
Proposition 4** **([45])
If for some bisimulation up to , then .
Proof.
Using the reflexivity of it suffices to show that is a bisimulation. Using symmetry and transitivity of this is straightforward. ∎∎
Theorem 3
Bisimilarity is a full congruence for any language specified by a TSS in the tyft/tyxt format with recursion.
- Proof:
By Thm. 1 I may assume, without loss of generality, that is a TSS in the pure tyft format with recursion. Let be recursive specifications with for all and . I need to show that \raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!X|S!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}}\equiv_{B}\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!X|S^{\prime}!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}} for all . Let be the smallest relation on processes satisfying
- –
\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!X|S!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}}\mathrel{\cal R}\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!X|S^{\prime}!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}}** and \raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!X|S^{\prime}!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}}\mathrel{\cal R}\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!X|S!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}} for all ,**
- –
if and for all , then ,
- –
and if with , and satisfy for all , then \raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!Z|{S^{\prime\prime}}!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}}[\rho]\mathrel{\cal R}\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!Z|{S^{\prime\prime}}!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}}[\nu].
**A trivial structural induction on , using the last two clauses, shows that if satisfy for all , then . (*)
So in the first clause one even has \raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!t|S!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}}\mathrel{\cal R}\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!t|S^{\prime}!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}} for all , (#)
and in the last clause \raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!t|{S^{\prime\prime}}!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}}[\rho]\mathrel{\cal R}\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!t|{S^{\prime\prime}}!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}}[\nu] for all . ($)**
It suffices to show that is a bisimulation up to , because with Prop. 4 this implies . By construction is symmetric. So it suffices to show that,
if and P\vdash p\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt\hskip 2.5pt}\hfil}}}}}p^{\prime}, then there is a with P\vdash q\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt\hskip 2.5pt}\hfil}}}}}q^{\prime} and ,
for all and , This I will do by structural induction on the proof of p\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt\hskip 2.5pt}\hfil}}}}}p^{\prime} from . I make a case distinction based on the derivation of .
- –
Let p=\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!X|S!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}} and q=\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!X|S^{\prime}!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}} with . Let be a proof of p\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt\hskip 2.5pt}\hfil}}}}}p^{\prime} from . By Definitions 4 and 13 \raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!S_{X}|S!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}}\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt\hskip 2.5pt}\hfil}}}}}p^{\prime} is provable from by means of a strict subproof of . By (#) above one has \raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!S_{X}|S!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}}\mathrel{\cal R}\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!S_{X}|S^{\prime}!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}}. So by induction there is an such that P\vdash\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!S_{X}|S^{\prime}!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}}\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt\hskip 2.5pt}\hfil}}}}}r^{\prime} and . Since \stackrel{{\scriptstyle\mbox{\tiny/}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny\backslash}}}\!\!\_\!\_|S^{\prime}\!\!\stackrel{{\scriptstyle\mbox{\tiny\backslash}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny/}}} is a substitution of the form , one has \raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!S_{X}|S^{\prime}!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}}\equiv_{B}\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!S^{\prime}_{X}|S^{\prime}!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}}. Hence there is a such that P\vdash\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!S^{\prime}_{X}|S^{\prime}!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}}\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt\hskip 2.5pt}\hfil}}}}}q^{\prime} and . So . By Definitions 4 and 13 P\vdash q\mathbin{=}\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!X|S^{\prime}!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}}\mathbin{\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt\hskip 2.5pt}\hfil}}}}}}q^{\prime}\!.
- –
The case p=\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!X|S^{\prime}!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}} and q=\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!X|S!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}} goes likewise, swapping the rôles of and , and using the substitution \stackrel{{\scriptstyle\mbox{\tiny/}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny\backslash}}}\!\!\_\!\_|S\!\!\stackrel{{\scriptstyle\mbox{\tiny\backslash}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny/}}}. 777This proof shows that in the full congruence property (2) one only needs to assume for two specific substitutions : namely \sigma(Y):=\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!Y|S^{\prime}!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}}, resp. \stackrel{{\scriptstyle\mbox{\tiny/}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny\backslash}}}\!\!Y|S\!\!\stackrel{{\scriptstyle\mbox{\tiny\backslash}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny/}}}.
- –
The remaining two cases proceed in the same way as in the proof of Claim 4 for Thm. 2, but suppressing and with substituted for the blue occurrences of . In the last case there are no further changes, so I will not repeat it here. The remaining case needs a few elaborations—these involve the blue coloured segments in the proof of Claim 4:
- –
Let and where for . Let be a proof of p\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt\hskip 2.5pt}\hfil}}}}}p^{\prime} from . By Defs. 4 and 13, there must be a pure tyft rule in and a closed substitution with for and , such that for each (t_{y}\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt\hskip 2.5pt}\hfil}}}}}y)\in H the transition t_{y}[\sigma]\mathbin{\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt\hskip 2.5pt}\hfil}}}}}}\sigma(y) is provable from by means of a strict subproof of . Next, I define a substitution such that
- (i)
** for ,** 2. (ii)
** for each ,** 3. (iii)
P\vdash t_{y}[\nu]\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt\hskip 2.5pt}\hfil}}}}}\nu(y)** for each (t_{y}\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt\hskip 2.5pt}\hfil}}}}}y)\in H.**
The definition of and the inference of (i)–(iii) above proceed with induction on the distance of from the source of ,
Base case:** Let for , so that Property (i) is satisfied. Regarding Property (ii), for .**
Induction step:** When defining for some with (t_{y}\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt\hskip 2.5pt}\hfil}}}}}y)\in H, by induction has been defined already for all , so I may assume that for all , i.e., there exists a substitution with for all . Now by (*******) and by Thm. 2.
By induction on , there is an with P\vdash t_{y}[\rho]\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt\hskip 2.5pt}\hfil}}}}}r_{y} and . By the definition of bisimilarity, there is a with P\vdash t_{y}[\nu]\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt\hskip 2.5pt}\hfil}}}}}q_{y} and . Define . Properties (ii) and (iii) now hold for .
Take . So by (*******), Property (ii) of , and Thm. 2. By Defs. 4 and 13, together with Property (iii) of , this implies**
P\vdash q=f(q_{1},\ldots,q_{n})\mathrel{\mathrel{\hbox{\mathop{\hbox to15.00002pt{\rightarrowfill}}\limits^{\hbox to15.00002pt{\hfil\hbox{\vrule height=6.45831pt,depth=3.44444pt,width=0.0pt\hskip 2.5pt\hskip 2.5pt}\hfil}}}}}t[\nu]=q^{\prime}****.
It remains an open question whether the above result can be generalised to the ntyft/ntyxt format with recursion. A direct combination of the proofs of Thms. 2 and 3 does not work, however. An attempt in this direction would substitute either or for the red \color[rgb]{1,0,0}\mathrel{\cal R} in Claim 2 in the proof of Thm. 2. Both attempts fail on the case p=\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!X|S!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}} and q=\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!X|S^{\prime}!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}} in the proof of Thm. 3.
The first attempt would from P\vdash\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!S^{\prime}{X}|S^{\prime}!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}}\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}q^{\prime} infer P\vdash\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!S{X}|S^{\prime}!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}}\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}r^{\prime} by bisimilarity, and then infer P\vdash\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!S_{X}|S!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}}\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}_{\lambda}p^{\prime} by induction. However, one may not use induction, as the transition \raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!S_{X}|S^{\prime}!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}}\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}r^{\prime} may be derived later than \raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!X|S^{\prime}!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}}\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}q^{\prime}. In fact, if a variant of this approach would work, skipping \raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!X|S^{\prime}!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}}\mathrel{\cal R}\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!X|S!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}} from the definition of , one could prove a false version of (2) that assumes the antecedent only for the single substitution \stackrel{{\scriptstyle\mbox{\tiny/}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny\backslash}}}\!\!\_\!\_|S^{\prime}\!\!\stackrel{{\scriptstyle\mbox{\tiny\backslash}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny/}}} (cf. Footnote 7); it is trivial to find a counterexample in the GSOS format with unguarded recursion.
The second attempt would from P\vdash\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!S^{\prime}{X}|S^{\prime}!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}}\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}q^{\prime} infer P\vdash\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!S^{\prime}{X}|S!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}}\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}_{\lambda}r^{\prime} by induction, and then P\vdash\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!S_{X}|S!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}}\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}_{\lambda}p^{\prime} by bisimilarity. The latter step is invalid, as \raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!S_{X}|S^{\prime}!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}}\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}_{\lambda}r^{\prime} is only an overapproximation of P\vdash\raisebox{0.0pt}[0.0pt][0.0pt]{\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}!!S_{X}|S^{\prime}!!\stackrel{{\scriptstyle\mbox{\tiny}}}{{\raisebox{-1.29167pt}[1.29167pt]{\tiny}}}}\mathbin{\stackrel{{\scriptstyle a}}{{\raisebox{0.0pt}[3.0pt][0.0pt]{\scriptstyle--\rightarrow}}}}r^{\prime}.
The reference list from the paper itself. Each links out to its DOI / PubMed record.
- 1[1]
- 2[2] L. Aceto, A. Birgisson, A. Ingólfsdóttir, M.R. Mousavi & M.A. Reniers (2012): Rule formats for determinism and idempotence . Science of Computer Programming 77(7-8), pp. 889–907, doi: http://dx.doi.org/10.1016/j.scico.2010.04.002 .
- 3[3] L. Aceto, M. Cimini, A. Ingólfsdóttir, M.R. Mousavi & M.A. Reniers (2011): SOS rule formats for zero and unit elements . Theoretical Computer Science 412(28), pp. 3045–3071, doi: http://dx.doi.org/10.1016/j.tcs.2011.01.024 .
- 4[4] L. Aceto, M. Cimini, A. Ingólfsdóttir, M.R. Mousavi & M.A. Reniers (2012): Rule formats for distributivity . Theoretical Computer Science 458, pp. 1–28, doi: http://dx.doi.org/10.1016/j.tcs.2012.07.036 .
- 5[5] L. Aceto, W.J. Fokkink & C. Verhoef (2000): Structural Operational Semantics . In J.A. Bergstra, A. Ponse & S.A. Smolka, editors: Handbook of Process Algebra , chapter 3, Elsevier, pp. 197–292.
- 6[6] G. Bacci & M. Miculan (2015): Structural operational semantics for continuous state stochastic transition systems . Journal of Computer and System Sciences 81(5), pp. 834–858, doi: http://dx.doi.org/10.1016/j.jcss.2014.12.003 .
- 7[7] J. C. M. Baeten, T. Basten & M. A. Reniers (2010): Process Algebra: Equational Theories of Communicating Processes . Cambridge University Press.
- 8[8] J.C.M. Baeten, editor (1990): Applications of Process Algebra . Cambridge Tracts in Theoretical Computer Science 17, Cambridge University Press.
