Synthesising Choreographies from Local Session Types
(extended version)
Julien Lange and Emilio Tuosto

arXiv:1204.2566v1 [] 11 Apr 2012

Department of Computer Science, University of Leicester, UK

Abstract. Designing and analysing multiparty distributed interactions can be
achieved either by means of a global view (e.g. in choreography-based approaches)
or by composing available computational entities (e.g. in service orchestration).
This paper proposes a typing systems which allows, under some conditions, to
synthesise a choreography (i.e. a multiparty global type) from a set of local session types which describe end-point behaviours (i.e. local types).

1

Introduction

Communication-centred applications are paramount in the design and implementation
of modern distributed systems such as those in service-oriented or cloud computing.
Session types [8] and their multiparty variants [7, 9] offer an effective formal framework
for designing, analysing, and implementing this class of applications. Those theories
feature rather appealing methodologies that consists of (i) designing a global view of
the interactions – aka global type –, (ii) effective analysis of such a global view, (iii)
automatic projection of the global view to local end-points – aka local types –, and (iv)
type checking end-point code against local types. Such theories guarantee that, when
the global view enjoys suitable properties (phase (ii)), the end-points typable with local
types enjoy e.g., liveness properties like progress.
A drawback of such approaches is that they cannot be applied when the local types
describing the communication patterns of end-points are not obtained by an a priori
designed global view. For instance, in service-oriented computing, one typically has
independently developed end-points that have to be combined to form larger services.
Hence, deciding if the combined service respects its specification becomes non trivial.
To illustrate this, we introduce a simple example used throughout the paper.
Consider a system SBS = b1 [P1 ] | s1 [S1 ] | b2 [P2 ] | s2 [S2 ] consisting of two buyers
(b1 and b2 ) and two servers (s1 and s2 ) running in parallel, so that
P1 = t1 !order.p1 ?price.r?price.(c1 !.t1 !addr ⊕ c2 !.no1 !)
P2 = t2 !order.p2 ?price.r!price.(c2 ?.t2 !addr + c1 ?.no2 !)
Si = ti ?order.pi !price.(ti ?addr + noi ?), i ∈ {1, 2}

is the behaviour of b1
is the behaviour of b2
is the behaviour of si

with a!e (resp. a?e) representing the action of sending (resp. receiving) a message of
type e on a channel a (we omit e when the message is immaterial), ⊕ representing an
internal choice, and + a choice made by the environment.

Intuitively, the overall behaviour of SBS should be that either b1 or b2 purchase from
their corresponding sellers. A natural question arises: is SBS correct? Arguably, it is not
immediate to decide this by considering the end-point behaviours.
We propose to construct a global view of distributed end-points like SBS by a straightforward extension of the multiparty session types introduced in [9]. Such types formalise a global view of the behaviour which, for SBS , resembles the informal diagram
below, where the choreography of the overall protocol becomes much clearer.

An advantage of our approach is that we can reuse the results of the theory of multiparty session types to prove properties of end-points e.g. safety and progress. In fact,
we show that when the choreography can be constructed, its projections correspond to
the initial end-points. Therefore, the well-formedness of the synthesised global choreography guarantees progress and safety properties of end-points.
The extraction of session types from programs has been studied extensively [6, 8, 9].
We assume in this work that such session types are readily available before addressing
the construction of a global type.
Contributions. We introduce a theory whereby, under some conditions, it is possible to
assign a global type to a set of local types. If a global type can be constructed from a
set of local types, we show that it is unique (Theorem 2) and well-formed (Theorem 3).
In addition, we show that typability is preserved by reduction (Theorem 4). Our theory
also guarantees progress and safety properties (Theorems 5 and 6). We also show that
the projections of a constructed global type are equivalent to the original system (Theorem 7). Finally, we show that for every well-formed global types, an equivalent global
type can be assigned to its projections (Theorem 8).
Synopsis. In § 2, we give the syntax and semantics of the local types from which it is
possible to construct a global type. In § 3, we present an extension of the global types
in [9]. In § 4, we introduce a typing systems for local types, and we give our main
results. Finally, in § 5 we conclude, and discuss related and future work.

2

Local Types

We use CCS-like processes (with guarded external and internal choices) to infer a global
type from local types that correspond to the participants in the inferred choreography.
2

Hereafter, P is a denumerable set of participant names (ranged over by s, r, n, . . . ) and
C is a denumerable set of channel names (ranged over by a, b, . . . ).
Syntax. The syntax of local types below is parametrised wrt basic data types such as
bool, int, . . . (ranged over by e):
S, T

::= S | S0 | n[P] | a : ρ | 0

P, Q

::=

L

i∈I ai !ei .Pi

| ∑i∈I ai ?ei .Pi | µ x.P | x

A system S consists of the parallel composition of processes and queues. A process
n[P] is a behaviour P identified by n ∈ P; we assume that the participant names are all
different. A behaviour is either a guarded external choice, a guarded internal choice,
L
or a recursive process. An internal choice i∈I ai !ei .Pi is guarded by output prefixes
ai !ei representing the sending of a value of sort ei on channel ai . An external choice
∑i∈I ai ?ei .Pi is guarded by input prefixes ai ?ei representing the reception of a value of
type ei on channel ai . We adopt asynchronous (order-preserving) communications and
assume that the channels in the guards of choices are pairwise distinct; moreover
def

=

0

L

i∈∅ ai !ei .Pi

=

∑i∈∅ ai ?ei .Pi

Finally, in a recursive behaviour µ x.P, all occurrences of x in P are bound and prefixguarded; also, we consider closed behaviours only that is, behaviours with no free occurrences of recursion variables. We assume that bound variables are pairwise distinct.
A program is a system with no queues, while a runtime system is a system having
exactly one queue a : ρ per channel name a ∈ C in S. In the following, S, T, . . . denote
either a program or runtime system.
Semantics. The semantics of local types is given by the labelled transition system (LTS)
whose labels are
λ ::= α | X | a · e | e · a | n[α] | n : α

where

α ::= a!e | a?e

Label α indicates either sending or reception by a process. Label X indicates termination, a · e and e · a respectively indicate push and pop operations on queues. Label
n[α] indicates a communication action done by participant n while n : a!e and n : a?e
indicate a synchronisation between n and a queue.
Assume the usual laws for commutative monoids for | and 0 on systems and µ x.P ≡
λ

P[µ x.P/x]. The LTS −→ is the smallest relation closed under the following rules:
[ INT ]
[ PUSH ]

L

i∈I ai !ei .Pi

a·e

n[a?e]

a j ?ej

−→ Pj

a : ρ −→ a : ρ · e

[ EXT ]
[ POP ]

[ OUT ]

n:a?e

e·a

a : e · ρ −→ a : ρ

X

0 −→ 0

[ END ]

P −→ P0
α

T −→ T 0

[ BOX ]

n:a!e

S | T −→ S0 | T 0
λ

α

[ EQ - S ]

P −→ P0
α

S −→ S0
λ

3

n[α]

n[P] −→ n[P0 ]

S ≡ T −→ T 0 ≡ S0

P ≡ Q −→ Q0 ≡ P0
[ EQ - P ]

j∈I

a·e

S −→ S0

T −→ T 0

S | T −→ S0 | T 0

∑i∈I ai ?ei .Pi −→ Pj

n[a!e]

e·a

S −→ S0
[ IN ]

a j !ej

Rules [ INT ] and [ EXT ] are trivial. By [ PUSH ] (resp. [ POP ]), a queue receives a (resp. sends the
first) datum (resp. if any). Processes can synchronise with queues according to rules [ IN ]
and [ OUT ]. The remaining rules are rather standard. Let S −→ iff there are S0 and λ s.t.
λ

λ ...λn

λ

1
S −→ S0 and =⇒
(resp. =⇒) be the reflexive transitive closure of −→ (resp. −→).

3

Global Types

A global type G specifies an ordering of the interactions in a choreography. The syntax
for global types in [9] is extended with a generalised sequencing in the following syntax:

G ::= s → r : ahei.G | G ; G 0 | G + G 0 | G | G 0 | µ χ.G | χ | 0
The prefix s → r : ahei represents an interaction where s ∈ P sends a value of sort e to
r ∈ P on a ∈ C (we let ι range over interactions s → r : ahei and assume that s 6= r). The
production G ; G 0 indicates a generalised form of sequencing, where the interactions in
G 0 are enabled only after the ones in G . The production G + G 0 indicates a (exclusive)
choice of interactions. Concurrent interactions are written G | G 0 . A global type µ χ.G ,
indicates a recursive type, where χ is bound in G . We assume that global types are
closed and that recursion is guarded. We often omit trailing occurrences of 0.
Example 1. The first two interactions between bi and si in the example of § 1 are

Gi = bi → si : ti horderi.si → bi : pi hpricei i ∈ {1, 2}

(3.1)

The type Gi says that a participant bi sends a message of type order to participant si
on channel ti , then si replies with a message of type price on channel pi .

The smallest equivalence relation satisfying the laws for commutative monoids for
| , +, and 0 and the axioms below is the structural congruence for global types:

G ;0 ≡ G
0;G ≡ G
(G ; G 0 ) ; G 00 ≡ G ; (G 0 ; G 00 )
ι.(G ; G 0 ) ≡ (ι.G ) ; G 0
µ χ.G ≡ G [µ χ.G /χ]
The syntax of global types may specify behaviours that are not implementable. The
rest of this section borrows from [5] and [9] and adapts the requirements a global type
must fulfil to ensure that the ordering relation it prescribes is indeed feasible.
3.1

Channel Usage and Linearity

It is paramount that no race occurs on the channels of a global type (i.e. a datum sent
on a channel is received by its intended recipient). As in [9], we require that a global
type is linear, that is actions on channels shared by different participants are temporally
ordered. For this, we use generic environments (ranged over by C) which keep track of
channel usage. Such environments are trees defined as follows:
c

c
•

C
root only

C1

C is a child of c

C2

C1 and C2 are children of c

4

Each node c has a label c of the form ◦, s → r : a, or µχ respectively representing
the root of choice or concurrent branches, an interaction between s and r on a, and a
recursive behaviour. We write c ∈ C if c is a node in C. We use as a wild-card when
some of the components of a label are immaterial, e.g. → : a matches any label
representing an interaction on a. Given a tree C, we write c1 ≺ c2 , if c1 , c2 ∈ C and c2
is a node in the sub-tree rooted at c1 . We adapt the definitions in [9] to our framework.
Definition 1 (Dependency relations [9]) Fix C, we define the following relations:
c1 ≺II c2 if c1 ≺ c2 and ci = si → r : ai i ∈ {1, 2}
c1 ≺IO c2 if c1 ≺ c2 and c1 = s1 → r : a1 and c2 = r → s2 : a2
c1 ≺OO c2 if c1 ≺ c2 and ci = s → ri : a i ∈ {1, 2}
An input dependency from c1 to c2 is a chain of the form c1 ≺φ1 . . . ≺φk c2 (k ≥ 0) such
that φi ∈ {II, IO} for 1 ≤ i ≤ k − 1 and φk = II. An output dependency from c1 to c2 is
a chain c1 ≺φ1 . . . ≺φk c2 (k ≥ 1) such that φi ∈ {OO, IO}.
Definition 2 (Linearity [9]) C is linear if and only if whenever c1 ≺ c2 with c1 = →
: a and c2 = → : a then there is both input and output dependencies from c1 to c2 .
We also define a function ? to append trees as follows
c

c
?C0 =

c
,

C0 ?C0

C0

c
?C0 =

• ?C = C,
C1

C2

C1 ?C0 C2 ?C0

and a partial function to append a tree C0 to a tree C while preserving linearity: CC0 =
C ?C0 if C ?C0 is linear, otherwise CC0 = ⊥. Also, let T (G ) be the total function (cf.
Appendix A.1) which returns a tree C corresponding to the use of channels in G .
3.2

Well-formed Global Types

We define the conditions for a global type to be well-formed. We write P (G ) (resp.
C (G )) for the set of participant (resp. channel) names in G , and fv(G ) for the set of
free variables in G , similarly for a system S. We give a few accessory functions. Let
def

R(G ) = {s → r : a | G ≡ (s → r : ahei.G1 + G2 | G3 ) ; G4 }
(
def FP (G1 ) ∪ FP (G2 ), G = G1 | G2
FP (G ) =
{P (G )},
otherwise

FO ({s, r} ∪ P , G1 ),
G = s → r : ahei.G1





F
(∅,
G
)
∪
F
(∅,
G
),
G = G1 | G2
O
1
O
2





G = G1 + G2 and FO (P , G1 ) = FO (P , G2 )
FO (P , G1 ),
def
FO (P , G ) = FO (P , G1 ),
G = µ χ.G1


FO (∅, G2 ),
G = G1 ; G2





{P },
G = 0 or G = χ



⊥,
otherwise
5

R(G ) is the ready set of G . FP (G ) is the family of sets of its participants running in
different concurrent branches. That is, N ∈ FP (G ) iff all n ∈ N are in a same top-level
thread of G . FO (G , P ) is the family of sets of participants of G , so that for all N, M ∈
FO (P , G ), the participants in N and those in M are in different concurrent branches in
def

the last part of G ; define FO (G ) = FO (∅, G ). Note that FO ( , ) is a partial function.
Example 2. Let Gi, j = b1 → b2 : ci hi.(bi → si : ti haddri | bj → sj : no j hi) describe
each of the branches of the or box in the example of § 1, where i 6= j ∈ {1, 2}, then
R(G1,2 ) = {b1 → b2 : c1 } , FP (G1,2 ) = {b1 , s1 , b2 , s2 } , FO (G1,2 ) = {{b1 , s1 }, {b2 , s2 }}
The global type below corresponds to the whole protocol of § 1

G = (G1 | G2 ) ; b2 → b1 : rhpricei.(G1,2 + G2,1 )
hence R(G ) = {bi → si : ti }i=1,2 , FP (G ) = FP (G1,2 ), and FO (G ) = FO (G1,2 ).



Well-formedness. The well-formedness of a global type G depends on how it uses
channels; a judgement of the form C `G states that G is well-formed according to the
channel environment C (cf. § 3.1); G is well-formed if • ` G can be derived from the
rules given in Fig. 1. We assume that each premise of the rules in Fig. 1 does not hold if
any of the functions used are not defined (e.g., in [ WF - ;], if FO (G ) = ⊥ then C `G ; G 0 is
not derivable). Hereafter, we assume that a node c is fresh (i.e. c 6∈ C). The environment
C permits to tackle one of the main requirements for a global type to be well-formed:
there should not be any race on channels. In the following, we discuss the rules of Fig. 1,
which are grouped according to three other requirements: sequentiality, single threaded,
and knowledge of choice.
Sequentiality [5]. Rules [ WF -.], [ WF - ;] and [ WF - ;-0] ensure that sequentiality is preserved.
In [ WF -.], there must be an ordering dependency between a prefix and its continuation so
that it is possible to implement each participant so that at least one action of the first
prefix always happens before an action of the second prefix. More concretely, we want
to avoid global types of the form, e.g.
s1 → r1 : ahei.s2 → r2 : bhe0 i 8

where, evidently, it is not possible to guarantee that s2 sends after r1 receives on a.
Since we are working in an asynchronous setting, we do not want to force both send
and receive actions of the first prefix to happen before both actions of the second one.
Rule [ WF - ;] requires the following for generalised sequencing. (i) For each pair of “first”
participants in G 0 , there exist two concurrent branches of G such that these two participants appear in different branches. This is to avoid global types of the form, e.g.
(s1 → r1 : ahei | s2 → r2 : bhei) ; s1 → r1 : chei 8
since there is no possible sequencing between the prefix on b and the one on c. (ii) For
all top-level concurrent branches in G , there is a participant in that branch which is also
in one of the branches of G 0 . This requirement discards global types of the form, e.g.
(s1 → r1 : ahei | s2 → r2 : bhei | s3 → r3 : chei) ; s1 → r2 : dhei 8
6

[ WF -.]

∀ s0 → r0 : ∈ R(G ) : {s0 , r0 } ∩ {s, r} 6= ∅

[ WF - ;]

C c `G

c=s→r:a

C `s → r : ahei.G
∀ s → r : ∈ R(G 0 ) . ∃N1 6= N2 ∈ FO (G ) . s ∈ N1 ∧ r ∈ N2
∀N ∈ FP (G ) . ∃N 0 ∈ FP (G 0 ) . N ∩ N 0 6= ∅
C `G
C T (G ) `G 0
C `G ; G 0
0

C (G ) ∩ C (G 0 ) = ∅
C `G
C `G 0
C `G | G 0
χ ∈ fv(G ) ⇒ #FO (G ) = 1
C ? c `G
c=χ
[ WF -µ χ]
C `µ χ.G
C `G
CC(χ)
[ WF - ;-0]
[ WF -χ]
C `G ; 0
C `χ
[ WF -0] C `0
C `G
C `G 0
∀ s → r : a ∈ R(G ).∀ s0 → r0 : b ∈ R(G 0 ) . s = s0 ∧ a 6= b
C `G + G 0

[ WF - | ]

[ WF -+]

P (G ) ∩ P (G ) = ∅

Fig. 1. Rules for Well-formedness

since it is not possible to enforce an order between s3 and r3 and the others. (iii) G and
G 0 are also well-formed. Observe that (i) implies that for G ; G 0 to be well-formed, G is
of the form G1 | G2 , with G1 6= 0 and G2 6= 0. Both [ WF -.] and [ WF - ;] are only applicable
when linearity is preserved. Finally, rule [ WF - ;-0] is a special case of G ; G 0 .
Single threaded [9]. A participant should not appear in different concurrent branches
of a global type, so that each participant is single threaded. This is also reflected in
the calculus of § 2, where parallel composition is only allowed at the system level.
Therefore, in [ WF - | ], the participant (resp. channel) names in concurrent branches must
be disjoints. Rule [ WF -µ χ] adds a new node in C to keep track of recursive usage of the
channels, and requires that G is single threaded, i.e. concurrent branches cannot appear
under recursion. If that was the case, a participant would appear in different concurrent
branches of the unfolding of a recursive global type. Rule [ WF -χ] unfolds C at χ to ensure
that the one-time unfolding of C preserves linearity (see [9] for details).
Knowledge of choice [5, 9]. Whenever a global type specifies a choice of two sets of
interactions, the decision should be made by exactly one participant. For instance,
s1 → r1 : a1 hei.G1

s2 → r2 : a2 he0 i.G2

+

8

specifies a choice made by two participants. Indeed, s1 is the one making a decision
in the first branch, while s2 makes a decision in the second one; this kind of choreographies cannot be implemented (without using hidden interactions). Also, we want
to avoid global types where a participant n behaves differently in two choice branches
without being aware of the choice made by others. For instance, in
s → r : ahei.n → r : chei.G1

+

s → r : bhei.n → r : dhei.G2
7

8

where n ignores the choice of s and behaves differently in each branch. On the other
hand, we want global types of following form to be accepted.
s → r : ahei.n → s : bhei.s → n : chei.n → r : dhei
+
s → r : a0 hei.n → s : bhei.s → n : c0 hei.n → r : d 0 hei

4

Indeed, in this case n behaves differently in each branch, but only after “being informed” by s about the chosen branch.
Together with the projection map defined below, rule [ WF -+] guarantees that “knowledge of choice” is respected. In particular, the rule requires that the participant who
makes the decision is the same in every branch of a choice, while the channels guarding
the choice must be distinct.
Definition 1 (  ). The projection of a global type G wrt. n ∈ P (G ) is defined as

0

a?e.G n ,


0

a!e.G n ,



G 0 n ,





G1 n ]G2 n ,
def
G n = Gi n ,



G1 n [G2 n /0],




µ χ.G 0 n ,





G,



⊥,

if G = s → n : ahei.G 0
if G = n → r : ahei.G 0
if G = s → r : ahei.G 0 and s 6= n 6= r
if G = G1 + G2
if G = G1 | G2 and n 6∈ P (G j ), i 6= j ∈ {1, 2}
if G = G1 ; G2
if G = µ χ.G 0
if G = χ or G = 0
otherwise

We say that a global type is projectable if G n is defined for all n ∈ P (G ).
The projection map is similar to the one given in [9], but for the generalised sequencing
case and the use of ] to project choice branches. Observe that if G = G1 ; G2 , we
replace 0 by the projection of G2 in the projection of G1 . Function ] basically merges
(if possible) the behaviour of a participant in different choice branches; ] is defined
only when the behaviour is the same in all branches, or if it differs after having received
enough information about the branch which was chosen. The definition of ] is given
in Appendix A.2. A global type may be projected even if is not well-formed, but in that
case none of the properties given below are guaranteed to hold.

4

Synthesising Global Types

We now introduce a typing systems to synthesise a global type G from a system S so that
S satisfies safety and progress properties (e.g. no race on channels and no participant
gets stuck). Also, the set of typable systems corresponds exactly to the set of systems
obtained by projecting well-formed global types. To synthesise G from a system S, a
careful analysis of what actions can occur at each possible state of S is necessary.
8

If S ≡ n[P] | S0 then S(n) denotes P (if S 6≡ n[P] | S0 then S(n) = ⊥). We define the
ready set of a system as follows:

{ai |i ∈ I} ∪ R(S0 ) if S ≡ r[∑i∈I ai ?ei .Pi ] | S0





 {ai |i ∈ I} ∪ R(S0 ) if S ≡ s[Li∈I ai !ei .Pi ] | S0
R(S) =

if S ≡ a : e · ρ | S0
{a} ∪ R(S0 )





∅
if S ≡ 0
def

We overload R( ) on behaviours in the obvious way and define R(S) = {a ∈ C | a ∈
R(S) or a ∈ R(S)} and S l ⇐⇒ ∃ a ∈ C : a ∈ R(S) ∧ a ∈ R(S); we write S 6l if S l does
not hold.
4.1

Validation Rules

A judgement of the form A ; Γ ; C ` S I G says that the system S forms a choreography
defined by a global type G , under the environments A, Γ, and C. The environment A is a
superset of the channel names used in S, and corresponds to the channels S is entitled to
use. The environment Γ maps participant names and local recursion variables to global
recursion variables (◦ is the empty context Γ). The channel environment C records the
use of channels. Hereafter, we use · for the disjoint union of environments.
Programs. A global type G can be synthesised from the program S if the judgement

C (S) ; ◦ ; • ` S I G
(stating that S is entitled to use all its channels in empty environments) is derivable from
the rules in Fig. 2 (driven by the ready set of S and the structure of its processes).
Rule [.] validates prefixes provided that the system is entitled to linearly use the
channel a, that the continuation is typable, and that no other interactions are possible in
S. For instance, [.] does not apply to
s1 [a!e.P1 ] | r1 [a?e.Q1 ] | s2 [b!e.P2 ] | r2 [b?e.Q2 ] 8
because there is no ordering relation between the actions on a and b; in this case either
[ | ] or [ ;] should be used.
Rule [ | ] validates concurrent branches when they can be validated using a partition A1
and A2 of the channels (recall that P (S) ∩ P (S0 ) = ∅).
Rule [ ;] splits the system into two sequential parts and it relies on the function split( )
defined in § 4.2; for now it suffices to notice that linearity is checked for in the second
part of the split by adding the channel environment corresponding to G1 to C (recall that
CC0 is undefined if C ?C0 is not linear).
Rule [⊕] introduces the global type choice operator, it requires that both branches are
typable and that no other interactions are possible in S.
Rule [+] allows to discharge a branch of an external choice; together with the premises
of [ | ], rule [+] discards systems such as the one on left below (due to a race on b) but
9

[.]

{a} ∪ A ; Γ ; C c ` s[P] | r[Q] | S I G

[|]

[ ;]

c=s→r:a

S 6l

{a} ∪ A ; Γ ; C ` s[a!e.P] | r[a?e.Q] | S I s → r : ahei.G
A2 ; ◦ ; C ` S 0 I G 0

A1 ; ◦ ; C ` S I G

A1 ∩ A2 = ∅

A1 ∪ A2 ; Γ ; C ` S | S0 I G | G 0

A ; ◦ ; C ` S1 I G1

split(S) = (S1 , S2 )

A ; ◦ ; C T (G1 ) ` S2 I G2

A ; Γ ; C ` S I G1 ; G2
[⊕]

A ; Γ ; C ` s[P] | S I G
R(Q) ⊆ A

A ; Γ ; C ` r[P] | S I G

S 6l

A ; Γ ; C ` r[P + Q] | S I G

∃ 1 ≤ i, j ≤ k . (ni [Pi ] | nj [Pj ]) l
A ; Γ · (n1 , x1 ) : χ, . . . , (nk , xk ) : χ ; C ? µχ ` n1 [P1 ] | . . . | nk [Pk ] I G
A ; Γ ; C ` n1 [µ x1 .P1 ] | . . . | nk [µ xk .Pk ] I µ χ.G
[X]

S≡S
[eq]

S 6l

A ; Γ ; C ` s[P ⊕ Q] | S I G + G 0
[+]

[µ]

A ; Γ ; C ` s[Q] | S I G 0

0

∀1 ≤ i ≤ k . Γ(ni , xi ) = χ CC(µχ)
A ; Γ ; C ` n1 [x1 ] | . . . | nk [xk ] I χ

A ; Γ ; C ` S0 I G

A; Γ; C ` S I G

[0]

∀n ∈ P (S) . S(n) = 0

C (S) = ∅

A; Γ; C ` S I 0

Fig. 2. Validation Rules for Programs

permits those like the one on the right (as only the channels guarding the choice must
be in A).
r1 [a?e + b?e] | s2 [b!e] | r2 [b?e] 8 s1 [a!e] | r1 [a?e + c?e.b?e] | s2 [b!e] | r2 [b?e] 4
Rules [µ] and [ X ] handle recursive systems. The former rule “guesses” the participants
involved in a recursive behaviour. If two of them interact, [µ] validates the recursion
provided that the system can be typed when such participants are associated to the
global recursion variable χ (assuming that χ is not in Γ). Rule [ X ] checks that all the
participants in the recursion have reached a local recursion variable corresponding to
the global recursion, and that the unfolding of C on µχ preserves linearity; for this we
define C(µχ) to be the subtree of C rooted at the deepest node of C labelled by µχ (note
that this node is unique since bound variables are distinct).
Rule [0] only applies when all the participants in S end while [eq] validates a system up
to structural congruence.
Theorem 1 (Decidability). Typability is decidable.
The proofs follows from the fact that the typing is done wrt to the (finite) partitions of
channels in a system, and that the number of required behaviour unfoldings is finite.
Theorem 2 (Unique typing). If A ; Γ ; C ` S I G and A ; Γ ; C ` S I G 0 then G ≡ G 0 .
10

Theorem 3 (Well-formedness). If A ; Γ ; C ` S I G then • `G and G is projectable.
The proofs for these two theorems are by induction on the structure of the derivation.
Runtime system. In order to have subject reduction for our typing systems, queues
have to be handled effectively; we use a distinguished participant name ∗ to denote an
anonymous participant. Assume ∗ 6∈ P and write ∗ → r : ahei.G to specify that there is
a message of sort e on channel a for participant r.
Example 3. Let S = n[a!e] | s[b!e.a?e] | r[b?e] | a : [] | b : []. Consider the judgement
A ; Γ ; C ` S I s → r : bhei.n → s : ahei
If S evolves to S0 = n[0] | s[b!e.a?e] | r[b?e] | a : e | b : [], the identity of the sender n
is lost. However, the judgement
A ; Γ ; C ` S0 I s → r : bhei.∗ → s : ahei
types S0 using ∗.



Runtime systems can be handled by slightly extending Def. 1 so that we have1
c1 ≺OO c2 if c1 ≺ c2 and c1 = ∗ → r : a and c2 = s → r : a
and by adding two rules to the validation rules for handling queues:
[ρ]

{a} ∪ A ; ◦ ; C c ` a : ρ | r[P] | S I G
c=∗→r:a
S 6l
{a} ∪ A ; Γ ; C ` a : e · ρ | r[a?e.P] | S I ∗ → r : ahei.G

[[]]

A; Γ; C ` S I G
A ; Γ ; C ` a : [] | S I G

Rule [ρ] is similar to rule [.], except that a non-empty queue replaces the sender, and Γ
is emptied. Rule [[]] simply allows to remove empty queues from the system.
λ

Theorem 4. If A ; ◦ ; C ` S I G , S −→ S0 , and C (λ) 6∈ C then A ; ◦ ; C ` S0 I G 0
The proof is by case analysis on the different types of transitions a system can make. The
recursive case follows from the fact that reduction preserves closeness of behaviours.
4.2

Splitting Systems

The purpose of systems’ splitting is to group participants according to their interactions.
For this we use judgements of the form
Ψ; Θ ` S m Ω

(4.1)

which reads as “S splits as Ω under Ψ and Θ”. The environment Ψ is a set of (pairwise
disjoint) ensembles that is disjoint sets N ⊆ P (S) containing participants that interact
with each other for a while; and then some of them may interact with participants in
other ensembles in Ψ. The environment Θ is a set of (pairwise disjoint) duos, that is
1

This extension makes sense since the order of messages is preserved in the calculus.

11

two-element sets of participants {s, r ∈ P (S) : r 6= s} representing the first participants
able to interact once the first part of the split is finished. Under suitable conditions,
one could identify when n ∈ N has to interact with a participant of another ensemble.
In other words, one can divide S(n) as n[P1 · ε · P2 ]: the interactions in P1 happen with
participants in the ensemble of n, while P2 starts interacting with a participant in another
ensemble. Finally, the environment Ω assigns behaviours augmented with a separator ε
to participant names, and lists of sorts to queues a.
Θ

Given a judgement as (4.1), we say that N, M ∈ Ψ are Θ-linked (N _ M in symbols)
Ω
/ also, we say that n, m ∈ P (S) are Ω-linked (n _ m in symiff ∃D ∈ Θ : N ∩ D ∩ M 6= 0;
def

/ We define S[N] = ∏n∈N n[S(n)] | ∏a∈C (S) a : S(a).
bols) iff C (Ω(n)) ∩ C (Ω(m)) 6= 0.
Definition 2. The judgement Ψ; Θ ` S m Ω is coherent if it can be derived from the
rules in Fig. 3, Θ 6= ∅, and for all N ∈ Ψ, S[N] l and the following conditions hold

∃!n ∈ N : (∃!m ∈ N \ {n} : S[N \ {n}] 6l ∧ S[N \ {m}] 6l) or (S[N \ {n}] 6l)
(4.2)
~ is total on N and ↔Θ is total on Ψ
def Θ ∗

Θ

(4.3)
def Ω +

where ↔Θ = _ is the reflexive and transitive closure of _ and ~ = _ is the transiΩ
tive closure of _.
Essentially, Def. 2 ensures that rule [ ;] is the only rule of Fig. 2 applicable when the
system can be split. Condition (4.2) ensures that, in each ensemble N, there is a unique
pair of synchronising participants or there is a unique participant that can synchronise
with a queue a. Condition (4.3) is the local counterpart of the well-formedness rule for
global types of the form G ; G 0 . The totality of ~ on N guarantees that the participants
in an ensemble share channels. The totality of ↔Θ on Ψ guarantees that each ensemble
in Ψ has one “representative” which is one of the first participants to interact in the
second part of the split. Together with condition Θ 6= ∅, the condition on ↔Θ ensures
that there are (at least) two ensembles of participants in Ψ. Note that (4.3) also ensures
that all the set of participants in Ψ are interdependent (i.e. one cannot divide them into
independent systems, in which case rule [ | ] should be used).
A judgement (4.1) is to be derived with the rules of Fig.3 (we omit rules for commutativity and associativity of systems). The derivation is driven by the structure of up
to two processes in S, and whether they are in the same ensemble and/or form a duo.
Rule [ε] marks two processes m and n as “to be split” when m and n form a duo in
Θ and are in different ensembles of Ψ. The continuation of the system is to be split as
well, with m and n removed from the system and from the environments.
Rule [sync] records in Ω the interactions of participants in a same ensemble of Ψ.
Rule [+] discharges the branch of an external choice for participants in a same ensemble
while [⊕] deals with internal choice. The premise Ω  Ω0 holds only when Ω and Ω0
have the same domain and differ only up to external choice, i.e. for each n either its
split is the same in both branches, or its split is an external choice (guarded by different
channels); Ω t Ω0 merges Ω and Ω0 accordingly (cf. Appendix A.3). The additional
premise s[P ⊕ P0 ] | r[Q] l is required so that the split is done before a branching if a
participant cannot interact with one of its peer in N after the branching.
12

n ∈ N, m ∈ M
[ε]

(n[P] | m[Q]) l

s, r ∈ N
[sync]

Ψ · N; Θ ` s[P] | r[Q] | S m Ω · s : π · r : ϕ

Ψ · N; Θ ` s[a!e.P] | r[a?e.Q] | S m Ω · s : a!e.π · r : a?e.ϕ

m, n ∈ N

(m[P] | n[Q]) l

[+]

[⊕]

Ψ · N\{n} · M\{m}; Θ ` S m Ω

Ψ · N · M; Θ · {n, m} ` n[P] | m[Q] | S m Ω · n : ε · m : ε

Ψ · N; Θ ` m[P] | n[Q] | S m Ω · m : π

Ψ · N; Θ ` m[P + P0 ] | n[Q] | S m Ω · m : π

n, m ∈ N
(n[P ⊕ P0 ] | m[Q]) l
Ω  Ω0
Ψ · N; Θ ` n[P] | m[Q] | S m Ω · n : π
Ψ · N; Θ ` n[P0 ] | m[Q] | S m Ω0 · n : ϕ
Ψ · N; Θ ` n[P ⊕ P0 ] | m[Q] | S m Ω t Ω0 · n : π ⊕ ϕ
[ax]

{∅}; ∅ ` 0 m ∅
(n[P] | S) 6l
[rem]

r∈N
[q]

[0]

P 6≡ 0

Ψ \ n; Θ ` S m Ω
Ψ; Θ ` n[0] | S m Ω · n : 0
Ψ \ n; Θ ` S m Ω

Ψ; Θ ` n[P] | S m Ω · n : ε
Ψ · N; Θ ` r[P] | S m Ω · r : π · a : ρ

Ψ · N; Θ ` r[a?e.P] | a : e · ρ | S m Ω · r : a?e.π · a : e · ρ

Fig. 3. Splitting Systems.

Rule [ax] terminates a derivation (all environments emptied) while [0] completes the split
of a process (abusing notation, Ψ \ n denotes the removal of n from any N ∈ Ψ).
Rule [rem] marks a process to be split when it cannot interact with anyone in S. The
premise P 6≡ 0 allows to differentiates a process which terminates after the split, from
others which terminate before. In the latter case, rule [0] is to be used.
Rule [q] records in Ω interactions with non-empty queues.
We now define a (partial) function split which splits a system into two parts.
Definition 3 (split( )). Let Ψ; Θ ` S m Ω be a coherent judgement. Define split(S) =
(S1 , S2 ) where
– ∀n ∈ P (S). S1 (n) = S(n) − Ω(n) and S2 (n) = S(n) % Ω(n)
– ∀a ∈ C (S). S1 (a) = Ω(a) and S2 (a) = S(a) \ Ω(a)
if S(n) % Ω(n) 6= ⊥ for all n ∈ P (S), and split(S) = ⊥ otherwise.
The auxiliay funtions − and % used in Def. 3 are defined in Appendix A.3; we
give here their intuitive description. Let n ∈ P (S), and Ψ; Θ ` S m Ω be a coherent
judgement. Function S(n) − Ω(n) returns the “first part” of the split of n, that is the
longest common prefix of S(n) and Ω(n), while S(n) % Ω(n) is partial and returns the
the remaining part of the behaviour of S(n) after Ω(n).
Example 4. Taking SBS as in § 1, we have split(SBS ) = (S1 , S2 ) such that
S1 (b1 ) = t1 !order.p1 ?price
S1 (si ) = ti ?order.pi !price

S2 (b1 ) = r?price.(c1 !.t1 !addr ⊕ c2 !.no1 !)
S2 (si ) = ti ?addr + noi ?

Note that {{b1 , s1 }, {b2 , s2 }} ; {{b1 , b2 }} ` SBS m Ω is coherent.
13



4.3

Properties of Synthesised Global Type

Progress and safety. If a system is typable, then it will either terminate or be able to
make further transitions (e.g. if there are recursive processes).
X

Theorem 5. If A ; ◦ ; C ` S I G then S −→ S0 , or ∀ n ∈ P (S) . S(n) = 0, or S −→.
Let us add the rule [ ERROR ] below to the semantics given in § 2.
a?e0

[ ERROR ]

e·a

T −→ T 0
S −→ S0
S | T −→ error

e 6= e0

Theorem 6. If A ; ◦ ; C ` S I G , then S is race free and S =⇒−→ error is not possible.
The proofs of Theorems 5 and 6 are by contradiction, using Theorem 4.
Behavioural equivalences. We show that there is a correspondence between the original
system and the projections of its global type. First, let us introduce two relations.
α

α

Definition 3 ( . and ≈) P . Q if and only if Q −→ Q0 then there is P0 such that P −→
α
α
α
P0 . Also, S ≈ T iff whenever S −→ S0 then T −→ T 0 and S0 ≈ T 0 ; and whenever T −→ T 0
α
then S −→ S0 and S0 ≈ T 0 where α ∈ {n : a!e, n : a?e, X}.
The behaviour of a participant in S is a simulation of the projection of a synthesised
global type from S onto this participant. Intuitively, the other direction is lost due to
rule [+], indeed external choice branches which are never chosen are not “recorded” in
the synthesised global type.
Lemma 1. If A ; ◦ ; C ` S I G then ∀n ∈ S . G n . S(n).
The proof is by case analysis on the transitions of S, using Theorem 4.
Since the branches that are not recorded in a synthesised global type are only those
which are never chosen, we have the following result.
Theorem 7. If A ; ◦ ; C ` S I G then ∏n∈P (S) n[G n ] ≈ S.
The proof is by case analysis on the transitions of S, using Theorem 4 and Lemma 1.
Our completeness result shows that every well-formed and projectable global type
is inhabited by the system consisting of the parallel composition of all its projections.
Theorem 8. If • ` G and G is projectable, then there is G 0 ≡ G such that A ; Γ ; C `
∏n∈P (G ) n[G n ] I G 0 .
The proof is by induction on the structure of (well-formed) G .

5

Concluding Remarks and Related Work

We presented a typing system that, under some conditions, permits to synthesise a
choreography (represented as global type) from a set of end-point types (represented
as local types). The synthesised global type is unique and well-formed; moreover, its
projections are equivalent to the original local session types. We have shown safety and
progress properties for the local session types. Finally, the derivatives of local types
which form a choreography can also be assigned a global type (subject reduction).
14

Related work. A bottom-up approach to build choreographies is studied in [11]; this
work relies on global and local types, but uses local and global graphs. A local graph
is similar to a local type while a global graph is a disjoint union of family of local
graphs. We contend that global types are more suitable than global graphs to represent
choregraphies; in fact, differently from the approach in [11], our work allows us to reuse
most of the theories and techniques based on multiparty global types.
Our work lies on the boundary between theories based on global types (e.g. [1, 5, 7,
9]) and the ones based on the conversation types [3]. Our work relies on the formalism
of global types, but uses it the other way around. We start from local types and construct
a global type. We have discussed the key elements of the global types in § 3.
Conversation types [3] abandon global views of distributed interactions in favour of
a more flexible type structure allowing participants to dynamically join and leave sessions. The approach in [6] fills the gap between the theories based on session types and
those based on behavioural contracts [4] (where the behaviour of a program is approximated by some term in a process algebra). We are also inspired from [12], where session
types are viewed as CCS-like “projections” of process behaviours. The approach of considering local types as processes is similar to ours. However, the theory of [12] is based
on a testing approach. The connectedness conditions for a choreography given in [2] is
similar to our notion of well-formed global type.
Future work. We aim to extend the framework so that global types can be constructed
from session types which features name passing and restriction. We also plan to refine
the theory and use it in a methodology so that if a choreography cannot be synthesised,
the designers are given indications on why this has failed. Finally, we are considering
implementing an algorithm from the rules of Fig. 2 and Fig. 3, and integrate it in an
existing tool [10] implementing the framework from [1].

References
1. L. Bocchi, K. Honda, E. Tuosto, and N. Yoshida. A theory of design-by-contract for distributed multiparty interactions. In CONCUR, 2010.
2. M. Bravetti, I. Lanese, and G. Zavattaro. Contract-driven implementation of choreographies.
In TGC, 2008.
3. L. Caires and H. T. Vieira. Conversation types. In ESOP, 2009.
4. S. Carpineti, G. Castagna, C. Laneve, and L. Padovani. A formal account of contracts for
web services. In WS-FM, 2006.
5. G. Castagna, M. Dezani-Ciancaglini, and L. Padovani. On global types and multi-party
sessions. In FMOODS/FORTE, 2011.
6. G. Castagna and L. Padovani. Contracts for mobile processes. In CONCUR, 2009.
7. P.-M. Deniélou and N. Yoshida. Dynamic multirole session types. In POPL, 2011.
8. K. Honda, V. T. Vasconcelos, and M. Kubo. Language primitives and type discipline for
structured communication-based programming. In ESOP, 1998.
9. K. Honda, N. Yoshida, and M. Carbone. Multiparty asynchronous session types. In POPL,
2008.
10. J. Lange and E. Tuosto. A modular toolkit for distributed interactions. In PLACES, 2010.
11. D. Mostrous, N. Yoshida, and K. Honda. Global principal typing in partially commutative
asynchronous sessions. In ESOP, 2009.
12. L. Padovani. On projecting processes into session types. MSCS, 22:237–289, 2012.

15

A

Additional Definitions

In this section, we give the definitions of the accessory functions used in the main
sections of the paper.

A.1

Linearity

Definition 4 (T ( )).
s→r:a

µχ

T (s → r : ahei.G ) =

T (µ χ.G ) =
T (G )

T (G )

◦

◦

T (G + G 0 ) =

T (G | G 0 ) =
T (G ) T (G 0 )

T (G ) T (G 0 )

T (G ; G 0 ) = T (G ) ? T (G 0 )

T (0) = T (χ) = •

The function T ( ) returns a channel environment corresponding to a global type.

A.2

Projections

Definition 5 ( ] ).
if P = ∑i∈I ai ?ei .Pi0 and Q = ∑ j∈J a j ?ei .Q0j
and ∀i ∈ I. ∀ j ∈ J. ai 6= a j and I, J 6= ∅
L
L
if P = i∈I ai !ei .Pi0 and Q = j∈J a j !ei .Q0j
P]Q =
and ∀i ∈ I. ∀ j ∈ J. ai 6= a j and I, J 6= ∅


0
0

ahei.(P ] Q ), if P = ahei.P0 and Q = ahei.Q0  ∈ {!, ?}





P,
if P ≡ Q



⊥,
otherwise

P + Q,










P ⊕ Q,

The function merges the behaviour of a participant in different choice branches. In the
first two cases, it merges two guarded internal (resp. external) choices, if their sets of
guard channels are disjoint. In the third case, the function merges the continuation of
both processes, if both are guarded by the same prefix. Note that it is a partial function,
e.g. it might be the case that a participant behaves differently in two branches without
being aware of which branch was chosen, in which case the projection of that participant
is undefined.
16

Definition 6 (Substitution). The substitution P[Q/R], where R is 0.

a!e.(P0 [Q/R])
if P = a!e.P0





a?e.(P0 [Q/R])
if P = a?e.P0





P1 [Q/R] ⊕ P2 [Q/R] if P = P1 ⊕ P2
P[Q/R] = P1 [Q/R] + P2 [Q/R] if P = P1 + P2



µ x.(P0 [Q/R])
if P = µ x.P0





Q
if P = R = 0



P
otherwise
Substitution is used in the projection map.
A.3

Splitting Systems

Omitted rules in Fig. 3:
[com]

Ψ; Θ ` S0 | S m Ω
Ψ; Θ ` S | S0 m Ω

[com]

Ψ; Θ ` (S | T ) | T 0 m Ω
Ψ; Θ ` S | (T | T 0 ) m Ω

Definition 7 (  ). Ω  Ω0 holds if and only if ∀n ∈ P (Ω) ∪ P (Ω0 ) either
Ω(n) ≡ Ω0 (n) or

(Ω(n) ≡ ∑ ai ?ei .Pj and Ω0 (n) ≡ ∑ a j ?ej .Pj )
i∈I

j∈ j

where ∀i ∈ I. ∀ j ∈ J. ai 6= a j .
The boolean function  holds only if two maps Ω differ wrt external choice.
Definition 8 ( t ).
Ω = Ω0 t Ω1 is defined only if Ω0  Ω1 holds, in which case
∀n ∈ P (Ω0 ) ∪ P (Ω1 ) . Ω(n) = merge(Ω0 (n), Ω1 (n))
where
(
P
if P ≡ Q
merge(P, Q)
P + Q if P ≡ ∑i∈I ai ?ei .Pj and Q ≡ ∑ j∈ j a j ?ej .Pj
The function t merges two Ω maps, if  holds.
Definition 9 ( − ).
L

(k,k0 )∈K ak !ek .(Pk − Qk0 )





P−Q = ∑(k,k0 )∈K ak ?ek .(Pk − Qk0 ) + ∑n∈N an ?en .Pn






0,
where K = {(i, j) ∈ I × J | ai = a j }

and

if P ≡

L

i∈I ai !ei .Pi

L

j∈J a j !ej .Q j

if P ≡ ∑i∈I ai ?ei .Pi and Q ≡ ∑ j∈J a j ?ej .Q j
if P ≡ 0 and Q ≡ 0, or Q = ε,

N = {n ∈ I | ∀ j ∈ J. an 6= a j }.
17

and Q ≡

The function − computes the first part of a split behaviour, given the original
behaviour, e.g. S(n) and its prefix in Ω(n). The case for external choices keeps the
branches from the original behaviour which do not appear in Ω(n). The rationale is that
even if some branches are never “chosen” in the system, they might still induce e.g.
races and therefore they need to be taken into account in the main system.
Definition 10 ( % ).


P0





P0
P % Q = 0,



P,



⊥,

if P ≡ i∈I ai !ei .Pi and Q ≡ j∈J a j !ej .Q j
if P ≡ ∑i∈I ai ?ei .Pi and Q ≡ ∑ j∈J a j ?ej .Q j
if P ≡ 0 and Q ≡ 0,
if Q = ε,
otherwise
L

with P0 defined as follows
(
Pi % Q j with (i, j) ∈ K
P0 =
⊥

L

if ∀(i, j)(k, l) ∈ K . Pi % Q j ≡ Pk % Ql
otherwise

where K = {(i, j) ∈ I × J | ai = a j }
The function % computes the second part of a split behaviour. Essentially, it returns the “rest” of a behaviour after Ω(n). Note that if Ω(n) is a branching behaviour,
then the rest must be the same in all branches (since only one behaviour can be returned), e.g. S(n) % Ω(n) = ⊥, if
S(n) = a!e.b!e ⊕ c!e.d!e and
A.4

Ω(n) = a!e.ε ⊕ c!e.ε

Results

Definition 11. There is a race in S if and only if there is S =⇒ S0 such that ∃ a ∈ R(S0 )
such that
∃ {n, m} ∈ P (S) :

a ∈ R(S(n)) and a ∈ R(S(m)) or

18

a ∈ R(S(n)) and a ∈ R(S(m))

B

Definitions Used in the Proofs

Definition 12 (Connected - R).
– Two participants are connected in a system S if (n, m) ∈ RS
(n, m) ∈ RS ⇐⇒ C (S(n)) ∩ C (S(m)) 6= ∅ or ∃n0 . (n, n0 ) ∈ RS ∧ (n0 , m) ∈ RS
– Two participants are connected in a global type G if (n, m) ∈ RG
(n, m) ∈ RG ⇐⇒ C (G n ) ∩ C (G m ) 6= ∅ or ∃n0 . (n, n0 ) ∈ RG ∧ (n0 , m) ∈ RG
Definition 13 (Projections with queues).

e · G 0 a ,
if G = ∗ → a : rhei.G 0





G 0 a ,
if G = s → r : ahei.G 0





G1 a ]G2 a , if G = G1 + G2
G a = Gi a ,
if G = G1 | G2 and a 6∈ C (G j ), i 6= j ∈ {1, 2}



G

·
G

,
if
G = G1 ; G2

1 a
2 a



[],
if ∗ → r : ahei 6∈ G



⊥,
otherwise
Definition 14 ( ] ).
(
ρ1 , if ρ1 = ρ2
ρ1 ] ρ2 =
⊥, otherwise

C

Proofs for Theorem 1 (Decidability)

Typability is decidable.
Proof. The typing systems is decidable from the fact that the ready set of a system, the
number of participants, and their behaviours are finite. Here, we show that the number
of behaviour unfoldings needed to type a system is also finite.
Let (non-recursive) behaviour context C [ ] defined as follows
C [ ] ::=

M

ai !ei .Ci [ ] |

i∈I

∑ ai ?ei .Ci [ ]

| [ ] | µ x.P | x

i∈I

and (possibly recursive) behaviour context C0 [ ] defined as follows
C0 [ ] ::=

M
i∈I

ai !ei .Ci0 [ ] |

∑ ai ?ei .Ci0 [ ]

| [ ] | µ x.C0 [ ] | x

i∈I

Let unfoldi (P) be the ith unfolding of P, defined as follows
unfoldi (P) = 
unfold1 (unfoldi−1 (P))
L

 i∈I ai !ei .unfold1 (Pi )
unfold1 (P) = ∑i∈I ai ?ei .unfold1 (Pi )


P[µ x.P/x]
19

i>1
L
if P ≡ i∈I ai !ei .Pi
if P ≡ ∑i∈I ai ?ei .Pi
if P ≡ µ x.P

The need for unfolding occurs whenever a recursive participants interact with another participant, while not all the participants feature directly a recursive behaviour.
In this case, we need to unfold some participants (rule [eq]), then use rules [⊕], [+], [.],
and/or [0] until rule [µ] is applicable. Note that rules [ ;], [ | ] and [ρ] cannot be used under
recursion.
Consider the following system
S = S0 | S1
where
 

 

S0 = n1 C1 µ x.C10 [x] | . . . | nj C j µ x.C0j [x]
S1 =

]nj+1 [µ x.C0j+1 [x]]

| ... |

nk [µ x.C0j+k [x]]

(C.1)
(C.2)

S l, S0 6l, and there is exactly one n ∈ P (S) such that
S ≡ n[S(n)] | T

and

T 6l

Let Ci for j ≤ i ≤ j + k be the empty context, we can rewrite S such that
 

S ≡ ∏ ni Ci µ x.Ci0 [x]
I = {i | 1 ≤ i ≤ j + k}
i∈I

Given S as above, we define |i|x to be the smallest k such that Ci [x] is a sub-tree
of unfoldk (Ci0 [x]), |i|x = ⊥ if there is no such k. Note that |i|x must be smaller than
the length of Ci [0] (since recursion is guarded). If one |i|x is not defined, then S is not
typable.
We also defined M = max{|i|x | i ∈ I}, and K(i) = M − |i|x . We can unfold each
behaviour so that all of them are unfolded to the same extent, let



S∗ ≡ ∏ ni unfoldK(i) (Ci µ x.Ci0 [x] )
i∈I

We show that
A ; Γ ; C ` S∗ I G ⇒ A ; Γ ; C ` S I G
By definition of unfold( ), and since C [ ] does not contain recursive definition, we
have
 

S∗ ≡ ∏ ni Ci unfoldK(i) (µ x.Ci0 [x])
(C.3)
i∈I

   

 
≡ ∏ ni Ci Ci0 Ci0 . . .Ci0 µ x.Ci0 [x] . . .

(C.4)

i∈I

Where in (C.4), Ci0 [ ] has been unfolded K(i) times. It is easy to see that S∗ is typable
if

∏ ni

  0 0
 
Ci Ci Ci . . .Ci0 [0] . . .

i∈I

and

∏ ni

 0 
Ci [0]

i∈I

are typable themselves, note that rule [eq] does not need to be used to unfold the lefthand side system, since it is recursion free; and there is exactly one recursion less in the
right hand side.
In fact, if we would unfold (C.3) once more, we would not get more chances to type
S∗ since it would amount to add the sub-derivation of the right-hand side to one of the
left-hand side.
20

D

Proofs for Lemma 2 (Uniqueness)

If A ; Γ ; C ` S I G and A ; Γ ; C ` S I G 0 then G ≡ G 0 .
Proof. The proof is by case analysis. We show that every time one rule from Fig.2 is
applicable, either no other rule is applicable, or the derivation produces an equivalent
global type.
Due to their syntactic restriction and the condition S6l, the cases for rules [.], [⊕], and
[µ] are straightforward. In addition, the cases for rule [+] is easy since it does not affect
G . The cases for rules [ X ] and [0] are trivial.
The case for rule [eq] follows from the fact that associativity and commutativity in
S do not affect G . In addition, if one unfold behaviour once more, we have the result
since µ χ.G ≡ G [µ χ.G /χ].
The interesting part of the proof is to show that [ | ] and [ ;] are mutually exclusive.
In fact, if [ | ] is applicable, [ ;] cannot be used because ~ and ↔Θ must be total on
Ψ and Θ 6= ∅. If a system S could be separated in two sub-system by [ | ], these two
conditions could not hold. If [ ;] is applicable, it means that it is not possible to split the
participant in two totally independent sub-systems, and therefore [ | ] is not applicable.
Finally, observe that by Lemma 16 the split is unique.

E

Proofs for Theorem 3 (Well-formedness)

If A ; Γ ; C ` S I G then • `G and G is projectable.
Proof. The proof is by induction on the derivation A ; Γ ; C ` S I G . We make a case
analysis on the last rule used.
Case [.]. We have

G = s → r : ahei.G 0

S = s[a!e.P] | r[a?e.Q] | S0

and

– WF. We show that we have
∀ n1 → n2 : ∈ R(G 0 ) . {s, r} ∩ {n1 , n2 } 6= ∅
by contradiction. By IH, we know that
{a} ∪ A ; Γ ; C s → r : a ` s[P] | r[Q] | S0 I G 0
If we had G 0 ≡ n1 → n2 : bhe0 i.G0 + G1 , with ni 6= s and ni 6= r with i ∈ {1, 2},
then we would have
S0 ≡ n1 [b!e0 .P00 ⊕ P10 ]n2 [b?e0 .Q00 + Q01 ] | S00
which is in contradiction with the premise S0 6l.
By Lemma 25, the result above and since C s → r : a is defined, we have • `G .
– Projection. By Def. 1, we have that G s = a!e.G 0 s , G r = a?e.G 0 r , and G n =
G 0 n , for s 6= n 6= r.
21

Case [⊕]. We have

G = G0 + G1 and S = s[P ⊕ Q] | S0
– WF. Observe that we have that all the guard channels are disjoint by definition of
processes. We have to show that
∀(n1 , n2 ) ∈ R(G0 ).∀(n01 , n02 ) ∈ R(G1 ) . n1 = n01
i.e. that for all prefixes in G0 and G1 , s is the sender. In other words, the participant
who makes the internal choice must be the same in all the branches. If that was not
the case, we would have
S0 ≡ n1 [b!e.Q0 ⊕ Q1 ] | n2 [b?e.Q2 + Q3 ] | S00
which is in contradiction with the premise S0 6l.
By Lemma 25, the result above and C `G0 and C `G1 by IH, we have • `G .
– Projection. We have to prove that
∀n ∈ P (G0 + G1 ). G0 n ]G1 n 6= ⊥
By IH, we have that both G0 n and G1 n exist. There are two cases where the
projection does not exist (i 6= j ∈ {0, 1} in the following):
• Gin = a!e.P and G jn = b?e0 .Q. This cannot happen by definition of behaviours,
i.e. such projections could only come from behaviours of the form (a!e.P) ⊕(b?e0 .Q),
which is not syntactically correct.
• Gi n = ∑k∈K ak ?ek .Pk and G j n = ∑k0 ∈K 0 ak0 ?ek0 .Pk0 , with ak = ak0 for some k
and k0 . This cannot happen by definition of behaviours, i.e. such projections
could only come from behaviours of the form a?e.P0 + a?e.P1 which is not a
syntactically correct behaviour. The same reasoning applies for internal choice.
Note that we have G s = G0 s ⊕ G1 s .
Case [+]
– WF. By induction hypothesis, we have C `G and by Lemma 25, we have • `G .
– Projection. By induction hypothesis.
Case [ | ] We have

G = G0 | G1 and S = S0 | S1
– WF. We have to show that

P (G0 ) ∩ P (G1 ) = ∅ and C (G0 ) ∩ C (G1 ) = ∅
By definition of systems, we know that there cannot be two participants of the same
name in a same system, since S | S0 is a system we have that

P (S0 ) ∩ P (S1 ) = ∅
and by Lemma 27, we have P (G0 ) ∩ P (G1 ) = ∅. By Lemma 29, the premise A0 ∩
A1 , we have C (G0 ) ∩ C (G1 ) = ∅. We have C `G0 and C `G1 by assumption, with
the result above and Lemma 25, we have • `G .
22

– Projection. For all n ∈ P (G ), G n is defined by IH and since P (G0 ) ∩ P (G1 ) = ∅.
Case [ ;]. We have

G = G0 ; G1 and C T (G0 ) and split(S) = (S0 , S1 )
– WF. We have to show that
∀ n1 → n2 : ∈ R(G1 ) . ∃N1 6= N2 ∈ FO (G0 ) . n1 ∈ N1 ∧ n2 ∈ N2

(E.1)

∀N ∈ FP (G0 ) . ∃N 0 ∈ FP (G1 ) . N ∩ N 0 6= ∅

(E.2)

and
We know that split(S) = (S0 , S1 ) therefore there is Ψ; Θ ` S m Ω coherent. We
show (E.1) first. We first show that
s → r : a ∈ R(G1 ) ⇐⇒ {s, r} ∈ Θ
We start with
ni → nj : ∈ R(G1 ) ⇐⇒ S1 (ni ) | S1 (nj ) l
(⇒) If ni → nj : ∈ R(G1 ) then we must have G1 = ((ni → nj : ahei.G2 + G3 ) | G4 ) ; G5
(by definition of R). And by Lemma 26, this implies that S1 (ni ) = a!e.P ⊕ P0 and
S1 (nj ) = a?e.Q + Q0 . Thus we have S1 (ni ) | S1 (nj ) l.
(⇐) If S1 (ni ) | S1 (nj )l, we must have S1 (ni ) = a!e.P ⊕ P0 and S1 (nj ) = a?e.Q + Q0
and since G1 is well-formed by IH, we have the required result by Lemma 26 and
the definition of R.
Now, let us show that
S1 (ni ) | S1 (nj ) l ⇐⇒ {ni , nj } ∈ Θ

(E.3)

(⇒) Since the processes interact, we know that they are 6= 0. Moreover, since they
appear in the second part of the split, the following rule must be applied so that
S1 (ni ) = S(ni ) % Ω(ni ) and S1 (nj ) = S(nj ) % Ω(nj ) ( 6= ⊥ by assumption) with
Ω(ni ) and Ω(nj ) ending with ε.

[ε]

ni ∈ N, nj ∈ M
ni [S1 (ni )] | nj [S1 (nj )] l
Ψ · N\{n} · M\{m}; Θ ` S m Ω
Ψ · N · M; Θ · {ni , nj } ` ni [S1 (ni )] | nj [S1 (nj )] | S m Ω · ni : ε · nj : ε

which gives us the expected result. Note that the rule [rem] cannot be applied because
the processes interact with each other we do not have n[P] | S 6l.
(⇐) If {ni , nj } ∈ Θ then, the rule [ε] must also be applied (the axiom cannot be
reach with Θ 6= ∅), since the rule requires that ni [S1 (ni )] | nj [S1 (nj )] l, we have
the expected result.
Let us now show that
∀{ni , n j } ∈ Θ . ∃Ni 6= N j ∈ FO (G0 ) . ni ∈ N j ∧ n j ∈ N j
23

(E.4)

First we show that
N ∈ FO (G0 ) ⇒ ∃!N 0 ∈ Ψ : N ∩ N 0 6= ∅

(E.5)

By Lemma 20, we have that ∀N ∈ FO (G0 ) . RG0 is total on N. By Lemma 21, we
have that (n, m) ∈ RG0 ⇒ (n, m) ∈ ~. By Lemma 12, we have that (n, m) ∈ ~ ⇒
{n, m} ∈ N ∈ Ψ. Therefore we have
N ∈ FO (G0 ) ⇒ ∃N 0 ∈ Ψ : N ∩ N 0 6= ∅
and N 0 is unique since Ψ is a set of pairwise disjoint sets.
We finalise the proof of (E.1), by showing (E.4) by contradiction. If we had
∃{n1 , n2 } ∈ Θ .∃N ∈ FO (G0 ) . {n1 , n2 } ∈ N
by Lemma 11, we have that ∃N1 6= N2 ∈ Ψ : n1 ∈ N1 ∈ Ψ and n2 ∈ N2 ∈ Ψ which
is contradiction with (E.5).
Let us now show (E.2), i.e.
∀N ∈ FP (G0 ) . ∃N 0 ∈ FP (G1 ) : N ∩ N 0 6= ∅
We first show that
FP (G ) = Ψ
By definition of FP , we have that

G=

∏

GN with GN 6≡ GN0 | GN00 .

N∈FP (G )

Therefore, by Lemma 20, RGN is total on P (GN ) for each N. By Lemma 21, we
have that ~ is total on each P (GN ) as well, and by Lemma 12, we have
N ∈ Ψ ⇐⇒ P (GN ) = N
Now, we show that
∀N ∈ Ψ. ∃N 0 ∈ FP (G1 ). N ∩ N 0 6= ∅
by contradiction, if we had
∃N ∈ Ψ.N ∩ P (G1 ) = ∅
by Lemma 11, we must have N 6= M ∈ Ψ such that {n, m} ∈ Θ and n ∈ N and m ∈ M.
Since n ∈ N is also in Θ, we must have S1 (n) | S1 (m)l which implies that S1 (n) ≡ 0
and therefore n ∈ P (G1 ), by Lemma 27. Thus N ∩ P (G1 ) 6= ∅
From (E.1), (E.2), the fact that by assumption C T (G0 ) is defined, and Lemma 25
we have • `G .
– Projection. By IH, we have that for all n G0 n and G1 n exist, thus we have that
G0 n [G1 n /0] is defined for all n. Note that since • `G0 , we have #(FO (G0 )) > 1
(cf. E.1). Therefore, by Lemma 23, fv(G1 ) = ∅. In addition, by Lemma 22, we
have bv(S) = ∅ (since the split(S) by assumption), and by Lemma 24, bv(G0 ) =
∅. Thus, every branch in G0 ends with 0, and all the projections of G0 end with 0.
24

Case [µ] We have

G = µ χ.G0 and S = n1 [µ x1 .P1 ] | . . . | nk [µ xk .Pk ] and
– WF. We have to show that
χ ∈ fv(G 0 ) ⇒ #FO (G 0 ) = 1
we can apply Lemma 23 and we have the result directly. Observe that the recursion
is prefix guarded since ∃ i, j : ni [Pi ] | mj [Pj ] l holds.
– Projection. By induction hypothesis.
Case [ X ] We have

G = χ and ∀n ∈ P (S).S(n) = xn
We have to show that CC(χ), which follows directly from the premises of rule [ X ].
Case [0] Trivial.
Case [ρ] We have

G = ∗ → r : ahei.G 0

S = r[a?e.Q] | a : e · ρ | S0

and

– WF. We show that we have
∀ n1 → n2 : ∈ R(G 0 ) . ni = r

with i ∈ {1, 2}

by contradiction. By IH, we know that
{a} ∪ A ; Γ ; C s → r : a ` r[Q] | a : ρ | S0 I G 0
If we had G 0 ≡ n1 → n2 : bhe0 i.G0 + G1 , with ni 6= r with i ∈ {1, 2}, then we would
have
S0 ≡ n1 [b!e0 .P00 ⊕ P10 ]n2 [b?e0 .Q00 + Q01 ] | S00
which is in contradiction with the premise S0 6l.
By Lemma 25, the result above, and since C ∗ → r : a is defined, we have • `G .
– Projection. By Def. 1, we have that G r = a?e.G 0 r , and G n = G 0 n , for n 6= r.

F

Proofs for Theorem 4 (Subject Reduction)
λ

If A ; ◦ ; C ` S I G , S −→ S0 , and C (λ) 6∈ C then A ; ◦ ; C ` S0 I G 0
Proof. There are three cases to consider.
n[a!e]

a·e

Case 1. S ≡ S1 | S2 with S1 −→ S10 and S2 −→ S20
In this case, S must have the following form
S ≡ n[a!e.P ⊕ P0 ] | a : ρ | T

and S0 ≡ n[P] | a : ρ · e | T

and by Lemma 2 we have that A ; ◦ ; C ` S0 I G 0 .
25

n[a?e]

e·a

Case 2. S ≡ S1 | S2 with S1 −→ S10 and S2 −→ S20
In this case, S must have the following form
S = n[a?e.P + P0 ] | a : e · ρ | T

and

S0 = n[P] | a : ρ | T

and by Lemma 2 we have that A ; ◦ ; C ` S0 I G 0
X

Case 3. S −→ S in this case, we have A ; ◦ ; C ` S0 I G 0 trivially since S0 ≡ S.
Case 4 (unfolding). If S ≡ n[µ x.P] | S0 and S0 ≡ n[P[µ x.P/x]] | S0 then G = µ χ.G0 ,
and ∀m ∈ P (S0 ) . S0 (m) ≡ µ x.Q. We have the result by unfolding all the participants in
S0 wiht rule [eq], so to have G 0 = G0 [µ χ.G0 /χ].
In the other direction, we have the result by folding all the participants in P (S0 ).
Case 5 (commutativity and associativity). If S ≡ S0 , then we have the result with rule
[eq].
Lemma 2. The following holds:
1. A ; ◦ ; C ` s[a!e.P ⊕ P0 ] | a : ρ | T I G ⇒ A ; ◦ ; C ` s[P] | a : ρ · e | T I G 0
2. A ; ◦ ; C ` r[a?e.P + P0 ] | a : e · ρ | T I G ⇒ A ; ◦ ; C ` r[P] | a : ρ | T I G 0
with → : a 6∈ C in 1 and 2.
Corollary 1.

G n = (a!e.G0 n ) ⊕ G1 n ⇒ G 0 n = G0 n
and

G n = a?e.G0 n ⇒ G 0 n = G0 n
Proof. We show that 1 and 2 hold by contradiction.
Case 1. Assume
A ; ◦ ; C ` s[a!e.P ⊕ P0 ] | a : ρ | S I G is derivable.
A ; ◦ ; C ` s[P] | a : ρ · e | S I G 0 is not.
Take S ≡ r[a?e.Q] | S0 , ρ = [], and S0 6l. We must have the following sub-derivation for

G

[.]

..
.
A ; ◦ ; C s → r : a ` s[P] | a : ρ | r[a?e.Q] | S0 I G0
A ; ◦ ; C ` s[a!e.P] | a : ρ | r[a?e.Q] | S0 I s → r : ahei.G0

Consider the non-derivable judgement for

[ρ]

(F.1)

G0

⊥
A ; ◦ ; C ∗ → r : a ` s[P] | a : ρ | r[a?e.Q] | S0 I G00
A ; ◦ ; C ` s[P] | a : e | r[a?e.Q] | S0 I ∗ → r : ahei.G00
26

(F.2)

Where the rule [ρ] must be applicable here, since the only difference with the above
system is C ∗ → r : a which is defined since → : a 6∈ C.
We have a contradiction here since
s[P] | a : ρ | r[a?e.Q] | S0 is derivable in (F.1).
while
s[P] | a : ρ | r[a?e.Q] | S0 is not derivable in (F.2).
Case 2. Assume
A ; ◦ ; C ` r[a?e.P + P0 ] | a : e · ρ | S I G is derivable.
A ; ◦ ; C ` r[P] | a : ρ | S I G 0 is not.
Take S such that S 6l. We must have the following sub-derivation for G

[ρ]

..
.
A ; ◦ ; C ∗ → r : a ` r[P] | a : ρ | S I G0
A ; ◦ ; C ` r[a?e.P] | a : e · ρ | S I ∗ → r : ahei.G0

(F.3)

This induces a contradiction since we would have the following for G 0
[ρ]

⊥
A ; ◦ ; C ` r[P] | a : ρ | S I G00

(F.4)

Note that the lack of ∗ → r : a in C does not affect since → : a 6∈ C.

G

Proofs for Theorem 5 (Progress)
X

If A ; ◦ ; C ` S I G then S −→ S0 , or ∀ n ∈ P (S) . S(n) = 0, or S −→.
Proof. The proof is by contradiction. If we had A ; Γ ; C ` S I G and S =⇒ S0 , with S0 6l,
S0 6= 0 and ∃n ∈ P (S0 ) : S0 (n) 6= 0. By Theorem 4, we should have A ; Γ ; C ` S0 I G 0 .
Let us take S0 ≡ n[a!e.P] | S00 (with S0 6l). No rule from Fig. 2 is applicable for this
process, and therefore S0 is not typable.

H

Proofs for Theorem 6 (Safety)

If A ; ◦ ; C ` S I G , then S is race free and S =⇒−→ error is not possible.
Proof. No error. The proof is by contradiction. Assume we have A ; Γ ; C ` S I G and
S =⇒ S0 with
S0 ≡ a : e · ρ | r[a?e0 .Q] | S00 and e 6= e0
so that S −→ error. By Theorem 4, we should have A ; Γ ; C ` S0 I G 0 , however, no
rule is applicable for S0 . Indeed we have S l, but e 6= e0 .
27

No Race. Straightforward by contradiction with Theorem 4, the following is not typable
S0 ≡ n[a?e.P] | m[a?e.Q] | S00
due to the condition on C, the premise S 6l in [.], and the fact that the set of channels
must be disjoint in concurrent branches. The other case (i.e. two sends) is similar.
Lemma 3. If A ; Γ ; C ` S I G , then, ∀ s → r : a ∈ FP (G ) : , either
∃!{s, r} ∈ P (S) : a ∈ R(S(s)) and a ∈ R(S(r)) or ∃!(r, a) ∈ P (S)× C (S) : a ∈ R(S(s))
Proof. By straightforward induction on the derivation. Each case follows by definition
of FP (G ), and the premise S 6l.

I

Proofs for Lemma 1 and Theorem 7 (Equivalences)

If A ; ◦ ; C ` S I G then ∀n ∈ S . G n . S(n).
Proof. Let B be a binary relation on processes defined as follows
(P, Q) ∈ B ⇐⇒ A ; Γ ; C ` S I G and ∃n ∈ P (S). G n = P and S(n) = Q
Let us show that B is a simulation.
a!e

– If G n −→ P1 then G n ≡ a!e.P1 ⊕ P2 and by Lemmas 30 and 32 we have that S(n) =
a!e

a!e.Q1 ⊕ Q2 and thus S(n) −→ Q1
Now we have to show that (P1 , Q1 ) ∈ B, i.e.
A ; Γ ; C ` S0 I G 0 with G 0 n = P1 and S0 (n) = Q1
Pose
S0 ≡ n[Q1 ] | a : e |

S(m)

∏

m6=n∈P (S)

by Lemma 2, A ; Γ ; C ` S0 I G 0 , and by Corollary 1, we have G 0n = P1 , as required.
a?e

– If G n −→ P1 then G n ≡ a?e.P1 + P2 and by Lemmas 30 and 32 we have that
a?e

S(n) = a?e.Q1 + Q2 and thus S(n) −→ Q1
Now we have to show that (P1 , Q1 ) ∈ B, i.e.
A ; Γ ; C ` S0 I G 0 with G 0 n = P1 and S0 (n) = Q1
Pose
S ≡ n[a?e.Q1 + Q2 ] | a : e · ρ |

∏

S(m)

m6=n∈P (S)

and
S0 ≡ n[Q1 ] | a : ρ |

∏

S(m)

m6=n∈P (S)

by Lemma 2, A ; Γ ; C ` S0 I G 0 , and by Corollary 1, we have G 0n = P1 , as required.
28

X

– If G n −→ P1 then G n ≡ 0 and P1 = 0, thus n 6∈ P (G ) and by Lemma 27 this means
X

that S(n) = 0, we then have S(n) −→ 0.
Lemma 4. The following holds:
1. If A ; Γ ; C ` n[a!e.P ⊕ P0 ] | S I G then G n ≡ a!e.Q ⊕ Q0
2. If A ; Γ ; C ` n[a?e.P + P0 ] | S I G then either G n ≡ a?e.Q + Q0 , or A ; Γ ; C `
n[P0 ] | S I G
Proof. The proof of 1 is by Lemma 26, and the proof of 2 is by Lemma 26 and rule [+].
If A ; ◦ ; C ` S I G then ∏n∈P (S) n[G n ] ≈ S.
Proof. For this proof we pose T = ∏m∈P (G ) m[G m ] | ∏b∈C (G ) b : G b .
n[a!e]

a·e

S sends. Assume S ≡ S0 | S1 , S0 −→ and S1 −→. We have
S ≡ n[a!e.P ⊕ P0 ] | a : ρ | S00

(I.1)

S0 ≡ n[P] | a : ρ · e | S00

(I.2)

and
n[a!e]

By Lemma 4, G n ≡ a!e.Q ⊕ Q0 , thus G n −→, and by Lemma 34 G a = ρ.
We then have (note that a ∈ C (G ))
T ≡ n[a!e.Q ⊕ Q0 ] | a : ρ |

m[G m ] |

∏

m6=n∈P (G )

b : G b

∏

(I.3)

b6=a∈C (G )

and by definition of −→,
T 0 ≡ n[Q] | a : ρ · e |

m[G m ] |

∏

m6=n∈P (G )

b : G b

∏

(I.4)

b6=a∈C (G )

Let us now show that
A ; Γ ; C ` S0 I G 0 with T 0 ≡

m[G 0 m ] |

∏

m∈P (G 0 )

∏

b : G 0 b

(I.5)

b∈C (G 0 )

By Lemma 2 we know that A ; Γ ; C ` S0 I G 0 , we have that G 0 n ≡ Q, by Corollary 1,
and G 0 a ≡ ρ · e by Lemma 34.
n[a!e]

a·e

T sends. Assume T ≡ T0 | T1 , T0 −→ and T1 −→. We have
T ≡ n[a!e.Q ⊕ Q0 ] | a : ρ |

∏

m[G m ] |

m6=n∈P (G )

∏

b : G b

(I.6)

b6=a∈C (G )

and
T 0 ≡ n[Q] | a : ρ · e |

∏

m6=n∈P (G )

29

m[G m ] |

∏

b6=a∈C (G )

b : G b

(I.7)

n[a!e]

By Lemma 1, we have S(n) −→, and since, by Lemma 28, a ∈ C (G ) ⇒ a ∈ C (S),
a·e
there is a queue a in S. Note that a queue a can always make a transition a : ρ0 −→
0
(regardless of ρ ). By Lemma 34, S(a) = ρ.
Therefore, we must have
S ≡ n[a!e.P ⊕ P0 ] | a : ρ | S00

(I.8)

And by definition of −→, we have
S0 ≡ n[P] | a : ρ · e | S00

(I.9)

Finally, we have
A ; Γ ; C ` S0 I G 0 with T 0 ≡

m[G 0 m ] |

∏0

m∈P (G )

b : G 0 b

∏0

(I.10)

b∈C (G )

by Lemma 2.
n[a?e]

e·a

S receives. Assume S ≡ S0 | S1 , S0 −→ and S1 −→. We have
S ≡ n[a?e.P + P0 ] | a : e · ρ | S00

(I.11)

S0 ≡ n[P] | a : ρ | S00

(I.12)

and
By Lemma 4 and (I.11), we have either

G n ≡ a?e.Q + Q0

(I.13)

A ; Γ ; C ` n[P0 ] | a : e · ρ | S00 I G

(I.14)

or
However, by assumption we have A ; Γ ; C ` S I G , with S as in (I.11), therefore (I.14)
cannot hold by Lemma 5.
e·a
a?e
By Lemma 34, we have that G a −→ and by (I.13), G n −→. By definition of −→,
we have
T ≡ n[a?e.Q ⊕ Q0 ] | a : e · ρ |

m[G m ] |

∏

m6=n∈P (G )

∏

b : G b

(I.15)

b : G 0 b

(I.16)

b6=a∈C (G )

Let us now show that
A ; Γ ; C ` S0 I G 0 with T 0 ≡

∏0

m[G 0 m ] |

m∈P (G )

∏0

b∈C (G )

By Lemma 2 we know that A ; Γ ; C ` S0 I G 0 , we have that G 0 n ≡ Q, by Corollary 1,
and G 0 a ≡ e · ρ by Lemma 34.
n[a?e]

e·a

T receives. Assume T ≡ T0 | T1 , T0 −→ and T1 −→. We have
T ≡ n[a?e.Q ⊕ Q0 ] | a : e · ρ |

∏

m[G m ] |

m6=n∈P (G )

∏

b : G b

(I.17)

b6=a∈C (G )

and
T 0 ≡ n[Q] | a : ρ |

m[G m ] |

∏

m6=n∈P (G )

30

∏

b6=a∈C (G )

b : G b

(I.18)

a?e

By Lemma 1, we have S(n) −→, and by Lemma 34, we have S(a) = ρ, therefore
S ≡ n[a?e.P + P0 ] | a : e · ρ | S00

(I.19)

S ≡ n[P] | a : ρ | S00

(I.20)

and
We now have to show that
A ; Γ ; C ` S0 I G 0 with T 0 ≡

∏

m[G 0 m ] |

m∈P (G 0 )

∏

b : G 0 b

(I.21)

b∈C (G 0 )

as before, we have G 0 n = P by Corollary 1 and G 0 a = ρ by Lemma 34.
X

X

End. If S −→ S, then S ≡ 0 and G ≡ 0, and vice versa if T −→ T .
Lemma 5. If
A ; Γ ; C ` r[a?e.P + P0 ] | a : e · ρ | S I G
is derivable then
A ; Γ ; C ` r[P0 ] | a : e · ρ | S I G 0
is not derivable.
Proof. Assume P0 ≡ b?e.P00 . We show that we must have

G ≡ (∗ → r : ahei.G0 | G1 ) ; G2
and the derivation of G must have the following form
..
.
A0 ; ◦ ; C ` r[P0 ] | a : ρ0 | S00 I G0
[.]
A0 ; ◦ ; C ` r[a?e.P0 ] | a : e · ρ0 | S00 I ∗ → r : ahei.G0
[+]
A0 ; ◦ ; C ` r[a?e.P0 + P00 ] | a : e · ρ0 | S00 I ∗ → r : ahei.G0
..
.
[|]
[ ;]

A1 ; ◦ ; C ` S01 I G1
A ; ◦ ; C ` r[a?e.P0 + P00 ] | a : e · ρ0 | S0 I ∗ → r : ahei.G0 | G1
A ; Γ ; C ` r[a?e.P + P0 ] | a : e · ρ | S I G

..
.

G2

where we must have
– S l or G1 = G2 = 0 and S0 l or S01 ≡ 0.
– split(S) = (r[a?e.P0 + P00 ] | a : e · ρ0 | S0 , ) (the second part of the split does not
matter)
– b 6∈ R(S) (by Lemma 7)
– A0 ∩ A1 = ∅ and b 6∈ A2 because of rules [ | ] and [+]
31

Now let us discuss a derivation for G 0 . Since we have b 6∈ R(S), we must have
split(r[P0 ] | a : e · ρ | S) = (S1 , S2 ) such that S1 (r) = P0 , and S1 (a) = e · ρ, if the split
does exist. If it does, we have Ψ; Θ ` r[P0 ] | a : e · ρ | S m Ω such that ∀N ∈ Ψ . r 6∈ N.
Therefore, the split for the rest of the system is the same as in the other derivation.
Again, we can divide the system using [ | ] if need be such that we get
A0 ; ◦ ; C ` r[P00 ] | a : e · ρ0 | S00 I ∗ → r : ahei.G0
with S00 6l therefore no rule is applicable for this judgement, and the derivation does not
exist.
Lemma 6. Let S a system such S 6l, and a, b 6∈ R(S) the following is not derivable
T ≡ s1 [a!e.P1 ] | s2 [b!e0 .P2 ] | r[a?e.Q + b?e0 .Q0 ] | S
Proof. We show this by contradiction. Given T as above, the only rule applicable is
[+] on r either selecting the branch on a or on b. Therefore, the following should be
derivable

[.]
[+]

..
.
A ; Γ ; C ` s1 [P1 ] | s2 [b!e0 .P2 ] | r[Q] | S I G
A ; Γ ; C ` s1 [a!e.P1 ] | s2 [b!e0 .P2 ] | r[a?e.Q] | S I s1 → r : ahei.G
A ; Γ ; C ` T I s1 → r : ahei.G

and, we must have a, b ∈ A and s1 [P1 ] | r[Q] | Sl. And the other derivation as the form:

[.]
[+]

..
.
A ; Γ ; C ` s1 [a!e.P1 ] | s2 [P2 ] | r[Q] | S I G
A ; Γ ; C ` s1 [a!e.P1 ] | s2 [b!e0 .P2 ] | r[b?e0 .Q0 ] | S I s2 → r : bhe0 i.G 0
A ; Γ ; C ` T I s2 → r : bhe0 i.G 0

where we have a, b ∈ A and s2 [P2 ] | r[Q] | S l. However, this is clearly in contradiction
with Theorem 2, i.e.
s1 → r : ahei.G 6≡ s2 → r : bhe0 i.G 0
Lemma 7. Let S a system such S 6l, and a, b 6∈ R(S) the following is not derivable
T ≡ s1 [a!e.P1 ] | b : e0 · ρ | r[a?e.Q + b?e0 .Q0 ] | S
Proof. The proof is similar to the one of Lemma 7 where b : e0 · ρ replaces s2 [b!e0 .P2 ].

J

Proofs for Theorem 8 (Completeness wrt G )

If • `G and G is projectable, then there is G 0 ≡ G such that A ; Γ ; C ` ∏n∈P (G ) n[G n
] I G 0.
32

Proof. By Lemma 8, with P = P (G ) and Γ = ◦ since G is closed by assumption.
Lemma 8. Let Proj(G , P) = ∏n∈P n[G n ] with P (G ) ⊆ P, and if G n = 0, then n is not
in P.
If C `G , G is projectable, and ∀ χ ∈ fv(G ) . ∀ n ∈ P . ∃ (n, χ) : χ ∈ Γ then

C (G ) ; Γ ; C ` Proj(G , P) I G 0 with G ≡ G 0
Proof. We show this by induction on the structure of G . Let
S ≡ ∏ G n

SQ ≡

n∈P

∏

G n

A = C (G )

n∈P\Q

G ≡ s → r : ahei.G0 + G1 .
By definition of projection, we have
S ≡ s[a!e.G0 s ⊕ G1 s ] | r[a?e.G0 s + G1 s ] | S{s,r}
We can apply rules [⊕], [+] (twice) and [.] in order to have the result, i.e.
by IH
[.]

A ; Γ ; Ca ` s[G0 s ] | r[G0 s ] | S{s,r} I G0

by IH

A ; Γ ; C ` s[a!e.G0 s ] | r[a?e.G0 s ] | S{s,r} I G 0

A ; Γ ; C ` Proj(G1 , P) I G1

A; Γ; C ` S I G

with G 0 = s → r : ahei.G0 , and Ca = C s → r : a note that the later is defined by
C `G . Observe that S{s,r} 6l otherwise that would mean that ∃ s0 → r0 : b ∈ R(G0 ) such
that {s, r} ∩ {s0 , r0 } = ∅ which is in contradiction with C `G . Finally, it is obvious that
a∈A

and

R(Gi r ) ⊆ A

i ∈ {0, 1}

since A = C (G ).

G ≡ G0 | G1 .
We have S of the form, by definition of projections (and well-formedness)
S ≡ Proj(G0 , P0 ) | Proj(G1 , P1 ) with P0 ∩ P1 = ∅
Note that since #(FO (G )) > 1, we have fv(G ) = ∅, therefore, by IH, we have
Ai ; ◦ ; C ` Proj(Gi , P) I Gi0

and

Gi ≡ Gi0 and Ai = C (Gi )

We have the result by applying rule [ | ]:
by IH
by IH
A0 ; ◦ ; C ` Proj(G0 , P0 ) I G1
A1 ; ◦ ; C ` Proj(G1 , P1 ) I G1
A1 ∪ A2 ; Γ ; C ` S I G
By well-formedness we have, A0 ∩ A1 = ∅, and Lemmas 28 and 28 guarantee that each
Ai is large enough.
33

G ≡ µ χ.G 0 .
By definition of projections, we have
S ≡ ∏ n[µ χ.G 0 n ]
n∈P

Since G 0 is prefix-guarded, there must be s, r ∈ P (G 0 ) such that
s[µ χ.G 0 s ] | r[µ χ.G 0 r ] l
Therefore, rule [µ] is applicable here
A ; Γ0 ; C ` s[G 0 s ] | r[G 0 r ] |

∏

n[G 0 n ] I G 0

n∈P\{s,r}

0

A ; Γ ; C ` s[µ χ.G s ] | r[µ χ.G 0 r ] | S{s,r} I G
where
Γ0 = Γ · (s, χ) : χ), (r, χ) : χ · ΓS

and

ΓS such that ∀ n ∈ P (S{s,r} ).Γ(n, χ) = χ

The rest follows by induction hypothesis.

G = χ. Then, we have
S ≡ ∏ n[χ]
n∈P

By assumption, we have ∀ n ∈ P . ∃ (n, χ) : χ ∈ Γ, hence we can apply rule
are done.

[X]

and we

G ≡ G0 ; G1 . Then we have
S ≡ ∏ G0 n [G1 n /0]
n∈P

Let us show that split(S) = (S0 , S1 ) and
S0 ≡ ∏ G0 n = Proj(G0 , P) and
n∈P

S1 ≡ ∏ G1 n = Proj(G1 , P)
n∈P

Since G is well-formed, we have Ψ; Θ ` S m Ω coherent if we pose
Ψ = {N|N ∈ FP (G0 )}

and

Θ = {{s, r}|s → r : a ∈ R(G1 )}

For each Gi a top level concurrent branch of G0 , we have that
{P (Gi )}; ∅ ` Proj(Gi , P (Gi )) m Ωi
is derivable by Lemma 15, since Proj(Gi , P (Gi )) is typable by IH. In addition, we have
Gi n = Ωi (n)[0/ε].
By construction, we have
Ψ0 ; Θ ` Proj(G0 , P) m Ω0
with Ψ0 = {N 0 |∃N ∈ Ψ : N 0 ⊆ N}.
34

with ∀n ∈ P . Ω0 (n) = ε

Finally, we have ∀n ∈ P . S(n) % Ω(n) 6= ⊥ since the same suffix G1 n is added to
each branch of a behaviour, and S(n) % Ω(n) = G1 n . We have the required result by IH
and rule [ ;].

G ≡ 0.
We have
S ≡ ∏ n[0]
n∈P

and the results holds by rule [0].

K
K.1

Accessory Results
Linearity

Lemma 9. If C s → r : a is defined, then either
1.

→ : a 6∈ C,
s→r:a

2. C( → : a) =

,
C0
∗→r:a

3. C( → : a) =

, or
C0
4. ∃ → r : and → s : ∈ C

Proof. The proofs of 1 and 2 follow directly from Def. 2 and the definition of C( ). The
proof of 3 follows by definition of C( ) and the fact that, by Def. 1, there cannot be an
output dependency from s0 → r0 : b and ∗ → r : a since
s → r : b 6≺OO ∗ → r : a

and

s → r0 : b 6≺IO ∗ → r : a

since s 6= ∗ 6= r

Therefore, ∗ → r : a must be the first prefix with label → : a in C. The proof of 4
follows from the Def. 2. In fact, since whenever the sender/receiver are different on
two nodes with common channel there must be two dependency relation we have the
following cases. In the following, we assume that there is no prefix on a in the ellipsis.
If only the senders are different, i.e. the following appears on a path in C
s0 → r : a . . . s → r : a
then we have s0 → r : a ≺II s → r : a and we must have at least a node between the two
such that, e.g. s0 → r : a ≺OO s0 → s : b ≺IO s → r : a and we have the result. If only
the receivers are different, we have
s → r0 : a . . . s → r : a
35

and we have s → r0 : a ≺OO s → r : a and we must have at least one node between the
two such that s → r0 : a ≺IO r0 → r : b ≺II s → r : a, and we have the result. If both
sender and receiver are different, i.e.
s0 → r0 : a . . . s → r : a
then we need two nodes c1 and c2 such that, (i) c1 = → r : b, otherwise there would
be a ≺II relation in the input dependency, (ii) c2 = → s : c otherwise there would be a
≺IO relation in the output dependency (note that ≺OO is only defined if the channels are
the same). In fact, there must an input dependency, e.g.
s0 → r0 : a ≺IO r0 → s1 : b1 ≺IO s1 → s2 : b2 ≺IO s2 → r : b3 ≺II s → r : a
and an output dependency, e.g.
s0 → r0 : a ≺IO r0 → s : c ≺IO s → r : a
Observe that, in the first chain, we have s2 → r : b3 , and r0 → s : c in the second.
Actually, the shortest (input) chain when both pair of participants are different is
s0 → r0 : a ≺IO r0 → s : c1 ≺IO s → r : c2 ≺II s → r : a
where we also have r0 → s : c1 ≺IO s → r : a, for the output chain. Notice that in this
case we have r0 → s : c1 and s → r : c2 in C.
Corollary 2. If linearity holds on C and ∗ → n : a ∈ C, then
∗→n:a
C( → : a) =
C0
Lemma 10. If C ∗ → r : a ` G then C ` G and if Γ ; C ∗ → r : a ; S ` G I then
Γ ; C ; S ` G I.
Proof. We have to show that if ∗ → r : a is involved in a input or output dependency,
then there is another dependency between the same two nodes without ∗ → r : a. Note
first that by Lemma 9, we know that ∗ → r : a 6∈ C, therefore, if there is a need to have
a chain of the form
∗ → r : a ≺ . . . ≺ s0 → r0 : a
this need disappears with ∗ → r : a (dependencies are needed only between nodes with
a common channel). Thus, if ∗ → r : a is the first node in a dependency chain, then the
result holds trivially. Observe that ∗ → r : a 6≺OO s → r0 : b and s → r0 : b 6≺OO ∗ → r : a
for any a, b since ∗ 6= s, for the same reason, we have s → r : b 6≺IO ∗ → r : a.
Finally, we have the following cases, where the left hand side describes the dependency involving a and the right hand side shows that the dependency between the two
external nodes still exists without the node on a.
s → r : b ≺II ∗ → r : a ≺II s0 → r : c

⇒

s → r : b ≺II s0 → r : c

s → r : b ≺II ∗ → r : a ≺IO r → s0 : c

⇒

s → r : b ≺IO r → s0 : c

36

K.2

Splitting systems

Lemma 11.
{n, m} ⊆ Θ ⇒ ∃N 6= M ∈ Ψ : n ∈ N ∧ m ∈ M
Proof. Direct from rules [ε] and [ax].
Lemma 12. If A ; Γ ; C ` S I G and Ψ; Θ ` S m Ω is derivable and coherent, then
(n, m) ∈ ~ ⇐⇒ {n, m} ⊆ N with N ∈ Ψ
Proof. (⇐) follows directly from the fact that the judgement is coherent. (⇒) The proof
is by contradiction. Assume that there is (n, m) ∈ ~ with n ∈ N and m ∈ M, where
N 6= M ∈ Ψ (assuming C (Ω(n)) ∩ C (Ω(m)) 6= ∅, without loss of generality).
Let us consider the following judgement:
Ψ0 · N · M; Θ ` n[a!e.P1 ] | m[a?e.P2 ] | S0 m Ω0 · n : a!e.π · m : a?e.ϕ
Note that rule [ε] is not applicable here since we do not have n : ε and m : ε. Looking
at the rules we see that only two applications of [sync] would introduce n : a!e.π and
m : a?e.ϕ.
For this rule to be applicable we must have S0 ≡ n0 [a?e.P3 ] | m0 [a!e.P4 ] | S00 , and
0
n ∈ N, m0 ∈ M.
By definition of split and since rule ; must be applied for A ; Γ ; C ` S I G to
hold, we should be able to derive
A ; Γ ; C ` n[a!e.Q1 ] | m[a?e.Q2 ] | n0 [a?e.Q3 ] | m0 [a!e.Q4 ] | S00 I G
However, this is not derivable due to the obvious race on channel a!
Lemma 13. If
split(r[P] | a : ρ | T ) = (S00 , S10 ) such that

S00 (r) = P0

and

S00 (a) = ρ0

then
split(r[a?e.P] | a : e·ρ | T ) = (S0 , S1 ) such that

S0 (r) = a?e.P0

and

S0 (a) = e·ρo

In addition, ∀n ∈ P (T ) : Si (n) = Si0 (n), for i ∈ {0, 1}.
Proof. Straightforward (runtime rule)
Lemma 14. If A ; Γ ; C ` s[a!e.P ⊕ P0 ] | a : ρ | T I G and
split(s[a!e.P ⊕ P0 ] | a : ρ | T ) = (S1 , S2 )
such that
S1 (s) = a!e.P0 ⊕ P00

and

S1 (a) = ρ

then we have
split(s[P] | a : ρ · e | T ) = (S10 , S20 ) such that

S10 (s) = P0

and

and ∀n 6= s ∈ P (S).S1 (n) = S10 (n) and S2 (n) = S20 (n), ditto ∀a ∈ C (S).
37

S10 (a) = ρ · e

Proof. We must have a judgement of the form
Ψ; Θ ` s[a!e.P ⊕ P0 ] | a : ρ | T m Ω · s : a!e.P0 ⊕ P00 · r : a?e.Q0 ⊕ Q00 · a : ρ
Since the system is derivable, we have to use [q] until the queue is empty (otherwise
linearity would not be preserved). Then only use [sync] to remove the send on a, therefore
both ρ and the send should be on the same part of the split. After reduction, we have
the following judgement
Ψ; Θ ` s[P] | a : ρ · e | T m Ω · s : P0 · r : a?e.Q0 ⊕ Q00 · a : ρ · e
Since r was able to receive e from s before, it must be able to receive it from the queue
as well (note that there is not restriction on wrt Ψ with action on queues).
Lemma 15. If A ; Γ ; C ` S I G then {P (S)}; ∅ ` S m Ω and Ω(n)[0/ε] ≡ S(n).
Proof. Straightforward induction on the derivation of {P (S)}; Θ ` S m Ω. Note that
for each rule of the split, there is a rule in the inference system, whose premises are
always weaker. Also, [ε] is not applicable (since Θ is empty) and Ω keeps track of
everything that happens (module the branches which are not taken).
Lemma 16. If A ; Γ ; C ` S I G and Ψ; Θ ` S m Ω is coherent, then ∀ Ψ0 , Θ0 , Ω0 such
that Ψ0 ; Θ0 ` S m Ω0 is coherent: Ψ = Ψ0 , Θ = Θ0 and Ω = Ω0 .
Proof. First, recall that by Lemma 12:
(n, m) ∈ ~ ⇐⇒ {n, m} ⊆ N with N ∈ Ψ
We first show that Ψ (such that the split is coherent) is unique. Note that because of
condition (4.2) and the fact that A ; Γ ; C ` S I G , it is not possible to have a coherent
judgement with Ψ0 like Ψ except for two sets in Ψ being merged (subdivided) in Ψ0 .
Indeed, the number of interacting pairs of participants is fixed in S. The only changes
one can do in Ψ are as follows
1. Add n in N ∈ Ψ (with n not in Ψ).
2. Remove n in N ∈ Ψ (with n in Ψ).
3. Permute n ∈ N ∈ Ψ with m ∈ M ∈ Ψ.
We now show that any of these changes makes the judgement not coherent.
Case 1. Assume Ψ = N · Ψ0 and Ψ0 = {n} ∪ N · Ψ0 . This means that Ω0 (n) 6= 0 and
0
Ω (n) 6= ε (otherwise ~ would not be total on {n} ∪ N), and Ω(n) = 0, or Ω(n) = ε, or
n only received from queues. This means that n interact with participants in Ω0 but not
in Ω, which means that at some point in the derivation of Ω we have n[ ] | S0 6l while
we have n[ ] | S0 l in the derivation for Ω0 . However, since G is typable, there cannot
be races in the systems and therefore, the interaction between pair of participants must
be the same in both derivations of Ω and Ω0 .
Case 2. Assume that Ψ = {n} ∪ N · Ψ0 and Ψ0 = N · Ψ0 , the case is similar to the
previous one, we have that at some point in the derivation of Ω0 we have n[ ] | S0 6l
while we have n[ ] | S0 l in the derivation for Ω.
38

Case 3. Assume that Ψ = {m} ∪ N · {n} ∪ M · Ψ0 and Ψ0 = {n} ∪ N · {m} ∪ M · Ψ0 .
We know that
∀n0 ∈ N . C (Ω(n0 )) ∩ C (Ω(m)) = ∅

and ∀m0 ∈ M . C (Ω(m0 )) ∩ C (Ω(n)) = ∅

since the original judgement is coherent and the system typable. This implies that we
cannot have ~ total neither on {n} ∪ N nor on {m} ∪ M. Therefore the judgement is not
coherent.
We now consider the changes that one can make on Ω. Note that changes on Ω
must be done on pairs of participants since they always interact by pair (except for
those which interact only with queues but that has no effect on Ψ or Θ).
1. There is n1 , n2 such that Ω(ni ) is a prefix of Ω0 (ni ). A pair of elements in Ω0 can
only be longer if one merges two in Ψ, which is possible (see above).
2. There is n1 , n2 such that Ω0 (ni ) is a prefix of Ω(ni ). A pair of elements in Ω0 can
only be shorter if two a set in Ψ is subdivided into two sets which is not allowed
either.
We consider changes that can be made on Θ:
1. Add {n, m} to Θ, then, that pair will not allow the derivation to reach the axiom,
unless sets in Ψ are sub-divided, which is not possible.
2. Remove {n, m} from Θ, then, there will be a pair missing to reach the axiom (plus
↔Θ might not be total any more); unless two sets in Ψ are merged, but this is not
possible.
3. Permutation in Θ would only possible if one could permute participants in sets of
Ψ which, by above, is not possible.
K.3

Others

Lemma 17. If G 6≡ G0 | G1 and • `G then RG is total on P (G ).
Proof. We show this by induction on the structure of G .
G ≡ s → r : ahei.G 0 . By definition (s, r) ∈ RG and by IH RG 0 is total on P (G 0 ). Since
G is well-formed we have
∀ n1 → n2 : ∈ R(G 0 ) . {n1 , n2 } ∩ {s, r}
Thus there is (s, ni ) ∈ RG or (r, ni ) ∈ RG and we have the required result by definition
of RG and Def. 1.

G ≡ G0 + G1 . By IH, RGi is total on P (Gi ) for i ∈ {0, 1}. Since G is well-formed we
have
∀ s → r : a ∈ R(G ).∀ s0 → r0 : b ∈ R(G 0 ) . s = s0 ∧ a 6= b
i.e. s = s0 ∈ Gi , and we have the required result by definition of RG and Def. 1.

G ≡ s → r : ahei.(G0 | G1 ). By IH RGi is total on P (Gi ). Since G is well-formed we
must have s ∈ P (Gi ) and r ∈ P (G j ) with i 6= j ∈ {0, 1}. We have the required result
since we have (s, r) ∈ RG by definition of RG and Def. 1.
39

G ≡ G0 ; G1 . Observe that by IH and by definition of FP , we have that ∀N ∈ FP (Gi ) . RGi
is total on N, with i ∈ {0, 1}.
Since the projection is defined as G n = G0 n [G1 n /0], we have that
∀ N0 × N1 ⊆ FP (G0 ) × FP (G1 ) : RG is total on N0 ∪ N1 if there is n ∈ N0 ∩ N1
Since RG is a transitive relation, let us define a transitive relation on the intersection of
sets of participants from G0 and G1 :

N0 ∩ N1 6= ∅ or

(N0 , N1 ) ∈ W
⇐⇒
∃ (M0 , M1 ) : (N0 , M1 ) ∈ W and (M0 , N1 ) ∈ W

It is easy to see that RG is total on any N0 ∪ N1 whenever (N0 , N1 ) ∈ W, thus
[

RG is total on

N0 ∪ N1

(N0 ,N1 )∈W

Let us show that
(N0 , N1 ) ∈ FP (G0 ) × FP (G1 ) ⇒ (N0 , N1 ) ∈ W
Since G is well-formed we have
∀ s → r : ∈ R(G1 ) . ∃N1 6= N2 ∈ FO (G0 ) . s ∈ N1 ∧ r ∈ N2

(K.1)

∀N ∈ FP (G0 ) . ∃N 0 ∈ FP (G1 ) . N ∩ N 0 6= ∅

(K.2)

and
Therefore, by (K.1) and the fact that s → r : ∈ R(G1 ) ⇒ {s, r} ⊆ N ∈ FP (G1 ), we have
∀N1 ∈ FP (G1 ) . ∃N0 6= N00 ∈ FP (G0 ) : N0 ∩ N1 6= ∅ and N00 ∩ N1 6= ∅

(K.3)

By (K.2), we have
∀N0 ∈ FP (G0 ) . ∃N1 ∈ FP (G1 ) : N0 ∩ N1 6= ∅

(K.4)

Now assume that there is (N0 , N1 ) ∈ FP (G0 ) × FP (G1 ) such that (N0 , N1 ) 6∈ W, this is
contradiction with (K.3) and (K.4).

G ≡ µ χ.G . By IH
Other cases. The cases where G = 0 or G = χ are trivial.
Lemma 18. If A ; Γ ; C ` S I G and • `G then the following holds
∀n ∈ P (S) : C (S(n)) ⊆ C (G n )
Proof. Straightforward induction on the validation rules.
Lemma 19. If A ; Γ ; C ` S I G and RG is total on P (G ) then RS is total on P (S).
Proof. By Lemmas 17 and 18 and the definition of RS .
40

Lemma 20. If • `G then ∀N ∈ FO (G ) . RG is total on N.
Proof. By Lemma 17 and the definition of FO .
Lemma 21. If A ; Γ ; C ` S I G0 ; G1 , C `G0 , Ψ; Θ ` S m Ω is coherent, and split(S) 6=
⊥ then
∀n, m ∈ P (S) : (n, m) ∈ RG0 ⇒ (n, m) ∈ ~
Proof. Straightforward by definitions of RG0 and ~. Note that external choice branches
which do not appear in Ω do not appear in G0 either.
Lemma 22. If bv(S) 6= ∅ then split(S) = ⊥.
Proof. If bv(S) 6= ∅, we must have
S ≡ n[P] | S0 where µ x.P0 is a suffix of P
The result follows from the fact that there is no rule in Fig. 3 which “removes” recursive definition. Therefore, it not possible to derive a split whenever there is a recursion
definition in the system to be split.
Lemma 23. If A ; Γ ; C ` S I µ χ.G and χ ∈ fv(G ) then #(FO (G )) = 1.
Proof. The proof follows from the fact that the context Γ is emptied each time the rule
[ | ] is used in the derivation (this rule is the only one introducing concurrent branches).
In addition, for the axiom [ X ] to be used in the derivation one must have ( , ) : χ ∈ Γ.
Therefore, the only way one could have #(FO (G )) > 1 (i.e. at least two concurrent
branches in G ) is if χ does not appear in G .
Lemma 24. If A ; Γ ; C ` S I G and bv(S) = ∅ then bv(G ) = ∅
Proof. By straightforward induction on the rules of Fig. 2.
Lemma 25. If C `G then • `G
Proof. This follows from the fact that •C is always defined.
Lemma 26. If A ; Γ ; C ` S I G and G is well-formed

G ≡ ((n → m : ahei.G1 + G2 ) | G3 ) ; G4 ⇐⇒ S ≡ n[a!e.P ⊕ P0 ] | m[a?e.Q + Q0 ] | S0
Proof. (⇒) Assume that
A ; Γ ; C ` S I ((n → m : ahei.G1 + G2 ) | G3 ) ; G4
is derivable. We show that either a rule introducing the corresponding operator is applicable or that an equivalent G can be inferred.
41

– If A ; Γ ; C ` S I G 0 ; G4 is derivable then we have either split(S) = ⊥ then G4 = 0,
thus
A; Γ; C ` S I G0
or split(S) 6= ⊥, in this case, we must have
split(S) = (S1 , S10 )
with
A ; ◦ ; C ` S1 I G 0 and A ; ◦ ; C T (G 0 ) ` S10 I G4
– Assume G 0 = G 00 | G3 , if A ; Γ ; C1 ` S1 I G 0 is derivable then we must have either
S1 ≡ S2 | S3 , A = A1 ∪ A2 , and A1 ∩ A2 = ∅ such that
A1 ; ◦ ; C ` S2 I G 00

and A2 ; ◦ ; C ` S3 I G3

are derivable, or S3 = 0 and G3 ≡ 0.
– Assume G 00 = G 000 + G2 , we must have either
S2 = n[P0 ⊕ P00 ] | S4

(K.5)

and
A1 ; ◦ ; C ` n[P0 ] | S4 I G 000

and

A1 ; ◦ ; C ` n[P00 ] | S4 I G2

are derivable, or P00 ≡ 0 and G2 ≡ 0.
– Assume G 000 = n → m : ahei.G1 , we must have
P0 ≡ a!e.P

and

S4 ≡ m[a?e.Q + Q0 ] | S0

(K.6)

and
A1 ; ◦ ; C ` n[P0 ] | m[a?e.Q + Q0 ] | S0 I G1
derivable.
Putting (K.5) and (K.6) together, we have that
S ≡ n[a!e.P ⊕ P0 ] | m[a?e.Q + Q0 ] | S0
(⇐) Assume
A ; Γ ; C ` n[a!e.P ⊕ P0 ] | m[a?e.Q + Q0 ] | S0 I G

(K.7)

We show that either a rule introducing the corresponding operator is applicable or that
an equivalent G can be inferred.
– Either split(S) = ⊥ in which case G ≡ G 0 ; 0 or
split(S) = (S1 , S10 )
and we must have G4 6≡ 0 and
A ; Γ ; C ` S1 I G
with
S1 (n) = a!e.P0 ⊕ P00

and

S1 (m) = a?e.Q0 + Q00

and S10 (n) = P1

and

S10 (m) = Q1

such that
a!e.P ⊕ P0 ≡ (a!e.P0 ⊕ P00 )[P1 /0] and
42

a?e.Q + Q0 ≡ (a?e.Q0 + Q00 )[Q1 /0]

– Either there is
S = n[a!e.P0 ⊕ P00 ] | m[a?e.Q0 + Q00 ] | S1 | S2

G 0 = G 00 | G3 and A = A1 ∪ A2 , and A1 ∩ A2 = ∅
A1 ; ◦ ; C ` n[a!e.P0 ⊕ P00 ] | m[a?e.Q0 + Q00 ] | S1 I G 00

and

A2 ; ◦ ; C ` S2 I G3

where S1 6l (this is a sound assumption, since one could apply
times as necessary to obtain this), or G3 ≡ 0.
– Either there is G 00 ≡ G 000 + G2 such that

[ ;]

and

[|]

as many

A ; ◦ ; C1 ` n[a!e.P0 ] | m[a?e.Q0 + Q00 ] | S1 I G 000
and
A ; ◦ ; C1 ` n[P0 ] | m[a?e.Q0 + Q00 ] | S1 I G2
or G2 = 0.
– For
A ; ◦ ; C1 ` n[a!e.P] | m[a?e.Q + Q0 ] | S1 I G 000
to be derivable, we must have G 000 ≡ n → m : aheiG1 .
Putting all the pieces together, we have the required result.
Lemma 27. If A ; Γ ; C ` S I G then
∀n ∈ P (S). S(n) 6= 0 : n ∈ P (S) ⇐⇒ n ∈ P (G )
and
∀n ∈ P (S). S(n) = 0 ⇐⇒ n 6∈ P (G )
Proof. Straightforward.
Lemma 28. If A ; Γ ; C ` S I G then C (G ) ⊆ C (S).
Proof. Straightforward induction on the derivation.
Lemma 29. If A ; Γ ; C ` S I G then C (S) ⊆ A.
Proof. Straightforward induction on the derivation.
Lemma 30. If G is well-formed and projectable then
– if G n ≡ a!e.P ⊕ Q then there is a branch of G such that the first prefix on n is
n → m : ahei.
– if G n ≡ a?e.P + Q then there is a branch of G such that the first prefix on n is
m → n : ahei.
Proof. By definition of Projection.
43

Lemma 31. If A ; Γ ; C ` S | a : e · ρ I G is derivable then for each branch in G the
first prefix on a is ∗ → n : ahei.
Proof. Follows from the fact that for a common channel, [ρ] must be used before [.] (see
Lemma 2).
Lemma 32. If A ; Γ ; C ` S I G and there is a branch in G such that n → m : ahei is
the first prefix on n (resp. m), then S(n) = a!e.P ⊕ P0 (resp. S(m) = a?e.Q + Q).
Proof. Straightforward.
Lemma 33. If fv(S) = ∅, and S −→ S0 , then fv(S0 ) = ∅, i.e. reduction of systems
preserves closeness.
Proof. Follows directly from the semantics of the calculus.
Lemma 34. If a ∈ C (G ) then
A ; Γ ; C ` a : ρ | S I G ⇐⇒ then G a = ρ
In addition, a 6∈ C (G ) ⇒ ρ = [].
Proof. Follows from rules [ρ] and [0].

44

