From rewrite rules to bisimulation congruences.
The dynamics of many calculi can be most clearly defined by a reduction semantics. To work with a calculus, however, an understanding of operational congruences is fundamental; these can often be given tractable definitions or characterisations using a labelled transition semantics. This paper considers calculi with arbitrary reduction semantics of three simple classes, firstly ground term rewriting, then left-linear term rewriting, and then a class which is essentially the action calculi lacking substantive name binding. General definitions of labelled transitions are given in each case, uniformly in the set of rewrite rules, and without requiring the prescription of additional notions of observation. They give rise to bisimulation congruences. As a test of the theory it is shown that bisimulation for a fragment of CCS is recovered. The transitions generated for a fragment of the Ambient Calculus of Cardelli and Gordon, and for SKI combinators, are also discussed briefly.
Introduction
The dynamic behaviour of many calculi can be defined most clearly by a reduction semantics,
comprising a set of rewrite rules, a set of reduction contexts in which they may be applied, and a
structural congruence. These define the atomic internal reduction steps of terms. To work with a
calculus, however, a compositional understanding of the behaviour of arbitrary subterms, as given by
some operational congruence relation, is usually required. The literature contains investigations of
such congruences for a large number of particular calculi. They are often given tractable definitions
or characterisations via labelled transition relations, capturing the potential external interactions
between subterms and their environments. Defining labelled transitions that give rise to satisfactory
operational congruences generally requires some mix of calculus-specific ingenuity and routine work.
In this paper the problem is addressed for arbitrary calculi of certain simple forms. We give
general definitions of labelled transitions that depend only on a reduction semantics, without requiring
any additional observations to be prescribed. We first consider term rewriting, with ground or
left-linear rules, over an arbitrary signature but without a structural congruence. We then consider
calculi with arbitrary signatures containing symbols 0 and j, a structural congruence consisting of
associativity, commutativity and unit, left-linear rules, and non-trivial sets of reduction contexts.
This suffices, for example, to express CCS-style synchronisation. It is essentially the same as the
Computer Laboratory, University of Cambridge. Email: Peter.Sewell@cl.cam.ac.uk

INTRODUCTION

class of Action Calculi in which all controls have some number of arguments of
In each case we define labelled transitions, prove that bisimulation is a congruence and
give some comparison results.
Background: From reductions to labelled transitions to reductions. Definitions of the
dynamics (or small-step operational semantics) of lambda calculi and sequential programming languages
have commonly been given as reduction relations. The -calculus has the rewrite rule
(-x:M)N \Gamma!M [N=x] of fi reduction, which can be applied in any context. For programming lan-
guages, some control of the order of evaluation is usually required. This has been done with abstract
machines, in which the states, and reductions between them, are ad-hoc mathematical objects. More
elegantly, one can give definitions in the structural operational semantics (SOS) style of Plotkin
[Plo81]; here the states are terms of the language (sometimes augmented by e.g. a store), the reductions
are given by a syntax-directed inductive definition. Explicit reformulations using rewrite rules
and reduction contexts were first given by Felleisen and Friedman [FF86]. (We neglect semantics in
the big-step/evaluation/natural style.)
In contrast, until recently, definitions of operational semantics for process calculi have been
primarily given as labelled transition relations. The central reason for the difference is not mathe-
matical, but that lambda and process terms have had quite different intended interpretations. The
standard interpretation of lambda terms and functional programs is that they specify computations
which may either not terminate, or terminate with some result that cannot reduce further. Confluence
properties ensure that such result terms are unique if they exist; they can implicitly be
examined, either up to equality or up to a coarser notion. The theory of processes, however, inherits
from automata theory the view that process terms may both reduce internally and interact with
their environments; labelled transitions allow these interactions to be expressed. Reductions may
create or destroy potential interactions. Termination of processes is usually not a central concept,
and the structure of terms, even of terms that cannot reduce, is not considered examinable.
An additional, more technical, reason is that definitions of the reductions for a process calculus
require either auxiliary labelled transition relations or a non-trivial structural congruence. For
example, consider the CCS fragment below.
Its standard semantics has reductions P \Gamma!Q but also labelled transitions P ff
\Gamma!Q and P -
ff
\Gamma!Q.
These represent the potentials that P has for synchronising on ff. They can be defined by an SOS
Out
ff
\Gamma!P
In
\Gamma!P
Com
ff
Par
\Gamma!Q
\Gamma!Q
\Gamma!Q
\Gamma! is either \Gamma!, ff
\Gamma! or -
ff
\Gamma!. It has been noted by Berry and Boudol [BB92], following work
of Ban-atre and Le M'etayer [BM86] on the \Gamma language, that semantic definitions of process calculi
could be simplified by working modulo an equivalence that allows the parts of a redex to be brought
syntactically adjacent. Their presentation is in terms of Chemical Abstract Machines; in a slight
variation we give a reduction semantics for the CCS fragment above. It consists of the rewrite rule
Q, the set of reduction contexts given by
and the structural congruence j defined to be the least congruence satisfying
and use of j on the right, this gives exactly the same reductions
as before. For this toy calculus the two are of similar complexity. For the -calculus ([MPW92],
building on [EN86]), however, Milner has given a reduction semantics that is much simpler that the
rather delicate SOS definitions of - labelled transition systems [Mil92]. Following this, more recent
name passing process calculi have often been defined by a reduction semantics in some form, e.g.
the HO- [San93], ae [NM95], Join [FG96], Blue [Bou97], Spi [AG97], dpi [Sew98b], D- [RH98] and
Ambient [CG98] Calculi.
Turning to operational congruences, for confluent calculi the definition of an appropriate operational
congruence is relatively straightforward, even in the (usual) case where the dynamics is
expressed as a reduction relation. For example, for a simple eager functional programming language,
with a base type Int of integers, terminated states of programs of type Int are clearly observable up
to equality. These basic observations can be used to define a Morris-style operational congruence.
Several authors have considered tractable characterisations of these congruences in terms of bisimulation
- see e.g. [How89, AO93, Gor95] and the references therein, and [GR96] for related work on
an object calculus.
For non-confluent calculi the situation is more problematic - process calculi having labelled transition
semantics have been equipped with a plethora of different operational equivalences, whereas
rather few styles of definition have been proposed for those having reduction semantics. In the
labelled transition case there are many more-or-less plausible notions of observation, differing e.g.
in their treatment of linear/branching time, of internal reductions, of termination and divergence,
etc. Some of the space is illustrated in the surveys of van Glabbeek [Gla90, Gla93]. The difficulty
here is to select a notion that is appropriate for a particular application; one attempt is in [Sew97].
In the reduction case we have the converse problem - a reduction relation does not of itself seem to
support any notion of observation that gives rise to a satisfactory operational congruence. This was
explicitly addressed for CCS and -calculi by Milner and Sangiorgi in [MS92, San93], where barbed
bisimulation equivalences are defined in terms of reductions and observations of barbs. These are
vestigial labelled transitions, similar to the distinguished observable transitions in the tests of De
Nicola and Hennessy [DH84]. The expressive power of their calculi suffices to recover early labelled
transition bisimulations as the induced congruences. Related work of Honda and Yoshida [HY95]
uses insensitivity as the basic observable.
.to labelled transitions Summarizing, definitions of operational congruences, for calculi having
reduction semantics, have generally been based either on observation of terminated states, in the
confluent case, or on observation of some barbs, where a natural definition of these exists. In
either case, characterisations of the congruences in terms of labelled transitions, involving as little
quantification over contexts as possible, are desirable. Moreover, some reasonable calculi may not
have a natural definition of barb that induces an appropriate congruence.
In this paper we show that labelled transitions that give rise to bisimulation congruences can
be defined purely from the reduction semantics of a calculus, without prescribing any additional
observations. It is preliminary work, in that only simple classes of reduction semantics, not involving
name or variable binding, will be considered. As a test of the definitions we show that they recover
the usual bisimulation on the CCS fragment above. We also discuss term rewriting and a fragment of
the Ambient calculus of Cardelli and Gordon. To directly express the semantics of more interesting
calculi requires a richer framework. One must deal with binding, with rewrite rules involving term or
name substitutions, with a structural congruence that allows scope mobility, and with more delicate
sets of reduction contexts. The Action Calculi of Milner [Mil96] are a candidate framework that
allows several of the calculi mentioned above to be defined cleanly; this work can be seen as a step
towards understanding operational congruences for arbitrary action calculi.
Labelled transitions intuitively capture the possible interactions between a term and a surrounding
context. Here this is made explicit - the labels of transitions from a term s will be contexts that,
when applied to s, create an occurrence of a rewrite rule. A similar approach has been followed by
Jensen [Jen98], for a form of graph rewriting that idealizes action calculi. Bisimulation for a particular
action calculus, representing a -calculus, has been studied by Mifsud [Mif96]. In the next three
sections we develop the theory for ground term rewriting, then for left-linear term rewriting, and
then with the addition of an AC1 structural congruence and reduction contexts. Section 5 contains
some concluding remarks. Most proofs are omitted, but can be found in the technical report
[Sew98a].
Ground term rewriting
In this section we consider one of the simplest possible classes of reduction semantics, that of ground
term rewriting. The definitions and proofs are here rather straightforward, but provide a guide to
those in the following two sections.
Reductions We take a signature consisting of a set \Sigma of function symbols, ranged over by oe, and
an arity function j j from \Sigma to N. Context composition and application of contexts to (tuples of)
terms are written A : B and A : s, the identity context as and tupling with +. We say an n-hole
context is linear if it has exactly one occurrence of each of its holes. In this section a; b; l;
range over terms, A; B; C; D;F; H range over linear unary contexts and E ranges over linear binary
contexts.
We take a set R of rewrite rules, each consisting of a pair hl; ri of terms. The reduction relation
is then
Labelled Transitions The transitions of a term s will be labelled by linear unary contexts. Transitions
s\Gamma!t labelled by the identity context are simply reductions (or -transitions). Transitions
\Gamma!t for F 6j indicate that applying F to s creates an instance of a rewrite rule, with target
instance t. For example, given the rule
we will have labelled transitions
for all C and
The labels are f F j 9hl; ri 2 R; s and the contextual labelled transition relations F
\Gamma!
are defined by:
\Gamma!t
ri
Bisimulation Congruence Let - be strong bisimulation with respect to these transitions. The
congruence proof is straightforward. It is given some detail as a guide to the more intricate
corresponding proofs in the following two sections, which have the same structure. Three lemmas
show how contexts in labels and in the sources of transitions interrelate; they are proved by
case analysis using a dissection lemma which is standard folklore.
then one of the following cases holds.
1. (b is in a) There exists D such that a
2. (a is properly in b) There exists D with D 6= such that D :
3. (a and b are disjoint) There exists E such that
then one of the following holds:
1. There exists some H such that
s.
2. There exists some - t, A 1 and A 2 such that
t.
Proof By the definition of reduction
ri
Applying the dissection lemma (Lemma 1) to A : l gives the following cases.
1. (l is in s) There exists B such that
Taking the second clause holds.
2. (s is properly in l) There exists B with B 6= such that
Taking the second clause holds.
3. (s and l are disjoint) There exists E such that
Taking r) the first clause holds.Lemma 3 If A : s F
\Gamma!t and F 6= then s F : A
\Gamma!t.
Proof By the definition of labelled transitions
ri
linear
\Gamma!t. 2
Lemma
\Gamma!t then A : s F
\Gamma!t.
Proof so the conclusion is immediate, otherwise by the definition of
transitions
ri
One then has A : s F
\Gamma!t by the definition of transitions, by cases for F 6= and
Proposition 5 - is a congruence.
Proof We show
is a bisimulation.
1. Suppose A : s\Gamma!t.
By Lemma 2 one of the following holds:
(a) There exists some H such that
s.
Hence
(b) There exists some - t, A 1 and A 2 such that
t.
By s - s 0 there exists - t 0 such that s 0 A2
t.
By the definition of reduction
2. Suppose A : s F
\gamma!t for F 6= .
\gamma!t.
By s - s 0 there exists t 0 such that s
t.
\gamma!t 0 .
alternative approach would be to take transitions
for unary linear contexts F . Note that these are defined using only the reduction relation, whereas
the definition above involved the reduction rules. Let - alt be strong bisimulation with respect to
these transitions. One can show that - alt is a congruence and moreover is unaffected by cutting
down the label set to that considered above. In general - alt is strictly coarser than -. For an
example of the non-inclusion, if the signature consists of constants ff; fi and a unary symbol fl with
reduction rules ff\gamma!ff, fi \gamma!fi and fl(fi)\gamma!fi, then ff 6- fi whereas ff - alt fi. This insensitivity to
the possible interactions of terms that have internal transitions suggests that the analogue of - alt ,
in more expressive settings, is unlikely to coincide with standard bisimulations for particular calculi.
Indeed, one can show that applying the alternative definition to the fragment of CCS
ff
ff
(with its usual reduction relation) gives an equivalence that identifies ff j -
ff with
fi.
Remark In the proofs of Lemmas 2-4 the labelled transition exhibited for the conclusion involves
the same rewrite rule as the transition in the premise. One could therefore take the finer transitions
F
annotated by rewrite rules, and still have a congruence result. In some cases this gives a
finer bisimulation relation.
Remark The labelled transition relation is linear in R, i.e. the labelled transitions generated by a
union of sets of rewrite rules are just the union of the relations generated by R 1 and R 2 .
rewriting with left-linear rules
In this section the definitions are generalised to left-linear term rewriting, as a second step towards
a framework expressive enough for simple process calculi.
Notation In the next two sections we must consider more complex dissections of contexts and
terms. It is convenient to treat contexts and terms uniformly, working with n-tuples of m-hole
contexts for m;n - 0. Concretely, we work in the category C \Sigma that has the natural numbers as
objects and morphisms
The identity on m is id m
composition is substitution, with
an [b strictly
associative binary products, written with +. If a : m! k and b : m! l we write a \Phi b for
l. Angle brackets and domain subscripts will often be
elided. We let a; b; e; q; range over 0 !m morphisms, i.e. m-tuples of terms,
range over m! 1 morphisms, i.e. m-hole contexts, and - over projections and permutations. Say a
morphism linear if it contains exactly one occurrence of each
if it contains at most one occurrence of each. We sometimes abuse notation in examples, writing
Remark Many slight variations of C \Sigma are possible. We have chosen to take the objects to be
natural numbers, instead of finite sets of variables, to give a lighter notation for labels. The concrete
syntax is chosen so that morphisms from 0 to 1 are exactly the standard terms over \Sigma, modulo
elision of the angle brackets and subscript 0.
Reductions The usual notion of left-linear term rewriting is now expressible as follows. We take
a set R of rewrite rules, each consisting of a triple hn; L; Ri where n - 0, linear and
1. The reduction relation over f s is then defined by
Labelled Transitions The labelled transitions of a term s again be of two forms,
s\gamma!t, for internal reductions, and s F
\gamma!T where F 6= is a context that, together with part of s,
makes up the left hand side of a rewrite rule. For example, given the rule
we will have labelled transitions
for all terms s Labelled transitions in which the label contributes the whole of the left hand
side of a rule would be redundant, so the definition will exclude e.g. s ffi(fl(
\gamma! ffl(s). Now consider the
rule
As before there will be labelled transitions
for all s. In addition, one can construct instances of the rule by placing the term ff in contexts
suggesting labelled transitions ff oe( ;fl(t))
\gamma! ffl(t) for any t. Instead, to keep the label sets
small, and to capture the uniformity in t, we allow both labels and targets of transitions to be
parametric in un-instantiated arguments of the rewrite rule. In this case the definition will give
In general, then, the contextual labelled transitions are of the form s F
\gamma!T , for
1. The first argument of F is the hole in which s can be placed to create an instance of a
rule L; the other n arguments are parameters of L that are not thereby instantiated. The transitions
are defined as follows.
, s\gamma!T .
\gamma!T , for linear and not the identity, iff there exist
permutation
linear and not the identity
such that
The definition is illustrated in Figure 1. The restriction to L 1 6= id 1 excludes transitions where the
label contributes the whole of L. The permutation - is required so that the parameters of L can be
divided into the instantiated and uninstantiated. For example the rule
F
R
nn
s

Figure

1: Contextual Labelled Transitions for Left-Linear Term Rewriting. Boxes with m input
wires (on their right) and n output wires (on their left) represent n-tuples of m-hole contexts. Wires
are ordered from top to bottom.
will give rise to transitions
(The last is redundant; it could be excluded by requiring - to be a monotone partition of m into
Bisimulation Congruence A binary relation S over terms f a j a is lifted to a relation
by A [S] A 0 def
Say S is a bisimulation if for any s S s 0
and write - for the largest such. As before the congruence proof requires a simple dissection lemma
and three lemmas relating contexts in sources and labels.
Lemma 6 (Dissection) If A :
then one of the following holds.
1. (a is not in any component of b) There exist
linear and not the identity
such that
i.e. there are m 1 components of b in a and m 2 in A.
2. (a is in a component of b) m - 1 and there exist
partition
such that
linear then one of the following holds.
1. There exists some
2.
Lemma 8 If A : s F
one of the following
holds.
1. There exists H : 1+n! 1 such that
id n ).
2. There exist
such that s F
Lemma 9 If s
\gamma! T for linear then for all
Theorem 1 - is a congruence.
Proof We show S   , where
is a bisimulation. First note that for any A : To see this,
take
linear such that
An
Each A i is linear, so A
We now show that if A
\gamma!T then there exists T 0 such that
1. Suppose A : s\gamma!t.
By Lemma 7 one of the following holds:
(a) There exists some
Hence
(b) There exist
By s - s 0 there exists T 0 such that s 0 F
By the definition of reduction A : s
2. Suppose A : s F
linear and F 6= id 1 .
By Lemma 8 one of the following holds.
(a) There exists
Hence
(b) There exist
such that s F
By s - s 0 there exists -
Now if
for A i linear and s
F
then by the above there exists Tn such
that
F
definition reduces to that of Section 2 if all rules are ground. For open rules, instead
of allowing parametric labels, one could simply close up the rewrite rules under instantiation, by
apply the earlier definition. In general
this would give a strictly coarser congruence. For an example of the non-inclusion, take a
signature consisting of a nullary ff and a unary fl, with R consisting of the rules fl( )\gamma!fl( ) and
fl(fl(ff))\gamma!fl(fl(ff)). We have g. The transitions are
for m;n - 1, so fl(ff) 6- R fl(fl(ff)) but fl(ff) - Cl(R) fl(fl(ff)).
Proposition
Comparison Bisimulation as defined here is a congruence for arbitrary left-linear term rewriting
systems. Much work on term rewriting deals with reduction relations that are confluent and ter-
minating. In that setting terms have unique normal forms; the primary equivalence on terms is ',
have the same normal form. This is easily proved to be a congruence. In
general, it is incomparable with -. To see one non-inclusion, note that - is sensitive to atomic
reduction steps; for the other that - is not sensitive to equality of terms - for example, with only
nullary symbols ff; fi; fl, and rewrite rule fl \gamma!fi, we have ff - fi and fi ' fl, whereas ff 6' fi and
fi 6- fl. One might address the second non-inclusion by fiat, adding, for any value v, a unary test
operator H v and reduction rule H v (v)\gamma!v. For the first, one might move to a weak bisimulation,
abstracting from reduction steps. The simplest alternative is to take - to be the largest relation S
such that if s S s 0 then
and symmetric clauses.
Say the set R of rewrite rules is right-affine if the right hand side of each rule is affine. Under
this condition - is a congruence; the result without it is left open.
Theorem 2 If R is right-affine then - is a congruence.
Example - Integer addition For some rewrite systems - coincides with '. Taking a signature
comprising nullary z for each integer z and binary plus and ifzero, and rewrite rules
for all integers x and z gives labelled transitions
x plus( ;z)
together with the reductions \gamma!. Here the normal forms are simply the integers; - and ' both
coincide with integer equality.
In general, however, - is still incomparable with '. For example, with unary ffi; fl, nullary ff, and
rules fl(ff)\gamma!ff, ffi(ff)\gamma!ff, and ffi(fl( ))\gamma! , we have ff 6- fi(ff). This may be a pathological rule set;
one would like to have conditions excluding it under which - and ' coincide.
Example - SKI Combinators Taking a signature \Sigma comprising nullary I ; K;S and binary ffl,
and rewrite rules
gives labelled transitions
I ffl 1
together with some permutation instances of these and the reductions \gamma!. The significance of -
and - here is unclear. Note that the rules are not right-affine, so Theorem 2 does not guarantee
that - is a congruence. It is quite intensional, being sensitive to the number of arguments that can
be consumed immediately by a term. For example, K
rewriting with left-linear rules, parallel and boxing
In this section we extend the setting to one sufficiently expressive to define the reduction relations
of simple process calculi. We suppose the signature \Sigma includes binary and nullary symbols j and 0,
for parallel and nil, and take a structural congruence j generated by associativity, commutativity
and identity axioms. Parallel will be written infix. The reduction rules R are as before. We now
allow symbols to be boxing, i.e. to inhibit reduction in their arguments. For each oe 2 \Sigma we suppose
given a set B(oe) ' defining the argument positions where reduction may take place. We
require 2g. The reduction contexts C ' f C linear are generated by
Formally, structural congruence is defined over all morphisms of C \Sigma as follows. It is a family of
relations indexed by domain and codomain arities; the indexes will usually be elided.
Reductions The reduction relation over f s is defined by s\gamma!t iff
This class of calculi is essentially the same as the class of Action Calculi in which there is no
substantive name binding, i.e. those in which all controls K have arity rules of the form
(here the a i are actions, not morphisms from C \Sigma ). It includes simple process calculi. For example,
the fragment of CCS in Section 1 can be specified by taking a signature \Sigma CCS consisting of unary
ff: and -
ff: for each ff 2 A, with 0 and j, and rewrite rules
Notation For a context f : m!n and i 2 1::m say f is shallow in argument i if all occurrences of
in f are not under any symbol except j. Say f is deep in argument i if any occurrence of i in f
is under some symbol not equal to j. Say f is shallow (deep) if it is shallow (deep) in all i 2 1::m.
Say f is i-separated if there are no occurrences of any j in parallel with an occurrence of i .
Labelled Transitions The labelled transitions will be of the same form as in the previous section,
with transitions s F
non-trivial label F may either
contribute a deep subcontext of the left hand side of a rewrite rule (analogous to the non-identity
labels of the previous section) or a parallel component, respectively with F deep or shallow in its
first argument. The cases must be treated differently. For example, the rule
TERM REWRITING WITH LEFT-LINEAR RULES, PARALLEL AND BOXING
will generate labelled transitions
As before, transitions that contribute the whole of the left hand side of a rule, such
as s j ff j fi
are redundant and will be excluded. It is necessary to take labels to be subcontexts of
left hand sides of rules up to structural congruence, not merely up to equality. For example, given
the rule
we need labelled transitions
Finally, the existence of rules in which arguments occur in parallel with non-trivial terms means
that we must deal with partially instantiated arguments. Consider the rule
The term -) j ae could be placed in any context oe( j s; t) to create an instance of the left hand side,
with - (from the term) instantiating 1 , t (from the context) instantiating 2 , and ae j s (from both)
instantiating 3 . There will be a labelled transition
parametric in two places but partially instantiating the second by ae. The general definition of
transitions is given in Figure 2. It uses additional notation - we write par n for h 1
and ppar n for n!n. Some parts of the definition are illustrated
in

Figure

3, in which rectangles denote contexts and terms, triangles denote instances of par, and
hatched triangles denote instances of ppar.
To a first approximation, the definition for F deep in 1 states that s F
\gamma!T iff there is a rule
L\gamma!R such that L can be factored into L 2 (with m 2 arguments) enclosing L 1 (with m 1 arguments)
in parallel with m 3 arguments. The source s is L 1 instantiated by u, in parallel with e; the label F is
roughly the target T is R with instantiated by u and m 3 partially instantiated by
e. It is worth noting that the non-identity labelled transitions do not depend on the set of reduction
contexts.
The intended intuition is that the labelled transition relations provide just enough information so
that the reductions of a term A : s are determined by the labelled transitions of s and the structure
of A, which is the main property required for a congruence proof. A precise result, showing that
the labelled transitions provide no extraneous information, would be desirable.
Bisimulation Congruence Bisimulation - is defined exactly as in the previous section. As
before, the congruence proof requires dissection lemmas, analogous to Lemmas 1 and 6, lemmas
showing that if A : s has a transition then s has a related transition, analogous to Lemmas 2,3 and
7,8, and partial converses to these, analogous to Lemmas 4 and 9. All except the main dissection
lemma are omitted here, but can be found in the long version.
Lemma 11 (Dissection) If m - 0,
with A and B linear, and A : a one of the following hold
Transitions s F
\gamma!T , for are defined by:
ffl For F j id
ffl For F deep in argument 1: s F
\gamma!T iff there exist
permutation
linear and deep
linear, deep in argument 1 and 1-separated
such that
ffl For F shallow in argument 1 and F 6j id
\gamma!T iff there exist
permutation
linear and deep
linear and deep
such that

Figure

2: Contextual Labelled Transitions
em 3
e
e
R
s
F
e
R
Deep Shallow

Figure

3: Contextual Labelled Transitions Illustrated
1. (a is not deeply in any component of b) There exist
linear and 1-separated
linear and deep
such that
a j par 1+m3
There are m 1 of the b in a, m 2 of the b in A and m 3 of the b potentially overlapping A and a.
The latter are split into e 1 , in a, and e 2 , in A.
2. (a is deeply in a component of b) m - 1 and there exist
partition
linear and deep
such that
The first clause of the lemma is illustrated in Figure 4. For example, consider A : a
Clause 1 of the lemma holds, with
This dissection should give rise to a transition
Theorem 3 - is a congruence.
Remark The definitions allow only rather crude specifications of the set C of reduction contexts.
They ensure that C has a number of closure properties. Some reduction semantics require more
delicate sets of reduction contexts. For example, for a list cons constructor one might want to
allow is taken from some given set of values. This would require a
non-trivial generalisation of the theory.
A a

Figure

4: Clause 1 of Dissection Lemma
Example - CCS synchronization For our CCS fragment the definition gives
\gamma!
\gamma!
together with structurally congruent transitions , i.e. those generated by
and the reductions.
Proposition 12 - coincides with bisimulation over the labelled transitions of Section 1.
Proof Write - std for the standard bisimulation over the labelled transitions of Section 1. To show
- std is a bisimulation for the contextual labelled transitions, suppose
\gamma! T . There
must exist u and r such that P j but then P ff
so there exists Q 0
such that P 0 ff
There must then exist u 0 and r 0 such that
hence
\gamma! . Using the fact that - std is a congruence we have
so
For the converse, suppose
\gamma!Q. There must exist u and r such that P j ff:u j r
and
\gamma! so there exists T 0 such that P
There must then exist u 0 and r 0 such that
the definition of [
The standard transitions coincide (modulo structural congruence) with the contextual labelled transitions
with their parameter instantiated by 0. One might look for general conditions on R under
which bisimulation over such 0-instantiated transitions is already a congruence, and coincides with
-.
Example - Ambient movement The CCS fragment is degenerate in several respects - in the
left hand side of the rewrite rule there are no nested non-parallel symbols and no parameters in
parallel with any non-0 term, so there are no deep transitions and no partial instantiations. As a
less degenerate example we consider a fragment of the Ambient Calculus [CG98] without binding.
The signature \Sigma Amb has unary m[ ] (written outfix), in m:, out m: and open m:, for all m 2 A. Of
these only the m[ ] allow reduction. The rewrite rules RAmb are
open
The definition gives the transitions below, together with structurally congruent transitions, permutation
instances, and the reductions.
in m:s j r n[
out
open
5 Conclusion
We have given general definitions of contextual labelled transitions, and bisimulation congruence
results, for three simple classes of reduction semantics. It is preliminary work - the definitions
may inform work on particular interesting calculi, but to directly apply the results they must be
generalized to more expressive classes of reduction semantics. Several directions suggest themselves.
Higher order rewriting Functional programming languages can generally be equipped with
straightforward definitions of operational congruence, involving quantification over contexts. As
discussed in the introduction, in several cases these have been given tractable characterisations in
terms of bisimulation. One might generalise the term rewriting case of Section 3 to some notion of
higher order rewriting [vR96] equipped with non-trivial sets of reduction contexts, to investigate the
extent to which this can be done uniformly.
Name binding To express calculi with mobile scopes, such as the -calculus and its descendants,
one requires a syntax with name binding, and a structural congruence allowing scope extrusion.
Generalising the definitions of Section 4 to the class of all non-higher-order action calculi would take
in a number of examples, some of which currently lack satisfactory operational congruences, and
should show how the indexed structure of - labelled transitions arises from the rewrite rules and
structural congruence.
Ultimately one would like to treat concurrent functional languages. In particluar cases it has
been shown that one can define labelled transitions that give rise to bisimulation congruences, e.g.
by Ferreira, Hennessy and Jeffrey for Core CML [FHJ96]. To express the reduction semantics of
such languages would require both higher order rules and a rich structural congruence.
Colouring The definition of labelled transitions in Section 4 is rather intricate - for tractable
generalisations, to more expressive settings, one would like a more concise characterisation. A
promising approach seems to be to work with coloured terms, in which each symbol except j and 0
is given a tag from a set of colours. This gives a notion of occurrence of a symbol in a term that is
preserved by structural congruence and context application, and hence provides a different way of
formalising the idea that the label of a transition s F
\gamma!T must be part of a redex within F : s.
Observational congruences We have focussed on strong bisimulation, which is a very intensional
equivalence. It would be interesting to know the extent to which congruence proofs can be
given uniformly for equivalences that abstract from branching time, internal reductions etc. More
particularly, one would like to know whether Theorem 2 holds without the restriction to right-affine
rewrite rules. One can define barbs for an arbitrary calculus by s # () 9F 6j id
\gamma!T , so s #
iff s has some potential interaction with a context. Conditions under which this barbed bisimulation
congruence coincides with - could provide a useful test of the expressiveness of calculi.
Structural operational semantics Our definitions of labelled transition relations are not inductive
on term structure. Several authors have considered calculi equipped with labelled transitions
defined by an SOS in some well-behaved format, e.g. [dS85, BIM95, GV92, GM98, TP97, Ber98].
The relationship between the two is unclear - one would like conditions on rewrite rules that ensure
the labelled transitions of Section 4 are definable by a functorial operational semantics [TP97].
Conversely, one would like conditions on an SOS ensuring that it is characterised by a reduction
semantics.

Acknowledgements

I would like to thank Philippa Gardner, Ole Jensen, S-ren Lassen, Jamey
Leifer, Jean-Jacques L'evy, and Robin Milner, for many interesting discussions and comments on
earlier drafts, and to acknowledge support from EPSRC grant GR/K 38403.



--R

A calculus for cryptographic protocols: The spi calculus.
Full abstraction in the lazy lambda calculus.
The chemical abstract machine.
A congruence theorem for structured operational semantics of higher-order languages
Bisimulation can't be traced.
A new computational model and its discipline of programming.

Mobile ambients.
Testing equivalences for processes.

A calculus of communicating systems with label-passing
Control operators
The reflexive CHAM and the join-calculus
A theory of weak bisimulation for core CML.
The linear time - branching time spectrum
The linear time - branching time spectrum II
The tile model.
Bisimilarity as a theory of functional programming.
Bisimilarity for a first-order calculus of objects with subtyping
Structured operational semantics and bisimulation as a congruence.
Equality in lazy computation systems.
On reduction-based process semantics
PhD thesis
Control Structures.
Functions as processes.
Calculi for interaction.
A calculus of mobile processes
Barbed bisimulation.
Constraints for free in concurrent computation.
A structural approach to operational semantics.
A typed language for distributed mobile processes.
Expressing Mobility in Process Algebras: First-Order and Higher-Order Paradigms
On implementations and semantics of a concurrent programming language.
From rewrite rules to bisimulation congruences.
Global/local subtyping and capability inference for a distributed
Towards a mathematical operational semantics.
Confluence and Normalisation for Higher-Order Rewriting
--TR
Equality in lazy computation systems
The linear time-branching time spectrum (extended abstract)
The chemical abstract machine
Dynamic congruence vs. progressing bisimulation for CCS
Structured operational semantics and bisimulation as a congruence
A calculus of mobile processes, I
Full abstraction in the lazy lambda calculus
Turning SOS rules into equations
Bisimulation can''t be traced
On reduction-based process semantics
A theory of weak bisimulation for core CML
The reflexive CHAM and the join-calculus
Bisimilarity for a first-order calculus of objects with subtyping
The MYAMPERSANDpgr;-calculus in direct style
A calculus for cryptographic protocols
A typed language for distributed mobile processes (extended abstract)
rewriting and all that
The tile model
Constraints for Free in Concurrent Computation
Barbed Bisimulation
Global/Local Subtyping and Capability Inference for a Distributed pi-calculus
From Rewrite to Bisimulation Congruences
A Categorical Axiomatics for Bisimulation
The Linear Time - Branching Time Spectrum II
On Implementations and Semantics of a Concurrent Programming Language
Mobile Ambients
Towards a Mathematical Operational Semantics
A Congruence Theorem for Structured Operational Semantics of Higher-Order Languages

--CTR
Davide Grohmann , Marino Miculan, Directed Bigraphs, Electronic Notes in Theoretical Computer Science (ENTCS), 173, p.121-137, April, 2007
Henrik Pilegaard , Flemming Nielson , Hanne Riis Nielson, Active Evaluation Contexts for Reaction Semantics, Electronic Notes in Theoretical Computer Science (ENTCS), v.175 n.1, p.57-70, May, 2007
Vladimiro Sassone , Pawe Sobociski, Locating reaction with 2-categories, Theoretical Computer Science, v.333 n.1-2, p.297-327, 1 March 2005
Ole Hgh Jensen , Robin Milner, Bigraphs and transitions, ACM SIGPLAN Notices, v.38 n.1, p.38-49, January
Hartmut Ehrig , Barbara Knig, Deriving bisimulation congruences in the DPO approach to graph rewriting with borrowed contexts, Mathematical Structures in Computer Science, v.16 n.6, p.1133-1163, December 2006
Massimo Merro , Francesco Zappa Nardelli, Behavioral theory for mobile ambients, Journal of the ACM (JACM), v.52 n.6, p.961-1023, November 2005
term rewriting;bisimuation;operational congruences;labelled transition systems;process calculi;operational sematics