Ntyft/ntyxt Rules Reduce to Ntree Rules

Wan Fokkink^{∗}

Department of Computer Science CWI Amsterdam, The Netherlands

                            wan@cwi.nl

Rob van Glabbeek^{†}

Computer Science Department Stanford University Stanford, CA 94305, USA

                                                          rvg@cs.stanford.edu

Groote and Vaandrager introduced the tyft/tyxt format for Transition System Specifications (TSSs), and established that for each TSS in this format that is well-founded, the bisimulation equivalence it induces is a congruence. In this paper, we construct for each TSS in tyft/tyxt format an equivalent TSS that consists of tree rules only. As a corollary we can give an affirmative answer to an open question, namely whether the well-foundedness condition in the congruence theorem for tyft/tyxt can be dropped. These results extend to tyft/tyxt with negative premises and predicates.

1 Introduction

A current method to provide process algebras and specification languages with an operational semantics is based on the use of transition systems, advocated by Plotkin [15]. Given a set of states, the transitions between these states are obtained inductively from a Transition System Specification (TSS), which consists of transition rules. Such a rule, together with a number of transitions, may imply the validity of another transition.

We will consider a specific type of transition systems, in which states are the closed terms generated by a single-sorted signature, and transitions are supplied with labels. A great deal of the operational semantics of formal languages in Plotkin style that have been defined over the years, are within the scope of this format.

To distinguish such labelled transition systems, many different equivalences have been defined, the finest of which is the strong bisimulation equivalence of Park [14]. In general, this equivalence is not a congruence, i.e. the equivalence class of a term f(p_{1}, ..., p_{m}) modulo strong bisimulation is not always determined by the equivalence classes of the terms p_{i}. However, congruence is an essential property, for instance, to fit the equivalence into an axiomatic framework.

Several formats have been developed which ensure that the bisimulation equivalence induced by a TSS in such a format is always a congruence. A first proposal was made by De Simone [16], which was generalized by Bloom, Istrail and Meyer [3] to the GSOS format. Next, Groote and Vaandrager [12] introduced the tyft/tyxt format, and proved a congruence theorem for TSSs in this format that satisfy a well-foundedness criterion.

∗Current affiliation: Department of Philosophy, Utrecht University, Utrecht, The Netherlands.

†This work was supported by ONR under grant number N00014-92-J-1974.

Up to now, it has been an open question whether or not well-foundedness is an essential ingredient of this congruence theorem. The requirement popped up in the proof, but no counter-example was found to show that the theorem breaks down if well-foundedness were omitted from it. In this paper, we prove that the congruence theorem does hold for general TSSs in tyft/tyxt format, i.e. that the requirement of well-foundedness can be omitted.

In fact, we will establish a stronger result, namely that for each TSS in tyft/tyxt format, there is an equivalent TSS which consists of ‘tree rules’ only. A tree rule is a well-founded rule of the form

\frac{\{z_{i} ⟶^{a_{i}} y_{i} | i ∈ I\}}{f(x_{1}, ..., x_{m}) ⟶^{a} t}

where the y_{i} and the x_{j} are distinct variables and are the only variables that occur in the rule, the z_{i} are variables, f is a function symbol, and t is any term. Using terminology from [12], we can say that a tree rule is a pure xyft rule. Since tree rules are well-founded, the reduction of tyft/tyxt rules to tree rules immediately implies that the congruence theorem concerning the tyft/tyxt format can do without well-foundedness.

A major advantage of the main theorem is that it facilitates reasoning about the tyft/tyxt format. Because often it is much easier to prove a theorem for TSSs in tree format than for TSSs in tyft/tyxt format. For example, this is the case with the congruence theorem itself. Another striking example consists of Theorems 8.6.6 and 8.9.1 in [12]. With our result at hand, the complicated proof of the second theorem can be skipped, because now the second theorem follows from the first one.

Furthermore, the removal of well-foundedness from the congruence theorem for tyft/tyxt increases the convenience of applying this theorem, since the user no longer has to recall and check the complicated well-foundedness criterion.

The main result of this paper was obtained independently by the authors in [9] and [5]. Our present proof improves the ones envisioned in [9] and given in [5]. It makes heavy use of a standard result from unification theory, which says that for each set of equations that is unifiable, there exists an idempotent most general unifier. In unification theory, this result is proved for finite sets of equations, and for substitutions that have a finite domain. However, we will need the result in a setting which does not satisfy these finiteness constraints. A proof of the unification result in the infinite case can be found in [6]. Here we prove the special case of this result that is needed for our main theorem.

Groote [11] added negative premises to tyft/tyxt, resulting in the ntyft/ntyxt format (that also generalizes the GSOS format of [3]), and proved that the congruence theorem extends to certain well-founded TSSs in ntyft/ntyxt format. We will show that the reduction of tyft/tyxt rules to tree rules can be lifted to the positive part of rules in ntyft/ntyxt format, but a simple example learns that this reduction cannot be applied to the negative premises. Again, we will find that the congruence theorem concerning the ntyft/ntyxt format can do without well-foundedness.

Verhoef [17] defined the panth format, which adds predicates to ntyft/ntyxt, and proved that the congruence theorem holds for well-founded TSSs in panth format. We will show that our results extend to the panth format too.

Acknowledgments. Catuscia Palamidessi and Fer-Jan de Vries noted the link with unification. Frits Vaandrager and Chris Verhoef provided useful comments.

2 Preliminaries

This section contains the basic definitions.

2.1 The signature

In the sequel we assume the existence of an infinite set of variables V.

Definition 2.1 A (single-sorted) signature Σ consists of a set of function symbols, disjoint with V, together with their arities.

The collection 𝕋(Σ) of (open) terms over Σ is defined as the least set satisfying:

– each variable from V is in 𝕋(Σ),

– if f ∈ Σ has arity n, and t_{1}, ..., t_{n} ∈ 𝕋(Σ), then f(t_{1}, ..., t_{n}) ∈ 𝕋(Σ). A term is called closed if it does not contain any variables.

In the sequel we assume a fixed signature Σ.

A substitution is a mapping σ : V → 𝕋(Σ). Each substitution is extended to a mapping from terms to terms in the standard way. As usual, σρ denotes the composition of the substitutions σ and ρ, in which ρ is applied first.

2.2 Transition system specifications

In the sequel we assume the existence of a set of labels A.

Definition 2.2 For each label a, the expression ⟶^{a} denotes a binary relation on terms. A pair t ⟶^{a} t′ is called a transition. A transition is closed if it involves closed terms only.

Definition 2.3 A (transition) rule r is an expression of the form H/c, with H a collection of transitions, called the premises (or the hypotheses), of r, and c a transition, called the conclusion of r. In the sequel, concl(r) will denote the conclusion of the rule r.

A Transition System Specification (TSS) is a collection of transition rules.

A TSS is small if for each of its rules, the cardinality of its collection of premises does not exceed the cardinality of the set V of variables.

The notion of substitution extends to transitions and rules as expected.

Definition 2.4 A proof structure is a tuple (B, r, ϕ), where – B is a collection of transition rules which do not have any variables in common,

– r ∈ B,

– ϕ is an injective mapping from B\{r} to the collection of premises of rules in B, such

that each chain b_{0}, b_{1}, b_{2}, ... in B with ϕ(b_{i+1}) a premise of b_{i} is finite.

In the sequel, top(B, r, ϕ) will denote the collection of premises of rules in B that are outside the image of ϕ.

Write (B′, r′, ϕ′) < (B, r, ϕ) iff B′ ⊂ B, ϕ′ = ϕ^{\}(B′\{r′}), top(B′, r′, ϕ′) ⊆ top(B, r, ϕ) and there is a chain r = b_{0}, b_{1}, ..., b_{n} = r′ with n > 0 and ϕ(b_{i+1}) a premise of b_{i}.

Note that < is a partial well-order, i.e. any chain (B_{0}, r_{0}, ϕ_{0}) > (B_{1}, r_{1}, ϕ_{1}) > (B_{2}, r_{2}, ϕ_{2}) > ⋯ is finite. Hence we may apply induction w.r.t. <.

Definition 2.5 A substitution σ matches with a proof structure (B, r, ϕ) if σ(concl(b)) = σ(ϕ(b)) for each b ∈ B\{r}.

A rule H/c is provable from a small TSS R if c ∈ H or there exists a proof structure (B, r, ϕ) where each rule in B is in R modulo α-conversion (bijective renaming of variables), and a substitution σ that matches with (B, r, ϕ), such that σ(top(B, r, ϕ)) ⊆ H and σ(concl(r)) = c.

Example 2.6 (A fragment of CCS with replication operator). Let A be a set of names. The set Ā of co-names is given by Ā = {ā | a ∈ A}, and L = A ∪ Ā is the set of visible actions. The function ¯· is extended to L by declaring ¯ ā = a. Furthermore A = L ∪ {τ} is the set of actions. Note that τ̄ is undefined. The language CCS has a constant 0, a unary operator a for a ∈ A, binary operators + and |, and a few constructs that are omitted here. In addition we consider the unary replication operator !. The transition system specification CCS! is given by the transition rules below. These rules are actually schemata, where a ranges over A.

\begin{matrix}ax ⟶^{a} x & \frac{x ⟶^{a} x′}{x + y ⟶^{a} x′} & \frac{y ⟶^{a} y′}{x + y ⟶^{a} y′} \\ \frac{x ⟶^{a} x′}{x | y ⟶^{a} x′ | y} & \frac{x ⟶^{a} x′, y ⟶^{ā} y′}{x | y ⟶^{τ} x′ | y′} & \frac{y ⟶^{a} y′}{x | y ⟶^{a} x | y′} & \frac{!x | x ⟶^{a} x′}{!x ⟶^{a} x′} \end{matrix}

Here follows an example of a proof structure (B, r, ϕ), together with a matching substitution σ. The rule on the bottom is r, and ϕ is indicated by the arrows. T op(B, r, ϕ) = {w ⟶^{ā} w′}.

[figure: \frac{!z | z ⟶^{τ} z′}{!z ⟶^{τ} z′}; \frac{v ⟶^{a} v′ w ⟶^{ā} w′}{v | w ⟶^{τ} v′ | w′}; \frac{x ⟶^{ā} x′}{y + x ⟶^{ā} x′}; \frac{!u | u ⟶^{a} u′}{!u ⟶^{a} u′}; \frac{t ⟶^{a} t′}{s | t ⟶^{a} s | t′}; \frac{q ⟶^{a} q′}{q + r ⟶^{a} q′}; ap ⟶^{a} p]  \begin{aligned}σ(p) & = & 0 \\ σ(q) & = & a0 \\ σ(q′) & = & 0 \\ σ(r) & = & x \\ σ(s) & = & !(a0 + x) \\ σ(t) & = & a0 + x \\ σ(t′) & = & 0 \\ σ(u) & = & a0 + x \\ σ(u′) & = & !(a0 + x) | 0 \\ σ(v) & = & !(a0 + x) \\ σ(v′) & = & !(a0 + x) | 0 \\ σ(w) & = & a0 + x \\ σ(w′) & = & x′ \\ σ(x) & = & x \\ σ(x′) & = & x′ \\ σ(y) & = & a0 \\ σ(z) & = & a0 + x \\ σ(z′) & = & !(a0 + x) | 0 | x′ \end{aligned}

This structure and σ demonstrate that the rule \frac{x ⟶^{ā} x′}{!(a0 + x) ⟶^{τ}!(a0 + x) | 0 | x′} is provable from CCS!.

We say that a transition t ⟶^{a} t′ is provable from R, if the rule with no premises and conclusion t ⟶^{a} t′ is provable from R. The transition relation ⟶_{R} determined by a TSS R is the set of all closed transitions provable from R.

Definition 2.7 Two TSSs are transition equivalent if they determine the same transition relation.

Our notion of provability is chosen in such a way that we can easily obtain our main result. In order to show that it coincides with the notions of provability found elsewhere in the literature, we need the following definition.

Definition 2.8 The provable closure of a TSS R is the smallest set R^{⊢} of rules such that

• if c ∈ H then H/c ∈ R^{⊢}, and

• if K/c ∈ R and H/σ(d) ∈ R^{⊢} for d ∈ K and some substitution σ, then H/σ(c) ∈ R^{⊢}.

For notions of provability found elsewhere in the literature (e.g. [2, 4, 5, 9, 10, 11, 12, 17]) the following proposition is easily obtained. By establishing the same for our notion, it follows that it coincides with the others. The proposition only holds for small TSSs, but this restriction will turn out to be inessential for our main result. Moreover, every TSS can be made ‘small’ by adding sufficiently many variables.

Proposition 2.9 A rule H/c is provable from a small TSS R iff it belongs to R^{⊢}.

Proof. “Only if”: The case c ∈ H is trivial. The other case is established by induction on the partial well-order < between proof-structures. Let H/σ(c) be provable from R by means of a proof structure (B, K/c, ϕ) and a matching substitution σ. Assume that any formula provable by means of a smaller proof structure belongs to R^{⊢}. Then H/σ(d) ∈ R^{⊢} for any d ∈ K. It follows that H/σ(c) ∈ R^{⊢}.

“If”: By induction on the construction of R^{⊢}. The induction base, c ∈ H, is again trivial. Now suppose K/c ∈ R and H/ρ(d) is provable from R for d ∈ K and some substitution ρ. Let (B_{d}, r_{d}, ϕ_{d}) be proof structures with matching substitutions σ_{d} that establish H/ρ(d) for d ∈ K. Since there exist at least as many variables as there are premises in K, the variables in these proof structures can be renamed to become all different, and different from the ones in K/c, and a substitution σ can be constructed that matches with each of these proof structures so as to yield the corresponding rule, and equals ρ on the variables in K/c. Now (⋃_{d∈K} B_{d} ∪ {K/c}, K/c, ⋃_{d∈K} ϕ_{d} ∪ ϕ′), where ϕ′ is the function that sends r_{d} to d for d ∈ K, is a proof structure that matches with σ, yielding H/ρ(c). □

The proof of the following lemma is straightforward and left to the reader.

Lemma 2.10 If all the rules in a TSS S are provable from a TSS R, then all the rules that are provable from S are also provable from R.

2.3 Strong bisimulation

Definition 2.11 Assume a TSS R. Two closed terms p_{0}, q_{0} are R-bisimilar, notation p_{0} \underline{↔}_{R} q_{0}, if there exists a symmetric binary relation B on closed terms such that

– p_{0}Bq_{0},

– if pBq and p ⟶^{a}_{R} p′, then there is a closed term q′ such that q ⟶^{a}_{R} q′ and p′Bq′.

2.4 The tyft/tyxt format

In general, bisimulation equivalence it is not a congruence, i.e. it may be the case that p_{i} \underline{↔}_{R} q_{i} for i = 1, ..., n, but f(p_{1}, ..., p_{n}) and f(q_{1}, ..., q_{n}) are not R-bisimilar. Therefore, Groote and Vaandrager [12] have introduced the tyft/tyxt format. If a TSS is in this format, and if it satisfies a wellfoundedness criterion, then the bisimulation it induces is a congruence.

Definition 2.12 A transition rule is a tyft rule if it is of the form

\frac{\{t_{i} ⟶^{a_{i}} y_{i} | i ∈ I\}}{f(x_{1}, ..., x_{m}) ⟶^{a} t}

where the x_{k} and the y_{i} are distinct variables (and I is some, not necessarily finite, index set). Similarly, a tyxt rule is of the form

\frac{\{t_{i} ⟶^{a_{i}} y_{i} | i ∈ I\}}{x ⟶^{a} t}

where x and the y_{i} are distinct variables. A TSS is said to be in tyft/tyxt format if it consists of tyft and tyxt rules only.

The TSS CCS! from Example 2.6 is in tyft/tyxt format. All its rules are tyft rules. Note that any TSS in tyft/tyxt format is ‘small’ in the sense of Definition 2.2.

Definition 2.13 Assume a set {t_{i} ⟶^{a_{i}} t′_{i} | i ∈ I} of transitions. Its ‘dependency graph’ is a directed graph, with the collection of variables V as vertices, and with as edges the collection

{⟨x, y⟩ | x and y occur in t_{i} and t′_{i} respectively, for some i ∈ I}.

A set of transitions is called well-founded if any backward chain of edges in its dependency graph is finite. A transition rule is well-founded if its collection of premises is so, and a TSS is well-founded if all its rules are so.

Example 2.14 Examples of sets of transitions that are not well-founded are:

– {y ⟶^{a} y},

– {y_{1} ⟶^{a} y_{2}, y_{2} ⟶^{b} y_{1}},

– {y_{i+1} ⟶^{a} y_{i} | i = 0, 1, 2, ...}.

The following congruence theorem originates from [12].

Theorem 2.15 If a TSS R is well-founded and in tyft/tyxt format, then \underline{↔}_{R} is a congruence.

In Section 4 we will see that the requirement of well-foundedness in this theorem can be dropped.

3 Unification

A standard result from logic programming says that if a finite collection E of equations between terms is unifiable, then there exists a unifier ρ′ for E such that each unifier for E is also a unifier for ρ′. This result follows from the well-known Martelli-Montanari algorithm [13]. See [1] for the basic definitions and for an introduction to the field of logic programming and unification.

In Fokkink [6], this theorem is generalized to the case where E may be infinite. The first property in Lemma 3.2, which will be vital in the proof of the main theorem, is a corollary of this unification result. However, we present a full proof of the lemma, because we will need two extra properties of the unifier ρ′, which follow most easily from its construction. Also, the proof of this lemma is much simpler than the proof of the stronger unification result in [6].

Definition 3.1 A substitution σ is a unifier for a substitution ρ if σρ = σ. In this case, ρ is called unifiable.

Lemma 3.2 If a substitution ρ is unifiable, then there exists a unifier ρ′ for ρ with the following properties:

1. Each unifier for ρ is also a unifier for ρ′.

2. If ρ(x) = x, then ρ′(x) = x.

3. If ρ^{n}(x) is a variable for all n ≥ 0, then ρ′(x) is a variable.

Proof. Let W denote the collection of variables x for which ρ^{n}(x) is a variable for all n ≥ 0. First, we define the restriction ρ′_{0} of ρ′ to W.

Define a binary relation ∼ on W by x ∼ x′ if ρ^{m}(x) = ρ^{n}(x′) for certain m and n. Note that ∼ is an equivalence relation. Under ρ′_{0}, we contract the elements of each equivalence class C ⊆ W to one variable from this class as follows.

– If ρ(x_{0}) = x_{0} for some x_{0} ∈ C, then for all x ∈ C ρ^{n}(x) = x_{0} for some n. This implies ρ(x) ≠ x for x ∈ C\{x_{0}}, so x_{0} is determined uniquely. Put ρ′_{0}(x) = x_{0} for x ∈ C.

– If ρ(x) ≠ x for all x ∈ C, then just pick some x_{0} ∈ C and put ρ′_{0}(x) = x_{0} for x ∈ C.

Put ρ′_{0}(y) = y for y ∉ W.

We construct ρ′(y) as follows. By assumption, ρ allows a unifier σ. Since σρ = σ, it follows that σρ^{n} = σ for n ≥ 0. Clearly, the size of each ρ^{n}(y) (that is, the number of function symbols it contains) is smaller or equal than the size of σρ^{n}(y) = σ(y). Moreover, each term ρ^{n+1}(y) has at least the size of ρ^{n}(y). Since the sizes of the ρ^{n}(y) cannot grow beyond the size of σ(y), it follows that from a certain natural number N(y) onwards, the terms ρ^{n}(y) all have the same size. Hence, for n ≥ N(y), ρ^{n+1}(y) is obtained from ρ^{n}(y) by replacing variables by variables. This means that all variables in ρ^{N(y)}(y) are in W. Put

ρ′(y) = ρ′_{0}ρ^{N(y)}(y).

Note that N(x) = 0 if x ∈ W, so ρ′ equals ρ′_{0} on W. We check the required properties for ρ′.

• ρ′ is a unifier for ρ.

First, consider a variable x ∈ W. Since ρ(x) ∼ x, and ρ′_{0} contracts variables in the same equivalence class, we have ρ′_{0}ρ(x) = ρ′_{0}(x). Since ρ′ equals ρ′_{0} on W, this implies ρ′ρ(x) = ρ′(x).

Next, consider a variable y ∉ W. Then clearly N(y) = N(ρ(y)) + 1, so

ρ′ρ(y) = ρ′_{0}ρ^{N(ρ(y))}ρ(y) = ρ′_{0}ρ^{N(y)}(y) = ρ′(y).

• Each unifier σ for ρ is a unifier for ρ′.

First, consider a variable x ∈ W. Since ρ′_{0}(x) ∼ x, there are m and n such that ρ^{m}ρ′_{0}(x) = ρ^{n}(x). After applying σ to both sides we get σρ′_{0}(x) = σ(x). Since ρ′_{0}(y) = y for variables y ∉ W, it follows that σρ′_{0} = σ.

So for each variable y we have

σρ′(y) = σρ′_{0}ρ^{N(y)}(y) = σρ^{N(y)}(y) = σ(y).

• If ρ(x) = x, then ρ′(x) = x.

Clearly x ∈ W, so ρ′(x) = ρ′_{0}(x). Since ρ(x) = x, the construction of ρ′_{0} ensures that ρ′_{0}(x) = x.

• If ρ^{n}(x) is a variable for all n ≥ 0, then ρ′(x) is a variable.

By definition x ∈ W, so ρ′(x) = ρ′_{0}(x). From the construction of ρ′_{0} it follows that its image contains variables only. □

4 Tyft/Tyxt Reduces to Tree

This section contains the proof of the main theorem, which says that for each TSS in tyft/tyxt format there exists a transition equivalent TSS in the more restrictive tree format.

4.1 Tyft/tyxt reduces to tyft

The following lemma from [12] indicates that we can refrain from tyxt rules.

Lemma 4.1 Each TSS R in tyft/tyxt format is transition equivalent to a TSS in tyft format.

Proof. Replace each tyxt rule r in R by a collection of tyft rules {r_{f}|f ∈ Σ}, where each r_{f} is obtained by substituting f(x_{1}, ..., x_{n}) for x in r, with x_{1}, ..., x_{n} variables that do not yet occur in r. Let R′ denote the collection of tyft rules that is thus obtained. Clearly, for each proof from R of a certain closed transition, there is a proof from R′ of the same transition, and vice versa. Hence, R and R′ are transition equivalent. □

4.2 Tyft reduces to xyft

Definition 4.2 A transition rule is said to be a xytt rule if the terms at both sides of its premises are all single variables.

Definition 4.3 A transition rule is called xyft if it is both tyft and xytt.

In this section, we show that each TSS in tyft format is xytt equivalent to a TSS in xyft format, where xytt equivalence is a stronger equivalence notion than transition equivalence.

Definition 4.4 Two TSSs are xytt equivalent if exactly the same xytt rules are provable from both.

Theorem 4.5 Each TSS R in tyft format is xytt equivalent to a TSS in xyft format.

Proof. We shall prove R xytt equivalent to the TSS S of xyft rules that are provable from R. Since all rules in S are provable from R, Lemma 2.10 yields that the xytt rules provable from S are provable from R. We show that the converse is also true, i.e. that each xytt rule H/c provable from R is provable from S. We apply induction on the partial well-order < between proof structures, so suppose that (B, r, ϕ) derives H/c from R, and the case has been proved for xytt rules that are derivable from R by means of a proof structure smaller than (B, r, ϕ).

Since (B, r, ϕ) is a proof structure for H/c, there exists a substitution σ that matches with (B, r, ϕ) such that σ(top(B, r, ϕ)) ⊆ H and σ(concl(r)) = c. From (B, r, ϕ) we construct recursively a sub-structure (B′, r, ϕ′) which is a proof structure for a rule s ∈ S. In parallel, we construct a partial substitution ρ which is unified by σ in the sense that σ(ρ(x)) = σ(x) for those variables x for which ρ has been defined.

• r ∈ B′,

• if b ∈ B\{r}, and if ϕ(b) is a premise t ⟶^{a} y of a rule in B′ such that for some k ≥ 0:

1. ρ^{i}(t) is defined for i = 0, ..., k,

2. ρ^{i}(t) is a variable for i = 0, ..., k − 1,

3. ρ^{k}(t) is of the form f(t_{1}, ..., t_{n}),

then b ∈ B′.

Since σ matches with (B, r, ϕ), we have σ(concl(b)) = σ(t ⟶^{a} y). By assumption, σ is a unifier for the partially defined ρ, so σ(t) = σρ^{k}(t) = σ(f(t_{1}, ..., t_{n})). Hence, concl(b) is of the form f(x_{1}, ..., x_{n}) ⟶^{a} u, with σ(x_{j}) = σ(t_{j}) for j = 1, ..., n and σ(u) = σ(y). Define ρ(x_{j}) = t_{j} for j = 1, ..., n and ρ(y) = u. Note that σ is a unifier for the extended ρ.

In order to extend ρ to a full substitution, we define ρ(x) = x for all variables x for which ρ has not yet been defined. Finally, ϕ′ is the restriction of ϕ to B′\{r}.

Since σ is a unifier for ρ, Lemma 3.2 indicates the existence of a unifier ρ′ for ρ with the following properties.

1. σρ′ = σ.

2. If ρ(x) = x, then ρ′(x) = x.

3. If ρ^{k}(x) is a variable for all k ≥ 0, then ρ′(x) is a variable.

Consider the rule b in the construction of B′ and ρ. Recall that its conclusion is of the form

f(x_{1}, ..., x_{n}) ⟶^{a} u and ϕ′(b) = t ⟶^{a} y, where ρ^{k}(t) = f(t_{1}, ..., t_{n}) = ρ(f(x_{1}, ..., x_{n})) and ρ(y) = u.

Since ρ′ is a unifier for ρ, it follows that

ρ′(ϕ′(b)) = ρ′(t ⟶^{a} y) = ρ′(ρ^{k}(t) ⟶^{a} ρ(y)) = ρ′(ρ(f(x_{1}, ..., x_{n})) ⟶^{a} u) = ρ′(concl(b)).

So ρ′ matches with (B′, r, ϕ′). Hence the rule s = ρ′(top(B′, r, ϕ′)/concl(r)) is provable from R.

We show that s is xyft. From the construction of ρ it follows that its domain (i.e. the variables x for which ρ(x) ≠ x) consists of two kinds of variables:

1. variables that occur at the left-hand side of the conclusion of rules in B′\{r},

2. variables that occur at the right-hand side of premises in the range of ϕ′.

Hence, if g(x_{1}, ..., x_{m}) ⟶^{b} t is the conclusion of r, then ρ(x_{j}) = x_{j} for j = 1, ..., m. Now property 2 of ρ′ yields ρ′(x_{j}) = x_{j} for j = 1, ..., m, so the conclusion ρ′(g(x_{1}, ..., x_{m}) ⟶^{b} t) of s is of the form

g(x_{1}, ..., x_{m}) ⟶^{b} ρ′(t).

The premises of s are in ρ′(top(B′, r, ϕ′)), so they are of the form ρ′(t ⟶^{a} y) where t ⟶^{a} y is a premise of a rule in B′ outside the range of ϕ′. Hence y is not in the domain of ρ, i.e. ρ(y) = y, so property 2 of ρ′ yields ρ′(y) = y. Moreover, as in a proof structure no two rules have variables in common, all variables y at the right-hand side of these premises and x_{1}, ..., x_{m} are distinct. In order to show that ρ′(t) is a variable, we distinguish two cases.

1. t ⟶^{a} y ∈ top(B, r, ϕ).

Then σ(t ⟶^{a} y) ∈ H, so σ(t) is a variable. As σρ′(t) = σ(t), also ρ′(t) is a variable.

2. t ⟶^{a} y ∉ top(B, r, ϕ).

Then ϕ(b) = t ⟶^{a} y for some b ∈ B. Since t ⟶^{a} y is outside the range of ϕ′, it follows that b ∉ B′. Hence the inductive construction of B′ and ρ implies that ρ^{k}(t) is a variable for k ≥ 0. So property 3 of ρ′ yields that ρ′(t) is a variable.

Hence, s is xyft.

Since s is provable from R and xyft, by definition s ∈ S. For c′ ∈ σ(top(B′, r, ϕ′)), the xytt rule H/c′ is provable from R by means of a strictly smaller sub-structure of (B, r, ϕ), so by induction such rules H/c′ are provable from S. Since σ(s) = σρ′(top(B′, r, ϕ′)/concl(r)) = σ(top(B′, r, ϕ′))/c it follows from Proposition 2.9 that H/c is provable from S. □

Example 4.6 Applying this construction to the proof structure (B, r, ϕ) of Example 2.6 gives rise to the sub-structure (B′, r, ϕ′) displayed below, together with the (partial) substitution ρ. Applying the construction in the proof of the unification lemma to ρ gives the substitution ρ′ (with ρ′(x) = x for variables x not explicitly mentioned).

[figure: \frac{!z | z ⟶^{τ} z′}{!z ⟶^{τ} z′}; \frac{v ⟶^{a} v′ w ⟶^{ā} w′}{v | w ⟶^{τ} v′ | w′}; \frac{!u | u ⟶^{a} u′}{!u ⟶^{a} u′}; \frac{t ⟶^{a} t′}{s | t ⟶^{a} s | t′}]

ρ(v) = !z
ρ(w) = z
ρ(z′) = v′ | w′
ρ(u) = z
ρ(v′) = u′
ρ(s) = !u
ρ(t) = u
ρ(u′) = s | t′

The resulting xyft rule s is \frac{z ⟶^{a} t′ z ⟶^{ā} w′}{!z ⟶^{τ}!z | t′ | w′}.

ρ′(v) = !z_{ρ′(w) = z}_{ρ′(z′) = !z | t′ | w′}_{ρ′(u) = z}_{ρ′(v′) = !z | t′}_{ρ′(s) = !z}_{ρ′(t) = z}_{ρ′(u′) = !z | t′}

Although according to Theorem 4.5 the tyft/tyxt format reduces to the more restrictive xyft format, this is by no means an argument to abandon the tyft/tyxt format. Because a simple TSS in tyft/tyxt format may take a much more complicated form if it is described in xyft format. This is demonstrated by the following example.

Example 4.7 Assume two functions a, b of arity zero, a function f of arity one, and a label l. Consider the following TSS in tyft format.

a ⟶^{l} a \frac{a ⟶^{l} y}{a ⟶^{l} f(y)}

In order to describe this TSS in xyft format, we need an infinite number of rules: a ⟶^{l} f^{n}(a) for n = 0, 1, 2, ... (The auxiliary function symbol b is present to avoid that the TSS can be described by the single rule a ⟶^{l} x.)

4.3 Xyft reduces to tree

The following terminology originates from [12].

Definition 4.8 A variable is called free in a rule if it does not occur at the right-hand side of the premises, nor at the left-hand side of the conclusion of the rule. A rule is called pure if it is well-founded and does not contain any free variables. A tree rule is a pure xyft rule.

Theorem 4.9 Each TSS R in xyft format is transition equivalent to a TSS in tree format.

Proof. We prove R transition equivalent with the TSS S of tree rules that can be proved from R. Since all rules in S can be proved from R, Lemma 2.10 implies that each transition provable from S is also provable from R. We check the converse, namely that a closed transition p ⟶^{a} p′ provable from R is provable from S.

Since p ⟶^{a} p′ is provable from R, there exist a rule r ∈ R and a substitution σ such that the premises of r under σ are provable from R and the conclusion of r under σ yields p ⟶^{a} p′. Let r be of the form

\frac{\{z_{i} ⟶^{a_{i}} y_{i} | i ∈ I\}}{f(x_{1}, ..., x_{m}) ⟶^{a} t}

Using induction, we may assume that σ(z_{i} ⟶^{a_{i}} y_{i}) is provable from S for i ∈ I.

We construct from r a rule r′ in S as follows. If there is no backward path in the dependency graph of r from a vertex y_{i} to a vertex x_{j}, then replace the variables z_{i} and y_{i} in r by σ(z_{i}) and σ(y_{i}) respectively. Moreover, replace free variables z in t by σ(z). As p ⟶^{a} p‘ is a closed transition, σ(z) does not contain any variables. The resulting rule r′′ is a substitution instance of r, so r′′ is provable from R. Remove each premise σ(z_{i} ⟶^{a_{i}} y_{i}) from r′′. Since those transitions are provable from R, the resulting rule r′ is provable from R as well.

Clearly, r′ is xyft and without free variables. Moreover, r′ is well-founded, because for each premise z_{i} ⟶^{a_{i}} y_{i} in r′, the (only) backward path from the vertex y_{i} in the dependency graph of r′ terminates at a vertex x_{j}. Hence, r′ is a tree rule, so r′ ∈ S. Since the premises of r′ under σ are provable from S, and since the conclusion of r′ under σ yields p ⟶^{a} p′, Proposition 2.9 implies that p ⟶^{a} p′ is provable from S. □

So, we have found that for each TSS in tyft/tyxt format there exists a transition equivalent TSS in tree format. Since tree rules are well-founded tyft rules, this result implies that the congruence theorem for tyft/tyxt can do without well-foundedness.

Corollary 4.10 If a TSS R is in tyft/tyxt format, then \underline{↔}_{R} is a congruence.

5 Extensions to Other Formats

5.1 The ntyft/ntyxt format

Groote [11] extended the tyft/tyxt format to the ntyft/ntyxt format, which as extra feature allows transition rules to contain negative premises, i.e. expressions of the form t ⟶^{a} / . In a setting with negative premises, the definition of the transition relation determined by a TSS has to be adapted. Certain TSSs may fail to determine a transition relation at all, for instance due to rules such as

\frac{t ⟶^{a} /}{t ⟶^{a} t′}

One of the most general ways to associate transitions to TSSs with negative premises is through the notion of a stability, which was introduced by Gelfond and Lifschitz [8] in logic programming. The transition relation determined by a TSS is then its unique stable transition relation if such exists. Bol and Groote [4], who adapted this notion for TSSs, showed that there exist TSSs in ntyft/ntyxt format with a unique stable transition relation for which bisimulation is not a congruence. However, they found a subclass of such TSSs for which it is. They defined a (somewhat complicated) notion of reduction of TSSs, inspired by the work of Van Gelder, Ross and Schlipf [7] in logic programming, and proved a congruence theorem for well-founded TSSs in the ntyft/ntyxt format that are positive (that is without negative premises) after applying reduction. The transition relation associated to a TSS that is positive after reduction consist of the closed transitions that are provable from the reduced TSS. This is then the unique stable transition relation of the TSS.

Earlier, Groote [11] had adapted the concept of stratification—also found in logic programming, see Apt [1]—to transition system specifications, and showed how a stratified TSS determines a transition relation. He also proved that bisimulation equivalence is a congruence for well-founded stratified TSSs in the ntyft/ntyxt format. A TSS that is stratified is surely positive after reduction, and the transition relation determined by the method of stratification is the same as the one determined by the method of reduction. Thus we have a hierarchy of properties

positive ⇒ stratified ⇒ positive after reduction ⇒ has unique transition relation.

The reverse of these inclusions does not hold.

In Van Glabbeek [10] the notion of a complete TSS is proposed, which is equivalent to positive after reduction. For this purpose, the notion of provability is extended in order to allow the derivation of negative transitions. Then, a TSS is said to be complete if for each closed transition p ⟶^{a} p′, the TSS can prove either p ⟶^{a} p′ or its negation p ⟶^{a} / p′. In the same paper it is also argued that the unique stable transition relation of an incomplete TSS is not always convincing as the determined transition relation. If for any reason a transition relation needs to be associated to arbitrary TSSs, it is suggested to take the set of closed transitions p ⟶^{a} p′ that are irrefutable, in the sense that p ⟶^{a} / p′ is not provable using the extended concept of provability. Although this method yields the ‘right’ transition relation for complete TSSs, in the case of incomplete TSSs with a unique stable transition relation it may yield a different—and equally unconvincing—result as the method of stability. The transition relation associated to incomplete TSSs usually has very unpleasant properties. In particular, the congruence result for TSSs in ntyft/ntyxt format does not extend to such TSSs [10]. The following proposition, taken from [10], gives a sufficient condition for two TSSs to be transition equivalent according to each of the methods stability, completeness (=reduction) and irrefutability.

Proposition 5.1 Let R and R′ be TSSs such that R ⊢ N/c ⇔ R′ ⊢ N/c for any closed transition rule N/c with only negative premises. Here ⊢ denotes provability in the sense of Section 2. Then

• R has a unique stable transition relation iff R′ has, and in that case these relations coincide;

• R is complete iff R′ is, and in that case they determine the same transition relation;

• and the transitions irrefutable from R are the same as the ones irrefutable from R′. Thus without committing ourselves on their precise meaning, we can extend our results to TSSs with negative premises by strengthening the requirement of transition equivalence to provability of the same closed transition rules without positive premises. All definitions, lemmas and propositions of Section 2 generalize straightforwardly to TSSs with negative premises, except that a rule is now called well-founded if its collection of positive premises is so.

Definition 5.2 A xyntt rule is an xytt rule enriched with arbitrary negative premises t ⟶^{a} / . A transition rule is called xynft if it is both ntyft and xyntt. It is an ntree rule if it moreover is pure.

Without any further complications, we can repeat the construction from the previous section to show that each complete TSS in ntyft/ntyxt format is transition equivalent—it proves the same closed rules without positive premises—to a complete TSS in the ntree format.

Again, TSSs in the latter format are well-founded, so as a corollary we see that the wellfoundedness condition in the congruence theorem for the ntyft/ntyxt format can be dropped.

Corollary 5.3 If a complete TSS R is in ntyft/ntyxt format, then \underline{↔}_{R} is a congruence.

We show that in general, terms in negative premises cannot be reduced to variables. The simple negative tree format allows complete TSSs which consist of pure and well-founded ntyft/ntyxt rules, where the variables of all the premises (so also of the negative premises) are variables. We present a complete TSS in ntyft/ntyxt format for which there does not exist a transition equivalent TSS in simple negative tree format.

Our counter-example is presented in the setting of the process algebra basic CCS. This formalism assumes a constant 0, a binary function alternative composition x + y, and unary functions prefix sequential composition ax, where a ranges over an alphabet A. Basic CCS assumes relations ⟶^{a} for a ∈ A, and its operational semantics is defined in Example 2.6.

Add two functions f and g with arity one to the signature of basic CCS, and extend the operational semantics by the following transition rules, to obtain the TSS R.

\frac{x ⟶^{a} y_{1} y_{1} ⟶^{a} y_{2}}{g(x) ⟶^{a} 0}  \frac{g(x) ⟶^{a} /}{f(x) ⟶^{a} 0}

The TSS R is complete and in ntyft/ntyxt format. The premise g(x) ⟶^{a} / cannot be reduced. An obvious attempt to delete this negative premise would be to replace the second rule by the following two rules.

\frac{x ⟶^{a} /}{f(x) ⟶^{a} 0}  \frac{x ⟶^{a} y y ⟶^{a} /}{f(x) ⟶^{a} 0}

However, this adapted TSS is not transition equivalent to R. For example, f(aa0 + a0) ⟶^{a} 0 holds in the new TSS, but not in R.

In order to provide a rigorous argument that R does not reduce to a TSS in simple negative tree format, we need the following lemma. First note that a TSS T in simple negative tree format is always stratified and hence complete [10], so that there is no ambiguity about the associated transition relation. The latter can thus be taken to be the set of closed transitions that are provable from T in the extended sense of [10]. This is the concept of provability used below.

Lemma 5.4 Let T be a TSS in simple negative tree format and p_{0} and p_{1} closed terms, such that:

1. if T proves p_{0} ⟶^{a} q, then T proves p_{1} ⟶^{a} q,

2. if T proves p_{0} ⟶^{a} / , then T proves p_{1} ⟶^{a} / .

If T proves f(p_{0}) ⟶^{b} q, then T proves f(p_{1}) ⟶^{b} q′ for some q′.

Proof. Let f(p_{0}) ⟶^{b} q be provable from T. Then, by Proposition 14 in [10], there exists a rule r ∈ T and a substitution σ, such that the premises of r under σ are provable from T and the conclusion of r under σ yields f(p_{0}) ⟶^{b} q. Since r is in ntyft format, it has a conclusion of the form f(x) ⟶^{b} t, where σ(x) = p_{0} and σ(t) = q.

Define a substitution σ′ by σ′(x) = p_{1}, and σ′(x) = σ(y) for y ≠ x. Since r is in simple negative tree format, and since the premises of r under σ are provable from T, properties 1,2 of the transition systems of p_{0} and p_{1} ensure that the premises of r under σ′ are provable from T. So according to Proposition 13 in [10], the conclusion of r under σ′, f(p_{1}) ⟶^{b} σ′(t), is provable from T as well. □

Suppose that the TSS R that was defined before is transition equivalent to a TSS T in simple negative tree format. If p_{0} = a0 and p_{1} = aa0+a0, then it is easy to see that the two properties that were formulated in Lemma 5.4 are satisfied. On the other hand, R (and so T) proves f(a0) ⟶^{a} 0 and f(aa0+a0) ⟶^{a} / . According to Lemma 5.4 this cannot be, so apparently R cannot be transition equivalent to a TSS in simple negative tree format.

5.2 The panth format

Baeten and Verhoef [2] extended the tyft/tyxt format with predicates, i.e. not only relations t ⟶^{a} t′, but also predicates such as t ⟶^{a} √ are allowed to occur in transition rules. The definition of strong bisimulation, Definition 2.11, is adapted accordingly by adding a third condition:

– if pBq and p ⟶^{a}_{R} √, then q ⟶^{a}_{R} √.

Next, Verhoef [17] extended the resulting format with negative premises. A congruence theorem holds for well-founded complete TSSs that are in the so-called panth format, which is essentially the natural extension of ntyft/ntyxt with predicates.

Without any further complications, we can repeat the construction from the previous section to show that each complete TSS in panth format is transition equivalent to a complete TSS in an extension of the tree format, which allows rules to have premises of the form z ⟶^{a} √ and t ⟶^{a} / and t ⟶^{a} / √, and a conclusion of the form f(x_{1}, ..., x_{m}) ⟶^{a} √. As a corollary, we see that the well-foundedness condition in the congruence theorem for the panth format can be dropped.

Corollary 5.5 If a complete TSS R is in panth format, then \underline{↔}_{R} is a congruence.

References

[1] K.R. Apt (1990): Logic programming. In J. van Leeuwen, editor: Handbook of Theoretical Computer Science, Volume B, Formal Methods and Semantics, Elsevier, pp. 493–574.

[2] J.C.M. Baeten & C. Verhoef (1993): A congruence theorem for structured operational semantics with predicates. In E. Best, editor: Proceedings 4th Conference on Concurrency Theory (CONCUR’93), Hildesheim, LNCS 715, Springer-Verlag, pp. 477–492.

[3] B. Bloom, S. Istrail & A.R. Meyer (1988): Bisimulation can’t be traced: preliminary report. In Proceedings 15th ACM Symposium on Principles of Programming Languages, San Diego, California, pp. 229–239. To appear in Journal of the ACM.

[4] R.N. Bol & J.F. Groote (1991): The meaning of negative premises in transition system specifications. In J. Leach Albert, B. Monien & M. Rodríguez Artalejo, editors: Proceedings 18th International Colloquium on Automata, Languages and Programming (ICALP’91), Madrid, LNCS 510, Springer-Verlag, pp. 481–494.

[5] W.J. Fokkink (1994): The tyft/tyxt format reduces to tree rules. In M. Hagiya & J.C. Mitchell, editors: Proceedings 2nd Symposium on Theoretical Aspects of Computer Software (TACS’94), Sendai, Japan, LNCS 789, Springer-Verlag, pp. 440–453.

[6] W.J. Fokkink (1994): Idempotent most general unifiers for infinite sets. Report CS-R9442, CWI, Amsterdam.

[7] A. van Gelder, K. Ross & J.S. Schlipf (1991): The well-founded semantics for general logic programs, JACM 38(3), pp. 620–650.

[8] M. Gelfond & V. Lifschitz (1988): The stable model semantics for logic programming. In R. Kowalski & K. Bowen, editors: Proceedings 5th Conference on Logic Programming, MIT press, pp. 1070–1080.

[9] R.J. van Glabbeek (1993): Full abstraction in structural operational semantics (extended abstract). In M. Nivat, C. Rattray, T. Rus & G. Scollo, editors: Proceedings 3rd Conference on Algebraic Methodology and Software Technology (AMAST’93), Twente, The Netherlands, Workshops in Computing, Springer-Verlag, pp. 77–84.

[10] R.J. van Glabbeek (1995): The meaning of negative premises in transition system specifi-

cations II. Available at ftp://boole.stanford.edu/pub/DVI/negative.dvi.Z.

[11] J.F. Groote (1993): Transition system specifications with negative premises. Theoretical Computer Science 118(2), pp. 263–299.

[12] J.F. Groote & F.W. Vaandrager (1992): Structured operational semantics and bisimulation as a congruence. Information and Computation 100(2), pp. 202–260.

[13] A. Martelli & U. Montanari (1982): An efficient unification algorithm. ACM Transactions on Programming Languages and Systems 4(2), pp. 258–282.

[14] D.M.R. Park (1981): Concurrency and automata on infinite sequences. In P. Deussen, editor: 5th GI Conference, LNCS 104, Springer-Verlag, pp. 167–183.

[15] G.D. Plotkin (1981): A structural approach to operational semantics. Report DAIMI FN-19, Aarhus University.

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

[17] C. Verhoef (1994): A congruence theorem for structured operational semantics with predicates and negative premises. In B. Jonsson & J. Parrow, editors: Proceedings 5th Conference on Concurrency Theory (CONCUR’94), Uppsala, LNCS 836, Springer-Verlag, pp. 433–448.