ISSN
02496399
ISRN
INRIA/RR4395FR+ENG apport
de recherche
THÈME 1
INSTITUT NATIONAL DE RECHERCHE EN INFORMATIQUE ET EN AUTOMATIQUE
Synthesising Labelled Transitions and Operational
Congruences in Reactive Systems, Part 2
James J. Leifer
N° 4395
March 2002
Unité de recherche INRIA Rocquencourt
Domaine de Voluceau, Rocquencourt, BP 105, 78153 Le Chesnay Cedex (France)
Téléphone : +33 1 39 63 55 11  Télécopie : +33 1 39 63 53 30
Synthesising Labelled Transitions and Operational
Congruences in Reactive Systems, Part 2
James J. Leifer
Th‘eme 1  R’eseaux et syst‘emes
Projet Moscova
Rapport de recherche n° 4395  March 2002  48 pages
Abstract: This paper is the second in a series of two. It relies on its companion, Part 1, to
motivate the central problem addressed by the series, namely: how to synthesise labelled
transitions for reactive systems and how to prove congruence results for operational equiv
alences and preorders defined above those transitions. The purpose of this paper is (i) to
show that the hypotheses required of functorial reactive systems from Part 1, for example
the sliding properties of IPO (idem pushout) squares, are indeed satisfied for functors of a
general form; (ii) to illustrate an example of a functorial reactive system based on Milner's
action calculi, which satisfy the RPO (relative pushout) hypothesis required in the proofs
of congruence from Part 1.
Keywords: labelled transition, structural congruence, bisimulation, action calculi,
pushout
Synth‘ese de transitions ’etiquet’ees et de congruences
op’erationnelles pour les syst‘emes r’eactifs, deuxi‘eme partie
R’esum’e : Cet article forme le second d'une s’erie. Le lecteur est renvoy’e ‘a l'article associ’e
(premi‘ere partie) pour un expos’e de la motivation du probl‘eme auquel s'attaque cette s’erie,
‘a savoir comment synth’etiser des transitions ’etiquet’ees pour des syst‘emes r’eactifs et com
ment prouver des r’esultats de congruence pour des ’equivalences et pr’eordres op’erationnels
d’efinis sur ces transitions. Le but de cet article est, premi‘erement, de montrer que les hy
poth‘eses de la d’efinition des syst‘emes r’eactifs fonctoriels de premi‘ere partie, par exemple
les propri’et’es de glissement des diagrammes d'IPO (``idem pushout''), sont bien satisfaites
pour des foncteurs d'une certaine forme g’en’erale ; deuxi‘emement, d'illustrer un exemple
de syst‘eme r’eactif fonctoriel bas’e sur les ``action calculi'' de Milner, qui v’erifient les hy
poth‘eses de RPO (``relative pushout'') des preuves de congruence de premi‘ere partie.
Motscl’es : transition ’etiquet’ee, congruence structurelle, bisimulation, action calculi,
somme amalgam’ee
Synthesising Labelled Transitions and Operational Congruences in Reactive Systems, Part 2 1
Contents
1 Introduction 2
1.1 Motivation and goals . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2
1.2 Outline . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2
1.3 Acknowledgements . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3
2 Recapitulation of key definitions and theorems 5
3 Sliding IPO squares 8
3.1 Introduction and motivation . . . . . . . . . . . . . . . . . . . . . . . . . . . 8
3.2 Properties of A . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9
3.3 Construction of “
C . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
3.4 Operations on “
C . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
3.5 Construction of C . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
3.6 Construction of F . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
3.7 Replacing precategories with bicategories . . . . . . . . . . . . . . . . . . . 19
4 Action graph contexts 22
4.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22
4.2 Action calculi reviewed . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23
4.3 Examples and a problem . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25
4.4 Closed shallow action graphs . . . . . . . . . . . . . . . . . . . . . . . . . . 30
4.5 The wellsupported precategory AIxt of arities and raw contexts . . . . . 32
4.6 Constructing a functorial reactive system . . . . . . . . . . . . . . . . . . . 37
5 Conclusions and future work 40
Bibliography 46
RR n° 4395
2 J.J. Leifer
1 Introduction
1.1 Motivation and goals
This paper is the second in a series of two. I rely on its companion [Lei02], referred to
as Part 1 throughout, to motivate the central problem addressed by the series, namely:
how to synthesise labelled transitions for reactive systems and how to prove congruence
results for operational equivalences and preorders defined above those transitions. Thus,
the present paper uses Part 1 as a base, sacrificing selfcontainedness in order to avoid
repetition, though the key definitions are recapitulated here in Section 2.
The purpose of this paper is to twofold:
(i) to show that the hypotheses required of functorial reactive systems from Part 1 are
indeed satisfied for functors of a general form;
(ii) to illustrate an example of a functorial reactive system, namely action graphs, which
satisfy the RPO (relative pushout) hypothesis required in the proofs of congruence
from Part 1.
Of the two, goal (i) is more critical since the techniques employed for generating the
functor and proving the relevant properties are widely applicable. The argument does not
fit neatly within standard category theory, though, and requires the use of precategories
 which have a partial composition operator, unlike the total one of categories. It seems
possible that this work could be recast by replacing precategories with bicategories. One
of the primary reasons for presenting (i) in detail is to expose this potential recasting as
a challenge to the (enriched) category theory community. This question is discussed in
detail in Subsection 3.7.
For goal (ii), I introduce action graphs (a subclass of Milner's action calculi). The
main motivation for defining these is to show that the properties required of them in the
definition of a functorial reactive system follow smoothly from the work on goal (i). The
proof of the existence of RPOs, by contrast, requires highly combinatorial manipulations
of graph contexts and embeddings. For the sake of brevity, I omit this proof, pointing
instead to its full treatment in my Ph.D. [Lei01b].
1.2 Outline
The outline of this paper is as follows:
Section 2: This section recapitulates the key definitions from Part 1 needed in the present
paper.
INRIA
Synthesising Labelled Transitions and Operational Congruences in Reactive Systems, Part 2 3
Section 3: As mentioned above in (i) the proofs of congruence in Part 1 rest on some
hypotheses about the functor F . The most important one of these is that F allows
an IPO square upstairs to ``slide'' so as to leave the Fimage of the square invariant.
This section eases the burden of showing that these hypotheses are satisfied by giving
an abstract way of generating a functor satisfying them from simpler data. The
section starts by assuming the existence of a wellsupported precategory A, which
is like a category but lacks some arrow compositions and has extra structure for
extracting and renaming the support of an arrow. The motivation for this comes
from the raw contexts in Section 4 for which composition of two contexts is not
defined unless their node sets (supports) intersect trivially. I derive from A two
categories and a functor between them. The upstairs category is formed from A
by adding extra information to the objects, so as to make composition total. The
downstairs category is formed by quotienting away the supports. The functor F
maps arrows to their quotient equivalence classes. By reasoning abstractly, I show
that F allows IPO sliding and has all of the other properties required of functorial
reactive systems (see Definition 2.5). By instantiating these results, as in Section 4
for example, one gets ``for free'' a functorial reactive system provided that one starts
with a wellsupported precategory, a light burden.
Section 4: This section gives a significant example of a family of functorial reactive sys
tems. The contexts are derived from closed, shallow action graphs, those with no
nesting and no free names. Their graph structure includes forked and discarded
wiring connecting interfaces on each node and on the inside and outside of each
context. By instantiating the results of the preceding section, we construct a func
torial reactive system with the following properties: the downstairs category does
not distinguishes the occurrences of controls, as desired when modelling agents of
a process calculus; the upstairs one does distinguish them, thus providing su#cient
RPOs.
Section 5: The section sets out the main open questions, whose solutions are critical to
the application of this work to a wide variety of process calculi.
1.3 Acknowledgements
I thank Robin Milner (my Ph.D. supervisor) for his inspiration and warmth. I learned
more about the ways of doing research and the style of presenting it from him than anyone
else. I had extensive and valuable discussions with Luca Cattani and Peter Sewell. Many
colleagues provided suggestions, for which I am grateful: Tony Hoare, Martin Hyland,
Philippa Gardner, Michael Norrish, Andy Pitts, John Power, Edmund Robinson, and
Lucian Wischik
RR n° 4395
4 J.J. Leifer
I was supported by the following funding sources: EPSRC Research Grant GR/L62290
and an NSF Graduate Research Fellowship.
INRIA
Synthesising Labelled Transitions and Operational Congruences in Reactive Systems, Part 2 5
m
f 0
f 1 g 0
g 1
1(1)
m
f 0
f 1 g 0
g 1
h 0
h 1 h
1(2)
m
f 0
f 1 g 0
g 1
h 0
h 1
h
h #
h # 0
h # 1
kk
1(3)
Figure 1: Construction of an RPO
2 Recapitulation of key definitions and theorems
This section recalls the key definitions and theorems from Part 1 needed in this paper.
The original motivation and explanation of each is not repeated, but can be found by
following each pointer into Part 1.
Definition 2.1 (RPO  see Definition 2.4 in Part 1) In any category C, consider
a commuting square (Figure 1(1)) consisting of g 0 f 0 = g 1 f 1 . An RPO is a triple h 0 , h 1 , h
satisfying two properties:
commutation: h 0 f 0 = h 1 f 1 and hh i = g i for i = 0, 1 (Figure 1(2));
universality: for any h # 0 , h # 1 , h # satisfying h # 0 f 0 = h # 1 f 1 and h # h # i = g i for i = 0, 1, there exists
a unique mediating arrow k such that h # k = h and kh i = h # i
(Figure 1(3)). #
Terminology: A triple, such as h # 0 , h # 1 , h # given above, that satisfies the commutation
property, i.e. h # 0 f 0 = h # 1 f 1 and h # h # i
= g i for i = 0, 1, is often called a candidate. Thus an
RPO triple is a candidate for which there is a unique mediating arrow from it to any other
candidate.
Definition 2.2 (IPO  see Definition 2.5 in Part 1) The commuting square in
Figure 1(1) is an IPO if the triple g 0 , g 1 , id m is an RPO. #
#
#
#
#
m
m #
f 0
f 1 g 0
g 1 2
Proposition 2.3 (IPOs in a full subcategory  see Proposition 2.10
in Part 1) Let m,m # be objects of C and let C # be a full subcategory of C
satisfying the following property:
obj C # # {n # obj C / #h # C(m,n) & #h # # C(n, m # )} .
Suppose the square in Figure 2 commutes, where f i , g i # C # for i = 0, 1. Then the square
is an IPO in C i# it is an IPO in C # . #
RR n° 4395
6 J.J. Leifer
Definition 2.4 (reactive system see Definition 2.1 in Part 1) A reactive system
consists of a category C with added structure. We let m,n range over objects. C has the
following extra components:
ˆ a distinguished object 0 (not necessarily initial);
ˆ a set of reaction rules called Reacts # # m#objC C(0, m) 2 , a relation containing pairs
of agents with common codomain;
ˆ a subcategory D of C, whose arrows are the reactive contexts, with the property
that D 1 D 0 # D implies D 1 , D 0 # D. #
Notation: a, b # C range over arrows with domain 0, called agents, and C, D,F # C
range over arbitrary arrows (contexts).
Definition 2.5 (functorial reactive system see Definition 3.1 in Part 1) Let C
be a reactive system. A functorial reactive system over C consists of a functor F : “
C C
which maps a distinguished object # # obj “
C to 0 (the distinguished object of C) and
which satisfies the following properties.
F lifts agents: for any a : 0 m there exists a : # m such that F(a) = a.
F creates isos: if F(C) is an iso then C is an iso.
F creates compositions: if F(C) = C 1 C 0 , there exist C 0 , C 1 # “
C such that C = C 1 C 0 and
F(C i ) = C i for i = 0, 1.
#
#
#
#
C
F # F
C # 3
C 0
F # 0 F 0
C # 0
4
F allows IPO sliding: for any IPO square as in Figure 3 and any
arrow F # 0 with F(F # 0 ) = F(F # ) there exist C 0 , C # 0 , F 0 forming an
IPO square as in Figure 4 with
F(C 0 ) = F(C) F(C # 0 ) = F(C # ) F(F 0 ) = F(F) . #
Notation: Uppercase teletype characters denote arrows in “
C and lowercase teletype
characters (a, l, . . .) denote arrows with domain # in “
C. The F images of these are agents in
C. The special domain requirement of a, l, . . . is left tacit throughout: thus (#l # “
C. . . .)
means (#l # “
C. Dom l = # & . . .).
#
#
#
#
a
l F
D 5
Definition 2.6 (F has all redexRPOs see Definition 3.4 in Part 1)
A functorial reactive system F : “
C C has all redexRPOs if any square, such
as in Figure 5, has an RPO, provided that F(D) # D and that there exists
r # C such that (F(l), r) # Reacts. #
INRIA
Synthesising Labelled Transitions and Operational Congruences in Reactive Systems, Part 2 7
Proposition 2.7 (characterisation of  see Proposition 3.2 in Part 1) a
a # i# there exist a, l, D # “
C and r # C such that a = Dl and
a # = F(D)r F(D) # D (F(l), r) # Reacts
F(a) = a .
#
RR n° 4395
8 J.J. Leifer
3 Sliding IPO squares
3.1 Introduction and motivation
Part 1 presents a series of congruence proofs, each one for a di#erent operational equiv
alence. The theme throughout is the separation of ``reactive system'' into two categories
with a functor F between them: the domain of F , i.e. “
C, is a category in which RPOs
and IPOs exist; the codomain of F , i.e. C, is a category containing (i) the agents that
perform reactions and labelled transitions and (ii) the agent contexts that serve as the
labels and specify the closure condition for congruence. This separation is useful because
the category for which we prove a congruence result is typically not one in which RPOs
exist, as I show in the next section when considering categories of graph contexts. Thus
functorial reactive systems are a powerful generalisation of reactive systems.
This separation imposes a burden, though, in the form of the list of requirements given
in Definition 2.5, i.e.: F lifts agents, creates isos, creates compositions, and allows IPO
sliding. The motivation for the current section is to alleviate this burden by showing that
all of these properties follow directly if we construct “
C, C, and F from a precategory A in
a particular way. The assumption is that A is easier to construct than the others. (The
next section gives a concrete instance of A.)
Precategories are defined formally below. By way of motivation, though, let us look
informally at an example we have in mind when deriving F : “
C C from A. A precate
gory is just like a category but has a composition operation that is partial, i.e. not always
defined. For example, consider a precategory A of ``raw contexts''. For the purpose of this
example, take the objects to be natural numbers (representing the number of ports in an
interface). Take the arrows m n to be just like normal graphs but with some added
structure, namely an inner and outer interface. An arrow is thus a doughnutshaped graph
consisting of a set of nodes (which we call the support) and an arc relation; the arcs link
nodes to one another and to the interface ports; m (ordered) interface ports sit on the
inside ``hole'' and n (ordered ones) on the outside. (These are simpler than the graph con
texts that appear in the next section.) Composition consists of placing one raw context
inside the hole of another and joining together common ports. To see how this works,
consider arrows A 0 : 1 2 and A 1 : 2 3:
A 1 =
v 1 v 2
A 0 =
v 0
INRIA
Synthesising Labelled Transitions and Operational Congruences in Reactive Systems, Part 2 9
Then their composition, which we denote A 1 # A 0 : 1 3, is as follows:
A 1 # A 0 =
v 2
v 0
v 1
This example reveals why composition is partial in A. If we form A # 0 from A 0 by renaming
the node v 0 by v 2 then the supports of A # 0 and A 1 are not disjoint. Thus the composition
A 1 # A # 0 is undefined since there is no clear choice for the support of the composite.
There are several possible ways of building a true category (i.e. with a total composition
relation) from the data provided by A. Two possible ways are as follows:
ˆ We can construct a category “
C whose objects are pairs (m, U) where m is an object
of A (in this case a natural number) and U is a set. An arrow (m 0 , U 0 ) (m 1 , U 1 )
consists of an Aarrow A : m 0 m 1 for which U 0 # U 1 and U 1 \ U 0 is equal to
the support of A. Thus we can incorporate A 1 (given above) into many possible
arrows in “
C, e.g. (2, #) A 1 (3, {v 1 , v 2 }) and (2, {w}) A 1 (3, {w, v 1 , v 2 }). As a result
composition is always welldefined: if (m i , U i ) A i (m i+1 , U i+1 ) are “
Carrows for i =
0, 1 then the supports of A 0 and A 1 are disjoint.
ˆ We can construct a category C, whose objects are the objects of A and whose arrows
are #equivalence classes of Aarrows. Two Aarrows are #equivalent i# they are
graphisomorphic, i.e. have (potentially) di#erent supports but look like the same
graphs. Composition for this category is also welldefined since it is always possible
when composing arrows to find representatives of each equivalence class with disjoint
supports.
One might consider a third way, i.e. to use the arrows of A but rename the supports
so as to make them disjoint when composing arrows; but this yields a bicategory, since
composition is not associative. I consider this possibility in detail in Subsection 3.7.
What is the relationship between “
C and C? There is a simple functor F which discards
the set component of each “
Cobject (i.e. F : (m, U) ## m) and maps each arrow to its
#equivalence class. As we see later in this section, this functor has all of the desired
properties listed earlier, e.g. F allows IPO sliding.
The rest of this section repeats the above constructions in full formality.
3.2 Properties of A
First we formally define a precategory (see [MSS00]):
RR n° 4395
10 J.J. Leifer
Definition 3.1 (precategory) A precategory A consists of similar data to that of a
category: a collection of objects m, n, . . .; a collection of arrows A(m,m # ) between objects
m and m # ; an identity arrow id m # A(m,m) for all m; and a partial composition operation,
which we write here as # : A(m 1 , m 2 ) × A(m 0 , m 1 ) # A(m 0 , m 2 ) on arrows. Identity:
composition with an identity arrow is always welldefined, i.e. for all A : m 0 m 1 , we
have that id m 1 # A = A = A # id m 0
and both compositions are defined. Associativity: if
A 2 # A 1 and A 1 # A 0 are defined then either both A 2 # (A 1 # A 0 ) and (A 2 # A 1 ) # A 0 are
undefined or both are defined and equal. #
Next we define some special properties of a precategory. These properties form a
specification (used in Section 4) which any precategory is required to satisfy in order to
make use of the constructions and propositions of this section.
Definition 3.2 (wellsupported precategory) A is a wellsupported precategory i# it
is a precategory and it satisfies the following properties:
ˆ A has a support function · that maps an arrow to a set such that A 1 # A 0 is defined
i# A 1  # A 0  = # and DomA 1 = CodA 0 . The support function satisfies additionally
two axioms:
A 1 # A 0  = A 1  # A 0  (provided A 1 # A 0 is defined) Suppcomp
id m  = # . Suppid
ˆ For any arrow A # A(m 0 , m 1 ) and any injective map # for which Dom # # A, there
exists an arrow # # A # A(m 0 , m 1 ), which is called the support translation by # of A,
where:
# # id m = id m Transidr
# # (A 1 # A 0 ) = # # A 1 # # # A 0 Transcompr
Id A # A = A Transidl
(# 1 # # 0 ) # A = # 1 # (# 0 # A) Transcompl
# 0 # A = # 1 # A implies # 0 # A = # 1 # A Transres
# # A = #A . Transsupp
A note about Transcompr: Since # is injective, Transsupp implies that the
LHS is defined i# the RHS is defined. (These axioms are similar to those of Honda's
Rooted PSets [Hon00], though his application concerns free names and renaming.)
#
INRIA
Synthesising Labelled Transitions and Operational Congruences in Reactive Systems, Part 2 11
3.3 Construction of “
C
We now turn to problem of building a genuine category from a wellsupported precategory
A. The idea is to enrich the object structure with enough data so that composition is
always defined. This construction is captured in the following definition:
Definition 3.3 (track) Given a wellsupported precategory A, the track of A is a
category “
C. An object of “
C is a profile: a pair (m, U) where m is an object of A and U
is a set. We let p range over profiles and adopt the firm convention that the components
of a profile p are always written (m, U) with suitable decoration, e.g. p # = (m # , U # ) and
p i = (m i , U i ). An arrow p 0
A p 1 consists of an arrow A # A(m 0 , m 1 ) such that U 0 # U 1
and A = U 1 \ U 0 . We always include the profiles when referring to an arrow of “
C since
di#erent “
Carrows can be constructed from the same Aarrow, each with di#erent profiles.
The identities of “
C are defined by id p “
= p id m p. Composition is defined in terms of the
underlying composition in A:
p 0
A 0 p 1
A 1 p 2 “
= p 0
A 1 #A 0 p 2 . #
Proposition 3.4 If “
C is the track of A then “
C is a category.
Proof
Composition is welldefined: if p i
A i p i+1 are arrows for i = 0, 1, then A 1  # A 0  =
(U 2 \ U 1 ) # (U 1 \ U 0 ) = #, so A 1 # A 0 is defined. Furthermore, U 0 # U 1 # U 2 and
U 2 \ U 0 = (U 2 \ U 1 ) # (U 1 \ U 0 ) = A 1  # A 0  = Suppcomp
A 1 # A 0  ,
so p 0
A 1 #A 0 p 2 is an arrow of “
C as desired.
The identity arrows are welldefined: By Suppid, id m  = #, so for any p = (m, U ),
p id m p is an arrow of “
C.
Composition is associative and respects identities: Immediate because these same
properties hold in A. #
3.4 Operations on “
C
In order to motivate the following results, let us recall the intuitions about the functor F
(defined formally later): F maps p 0
A p 1 to an isomorphism equivalence class of A and
throws away the set data contained in the profiles p 0 , p 1 . To prove that F allows IPO
sliding, we require two things. (i) We have to understand how two “
Carrows are related
when they have the same F image, i.e. F(p 0
A p 1 ) = F(p # 0
A # p # 1 ). (ii) From the first piece
of information, we have to slide similarly an IPO square whose left leg is p 0
A p 1 to one
whose left leg is p # 0
A # p # 1
.
RR n° 4395
12 J.J. Leifer
For (i), it is clear that we can perform some profile translation (defined precisely later)
on p 0
A p 1 to replace the set components of p 0 and p 1 and then perform a support transla
tion on the resulting arrow to arrive at p # 0
A # p # 1 . If these two operations (profile translation
and support translation) are iso functors (and thus preserve categorical constructions) then
we can accomplish (ii).
These two operations are not in fact iso functors on the whole of “
C but they are on
certain convex subcategories, as defined next. Fortunately, the subcategories in question
are rich enough to be proxies for “
C with respect to IPO squares, as shown in the result
immediately following the definition:
Definition 3.5 (convex subcategories of “
C) For any sets U 0 # U 1 , we write “
CU 0 ,U 1
for the convex subcategory of “
C w.r.t. U 0 , U 1 , namely the full subcategory of “
C formed by
taking only those profiles (m, U) for which U 0 # U # U 1 . #
#
#
#
#
p p 0
p 1 p 2
A 0
A 1 B 0
B 1
6
Proposition 3.6 Suppose that Figure 6 commutes in “
C. Then it is an
IPO in “
C i# it is an IPO in “
CU,U 2
.
Proof For any pair of arrows p C p # C # p 2 , we have that U # U # # U 2 ,
so p # # obj “
CU,U 2
(Definition 3.5) hence “
CU,U 2
satisfies the hypothesis of Proposition 2.3,
whence the result follows. #
Now we now define precisely profile translation and establish that it is an iso functor:
Proposition 3.7 (profile translation is an iso functor) If W 1 = W 0 #W and W #
1 =
W #
0 # W then the following operation, called profile translation, induces an isomorphism
of categories H : “
CW 0 ,W 1
“
CW #
0 ,W #
1
,
H : (m, W 0 # V ) ## (m, W #
0 # V ) for V # W
H : (p 0
A p 1 ) ## H(p 0 ) A
H(p 1 ) .
Proof
H is welldefined on arrows: Suppose that (p 0
A p 1 ) # “
CW 0 ,W 1
where U i = W 0 # V i ,
i = 0, 1 for some V 0 # V 1 # W . Now, W #
0 # V 0 # W #
0 # V 1 and
(W #
0 # V 1 ) \ (W #
0 # V 0 ) = V 1 \ V 0 = A
so (H(p 0 ) A
H(p 1 )) # “
CW #
0 ,W #
1
as desired.
H is a functor: Consider the action of H on identities:
H(id p ) = H(p id m p) = H(p) id m
H(p) = id H(p)
and on compositions:
H(p 0
A 0 p 1
A 1 p 2 ) = H(p 0
A 1 #A 0 p 2 )
= H(p 0 ) A 1 #A 0
H(p 2 )
= H(p 0 ) A 1
H(p 1 ) A 0
H(p 2 )
INRIA
Synthesising Labelled Transitions and Operational Congruences in Reactive Systems, Part 2 13
H is an isomorphism of categories: By symmetry, the map H # : “
CW #
0 ,W #
1
“
CW 0 ,W 1
defined by
H # : (m, W #
0 # V ) ## (m, W 0 # V ) for V # W
H # : (p 0
A p 1 ) ## H # (p 0 ) A
H # (p 1 ) .
is also a functor and clearly inverts H, as desired. #
Finally we lift the support translation operation from A to “
C in a straightforward way.
This definition induces a functor on convex subcategories of “
C
Proposition 3.8 (support translation is an iso functor) Given W 0 # W 1 and an
injection # with Dom # # W 1 , the following operation, called support translation, induces
an isomorphism of categories # # (·) : “
CW 0 ,W 1
“
C#W 0 ,#W 1
,
# # (m, U) “
= (m, #U)
# # (p 0
A p 1 ) “
= # # p 0
# # A
# # p 1 ,
where # # A is the support translation by # of A in A.
Proof
# # (·) is welldefined on arrows: Suppose that (p 0
A p 1 ) # “
CW 0 ,W 1
. Then W 0 # U 0 #
U 1 # W 1 # Dom #. Thus #U 0 # #U 1 and
#U 1 \ #U 0 = # injective #(U 1 \ U 0 ) = #A = Transsupp
# # A ,
so # # (·) maps an arrow to an arrow.
# # (·) is a functor: By Transidr and Transcompr, # # (·) preserves identities and
compositions, so is a functor.
# # (·) is an iso functor: Note that # has an inverse # 1 : Im # # Dom #. Furthermore,
# 1 # (·) : “
C#W 0 ,#W 1
“
CW 0 ,W 1
is a functor for the same reasons (given above) that # # (·) is. By Transcomp
l and Transidl, the functors # # (·) and # 1 # (·) invert each other, so # # (·) is an
isomorphism of categories, as required. #
3.5 Construction of C
We now turn to the construction of C, which was described informally in Subsection 3.1.
Recall that the arrows of C are equivalence classes of arrows of A. In this subsection we
make precise the underlying equivalence relation and the construction of C and verify that
C is a welldefined category.
RR n° 4395
14 J.J. Leifer
Definition 3.9 (#equivalence for A) Given two arrows A, A # : m 0 m 1 in A, we say
that they are #equivalent, written A # A # , i# there exists a bijection # : A ## A #  such
that # # A = A # . By Transidl and Transcompl, # is an equivalence relation. #
Now the construction of C is straightforward:
Definition 3.10 (support quotient) Given a wellsupported precategory A, the sup
port quotient of A is a category C. The objects of C are the objects of A. The arrows
m 0 m 1 of C are #equivalence classes of arrows in A:
C(m 0 , m 1 ) “
= {[A] # / A # A(m 0 , m 1 )} .
Identities: id m # C(m,m) “
= [id m ] # . Composition: if A 1 # A 0 is defined in A then
[A 1 ] # [A 0 ] # “
= [A 1 # A 0 ] # . #
This definition yields a welldefined category:
Proposition 3.11 If C is the support quotient of A then C is a category.
Proof
Composition is total: Consider any two arrows in C such as [A i ] # : m i m i+1 for
i = 0, 1. Let W be a fresh set in bijection with A 1 , as witnessed by # : A 1  ## W .
Then # # A 1 # A 0 is defined since # # A 1  # A 0  = Transsupp W # A 0  = #; thus
[A 1 ] # [A 0 ] # = [# # A 1 ] # [A 0 ] # = [# # A 1 # A 0 ] # ,
as desired.
Composition is welldefined: Let [A i ] # = [A # i ] # for i = 0, 1 with both A 1 # A 0 and A # 1 #
A # 0 defined. Claim: [A 1 ] # [A 0 ] # = [A # 1 ] # [A # 0 ] # . By hypothesis, there exist bijections
# i : A i  ## A # i  such that A # i = # i # A i for i = 0, 1. Since A 1  # A 0  = # and
A # 1  # A # 0  = #, we can define # “
= # 0 # # 1 , a union of bijections with disjoint
domains and disjoint codomains. Now,
# # (A 1 # A 0 ) = Transcompr # # A 1 # # # A 0 = Transres # 1 # A 1 # # 0 # A 0 = A # 1 # A # 0
so
[A 1 ] # [A 0 ] # = [A 1 # A 0 ] # = [A # 1 # A # 0 ] # = [A # 1 ] # [A # 0 ] # ,
as desired.
Composition is associative: Follows from the associativity of the underlying composi
tion in A.
Composition respects identities: Follows from the fact that composition respects
identities in A. #
INRIA
Synthesising Labelled Transitions and Operational Congruences in Reactive Systems, Part 2 15
3.6 Construction of F
In this final subsection we define a functor F from “
C (the track of A) to C (the support
quotient of A). We then verify that F has all the required properties, i.e.: F lifts agents,
creates isos, creates compositions, and allows IPO sliding. For the first we verify a stronger
property defined below, namely F lifts arrows by their domain. The reason for this choice
is that there is no postulated distinguished object in A or C corresponding to the 0
of a functorial reactive system (see Definition 2.5), which is required when defining the
property ``F lifts agents''. However, the stronger property ``F lifts arrows by their domain''
is welldefined.
Definition 3.12 (supportquotienting functor) Let A be a wellsupported precat
egory and “
C and C be as in Definition 3.3 and Definition 3.10. Then we define a map
F : “
C C called the supportquotienting functor :
F : (m, U) ## m
F : (p 0
A p 1 ) ## F(p 0 ) [A]#
F(p 1 ) . #
Lemma 3.13 F is a functor.
Proof Observe the action on identities:
F(id p ) = F(p id m p) = [id m ] # = id m
and on compositions:
F(p 0
A 0 p 1
A 1 p 2 ) = F(p 0
A 1 #A 0 p 2 )
= [A 1 # A 0 ] #
= [A 1 ] # [A 0 ] #
= F(p 1
A 1 p 2 ) F(p 0
A 0 p 1 ) #
Now we prove all the easy properties of F :
Theorem 3.14 Let F : “
C C be the supportquotienting functor constructed from A.
Then:
ˆ F lifts arrows by their domain: if F(p 0 ) = Dom [A] # then there exists p 0
B p 1 such
that F(p 0
B p 1 ) = [A] # .
ˆ F creates isos: if F(p 0
A p 1 ) is an iso then p 0
A p 1 is an iso.
ˆ F creates compositions: if
F(p # 0
B p # 2 ) = [A 1 ] # [A 0 ] #
RR n° 4395
16 J.J. Leifer
then there exist “
Carrows p # i
B i p # i+1 with
F(p # i
B i p # i+1 ) = [A i ] # for i = 0, 1 (1)
p # 0
B p # 2 = p # 0
B 0 p # 1
B 1 p # 2 (2)
Proof
F lifts arrows by their domain: Suppose [A] # : (m 0 , n 0 ) (m 1 , n 1 ), thus
A : (m 0 , n 0 ) (m 1 , n 1 ) in A. Let W be a fresh set in bijection with A, as
witnessed by # : A ## W . Then p 0
# # A
p 1 is an arrow in “
C, where U 1 “
= U 0 # W .
Furthermore F(p 0
# # A
p 1 ) = [A] # as desired.
F creates isos: Suppose F(p 0
A p 1 ) is an iso, i.e. there exists an Aarrow A # : m 1 m 0
such that:
[A # ] # [A] # = id m 0
= [id m 0
] #
[A] # [A # ] # = id m 1
= [id m 1
] #
Without loss of generality, assume that A # A #  = #. Then A # # A # id m 0
and
A # A # # id m 1
. By Suppid and Transidr, A # # A = id m 0
and A # A # = id m 1
. By
Suppcomp, A = A #  = #. Thus U 1 = U 0 and p 1
A # p 0 is a “
Carrow. Moreover,
p 0
A p 1
A # p 0 = p 0
A # #A p 0 = p 0
id m 0 p 0 = id p 0
and symmetrically. Thus p 0
A p 1 is an iso in “
C as desired.
F creates compositions: Without loss of generality, assume that A 1  # A 0  = #. Then
there exist p 0 , p 1 , p 2 such that p i
A i p i+1 are arrows in “
C for i = 0, 1. By the
definition of F , there exists a bijection # : A 1  # A 0  ## B such that # # (A 1 #
A 0 ) = B; moreover m 0 = m # 0
and m 2 = m # 2
. Let B i “
= # # A i for i = 0, 1. Let
(m # 1 , U #
1 ) “
= (m 1 , U #
0 # B 0 ), thus defining p # 1 . We claim that p # i
B i p # i+1 are arrows in
“
C for i = 0, 1; there are three things that we need to check:
U #
0 # U #
0 # B 0  # U #
0 # B = U #
2
U #
1 \ U #
0 = B 0 
U #
2 \ U #
1 = (U #
0 # B) \ (U #
0 # B 0 ) = B \ B 0  = B 1  .
Now, B 1 # B 0 = B by Transcompr, from which (2) follows. Also, by Transres,
B i # A i for i = 0, 1, from which (1) follows.
#
INRIA
Synthesising Labelled Transitions and Operational Congruences in Reactive Systems, Part 2 17
An aside on the condition ``F creates compositions'': This looks tantalisingly close
to the Conduch’e fibration property [Con72, Joh99, BF00], especially if one says that two
decompositions in “
C are equivalent if one is the result of a support translation of the other.
Perhaps there is some 2category version of the Conduch’e property which works exactly
if one thinks of “
C as a 2category with support translations as 2cells. Let us now return
to the main flow of the argument.
Finally, we prove the key property, namely that F allows IPO sliding. The proof
follows the outline given in Subsection 3.4. We start with two “
Carrows with the same
image under F , namely F(p A 1 p 1 ) = F(p # A # 1 p # 1 ). The first arrow is the left leg of an
IPO square in “
C. This square is also an IPO in “
CU,U 2
, the convex subcategory w.r.t. U, U 2
(Definition 3.5), where U # U 2 are the sets in, respectively, the upperleft and lowerright
profiles of the square. We isomorphically transform this subcategory by profile translation
and then support translation, gaining a new square that has three properties: it has the
same image under F as the original; its left leg is p # A # 1 p # 1 ; it is an IPO in a convex
subcategory, so is an IPO in “
C.
Before looking at the technical details, it is useful to consider a concrete case of sliding.
Because we have not formally defined the graph contexts referred to at the beginning of
this section, it is impossible to be precise about which commuting squares are IPOs and
which are not. Nonetheless, the activity of ``sliding'' is relevant for all commuting squares,
whether or not they are IPOs.
Let us consider a category of graph contexts formed as the track (Definition 3.3) of
the precategory or raw contexts informally defined in Subsection 3.1. The arrows of this
category are just like the raw contexts (doughnutshaped graphs with an inner and outer
interface) but with profiles (Definition 3.3) rather than just natural numbers as objects.
Consider the square in Figure 7(1). Its left leg has the same F image as the left leg
of the square in Figure 7(3): the two graph contexts look essentially the same, the only
di#erence being the supports. With a profile translation, we can replace the singleton set
{u} in the topleft corner of Figure 7(1) with a fresh 2element set {u ## 0 , u ## 1 }, as shown in
Figure 7(2). The freshness is essential to prevent clashes with the other nodes present in
the square, namely v 0 , v 1 . Now, if # is defined as follows:
# : v i ## v # i i = 1, 2
# : u ## i ## u # i i = 1, 2
then the support translation by # of Figure 7(2) yields Figure 7(3), as desired. Since
the passage from Figure 7(1) to Figure 7(2) and then to Figure 7(3) was e#ected by iso
functors, all the universal properties of Figure 7(1) (e.g. being an IPO) hold of Figure 7(3)
too.
RR n° 4395
18 J.J. Leifer
v 1
v 0
v 1
(2, {u})
(2, {v0 , v1 , u}) (0, {v0 , v1 , u})
(4, {v0 , u})
v 0
7(1) A commuting square before sliding
v1
v0
v1
(2, {u ## 0 , u ## 1 })
(2, {v0 , v1 , u ## 0 , u ## 1 }) (0, {v0 , v1 , u ## 0 , u ## 1 })
(4, {v0 , u ## 0 , u ## 1 })
v0
7(2) First we apply profile translation . . .
v # 0 v #
1
v # 0
v # 1
(4, {v # 0 , u # 0 , u # 1 })
(2, {u # 0 , u # 1 })
(2, {v # 0 , v # 1 , u # 0 , u # 1 }) (0, {v # 0 , v # 1 , u # 0 , u # 1 })
7(3) . . . and then support translation by #
Figure 7: Sliding
INRIA
Synthesising Labelled Transitions and Operational Congruences in Reactive Systems, Part 2 19
#
#
#
#
p p 0
p 1 p 2
A 0
A 1 B 0
B 1
8
Theorem 3.15 (F allows IPO sliding) Let F : “
C C be the
supportquotienting functor constructed from A. Then F allows IPO slid
ing (Definition 2.5).
Proof Consider any IPO square in “
C, as in Figure 8, and any arrow p # A # 1 p # 1 with
F(p # A # 1 p # 1 ) = F(p A 1 p 1 ); thus A # 1 = # # A 1 for some bijection # : A 1  A # 1  and U #
1 =
U # # #A 1 .
#
#
#
#
H(p) H(p 0 )
H(p 1 ) H(p 2 )
A 0
A 1 B 0
B 1
9
By Proposition 3.6, Figure 8 is an IPO in “
CU,U 2
. Let U ## be a
fresh set in bijection with U # , as witnessed by µ : U ## ## U # . Let
U ##
2 “
= U ## #(U 2 \U ). Then U 2 \U = U ##
2 \U ## so by Proposition 3.7, there
is a profile translation H : “
CU,U 2
“
C U ## ,U ##
2
which is an iso functor and
whose action on profiles is:
H : (m, U # V ) ## (m, U ## # V ) for V # U 2 \ U
and whose action on arrows leaves the underlying Aarrow component unchanged. Since
isomorphisms of categories preserve universal constructions, Figure 9 is an IPO in “
C U ## ,U ## 2
and has the same image under F as Figure 8 does.
#
#
#
#
# # H(p) # # H(p 0 )
# # H(p 1 ) # # H(p 2 )
# # A 0
# # A 1 # # B 0
# # B 1 10
Let W be a fresh set in bijection with B 1 , as witnessed
by # : B 1  ## W . Let # “
= µ # # # #, a union of bijections
with mutually disjoint domains and codomains. Also Dom # =
U ## # A 1  # B 1  = U ##
2 . Because # is bijective, Proposition 3.8 im
plies that there is a support translation # # (·) : “
C U ## ,U ##
2
“
C #U ## ,#U ##
2
which is an iso functor. Iso functors preserve universal constructions, so Figure 10 is a
IPO in “
C #U ## ,#U ##
2
and has the same image under F . By Proposition 3.6, this square is an
IPO in “
C. Moreover,
# # (H(p) A 1
H(p 1 )) = µ # H(p) # # A 1 (µ # #) # H(p 1 ) = p # A # 1 p # 1
as desired. #
3.7 Replacing precategories with bicategories
As explained in Section 1, one of the main motivations for presenting the sliding arguments
of this section is to advertise them to the (enriched) category theory community. The
reason is that precategories are probably not optimal: it would be worthwhile to rework
these arguments, replacing precategories with something more ``natural'' from enriched
category theory, e.g. bicategories. Such a change might have sidee#ects on the results of
Part 1 as well, which are discussed later in this subsection.
Recall from Subsection 3.1 that the composition operation # of A is partial, not total,
since it requires the supports of the operands to be disjoint: A 1 # A 0 is defined i# A 1  #
RR n° 4395
20 J.J. Leifer
A 0  = # and DomA 1 = CodA 0 (Definition 3.2). Composition can be made total by
forcing the supports of the operands to be disjoint, i.e. defining a new composition # for
which
A 1 # A 0 = (# 1 # A 1 ) # (# 0 # A 0 )
where # j : A j  A 1  + A 0  is the jth injection into the coproduct of the supports in
Set (the category of sets and functions), for j = 0, 1. This new definition of composition
is total. It is not strictly associative, nor does it have strict identities  which is exactly
the kind of situation that bicategories cater for! Let the 2cells from A : m n to
A # : m n be the support translations # : A A #  such that # # A = A # . All of
these 2cells are isos. Moreover, there are 2cells mediating between the compositions
A 2 # (A 1 # A 0 ) and (A 2 # A 1 ) # A 0 as generated from the underlying isos in Set between
the coproducts A 2  + (A 1  + A 0 ) and (A 2  + A 1 ) + A 0 . It remains to be checked that
all the bicategory coherence requirements are satisfied, but it seems likely since here they
rely on the underlying properties of a coproduct, which is a universal construction.
Having indicated how to derive a bicategory from A, it may be possible to go a step
further, namely to dispense with A and “
C altogether and to postulate the existence of a
bicategory B whose 2cells are all isos. Since the 2cells are isos, the property ``the 1cells
A, A # have a 2cell between them'' is an equivalence relation on the 1cells of B. We can
thereby construct the ``support quotient'' (cf. Definition 3.10) of B by quotienting out the
2cells, thus obtaining a category E. This quotienting is an enriched functor G : B E.
Before looking at the advantages gained by giving this functor a central role, let us
consider the price to be paid. First, the congruence results of Part 1 depend on the
existence of RPOs in the ``upstairs'' category “
C of a functorial reactive system F : “
C C.
The domain of the functor G is instead a bicategory, thus necessitating a bicategorical
version of RPOs, which we might call 2RPOs. One possible definition for 2RPOs (of
which Peter Sewell has made a preliminary study) is to replace in Definition 2.1 each
commuting square and triangle by the relevant 2cell, and their juxtaposition by horizontal
and vertical 2cell compositions. This change would have knockon e#ects in the proofs
of congruence which would have to be rewritten accordingly. Also, the existence proofs of
RPOs for concrete systems would have to be redone to provide 2RPOs. Neither change
seems daunting. The potential reward of using bicategories is the ability to simplify the
collection of axioms postulated about F in the definition of a functorial reactive system
(Definition 2.5). The goal would be to give a neater collection involving G which might be
verified for many cases based directly on general categorical reasoning about quotienting
bicategories by their 2cells.
Finally, note that the strategy of bringing in enriched categorical machinery is directly
opposite to Milner's in [Mil01]. He discards “
C (the track of A) and works directly with a
precategory A: he then calculates RPOs in A, slides IPO in A, etc. His approach demands
INRIA
Synthesising Labelled Transitions and Operational Congruences in Reactive Systems, Part 2 21
that he be vigilant, since he is required to verify that compositions he encounters in A
are welldefined. Nonetheless, this extra care seems bearable: for most compositions, a
trivial inspection of the operands su#ces. It is therefore a challenge to category theorists
to provide a collection of theorems for smoothly manipulating bicategories (for example)
in which the e#ort needed to apply these results is less than the e#ort needed to work in
the setting of precategories.
RR n° 4395
22 J.J. Leifer
4 Action graph contexts
4.1 Introduction
As promised in the previous section, the present one gives a substantial example of a
precategory AIxt of raw contexts based on action calculi. (The ``Ixt'' is for ``insertion
context'', a terminology explained in Subsection 4.6.) The need to handle graphs was
the original motivation for functorial reactive systems: as we will see in Subsection 4.3,
RPOs do not always exist for CIxt, the support quotient (Definition 3.10) of AIxt, so
it is necessary to consider an upstairs category which does possess su#cient RPOs and a
functor down to CIxt.
The precategory AIxt has all the extra structure required of A, namely a sup
port function and a support translation operation, so is a wellsupported precategory
(Definition 3.2). By direct instantiation of the results of the previous section, we can
construct three things: the track of AIxt, which we call “
CIxt; the support quotient of
AIxt, which we call CIxt; and a functor F : “
CIxt CIxt. These are related in the
following table to their counterparts from the Section 3:
wellsupported precategory: A AIxt
track: “
C “
CIxt
supportquotienting functor: # F # F
support quotient: C CIxt
Thus by Theorem 3.14 and Theorem 3.15, F lifts arrows by their domain, creates isos,
creates compositions, and allows IPO sliding. Furthermore AIxt has a distinguished ob
ject 0, hence there are distinguished objects 0 and # of CIxt and “
CIxt, with F(#) = 0,
whence F lifts agents. Thus, any choice of reaction rules Reacts for CIxt and reac
tive context subcategory D of CIxt (Definition 2.4) yields a functorial reactive system
(Definition 2.5).
The main hurdle then in using the congruence results of the section ``Further congru
ence results'' in Part 1 is proving that F has all redexRPOs (Definition 2.6). It turns out
that this property fails for some choices of reaction rules, but that it does hold for a rich
class of them.
As promised in Section 3 of Part 1, the category CIxt of graph contexts (the
codomain of F) does not admit enough RPOs for subtle reasons. Examples are shown
in Subsection 4.3. The cause is the lack of su#cient intensional information as to which
node in contexts C 0 or C 1 , say, corresponds to a node in the composite C 0 C 1 . It is ex
actly “
CIxt, the domain of F , that contains just enough structure to track how the nodes
of two contexts are related to the nodes of their composition. By the definition of ``F
INRIA
Synthesising Labelled Transitions and Operational Congruences in Reactive Systems, Part 2 23
has all redexRPOs'', the proof obligation is to show that su#cient RPOs exist in “
CIxt
(Theorem 4.16). The proof of their existence is not done in the present paper, but is
contained in full in [Lei01b].
The development of action calculi presented in this section intersects with that of
[CLM00]; however the latter makes no use of functorial reactive systems, a key contribution
of the present paper. Note as well that there are some di#erences in naming: in this paper
I write “
CIxt and CIxt; in [CLM00], these are denoted PIns 0 and ACxt 0 respectively.
4.2 Action calculi reviewed
I review a restricted class of the action calculi which were presented in [Mil96]. The rest
of this section and the next make no specific use of the algebra of action calculi shown
here since all of the work is done directly on graphs. Nonetheless, the design decisions
taken when defining graphs are guided by the algebraic presentation of action calculi, so
the latter provide valuable motivation.
A closed, shallow action calculus is a strict monoidal category whose objects are
natural numbers k, m, n, o . . ., and whose arrows are called action graphs and written
a : (k, o), b : (m, n). (I avoid the usual arrow notation a : k o, reserving it for the
context arrows of reactive systems.) The tensor product of these two action graphs is
a# b : (k +m, o+n); the composition of a : (k, o) and b : (o, m) is a·b : (k, m); the identity
action graph of arity (m, m) is i m . The order of composition is not conventional in category
theory: it connotes the orientation of the action graphs we work with. (Note that this
composition is the horizontal juxtaposition of action graphs and has nothing to do with
contextual composition which we consider later.) A pair of natural numbers (k, o) is an
arity ; let #, #, . . . range over arities. I deal only with closed, shallow action calculi and so
usually omit these adjectives from now on.
An action calculus has a control signature K = {K, L, . . .} consisting of controls, each of
which has an arity. There are constants p : (2, 2), c : (1, 2) and # : (1, 0) for permutation,
copy and discard. These constants represent only the swapping, sharing and elimination
of arcs, not of nodes. They satisfy simple equations, e.g. c·p = c representing the com
mutativity of copying. There is also an operator called reflexion [Mil94] (similar to the
``trace'' of Joyal et al. [JSV96]) which we need not detail here.
Finally, each action calculus has a binary reaction relation , relating action graphs
of equal arity. This relation is preserved by all constructions, i.e. by composition, tensor
product and reflexion.
RR n° 4395
24 J.J. Leifer
L
M
M
M
K
Figure 11: The action graph K·c·(M # L) and the context  1,1 ·c·(M #M)
For examples of action graphs, let K : (0, 1), M : (1, 1) and L : (1, 0) be controls. Then
the following are action graphs, with their arities:
K #M : (1, 2)
K·c·(M # L) : (0, 1)
(K·M) # (M ·L) : (1, 1) .
Composition · binds tighter than tensor #, so the last can be written K·M #M ·L.
A context C is an action graph containing a single hole with arity #, written # . I
omit the arity, writing , if it is determined by the rest of the context or the surrounding
discussion. Thus a context C : # # is an action graph of arity # with a hole of arity #.
Here are two contexts along with their domain and codomain arities (the arity of the hole
being fully determined in the second case):
 1,1 ·c·(M #M) : (1, 1) (1, 2)
K··L : (1, 1) (0, 0) .
Figure 11 shows an action graph and a context using a graphical notation. It uses
nodes (rectangles with two blunt corners) to represent occurrences of controls, and arcs
to represent composition. An action graph with arity (m, n) has m source ports on its
left side and n target ports on its right side. A control node or hole of arity (m, n) has m
target ports at its left side n source ports at its right side. At a source node, branching of
arcs represents c and absence of arcs represents #.
Two contexts are equal if the algebraic theory equates them, treating the hole as
a control distinct from all others. The composition of two contexts C : # # and
D : # #, written here DC (note the conventional order of composition), is formed
by replacing the hole in D by C and joining the arcs according to the common ports.
(This is context composition, not horizontal action graph composition described earlier.)
Composition is clearly associative, and there is an identity context id # =  # for each
arity. An action graph a : # can be considered as a context a : (0, 0) # whose hole has
minimum arity. We shall use lower case letters a, . . . for action graphs.
INRIA
Synthesising Labelled Transitions and Operational Congruences in Reactive Systems, Part 2 25
We have thus associated with an action calculus a reactive system CIxt, whose objects
are arities, with distinguished null arity (0, 0), and whose arrows are contexts, including
action graphs.
4.3 Examples and a problem
In this subsection I give examples of specific RPOs in CIxt, illustrating several phenom
ena. I end with an example showing cases in which RPOs fail to exist; this motivates the
strategy of defining a category ``upstairs'' (the domain of a functor with codomain CIxt)
for which enough RPOs do exist.
Remember that CIxt is really a family of reactive systems arising from action calculi;
each is determined by a control signature and a set of reaction rules.
Example 4.1 (arithmetic) I first illustrate how an RPO can determine a labelled
transition, using an action calculus for elementary arithmetic having controls 0 : (0, 1),
S : (1, 1), and + : (2, 1). The reactive system is shown in Figure 12; it is an example
of the sharing graphs of Hasegawa [Has99], which add sharing to the interaction nets of
Lafont [Laf90]. Nodes represent subexpressions, and the forking of arcs allows these to
be shared. The reaction rules are in the top diagram; the garbage collection rules allow
unattached expressions to be incrementally destroyed.
The middle diagram shows an action graph a occurring in a larger one b # , which also
contains an occurrence of the redex l 1 of the rule for S. The contexts C # and D # correspond
to the two occurrences, which overlap. Now what is the ``just large enough'' context C
which extends a to contain l 1 ? It is not quite C # , because C # has destroyed the possibility
of sharing S which is o#ered by l 1 . In fact it is C as shown in the lower diagram; it may not
seem ``smaller'' than C # , but it is indeed a factor of C # , as witnessed by the context E. (C #
cannot be a factor of C; no context F surrounding C # can cause its Snode to be shared.)
So our synthesised labelled transition system will admit the transition a C Dr 1 . We
would expect to add further controls, e.g. for subtraction, before obtaining an interesting
behavioural congruence.
Example 4.2 (wiring) The preceding example used the forking and deletion of arcs to
represent the sharing of components. This nonlinearity is a pervasive feature in process
calculi. CCS and the #calculus depend heavily on it; witness the double occurrence of x
in its reaction rule for CCS: •
x.a  x.b a  b (and similarly for the #calculus). The redex
has no direct representation in the family of action calculi introduced in this subsection
because we confine our attention to shallow, closed action graphs, i.e. ones without nesting
of graphs (needed for prefixing) and free names. Without such limitations, the redex is
exactly modelled by an action graph with a forked arc (representing the sharing of x)
connected to two controls representing the output and input prefixes, containing inside a
and b respectively. See [Mil96] for many examples.
RR n° 4395
26 J.J. Leifer
+
Arithmetic rules
+
+
S
+
0
S
S
S
0 0
Garbage collection rules
r 1
l 0 r 0
l 1
+
0
+
S
+
0
S
b #
(0, 0) (1, 1)
(1, 1)
(2, 2)
a
l 1
D #
C #
C # a = D # l 1 = b #
S
0
An action graph a overlapping a redex l 1
a
l 1 D #
0
S
(0, 0)
(1, 2) (1, 1)
(2, 2)
(1, 1)
C #
D
C
E
Ca = Dl 1 = b
S
+
0
b
An RPO for a and l 1 w.r.t. C # and D #
Figure 12: A reactive system for arithmetic (Example 4.1)
INRIA
Synthesising Labelled Transitions and Operational Congruences in Reactive Systems, Part 2 27
(0, 2)
(0, 2)
(0, 2)
(0, 0)
C #
C
D
(0, 0) (0, 2)
a t 0
t 1
b
t 2
t 3
D #
K
K
K
K
(t 1 ,t 3 )
(t 1 ,t 2 )
(t 0 ,t 3 )
(t 0 ,t 2 )
E
(0, 4)
Figure 13: An RPO for copied wiring (Example 4.2)
Nonlinearity can give rise to RPOs which are more complex than one might expect.
Figure 13 shows two identical action graphs a = b = K·c, where K : (0, 1); using the
identity contexts C # = D # =  0,2 they are embedded in K·c. But the RPO C, D,E does
not consist of identity contexts! A candidate might choose to identify t 0 in a with either
t 2 or t 3 in b, and similarly for t 1 . To be the ``best'' candidate, the C, D,E must handle
all these pairings; to indicate this we have indexed its targets by pairs in the diagram. In
fact we have
Ca = Db = K·c·(c # c) .
Example 4.3 (reflexion) A surprising phenomenon is how the presence of reflexion
can a#ect the RPO. Let K,N : (1, 1), L : (0, 2) and M : (2, 0), and recall that i 1 is the
identity of arity (1, 1) for action graph composition. Figure 14 shows a = L·(i 1 #K) and
b = (i 1 #K)·M embedded in C # a = D # b = L·(N #K)·M . The contexts C # and D # do not
involve reflexion. In the RPO C, D,E shown we have Ca = Db = (i 1 #L)·(p#K)·(i 1 #M );
this extends a by only one control (M) in order to create an occurrence of b. The contexts
C and D do not use reflexion, but E does use it. If reflexion is forbidden then the
RPO C + , D + , E + is such that C + a = D + b contains N ; this would yield a more complex
synthesised labelled transition relation.
These examples do not exhaust the phenomena which arise in finding RPOs in CIxt,
but they indicate that the general construction will not be trivial. The reader may feel
that, having coped informally with a number of phenomena, we are well on the way to
finding RPOs in every case. However, they do not always exist in CIxt! Here is a
counterexample.
RR n° 4395
28 J.J. Leifer
M
N
L
K
(0, 0)
L
K
K
L N
(0, 0) (0, 0)
(0, 0)
(1, 1)
(0, 2)
(2, 0)
M
M
a
b D
C
E
N
M
D #
C #
L
N
K
Figure 14: An RPO using reflexion (Example 4.3)
Example 4.4 (missing RPO) Let K : (0, 1) and L : (1, 0). Let a = b = K and let
C # = D # = K·L # 0,1 ·L with arity (0, 1) (0, 0). Then C # a = D # b = K·L #K·L; this is
shown in the upper diagram of Figure 15. The lower diagram shows two candidate RPOs,
for which it is easy to verify commutation:
C 0 , D 0 , E 0 = , , K·L # ·L
C 1 , D 1 , E 1 = #K, K #, ·(L # L) .
But if there were an RPO, then contexts C, D,F 0 , F 1 would exist as shown making the
diagram commute, yielding a contradiction as follows: Neither C nor D can contain any
control, since F 0 C = F 0 D = . Hence from CK = DK we deduce C = D, using the
criterion for context equality stated above (since the control K appears in neither C nor
D). Hence #K = F 1 C = F 1 D = K #, a contradiction.
This counterexample involves neither copying nor discard of arcs, so is applicable to
linear action calculi too [LM02]  those in which all source ports bear exactly one arc.
Thus we cannot attribute the lack of RPOs to c and #, even though they demand careful
treatment as shown in Example 4.1 and Example 4.2.
The counterexample also illustrates why RPOs do not always exist in CIxt. The
equations C 0 K = D 0 K = K and C 1 K = D 1 K = K # K hold respectively for the two
candidates; but if we ``track'' the two occurrences of a = K and b = K through these
equations, we find that they correspond to the same occurrence of K in the first case,
and to two di#erent occurrences in the second case. This is a key to solving our problem;
we seek a suitable refinement of CIxt that possesses the RPOs we need. We expect its
INRIA
Synthesising Labelled Transitions and Operational Congruences in Reactive Systems, Part 2 29
K
K
K L
L
K
K
K L
L
L
L
(0, 0)
(0, 0) (0, 0)
(0, 1)
(0, 1)
(0, 0)
b
a
D #
C #
A context equation C # a = D # b
·(L # L)
K·L # ·L
(0, 0)

K
K
K #
K·L # ·L
K·L # ·L
D
#K
F 0

F 1
(0, 0)
(0, 0)
(0, 1)
(0, 1)
impossible!
(1, 1)
C
Figure 15: A missing RPO in CIxt (Example 4.4)
RR n° 4395
30 J.J. Leifer
contexts to track the occurrences of nodes. This is a similar idea to that of ``colouring'',
which has been suggested by Sewell to replace his dissection based definitions [Sew].
The strategy is as follows. The next two subsections are devoted to the construc
tion of AIxt, a wellsupported precategory of arities and raw contexts. Replaying
the constructions of Section 3, we derive two categories from AIxt and a functor be
tween them F : “
CIxt CIxt. Finally we state the RPO existence theorem for “
CIxt
(Theorem 4.16), thus showing that F has all redexRPOs (Theorem 4.17).
4.4 Closed shallow action graphs
In this subsection, after introducing some notation, I define a class of action graphs. These
graphs are enriched in the next subsection to form raw contexts (graphs with a hole in
them), the arrows of the precategory AIxt. No attempt is made to verify formally that
the action graphs presented here correspond to action calculi terms quotiented by the
action calculi axioms (which are not presented here). Such an undertaking represents
future work and will be of more value when the tractable graphtheoretic features include
free names and nesting.
Notation I write [m] for the ordinal number {0, 1, . . . , m1}. The disjoint sum
# i#I X i
of a family of sets is taken to be the set # i#I ({i} ×X i ). A particular case is when I = [n];
then the disjoint sum may be written, without parentheses, as X 0 + X 1 + · · · + X n1 .
Examples in this section take the form S =
# v#V S v + [m] + [n], a ternary disjoint sum,
the first summand of which is itself a disjoint sum; S has elements of the form (0, (v, s))
for each v # V and s # S v , (1, i) for each i # [m], and (2, j) for each j # [n].
If the sets X and Y are disjoint, I often write their union as X #Y . This notation is to
be distinguished from a disjoint sum. In particular, (X 1 #X 2 )#X 3 = X 1 #(X 2 #X 3 ) and will
often be written without parentheses; on the other hand, the disjoint sums X 1 +X 2 +X 3 ,
(X 1 + X 2 ) + X 3 and X 1 + (X 2 + X 3 ) are all distinct but in bijective correspondence. If
f : X Z and g : Y Z are two functions with X disjoint from Y , then f#g : X#Y Z
is their union.
I use f : X # Y , f : X # Y and f : X ## Y for respectively injective, surjective
and bijective functions, and f : X ## Y for an injection which is an inclusion. Finally, #
denotes function composition, Id X the identity function on the set X, and #X the empty
function from # to X.
Definition 4.5 (control signature) We fix a control signature K, a set of controls,
equipped with an arity function called arity : K N 2 and let K, L, . . . range over K. For
arity(K) = (m, n) we write K : (m, n); in this case, two functions extract the components
of the pair: arin(K) “
= m and arout(K) “
= n. #
INRIA
Synthesising Labelled Transitions and Operational Congruences in Reactive Systems, Part 2 31
Definition 4.6 (action graphs) A (closed, shallow) action graph G =
(m, n, V, contr , src) comprises an arity (m, n), a set V of nodes, called a support, a
control map contr : V K assigning a control in K to each node in V , and a source map
src : T S assigning a source (port) in S to each target (port) in T , where
ˆ the source set S “
=
# v#V [arout(contr(v))] + [m] comprises the binding sources for
each v # V and the input sources indexed by [m];
ˆ the target set T “
= # v#V [arin(contr(v))] + [n] comprises the argument targets for
each v # V and the output targets indexed by [n]. #
Nomenclature We may write a graph as G = (V, contr , src) : (m, n), or just
G = (V, contr , src) when the arity is understood. We denote the empty graph
(#, #K , ## ) : (0, 0) by 0. We shall abbreviate arin(contr(v)) to arin(v) etc., when there
is no ambiguity. We denote the injections induced by the disjoint sums S and T as
follows:
bind(v) : [arout(v)] # S for the binding sources of each v # V ;
in : [m] # S for the input sources;
arg(v) : [arin(v)] # T for the argument targets of each v # V ;
out : [n] # T for the output targets. #
We shall write bind(v, i) and arg(v, j) for the ports bind(v)(i) and arg(v)(j). For any
injection f into a set A we write A f for the range of f ; thus for example S in is the set
of all input sources and T arg(v) the set of argument targets of v. We shall also write for
example S bind for # v#V S bind(v) . With this notation we can represent our partitions as
S = S in
# S bind
T = T out
# T arg .
An example of an action graph with arity (1, 3) is shown in Figure 16, with node names
and the control map omitted. The whole graph is in a rectangle, with input sources at
the left and output targets at the right. Nodes are drawn as rectangles with two corners
blunted to give orientation; we may want to tilt some of them, as here, or even turn them
upside down. The three nodes have arities (1, 1), (2, 1) and (1, 2). The arcs represent the
source map, with arrows pointing from source to target. Ports could be drawn as blobs,
but this is somewhat redundant; a target is always indicated by exactly one incoming arc,
and we indicate a source with no outgoing arcs by a little aborted arc.
Cycles are allowed. The graphs studied here are for action calculi which are closed,
meaning that free names such as x, y, . . . are not used as sources, and shallow, meaning
that nodes do not contain action graphs nested inside. I study the closed, shallow action
RR n° 4395
32 J.J. Leifer
Figure 16: A closed shallow action graph
graphs in this paper as a preliminary to future work on a full graphical presentation of
action calculi, since notions such as graph contexts are more clearly handled in this simpler
setting.
Convention Action graphs are almost always denoted by G suitably subscripted.
Rather than always explicitly list all their primary components V , contr , and src, or
their derived components S, T , bind , in etc., we shall follow a firm convention that the
names of these components are standard, decorated as necessary to connote the graph's
name.
4.5 The wellsupported precategory AIxt of arities and raw contexts
I proceed now to construct the wellsupported precategory AIxt of raw contexts with a
support function and support translation operation (Definition 3.2).
The intuition of ``context'' is wellsupplied by Figure 17; the graph G occurs inside
the dotted rectangle in G # , and we may think of the context in which G is placed as that
part of G # lying outside the dotted rectangle. A context is therefore an action graph, but
with a little more structure since it has an internal as well as an external interface. The
internal interface is often called a hole. (I do not consider here contexts with more than
one hole.)
The lower diagram shows the context C which results when G is excised from G # ;
in the notation of what follows, G # = CG (C composed with G). Note the new targets
and sources on respectively the left and right sides of C's internal interface; in particular,
INRIA
Synthesising Labelled Transitions and Operational Congruences in Reactive Systems, Part 2 33
G #
G
The action graph G is a subgraph of G #
C
The corresponding context
Figure 17: The bottom context composed with the middle action graph yields the top
action graph
RR n° 4395
34 J.J. Leifer
the middle internal source lacks any targets and therefore represents the discard of the
corresponding output target of G  or of any other graph  when placed in the hole.
Definition 4.7 (raw context) A (closed, shallow, loose) raw context A = (V, contr , src)
of arity (m # , n # ) to (m, n), written A : (m # , n # ) (m, n), comprises a support V , which is
a set of nodes, a control map contr : V K assigning a control in K to each node in V ,
and a source map src : T S assigning a source (port) in S to each target (port) in T ,
where
ˆ the source set S “
=
# v#V
[arout(v)] + [m] + [n # ] comprises the binding sources for
each v # V , the input sources indexed by [m], and the upput sources indexed by [n # ];
ˆ the target set T “
= # v#V [arin(v)] + [n] + [m # ] comprises the argument targets for
each v # V , the output targets indexed by [n], and the downput targets indexed by
[m # ].
Furthermore, we require that the looseness condition is satisfied (see nomenclature defined
below):
src(T down ) # S up = # . Loose
The looseness condition precludes a ``tight'' loop from the back of the hole to the front, such
as is formed by reflexion in action calculi. It does not preclude such a loop proceeding via a
control, which indeed occurs in Figure 17; thus the contexts permit only limited reflexion,
which simplifies the definition of composition. (See Section 5 for further discussion.)
Finally, A is the support of A, i.e. V in this case. #
Note that an action graph G is just a raw context A as above in which m # = n # = 0.
Nomenclature As for action graphs, there are induced injections for raw contexts as
follows:
bind(v) : [arout(v)] # S for the binding sources of each v # V ;
in : [m] # S for the input sources;
up : [n # ] # S for the upput sources;
arg(v) : [arin(v)] # T for the argument targets of each v # V ;
out : [n] # T for the output targets;
down : [m # ] # T for the downput targets.
With naming similar to that in action graphs for the partitions of S and T , we have
S = S bind
# S in
# S up
T = T arg
# T out
# T down .
INRIA
Synthesising Labelled Transitions and Operational Congruences in Reactive Systems, Part 2 35
A 0
A 1
T down
0
S in
1 S up
0
T down
1 S in
0 S up
1
T out
1
T out
0
Figure 18: The composition of two raw contexts
Raw contexts cannot be composed when the supports of each operand in a composi
tion intersect nontrivially. Composition is welldefined when the operands have disjoint
supports one of the required properties of a wellsupported precategory (Definition 3.2).
Definition 4.8 (identity and composition for raw contexts) The identity raw
context id (m,n) = (#, #K , src) : (m, n) (m, n) has
S “
= #+ [m] + [n] = S in
# S up
T “
= #+ [n] + [m] = T out
# T down
src : # down(i) ## in(i) i # [m]
out(j) ## up(j) j # [n] .
Let A i = (V i , contr i , src i ) : (m i , n i ) (m i+1 , n i+1 ) be two raw contexts for i = 0, 1, with
V 0 # V 1 = #. Their composition, illustrated in Figure 18 by nesting A 0 inside A 1 , is
A 1 # A 0 “
= A 2 = (V 2 , contr 2 , src 2 ) : (m 0 , n 0 ) (m 2 , n 2 ) ,
where V 2 “
= V 1 # V 0 and contr 2 “
= contr 1 # contr 0 (thus determining arin 2 = arin 1 # arin 0
and likewise arout 2 , bind 2 , arg 2 ), and
S 2 “
=
# v#V 2
[arout 2 (v)] + [m 2 ] + [n 0 ] = (S bind
1 # S bind
0
) # S in
1 # S up
0
T 2 “
=
# v#V 2
[arin 2 (v)] + [n 2 ] + [m 0 ] = (T arg
1 # T arg
0 ) # T out
1 # T down
0 .
Note (see Figure 18) that T down
1 is in bijection with S in
0 and [m 1 ], while S up
1 is in bijection
with T out
0 and [n 1 ]. It remains to define the source function src 2 ; this is done in terms of
two auxiliary functions # i : S i S 2 (i = 0, 1) which describe how sources of A 0 and A 1
RR n° 4395
36 J.J. Leifer
``become'' sources of A 2 :
# 0 (s) “
= # s if s # S bind
0 # S up
0
src 1 down 1 (i) if s = in 0 (i) # S in
0
# 1 (s) “
= # s if s # S bind
1 # S in
1
# 0 src 0 out 0 (j) if s = up 1 (j) # S up
1
src 2 (t) “
= # # 1 src 1 (t) if t # T arg
1 # T out
1
# 0 src 0 (t) if t # T arg
0 # T down
0 .
#
We have adopted the symbol `` # '' for composition of raw contexts as a reminder that it is
partial: the supports of the operands are required to be disjoint in order for a composition
to be defined.
Proposition 4.9 (raw contexts form a precategory) If A 0 and A 1 are raw contexts
with A 1  # A 0  = # then A 1 # A 0 is a raw context too. (In particular, # preserves the
Loose condition.) Composition is associative and has identity id (in the way required of
a precategory, see Definition 3.1).
Proof Follows immediately from Propositions 21 and 22 of [CLM00]. #
By definition composition satisfies Suppcomp and Suppid (Definition 3.2), i.e.
A 1 # A 0  = A 1  # A 0  Suppcomp
id m  = # . Suppid
The only task remaining in order to show that AIxt is a wellsupported precategory
is the definition of a support translation operation and the verification of its properties.
Definition 4.10 (support translation for raw contexts) Given a raw context
A : (m 0 , n 0 ) (m 1 , n 1 ) and an injection # whose domain contains the support of A,
i.e. Dom # # A, we define the support translation by # of A, written # # A, as follows:
# # A “
= A # , where:
V # “
= #V
contr # (v) “
= contr(# 1 (v)) thus determining arin, arout , bind , arg
S # “
= # v#V # [arout # (v)] + [m 1 ] + [n 0 ]
T # “
=
# v#V # [arin # (v)] + [n 1 ] + [m 0 ]
thus determining bijections # S : S ## S # and # T : T # ## T whence we define:
src # “
= # S
# src # # T . #
INRIA
Synthesising Labelled Transitions and Operational Congruences in Reactive Systems, Part 2 37
This definition satisfies the appropriate healthiness conditions:
Proposition 4.11 (support translation is welldefined) If A satisfies Loose then
so does # # A, thus # # (·) is a welldefined operation on raw contexts.
Proof Immediate from src # “
= # S
# src # # T , since # S and # T are the identity on upput
sources and downput targets respectively. (Proposition 24 in [CLM00].) #
Furthermore, support translation satisfies the remaining axioms in the definition of a
wellsupported precategory (Definition 3.2):
Proposition 4.12 (support translation properties) All of the following properties
hold:
# # id m = id m Transidr
# # (A 1 # A 0 ) = # # A 1 # # # A 0 Transcompr
Id A # A = A Transidl
(# 1 # # 0 ) # A = # 1 # (# 0 # A) Transcompl
# 0 # A = # 1 # A implies # 0 # A = # 1 # A Transres
# # A = #A . Transsupp
Proof All of these except the last follow from Proposition 25 in [CLM00]. Transsupp
follows immediately from Definition 4.10. #
Thus:
Theorem 4.13 AIxt is a wellsupported precategory. #
4.6 Constructing a functorial reactive system
Having established that AIxt is a wellsupported precategory, the rest of the results
of Section 3 are immediately applicable, as we next see. We let “
CIxt be the track of
AIxt (Definition 3.3), a category of profiles and insertion contexts. The arrows are called
``insertion contexts'' to remind us that they ``insert'' the nodes of the domain profile into
the codomain profile.
Now let CIxt be the support quotient (Definition 3.10) of AIxt. Finally let
F : “
CIxt CIxt be the supportquotienting functor (Definition 3.12). Then by
Theorem 3.14, F lifts arrows by their domain, creates isos, and creates compositions.
By Theorem 3.15, F allows IPO sliding.
AIxt has a distinguished object (0, 0): as stated immediately after Definition 4.7, a
raw context with domain (0, 0) is identical to an action graph. Recall that CIxt has the
same objects as AIxt does, so the distinguished object 0 of CIxt (viewed as a reactive
system) is just (0, 0). Likewise, let # “
= (0, 0, #), the distinguished object for “
CIxt. Since
F(#) = 0, we have that F lifts agents, and thus:
RR n° 4395
38 J.J. Leifer
Theorem 4.14 (F is functorial reactive system) The supportquotienting functor
F : “
CIxt CIxt is a functorial reactive system for any choice of D and Reacts. #
Thus all the congruence results of Section 3 in Part 1 are applicable to F (except
Theorem 3.34 since we are not dealing with multihole contexts) with one proviso: we
wish to determine choices of D and Reacts such that F has all redexRPOs.
#
#
#
#
# p 0
p 1 p
G 0
G 1 A 0
A 1
19
With regard to D, the strongest result obtainable is with D = CIxt,
i.e. with all contexts in CIxt reactive, so let us fix on this. Recall from
Definition 2.6, that F has all redexRPOs if any square in “
CIxt, such as
in Figure 19, has an RPO provided that there exists r # CIxt such that
(F(# G 1 p 1 ), r) # Reacts.
So the key question is: for which choice of redexes l (first components of the Reacts
relation) do there exist RPOs in “
CIxt for squares such as Figure 19 where F(# G 1 p 1 ) = l.
The answer is that for almost an any choice of redexes, except the most pathological, RPOs
exist. In order to make precise which are these pathological cases, we need a definition
about action graphs.
Definition 4.15 (outputcontrolled) In any graph, a target is controlled if its source
is a bound source. G is outputcontrolled if all its output targets are controlled;
formally:
src(T out ) # S bind . (outputcontrolled)
Since Cod src = S in
# S bind , an equivalent formulation is:
src(T out ) # S in = # . (outputcontrolled)
#
Informally, a graph satisfies this definition when it contains no ``floating'' wires con
necting the lefthand interface ports with the righthand ones.
Recall that in “
CIxt a context # G (m, n, U ), whose domain is the empty profile #, is
actually a graph G : (m, n) with G = U . Thus the definition of outputcontrolled
applies to contexts in “
CIxt with domain #.
RPOs do exist provided one of the legs is outputcontrolled:
Theorem 4.16 Let C 0 G 0 = C 1 G 1 = G in “
CIxt, where G 1 is outputcontrolled.
Then there exists an RPO for G 0 , G 1 w.r.t. C 0 , C 1 .
Proof See Corollary 6.28 in [Lei01b]. #
Now note that if G is outputcontrolled then # # G is too for any injection # with
Dom # # G. Thus it is welldefined to say that a context with domain (0, 0) in CIxt
(the category formed by quotienting out support translations) is outputcontrolled.
INRIA
Synthesising Labelled Transitions and Operational Congruences in Reactive Systems, Part 2 39
Because Theorem 4.16 is asymmetric in the use of the outputcontrolled hypothesis,
it directly implies the following.
Theorem 4.17 (F has all redexRPOs) The functorial reactive system F : “
CIxt
CIxt has all redexRPOs provided that every redex is outputcontrolled, i.e. pro
vided that for all (l, r) # Reacts, l is outputcontrolled. #
Happily, the requirement that redexes be outputcontrolled is a tolerable one since
redexes that are not are pathological (see Chapter 7 in [Lei01b]). Finally, Theorem 4.17
implies that all of the congruence results of Section 3 in Part 1 (except the one for multi
hole contexts) are immediately applicable to F : “
CIxt CIxt, as desired.
RR n° 4395
40 J.J. Leifer
5 Conclusions and future work
Constructing RPOs is di#cult, as witnessed by the daunting complexity in Chapter 6,
``RPOs for action graph contexts'', in [Lei01b] (the proof of Theorem 4.17 in the present
paper). It is therefore desirable that it not be done afresh for each new process calculus.
This is the impetus for the leading example in this paper, namely action calculilike con
texts. Recall that the functorial reactive system F : “
CIxt CIxt is really a family
with varying choices of control signature K and of reaction rules Reacts. The fragment
of action calculi considered in Section 4 is thus a framework : if one can express states of
a computational model using controls (for atoms) and arcs (for names and sharing) and
reactions in terms of redexes that satisfy the condition outputcontrolled then RPOs
exist and hence Section 3 of Part 1 gives labelled transitions and operational congruences.
A framework is often deficient for two reasons: (i) it provides insu#cient benefits to
compensate for the e#ort of casting a specific example in the framework's form; (ii) it is
not rich enough to cover all the phenomena that one wants. Criticism (ii) hits home. The
fragment of action calculi presented in this paper is inadequate for most purposes: there
is no nesting of action graphs (needed for prefixing), no free names, no binding, limited
reflexion, no choice operator, and no multihole redexes (needed to represent faithfully
metavariables in reaction rules). I describe future work below that addresses these other
issues. Criticism (i), however, is unjustified when applied to the action calculi shown here:
getting ``for free'' a labelled transition system and a collection of operational congruences
is a worthwhile benefit.
The reverse situation held for action calculi as originally presented by Milner [Mil96]:
criticism (ii) was not such a problem but criticism (i) was: up until now there has been
little tangible reward to using action calculi to present specific examples of process calculi.
The central goal of future work is to construct a framework with rich enough structure
(perhaps like Milner's original action calculi) to dodge criticism (ii) while still providing
the rewards of labelled transitions and operational congruences.
To this end, it will be important to pursue several research directions:
multihole redexes: The basic reaction rule of the #calculus is
•
x#y#.a  x(z).b a  {y/z}b . (3)
There is a problem of adequately representing (3) in a reactive system. Currently I
require that the reaction rules Reacts consist of pairs of agents, not agent contexts.
As a result, the only way to represent (3) is via an infinite family of rules, one for
each possible instantiation of a and b. Thus there might be labelled transitions of
the form
•
x#y# x(z).b (4)
INRIA
Synthesising Labelled Transitions and Operational Congruences in Reactive Systems, Part 2 41
out
in
in
x
y
Figure 20: Nesting of nodes
for all instantiations of b. But these are ungainly labels: the only important part
of any label of the form   x(z).b is the toplevel structure, namely x(z); the b is
irrelevant.
How can we winnow down the family of labels to a single one? The answer lies in
using the uniformity present in (3). The a and b there are really metavariables and
the rule can be expressed thus:
•
x#y#. 1  x(z). 2  1  {y/z} 2 . (5)
This rule consists of a pair of 2hole contexts which capture the uniformity present
in it. In Figure 13 of [Mil01], Milner proposes a formalisation of exactly this rule in
his bigraphical reactive systems, which cater directly for multihole contexts.
If we relax the condition on Reacts and allow it to contain pairs of contexts (L, R) for
which L, R : m n are arbitrary contexts, then it is easy to generate the reaction
relation (forgetting about the details of D)
A A # i# (#(L, R) # Reacts, C, D. A = DLC & A # = DRC) .
#
#
#
#
B
A
F
C
L
D
B # F #
C # D #
21
Contrast this to Proposition 2.7 for which the reaction rules
are closedup under context application on the outside, not
also on the inside (as shown here). The hard problem is
to define labelled transitions A F A # . We cannot rely on
IPOs anymore since the domain of A is potentially di#erent
from the domain of any redex L. A possible replacement for IPOs might be via
hexagon idem pushouts (which are special kinds of hexagon relative pushouts) as
suggested by Sewell. Notice how L and A are wrapped up in Figure 21 by arrows
RR n° 4395
42 J.J. Leifer
composed on either side. The hexagon idem pushout property guarantees that there
is no lesser hexagon bounded by B # , C # , F # , D # . It seems plausible that such hexagons
can yield the single labelled transition •
x#y#  1 x(z). 2 from (5), which is lighter than
having the infinite family shown in (4).
In [Sew], Sewell already exploited the uniformity present in reaction rules when
looking at term algebras with parallel composition. He achieved lightweight labelled
transitions, but made use of complex context dissection lemmas. He is now look
ing at the problem of recasting his results in terms of universal constructions (such
as hexagons). In conclusion, there are two important lines of research related to
multihole redexes which mirror what was done in my paper: (i) defining labelled
transitions by universal constructions and proving congruence for a variety of equiv
alences and preorders; (ii) showing that the relevant universal constructions exist in
categories of interest (term algebras, graphs, etc.).
nesting: The nesting of agents inside nodes is essential for representing prefixing. For
example, in CCS the agent x.y.•x contains three levels of nesting with the name x
shared by the outermost and the innermost. In order to represent this with graph
like constructions, we need that each node packages up the continuation agent, e.g.
as in Figure 20 which gives a possible representation of the CCS agent above.
At first glance, nesting is a trivial thing: term algebras, for instance, consists of just
pure nesting structure with nothing else. It is straightforward to calculate RPOs
for them. However the real challenge is the combination of wiring and nesting:
Figure 20 has an arc sourced by x that is forked and has targets at multiple levels.
In particular, even the notion of context composition is di#cult: when composing
contexts that fork an arc at di#erent nesting levels, the forks have to be normalised
in some way, either by pushing them in to the innermost level or pulling them out
to the outermost.
There are many possible representations for nested graphs. One that seems most
promising comes out of recent work by Milner [Mil01]: the idea is to treat a nested
graph as a flat graph with an added parent function overlaid, a so called topograph
structure. RPOs can then be calculated by handling the wiring structure and the
nesting structure orthogonally.
Even without the full power of nesting, it may be possible to handle the #calculus
(or variants thereof) indirectly. Honda and Yoshida [HY94a] give a translation in
terms of ``concurrent combinators''; these encode prefixing in a flat structure by
using triggers to point to parts of agents that may execute. A synthesised labelled
transition relation for their combinator reaction rules might be too intensional since
the labels could detect exactly the combinators present in an agent. It is worth
trying this, though, to see what kind of equivalences would transpire.
INRIA
Synthesising Labelled Transitions and Operational Congruences in Reactive Systems, Part 2 43
free names and binding: It is straightforward to add free names to graphs: the idea
is to enrich the set of source ports to include names. It is more subtle though to
make precise how a context can bind the names of the thing that goes in its hole.
It seems likely that the objects of the category of contexts need to contain name
sets to ensure that RPOs exist (analogously to inclusion of node sets in “
CIxt), i.e.
a context is an arrow of the form (m, n, U, X) (m # , n # , U # , X # ), meaning that its
hole is expecting a context with support (nodes) U and names X. (This is similar to
Definition 67 in Milner's work on bigraphical reactive systems [Mil01].) It is not clear
whether the downstairs category (the analogue of CIxt) should include these name
sets. For example, in #calculus we write the binding context (#x) without saying
which names can fit in the hole. Perhaps the functor from upstairs to downstairs
(like F : “
CIxt CIxt in this paper) will allow two kinds of IPO sliding: the first
with respect to nodes (as I have shown here) and the second with respect to names.
There has been recent work on modelling names and name binding in a categorical
way [TFP99, GP99] and it would be exciting to join together those syntactic models
with operational semantics, and in particular, the reactive systems shown here.
Name binding carries with it the problem of scope extrusion in labelled transitions.
In #calculus, for example, it is a subtle problem to handle the labelled transition of
(#x)(•y#x#). There are many ways of handling this when looking at bisimulation, for
example, but most involve augmenting the definition with freshness side conditions to
cater explicitly for extrusion. An alternate approach [CS00] keeps track of extruded
names as annotations of the agents themselves, thus gaining the power of extrusion
but keeping the simplicity of bisimulation without added conditions. Adding these
annotations seems almost identical to adding name sets in the objects of a context
category (as outlined above).
sum: As discussed in Subsection 3.5 in Part 1, the proper treatment of summation (such
as occurs in CCS and the #calculus) requires care. It is not good enough for sum to
be a free operator (just another control) if we want to describe its reactive behaviour,
e.g.
(•x.a + b)  (x.a # + b # ) a  a #
#.a + b a .
Consider the second reaction rule. In order for the sum to be rearranged so that
#.a is on the left and the rest is on the right, we require + to be commutative,
associative, and have the empty agent as an identity.
The same problem surfaces for other operators that change the structural congruence
(syntactic equality). In the #calculus, for example, replication is handled by the
RR n° 4395
44 J.J. Leifer
axiom
! a # a  ! a . (6)
This seems hard to represent in terms of graphs since the RHS has, potentially, more
nodes than the LHS. When the problems of finding graph theoretic representation
of sum and replication are overcome (see Milner's proposal in Figures 12 and 13
of [Mil01]), it may still be di#cult to construct RPOs. A possible solution, at
least for replication, is to disallow the structural equality in (6), and instead confine
replication to be input guarded and to have a reaction rule of the form
•
x#y#  ! x(z).a {y/z}a  ! x(z).a .
This is a commonly done in asynchronous variations of #calculus [HT91].
Another way of handling replication is via an encoding in terms of combinators
(already mentioned above) [HY94b]. For input guarded summation, encoding [NP96]
is also an option.
full reflexion: The contexts considered in Section 4 have only a limited form of reflexion,
as enforced by the condition Loose that prevents tight loops linking a hole to itself.
This simplifying assumption makes the composition of contexts and the composition
of the associated embeddings easy. (Embeddings, which are morphisms between
graphs, are not introduced in this paper but play a central role in the construction
of RPOs; see Section 6.2 in [Lei01b].) With full reflexion, the composition of contexts
can create arcs that are formed from arbitrarily many segments of arcs present in the
inner and outer context. Indeed, it is di#cult to prove even that the composition of
reflexive embeddings is associative [Lei01a]. Better technology for handling reflexion
has been developed in [LM02] for graphs with linear wiring. Proving the existence
of RPOs for full reflexion with nonlinear wiring represents a future challenge.
inductive presentation of labelled transitions: In Part 1, the way of deriving la
belled transitions from reactions yields a direct characterisation. This is in contrast
to the inductive presentation usually found in the process calculus literature. Can
the gap be bridged, though? In other words, can an inductive presentation of labelled
transitions be synthesised from reaction rules? It seems plausible. For any partic
ular reactive system whose syntax is generated from some constructors, one could
instantiate Lemma 2.17 of Part 1 (recalled here) by substituting each constructor
for C:
C
F # F
C #
is an IPO a F # a ## C # # D
Ca F C # a ##
.
INRIA
Synthesising Labelled Transitions and Operational Congruences in Reactive Systems, Part 2 45
There are several interesting questions that follow: Under what conditions can we
synthesise an inductive presentation that generates precisely the same labelled tran
sition relation as the direct presentation gives? Under what conditions would an
inductive presentation satisfy any of the GSOS rule formats [GV92, Blo93]? If some
set of the latter is satisfied, it would be enlightening to compare two di#erent proofs
of congruence for strong bisimulation, say  one based on the RPO theory shown
in this paper and the other based on GSOS reasoning, particularly as provided by
recent categorical treatments of the latter [TP97].
It is not surprising that some of these areas (e.g. free names and multihole redexes)
require changes to the categorical abstractions of a reactive system, not just cleverer ways
of constructing RPOs. This pattern is wellestablished in this series of papers. I started
with reactive systems, then passed to functorial reactive systems when it became clear that
RPOs needed to be calculated in a separate category, then considered functorial monoidal
reactive system to cater explicitly for RPOs resulting in multihole contexts. As argued
in Subsection 3.7, it may be advantageous to make an orthogonal extension, replacing
categories by bicategories throughout. An intriguing possibility is that this extension is
not truly ``orthogonal'', i.e. the power of enriched category theory could be brought to
bear on the problems listed above.
A test of the future work outlined above is to see what labelled transitions and opera
tional congruences are generated for applications such as CCS, #calculus, #calculus, and
ambients. It would be exciting (though not likely) to get congruences that coincide exactly
with wellknown ones (open bisimulation for #calculus, say). It should not be a cause
for dejection if the derived congruences do not match exactly the historically established
ones: #calculus comes with a zoo of bespoke congruences, no single one of which is good
for all applications.
The best outcome of this work will be if the mathematical tools that are proposed
here ease the path for exploring new primitives and new patterns of behaviour inherent
in distributed computing. The development of mathematical techniques for reasoning
about hosts and host failure, agent mobility, and cryptography, for example, is critical for
guiding infrastructure and language design. Proofs techniques for these models are critical
for precise reasoning. Much work needs to be done before the tools of this paper are good
enough to address these applications.
RR n° 4395
46 J.J. Leifer
References
Curly braces enclose pointers back to the pages in this paper that cite the work.
[BF00] M. Bunge and M. P. Fiore. Unique factorisation lifting functors and categories
of linearlycontrolled processes. Mathematical Structures in Computer Science,
10(2):137163, 2000. {17}
[Blo93] B. Bloom. Structural operational semantics for weak bisimulations. Techni
cal Report TR931373, Department of Computer Science, Cornell University,
August 1993. {45}
[CLM00] G. L. Cattani, J. J. Leifer, and R. Milner. Contexts and embeddings for closed
shallow action graphs. Technical Report 496, Computer Laboratory, University
of Cambridge, July 2000. Available from http://pauillac.inria.fr/#leifer/. {23,
36, 37}
[Con72] F. Conduch’e. Au sujet de l'existence d'adjoints ‘a droite aux foncteurs ``image
r’eciproque'' dans la cat’egorie des cat’egories. Comptes rendus de l'Acad’emie des
sciences A, pages 891894, 1972. {17}
[CS00] G. L. Cattani and P. Sewell. Models for namepassing processes: interleaving
and causal. In 15th Annual IEEE Symposium on Logic in Computer Science,
2629 June 2000, Santa Barbara, California, USA, pages 322332. IEEE Press,
2000. {43}
[GP99] M. J. Gabbay and A. M. Pitts. A new approach to abstract syntax involving
binders. In 14th Annual Symposium on Logic in Computer Science, 25 July,
1999, Trento, Italy, pages 214224. IEEE Press, 1999. {43}
[GV92] J. F. Groote and F. W. Vaandrager. Structural operational semantics and bisim
ulation as a congruence. Information and Computation, 100(2):202260, 1992.
{45}
[Has99] M. Hasegawa. Models of sharing graphs: a categorical semantics of let and letrec.
BCS Distinguished Dissertation Series. SpringerVerlag, 1999. {25}
[Hon00] K. Honda. Elementary structures for process theory (1): sets with renaming.
Mathematical Structures in Computer Science, 10(5):617663, October 2000.
{10}
[HT91] K. Honda and M. Tokoro. An object calculus for asynchronous communica
tion. In ECOOP '91: European Conference on ObjectOriented Programming,
INRIA
Synthesising Labelled Transitions and Operational Congruences in Reactive Systems, Part 2 47
Geneva, Switzerland, July 1519, 1991, Proceedings, volume 512, pages 133147.
SpringerVerlag, 1991. {44}
[HY94a] K. Honda and N. Yoshida. Combinatory representation of mobile processes. In
POPL '94: 21st ACM SIGPLANSIGACT Symposium on Principles of Pro
gramming Languages, Portland, Oregon, January 1721, 1994, pages 348360.
ACM Press, 1994. {42}
[HY94b] K. Honda and N. Yoshida. Replication in concurrent combinators. In Theoreti
cal Aspects of Computer Software, International Conference TACS '94, Sendai,
Japan, April 1922, 1994, Proceedings, volume 789, pages 786805. Springer
Verlag, 1994. {44}
[Joh99] P. Johnstone. A note on discrete Conduch’e fibrations. Theory and Application
of Categories, 5(1):111, 1999. {17}
[JSV96] A. Joyal, R. Street, and D. Verity. Traced monoidal categories. Mathematical
Proceedings of the Cambridge Philosophical Society, 119(3):425446, 1996. {23}
[Laf90] Y. Lafont. Interaction nets. In Conference Record of the Seventeenth Annual
ACM Symposium on Principles of Programming Languages, San Francisco, Cal
ifornia, January 1990, pages 95108. ACM Press, 1990. {25}
[Lei01a] J. J. Leifer. A category of action graphs and reflexive embeddings. Technical
report, Computer Laboratory, University of Cambridge, 2001. To appear. {44}
[Lei01b] J. J. Leifer. Operational congruences for reactive systems. PhD thesis, Computer
Laboratory, University of Cambridge, 2001. Available in revised form as Tech
nical Report 521,Computer Laboratory, University of Cambridge, 2001, from
http://pauillac.inria.fr/#leifer/. {2, 23, 38, 39, 40, 44}
[Lei02] J. J. Leifer. Synthesising labelled transitions and operational congruences in
reactive systems, part 1. 2002. Submitted for publication. Available from
http://pauillac.inria.fr/#leifer/. {2}
[LM02] J. J. Leifer and R. Milner. Shallow linear action graphs and their embeddings.
Formal Aspects of Computing, 2002. To appear. Special issue in honour of Rod
Burstall. Available from http://pauillac.inria.fr/#leifer/. {28, 44}
[Mil94] R. Milner. Action calculi V: reflexive molecular forms.
Third draft; with an appendix by O. Jensen. Available from:
ftp://ftp.cl.cam.ac.uk/users/rm135/ac5.ps.Z, 1994. {23}
[Mil96] R. Milner. Calculi for interaction. Acta Informatica, 33(8):707737, 1996. {23,
25, 40}
RR n° 4395
48 J.J. Leifer
[Mil01] R. Milner. Bigraphical reactive systems: basic theory. Technical Report
523, Computer Laboratory, University of Cambridge, 2001. Available from
http://www.cl.cam.ac.uk/#rm135/. {20, 41, 42, 43, 44}
[MSS00] P. Mateus, A. Sernadas, and C. Sernadas. Precategories for combining proba
bilistic automata. In M. Hofmann, G. Rosolini, and D. Pavlovic, editors, Proc.
CTCS '99, volume 29 of Electronic Notes in Theoretical Computer Science. El
sevier Science, 2000. {9}
[NP96] U. Nestmann and B. C. Pierce. Decoding choice encodings. In CONCUR '96,
Concurrency Theory, 7th International Conference, Pisa, Italy, August 2629,
1996, Proceedings, volume 1119 of Lecture Notes in Computer Science. Springer
Verlag, 1996. {44}
[Sew] P. Sewell. From rewrite rules to bisimulation congruences. Theoretical Computer
Science. To appear. {30, 42}
[TFP99] D. Turi, M. P. Fiore, and G. D. Plotkin. Abstract syntax and variable binding. In
14th Annual Symposium on Logic in Computer Science, 25 July, 1999, Trento,
Italy, pages 193202. IEEE Press, 1999. {43}
[TP97] D. Turi and G. Plotkin. Towards a mathematical operational semantics. In 12th
Annual IEEE Symposium on Logic in Computer Science, Warsaw, Poland, June
29  July 2, 1997, pages 280291. IEEE Press, 1997. {45}
INRIA
Unité de recherche INRIA Rocquencourt
Domaine de Voluceau Rocquencourt BP 105 78153 Le Chesnay Cedex (France)
Unité de recherche INRIA Lorraine : LORIA, Technopôle de NancyBrabois Campus scienti£que
615, rue du Jardin Botanique BP 101 54602 VillerslèsNancy Cedex (France)
Unité de recherche INRIA Rennes : IRISA, Campus universitaire de Beaulieu 35042 Rennes Cedex (France)
Unité de recherche INRIA RhôneAlpes : 655, avenue de l'Europe 38330 MontbonnotStMartin (France)
Unité de recherche INRIA Sophia Antipolis : 2004, route des Lucioles BP 93 06902 Sophia Antipolis Cedex (France)
Éditeur
INRIA Domaine de Voluceau Rocquencourt, BP 105 78153 Le Chesnay Cedex (France)
http://www.inria.fr
ISSN 02496399