A non-interleaving process calculus for multi-party
synchronisation
Paweł Sobociński
ECS, University of Southampton

We introduce the wire calculus. Its dynamic features are inspired by Milner’s CCS: a unary prefix operation, binary choice and a standard recursion construct. Instead of an interleaving parallel
composition operator there are operators for synchronisation along a common boundary (;) and noncommunicating parallel composition (⊗) . The (operational) semantics is a labelled transition system
obtained with SOS rules. Bisimilarity is a congruence with respect to the operators of the language.
Quotienting terms by bisimilarity results in a compact closed category.

Introduction
Process calculi such as CSP, SCCS, CCS and their descendants attract ongoing theoretical attention because of their claimed status as mathematical theories for the study of concurrent systems. Several concepts have arisen out of their study, to list just a few: various kinds of bisimulation (weak, asynchronous,
etc.), various reasoning techniques and even competing schools of thought (‘interleaving’ concurrency
vs ‘true’ concurrency).
The wire calculus does not have a CCS-like interleaving ‘k’ operator; it has operators ‘⊗’ and ‘;’
instead. It retains two of Milner’s other influential contributions: (i) bisimilarity as extensional equational
theory for observable behaviour, and (ii) syntax-directed SOS. The result is a process calculus which is
‘truly’ concurrent, has a formal graphical representation and on which ‘weak’ bisimilarity agrees with
‘strong’ (ordinary) bisimilarity.
The semantics of a (well-formed) syntactic expression in the calculus is a labelled transition system
(LTS) with a chosen state and with an associated sort that describes the structure of the labels in the LTS.
In the graphical representation this is a ‘black box’ with a left and a right boundary, where each boundary
is simply a number of ports to which wires can be connected. Components are connected to each other
by ‘wires’—whence the name of the calculus. The aforementioned sort of an LTS prescribes the number
of wires that can connect to each of the boundaries.
Notationally, transitions have upper and lower labels that correspond, respectively, to the left and the
right boundaries. The labels themselves are words over some alphabet Σ of signals and an additional
symbol ‘ι’ that denotes the absence of signal.
The operators of the calculus fall naturally into ‘coordination’ operators for connecting components
and ‘dynamic’ operators for specifying the behaviour of components. There are two coordination operators, ‘⊗’ and ‘;’. The dynamic operators consist of a pattern-matching unary prefix, a CSP-like choice
operator and a recursion construct. Using the latter, one can construct various wire constants, such as
different kinds of forks. These constants are related to Bruni, Lanese and Montanari’s stateless connectors [5] although there they are primitive entities; here they are expressible using the primitive operations
of the calculus.
The wire calculus draws its inspiration form many sources, the two most relevant ones come from
the model theory of processes: tile logic [6] and the Span(Graph) [7] algebra. Both frameworks are
F. Bonchi, D. Grohmann, P. Spoletini, and E. Tuosto:
ICE’09 Structured Interactions
EPTCS 12, 2009, pp. 87–98, doi:10.4204/EPTCS.12.6

c Paweł Sobociński
This work is licensed under the
Creative Commons Attribution License.

88

A non-interleaving process calculus for multi-party synchronisation

aimed at modeling the operational semantics of systems. Tile logic inspired the use of doubly-labeled
transitions, as well as the use of specific rule formats in establishing the congruence property for bisimilarity. Work on Span(Graph) informs the graphical presentation adopted for the basic operators of the
wire calculus and inspired the running example. Similarly, Abramsky’s interaction categories [1] are a
related paradigm: in the wire calculus, processes (modulo bisimilarity) are the arrows of a category and
sequential composition is interaction. There is also a tensor product operation, but the types of the wire
calculus have a much simpler structure.
One can argue, however, that the wire calculus is closer in spirit to Milner’s work on process algebra than the aforementioned frameworks. The calculus offers a syntax for system specification. The
semantics is given by a small number of straightforward SOS rules. No structural equivalence (or other
theory) is required on terms: the equational laws among them are actually derived via bisimilarity. The
fact that operations built up from the primitive operators of the wire calculus preserve bisimilarity means
that there is also a shared perspective with work on SOS formats [2] as well as recent work on SOS-based
coordination languages [3].
An important technical feature is the reflexivity of labelled transition systems—any process can always ‘do nothing’ (and by doing so synchronise with ι’s on its boundaries). This idea is also important
in the Span(Graph) algebra; here it ensures that two unconnected components are not globally synchronised. The wire calculus also features ι-transitivity which ensures that unconnected components
are not assumed to run at the same speeds and that internal reduction is unobservable. Reflexivity and ιtransitivity together ensure that weak and strong bisimilarities coincide—they yield the same equivalence
relation on processes.
Structure of the paper. The first two sections are an exposition of the syntax and semantics of the
wire calculus. In §3 we model a simple synchronous circuit. The next two sections are devoted to the
development of the calculus’ theory and §6 introduces a directed variant.

1

Preliminaries

A wire sort Σ is a (possibly infinite) set of signals. Let ι be an element regarded as “absence of signal”,
with ι ∈
/ Σ. In order to reduce the burden of bureaucratic overhead, in this paper we will consider calculi
with one sort. The generalisation to several sorts is a straightforward exercise.
Before introducing the syntax of the calculus, let us describe those labelled transition systems (LTSs)
that will serve as the semantic domain of expressions: (k, l)-components. In the following #a means the
length of a word a. We shall use ι for words that consist solely of ι’s.
def

Definition 1 (Components). Let L = Σ + {ι} and k, l ≥ 0. A (k, l)-transition is a labelled transition
a
of the form −
→
where a, b ∈ L∗ , #a = k and #b = l. A (k, l)-component C is a pointed, reflexive and
b
ι-transitive LTS (v0 ,V, T ) of (k, l)-transitions. The meanings of the adjectives are:
• Pointed: there is a chosen state v0 ∈ V ;
ι

• Reflexive: for all v ∈ V there exists a transition v −
→
v;
ι

• ι-Transitive: if v −
→
v1 , v1 −
→
v2 and v2 −
→
v0 then also v −
→
v0 .
ι
ι
b
b
To the right is a graphical rendering of C ; a box with k wires on the left and l k { v0
}l
wires on the right:
When the underlying LTS is clear from the context we often identify a component with its chosen
state, writing v0 : (k, l) to indicate that v0 is (the chosen state of) a (k, l)-component.
ι

a

ι

a

..
.

..
.

Paweł Sobociński

89

Definition 2 (Bisimilarity). For two (k, l)-components C , C 0 , a simulation from C to C 0 is a relation
a
a
S that contains (v0 , v00 ) and satisfies the following: if (v, w) ∈ S and v −
→
v0 then ∃w0 s.t. w −
→
w0 and
b
b
(v0 , w0 ) ∈ S. A bisimulation is a relation S such that itself and its inverse S−1 are both simulations. We
say that C , C 0 are bisimilar and write C ∼ C 0 when there is some bisimulation relating C and C 0 .
Remark 3. One pleasant feature of reflexive and ι-transitive transition systems is that weak bisimilarity
agrees with ordinary (“strong”) bisimilarity, where actions labelled solely with ι’s are taken as silent.
Indeed, ι-transitivity implies that any weak (bi)simulation in the sense of Milner [9] is also an ordinary
(bi)simulation.

2

Wire calculus: syntax and semantics

The syntax of the wire calculus is given in (1) and (2) below:
P ::= Y | P ; P | P ⊗ P |

M
MP

| P + P | µY : τ. P

M ::= ε | x | λ x | ι | σ ∈ Σ | MM

(1)
(2)

All well-formed wire calculus terms have an associated sort (k, l) where k, l ≥ 0. We let τ range over
sorts. The semantics of τ-sorted expression is a τ-component. There is a sort inference system for the
syntax presented in Fig. 1. In each rule, Γ denotes the sorting context: a finite set of (i) process variables
with an assigned sort, and (ii) signal variables. We will consider only those terms t that have a sort
derived from the empty sorting context: i.e. only closed terms.
The syntactic categories in (1) are, in order: process variables, composition, tensor, prefix, choice
and recursion. The recursion operator binds a process variable that is syntactically labelled with a sort.
When we speak of terms we mean abstract syntax where identities of bound variables are ignored. There
are no additional structural congruence rules. In order to reduce the number of parentheses when writing
wire calculus expressions, we shall assume that ‘⊗’ binds tighter than ‘;’.
The prefix operation is specific to the wire calculus and merits an extended explanation: roughly, it
is similar to input prefix in value-passing CCS, but has additional pattern-matching features. A general
u
prefix is of the form v P where u and v are strings generated by (2): ε is the empty string, x is a free
occurrence of a signal variable from a denumerable set x = {x, y, z, . . . } of signal variables (that are
disjoint from process variables), λ x is the binding of a signal variable, ι is ‘no signal’ and σ ∈ Σ is a
signal constant. Note that for a single variable x, ‘λ x’ can appear several times within a single prefix.
Prefix is a binding operation and binds possibly several signal variables that appear freely in P; a variable
u
x is bound in P precisely when λ x occurs in u or v. Let bd( v ) denote the set of variables that are bound
u
u
by the prefix, i.e. x ∈ bd( v ) ⇔ λ x appears in uv. Conversely, let f r( v ) denote the set of variables that
appear freely in the prefix.
When writing wire calculus expressions we shall often omit the sort of the process variable when
def
writing recursive definitions. For each sort τ there is a term 0τ = µY : τ.Y . We shall usually omit the
subscript; as will become clear below, 0 has no non-trivial behaviour.
The operations ‘;’ and ‘⊗’ have graphical representations that are convenient for modelling physical
systems; this is illustrated below.

..
.

P

..
.

R

..
.

P

..
.

..
.

Q

..
.

..
.

90

A non-interleaving process calculus for multi-party synchronisation
Γ ` P : (k, n)

Γ ` R : (n, l)

Γ ` P : (k, l)

Γ ` P;R : (k, l)

Γ, X:τ ` X : τ

Γ,Y :τ 0 ` P : τ

Γ ` P⊗Q : (k+m, l+n)

#u=k, #v=l, f r( uv )∩bd( uv )=∅, f r( uv )⊆Γ
Γ`

Γ ` Q : (m, n)

Γ, bd( uv ) ` P : (k, l)

Γ ` µY :τ 0 . P : τ

Γ ` P:τ

u
v P : (k, l)

Γ ` Q:τ

Γ ` P+Q : τ

Figure 1: Sorting rules.
P−
→P

P−
→
R
ι

(R EFL )

a

R−
→
Q
b

P−
→
Q
b

a

P−
→
Q
c

c

R−
→
S
b

a

P;R −
→
Q;S
b

u
vP

−−
→ P|σ
v|σ

(P REF )

(C UT )

P[µY. P/Y ] −
→
Q
b
a

µY. P −
→
Q
b

P−
→
R
b

(ι L)
P−
→
Q
b

a

ac

(T EN )
a

ι

P−
→
Q R−
→
S
ι
ι
ι
ι

(ι R)

c

R−
→
S
d

P⊗R −
→ Q⊗S
bd

ι

(R EC )

ι

R−
→
Q
ι

P−
→
Q
b

a

a

u|σ

a

a

ι

ι
ι

P+R −
→ Q+S

P−
→
Q
b

(+ι )

(ab6=ι)
a

P+R −
→
Q
b

(+L)

Figure 2: Semantics of the wire calculus. Symmetric rule (+R) omitted.
The semantics of a term t : (k, l) is the (k, l)-component with LTS defined using SOS rules: (R EFL ),
and (R EC ) of Fig. 2. The rules (R EFL ), (ι L) and (ι R) guarantee
that the LTS satisfies reflexivity and ι-transitivity of Definition 1. Note that while any calculus with
global rules akin to (R EFL ), (ι L), (ι R) for ‘silent’ actions is automatically ι-transitive and reflexive with
the aforementioned result on bisimilarity (Remark 3), there are deeper reasons for the presence of these
rules: see Remark 5.
The rules (C UT ) and (T EN ) justify the intuition that ‘;’ is synchronisation along a common boundary
u
u
and ‘⊗’ is parallel composition sans synchronisation. For a prefix v P a substitution is a map σ : bd( v ) →
u
Σ + {ι}. For a term t with possible free occurrences of signal variables in bd( v ) we write t|σ for the term
u
resulting from the substitution of σ (x) for x for each x ∈ bd( v ). Assuming that u, v have no free signal
variables, we write u|σ , v|σ for the strings over Σ + {ι} that result from replacing each occurrence of
‘λ x’ with σ (x). The SOS rule that governs the behaviour of prefix is (P REF ), where σ is any substitution.
The choice operator + has a similar semantics to that of the CSP choice operator ‘@’, see for instance [4]:
a choice is made only on the occurrence of an observable action. Rules (+ι ), (+L) and (+R) make this
statement precise. The recursion construct and its SOS rule (R EC ) are standard. We assume that the
substitution within the (R EC ) rule is non-capturing.
As first examples of terms we introduce two wire constants1 , their graphical representations as well
as an SOS characterisation of their semantics.
(ι L), (ι R), (C UT ), (T EN ), (P REF ), (+ι ), (+L), (+R)

def

λx

I = µY. λ x Y : (1, 1)
def

λ xλ y

X = µY. λ yλ x Y : (2, 2)

a

I−
→
I
a
ab

(I D )

X −ba
→X

(T W )

Remark 4. Wire constants are an important concept of the wire calculus. Because they have a single
state, any expression built up from constants using ‘;’ and ‘⊗’ has a single state. Bisimilar wirings can
1 Those

terms whose LTS has a single state.

Paweł Sobociński

91

thus be substituted in terms not only without altering externally observable behaviour, but also without
combinatorially affecting the (intensional) internal state.

3

Global synchrony: flip-flops

As a first application of the wire calculus, we shall model the following circuit2 :
F0

F1

(3)

F0

where the signals that can be sent along the wire are {0, 1} (n.b. 0 is not the absence of signal, that is
represented by ι). The boxes labelled with F0 and F1 are toggle switches with one bit of memory, the
state of which is manifested by the subscript. They are simple abstraction of a flip-flop. The switches
synchronise to the right only on a signal that corresponds to their current state and change state according
to the signal on the left. The expected behaviour is a synchronisation of the whole system — here
a tertiary synchronisation. In a single “clock tick” the middle component will change state to 0, the
rightmost component to 1 and the leftmost component will remain at 0. F0 and F1 are clearly symmetric
and their behaviour is characterised by the SOS rules below (where i ∈ {0, 1}) .
i

Fi →
−i Fi

(iSETi)

1−i

Fi −−
→ F1−i
i

(iSET1 − i)

ι

Fi −
→
Fi
ι

(iR EFL )

In the wire calculus F0 and F1 can be defined by the terms:
def

0

1

1

def

0

1

0

0

1

F0 = µY. 0 Y + 0 µZ. ( 1 Z + 1 Y ) and F1 = µZ. 1 Z + 1 µY. ( 0 Y + 0 Z).
In order to give an expression for the whole circuit, we need two additional wire constants d and e.
They are defined below, together with a graphical representation and an SOS characterisation. Their
mathematical significance will be explained in Section 5.
def

d : (0, 2) = µY. λ xλ x Y
def

e : (2, 0) = µY.

λ xλ x

Y

d→
−
d
aa
aa

e −→ e

(d)

(e)

Returning to the example, the wire calculus expression corresponding to (3) can be written down in the
wire calculus by scanning the picture from left to right.
def

A = d ; (I ⊗ (F0 ; F1 ; F0 )) ; e.
What are its dynamics? Clearly A has the sort (0, 0). It is immediate that any two terms of this sort are
extensionally equal (bisimilar) as there is no externally observable behaviour. This should be intuitively
obvious because A and other terms of sort (0, 0) are closed systems; they have no boundary on which
an observer can interact. We can, however, examine the intensional internal state of the system and the
possible internal state transitions. The semantics is given structurally in a compositional way – so any
2 This

example was proposed to the author by John Colley.

92

A non-interleaving process calculus for multi-party synchronisation

non-trivial behaviour of A is the result of non-trivial behaviour of its components. Using
possible behaviour of F0 ; F1 is of the form (i) below.
x

F0 −
→
X
z

z

x

F1 −
→
Y
y

F0 ;F1 −
→
X;Y
y

0

x

F0 −
→
X
0

(C UT )

x

F1 −
→
F0
1

→
X;F0
F0 ;F1 −
1

(i)

x

→
X;F0
F0 ;F1 −
1

(C UT )

x

(C UT )

the only

1

→
F1
F0 −
0

→
X;F0 ;F1
F0 ;F1 ;F0 −
0

(ii)

(C UT )

(iii)

The dynamics of F0 and F1 imply that z = 0 and y = 1, and the latter also implies that Y = F0 , hence the
occurrence of (C UT ) must be of the form (ii) above. Composing with F0 on the right yields (iii).
wx

I⊗(F0 ;F1 ;F0 ) −w0
→ I⊗(X;F0 ;F1 )

(⊗)

(iv)

Next, tensoring with I yields (iv) above. In order for (C UT ) to apply after post-composing with e, w must
be equal to 0, yielding (iv) below.
0x

(I⊗(F0 ;F1 ;F0 ));e −→ (I⊗(X;F0 ;F1 ));e

(C UT )

d;(I⊗(F0 ;F1 ;F0 ));e →
− d;(I⊗(F0 ;F0 ;F1 ));e

(iv)

(C UT )

(v)

The final application of (C UT ) forces x = 0 and hence X = F0 , resulting in (v). It is easy to repeat this
argument to show that the entire system has three states — intuitively ‘1 goes around the ring’. It is
equally easy to expand this example to synchronisations that involve arbitrarily many components. Such
behaviour is not easily handled using existing process calculi.
Remark 5. Consider the wire calculus expression represented by (†).
F0

F1

F0

F0

(†)
F1

The two components are unconnected. As a consequence of (R EFL ) and (T EN ), a “step” of the entire system
is either a (i) step of the upper component, (ii) step of the lower component or (iii) a ‘truly-concurrent’
step of the two components. The presence of the rules (ι L) and (ι R) then ensures that behaviour is not
scheduled by a single global clock — that would be unreasonable for many important scenarios. Indeed,
in the wire calculus synchronisations occur only between explicitly connected components.

4

Properties

In this section we state and prove the main properties of the wire calculus: bisimilarity is a congruence
and terms up-to-bisimilarity are the arrows of a symmetric monoidal category W . In fact, this category
has further structure that will be explained in section 5.
ak
ak
a1
Let P ( −b→
) Q denote trace P −b→
P1 · · · Pk−1 −b→
Q, for some P1 , . . . , Pk−1 .
1
k

k

Lemma 6. Let P : (k, l) and Q : (l, m), then:

(i) If P ; Q −
→
R then R = P0 ; Q0 and there exist traces
b
a

P(−
→
) Pk −
→
Pl0 ( −
→
) P0 ,
c
el
d
ι

k

a

ι

d

e

k
l
Q ( −→
) Qk −
→
Q0l ( −→
) Q0 ;
ι
ι
b
c

Paweł Sobociński

93

(ii) If P ⊗ Q −
→
R then R = P0 ⊗ Q0 and there exist transitions:
b
a

a

1
P −b→
P0 ,
1

a

2
Q −b→
Q0 with a = a1 a2 and b = b1 b2 .
2
a

Proof. Induction on the derivation of P ; Q −
→
R. The base cases are: a single application of (C UT )
b
a
c
0
0
0
0
whence P −
→
P and Q −
→
Q and R = P ; Q , and a single application of (R EFL ) whence R = P ; Q but by
c
b
ι
ι
reflexivity we have also that P −
→
P and Q −
→
Q. The first inductive step is an application of (ι L) where
ι
ι
ι
a
P;Q −
→
R
and
R
−
→
S.
Applying
the
inductive
hypothesis to the first transition we get R = P00 ; Q00
ι
b
a
and suitable traces. Now we apply the inductive hypothesis again to R00 ; Q00 −
→
S and obtain S = P0 ; Q0
b
together with suitable traces. The required traces are obtained by composition in the obvious way. The
second inductive step is an application of (ι R) and is symmetric. Part (ii) involves a similar, if easier,
induction.
Theorem 7 (Bisimilarity is a congruence). Let P, Q : (k, l), R : (m, n), S : (l, l 0 ) and T : (k0 , k) and suppose
that P ∼ Q. Then:
(i) P ; S ∼ Q ; S and T ; P ∼ T ; Q;

(ii) P ⊗ R ∼ Q ⊗ R and R ⊗ P ∼ R ⊗ Q;
(iii)

u
vP

u

∼ v Q;

(iv) P + R ∼ Q + R and R + P ∼ R + Q.
Proof. Part (i) follows easily from the conclusion of Lemma 6, (i); in the first case one shows that
def
a
A = { (P ; R, Q ; R) | P, Q : (k, l), R : (l, m), P ∼ Q } is a bisimulation. Indeed, if P ; R −
→
P0 ; R0 then
b
0
0
0
there exists an appropriate trace from P to P and from R to R . As P ∼ Q, there exists Q with P0 ∼ Q0
a
and an equal trace from Q to Q0 . We use the traces from Q and R to obtain a transition Q ; R −
→
Q0 ; R0
b
0
0
0
0
via repeated applications of (C UT ) and (ι L,R). Clearly (P ; R , Q ; R ) ∈ A. Similarly, (ii) follows from
Lemma 6, (ii); (iii) and (iv) are straightforward.
λ x ...λ x

def

def

λ x ...λ x λ y ...λ y

Let Ik = µY. λ x11 ...λ xkk Y and Xk, l = µY. λ y11 ...λ ykl λ x11...λ xkl Y . Xk, l is drawn as

k{

..
.

..
.

}l

l{

..
.

..
.

}k

.

Lemma 8 (Categorical axioms). In the statements below we implicitly universally quantify over all
k, l, m, n, u, v ∈ N, P : (k, l), Q : (l, m), R : (m, n), S : (n, u) and T : (u, v).
(i) (P ; Q) ; R ∼ P ; (Q ; R);

(ii) P ; Il ∼ P ∼ Ik ; P;

(iii) (P ⊗ R) ⊗ T ∼ P ⊗ (R ⊗ T );

(iv) (P ⊗ S) ; (Q ⊗ T ) ∼ (P ; Q) ⊗ (S ; T );



(v) (P ⊗ R) ; Xl,n ∼ Xk,m ; (R ⊗ P);

(vi) Xk,l ; Xl,k ∼ Ik+l .

..
.

P

..
.

..
.

..
.

R

..
.

..
.

∼

..
.

..
.

R

..
.

..
.

..
.

P

..
.



Proof. (i) Here we use Lemma 6, (ii) to decompose a transition from (P ; Q) ; R into traces of P, Q and
a
R and then, using reflexivity, compose into a transition of P ; (Q ; R). Indeed, suppose that (P ; Q) ; R −
→
b
(P0 ; Q0 ) ; R0 . Then:
P ; Q (−
→
) Pk ; Qk
d
ι

i

a

−
→
c

d

i
Pl0 ; Q0l ( −
→
) P0 ; Q0 and R ( −→
) Rk
ei
ι
ι

c

−
→
b

e

i
R0l ( −
→
) R0 .
ι

94

A non-interleaving process calculus for multi-party synchronisation

Decomposing the first trace into traces of P and Q yields
P(−
→
) P1k1 −
→
) P1 · · · Pk ( −
→
)−
→
→
P1l0 1 ( −
(−
→
) Pl0 · · · P0
e1i
c1
d
c0
d0
e0
ι

ι

ι

a

ι

1i

i

ι

i

c

d1i
ι

d0

e

c0

e0

1
1i
i
i
Q01l1 ( −
→
) Q1 · · · Qk ( −
and Q ( −→ ) Q1k1 −d→
→
)−
→
(−
→
) Q0l · · · Q0 .
ι
ι
c
ι
1

Using reflexivity and (C UT ) we obtain
d

c

d0

e

e0

c0

1i
1
1i
i
i
Q ; R ( −−→
) Q1k1 ; R −→
Q01l1 ; R1 ( −→
) Q1 ; R1 · · · Qk ; Rk ( −→
)−
→
(−
→
) Q0l ; R0l · · · Q0 ; R0 .
ι
ι
ι
ι
ι
b

Now by repeated applications of (C UT ) followed by (ι L,R) we obtain the required transition P ; (Q ; R) −
→
b
0
0
0
P ; (Q ; R ). Similarly, starting with a transition from P ; (Q ; R) one reconstructs a matching transition
from (P ; Q) ; R.
aa0
Parts (ii) and (iii) are straightforward. For (iv), a transition (P ⊗ R) ; (Q ⊗ S) −−
→ (P0 ⊗ R0 ) ; (Q0 ⊗
bb0
0
S ) decomposes first into traces:
a

aa0

P ⊗ R ( d−
→
) Pk ⊗ Rk −−
→ Pl0 ⊗ R0l ( −
→
) P0 ⊗ R0
cc0
d0
e e0
ι

ι

i i

i i

di d0

ei e0

cc0

i
i
→ Q0l ⊗ Sl0 ( −−ι→
Q ⊗ S ( −−ι→
) Qk ⊗ Sk −−
) Q0 ⊗ S0
bb0

and then into individual traces of P, R, Q and S:
P(−
→
) Pk −
→
Pl0 ( −
→
) P0
c
ei
d
a

ι

ι

i

d

ι

i

i

d0

e

c0

e0

i
i
→
Sl0 ( −
→
) S0
S ( −→
) Sk −
ι
ι
b0

i
i
→
Q0l ( −
→
) Q0
Q ( −→
) Qk −
ι
ι
b
c

a0

R(−
→
) Rk −→
R0l ( −
→
) R0
c0
d0
e0

ι

a0

and hence transitions P ; Q −
→
P0 ; Q0 and R ; S −→
R0 ; S0 , which combine via a single application of
b
b0
a

aa0

→ (P0 ; Q0 ) ⊗ (R0 ; S0 ). The converse is similar. Parts (v) and (vi) are
to give (P ; Q) ⊗ (R ; S) −−
bb0
trivial.
(⊗)

As a consequence of (i) and (ii) there is a category W that has the natural numbers as objects and
terms of sort (k, l) quotiented by bisimilarity as arrows from k to l; for P : (k, l) let [P] to denote P’s
equivalence class wrt bisimilarity – then [P] : m → n is the arrow of W . The identity morphism on
m is [Im ]. Composition [P] : k → l with [Q] : l → m is [P ; Q] : k → m.3 Parts (iii) and (iv) imply
def

that W is monoidal with a strictly associative tensor. Indeed, on objects let m ⊗ n = m + n and on
def
arrows [P] ⊗ [Q] = [P ⊗ Q].4 The identity for ⊗ is clearly 0. Subsequently (v) and (vi) imply that
W is symmetric monoidal. Equations (i)–(iv) also justify the use of the graphical syntax: roughly,
rearrangements of the representation in space result in syntactically different but bisimilar systems.

5

Closed structure

Here we elucidate the closed structure of W : the wire constants d and e play an important role.

Lemma 9. d ⊗ I ; I ⊗ e ∼ I ∼ I ⊗ d ; e ⊗ I
∼
∼
.
3 Well-defined
4 Well-defined

due to Theorem 7.
due to Theorem 7.

Paweł Sobociński

95

Given k ∈ N, define recursively
d1

def

= d and dn+1

def

= d ; I ⊗ dn ⊗ I and dually e1

def

= e and en+1

def

= In ⊗ e ⊗ In ; en .

def

Let d0 , e0 = I0 = 0.
Lemma 10. For all n ∈ N, dn ⊗ In ; In ⊗ en ∼ In ∼ In ⊗ dn ; en ⊗ In .
Proof. For n = 0 the result is trivial. For n = 1, it is the conclusion of Lemma 9. For n > 1 the result
follows by straightforward inductions:
dn+1 ⊗ In+1 ; In+1 ⊗ en+1

= (d ; I ⊗ dn ⊗ I) ⊗ In+1 ; In+1 ⊗ (In ⊗ e ⊗ In ; en )

∼ d ⊗ In+1 ; I ⊗ dn ⊗ In+2 ; I2n+1 ⊗ e ⊗ In ; In+1 ⊗ en

∼ d ⊗ In+1 ; I ⊗ e ⊗ In ; I ⊗ dn ⊗ In ; In+1 ⊗ en

∼ (d ⊗ I ; I ⊗ e) ⊗ In ; I ⊗ (dn ⊗ In ; In ⊗ en )

∼ In+1

In+1 ⊗ dn+1 ; en+1 ⊗ In+1

= In+1 ⊗ (d ; I ⊗ dn ⊗ I) ; (In ⊗ e ⊗ In ; en ) ⊗ In+1

∼ In+1 ⊗ d ; In+2 ⊗ dn ⊗ I ; In ⊗ e ⊗ I2n+1 ; en ⊗ In+1

∼ In+1 ⊗ d ; In ⊗ e ⊗ I ; In ⊗ dn ⊗ I ; en ⊗ In+1

∼ In ⊗ (I ⊗ d ; e ⊗ I) ; (In ⊗ dn ; en ⊗ In ) ⊗ I

∼ In+1

With Lemma 10 we have shown that W is a compact-closed category [8]. Indeed, for all n ≥ 0 let
n; we have shown the existence of arrows

def
n? =

[dn ] : 0 → n ⊗ n?

[en ] : n? ⊗ n → 0

(4)

that satisfy [dn ] ⊗ idn ; In ⊗ [en ] = In = idn ⊗ [dn ] ; [en ] ⊗ In .5
While the following is standard category theory, it may be useful for the casual reader to see how this
data implies a closed structure. For W to be closed wrt ⊗ we need, for any l, m ∈ W an object l ( m
and a term
evl,m : ((l ( m) ⊗ l, m)

that together satisfy the following universal property: for any term P : (k ⊗ l, m) there exists a unique
(up to bisimilarity) term Cur(P) : (k, l ( m) such that the diagram below commutes:
O

[Cur(P)⊗Il ]

k⊗l

[evl,m ]

/
t9 m
tt
t
t
tt
tt [P]
t
t

(l ( m) ⊗ l

5 The (−)? operation on objects of W may seem redundant at this point but it plays a role when considering the more
elaborate sorts of directed wires in §6.

96

A non-interleaving process calculus for multi-party synchronisation
def

def

def

Owing to the existence of dn and en we have l ( m = m+l, evl,m = Im ⊗ el and Cur(P) = Ik ⊗ dl ; P ⊗ Il .
Indeed, it is easy to verify universality: suppose that there exists Q : (k, m+l) such that Q ⊗ Il ; evl,m ∼ P.
Then
Cur(P) = Ik ⊗ dl ; P ⊗ Il

∼ Ik ⊗ dl ; (Q ⊗ Il ; evl,m ) ⊗ Il

∼ Ik ; Q ; Im ⊗ (Il ⊗ dl ; el ⊗ Il )

∼Q

Starting from the situation described in (4) and using completely general reasoning, one can define a
contravariant functor (−)? : W op → W by A 7→ A? on objects and mapping f : A → B to the composite
B? ⊗ f ⊗A?

B? ⊗d

e ⊗A?

A
B
B? −−−−→
B? ⊗ A ⊗ A? −−−−−→ B? ⊗ B ⊗ A? −−
−→ A? .

Indeed, the fact that (−)? preserves identities is due to one of the triangle equations and the fact that
it preserves composition is implied by the other. We can describe (−)? on W directly as the up-tobisimulation correspondent of a structurally recursively defined syntactic transformation that, intuitively,
rotates a wire calculus term by 180 degrees. First, define the endofunction (−)? on strings generated
by (2) to be simple string reversal (letters are either free variables, bound variables, signals or ‘ι’).
Definition 11. Define an endofunction (−)? on wire calculus terms by structural recursion on syntax as
follows:
def

def

(R ; S)? = S? ; R?
u

def v? ?
u? R

( v R)? =

(R ⊗ S)? = S? ⊗ R?
def

(R + S)? = R? + S?

def

(µY. R)? = µY. R?

Notice that d? = e and, by a simple structural induction, P?? = P. This operation is compatible with
d and e in the following sense.
Lemma 12. Suppose that P : (k, l). Then dk ; P ⊗ Ik ∼ dl ; Il ⊗ P? . Dually, P ⊗ Il ; el ∼ Ik ⊗ P? ; ek .
The conclusion of the following lemma implies that for any k, l ≥ 0 one can define a function (−)? :
def

W (k, l) → W (l, k) by setting [P]? = [P? ].

b?

Lemma 13. If P : (k, l) then P? : (l, k). Moreover P −
→
R iff P? −a→
R? . Consequently P ∼ Q iff
?
b
P? ∼ Q? .
a

Proof. Structural induction on P.
Moreover, by definition we have:
([P]; [Q])? = [P ; Q]? = [(P ; Q)? ] = [Q? ; P? ] = [Q? ] ; [P? ] = [Q]? ; [P]?
and [Ik ]? = [Ik ], thus confirming the functoriality of (−)? : W op → W .

Paweł Sobociński

6

97

Directed wires

In the examples of §3 there is a suggestive yet informal direction of signals: the components set their state
according to the signal coming in on the left and output a signal that corresponds to their current state
on the right. It is useful to make this formal so that systems of components are not wired in unintended
ways. Here we take this leap, which turns out not to be very difficult. Intuitively, decorating wires with
directions can be thought as a type system in the sense that the underlying semantics and properties are
unchanged, the main difference being that certain syntactic phrases (ways of wiring components) are no
longer allowed.
def

def

Definition 14 (Directed components). Let D = {L, R} and subsequently Ld = (Σ + {ι}) × D. Abbrevi−
−
ate (a, L) ∈ Ld by ←
a and (a, R) by →
a . Let π : Ld → D be the obvious projection.
a
∗
Let k, l ∈ D . A (k, l)-transition is a labelled transition of the form −
→
where a, b ∈ Ld∗ , π ∗ (a) = k
b
∗
and π (b) = l. A (k, l)-component C is a pointed, reflexive and ι-transitive LTS (v0 ,V, T ) of (k, l)transitions.
The syntax of the directed version of the wire calculus is obtained by replacing (2) with (5) below:
signals are now either inputs (?) or outputs (!).
M ::= ε | D | MM

(5)

D ::= A? | A!
A ::= x | λ x | ι | σ ∈ Σ
def

def

def

def

Define a map (−) : D ∗ → D ∗ in the obvious way by letting L = R and R = L. Now define a function

d from terms generated by (5) to D ∗ recursively by letting d(ε) = ε, d(uv) = d(u)d(v), d(x?) = L and
d(x!) = R. The terms are sorted with the rules in Fig. 1, after replacing the rule for prefix with the
following:
du=k, dv=l, f r( uv )∩bd( uv )=∅, f r( uv )⊆Γ

Γ, bd( uv ) ` P : (k, l)

Γ ` uv P : (k, l)

The semantics is defined with the rules of Fig. 2 where labels are strings over Ld and (P REF ) is replaced
with ( D P REF ) below. In the latter rule, given a substitution σ , let eσ be the function that takes a prefix
component generated by (5) with no occurrences of free signal variables to Ld∗ , defined by recursion in
the obvious way from its definition on atoms: eσ (λ x?) = (σ x, L), eσ (λ x!) = (σ x, R), eσ (a?) = (a, L),
eσ (a!) = (a, R). Abusing notation, let (−) be the endofunction of Ld∗ that switches directions of components. Then:
u
vP

e u

σ
−−
→ P|σ
eσ v

( D P REF )

Below are some examples of wire constants in the directed variant of the calculus:
def

λ x!

IL = µY. λ x? Y : (L, L)

←
−
a

IL −←
→
− IL

(IL )

a

def

λ x?

IR = µY. λ x! Y : (R, R)

→
−
a

IR −→
→ IR
−

(IR )

a

def

dL = µY. λ x?λ x! Y : (ε, LR)

dL −←
−
→ dL
−→
−
a a

(dL )

98

A non-interleaving process calculus for multi-party synchronisation

def

eL = µY.

λ x?λ x!

Y : (RL, ε)

→
−
−
a←
a

eL −
−−→ eL

(eL )

At this point the Fx components of §3 can modelled in the directed wire calculus. The results of §4 and
§5 hold mutatis mutandis with the same proofs – this is not surprising as only the semantics of prefix and
the structure of sorts is affected.

7

Conclusion and future work

As future work, one should take advantage of the insights of Selinger [10]: it appears that one can
express Selinger’s queues and buffers within the wire calculus and thus model systems with various
kinds of asynchronous communication. Selinger’s sequential composition, however, has an interleaving
semantics.
From a theoretical point of view it should be interesting to test the expressivity of the wire calculus
with respect to well-known interleaving calculi such as CCS and non-syntactic formalisms such as Petri
nets.
Acknowledgement. The author thanks the anonymous referees and the participants in the ICE forum
for their suggestions, many of which have improved the paper. Early discussions with R.F.C. Walters
and Julian Rathke were fundamental in stabilising the basic technical contribution. Special thanks go to
Fabio Gadducci and Andrea Corradini.

References
[1] Samson Abramsky, Simon Gay & Rajogopal Nagarajan (1995): Interaction Categories and the Foundations
of Typed Concurrent Programming. In: Proceedings of the 1994 Marktoberdorf Summer School, NATO ASI
Series F. Springer.
[2] Luca Aceto, Willem Jan Fokkink & Chris Verhoef (1999): Structural Operational Semantics. In: Bergstra,
Ponse & Smolka, editors: Handbook of Process Algebra. Elsevier.
[3] Simon Bliudze & Joseph Sifakis (2008): A Notion of Glue Expressiveness for Component-Based Systems.
In: Proceedings of the 19th International Conference on Concurrency Theory (CONCUR’08), LNCS 5201.
Springer, pp. 508–522.
[4] Stephen D. Brookes, A. William Roscoe & David J. Walker (1988): An Operational Semantics for CSP.
Manuscript.
[5] Roberto Bruni, Ivan Lanese & Ugo Montanari (2005): Complete Axioms for Stateless Connectors. In: Algebra and Coalgebra in Computer Science, (CALCO ’05), LNCS 3629. pp. 98–113.
[6] Fabio Gadducci & Ugo Montanari (2000): The tile model. In: Proof, Language and Interaction: Essays in
Honour of Robin Milner. MIT Press, pp. 133–166.
[7] Piergiulio Katis, Nicoletta Sabadini & Robert Frank Carslaw Walters (1997): Span(Graph): an algebra of
transition systems. In: Proceedings of 6th International Conference on Algebraic Methodology and Software
Technology (AMAST ’97), LNCS 1349. Springer, pp. 322–336.
[8] G. M. Kelly & M. L. Laplaza (1980): Coherence for compact closed categories. Journal of Pure and Applied
Algebra 19, pp. 193–213.
[9] Robin Milner (1989): A calculus of communicating systems. Prentice Hall.
[10] Peter Selinger (1997): First-order axioms for asynchrony. In: Proceedings of 8th International Conference
on Concurrency Theory, CONCUR ’97, LNCS 1243. Springer, pp. 376–390.

