GRAPH TYPES FOR MONADIC MOBILE PROCESSES

NOBUKO YOSHIDA

Department of Computer Science University of Edinburgh The King’s Buildings Mayfield Road Edinburgh, EH9 3JZ, UK

                        e-mail: ny@dcs.ed.ac.uk

abstract

While types for name passing calculi have been studied extensively in the context of sorting of polyadic π-calculus [26, 7, 43, 11, 36, 41, 24, 42, 14, 22], the type abstraction on the corresponding level is not possible in the monadic setting, which was left as an open issue by Milner [26]. We solve this problem with an extension of sorting which captures dynamic aspects of process behaviour in a simple way. Equationally this results in the full abstraction of the standard encoding of polyadic π-calculus into the monadic one: the sorted polyadic π-terms are equated by the basic behavioural equality in the polyadic calculus if and only if their encodings are equated in the basic typed behavioural equality in the monadic calculus. This is the first result of this kind we know of in the context of the encoding of polyadic name passing, which is a typical example of translation of high-level communication structures into π-calculus. The construction is general enough to be extendable to encodings of calculi with more complex operational structures.

1. Introduction

The monadic π-calculus [28, 25] is a powerful formalism in which we can construct complex structures of concurrent computing by combining simple monadic name passing. The construction of significant computational structures in this calculus is done by passing and using private names between interacting parties to control the sharing of interaction points. For example, the following process expresses communication of a sequence of names (below ax.P is input and \overline{a}v.P is output, (a)P denotes scope restriction, and c, z are fresh).

az.zx_{1}.zx_{2}.zx_{3}.P | (c) \overline{a}c.\overline{c}v_{1}.\overline{c}v_{2}.\overline{c}v_{3}.Q ⟶ P \{v_{1}v_{2}v_{3}/x_{1}x_{2}x_{3}\} | Q (1.1)

In this example, coming from [28], the private channel c is used during interaction, so that, after the initial step, the communication of v_{1}, v_{2} and v_{3} is done deterministically without interference from the third party. This example also shows that we can represent polyadic (multiple) name passing from monadic name passing. Another example with a more complex communication structure follows.

az.zx_{1}.\overline{z}v_{1}.zx_{2}.\overline{z}v_{2}.P | (c) \overline{a}c.\overline{c}w_{1}.cy_{1}.\overline{c}w_{2}.cy_{2}.Q ⟶ P \{w_{1}w_{2}/x_{1}x_{2}\} | Q\{v_{1}v_{2}/y_{1}y_{2}\} (1.2)

Note input and output are mixed together. As in the previous example, once two parties start interaction, a sequence of communication is done following a prescribed protocol using a private channel. The same scheme can be easily generalised to more complex communication structures, including those with parallelism and complex information flow.

As a means to study rich computational structures representable in name passing processes, a notion of types called sorting was introduced by Milner [26] and has been studied extensively since then [7, 43, 11, 36, 41, 24, 42, 14, 22]. Sorting shows how a name carries another name. For example, if v has a type, say, nat, and we have a term \overline{a}v.0, then a should have a type (nat), a type which carries nat. This idea and its ramifications have been used to analyse significant semantic properties of calculi with polyadic name passing. However, as was already noticed in [26], the sorting in the monadic π-calculus is not powerful enough to type-abstract known encodings of polyadic name passing like (1.1) above: Indeed, (1.1) becomes ill-sorted if v_{1}, v_{2}, v_{3} have different sorts. As far as we know, the situation remains the same with the refinements of sorting proposed in [36, 22, 14]. This means, among other things, the sorting restricted to the monadic terms does not give as rich semantic analysis as in the polyadic case, while behaviourally the above encoding does mimic polyadic name passing. In general, this is because the sorting does not capture the dynamic structure of interaction, especially those using the transmission of private names as in (1.1) and (1.2), which is omnipresent even in the polyadic setting.

The present paper develops a syntactic theory of types for monadic π-calculus which extends the sorting in a simple way and by which we can extract the abstract operational structures of π-terms including those of (1.1), (1.2) as well as more complex ones (cf.2.5). The key technical idea is to represent a class of dynamic communication behaviour of mobile processes using simple combinatorial expressions, i.e. graphs. In a graph type, nodes denote atomic actions and edges denote the activation ordering between them, representing as a whole a deterministic protocol a process will be engaged in. As a simple example, suppose we have two terms gb.(cx.\overline{b}x | (f)\overline{d}f.c′x.\overline{f}x) and px.(\overline{c}x | \overline{c′}x). Then they may be given types: Here on the left side, the action

g ↓ (b) (the input of fresh name b) should take place directly preceding c ↓ x and d ↑(f) (and indirectly all the rest), while there is no activation ordering between, for example, c ↓x and f ↑x in the same graph. Now if two protocols are compatible, we can compose them via “cuts,” i.e. pairs of complementary atomic actions, to yield more complex types. Think of the following composition of the above two terms:

(cc′f) ( \overline{g}b.(cx.\overline{b}x | \overline{d}f.c′x.\overline{f}x) | px.(\overline{c}x | \overline{c′}x) )  (1.3)

The process of giving a type to this composed term is illustrated in the following.

The picture shows how the term (1.3) is given a type on the right hand side after the procedure of “cut elimination.” Notice how the original activation ordering relations are merged to generate a new relation, so that a proper graph structure arises even if the original types are trees.^{1} In the above example, the existence of two arrows going to b↑x shows that the action should take place after its two parent actions take place. It also shows how the graph-based representation allows a refined expression of the flow of control in comparison with the syntactic construct like prefix, while still keeping a simple combinatorial structure. Compared with sorting and its refinements, the graph type tries to capture dynamic interactive behaviour of name passing processes including the new name passing (as d↑(f) above) based on a simple graphical expression.

This departure from the type abstraction of static usage of names to that of dynamic process behaviour makes it possible to type-abstract many non-trivial computational structures representable in π-calculus. Indeed it allows us to solve Milner’s open issue mentioned above in a sharper form. We show that not only the encoding of sorted polyadic π-terms into the monadic terms is typable preserving the original type structure, but also it results in equational full abstraction: let =_{p} and =_{π} be suitably defined behavioural equalities over sorted polyadic π-terms and monadic πterms, respectively. Then we get:

1We also note that such protocol composition enables the distribution and merging of information in communication, and the increase of parallelism, so can have a practical significance. It also plays a key role in theory of combinators for mobile processes [18, 19, 46].

P =_{p} Q ⇔ [[P]] =_{π} [[Q]]

where [[·]] is the standard encoding from polyadic π-terms to monadic π-terms. In the untyped setting, we can only get “⇐” (adequacy) direction in terms of usual weak behavioural equivalences. This is due to possible violation of “protocols” by environment processes, and relates to the lack of precise type abstraction of the communication structure of various encodings such as (1.1) and (1.2) in preceding type disciplines, even though the effect of process types on behavioural equalities has been studied since the work of Pierce and Sangiorgi [36, 22]. In this context, our result (which seems the first of this kind with respect to the encoding of polyadic name passing) shows how precisely our type discipline captures essential behavioural information these protocols carry. What may be surprising is that this can be done using a simple idea of graph-based types and a small typing system. Moreover the results can be easily extended to encodings of calculi with more complex communication structures, cf. 7.17/7.18 later. We also notice that the polyadic name passing is a typical example of encoding of high-level communication structures into π-calculus, cf. [25, 21, 44], so that the presented construction and its extensions will hopefully become a basis for using typed equality over π-terms to verify semantic equality of various target languages and calculi in a uniform framework.

We now give the structure of the rest of the paper. Section 2 reviews the basic definition of the untyped monadic π-calculus. Section 3 introduces graph types and their composition. Section 4 gives the typing system for monadic π-terms and proves Subject Reduction property of typed terms. Section 5 introduces reduction-based equality over typed π-terms and clarifies the behavioural properties which the types given to π-terms ensure. Section 6 studies basic properties of reduction-based equality. Section 7 then uses the preceding constructions to show that the standard encoding of polyadic π-calculus into monadic π-calculus preserves both type structures and equality of the original world. We also refer to extensions of the result to encodings of more complex structures at the end. Section 8 concludes the paper with comparison with related work and discussions on further works.

2. Preliminaries on Untyped Monadic π-calculus

2.1. Terms. We mainly work with the following syntax [28, 25], where a, b, c, .. or x, y, z, .. range over a countable set N of names (fixed throughout the paper).

P ::= ax.P | \overline{a}x.P | P |Q | (a)P | !P | 0

P, Q, R, … range over the set of terms generated by the above grammar. “\overline{a}v.P ” denotes an agent which sends a value v to a port a and becomes P. “ax.P ” denotes an agent which receives a name and instantiates it in free x’s in P. In ax.P, the name x binds free occurrences of x in P (like x in λx.M). “(a)P ” is a name hiding of a in P. The initial a binds its free occurrences in P. “P |Q” is a parallel composition of P and Q. “!P ” is a replicator which represents the copy of P. “0” is a syntactic convention to denote inaction. The set of free (resp. bound) names in P is denoted by FN (P) (resp. BN (P)). The usual notions of simultaneous substitutions and αconvertibility are assumed. Let us define the set of active names as: a ∈ AN_{+}(P) iff P ≡ (c̃)(\overline{a}v.Q | R) with a ∉ \{c̃\}, and a ∈ AN_{−}(P) iff P ≡ (c̃)(ax.Q | R) with a ∉ {c̃}. Such a occurs actively in P.

A term obeys the binding condition if bound names are disjoint from free names and binding names are pairwise distinct. We often write (ab)P to denote (a)(b)P. \overline{a}(x).P denotes (x)\overline{a}x.P. We let “|” to be the weakest in association, e.g. (a)P | Q =^{def} ((a)P) | Q, and associates to the left. We often cut off the trailing inaction, i.e. \overline{a}v denotes \overline{a}v.0.

Henceforth, terms are often considered modulo the structural congruence, following [25, 3].

2.2. Structure Rule. ≡ is the smallest congruence relation over π-terms generated by the following rules.

(i) P ≡ Q if P ≡_{α} Q (ii) P, Q ≡ Q, P (P, Q), R ≡ P, (Q, R) P, 0 ≡ P !P ≡ P |!P (iii) (aa)P ≡ (a)P (ab)P ≡ (ba)P (a)0 ≡ 0 (a)P, Q ≡ (a)(P, Q) if

a ∉ FN (Q)

The reduction relation which provides the notion of computing is given in the following.

2.3. Reduction. The one-step reduction relation ⟶ over π-terms is generated by the following rule.

(COM) ax.P | \overline{a}v.Q ⟶ P \{v/x\} | Q
(PAR) P ⟶ Q ⇒ P | R ⟶ Q | R.
(RES) P ⟶ Q ⇒ (a)P ⟶ (a)Q.
(STR) P ≡ P′ P′ ⟶ Q′ Q ≡ Q′ ⇒ P ⟶ Q.

The multi-step reduction relation, ⟶, is defined by ⟶ =^{def} ⟶^{∗} ∪ ≡.

We shall also use the standard early labeled transition relation, written P ⟶^{l} P′, as given in e.g. [28].

Several π-terms with significant operational structures are listed in the following. These examples will often be used later.

2.4. Example. (i) (polyadic name passing) Let us assume c and y are fresh.

\begin{matrix}a^{∗}:(x_{1}..x_{n}).P & =^{def} ay.yx_{1}.yx_{2}...yx_{n}.P \\ \overline{a}^{∗}:⟨v_{1}..v_{n}⟩.P & =^{def} \overline{a}(c).\overline{c}v_{1}.\overline{c}v_{2}...\overline{c}v_{n}.P \end{matrix}

Then we have: a^{∗}: (x_{1}x_{2}).P | \overline{a}^{∗}: ⟨v_{1}v_{2}⟩.Q ⟶ P \{v_{1}v_{2}/x_{1}x_{2}\} | Q. Moreover, with =_{π} being the maximum sound equality [20] on π-terms, we have:

a^{∗}:(x_{1}x_{2}).P | \overline{a}^{∗}:⟨v_{1}v_{2}⟩.Q ⟶ =_{π} P \{v_{1}v_{2}/x_{1}x_{2}\} | Q

which shows the mutual communication steps after the initial interaction are deterministic, and do not meet interference from outside since they use private names.

(ii) (mixed input/output structure) The above encoding can be easily extended to mixed input and output. We denote (x̃_{i})[x̃_{i+1}]_{i≤2n} =^{def} (x̃_{1})[x̃_{2}]...(x̃_{2n−1})[x̃_{2n}] where x̃_{i} = x_{i1}...x_{ik_{i}} with k_{i}, n ≥ 0. Similarly for [x̃_{i}](x̃_{i+1})_{i≤2n}. Then define:

\begin{matrix}a^{∗}:(x̃_{i})[ṽ_{i+1}]_{i≤2n}.P & =^{def} & az.zx_{11}..zx_{1k_{1}}.\overline{z}v_{21}..\overline{z}v_{2k_{2}}...\overline{z}v_{2n1}..\overline{z}v_{2nk_{2n}}.P \\ \overline{a}^{∗}:[x̃_{i}](ṽ_{i+1})_{i≤2n}.P & =^{def} & \overline{a}(c).\overline{c}v_{11}..\overline{c}v_{1k_{1}}.cx_{21}..cx_{2k_{2}}...cx_{2n1}..cx_{2nk_{2n}}.P \end{matrix}

with z, c fresh and x_{ij} ≠ x_{kl} and x_{ij} ≠ v_{kl} for all i ≠ k and j ≠ l. Then we have

a^{∗}: (x_{1}x_{2})[v](x_{3}).P | a^{∗}:[w_{1}w_{2}](y)[w_{3}].Q ⟶ P {v/y} | Q{w_{1}w_{2}/x_{1}x_{2}}

as well as the safety property as in (1).

(iii) (parallel name passing and merging) A more complicated but significant structure follows. We use the notation in (i), with \overline{a}^{∗}: (c̃).P standing for (c̃)(\overline{a^{∗}}⟨c̃⟩.P) and ∏i≤n P_{i} for P_{1} | P_{2} | ... | P_{n}. Let us define:

\begin{matrix}a^{∗}:⊗_{n}(x̃_{i}).P & =^{def} & a^{∗}:(w̃).(c̃)(_{∏i≤n} w_{i}^{∗}:(z̃_{i}).\overline{c_{i}}^{∗}:⟨z̃_{i}⟩ | c_{1}^{∗}:(x̃_{1})...c_{n}^{∗}:(x̃_{n}).P) \\ \overline{a^{∗}}:⊗_{n}⟨ṽ_{i}⟩.P & =^{def} & \overline{a}^{∗}: (ẽ).(_{∏i≤n} \overline{e_{i}}^{∗}:⟨ṽ_{i}⟩ | Q) \end{matrix}

where c̃ = c_{1}...c_{n} and ẽ = c_{1}...c_{n} are fresh and distinct and z_{i} and z′_{i} are all fresh with n ≤ 0. Now we have:

a^{∗}:⊗_{n}(x̃_{i}).P | \overline{a^{∗}}:⊗_{n}⟨ṽ_{i}⟩.Q ⟶ P \{ṽ_{1}/x̃_{1}\}..\{ṽ_{n}/x̃_{n}\} | Q

with |x̃_{i}| = |ṽ_{i}|, together with the safety property after the first step as in (i). Here \overline{a^{∗}} : ⊗_{n}⟨ṽ_{i}⟩.Q sends n sequences of data v_{i1}..v_{ik_{i}} in parallel, which are received and instantiated individually by a^{∗}: ⊗_{n}(x̃_{i}).P but part of n sequences are merged to get instantiated in another agent. See the following remark.

2.5. Remark. (parallel name passing) In the third example, there is no order between c_{i} and c_{k} in the above encoding, so that we can safely permute the order of prefixes from c_{i}^{∗}: (x̃_{i})..c_{k}^{∗}: (x̃_{k})..P to c_{k}^{∗}: (x̃_{k})..c_{i}^{∗}: (x̃_{i})..P preserving the semantics, e.g. weak bisimilarity.

3. Graph Types

3.1. Given a finite poset ⟨X, ≤⟩, its covering relation → is defined: x → y iff (1) x ⪇ y and (2) for no z, x ⪇ z ⪇ y where x, y, z ∈ X (cf. [5], Chap.2). Then ⟨X, →⟩ gives an acyclic directed simple graph (equivalent to the familiar Hasse diagram), from which ≤ is recovered as →^{∗} (the reflexive transitive closure) and ⪇ as →^{+} (the transitive closure). In this paper the term “graph” always mean this kind of a directed graph, presented by the covering relation denoted →. Note x →^{∗} y says y is bigger. We write G, G′, … for such graphs, N(G) for the sets of nodes of G, and G_{1} ⊎ G_{2} for the (disjoint) graph union of G_{1} and G_{2}.

3.2. Definition. (graph types) A graph type is a graph in the above sense whose nodes are occurrences of the following atomic types^{2}:

n ::= a↓(b) | a↑(b) | a↓x | a↑x

where a, b, c, … range over N (cf. 2.1) and x, x′, … range over the set V of base types. In a ↕ (b) or a ↕ x, a is the subject and b, x are objects. Over atomic types we define a self-inverse function \overline{(· )} such that: \overline{a ↓(b)} = a ↑(b) and \overline{a↓x} = a ↑x, which is extended to graph types so that \overline{G} (the dual of G) is the result of replacing all occurrences of atomic types in G by their duals. Heads of a graph type are those occurrences of atomic types which are minimal w.r.t. the order →^{∗}. We often use atomic types to denote their occurrences in a graph type, writing, for example, n_{1} → n_{2}, if no confusion arises.

Intuitively, nodes in a graph type denote atomic actions of a process (which are best understood as (abstraction of) labels in transition relation), while edges denote their synchronisation ordering. If a graph type represents a structure of interaction from one party’s viewpoint, then its dual represents the same interaction from another party’s viewpoint.

3.3. Binding. In atomic types, the only bound occurrence of a name is b in a ↕ (b), others occurring free. bn(n) and fn(n) are the sets of a bound/free name in n, respectively. If n occurs in G and bn(n) = {b}, it is a b-binder, and its scope is the set of nodes strictly bigger than n. Then a b-binder binds a free occurrence of b in n′, denoted n ≻≻_{b} n′ or simply n ≻≻ n′, if n′ is in n’s scope but is not in the scope of any b-binder strictly bigger than n.

A graph type is normal if, in any of its bindings, no two binders bind the same name occurrence (see Example below). Hereafter a “graph type” always means a normal graph type. For (normal) graph types, the standard idea of the sets of free/bound names and the α-equality applies, which we denote bn(G), fn(G) and ≡_{α}, respectively.

2Equivalently nodes of a graph type are labeled by atomic types. Graph types are considered modulo the graph isomorphism preserving these labels and direction of edges.

W.l.o.g. we always assume that a graph type obeys the usual binding condition, i.e. no two binding occurrences are of the same name and bn(G) and fn(G) are disjoint.

3.4. Examples. Some simple graph types can be written syntactically, for example, b ↓x → a ↑x′ and b ↑(c) → a ↑x. Further examples are given in Figure 1. Notice the bindings in (2) and (3) of Figure 1 are normal, while that of (1) is not (so (1) is not considered as a graph type). We can also see (2) and (3) α-convertible to each other and both obey the binding condition.

Figure 1. Graph Types

The following two kinds of graph types are important for our theory.

3.5. Definition.

(i) (safety) A graph type G is safe, if, for any n_{1}, n_{2} ∈ N(G), fn(n_{1}) = fn(n_{2}) implies either n_{1} →^{+} n_{2} or n_{2} →^{+} n_{1}.

(ii) (pointedness) A graph type G is pointed, if: (1) There is a unique head in G, whose name is free in G. (2) All name occurrences except the above are bound, and (3) G is safe. We write G_{⟨a⟩} if G is pointed with a free.

In a safe graph type, two nodes with the same subject are strictly ordered so that, while the same subject may be used several times in interaction, at any one time, only one input and one output are active, so that interaction becomes deterministic. In Figure 2, (1) is not safe because there is no ordering between c↑x and c↑(e).

Figure 2. Unsafe and Safe Types

Safe graph types can be shared if they are pointed. The pointedness says that an interaction starts at a single interacting point, and that, after the initial interaction, the communications are always done using private channels, so that they are free from the interference of the third party. An example of a pointed graph type is shown in (2) of Figure 2.

3.6. Proposition.

(i) If G is safe (resp. pointed) then \overline{G} is safe (resp. pointed). (ii) In a pointed graph type G, if n ∈ N(G) is not the head of G, there is a sequence

n_{0} ≻≻ n_{1} ≻≻ .. ≻≻ n_{m} =^{def} n where n_{0} is the head of G and the subject of n_{i+1} is bound by n_{i}.

Proof. Easy by induction on the number of nodes in G.

3.7. Cut Function. We next discuss composition of graph types. Write dom(Ψ) and ran(Ψ) for the domain and the range of a partial function Ψ. Given G and G′, assume n, n_{i} ∈ N(G) and n′, n′_{i} ∈ N(G′). Then a cut function Ψ from G to G′ is a partial injection Ψ : N(G) ⇀ N(G′) such that:

(i) (duality) If n ∈ dom(Ψ), then Φ(n) = \overline{n}. (ii) (acyclicity) n_{1} →^{+} n_{2} and Ψ(n_{2}) →^{+} Ψ(n_{1}) cannot hold simultaneously for any

n_{1}, n_{2} ∈ dom(Ψ). (iii) (covering) (1) if a ∈ fn(G) ∩ fn(G′), then a ∈ fn(n) implies n ∈ dom(Φ) (resp.

a ∈ fn(n′) implies n ∈ ran(Φ)). (2) if there is any binding chain n_{1} ≻≻ n_{2} ≻≻ ⋯ ≻≻ n_{n} in G and n_{i} ∈ dom(Φ) for some i ≤ n, then for all 1 ≤ j ≤ n, n_{j} ∈ dom(Φ), and then Φ(n_{1}) ≻≻ Φ(n_{2}) ≻≻ ⋯ ≻≻ Φ(n_{n}). Similarly for any binding chain in G′ and Φ^{−1}.

Immediately we have:

3.8. Proposition. Suppose G and G′ are safe, then there can be at most one cut function from G to G′.

Proof. For nodes with a common free subject the injection is determined uniquely by safety and acyclicity; then we use the covering to inductively apply the same argument.

We write G_{1} ≍ G_{2} if, for some G′_{1} ≡_{α} G_{1} and G′_{2} ≡_{α} G_{2}, there is a cut function from G′_{1} to G′_{2}. For convenience we assume, when we write G_{1} ≍ G_{2}, they are already suitably α-converted so that the cut function relates their nodes directly. We now introduce two operations on graph types.

3.9. Operations on Graph Types.

(i) (prefix) Given a safe graph type G, “n → G” denotes the result of adding a new node (occurrence) of n to G together with edges from the new node to all heads of G.

(ii) (parallel composition) Given safe graph types G_{1} and G_{2} s.t. G_{1} ≍ G_{2} together with the corresponding cut function Φ, we define the composition of G_{1} and G_{2}, denoted by G_{1}⊙G_{2}, as a graph type obtained by: first identifying Φ-related nodes of G_{1} ⊎ G_{2}, getting a graph, say, G′, and then by eliminating every identified node, preserving and reflecting →^{∗} of G′, deleting all redundant edges if any.

Figure 3. Cut Elimination

Figure 3 shows a simple example of parallel composition. Given two safe graphs in (1) and (2), first we identify the same nodes as in ⟨c ↓x, c ↑x⟩ and ⟨c′ ↓x, c′ ↑x⟩ in (3), next eliminate one by one (the order does not matter). Then we have the final graph (4). In this way the original dependency relations are merged to generate a more complex one.

A few basic properties of the operations follow.

3.10. Proposition.

(i) If G is safe then (1) n_{1} ≻≻_{b} n_{2} in n → G implies either n_{1} ≻≻_{b} n_{2} in G or n_{1} = n and b of n_{2} occurs free in G, and (2) n → G is safe.

(ii) If G_{1}, G_{2} are safe and G_{1} ≍ G_{2}, then (1) for n, n’ ∈ N(G_{1} ⊙G_{2}), we have n ≻≻ n’ in G_{1} ⊙ G_{2} iff n ≻≻ n’ in G_{i} for i = 1 or i = 2, and (2) G_{1} ⊙ G_{2} is again safe. In particular always G_{1} ≍ \overline{G_{1}} and G_{1} ⊙ \overline{G_{1}} is the empty graph.

(iii) Any graph type can be constructed by the operations in 3.9, starting from atomic graph types, i.e. graph types with a unique node.

Proof. (i) and (ii) are easy (notice the item (1) in each case implies that all bindings in the resulting graph are normal). (iii) uses the fact any connected graph type G consists of a head and subgraph G′ together with edges from the head to some nodes of G′, some to heads of G′ and the rest to its non-heads, and argue by induction on the sum of the number of nodes and that of edges. If G with the sum n + 1 has a unique head the result is immediate (use (prefix) in 3.9). If not, we take off a head and extend G′ with additional fresh action types (a) on the top of each connected head and (b) in the middle of an edge going to each connected non-head. The sum becomes n so the induction applies. Now take the disjoint union of the duals of the newly introduced action types and prefix it with the eliminated node. When two new graphs are composed (which is well-defined) we have the original G, as required.

An important property of parallel composition follows. For the second clause, notice (G_{1} ⊙ G_{2}) ⊙ G_{3} ≡_{α} G_{1} ⊙ (G_{2} ⊙ G_{3}) does not always hold.

3.11. Proposition. Suppose G_{i} is safe. Then:

(i) G_{1} ≍ G_{2} implies G_{1} ⊙ G_{2} ≡_{α} G_{2} ⊙ G_{1}. (ii) Suppose fn(G_{1}) ∩ fn(G_{2}) ∩ fn(G_{3}) = ∅. If ((G_{1} ⊙ G_{2}) ⊙ G_{3}) is defined, then

((G_{1} ⊙ G_{2}) ⊙ G_{3}) ≡_{α} (G_{1} ⊙ (G_{2} ⊙ G_{3})).

Proof. (i) is easy. For (ii), we first note: if ((G_{1} ⊙ G_{2}) ⊙ G_{3}) is defined, then G_{1} ≍ G_{2} and (G_{1} ⊙G_{2}) ≍ G_{3}. By assumption, a ∈ fn(G_{1} ⊙G_{2})∩fn(G_{3}) implies either a ∈ fn(G_{1}) or a ∈ fn(G_{2}), hence G_{1} ≍ G_{3} and G_{2} ≍ G_{3}, and then G_{1} ≍ (G_{2} ⊙ G_{3}) by Proposition 3.10 (ii-1). Hence ((G_{1} ⊙ G_{2}) ⊙ G_{3}) ≡_{α} (G_{1} ⊙ (G_{2} ⊙ G_{3})) by Proposition 3.8.

The final proposition is essential to prove the typing system introduced in the next section is closed under the structural rule.

4. The Typing System and Its Basic Properties

4.1. General Idea. This section introduces a typing system based on graph-types for monadic π-terms and establishes its basic syntactic properties, including the subject reduction property. For simplicity of presentation we do not treat recursive types, whose incorporation is straightforward, cf. 8.2. The typing judgment for a π-term P has a form:

Γ ⊢ P ▷_{A}G

where Γ is an environment assigning protocol types (which we introduce below) to some of free names in P, P is a π-term, A is a hidden name set, and G is a graph type. This judgment tells us: “P has a linear behaviour specified in G, and otherwise obeys the protocols specified in Γ.” The separation between linear behaviour and “shared” interaction is essential for tractability of type inference. A is an auxiliary name set to record the linear usage of names, cf.[22]. The sequent is derived roughly in the following three stages:

(1) Starting from a subterm, we construct a graph type G, which should obey a safe condition.

(2) When a term is given as a parallel composition of two subterms, we check whether two corresponding graph types, say G_{1} and G_{2}, are compatible or not, i.e. G_{1} ≍ G_{2} or not, and if so we merge them to get G_{1} ⊙ G_{2}, inducing a more complex structure in general. We record the set of names lost in cut elimination in the hidden name set.

(3) If a subgraph of G is a pointed graph, we may move it from the “linear space” to the “classical space” (shared environments), i.e. from G to Γ. This allows an interaction point to be shared by multiple subterms while ensuring any interaction starting from that point to obey the fixed deterministic protocols. In this way, types which are moved to the non-linear space give generalisation of sorting.

The typing system extracts certain significant behavioural properties of a π-term as its type. The relationship between assigned types and terms behavioural properties will be clarified in the next section. We start from introducing the idea of protocol types, which are essentially pairs of pointed types, and which generalise the notion of sorting.

4.2. Protocol Types. Write “λa.G_{⟨a⟩}” for the name abstraction of a in a pointed graph G_{⟨a⟩}, with the usual notion of binding. (We only need this restricted abstraction in this paper, cf. 6.2). Then a protocol type of λa.G_{⟨a⟩} is the set \{λa.G_{⟨a⟩}, λa.\overline{G}_{⟨a⟩}\}.

Using this notion, we fix the set of types we shall use in our typing system, given any base V′, we get the set of atomic types, from which we get the set of graph types, and then that of protocol types. The corresponding set functions are written ψ_{A}(V′), ψ_{G}(V′) and ψ_{P} (V′), respectively. Then we define, given an initial base V (say {nat}), A_{V}, G_{V} and P_{V} as the smallest sets closed under

P_{V} ⊇ V ∪ ψ_{P} (P_{V}), A_{V} ⊇ ψ_{A}(P_{V}) and G_{V} ⊇ ψ_{G}(P_{V}).

α, β, … range over P_{V}. We shall use these sets for our typing system. We also use the following notations.

• “↕(x) → G” denotes abstraction λa.(a↕(x) → G).

• For α ∈ P_{V}, we write (α) for {λa.a↓α, λa.a↑α}.

A protocol type (similar to a pointed graph (2) in Figure 2) is given in Figure 4.

Figure 4. Protocol Type

4.3. Remark. Note the expression corresponding to the monadic sorting, (α), is the simplest kind of protocol types. The notation is intentional (cf. [24, 14]), since it does function as such. This also shows how we generalise the notion of sorting. As in the sorting, a name can carry another type, admitting the nested structures. However carried information can be a complex protocol, by which we can represent (and guarantee) more refined communication behaviour of mobile processes.

(I) Prefix Rules.

(in_{1}) \frac{Γ ⊢ P ▷_{A}G}{Γ ⊢ ax.P ▷_{A} a↓(x) → G} (1, 2) (out_{1}) \frac{Γ ⊢ P ▷_{A}G}{Γ ⊢ \overline{a}x.P ▷_{A∪\{x\}} a↑(x) → G} (1, 2)
(in_{2}) \frac{x: α, Γ ⊢ P ▷_{A}G}{Γ ⊢ ax.P ▷_{A} a↓α → G} (1)  (out_{2}) \frac{x: α, Γ ⊢ P ▷_{A}G}{x: α, Γ ⊢ \overline{a}x.P ▷_{A} a↑α → G} (1)
(in_{3}) \frac{a: β, Γ ⊢ P ▷_{A}G}{a: β, Γ ⊢ ax.P ▷_{A}} (2, 3)  (out_{3}) \frac{a: β, Γ ⊢ P ▷_{A}\overline{G}}{a: β, Γ ⊢ \overline{a}x.P ▷_{A∪\{x\}}} (2, 3)
(in_{4}) \frac{a: (α), x: α, Γ ⊢ P ▷_{A}}{a: (α), Γ ⊢ ax.P ▷_{A}}  (out_{4}) \frac{a: (α), x: α, Γ ⊢ P ▷_{A}}{a: (α), x: α, Γ ⊢ \overline{a}x.P ▷_{A}}

(II) Other Rules.

(par) \frac{Γ ⊢ P ▷_{A_{1}} G_{1} Γ ⊢ Q ▷_{A_{2}} G_{2}}{Γ ⊢ P | Q ▷_{A_{1}∪A_{2}∪A} G_{1} ⊙ G_{2}} (4) (res)  \frac{Γ ⊢ P ▷_{A} G}{Γ\a ⊢ (a)P ▷_{A\\{a\}} G} (5)
(rep) \frac{Γ ⊢ P}{Γ ⊢!P}  (weak) \frac{Γ ⊢ P ▷_{A} G}{a: α, Γ ⊢ P ▷_{A∪\{b\}} G} (6)
(nil) ⊢ 0  (alpha) \frac{Γ ⊢ P ▷_{A} G G ≡_{α} G′ Γ ≡_{α} Γ′}{Γ′ ⊢ P ▷_{A} G′}

(1) a ∉ fn(Γ)∪A. (2) x ∉ fn(Γ)∪A. (3) β = \{↓(x) → G, ↑(x) → \overline{G}\}. (4) ⟨G_{1}, A_{1}⟩ ≍ ⟨G_{2}, A_{2}⟩, A = fn(G_{1}) ∩ fn(G_{2}). (5) a ∉ fn(G). (6) a ∉ A ∪ fn(G), b ∉ fn(Γ) ∪ fn(G) .

Figure 5. Typing System π_{G}

4.4. Typing Function. A typing function is a function from a finite subset of N to a set of protocol types. The set of typing functions are ranged over by Γ, Δ, . . .. We often regard Γ as a finite set of elements of form: a: α. fn(Γ) denotes {a | a: α ∈ Γ}. Let A, B, C, … denote a finite subset of N. “Γ\A” denotes {a: α ∈ Γ | a ∉ A}, while “Γ⌈A” denotes {a: α ∈ Γ | a ∈ A}. “a: α, Γ” means Γ ∪ {a: α} together with the assumption a ∉ fn(Γ). “Γ ≍ Δ” represents, if x: α ∈ Γ and x: β ∈ Δ, we have α = β. If we get Γ by α-conversion of some protocol graph in Δ, then we write Γ ≡_{α} Δ.

4.5. Sequent and Typing System. The sequent has a form Γ ⊢ P ▷_{A}G, which we read: “P has a type G under Γ with hidden names A”. Γ is called the basis of the sequent, P is its subject, A is the hidden name set, and G is its type. We write Γ ⊢ P ▷ G if A = ∅ (read “P has a type G under Γ”), Γ ⊢ P ▷_{A} if G = ∅, and Γ ⊢ P if both are empty. The typing system, denoted π_{G}, is given in Figure 5, where “⟨G_{1}, A_{1}⟩ ≍ ⟨G_{2}, A_{2}⟩” denotes both G_{1} ≍ G_{2} and (fn(G_{i}) ∪ A_{i}) ∩ A_{j} = ∅ for i ≠ j. We hereafter write Γ ⊢ P ▷_{A} G if the sequent is derivable in π_{G}.

4.6. Comments on Typing Rules (1): Prefix Rules. There are four pairs of (in) and (out) rules, corresponding to the kind of types to be introduced.

(in_{1}, out_{1}): In (in_{1}), “a ↓(x) → G” represents a process gets a new name x and

acts with behaviour G (corresponding to ax.P ⟶^{a(x)} P in the late transition [28]).

Similarly (out_{1}), represents a “bound output” (x)\overline{a}x.P ⟶^{\overline{a}(x)} P. In the latter x is recorded as a hidden name because it should be later restricted by (res) rule.

(in_{2}, out_{2}): Each rule represents that name a gets/emits a name with a protocol

type α, and then acts like G. (in_{3}, out_{3}): These show that if we have successfully construct protocol type β by

finally putting a↕(x) to G, then we may remove the whole of the pointed graph type to the shared environment. In (out_{3}), we again memorize “x” as a hidden name.

(in_{4}, out_{4}): These rules correspond to monadic sorting.

4.7. Remark.

(i) Using (in_{2}) and (out_{2}) instead of (in_{4}) and (out_{4}), we can keep a ↕ (x) → G in the linear realm to construct more complex protocol type. This also shows the usual notion of principal types does not exist in π_{G}.

(ii) By (in_{3,4}) and (out_{3,4}), we make it possible to infer types of a term which contains a shared name at which multiple agents with consistent protocols may interact.

4.8. Comments on Typing Rules (2): Other Rules.

(par): This is the key rule which allows us to extract versatile forms of interaction structures from π-terms. Notice that, even if G_{1} and G_{2} are sequential (i.e. →^{∗} is a total order), we may get a non-sequential graph (but still representing a linear behaviour, see 5.12/5.14). Cuts and their elimination also play the central role in our main results of this paper, Theorems 4.13 and 7.16 (cf. Remark 4.10). Notice also we memorize the set of names lost by cut-elimination: this prevents further connection to these names so that reduction at these points is deterministic.

(res): The combination of this rule and other rules that manipulate the hidden name set such as (out_{1,3}) and (par) enables us to record the linear usage of names during the type inference before the actual occurrence of the scope restriction.

(rep, nil, weak, alpha): These are standard. By (alpha), we hereafter safely consider graph types and basis modulo their respective α-equality.

4.9. Example. Some examples of terms and their graph types follow. Note that all the final graph types in the following are a-pointed, so that we could have moved them using (in_{3}) to the l.h.s. as protocol types.

(i) (polyadic name passing) Define P =^{def} a^{∗}(x_{1}x_{2}).\overline{x_{2}}x_{1}. Then

⊢ P ▷ a↓(z) → z ↓nat → z ↓(x_{2}) → x_{2} ↑nat

as well as

⊢ P ▷ a↓(z) → z ↓nat → z ↓(nat)

(note (nat) =^{def} {↓nat, ↑nat} in 4.2).

(ii) (input/output structure) Assume given P =^{def} a^{∗}(x)[w].w^{∗}[vv]. Then

v: nat, w: β ⊢ P ▷ a:↓(z) → z ↓nat → z ↑β

as well as

v: nat ⊢ P ▷ a↓(z) → z ↓nat → z ↑w → w ↓(x) → x↑nat → x↑nat

where β =^{def} {↓(x) → x ↓nat → x ↓nat, ↑(x) → x ↑nat → x ↑nat}. Note input and output types indeed appear in turn.

(iii) (protocol with parallelism) Let P_{1} =^{def} z_{1}y.cx.\overline{z_{1}}c, P_{2} =^{def} z_{2}x.\overline{c}w and P =^{def} az_{1}.z_{1}z_{2}.(c) (P_{1} | P_{2}). Then we have:

w: nat ⊢ P_{1} ▷ z_{1} ↓nat → c↓nat → z_{1} ↑(nat) and w: nat ⊢ P_{2} ▷ z_{2} ↓nat → c↑nat

Note z_{1} carries two different types. By (par) rule a proper graph structure arises.

w : nat ⊢ (P_{1} | P_{2}) ▷_{{c}} z_{1} ↓nat → z_{1} ↑(nat).
z_{2} ↓nat ↗

After restricting and prefixing, we have the final state.

v : nat, w : nat ⊢ P ▷ a↓(z_{1}) → z_{1} ↓(z_{2}) → z_{1} ↓nat → z_{1} ↑(nat).
↘ z_{2} ↓nat ↗

4.10. Remark. Assume we use (par0) rule below instead of (par) in Figure 5:

(par0) \frac{Γ ⊢ P ▷_{A_{1}} Γ ⊢ Q ▷_{A_{2}}}{Γ ⊢ P | Q ▷_{A_{1}∪A_{2}}} (A_{1} ∩ A_{2} = ∅)

Let us consider following terms

P ≡ \overline{c}v_{1}.\overline{c}v_{2} Q ≡ xy_{1}.xy_{2} \overline{a}(c).P | ax.Q ⟶ (c)(P | Q\{c/x\})

where v_{1} has type nat and v_{2} has a different type (nat). With (par0) rule, (\overline{a}(c).P |ax.Q) is typable, while (c)(P | Q{c/x}) is not typable, even with (weak) rule, which means the subject reduction doesn’t hold. Thus the incorporation of cuts plays a crucial role in the consistency of the present type system. We also note graph structures naturally arise, once some form of cuts is introduced, since without graphs we should artificially restrict the form of composition of types.

One basic result concerning the derivable sequent follows. The second half is notable in that it shows all graph types can be realisable by π-terms.

4.11. Proposition. If Γ ⊢ P ▷_{A} G, then G is safe graph type. Conversely, for any safe graph type G, there is a term P such that, for some Γ, we have Γ ⊢ P ▷ G.

Proof. By Proposition 3.10 (the first half uses the clauses (i)(ii) while the second half uses the third clause).

We list several basic syntactic properties of π_{G}.

4.12. Lemma.

(i) (properties of names) Suppose Γ ⊢ P ▷_{A} G. Then: fn(Γ) ∩ fn(G) = A ∩ fn(G) = A ∩ fn(Γ) = ∅, fn(P) ⊂ fn(G) ∪ A ∪ fn(Γ), fn(G) ⊂ fn(P), and Γ⌈fn(P) ⊢ P ▷_{A∩fn(P)} G.

(ii) (renaming) Suppose Γ ⊢ P ▷_{A}G and b ∉ fn(Γ) ∪ A ∪ fn(G). Then we have

Γ{b/a} ⊢ P {b/a} ▷_{A{b/a}}G{b/a}. (iii) (subterm property) Suppose Γ ⊢ P ▷_{A} G. Then any term occurring as the

subject of some sequent in the proof is a subterm of P and, conversely, any subterm of P occurs as the subject of some sequent in the proof.

(iv) (≡) If Γ ⊢ P ▷_{A} G and P ≡ Q, then Γ ⊢ Q ▷_{A} G.

(v) (combination) Suppose there is the following derivation. Then i = j.

{Γ_{1} ⊢ P ▷_{A_{1}}G′_{1} \atop Γ ⊢ ax.P ▷_{A_{1}}G_{1}} (in_{i}) {Γ ⊢ Q ▷_{A′_{2}}G′_{2} \atop Γ ⊢ \overline{a}v.Q ▷_{A_{2}}G_{2}} (out_{j})

Γ ⊢ ax.P | \overline{a}v.Q ▷_{A_{1}∪A_{2}∪A′} G_{1} ⊙ G_{2} (par)

(vi) (substitution) If a: β, b: β, Γ ⊢ P ▷_{A} G, then b: β, Γ ⊢ P {b/a} ▷_{A} G.

Proof. (i) is easy by checking each rule, staring from (nil). (ii) uses (i), verifying each rule considering in which of Γ, A, G a occurs. (iii) is immediate from the form of each rule. In (iv), we mention three cases. For the closure under αconvertibility we use (ii) above. The commutativity follows from Proposition 3.11 (i). Γ ⊢ (P_{1} | P_{2}) | P_{3} ▷_{A} G ⇔ Γ ⊢ P_{1} | (P_{2} | P_{3}) ▷_{A} G is most non-trivial. But we can easily check if which one of above sequent is derived from Γ_{i} ⊢ P_{i} ▷_{A_{i}}G_{i}, then fn(G_{1}) ∩ fn(G_{2}) ∩ fn(G_{3}) = ∅ (because we record the lost names). Then we can use Proposition 3.11 (ii). (v) is easy by checking the forms of graph type or protocol type in each rule. (vi) is by induction on the structure of P using the above results. Appendix A shows the details of (iv)(v) and (vi).

Notice, by (i,ii) we safely assume binding occurrences in types and a term of Γ ⊢ P ▷_{A}G are all distinct and disjoint from free occurrences.

The main result about the typing system follows, establishing the subject reduction property. It is notable that not only the environment Γ (which corresponds to sorting) but also the graph type of a term is invariant under reduction. This is because all possible reduction concerning the (names of the) graph type is already consumed when (par) rule is applied: and reduction concerning the basis only creates dual graphs which eliminate each other to leave the graph type unchanged.

4.13. Theorem. (Subject Reduction).

If Γ ⊢ P ▷_{A}G and P ⟶ P′, then we have Γ ⊢ P′ ▷_{A}G.

Proof. By induction on the derivation of the one-step reduction. By Lemma 4.12 (iii,iv), we can show that it is enough to prove the following property.

Γ ⊢ ax.P | \overline{a}v.Q ▷_{A} G ⇒ Γ ⊢ P \{v/x\} | Q ▷_{A} G

Without loss of generality, we assume ax.P | \overline{a}v.Q obeys the binding condition. Then we can show its type is derived directly from the following antecedents:

(in_{i}) \frac{Γ_{1} ⊢ P ▷_{A_{1}}G′_{1}}{Γ ⊢ ax.P ▷_{A_{1}}G_{1}} (out_{j}) \frac{Γ ⊢ Q ▷_{A′_{2}}G′_{2}}{Γ ⊢ \overline{a}v.Q ▷_{A_{2}}G_{2}}  (4.1)

The existence of multiple (in)(out) rules seems to make the reasoning complex, but by Combination Lemma (Lemma 4.12 (v)), we know i = j in (4.1). Thus the case analysis becomes simpler and leads to a tractable proof. In the cases of (in_{1,2}) and (out_{1,2}), note G′_{1} and G′_{2} are the results of eliminating unique and mutually dual head nodes from G_{1} and G_{2}, respectively. Since (G_{1} ⊙ G_{2}) ≡_{α} ((G_{1}\n) ⊙ (G_{2}\\overline{n})) we obtain the result. The case of (in_{3}) and (out_{3}) is similar, considering the cut elimination corresponding protocol types. In (in_{4}) and (out_{4}), we use Substitution Lemma (Lemma 4.12 (vi)). The full proof of the theorem is given in Appendix B.

The subject reduction property immediately implies there is no type error if we assume communication of constant values. Also, in such a setting, the set of typable terms is extended non-trivially even under the recursive sorting (with the corresponding extension of protocol types, cf. Section 8), as can be seen from e.g. Example 4.9 (ii).

5. Behavioural Equality over Typed π-terms

This section introduces the basic constructions of typed behavioural equality over monadic π-terms following the untyped construction in [17, 20]. A derived equality is then used to clarify the behavioural properties of a typed term ensured by the assigned type.

5.1. Typed Terms and Typed Relation. A typed term is a tuple ⟨Γ, P, A, G⟩ such that Γ ⊢ P ▷_{A} G. We simply write Γ ⊢ P ▷_{A} G for a typed term ⟨Γ, P, A, G⟩. A relation over typed terms, ranged over R, R′..., is called a typed relation, if:

(a) Γ ⊢ P ▷_{A} G R Δ ⊢ Q ▷_{B} G′ ⇒ A = B, G = G′, and Γ = Δ, and

(b) Γ ⊢ P ▷_{A} G R Γ ⊢ Q ▷_{A} G ⇒ (a: α, Γ ⊢ P ▷_{A∪{b}} G) R (a: α, Γ ⊢ P ▷_{A∪{b}} G) with (6) in Fig.5.

We often write Γ ⊢ P R Q ▷_{A}G for a tuple of a typed relation, or just P R Q if the type assignment is obvious from the context.

Notice ≡ and ⟶ restricted to typed terms are typed relations (by Lemma 4.12 (iv) and Theorem 4.13 respectively). Several important classes of typed relations are:

(i) A typed relation is reflexive if it contains the structural equality over typed πterms. The transitive/symmetric relations are defined in a similar way. If a typed relation is reflexive, transitive and symmetric, then it is an equivalence.

(ii) The relation R is substitution closed if it is closed under the following rules.

(1) Γ ⊢ P R Q ▷_{A}G and b ∉ fn(Γ) ∪ A ∪ fn(G), then Γ{b/a} ⊢ P {b/a} R Q{b/a} ▷_{A{b/a}}G{b/a}.

(2) a: β, b: β, Γ ⊢ P R Q ▷_{A} G, then b: β, Γ ⊢ P {b/a} R Q{b/a} ▷_{A} G.

(iii) A typed relation R is a congruence if R is an equivalence and moreover is closed under the following rule, for each inference rule (and in (par) for each selection of one side of the antecedents) in Figure 5: Γ ⊢ P_{1} R P_{2} ▷_{A} G ⇒ Γ′ ⊢ C[P_{1}] R C[P_{2}] ▷_{A′} G′ if, in an instance of the inference rule, Γ′ ⊢ C[P_{i}] ▷_{A′} G′ is the conclusion with an antecedent Γ ⊢ P_{i} ▷_{A} G, for i = 1, 2 respectively. We write ≅, ≅′, ... for congruence relations.

Hereafter binary relations over typed terms are always considered to be typed, unless otherwise stated.

5.2. Definition. (sound congruence)

(1) A congruence ≅ over typed π-terms is reduction-closed (r.c) iff, whenever Γ ⊢ P ≅ Q ▷_{A} G, P ⟶ P′ implies, for some Q′, Q ⟶ Q′ and Γ ⊢ P′ ≅ Q′ ▷_{A} G.

(2) With θ ranging over + and −, we define a family of action predicates: P ⇓_{a^{θ}} ⇔^{def}

∃P′. P ⟶ P′ ∧ a ∈ AN_{θ}(P′). Then Γ ⊢ P ⇓_{a^{θ}} ▷_{A} G ⇔^{def} (P ⇓_{a^{θ}} ∧ a ∉ A).

A typed relation R respects action predicates iff Γ ⊢ P RQ ▷_{A} G and Γ ⊢ P ⇓_{a^{θ}} ▷_{A} G implies Γ ⊢ Q ⇓_{a^{θ}} ▷_{A} G.

A congruence ≅ is ⇓_{a^{θ}}-sound, or simply sound, if it is reduction closed and respects action predicates.

Note that a sound congruence is automatically non-trivial (i.e. neither universal nor empty). Moreover we can easily verify that the congruence closure of a family of sound congruences is again sound. Then, by taking the congruence closure of the whole family of sound congruences, we immediately know:

5.3. Proposition. There is the maximum sound congruence within the family of all sound congruences. The sound maximum equality is denoted =_{π}.

In the following we use =_{π} as the representative notion of equality over typed π-terms.

5.4. Remark. (semantics based on reduction relation) Semantics based on reduction relation are now used in many studies both in untyped setting [17, 20, 18, 19, 29, 40, 33] and the typed setting [36, 22]. The above definition is based on the semantic framework developed in [17, 18, 19, 12, 46, 20]. There are two notable points. One is the use of reduction closure. A contrasting method is barbed congruence [39]. We notice that if we combine the usual notion of equality in algebra with reduction relation, reduction-closure would be more natural since it guarantees that a process in some congruent class moves to the same congruent class again.

The second point is the choice of action predicates. We discuss this point below.

5.5. Definition. We define two kinds of weaker action predicates over untyped πterms w.r.t [29] and [39], respectively.

P ⇓_{a} ⇔^{def} P ⇓_{a^{+}} or P ⇓_{a^{−}}. and P ⇓ ⇔^{def} ∃a. P ⇓_{a}

We then say Γ ⊢ P ▷_{A} G is insensitive if ¬Γ ⊢ P ⇓ ▷_{A} G (cf. Definition 3.11 and 4.12 in [20]).

5.6. Proposition. Let ≅ be a non-trivial r.c. congruence in which we have: Γ ⊢ P_{i} ▷_{A} G is insensitive (i = 1, 2) ⇒ Γ ⊢ P_{1} ≅ P_{2} ▷_{A} G. Then ≅ is ⇓_{a^{θ}}-sound.

Proof. By the similar reasoning as in Proposition 4.13 of [20], using the type-correct contexts.

The following result shows we can use any of these criteria to get the unique behavioural equality (as far as I know, it has not been proved yet whether the result similar to the following proposition holds or not in weak barbed congruence, cf. p.49 in [39]).

5.7. Proposition. Let us define =_{1} and =_{2} are maximum sound congruences based on ⇓ and ⇓_{a}, respectively. Let =_{3} be any maximal and non-trivial r.c.congruence extending =_{2}. Then =_{3} is uniquely determined and =_{π} = =_{1} = =_{2} = =_{3}.

Proof. Note that =_{π} ⊆ =_{1} ⊆ =_{2} ⊆ =_{3} ⊆ ≅, hence the result by the above proposition.

This may suggest we may use =_{π} as the basic (weak) behavioural equality over typed π-terms. The proposition also implies that we can use any of these predicates which is most convenient to a given situation, in order to check if two terms are equated or not in =_{π} (we however believe that the same full abstraction result can be gained with the barbed congruence).

We next clarify basic behavioural properties types ensure for π-terms. We start from the reduction corresponding to cut elimination.

5.8. Definition. (β-reduction) The one-step β-reduction, →_{β}, is the smallest relation defined by

(β_{1}) Γ ⊢ ax.P | \overline{a}v.Q →_{β} P \{v/x\} | Q ▷_{A} G  (a ∈ A)
(β_{2}) Γ ⊢ (a)(ax.P | \overline{a}v.Q) →_{β} (a)(P \{v/x\} | Q) ▷_{A} G
(Par) Γ ⊢ P →_{β} P′ ▷_{A_{1}} G_{1} ∧ Γ ⊢ Q ▷_{A_{2}} G_{2}
⇒ Γ ⊢ P | Q →_{β} P′ | Q ▷_{A_{1}∪A_{2}∪A} G_{1} ⊙ G_{2}  (4)
(Res) Γ ⊢ P →_{β} P′ ▷_{A} G ⇒ Γ\a ⊢ (a)P →_{β} (a)P′ ▷_{A\{a}} G  (5)
(Str) P ≡ P′ Γ ⊢ P′ →_{β} Q′ ▷_{A} G Q ≡ Q′ ⇒ Γ ⊢ P →_{β} Q ▷_{A} G

where (4) and (5) come from Figure 5. → →_{β} is reflexive transitive closure of →_{β}, while =_{β} is the congruent closure of →_{β}.

We note →_{β}, which is clearly a subset of ⟶, is more general than linear reduction studied in [23, 14, 22] in the sense that it allows the case when one name occurs many times on a process but at any one time only one input/output pair occurs actively (cf. Figure 3) and similar to the one studied in [18]. As in all these “safe” reductions, we have he following non-interference property for →_{β}.

5.9. Proposition. (non-interference) Suppose P → →_{β} Q_{1} and P ⟶ Q_{2}. Then there exists Q′ s.t. Q_{1} ⟶ Q′ and Q_{2} → →_{β} Q′.

Proof. See Appendix C.

A notable fact is =_{β} is behaviourally sound.

5.10. Proposition. =_{β} is a sound congruence, hence P =_{β} Q implies P =_{π} Q. Also =_{β} is substitution closed.

Proof. The reduction closure property is obtained by the non-interference property (Proposition 5.9) as proved in Proposition 3.7 in [18]. For action predicate, we firstly note Γ ⊢ P →_{β} Q ▷_{A} G ⇒ AN_{θ}(P)\A ⊂ AN_{θ}(Q)\A. Then we get the result with the same reasoning as in Proposition 3.7 in [20] and in Proposition 2.3.9 in [12]. The substitution closure property is mechanical by induction on derivation of →_{β} with renaming and substitution lemma in Lemma 4.12 (ii,iv).

We also notice, using the above Proposition:

5.11. Proposition. =_{π} is closed under substitution.

Proof. The condition (1) in 5.1 is obvious. For the condition (2), let a: β, b: β, Γ ⊢ P =_{π} Q ▷_{A} G and c fresh. Then b: β, Γ ⊢ ca.P | \overline{c}b =_{π} ca.Q | \overline{c}b ▷_{A∪\{c\}} G, where both sides β-reduce to P {b/a} and Q{b/a}, hence by =_{β} ⊂ =_{π}, we have the result.

Using →_{β}, which is behaviourally “neutral” by Proposition 5.10, we can clarify how types of typed terms ensure their basic behavioural properties. We first give the case for “linear” behaviour, i.e. the behaviour corresponding to a given graph type. Essentially the following two propositions say that the term does act as its graph type specifies, following the activation ordering in the graph. Hereafter ⟶^{l} denotes the standard early transition relation, cf.[28].

5.12. Proposition. (behaviour of typed terms: (1) linear case) Write Hd(G) for the set of head nodes in G and G\n for the elimination of the head with a label n from G. Then Γ ⊢ P ▷_{A} G implies:

(i) a↓(x) ∈ Hd(G) ⇒ ∀x′. x′ fresh in Γ, A, G.

P → →_{β}⟶^{ax′} P′ and Γ ⊢ P′ ▷_{A} (G\a↓(x)){x′/x}.

(ii) a↑(x) ∈ Hd(G) ⇒

\{ \begin{matrix}P → →_{β}⟶^{\overline{a}(x′)} P′ & and & Γ ⊢ P′ ▷_{A} (G\a↑(x))\{x′/x\} with x′ ∉ A, or : \\ P → →_{β}⟶^{\overline{a}x′} P′ & and & Γ ⊢ P′ ▷_{A\\{x′\}} (G\a↑(x))\{x′/x\} with x′ ∈ A \end{matrix}

(iii) a↓α ∈ Hd(G) ⇒ ∃x. {x: α} ≍ Γ ∧ x ∉ (fn(G) ∪ A) ∧

P → →_{β}⟶^{ax} P′ and {x: α} ∪ Γ ⊢ P′ ▷_{A} G\a↓α.

(iv) a↑α ∈ Hd(G) ⇒ ∃x. x ∉ fn(G) ∪ A ∧

\{ \begin{matrix}P → →_{β}⟶^{\overline{a}x} P′ & and & Γ ⊢ P′ ▷_{A} G\a↑α with x: α ∈ Γ, or : \\ P → →_{β}⟶^{\overline{a}(x)} P′ & and & \{x: α\} ∪ Γ ⊢ P′ ▷_{A} G\a↑α if else \end{matrix}

(v) fn(Hd(G)) = {a_{1}, .., a_{n}} ⇒ P → →_{β} P′ s.t. there is a unique free active occurrence of each a_{i} in P′.

(vi) a ∈ fn(G) ∧ a ∉ fn(Hd(G)) ∪ A ⇒ ¬∃l. P ⟹^{l} with a ∈ fn(l).

Proof. (i–iv) are by induction on P. The most difficult case is the parallel composition. We leave the detailed proof to Appendix D. (v) and (vi) are easy by checking the inference rules in Figure 5.

5.13. Definition. If Γ ⊢ P ▷_{A} G and n ∈ Hd(G), we say “P has a transition P → →_{β}⟶^{l} P′ corresponding to n” if the transition is the one given in (i)..(iv) of Proposition 5.12 according to the form of n.

The following is also notable.

5.14. Corollary. Suppose Γ ⊢ P ▷_{A} G and n_{1}, n_{2} ∈ Hd(G) which are distinct. Suppose also if P → →_{β}⟶^{l_{1}} P_{1} and P → →_{β}⟶^{l_{2}} P_{2} corresponding to n_{1} and n_{2}, respectively. Then there exists Q such that P_{1} → →_{β}⟶^{l_{2}} Q and P_{2} → →_{β}⟶^{l_{1}} Q.

Proof. By the analysis of the case for (par) in the proof of Proposition 5.12.

Next we present how protocol types constrain the behaviour of a typed term. Together with the preceding Propositions 5.12 and 5.9, the following says that a typed term does communicate obeying the specified protocol, up to β-equality.

5.15. Proposition. (behaviour of typed terms: (2) protocol types) Suppose Γ ⊢ P ▷_{A}G and {a: β} ∈ Γ.

(i) Assume β = \{↓(x) → G′, ↑(x) → \overline{G}′\}. Then:

(1) a ∈ AN_{−}(P) ⇒ ∀x′. x′ fresh in Γ, A, G.

P ⟶^{ax′} P′ and Γ ⊢ P′ ▷_{A} (G ⊎ G′{x′/x}).

(2) a ∈ AN_{+}(P) ⇒

\{ \begin{matrix}P ⟶^{\overline{a}(x′)} P′ & and & Γ ⊢ P′ ▷_{A} (G ⊎ \overline{G}′\{x′/x\}) & with x′ ∉ A, or : \\ P ⟶^{\overline{a}x′} P′ & and & Γ ⊢ P′ ▷_{A\\{x′\}} (G ⊎ \overline{G}′\{x′/x\}) & with x′ ∈ A. \end{matrix}

(ii) Assume β = (α). Then:

(1) a ∈ AN_{−}(P) ⇒ ∀b. {b: α} ≍ Γ ∧ b ∉ fn(G) ∪ A ∧

P ⟶^{ab} P′ and {b: α} ∪ Γ ⊢ P′ ▷_{A} G.

(2) a ∈ AN_{+}(P) ⇒ ∃b. b ∉ fn(G) ∪ A ∧

P ⟶^{\overline{a}b} P′ and Γ ⊢ P′ ▷_{A} G with b: α ∈ Γ, or :
P ⟶^{\overline{a}(b)} P′ and \{b: α\} ∪ Γ ⊢ P′ ▷_{A} G if else.

Proof. Easily derived by case analysis on the form of the protocol types and binding condition between Γ and G.

We use Propositions 5.12 and 5.15 for the proof of the main theorem in Section 7.

6. Properties of Reduction-Closed Equalities

In the following, we list basic properties of reduction-closed equalities, introducing a general proof method suggested by [40]. The schemes from Definition 6.1 to Proposition 6.7 can often be adopted to other calculi, see [48] for details. We use the final proposition (Proposition 6.7) for the proof of the main theorem. Those who are not interested in general proof methods may safely skip this section without losing consistency.

First we define several closure operation over typed relations.

6.1. Definition. (closure operation) Let Φ, Φ′,... range over functions between relations on typed π-terms. We write Φ_{p}(R) for the result of closing R under parallel composition and structure rules. Φ_{pr}(R) denotes the result of closing R under under parallel composition, restriction and structure rules. Then we say R is p-closed (resp. pres-closed) if we have Φ_{p}(R) = R (resp. Φ_{pr}(R) = R). Φ_{c}() denotes a congruence closure operation. We also define up-to closure of R under ∼, as: Φ_{∼}(R) =^{def} ∼ R ∼.

First let us note the following fact on substitution closure.

6.2. Proposition. Suppose R is substitution closed. Then Φ_{p}(R), Φ_{pr}(R) and Φ_{c}(R) are substitution closed.

Proof. Mechanical by induction on derivation using Lemma 4.12 (ii) and (vi).

In the weak setting, we introduce the following definitions corresponding to those in [40] without using label transition relation.

6.3. Definition. (r.c.progression, r.c.respectable)

(1) Given two reflexive relations R and S, we say that R r.c.progresses to S, written R ↦ S , if P and Q implies whenever P ⟶ P′, there exists Q′ s.t. Q ⟶ Q′ with P′ S Q′, and the symmetric case.

(2) A function Φ is r.c. respectable if Φ is a closure operator over typed relations, and R ↦ S implies Φ(R) ↦ Φ(S) .

Given a typed relation R, the notions of reduction closed property and respectness ⇓_{a^{θ}} are easily adopted to (any) typed relations in general: R is reduction-closed iff R ↦ R, and we say R respects ⇓_{a^{θ}} if Γ ⊢ P RQ ▷_{A} G and Γ ⊢ P ⇓_{a^{θ}} ▷_{A} G then Γ ⊢ Q ⇓_{a^{θ}} ▷_{A} G, and the symmetric case.

We list the following three technical lemmas, whose detailed proof is given in Appendix E. Lemma 6.4 says r.c.respectable functions are compositional under a mild condition and Lemma 6.5 tells us that we only have to consider p-closed context and closure under substitution, while Lemma 6.6 states that on reduction closed theories, we can easily apply “up to technique” in the weak setting.

6.4. Lemma.

(i) Suppose Φ is r.c.respectable. Then R ↦ Φ(R) implies Φ(R) is reduction closed. (ii) Suppose Φ and Φ′ are r.c.respectable and Φ ∘ Φ′ ⊃ Φ′ ∘ Φ. Then Φ ∘ Φ′ is

r.c.respectable.

6.5. Lemma. Assume R is substitution closed.

(i) Φ_{p}(R) is reduction closed ⇒ Φ_{c}(R) is reduction closed. (ii) Φ_{p}(R) respects ⇓_{a^{θ}} ⇒ Φ_{c}(R) respects ⇓_{a^{θ}}.

6.6. Lemma. (up to reduction-closed congruence) Suppose ≅ is a congruence relation, R is a p-closed relation, and both are substitution and reduction closed. Then:

(i) Φ≅ is r.c.respectable and Φ_{c}(R∪ ≅) is reduction closed. (ii) Φ_{pr}(R) is reduction closed. (iii) R ↦ Φ≅(Φ_{pr}(R)) implies Φ_{c}(R∪ ≅) is reduction and substitution closed.

We use these lemmas to prove:

6.7. Proposition. Suppose =_{s} is sound and substitution closed and R is a substitution and p-closed relation, and moreover satisfies the following properties:

(1) R ↦ Φ_{=_{s}}(Φ_{pr}(R)) .

(2) R respects the action predicate. Then Φ_{c}(=_{s} ∪R) is sound and substitution closed.

Proof. First the substitution closure is given by Lemma 6.6 (iii). Assume Γ ⊢ C_{r}[ ]_{Δ,A_{0},G_{0}} ▷_{A′}G′ (often simply C_{r}[ ]_{Δ,A_{0},G_{0}}) denotes a typed reduction context, i.e. a context whose hole is not under prefix nor replication, with the type of the hole specified. C_{r}, C′_{r}, C′′_{r}... range over reduction context. We firstly note that (1) and (2) are equivalent to the following property by Lemma 6.6 (iii).

(1) whenever Γ ⊢ C_{r}[P]_{Δ,A_{0},G_{0}} R C_{r}[Q]_{Δ,A_{0},G_{0}} ▷_{A} G, C_{r}[P] ⟶ P′ implies, for some Q′, C_{r}[Q] ⟶ Q′, P′ =_{s} C′_{r}[P′_{0}]_{Δ,A_{0},G_{0}}, Δ ⊢ P′_{0} R Q′_{0} ▷_{A_{0}} G_{0}, and C′_{r}[Q′_{0}]_{Δ,A_{0},G_{0}} =_{s} Q′, and its symmetric case.

(2) R respects the action predicate. The reduction closure property is by Lemma 6.6 (iii). For the action predicate, first we prove if R as above respects ⇓_{a^{θ}}, then Φ_{pr}(R) respects ⇓_{a^{θ}}. If these are proved, then we know, if Φ_{pr}(R) respects ⇓_{a^{θ}}, the transitive closure of (=_{s} Φ_{pr}(R) =_{s}) respects ⇓_{a^{θ}}, which means the p-closed relation respects ⇓_{a^{θ}}, hence the result by Lemma 6.5.

7. Fully Abstract Encoding for Polyadic π-calculus

This section establishes the full abstraction result for the standard encoding of polyadic π-calculus into monadic π-calculus in terms of a basic behavioural equality in each setting, as a non-trivial application of our type discipline. We first give a brief review of Polyadic π-calculus and its sorting, including behavioural equality. Then, after introducing the encodings, we make it clear what is the essential problems for such an equational embedding. Then we go into the main technical discussions, establishing the full abstraction result.

As discussed at the end of the section, the result is easily extended to encodings of calculi with more general and complex operational structures realizable in monadic π-calculus. We start from a review of polyadic π-calculus and its sorting.

7.1. Polyadic π-calculus. The syntax of the polyadic π-calculus is given below [26, 39].

P ::= a(x_{1}..x_{n}).P | \overline{a}⟨v_{1}..v_{n}⟩.P | P | Q | (a)P | !P | 0

a(x_{1}..x_{n}).P and \overline{a}⟨v_{1}..v_{n}⟩.P are input and output processes respectively, with n being the arity of the input (output) prefix. The set of sorting S (S_{1}, S_{2}, ...) is given by the following grammar:

S ::= x | (S_{1}S_{2}...S_{n})

with n ≥ 0. (We omit the recursive sorting for simplicity of presentation, whose incorporation does not affect the reasoning and the result in the following, cf. 8.2). Γ, Γ′, … denote typing functions, i.e. functions from a finite subset of N to the above set.

7.2. Reduction and Equality over Sorted Terms. The reduction relation in polyadic π-calculus is given by replacing (COM) rule in 2.3 with the following (COM_{p}) as in the standard way.

(COM_{p}) a(x_{1}..x_{n}).P | \overline{a}⟨v_{1}..v_{n}⟩.Q ⟶ P \{v_{1}v_{2}...v_{n}/x_{1}x_{2}...x_{n}\} | Q

We use the standard typing system and the early labeled transition system for polyadic π-terms as in [43] and [39], respectively, which we list in Appendix F for easy reference. We write Γ ⊢ P in the following, where Γ is a map from a finite set of names to the set of sortings. The following subject reduction property is known concerning the sorted terms, cf. [26, 43].

If Γ ⊢ P and P ⟶ P′, then we have Γ ⊢ P′.

To avoid ambiguity, here and henceforth we often write, Γ_{p}, Δ_{p}, ... for the set of sorting, →_{p} for the reduction relation and ⟶_{p}^{l} for the labeled transition relation. Typed relations and various classes of relations over polyadic π-terms are defined in the same way as in 5.1. Notice the subject reduction property tells us →_{p} is a typed relation in this setting. We define a sound congruence as in Definition 5.2 based on action predicates. Then we have:

7.3. Proposition. There is the maximum sound equality over sorted polyadic πterms which we denote by =_{p} .

By the similar reasoning to Proposition 5.11, =_{p} is substitution closed. We use =_{p} , which can again be characterised in various ways like =_{π}, as the representative notion of behavioural equality over polyadic π-terms from now on.

The following mapping of polyadic π-terms into monadic π-terms is standard, except we present the mapping at the level of types too (which, as we shall see later, plays the central role for our main result).

7.4. Definition. (translation from polyadic to monadic π-calculus, [28, 26]) • Mapping for terms (with c, z fresh).

[[\overline{a}⟨v_{1}..v_{n}⟩.P]] =^{def} \overline{a}^{∗}⟨v_{1}..v_{n}⟩.[[P]]  [[P_{1} | P_{2}]] =^{def} [[P_{1}]] | [[P_{2}]]  [[0]] =^{def} 0
[[a(x_{1}..x_{n}).P]] =^{def} a^{∗}(x_{1}..x_{n}).[[P]]  [[(a)P]] =^{def} (a)[[P]]  [[!P]] =^{def}![[P]]

• Mapping for types (with x fresh).

[[x]] =^{def} x [[(S_{1}...S_{n})]] =^{def} {↓(x) → x↓[[S_{1}]] ⋯ → x↓[[S_{n}]], ↑(x) → x↑[[S_{1}]] ⋯ → x↑[[S_{n}]]}

Notice a sorting is mapped to a protocol type which consists only of consecutive inputs or outputs. The syntactic correspondence follows.

7.5. Lemma.

(i) fn(P) = fn([[P]]), fn(Γ_{p}) = fn([[Γ_{p}]]), AN_{θ}(P) = AN_{θ}([[P]]). (ii) For any substitution σ, [[P σ]] ≡_{α} [[P]]σ and [[Γ_{p}σ]] ≡_{α} [[Γ_{p}]]σ. (iii) P ≡ Q ⇔ [[P]] ≡ [[Q]].

Proof. Easy by induction.

Now we show the first basic result concerning Milner’s open issue [26]: a polyadic π-term has a sort if and only if its mapping in monadic π-term has the corresponding graph (protocol) type.

7.6. Proposition. Γ_{p} ⊢ P ⇔ [[Γ_{p}]] ⊢ [[P]].

Proof. By the structural induction on a polyadic term P. For (⇒) direction, the cases P ≡ 0, P ≡!P′ and P ≡ (a)P′ are trivial. For the case P ≡ a(x_{1}...x_{n}).P′, we first use (in_{2}) rules n times.

[[Γ]] ⊢ zx_{1}....zx_{n}.[[P]] ▷ z ↓[[S_{2}]] → ⋯ → z ↓[[S_{n}]]

Then we apply (weak) rules as several times as we need and (in_{3}) rule once to get the result. The case of P ≡ \overline{a}⟨v_{1}...v_{n}⟩.P′ is just similar. The case of parallel composition is obvious by taking A_{1} = A_{2} = ∅ and G_{1} = G_{2} = ∅ in (par) rule. (⇐) direction is also easily obtained with the same reasoning by translating the protocol type into the sorting.

While the result may seem straightforward, we note that none of the preceding refinements of sorting [36, 35, 14, 22] may give this result, at least with this generality. Notice also that the above result allows us to regard the mapping as the one from explicitly sorted terms to typed monadic terms. Thus we have embedded the sorted terms to the universe of typed monadic π-calculus: our interest is how this embedding is faithful at the semantic (observational) level, i.e. at the level of =_{π} and =_{p} . Before going into technical development, we recall the following fact in the untyped setting.

7.7. Fact. Let =p^{u} and =_{π}^{u} be the maximum sound equalities for untyped polyadic and monadic calculi, defined as in 5.2. Then:

[[P]] =_{π}^{u} [[Q]] ⇒ P =p^{u} Q, but P =p^{u} Q ⇏ [[P]] =_{π}^{u} [[Q]].

Proof. We know the first clause holds as seen in [26]. For the second clause, we present the following counter example.

P ≡ \overline{a}⟨v⟩.\overline{a}⟨v⟩.0 Q ≡ \overline{a}⟨v⟩.0 | \overline{a}⟨v⟩.0  (7.1)

Obviously P =p^{u} Q. The translations are given as:

[[P]] ≡ \overline{a}(c).\overline{c}v.\overline{a}(c).\overline{c}v.0 [[Q]] ≡ \overline{a}(c).\overline{c}v.0 | \overline{a}(c).\overline{c}v.0  (7.2)

Then take the context (a)([ ] | ax.ax.\overline{e}.0) where e is fresh. Then C[[[Q]]] gives an observable at e while [[P]] does not.

The same results hold taking any of weak/strong versions of late/early/barbed bisimilarities and congruences [28, 29, 39], and other kinds of examples also exist. The failure of full abstraction is because the atomicity of the original polyadic name passing is not preserved: one action is decomposed into many finer communication, and intermediate steps can be interfered by another party. In the following, we show that atomicity is semantically preserved for the same encoding, if we use the theory of types we have developed so far. We start from the adequacy result. This is easily proved by the following operational correspondence.

7.8. Proposition. (operational correspondence)

(i) If Γ_{p} ⊢ P →_{p} Q, then [[Γ_{p}]] ⊢ [[P]] ⟶→ →_{β} [[Q]]. (ii) If [[Γ_{p}]] ⊢ [[P]] ⟶ P′, then for some Q, we have [[Γ_{p}]] ⊢ P′ → →_{β} [[Q]] with

Γ_{p} ⊢ P →_{p} Q.

Proof. By structural induction of P. We use, as well as syntactic checking, the subject reduction theorems of both of polyadic π-calculus (Theorem 2.7 in [43]) and monadic one (Theorem 4.13). Suppose P ≡ a(x_{1}x_{2}...x_{n}).Q | \overline{a}⟨v_{1}v_{2}...v_{n}⟩.R and Γ_{p} ⊢ P →_{p} Q{ṽ/x̃} | R. By Proposition 7.6, we have

[[Γ_{p}]] ⊢ az.zx_{1}.zx_{2}...zx_{n}.[[Q]] | \overline{a}(c).\overline{c}x_{1}.\overline{c}x_{2}...\overline{c}x_{n}.[[R]]

By Theorem 4.13, after one step reduction, we get:

[[Γ_{p}]] ⊢ (c)(cx_{1}.cx_{2}...cx_{n}.[[Q]] | \overline{c}x_{1}.\overline{c}x_{2}...\overline{c}x_{n}.[[R]])  (7.3)

In fact, assuming v_{i} : α_{i} ∈ [[Γ_{p}]], this sequent can be derived from the following deductions.

{[[Γ_{p}]] ⊢ cx_{1}.cx_{2}...cx_{n}.[[Q]] ▷ c ↓α_{1} → ⋯ c ↓α_{n} [[Γ_{p}]] ⊢ \overline{c}v_{1}.\overline{c}v_{2}...\overline{c}v_{n}.[[R]] ▷ c ↑α_{1} → ⋯ c ↑α_{n} \atop [[Γ_{p}]] ⊢ (cx_{1}.cx_{2}...cx_{n}.[[Q]] | \overline{c}x_{1}.\overline{c}x_{2}...\overline{c}x_{n}.[[R]]) ▷_{\{c\}}} (par)

[[Γ_{p}]] ⊢ (c)(cx_{1}.cx_{2}...cx_{n}.[[Q]] | \overline{c}v_{1}.\overline{c}v_{2}...\overline{c}v_{n}.[[R]]) (res)

Now we know

[[Γ_{p}]] ⊢ (cx_{1}.cx_{2}...cx_{n}.[[Q]] | \overline{c}x_{1}.\overline{c}x_{2}...\overline{c}x_{n}.[[R]]) ▷_{\{c\}} → →_{β} [[Γ_{p}]] ⊢ [[Q]]\{ṽ/x̃\} | [[R]] ▷_{\{c\}}

Since →_{β} is closed under name restriction by definition, we get the following required result from 7.3.

[[Γ_{p}]] ⊢ (c)(cx_{1}.cx_{2}...cx_{n}.[[Q]] | \overline{c}x_{1}.\overline{c}x_{2}...\overline{c}x_{n}.[[R]]) → →_{β} [[Γ_{p}]] ⊢ [[Q]]\{ṽ/x̃\} | [[R]]

From this Proposition, together with Lemma 7.5 and Proposition 5.10, we obtain the correspondence in terms of the action predicate.

7.9. Proposition. (action predicate) Γ_{p} ⊢ P ⇓_{a^{θ}} ⇔ [[Γ_{p}]] ⊢ [[P]] ⇓_{a^{θ}}.

Proof. Firstly note that by Lemma 7.5 (i), a ∈ AN_{θ}(P) ⇔ a ∈ AN_{θ}([[P]]). (⇒) direction is obvious because Γ ⊢ P →_{p} Q ⇒ [[Γ]] ⊢ [[P]] ⟶ [[Q]] by Proposition 7.8 (i), and this implies Γ ⊢ P ⇓_{a^{θ}} ⇒ [[Γ]] ⊢ [[P]] ⇓_{a^{θ}}. (⇐) direction is also easy because =_{β} is sound equality.

Now we can show that the encoding is equationally “adequate.”

7.10. Theorem. (Adequacy)

[[Γ_{p}]] ⊢ [[P]] =_{π} [[Q]] ⇒ Γ_{p} ⊢ P =_{p} Q.

Proof. We first construct a relation ≅ as follows.

[[Γ_{p}]] ⊢ [[P]] =_{π} [[Q]] ⇒ Γ_{p} ⊢ P ≅ Q

Then we show that ≅ is (a) substitution-closed congruence, (b) reduction-closed, and (c) respects the action predicate ⇓_{a^{θ}}. (a) is obvious by substitution closure of the mapping, congruence of =_{π}, and Lemma 7.5 (iii). For (b), let us assume [[P]] =_{π} [[Q]]. By Proposition 3.2 (ii) in [20], it only has to be proved the one step reduction from P. Then

Γ_{p} ⊢ P →_{p} P′ ⇒ [[Γ_{p}]] ⊢ [[P]] ⟶^{+} [[P′]]  (Prop.5.9, 7.8(i))
⇒ [[Γ_{p}]] ⊢ [[Q]] ⟶ Q′′ ∧ Q′′ =_{π} [[P′]] (reduction closure of =_{π})
⇒ Q′′ → →_{β} [[Q′]] ∧ Q → →_{p} Q′  (Prop 5.10, 7.8(ii))
⇒ [[P′]] =_{π} Q′′ =_{π} [[Q′]]  (soundness of =_{β})
⇒ Γ_{p} ⊢ P′ ≅ Q′.  (transitivity of =_{π})

(c) is obvious because P_{p} ⇓_{a^{θ}} ⇔ [[P_{p}]] ⇓_{a^{θ}} ⇔ [[Q_{p}]] ⇓_{a^{θ}} ⇔ Q_{p} ⇓_{a^{θ}} by Proposition 7.9.

Now we turn to the difficult direction, i.e. completeness. The completeness part crucially relies on two essential roles of the types in the present setting, i.e. as information to control the composition of terms and as a guarantee of terms’ behaviour. We need to establish a few basic behavioural properties of the encoding, using the relationship between types and behaviour studied in Section 5. We start from an easy but useful corollary of Proposition 5.12. Below ↔ is defined as a symmetric irreflexive relation over non-τ labels for the early transition relation generated from \overline{a}c ↔ ac and \overline{a}(c) ↔ ac.

7.11. Lemma. Suppose there is a derivation:

{Γ ⊢ P_{1} ▷_{A_{1}} G_{1} Γ ⊢ P_{2} ▷_{A_{2}} G_{2} \atop Γ ⊢ P_{1} | P_{2} ▷_{A_{1}∪A_{2}∪A} G_{1} ⊙ G_{2}} (par)

Then if n ∈ Hd(G_{1}) and \overline{n} ∈ Hd(G_{2}), for some R we have Γ ⊢ P_{1} | P_{2} → →_{β}

R ▷_{A_{1}∪A_{2}∪A} G_{1} ⊙ G_{2} such that P_{1} → →_{β}⟶^{l_{1}} P′_{1} corresponding to n, P_{2} → →_{β}⟶^{l_{2}} P′_{2}

corresponding to \overline{n}, l_{1} ↔ l_{2}, and (1) BN (l_{1}) ∪ BN (l_{2}) = ∅ then R ≡ P′_{1}|P′_{2}, (2) BN (l_{1}) ∪ BN (l_{2}) = {c} then R ≡ (c)(P′_{1}|P′_{2}).

Proof. Easy syntactic analysis.

The next result shows the effect of the observable action initiating the encoded protocol for a polyadic name passing.

7.12. Proposition. Suppose [[Γ_{0}]] ⊢ [[P]], a: [[(S_{1}..S_{n})]] ∈ [[Γ_{0}]] and [[Γ_{0}]] ⊢ [[P]] ⟶ P′. Then:

(i) If a ∈ AN_{−}(P′), then for all x′. x′ fresh in Γ_{0}, P′ ⟶^{ax′} P′′ and [[Γ_{0}]] ⊢ P′′ ▷ x′ ↓[[S_{1}]] → ⋯ → x′ ↓[[S_{n}]].

(ii) If a ∈ AN_{−}(P′), then for any name c, P′ ⟶^{\overline{a}c} is impossible, and for some P′′ we

have P′ ⟶^{\overline{a}(x′)} P′′ such that [[Γ_{0}]] ⊢ P′ ▷ x′ ↑[[S_{1}]] → ... → x′ ↑[[S_{n}]].

Proof. Obvious by Proposition 5.15 (i-1) and the first clause in (i-2), respectively, considering the form of the mapping of sorting.

For stating further results we need the mappings at the level of labeled transition relation, following the mapping in Definition 7.4.

[[τ]] =^{def} τ
[[a⟨x_{1}...x_{n}⟩]] =^{def} az · zx_{1} ⋯ zx_{n}  (z fresh)
[[(b̃)\overline{a}⟨v_{1}...v_{n}⟩]] =^{def} \overline{a}(c) · (b̃_{1})cv_{1} ⋯ (b̃_{n})cv_{n} (c fresh)

where b̃_{i} =^{def} b̃\v_{1}..v_{i−1} (the result of taking off each v_{1}..v_{i−1} from b̃), and (b̃_{i})cv_{i} =^{def} c(v_{i}) if v_{i} ∈ {b̃_{i}}. Then the decomposition at the level of labeled transition relation becomes:

\begin{matrix}⟶^{[[l]]} & ⇔^{def} & ⟶^{l_{1}}⟶^{l_{2}} ⋯ ⟶^{l_{n}} \\ ⟹^{[[l]]} & ⇔^{def} & ⟶⟶^{l_{1}}⟶⟶^{l_{2}}⟶ ⋯ ⟶⟶^{l_{n}}⟶ \end{matrix}

where [[l]] = l_{1} · l_{2} ⋯ l_{n}. In particular, if all ⟶ is → →_{β} in the second line, we write

⟹_{β}^{[[l]]}.

We notice the following property of the mapped transition.

7.13. Proposition. For l ≠ τ, P ⟶_{p}^{l} P′ ⇔ [[P]] ⟶^{[[l]]} [[P′]].

Proof. Easy syntactic analysis, observing, for ⇐ direction, that the fresh name used for the initial action of the encoding occurs only in the part which encodes the concerned polyadic name passing.

7.14. Remark. While Proposition 7.13 together with Proposition 7.8 gives the strong correspondence between behaviour of the original polyadic terms and their encodings, the analysis of semantic properties of the encodings cannot rely on such correspondence only. This is because we should think of interaction between the encoding and monadic terms which may not be the encodings themselves. The following monadic term makes us understood the reason why we should consider such a situation.

R ≡ (bb_{1}b_{2})(\overline{a}(c).(\overline{b}v | \overline{c}v_{1}.bz.\overline{c}v_{2}) | \overline{e}b_{1}.\overline{f}b_{2})

R is clearly not in the form of the encoding, but R is typable in the way [[a: (x_{1}x_{2})]] ⊢ R ▷e↑(b_{1}) → f ↑(b_{2}), and therefore can be composed to, say, [[a: (x_{1}x_{2})]] ⊢ [[a(x_{1}x_{2}).0]]. This example shows that what we need to establish is:

A sequence of transitions ⟶^{[[l]]} by [[Γ]] ⊢ [[P]] cannot be interfered if the other party is a monadic typed term R which is composable to [[Γ]] ⊢ [[P]].

This is the content of the following key lemma.

7.15. Lemma. (Composition Lemma) First assume Γ_{p} ⊢ P. Next suppose, with Γ_{0} ⊃ [[Γ_{p}]], we have a derivation:

{Γ_{0} ⊢ [[P]] Γ_{0} ⊢ R ▷_{A}G \atop Γ_{0} ⊢ [[P]] | R ▷_{A}G} (par)

Then if [[P]] | R ⟶ P_{0}, one of the following is satisfied.

(1) P_{0} ≡ [[P]] | R′ with R ⟶ R′.

(2) P_{0} → →_{β} [[P′]] | R with P →_{p} P′.

(3) P_{0} → →_{β} (c̃)([[P′]] | R′) with [[P]] ⟶^{[[l]]} [[P′]] and P ⟶_{p}^{l} P′, such that either:

(a) l = a⟨v_{1}v_{2}...v_{n}⟩ and R ⟹_{β}^{[[(c̃)\overline{a}⟨v_{1}v_{2}...v_{n}⟩]]} R′, or

(b) l = (c̃)\overline{a}⟨v_{1}v_{2}...v_{n}⟩ and R ⟹_{β}^{[[a⟨v_{1}v_{2}...v_{n}⟩]]} R′.

Proof. (1) is obvious. (2) is from Proposition 7.8 (ii). Suppose neither (1) nor (2) holds. We note if [[P]] ⟶^{l} P_{1} where a free subject of l is a, then a type mapped from a sorting, say a: [[(S_{1}..S_{n})]] should be in Γ_{0}. This implies that there is no free output from R or [[P]] by Proposition 7.12, so there are two cases for (3): by Lemma 7.11, P ⟶^{l} P_{1} and P_{0} ≡ (c)(P_{1} |R′′) where, with c ∉ fn(G)∪A and a: \{↓(c′) → G′, ↑(c′) → \overline{G}′\} ∈ Γ_{0},

(a) [[P]] ⟶^{ac} P_{1} with Γ ⊢ P_{1} ▷G′\{c/c′\}, and R ⟶^{\overline{a}(c)} R′′ with Γ ⊢ R′′ ▷_{A}\overline{G}′\{c/c′\} ⊎ G.

(b) [[P]] ⟶^{\overline{a}(c)} P_{1} with Γ ⊢ P_{1} ▷\overline{G}′\{c/c′\}, and R ⟶^{ac} R′′ with Γ ⊢ R′′ ▷_{A}G′\{c/c′\} ⊎ G.

For (a), by Proposition 7.12 (ii), we have

Γ_{0} ⊢ P_{1} ▷ c↓[[S_{1}]] → ... → c↓[[S_{n}]] and Γ_{0} ⊢ R′′ ▷ c↑[[S_{1}]] → ... → c↑[[S_{n}]] ⊎ G

By repeatedly applying Lemma 7.11, we get the behaviour of R and P_{1} (hence [[P]]). The latter is then translated back to the corresponding single transition of P by Proposition 7.13. The next case (b) is similar starting from Proposition 7.12 (i).

Now we are ready to prove the main theorem of this paper.

7.16. Theorem. (Main Theorem, Full Abstraction)

Γ_{p} ⊢ P =_{p} Q ⇔ [[Γ_{p}]] ⊢ [[P]] =_{π} [[Q]].

Proof. By Theorem 7.10, we have only to prove (⇒) direction. Let us first construct the relation ≅^{−} as the smallest typed relation including the following base equations and closed under parallel composition.

[[Γ_{p}]] ⊢ [[P]] ≅^{−} [[Q]] if Γ_{p} ⊢ P =_{p} Q

Clearly ≅^{−} is neither congruent nor reduction-closed. However if ≅^{−} satisfies the following Claim, by Proposition 6.7, taking =_{s} = =_{β} the congruence relation which is generated by ≅^{−} is sound, which leads to the required result. Note: Γ_{0} ⊢ P_{1} ≅^{−} Q_{2} ▷_{A}G implies P_{1} ≡ [[P]] | R and Q_{1} ≡ [[Q]] | R with Γ_{p} ⊢ P =_{p} Q and [[Γ_{p}]] ⊂ Γ_{0}, by induction of the derivations of ≅^{−} (hereafter we often write such a situation just [[Γ_{p}]] ⊂ Γ_{0} ⊢ [[P]]|R ≅^{−} [[Q]]|R ▷_{A}G, understanding conditions on terms and types as just noted).

Claim:

(i) ≅^{−} is substitution closed. (ii) whenever Γ_{p} ⊢ [[P]] | R ≅^{−} [[Q]] | R ▷_{A} G, P ⟶ P_{0} implies, for some Q_{0},

Q ⟶ Q_{0}, P_{0} =_{β} C_{r}[[[P′]]]_{[[Γp]]}, Γ_{p} ⊢ P′ =_{p} Q′ and C_{r}[[[Q′]]]_{[[Γp]]} =_{β} Q_{0}, and the symmetric case.

(iii) ≅^{−} respects the action predicate.

(i) is easy by ≅^{−} ⊃ → →_{β} and reasoning similarly as in Proposition 5.11.

Now we show ≅^{−} satisfies the other two conditions in the above Claim. For reduction closure, it is enough to prove the case when P_{1} ≡ [[P]]|R reduces by one step. Assume:

Γ_{0} ⊢ [[P]] | R ⟶ P_{0} ▷_{A} G

Then there are three cases by Lemma 7.15.

(1) P_{0} ≡ [[P]] | R′ with R ⟶ R′.

(2) P_{0} → →_{β} [[P′]] | R with P →_{p} P′.

(3) P_{0} → →_{β} (b̃)([[P′]] | R′) with [[P]] ⟶^{[[l]]} [[P′]] and P ⟶_{p}^{l} P′, such that either:

(a) l = a⟨v_{1}v_{2}...v_{n}⟩ and R ⟹_{β}^{[[(b̃)\overline{a}⟨v_{1}v_{2}...v_{n}⟩]]} R′, or

(b) l = (b̃)\overline{a}⟨v_{1}v_{2}...v_{n}⟩ and R ⟹_{β}^{[[a⟨v_{1}v_{2}...v_{n}⟩]]} R′.

Case (1): Straightforward by taking ([[Q]] | R) ⟶ ([[Q]] | R′).

Case (2): Γ_{p} ⊢ P →_{p} P′

⇒ ∃ Q′. Γ_{p} ⊢ Q → →_{p} Q′ ∧ Γ_{p} ⊢ P′ =_{p} Q′ (soundness of =_{p} )
⇒ Γ_{0} ⊢ [[Q]] | R ⟶ [[Q′]] | R  (Prop.7.8(i))
⇒ P_{0} → →_{β} C_{r}[[[P′]]] ∧ Q_{0} ≡ C_{r}[[[Q′]]]  with C_{r}[·] =^{def} [·] | R

For case (3-a), the following property of =_{p} is used: it says that the input observability is derived from sound theories (cf. Propositions 4.13 in [20]).

Claim (A): Suppose Γ^{0} ⊢ P =_{p} Q. Then, with some Γ ⊃ Γ^{0},

Γ ⊢ P ⟶_{p}^{a⟨v_{1}v_{2}...v_{n}⟩} P′ ⇒ Γ ⊢ Q ⟹_{p}^{a⟨v_{1}v_{2}...v_{n}⟩} Q′ for some Q′ with Γ ⊢ P′ =_{p} Q′. (7.4)

Proof of Claim (A): Let us take the context C[·] =^{def} [·] | \overline{a}⟨v_{1}..v_{n}⟩.f | \overline{f} with f fresh. First Γ ⊢ C[P] ⟶^{2} P′ and ¬P′ ⇓_{f^{θ}}. Thus by definition of sound congruence, Γ ⊢ C[Q] ⟶ Q′′ and Q′′ =_{p} P′ with ¬Q′′ ⇓_{f^{θ}}. But if ¬Q′′ ⇓_{f^{θ}}, there should be a

transition from Q such that Γ ⊢ Q ⟶ ⟶_{p}^{a⟨v_{1}v_{2}...v_{n}⟩}⟶ Q′. The closure property is proved with the same reasoning found in Theorem 3.19 in [20] using the incompatible pairs \overline{f} // = 0 and (f | \overline{f}) // = 0. (end of the proof of Claim (A)).

With this claim the input case is easily obtained as follows.

Case (3-a): l = a⟨v_{1}v_{2}...v_{n}⟩.

Γ_{p} ⊢ P ⟶_{p}^{a⟨v_{1}v_{2}...v_{n}⟩} P′ ∧ R ⟹_{β}^{[[(b̃)\overline{a}⟨v_{1}v_{2}...v_{n}⟩]]} R′

⇒ ∃ Q′.Γ_{p} ⊢ Q ⟹_{p}^{a⟨v_{1}v_{2}...v_{n}⟩} Q′ ∧ Γ_{p} ⊢ P′ =_{p} Q′ (Claim (A))
⇒ Γ_{0} ⊢ [[Q]] | R ⟶ (b̃)([[Q′]] | R′)  (Prop.7.8(i) and Lem.7.15(3-a))
⇒ P_{0} → →_{β} C_{r}[[[P′]]]_{[[Γp]]} ∧ Q_{0} ≡ C_{r}[[[Q′]]]_{[[Γp]]}  with C_{r}[·] =^{def} (b̃)([·] | R′)

The final output case is the most non-trivial since we can not observe the value of the output label (cf. [20]). We also note that we will be often using late transition below and for the next claim, which is defined in the standard way, see e.g. [28].

Case (3-b): l = (b̃)\overline{a}⟨v_{1}v_{2}...v_{n}⟩.

Let C[ ] =^{def} [ ] | a(x_{1}...x_{n}).(\overline{c}⟨x_{1}...x_{n}⟩ | \overline{f}) | f with f, c fresh. W.l.o.g we can assume Γ_{p} ⊢ C[P]_{Γp} =_{p} C[Q]_{Γp}. Then we have:

Γ_{p} ⊢ P ⟶_{p}^{(b̃)\overline{a}⟨v_{1}v_{2}...v_{n}⟩} P′

⇒ Γ_{p} ⊢ C[P]_{Γp} ⟶^{2} (b̃)(P′ | \overline{c}⟨v_{1}v_{2}...v_{n}⟩) =^{def} P′′  (7.5)
⇒ Γ_{p} ⊢ C[Q]_{Γp} ⟶ (b̃′)(Q′ | \overline{c}⟨v′_{1}v′_{2}...v′_{n}⟩) =^{def} Q′′ =_{p} P′′  (7.6)

with Γ_{p} ⊢ Q ⟹_{p}^{(b̃′)\overline{a}⟨v′_{1}v′_{2}...v′_{n}⟩} Q′ because ¬Q′′ ⇓_{f^{θ}} and Q′′ ⇓_{c^{−}}. Then from (7.5) we have:

Γ_{0} ⊢ [[P]] | R ⟶ P_{0} → →_{β} (b̃)([[P′]] | R′′{ṽ/x̃}) ▷_{A} G for some R ⟹_{β}^{[[a⟨v_{1}...v_{n}⟩]]} R′′{ṽ/x̃}

by again Lemma 7.15 (3-b) where R ⟹_{β}^{[[a(x_{1}...x_{n})]]} R′′ in the late transition relation [28].

Suppose v_{i} : α_{i} ∈ Γ_{p}. Then there exists a transition R ⟶^{[[a⟨v′_{1}...v′_{n}⟩]]} R′′{ṽ′/x̃} with v′_{i}: α_{i} ∈ Γ_{p}. Thus from (7.6), we have

Γ_{0} ⊢ [[Q]] | R ⟶ (b̃′)([[Q′]] | R′′{ṽ′/x̃}) ▷_{A} G with R ⟹_{β}^{[[a⟨v′_{1}...v′_{n}⟩]]} R′′{ṽ′/x̃}

by Lemma 7.15 (3-b) and Proposition 7.8 (i). Then, by noticing c occurs as only one positive and one negative active name, we have the following sequence of relations:

\begin{aligned}[[P]] | R & ⟶ & P_{0} & → →_{β} & (b̃)([[P′]] | R′′\{ṽ/x̃\}) & _{β} ← ← & (c)([[P′′]] | c^{∗}(x_{1}x_{2}...x_{n}).R′′) \\ [[Q]] | R & ⟶ & Q_{0} & ≡ & (b̃′)([[Q′]] | R′′\{ṽ′/x̃\}) & _{β} ← ← & (c)([[Q′′]] | c^{∗}(x_{1}x_{2}...x_{n}).R′′) \end{aligned}

Taking C_{r}[·]_{[[Γp]]} =^{def} (c)([·] | c^{∗}(x_{1}x_{2}...x_{n}).R′′), we are done with [[Γ_{p}]] ⊢ [[P′′]] ≅^{−} [[Q′′]] by Γ_{p} ⊢ P′′ =_{p} Q′′ in (7.6).

For the action predicate, assume

[[Γ_{p}]] ⊂ Γ_{0} ⊢ ([[P]]|R) ≅^{−} ([[Q]]|R) ▷_{A}G  (7.7)

with Γ_{p} ⊢ P =_{p} Q. Notice, if Γ_{0} ⊢ ([[P]]|R) ▷_{A}G ⇓_{a^{θ}} with a ∈ fn(G) \ A, then by Proposition 5.12 we immediately know Γ_{0} ⊢ ([[Q]]|R) ▷_{A}G ⇓_{a^{θ}}. Hence we are only concerned at the observable at Γ_{0}. For the purpose, we establish the following claim.

Claim (B): Assume (7.7). There is a well-sorted polyadic term Γ_{p} ⊂ Γ′_{0} ⊢ R_{0} with fn(Γ′_{0}) = fn(Γ) such that, for any Γ_{p} ⊢ P′, we have:

(i) If Γ_{0} ⊢ ([[P′]]|R) ⇓_{a^{θ}}^{m} ▷_{A}G ∧ a ∈ fn(Γ_{0}) then Γ′_{0} ⊢ P′|R_{0} ⇓_{a^{θ}} where ⇓_{a^{θ}}^{m} means, after m reduction steps, one reaches an immediate observable a with polarity θ.

(ii) If Γ′_{0} ⊢ P′|R_{0} ⇓_{a^{θ}} then Γ_{0} ⊢ P′|R_{0} ⇓_{a^{θ}}. Proof of Claim (B): We construct such R_{0} indexed by some n, called an n-simulator, which simulates R in the above way up to the n transition sequences R may be engaged in, by the following procedure. We use a sequence of prefixes, like a(x_{1}..x_{n})(v_{i}v_{j})\overline{b}⟨v_{1}..v_{n}⟩ (v_{i}v_{j} shows the bound output), ranged over s, s_{1}, . . .. Each prefix itself is written p, p′, . . .. The null sequence is denoted ε. Notice s.0 gives a polyadic π-term.

(1) Unfold R_{0}’s replications n-times, and let the term obey the binding condition. By this note any τ-transition from R_{0} does not need α-conversion until n-steps.

(2) We use three sets, Ξ_{0}, Ξ_{1}, Ξ_{2}. An element of the first one is essentially a tuple of prefix sequence together with an intermediate term which arises as a result of the transitions corresponding to the prefix sequence. An element of the second one is a triple of a prefix sequence, an intermediate term, and a name z which is being used by R for communication via a name with a type of encoded sorting. The third contains completed prefix sequences.

(3) We initially set Ξ_{0} = {⟨ε, Γ_{0} ⊢ R ▷_{A}G⟩}, and Ξ_{1} = Ξ_{2} = ∅. This is the state for n = 0.

(4) Let n = m and Ξ_{0}, Ξ_{1}, Ξ_{2} are given. We use auxiliary sets Ξ′_{0}, Ξ′_{1}, Ξ′_{2} which are initially given by: Ξ′_{0} = Ξ′_{1} = ∅ and Ξ′_{2} = Ξ_{2}.

(5) For each ⟨s, Γ′ ⊢ R′ ▷_{A′}G′⟩ ∈ Ξ_{0}, we do the following.

(1) For each free active occurrence of a in R′ where a ∈ fn(Γ′) and which, in addition, has the type of encoded sorting, we first let R′ make a late transition corresponding to that active occurrence, say R′ ⟶_{l}^{l} R′′, with Γ′ ⊢ R′′ ▷_{A′}G′′ (note G′′ is the graph union of G′ and the tail of the graph type for the sorting). Now we get the continuation for polyadic name passing (z in ↕ (z) → G), and track the binding structure (for input) or the vector of output names (for output) analysing the term structure of R′′ (which is possible since cuts are always finite), thus obtaining the corresponding polyadic prefix, say p, and then let ⟨s · p, z, Γ′ ⊢ R′′ ▷_{A′}G′⟩ be added to Ξ′_{1}.

(2) For each free active occurrence of a in R′ such that a ∈ fn(Γ_{0}) (note we go back to Γ_{0} here) and which does not have the type of encoded sorting, if it is input we add s · a(ε) into Ξ′_{2}, if it is output we add s · \overline{a}⟨ε⟩ into Ξ′_{2}.

(3) For each redex in R′, let Γ′ ⊢ R′ ⟶ R′′ ▷_{A′}G′ be the corresponding reduction, then we put the new term into Ξ′_{0}. If neither of (1)(2)(3) is possible, then we put s into Ξ′_{2}.

(6) For each ⟨s, z, Γ′ ⊢ R′ ▷_{A′}G′⟩ ∈ Ξ_{1}, we do the following. (1) If there is a free active z in R′, then there is a corresponding late transition, say R′ ⟶_{l}^{l} R′′, and correspondingly a new name with type of the encoded sorting may be added to Γ′, resulting in Γ′′ (if not Γ′′ = Γ′), while one head of G′ will be gone, resulting in G′′. If z still occurs in R′ (showing it has not finished that part of interaction) then ⟨s, z, Γ′′ ⊢ R′′ ▷_{A′}G′′⟩ is added to Ξ′_{1}. If z does not occur, then ⟨s, Γ′′ ⊢ R′′ ▷_{A′}G′′⟩ is added to Ξ′_{0}.

(2) If there is no free active z in R′, there should be some β-reduction. For each β-reduction Γ′ ⊢ R′ ⟶ R′′ ▷_{A′}G′, we put ⟨s, z, Γ′ ⊢ R′′ ▷_{A′}G′⟩ to Ξ′_{1}.

(7) Finally we set Ξ_{i} = Ξ′_{i} for i = 0, 1, 2 and n becomes n + 1.

Now let Ξ_{0}, Ξ_{1}, Ξ_{2} are the above sets with n = m + 1. Then an m-simulator is given by extracting all prefix sequences from elements of these sets, and postfix 0 to each to get polyadic terms (say P_{0}, ..P_{k}), and define:

R_{0} =^{def} ⨁_{0≤i≤k} P_{k}

where the right hand side is given by (c)(∏_{i≤k} c(ε).P_{k} | \overline{c}⟨ε⟩) with c fresh. We then sort the term as:

Γ′_{0} ⊢ R_{0}

where fn(Γ′_{0}) = fn(Γ_{0}) and (1) for a such that Γ_{0}(a) is the encoding of sorting, we have Γ′_{0}(a) = Γ_{0}(a), while (2) for a such that Γ_{0}(a) is not the encoding of sorting, then Γ′_{0}(a) = (ε). This is clearly well-sorted. Now using Lemma 7.15 repeatedly, we can check, by induction on the construction of R_{0}, at least up to m-steps of (monadic) transitions of R, [[R_{0}]] can simulate all transitions of R as far as the interaction with [[P_{0}]] and observability at Γ_{0} go. But this means [[P]]|R has more than m steps of monadic transitions, hence we have the clause (i) of Claim (B). Moreover clearly the transition traces of [[R_{0}]] is smaller than R (by induction on n we can verify, for each visible transition of [[R_{0}]], there is the corresponding transition of R). This gives the clause (ii) of Claim (B). (end of the proof of Claim (B)).

We now prove that ≅^{−} respects the action predicates. Suppose Γ_{0} ⊢ [[P]]|R ⇓_{a^{θ}} ▷_{A}G with a ∈ Γ_{0}, taking n reduction steps to reach the immediate observable. Take the n′-simulator of Γ′_{0} ⊢ R with any n′ ⪈ n (actually n′ = n suffices). Then by the clause (i) of Claim (B) we know Γ′_{0} ⊢ P′|R_{0} ⇓_{a^{θ}}. But because Γ′_{0} ⊢ P′ =_{p} Q′, we know Γ′_{0} ⊢ Q′|R_{0} ⇓_{a^{θ}}. By Proposition 7.8 (iii) this implies [[Γ′_{0}]] ⊢ [[Q′]]|[[R_{0}]] ⇓_{a^{θ}}. Hence by the clause (ii) of Claim (B) we know Γ_{0} ⊢ [[Q′]]|R ⇓_{a^{θ}}. This shows that two conditions of Lemma 6.7 are satisfied by ≅^{−}, hence it is in =_{π}, concluding the proof.

Now we will briefly touch upon some extensions. Our type framework is general enough to apply to more complex operational structures, cf. Example 2.4 (ii) and (iii).

7.17. Mixed Input/Output Interaction. The abstract syntax of the calculus (which is a subset of [11]) is given by replacing input and output agents with the following terms (for notation, see 2.4 (ii)):

a:(x̃_{i})[ṽ_{i+1}]_{i≤2n}.P \overline{a}:[x̃_{i}](ṽ_{i+1})_{i≤2n}.P

where x̃_{i} = x_{i1}...x_{ik_{i}} with k_{i}, n ≥ 0 and we assume all binding names are pairwise distinct and disjoint from free names. In IO interaction types, ↓S (resp. ↑S) represents a type which receives (resp. emits) S, while ↕ S; ↕ S′ denotes the sequential composition of ↕ S and ↕ S′. We use abbreviation ↓S̃_{i} =^{def}↓S_{i1}; ...; ↓S_{ik_{i}} and similarly for ↑S̃_{i} with k_{i} ≥ 0, where we set ∅; ↕ S =↕ S; ∅ =↕ S. Then the set of IO interaction types I (S, S′, …), is given by following grammar:

S ::= x | {↓S̃_{1}; ↑S̃_{2}; ...; ↓S̃_{2n−1}; ↑S̃_{2n} , ↑S̃_{1}; ↓S̃_{2}; ...; ↑S̃_{2n−1}; ↓S̃_{2n}}

with n ≤ 0. Note the sorting is the special mixed interaction type such that: {↓ S̃_{1}, ↑S̃_{1}}. The reduction relation is given by replacing (COM) rule in 2.3 with the following rule, where we assume the whole term obeys the binding condition.

\begin{matrix}a:(x̃_{i})[ṽ_{i+1}]_{i≤2n}.P | \overline{a}:[w̃_{i}](ỹ_{i+1})_{i≤2n}.Q \\ ⟶ (P | Q)\{ṽ_{2n}/ỹ_{2n}\}\{w̃_{2n−1}/x̃_{2n−1}\}...\{ṽ_{2}/ỹ_{2}\}\{w̃_{1}/x̃_{1}\} \end{matrix}

with |w̃_{i}| = |x̃_{i}| and |ṽ_{i}| = |ỹ_{i}|. Note the sequence of substitution is reversed to represent receiving and sending the same name at one time, e.g. a: (x_{1})[x_{1}].P. The typing system and labeled transition relation are easily defined by “mixing” input/output rules (cf. 4.2 in [11]). This system also has the subject reduction property (cf. Theorem 4.3 in [11]). We use the encoding in 2.4 (ii) for the mapping of terms. Based on this, the mapping of type [[ ]]_{i} is given as:

{↓(x) → x↓[[S̃_{1}]]_{i} → x↑[[S̃_{2}]]_{i} ⋯ → x↑[[S̃_{2n}]]_{i}, ↑(x) → x↑[[S̃_{1}]]_{i} → x↓[[S̃_{2}]]_{i} ⋯ → x↓[[S̃_{2n}]]_{i}}

where x ↕ [[S̃_{i}]]_{i} =^{def} x ↕ [[S_{i1}]]_{i} → x ↕ [[S_{i2}]]_{i} ⋯ → x ↕ [[S_{ik_{i}}]]_{i}. Now defining =_{i} as the maximum sound congruence (cf. Definition 5.2), we have:

Γ_{i} ⊢ P =_{i} Q ⇔ [[Γ_{i}]]_{i} ⊢ [[P]]_{i} =_{π} [[Q]]_{i}.

By the same operational correspondence as Proposition 7.8, ⇒ is immediately obtained. For the ⇐ direction, by Proposition 6.7, we prove the same claim together with Lemma 7.15 using the label and its mappings. But by Proposition 5.15, we only have to replace one-way name passing with IO interaction in order to obtain the same previous propositions and lemmas: e.g. in Proposition 7.12, we replace x′ ↓[[S_{1}]] ⋯ → x′ ↓[[S_{n−1}]] → x′ ↓[[S_{n}]] with

Γ_{0} ⊢ P′′ ▷ x′ ↓[[S̃_{1}]]_{i} → x′ ↑[[S̃_{2}]]_{i} ⋯ → x′ ↓[[S̃_{2n−1}]]_{i} → x′ ↑[[S̃_{2n}]]_{i}

7.18. Parallel Name Passing. Now we show graph types make it possible to typeabstract the following non-sequential protocols. The abstract syntax of the calculus is given by replacing input and output agents with the following terms (for notation, see 2.4 (iii)):

a:⊗_{n}(x̃_{i}).P \overline{a}:⊗_{n}⟨x̃_{i}⟩.P

with n ≥ 0 and we assume all binding names are pairwise distinct and disjoint from free names. Then the set of parallel types P (S, S′, …) is simply given as S ::= x | ⊗_{n}S̃_{i} with n ≤ 0. The sorting is the case n = 1. The reduction relation is given as:

(COM_{⊗}) a:⊗_{n}(x̃_{i}).P | \overline{a}:⊗_{n}⟨ṽ_{i}⟩.Q ⟶ P σ̃ | Q

where σ̃ is a sequence of substitutions σ_{i} = {ṽ_{i}/x̃_{i}} with |x̃_{i}| = |ṽ_{i}| and 1 ≤ i ≤ m (actually the ordering does not matter). Then the typing system/labeled transition relation are defined just by replacing a: S̃ with a: ⊗_{n}S̃. We use Example 2.4 (iii) for the mapping of terms. Now we translate its types [[⊗_{n} S̃_{i}]]_{⊗} to “graph” types \{λa.G, λa.\overline{G}\} where

G =^{def} a↓(c) → c↓ ˜(c_{i}) → c_{1} ↓[[S_{11}]]_{⊗} ⋯ → c_{1} ↓[[S_{1k_{i}}]]_{⊗}
↘  :
c_{n} ↓[[S′_{n1}]]_{⊗} ⋯ → c_{n} ↓[[S′_{nk_{n}}]]_{⊗}

with c̃ =^{def} c_{1}...c_{n} fresh and distinct. Note the above mapping to graph types shows that it does not matter to change the order of prefixes of c_{i} and c_{j} in the mapping a:⊗_{n}(x̃_{i}).P, as mentioned in Remark 2.5. The difference from the previous encodings of calculi with sequential types is n-redex pairs appear at once during β-reduction between [[P]]_{⊗} and another typed agent (i.e. R in Lemma 7.15). By defining the mapping [[l]] by a function from a label l to a set of sequences of labels {l̃_{1}, l̃_{2}, .., l̃_{m}} in which we preserve the ordering between the same subject names, we can use the same proof technique developed in this section because the basic properties studied in Section 5 (Prop.5.12,5.15 and Col.5.14) do not depend on sequential graph types. Finally we can establish the full abstraction result.

We can combine the mixed IO interaction and parallel (multi) name passing, and show the fully abstraction results, though we omit the formulation of the superset calculus and its mappings.

8. Discussion

8.1. Related Works. While there have been many studies on types for mobile processes based on sorting [26, 7, 36, 11, 43, 41, 24, 22, 14, 42], as far as we know, the present work is the first one which captures the structure of protocol construction as types and establishes the full abstraction results for the basic encoding such as polyadic name passing.

(types with sequencing): A study to give a type-abstraction in the monadic asynchronous π-calculus with the same aim had been tried by Honda in 1992 [10], whose idea is reflected to the present construction to some extent. In that moment, however, his formulation (especially binding construction) was very complex. Independently, Pierce discovered the way to type-check a class of encodings of polyadic name passing in (a variant of) monadic π-calculus in which two local names are used only for input and output, respectively [35]. The differences are (1) a name can only carry one kind of types so typable terms are restricted, and (2) however the length of sequence can be indefinite. In both studies, the basic results as we established here, such as the subject reduction theorem and the full abstraction, are not presented.

(graphs): Representation of processes in the graphical (or geometric) framework gives us another grasp of name passing from the different viewpoint [13, 27, 31, 34, 46]. Our aim is to capture process behaviour as “types” and to obtain full abstraction, which is different from these works.

(linearity in processes): The notion of linearity is studied by Kobayashi and others [22] in Pict language and by [14] in an algebraic framework, though dynamic communication structures are not captured. In the former, the idea of “linearizability,” based on the above mentioned Pierce’s work, was proposed as an extension of their linear channel types. However structures of polyadic name passing or of (1.2) may not be typable when a name carries different types. Another difference is our explicit treatment of name transmission in a type, which we believe to be important for the kind of results we have obtained here.

(linear logic): Some ideas of Linear Logic [9] and Interaction Categories [1, 2, 8] are related (e.g. “multi-cuts” in [8]). Prasad [37] studies a term assignment to a generalisation of linear logic, where the distinction between “linear” and “classical” realms exists, which is also related.

(true concurrency): The causality of communication in process calculi has been studied in the setting of true concurrency, cf. [45]. The order relation in our safe graph is a concise way to encapsulate linear interaction behaviour rather than to describe general dependency among communication events. To capture more complex causality structure (such as labeled event structure in [45]) may be one possibility, though we may lose a simple combinatorial expression as we have in the present paper.

8.2. Extensions and Further Issues. There are several possible extensions and further issues of the present typing system, which we outline below.

(recursive type): For simplicity of presentation we do not form recursive protocol types. Its incorporation is standard by introducing the expressions μx.α and consider them modulo their tree unfoldings, cf.[43]. Immediately all results in the paper hold with this extension, with the corresponding set of polyadic terms extended with recursive sortings.

(full abstraction): There are many significant and useful encodings in (polyadic) π-calculus in which full abstraction results have not been known [25, 21, 44, 32]. This framework with extension [47] will be able to analyse and justify such nontrivial problems on translations [21, 25].

(asynchronous π and its combinators): In this paper we have exclusively dealt with graph types for synchronous monadic π-calculus. It is however possible to extend the present type discipline so that we can type asynchronous monadic mobile processes and their combinators [4, 12, 17, 18] (cf. [33, 38]), which is smaller than the present system but as expressive. Because there is no direct sequencing in output, the same notion of “safety condition” cannot be used. However, an extension of the notion of graph types and the safety condition can be done so that we can form a typing system for the asynchronous calculus along the same line as in Section 5. This will be treated in the sequel to present paper [47].

(other typing constructs): The construction of present types can be combined with various refinements on sorting studied by e.g. in [36, 11, 41, 24, 22, 14, 42] in either monadic or polyadic setting, which will be an interesting subject of study.

(algorithm): The present system does not induce the typing algorithm because a name can be used in several ways in linear space and classical space (cf. [22]). In this context, finding some analogue of the principal type schemes would be an interesting subject of study.

(general protocol types): It may be interesting to consider extensions such as a general name abstraction of graph types, pointed types with two or more heads (cf. [6]), and with a non-dual pairs (cf. [24]).

(semantics): Apart from practical viewpoints, one of the most essential issues for further study is to seek the canonical notion of semantics of types in process calculi, like “arrow types” well studied in λ-calculi and combinators [30]. Since our framework suggests one way to build up a significant computational causal chains in the basic π-calculus like functional types, we hope this work becomes a stepping stone in this line of research.

Acknowledgments. The author is indebted to Kohei Honda for his invaluable suggestion and continuous discussions on this work. Naoki Kobayashi provided helpful comments on the early version. She thanks Samson Abramsky, Cliff Jones, Benjamin Pierce, Kenjiro Taura and the members of Interaction Club at Edinburgh for their discussions, and Mario Tokoro for his encouragements. She is partially supported by JSPS Fellowship for Japanese Junior Scientists and Ogata-jyosei grant of Keio University.

References

[1] Abramsky, S., Computational interpretations of linear logic. TCS, 111(1-2):3-57, 1993.

[2] Abramsky, S., Gay, S. and Nagarajan, R., Interaction Categories and Foundations of Typed Concurrent Computing. Deductive Program Design, Springer-Verlag, 1995.

[3] Berry, G. and Boudol, G., The Chemical Abstract Machine. TCS, vol 96, pp. 217–248, 1992.

[4] Boudol, G., Asynchrony and π-calculus. INRIA Report 1702, INRIA, Sophia Antipolis, 1992.

[5] Davey, B.A. and Priestley, H.A., Introduction to Lattices and Order, CUP, 1990.

[6] Fournet, C. and Gonthier, G., The reflexive CHAM and the join-calculus, POPL’96, pp.372–385, ACM Press, 1996.

[7] Gay, S., A Sort Inference Algorithm for the Polyadic π-Calculus. POPL’93, ACM Press, 1993.

[8] Gay, S. and Nagarajan, R., A Typed Calculus of Synchronous Processes. LICS’95, IEEE, pp.210– 220, 1995.

[9] Girard, J.-Y., Linear Logic, TCS, Vol. 50, pp.1–102, North-Holland, 1987.

[10] Honda, K., Pre-types in mobile processes, a manuscript, 1992.

[11] Honda, K., Types for Dyadic Interaction. CONCUR’93, LNCS 715, pp.509–523, Springer-Verlag, 1993.

[12] Honda, K., A Study of ν-calculus and its Combinatory Representation, Phd Thesis in the Department of Computer Science, October, 1994.

[13] Honda, K., Notes on P-Algebra (1): Process Structure. Proc. TPPP’94, LNCS 907, pp.25–44, Springer-Verlag, 1995.

[14] Honda, K., Composing Processes, POPL’96, pp.344-357, ACM Press, 1996.

[15] Honda, K., An Object Calculus for Asynchronous Communication. To appear as LFCS report, 1996.

[16] Honda, K. and Tokoro, M., An Object Calculus for Asynchronous Communication. ECOOP’91, LNCS 512, pp.133–147, Springer-Verlag 1991.

[17] Honda, K. and Yoshida, N., On Reduction-Based Process Semantics. FSTTCS’13, LNCS 761, pp. 373–387, Springer-Verlag, December 1993.

[18] Honda, K. and Yoshida, N., Combinatory Representation of Mobile Processes. POPL’94, pp.348–360, ACM Press, 1994.

[19] Honda, K. and Yoshida, N., Replication in Concurrent Combinators, TACS’94, LNCS 789, pp.786–805, Springer, 1994.

[20] Honda, K. and Yoshida, N., On Reduction-Based Process Semantics. Full version of [17], TCS, pp.437–486, No.151, North-Holland, December, 1995.

[21] Jones, C.B., Process-Algebraic Foundations for an Object-Based Design Notation. UMCS-93-10-1, Computer Science Department, Manchester University, 1993.

[22] Kobayashi, N., Pierce, B., and Turner, D., Linear Types and π-calculus, POPL’96, pp.358–371, ACM Press, 1996.

[23] Lafont, Y., Interaction Nets, POPL’90, pp. 95–108, ACM press, 1990.

[24] Liu, X. and Walker, D., A polymorphic type system for the polyadic pi-calculus, CONCUR’95, LNCS, Springer-Verlag, 1995.

[25] Milner, R., Functions as Processes. Mathematical Structure in Computer Science, 2(2), pp.119– 146, 1992.

[26] Milner, R., Polyadic π-Calculus: a tutorial. Logic and Algebra of Specification, Springer-Verlag, 1992.

[27] Milner, R., Action structure for the π-calculus. Research Report ECS-LFCS-93-264, Department of Computer Science, University of Edinburgh 1993.

[28] Milner, R., Parrow, J.G. and Walker, D.J., A Calculus of Mobile Processes, Information and Computation 100(1), pp.1–77, 1992.

[29] Milner, R. and Sangiorgi, D., Barbed Bisimulation. Proc. of ICALP’92, LNCS 623, pp.685–695, Springer-Verlag, 1992.

[30] Mitchell, J., Type Systems for Programming Languages. Handbook of Theoretical Computer Science B, pp.367–458, MIT Press, 1990.

[31] Montanari, U. and Pistore, M., Concurrent Semantics for π-calculus, MFCS’95 and ENTCS, Vol. 1. Elsevier, 1995.

[32] Odersky, M., Applying π: Towards a basis for concurrent imperative programming, 2nd. SIPL, pp.95–108, 1995.

[33] Odersky, M., Polized Name Passing. FSTTCS’15, LNCS, Springer-Verlag, 1995.

[34] Parrow, J.G., Interaction Diagrams, REX’93., LNCS, Springer-Verlag, 1993.

[35] Pierce, B.C., Linearized Types for the π-calculus, a type script, December, 1994.

[36] Pierce, B.C. and Sangiorgi. D, Typing and subtyping for mobile processes. LICS’93, pp.187–215, 1993.

[37] Prasad, S., Towards a Formulae-as-Types View of Communicating Applicative Processes, Technical report ECRC-94-32, ECRC, 1994.

[38] Raja, N. and Shyamasundar, R.K., Combinatory Formulations of Concurrent Languages, pp. 156–170, ACSC’95, LNCS 1023, 1995.

[39] Sangiorgi, D., Expressing Mobility in Process Algebras: First Order and Higher Order Paradigms. Ph.D. Thesis, University of Edinburgh, 1992.

[40] Sangiorgi, D., On the Bisimulation Proof Method, LFCS report, ECS-LFCS-94-299, University of Edinburgh, 1994.

[41] Takeuchi, K., Honda, K. and Kubo, M., An Interaction-based Language and its Typing System. PARLE’94, LNCS 817, pp.398–413, Springer-Verlag, 1994.

[42] Turner, D., The π-calculus: Types, polymorphism and implementation, Phd Thesis, University of Edinburgh, 1996.

[43] Vasconcelos, V. and Honda, K., Principal Typing Scheme for Polyadic π-Calculus. CONCUR’93, LNCS 715, pp.524-538, Springer-Verlag, 1993.

[44] Walker, D., Objects in the π-calculus. Information and Computation, Vol. 116, pp.253–271, 1995.

[45] Winskel, G., An Introduction to Event Structures. In Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, LNCS 354, pp. 364–397,

[46] Yoshida, N., Graph Notation for Concurrent Combinators, TPPP’94, LNCS 907, pp.393–412, Springer-Verlag, 1995.

[47] Yoshida, N., Graph Types for Mobile Process Calculi II and III. To appear as CS technical reports, Keio University.

[48] Yoshida, N., A Study of Behavioural Semantics for Concurrent Calculi, Forthcoming PhD Thesis, Department of Computer Science, Keio University, October, 1996.

Appendix A. Proof of Lemma 4.12

We start from two lemmas: the first clause of the next one is needed for the proof of Lemma A.2 (ii), while the second one is for Lemma A.4. In the following, we use a notation: let us define the set of free subjects of P denoted by fs(P) inductively as follows.

fs(0) = ∅  fs(\overline{a}v.P) = \{a\} ∪ fs(P) fs(ax.P) = \{a\} ∪ (fs(P)\\{x\})
fs((a)P) = fs(P)\{a} fs(P | Q) = fs(P) ∪ fs(Q) fs(!P) = fs(P)

A.1. Lemma. Suppose Γ′ ⊢ P_{1} | P_{2} ▷_{A′}G is derived by applying a sequence of zero or more (weak) rules and (par) rule like the following.

{Γ_{1} ⊢ P_{1} ▷_{A_{1}}G_{1} \atop ⋮ . (weak) × m} ; Γ ⊢ P_{1} ▷_{A′_{1}}G_{1} {Γ_{2} ⊢ P_{2} ▷_{A_{2}}G_{2} \atop ⋮ . (weak) × n} ; Γ ⊢ P_{2} ▷_{A′_{2}}G_{2}

Γ ⊢ P_{1} | P_{2} ▷_{A′_{1}∪A′_{2}∪A}G_{1} ⊙ G_{2} (par)

⋮ . (weak) × k

Γ′ ⊢ P_{1} | P_{2} ▷_{A′}G_{1} ⊙ G_{2}

Then we have:

(i) a ∈ fs(P_{1}) ∩ fs(P_{2}) implies either a ∈ A′ or a ∈ fn(Γ′). Moreover, if a ∈ A′, there is only one prime term a ∈ fs(P_{1i}) in P_{1} and also only one prime term a ∈ fs(P_{2i}) in P_{2}.

(ii) a ∈ fn(Γ′) implies a ∉ fn(G_{1}) ∪ fn(G_{2}) ∪ A_{1} ∪ A_{2}. Proof. For the first clause in (i), we show a ∈ fs(P_{1}) ∩ fs(P_{2}) ⇒ a ∉ A_{1} ∪ A_{2} ∪ fn(G_{1} ⊙ G_{2}). a ∉ fn(G_{1} ⊙ G_{2}) is obvious by the definition of cut function. Then we know a ∈ A_{1} ⇒ a ∉ A_{2} ∧ a ∉ fn(G_{2}) ∧ a ∉ fn(Γ). But fn(P_{2}) ⊂ fn(Γ) ∪ A_{2} ∪ fn(G_{2}). Therefore a ∉ fn(P_{2}), a contradiction. Similarly for the case a ∈ A_{2}, hence done.

(ii) is easy because if a ∈ fn(Γ), then a ∉ A′ nor a ∉ fn(G_{1} ⊙ G_{2}) = (fn(G_{1}) ∪ fn(G_{2}))\(fn(G_{1})∩fn(G_{2})), which implies a ∉ A_{1} ∪A_{2} because A′ ⊃ A_{1} ∪A_{2}. Moreover, a ∉ (fn(G_{1}) ∩ fn(G_{2})) = A because A′ ⊃ A, hence the result.

The following lemma is necessary for the proof of (iv) of Lemma 4.12.

A.2. Lemma. Suppose Γ ⊢ (P |Q)|R ▷_{A}G is derived from Γ ⊢ P ▷_{A_{1}}G_{1}, Γ ⊢ Q ▷_{A_{2}}G_{2} and Γ ⊢ R ▷_{A_{3}} G_{3} with G ≡_{α} ((G_{1} ⊙ G_{2}) ⊙ G_{3}). Then we have:

(i) fn(G_{1}) ∩ fn(G_{2}) ∩ fn(G_{3}) = ∅. (ii) Γ ⊢ P | (Q | R) ▷_{A} G is proved. Proof. For (i), suppose Γ ⊢ (P | Q) ▷_{A_{1}∪A_{2}∪A′} G′ is derived from Γ ⊢ P ▷_{A_{1}} G_{1} and Γ ⊢ Q ▷_{A_{2}}G_{2}. Then by the definition of the cut function, we know a ∈ fn(G_{1}) ∩ fn(G_{2}) ⇒ a ∈ A′, which means a ∉ fn(G_{3}). (ii) is easy from Proposition 3.11 (ii), Lemma A.1 (i) and the above.

Now we prove the typing system is closed under structural rules.

Proof of Lemma 4.12 (iv) (structural rules)

For α-conversion, the case ax.P ≡_{α} ay.P {y/x} (y fresh) is easy by checking (in_{i}) rules. For (a)P ≡_{α} (b)P {b/a} (b fresh), assume

\frac{Γ ⊢ P ▷_{A} G}{Γ\a ⊢ (a)P ▷_{A\\{a\}} G} (res)

then with noting a ∉ fn(G) and assuming b fresh, we have:

\frac{\frac{Γ ⊢ P ▷_{A} G}{Γ\{b/a\} ⊢ P \{b/a\} ▷_{A\{b/a\}} G\{b/a\}} (renaming lemma)}{Γ\{b/a\}\b ⊢ (b)P \{b/a\} ▷_{A\{b/a\}\\{b\}} G} (res)

The most careful rule is (P | Q)R ≡ P | (Q | R), but it is proved with Lemma A.2 (ii). For the case of “scope open”, i.e. (a)P | Q ≡ (a)(P | Q) (a ∉ FN (Q)), assume

\begin{matrix}{Γ ⊢ P ▷_{A_{1}} G_{1} \atop Γ\a ⊢ (a)P ▷_{A_{1}\\{a\}} G_{1}} (res) & Γ\a ⊢ Q ▷_{A_{2}} G_{2} \\ Γ\a ⊢ (a)P | Q ▷_{A_{1}\\{a\}∪A_{2}∪A′} G_{1} ⊙ G_{2} \end{matrix} (par)

W.l.o.g. we can assume a ∉ A_{2} ∪ fn(G_{2}) because typing system is closed under αconversion and renaming lemma. Then by (weak) rule, Γ ⊢ Q ▷_{A_{2}}G_{2} is derived from Γ\a ⊢ Q ▷_{A_{2}}G_{2}. Hence Γ\a ⊢ (a)(P | Q) ▷_{(A_{1}∪A_{2}∪A′)\{a}} G_{1} ⊙ G_{2} is proved. The other direction is similar. Other rules are obvious.

Proof of Lemma 4.12 (v): (combination)

Suppose (in_{1}) is used. Then by Lemma 4.12 (i), a cannot be in Γ, therefore it should again be in G_{1} and G_{2}. So j = 3, 4 are impossible. But the combination with (out_{2}) is also forbidden because there is no complete type like “(y)”. Similarly for other cases.

For the next lemma, we define “inversion”. Hereafter we assume π-terms always obey the binding condition. Also, by 4.13 (iv), we shall safely consider typed π-terms modulo their α-equality, so that α-conversion of terms may be done implicitly during deduction.

A.3. Definition. (inversion) We say an ordered tuple of rules written (rule A) → (rule B) is invertible when, if any proof ends with a successive application of those two rules, there is a proof with the same conclusion in which the final two deductions are by those two rules in the reversed order.

A.4. Lemma. (inversions) (any rule in π_{G}) → (weak) is invertible.

Proof. For (par) rule, we use Lemma A.2 (ii). Others are mechanical.

Now we can prove the fundamental lemma using Lemma 5.8 (i–v).

Proof of Lemma 4.12 (vi): (substitution lemma)

By the last clause of Lemma 4.12 (i) we assume names in fn(Γ) ∪ {a, b} and A are restricted to free names of P. When either a or b is not in fn(P), or when we have a = b, the statement is immediate using (Renaming Lemma when b ∉ fn(P)). We thus assume a, b ∈ fn(P) and a ≠ b in the following. This means that we do not have to consider (weak) rule by Lemma 4.12 (i).

So assume a: β, b: β, Γ ⊢ P ▷_{A}G is derived. We use induction on the structure of P.

(i) The cases P =^{def} 0 is trivial using Lemma 4.12 (i).

(ii) The cases P =^{def} !P′ is obvious by Lemma 4.12 (vi) with inductive hypothesis of

P′. (iii) For the case P =^{def} (c)P′, by Lemma A.4, we safely assume the last deduction is:

(res) \frac{a: β, b: β, Γ ⊢ P′ ▷_{A∪\{c\}}G}{a: β, b: β, Γ ⊢ (c)P′ ▷_{A}G}

Note, by assumption, we have a, b ∈ fn(P) hence a ≠ c and b ≠ c. Thus b : β, Γ ⊢ P′{b/a} ▷_{A∪{c}}G by induction, and then by using (res), we get the required sequent. The case c ∈ fn(Γ) is similar.

(iv) For the case P =^{def} P_{1} | P_{2}, by Lemma A.4, we can safely assume it is derived from (par). Thus we have:

(par) \frac{a: β, b: β, Γ ⊢ P_{1} ▷_{A_{1}}G_{1} a: β, b: β, Γ ⊢ P_{2} ▷_{A_{2}}G_{2}}{a: β, b: β, Γ ⊢ P_{1} | P_{2} ▷_{A_{1}∪A_{2}∪A}(G_{1} ⊙ G_{2})}

By applying inductive hypothesis, we have b: β, Γ ⊢ P_{i}{b/a} ▷_{A_{i}}G_{i} (i = 1, 2). Then using (par) rule again, we are done.

(v) If P =^{def} cx.P′, we have a: β, b: β, Γ ⊢ cx.P ▷_{A}G. We safely assume, by Lemma A.4, the sequent is derived using (in) directly and x ∉ {a, b}. If c ∉ {a, b}, the inductive hypothesis can be easily applied. So assume a = c. We first notice the last rule cannot be (in_{i}) for 1 ≤ i ≤ 2. So there are two cases.

(1) Suppose the sequent is derived with the last rule (in_{3}), i.e.

\frac{a: β, b: β, Γ ⊢ P ▷_{A}G β = \{↓(x) → G, ↑(x) → \overline{G}\}}{a: β, b: β, Γ ⊢ ax.P ▷_{A}}

Note a cannot occur in G, hence by induction we have: b: β, Γ ⊢ P {b/a} ▷_{A}G. By applying (in_{3}) rule again, we get b: β, Γ ⊢ bx.P {b/a} ▷_{A}, as required.

(2) Suppose the sequent is derived with the last rule (in_{4}), i.e.

(in_{4}) \frac{a: (α), b: (α), x: α, Γ ⊢ P ▷_{A}}{a: (α), b: (α), Γ ⊢ ax.P ▷_{A}}

By induction we have b: (α), x: α, Γ ⊢ P {b/a} ▷_{A}. Then, using (in_{4}) again, we get b: (α), Γ ⊢ bx.P {b/a} ▷_{A}, as required.

(vi) The case for P =^{def} \overline{c}x.P′ is essentially the same as above, with some care in the

manipulation of the auxiliary name set when (out_{3}). The case b = c is similar so we omit it.

Appendix B. Proof of Subject Reduction Theorem

First we state the property on cut-elimination.

B.1. Lemma. Suppose: (1) G_{1} ≍ G_{2} (2) G_{1} is a-pointed whose head is n and G_{2} is a-pointed whose whose head is \overline{n}. Then:

(i) (G_{1}\n) ≍ (G_{2}\\overline{n}). (ii) (G_{1} ⊙ G_{2}) ≅ ((G_{1}\n) ⊙ (G_{2}\\overline{n})). Proof. Easy by Propositions 3.8 and 3.10.

To prove subject reduction, we use the following characterisation of one-step reduction and the form of π-terms.

B.2. Lemma. Define ⟶′ by the least relation generated by:

\begin{matrix}(COM’) & (c̃)(P_{1} | ... | (ax.P | \overline{a}v.Q) | .... | P_{n}) ⟶′ (c̃)(P_{1} | ... | (P \{v/x\} | Q) | ... | P_{n}) \\ (STR) & P ≡ P′ P′ ⟶′ Q′ Q ≡ Q′ ⇒ P ⟶′ Q. \end{matrix}

where we assume P_{i} in (COM’) are all input, output agents, or replicator. Then we have ⟶′ = ⟶.

Proof. By checking each rule for ⟶′ is derivable from those for ⟶ and vice versa.

Now we are ready to prove the subject reduction theorem.

Proof of the Theorem 4.13: (Subject Reduction Theorem) By induction on the length of derivation of ⟶′. We assume ⟶′ is derived by the rules in Lemma B.1. If the derivation ends with the application of (STR), then the result is immediate from Lemma 4.12 (iv). So suppose the derivation ends with (COM’) rule. Then we have a sequent: Δ ⊢ (c̃)(P_{1}|P_{2}|...|(ax.P |\overline{a}v.Q)|...|P_{n}) ▷_{A_{0}} G_{0}. By Lemma 4.12 (iii), we can assume there is a deduction:

Γ ⊢ ax.P | \overline{a}v.Q ▷_{A} G.  (B.1)

Now we prove

Γ ⊢ P {v/x} | Q ▷_{A} G  (B.2)

Once (B.2) is proved, by replacing the deduction for (B.1), we can get the sequent Δ ⊢ (c̃)(P_{1} | P_{2} | ... | P {v/x} | Q | ... | P_{n}) ▷_{A_{0}} G_{0}, hence the result.

Note, by Lemma A.4, we can assume that the application of (weak) occurs only at the first step after each axiom. So we can safely assume that (B.1) is derived by applying (par) rule at the last step, with antecedents Γ ⊢ ax.P ▷_{A_{1}}G_{1} and Γ ⊢ \overline{a}v.Q ▷_{A_{2}}G_{2}, where, by Lemma 4.12 (i), we have

fn(Γ) ∩ A = fn(Γ) ∩ fn(G) = A ∩ fn(G) = ∅.  (B.3)

Now we can assume that these antecedents are derived first introducing these prime terms by:

(in_{i}) \frac{Γ_{1} ⊢ P ▷_{A_{1}}G′_{1}}{Γ ⊢ ax.P ▷_{A_{1}}G_{1}} (out_{j}) \frac{Γ ⊢ Q ▷_{A′_{2}}G′_{2}}{Γ ⊢ \overline{a}v.Q ▷_{A_{2}}G_{2}}  (B.4)

with A = A_{1} ∪ A_{2} ∪ A′ (A′ = fn(G_{1}) ∩ fn(G_{2})) and G = G_{1} ⊙ G_{2}.

By Combination Lemma, the step (B.4) above cannot be done for arbitrary combination of i and j. So there are following four cases.

Case (in_{1})–(out_{1}): There are derivations such that

\frac{Γ ⊢ P ▷_{A_{1}}G′_{1}}{Γ ⊢ ax.P ▷_{A_{1}} a↓(x) → G′_{1}}  \frac{Γ ⊢ Q ▷_{A_{2}\\{v\}}G′_{2}}{Γ ⊢ \overline{a}v.Q ▷_{A_{2}} a↑(v) → G′_{2}}  (B.5)

We immediately know v ∉ fn(G′_{1}), hence, by Renaming Lemma, that

Γ ⊢ P {v/x} ▷_{A_{1}}G′_{1}{v/x}  Γ ⊢ Q ▷_{A_{2}}G′_{2}.  (B.6)

Now we note that, by the condition of (par) rule,

(a↓(x) → G′_{1}) ≍ (a↑(v) → G′_{2})  (B.7)

By α-conversion (noting v ∉ fn(G′_{1})), (B.7) becomes:

(a↓(v) → G′_{1}{v/x}) ≍ (a↑(v) → G′_{2})  (B.8)

We then safely assume (G′_{1}{v/x} ⊙ G′_{2}) ≡_{α} G by Lemma B.1. This shows, if we apply (par) to (B.6), that:

Γ ⊢ P {v/x} | Q ▷_{A_{1}∪A_{2}∪A′′}G

where A′′ ∪{a, v} = A′ (note v, a ∉ fn(Γ)∪fn(G) by v ∈ A_{2} and (B.5)). Then applying (weak) rule, we get the required result.

Case (in_{2})–(out_{2}): There are derivations such that

\frac{x : α, Γ ⊢ P ▷_{A_{1}}G′_{1}}{Γ ⊢ ax.P ▷_{A_{1}} a↓α → G′_{1}}  \frac{Γ ⊢ Q ▷_{A_{2}\\{v\}}G′_{2}}{Γ ⊢ \overline{a}v.Q ▷_{A_{2}} a↑α → G′_{2}}  (B.9)

with v ≠ x, x, v ∉ fn(G_{1}) ∪ A_{1} and v : α ⊂ Γ. By Substitution Lemma, we have Γ ⊢ P {v/x} ▷_{A_{1}}G′_{1}. Then, using Lemma B.1, we have the required result.

Case (in_{3})–(out_{3}): There are derivations such that:

\frac{a: β, Γ′ ⊢ P ▷_{A_{1}}G′_{1}}{a: β, Γ′ ⊢ ax.P ▷_{A_{1}}}  \frac{a: β, Γ′ ⊢ Q ▷_{A_{2}\\{v\}}\overline{G′_{1}}\{v/x\}}{a: β, Γ′ ⊢ \overline{a}v.Q ▷_{A_{2}}}  (B.10)

with a : β, Γ′ = Γ, β = \{↓ (x) → G′_{1}, ↑ (x) → \overline{G′_{1}}\}. By Proposition 3.10 (ii) (G_{1} ⊙ \overline{G}_{1} = ∅) and Lemma B.1, α-conversion as in the case of (in_{1})–(out_{1}), we have the required result.

Case (in_{4})–(out_{4}) Easy by Substitution Lemma (cf. the case (in_{2})–(out_{2})).

Appendix C. Proof for Lemma 5.9

.

Suppose Γ ⊢ P ▷_{A} G. Then we can write P as a normal form: P ≡ (b̃)P′ ≡ (b̃)(P_{1} | P_{2} | ... | P_{n}) where P_{i} is an input, output agents, or replicator. We prove the strong statement: P →_{β} Q_{1} and P ⟶ Q_{2} with Q_{1} ≢ Q_{2} then there exists Q′ s.t. Q_{1} ⟶ Q′ and Q_{2} →_{β} Q′.

If P →_{β} Q_{1} is derived starting from the rule (β_{2}), it is obvious (cf. [18, 19, 22]). So suppose P →_{β} Q_{1} is derived starting from the rule (β_{1}). Then there should be a name c s.t. c ∈ A ∩ fs(P′), which is obtained by cut eliminations in (par) rule. So by Lemma 4.12 (iv) and Lemma A.4, there is a derivation

{Γ ⊢ P_{i} ▷_{A_{i}} G_{i} Γ ⊢ P_{j} ▷_{A_{j}} G_{j} \atop Γ ⊢ P_{i} | P_{j} ▷_{A′} G_{i} ⊙ G_{j}} (par)

for some 1 ≤ i ≠ j ≤ n with A′ ⊂ A. By Lemma A.1 (i), if P_{i} ≡ cx.P′_{i}, there is no other receptor whose subject is c in P, and there is only one output agent whose subject is c by definition of a cut function. So we set P_{j} ≡ \overline{c}v.P′_{j}.

Suppose P ≡ (b̃)(cx.P′_{i} | \overline{c}v.P′_{j} | R) →_{β} (b̃)(P′_{i}\{v/x\} | P′_{j} | R) ≡ Q_{1} and P ⟶ Q_{2} with Q_{1} ≢ Q_{2}. Then Q_{2} should have a form: Q_{2} ≡ (b̃)(cx.P′_{i} | \overline{c}v.P′_{j} | R′) with R ⟶ R′ because of c ∉ fs(R′). Thus two redex pairs are never overlapped. Hence

Q_{1} ⟶ (b̃)(P′_{i}{v/x} | P′_{j} | R′) =^{def} Q′ and Q_{2} →_{β} Q′, as required.

Appendix D. Proof of Proposition 5.12

By induction on P. Suppose Γ ⊢ P ▷_{A}G.

There is no case for P ≡ 0 and P ≡!Q because G ≠ ∅.

Case P ≡ ax.Q. By rules in Figure 5, if n is head in G, then n = a ↓(x) or n = a ↓α, and G ≡_{α} n → G_{0}. So we only consider (in_{1}) and (in_{2}) neglecting (weak) rule by Lemma A.4.

If n = a↓(x), there is a derivation

(in_{1}) \frac{Γ ⊢ Q ▷_{A}G_{0}}{Γ ⊢ ax.Q ▷_{A} a↓(x) → G_{0}}  (D.1)

with x ∉ fn(Γ) ∪ A. Thus by selecting x′ ∉ fn(Q) ∪ fn(G) ∪ {a} and then renaming

x with x′, we have Γ ⊢ Q{x′/x} ▷_{A}G_{0}{x′/x} with ax.Q ⟶^{ax′} Q{x′/x}, which satisfies

the (i), as required.

If n = a↓α, there is a derivation

(in_{2}) \frac{x: α, Γ ⊢ Q ▷_{A}G_{0}}{Γ ⊢ ax.Q ▷_{A} a↓α → G_{0}}  (D.2)

with x ∉ fn(G) ∪ A. Hence x: α, Γ ⊢ Q ▷_{A}G with ax.Q ⟶^{ax} Q, which satisfies (iii).

Case P ≡ \overline{a}x.Q. By the same reasoning, we only have to consider (out_{1}) and (out_{2}). If n = a↑(x), there is a derivation

(out_{1}) \frac{Γ ⊢ Q ▷_{A_{0}}G_{0}}{Γ ⊢ \overline{a}x.Q ▷_{A_{0}∪\{x\}} a↑(x) → G_{0}}  (D.3)

with A_{0} ∪ \{x\} = A. Thus \overline{a}x.Q ⟶^{\overline{a}x} Q, which is just the second clause in (ii). If n = a↑α, there is a derivation

(out_{2}) \frac{x: α, Γ_{0} ⊢ Q ▷_{A}G_{0}}{x: α, Γ_{0} ⊢ \overline{a}x.Q ▷_{A} a↑α → G_{0}}  (D.4)

with Γ = x: α, Γ_{0}. Thus \overline{a}x.Q ⟶^{\overline{a}x} Q, which is just the second clause in (ii).

Case P ≡ (b)Q. Suppose there is a derivation

(res) \frac{Γ_{0} ⊢ Q ▷_{A_{0}} G}{Γ_{0}\b ⊢ (b)Q ▷_{A_{0}\\{b\}} G} (b ∉ fn(G))  (D.5)

and Q → →_{β} Q′′ ⟶^{l} Q′ with either l = ac, \overline{a}c or a(c). First we note b ≠ a by the condition in (res) rule. If c ≠ b, it is obvious by the induction on Q. Suppose l = \overline{a}b (when l = a(b), ab, we can use α-convertibility on (b)Q). Then it relates with either the second clause in (ii) or the second one in (iv). In the second clause in (ii),

Q′′ ⟶^{\overline{a}b} Q′ and Γ ⊢ Q′ ▷_{A} (G\a↑(x))\{b/x\} with A_{0} = A ∪ \{b\}

By scope open rule in the labeled transition system, we know (b)Q′′ ⟶^{\overline{a}(b)} Q′. By (D.5) together with the subject reduction theorem, now Γ ⊢ (b)Q → →_{β} (b)Q′′ ▷_{A}G fits the first clause in (ii), as required. The second case in (iv) is similar with considering the elimination of b from Γ_{0} in (D.5).

Case P ≡ P_{1} | P_{2}. This is the most non-trivial case. Suppose a↓(x) ∈ Hd(G). There exists the following deduction:

{Γ ⊢ P_{1} ▷_{A_{1}} G_{1} Γ ⊢ P_{2} ▷_{A_{2}} G_{2} \atop Γ ⊢ P_{1} | P_{2} ▷_{A_{1}∪A_{2}∪A′} G_{1} ⊙ G_{2}} (par)

with A = A_{1} ∪ A_{2} ∪ A′ and G_{1} ⊙ G_{2} ≡_{α} G. By inductive hypothesis, Γ ⊢ P_{i} ▷_{A_{i}} G_{i} satisfies one of the cases from (i) to (iv) in Proposition 5.12.

Then there are two cases.

(1) a↓(x) ∈ Hd(G_{i}).

Then a ∉ fn(G_{j}) with i ≠ j because A′ = fn(G_{1}) ∩ fn(G_{2}) by definition of cut function.

(2) a↓(x) ∉ Hd(G_{1}) ∪ Hd(G_{2}), i.e. a head a↓(x) is newly appeared after multi-cuts. Case (1) is easy by induction hypothesis. In case (2), w.o.l.g. we assume newly appeared head was contained in G_{1}. Then this implies, in (par), we did multi-cuts of all the nodes of n_{i} such that n_{1} → n_{2} ⋯ → n_{n} → n in G_{1}.

Assume b is a subject in n_{i}. If b is bound name in G_{1}, there is an atomic node n_{j} whose label is c ↑(b) or c ↓(b) with j < i. Note by covering condition (ii-2) of the cut function, such a node n_{j} is in domain preserving the ordering n_{j} ≻≻ n_{i}. If n_{j} = c↑(b), then b ∈ A_{1}, or if n_{j} = c↓(b), then b ∈ A_{2} by definition of (out_{1}) in Figure 5. On the other hand, if b = fn(n_{i}) is free in G_{1}, then clearly b ∈ A′ again by definition of cut function. So we have b ∈ fn(n_{i}) ∪ fn(Hd(G_{1} ⊙ G_{2})) ⇒ b ∈ A.

Now noting ordering → is preserved by multi-cuts by Proposition 3.10, we know if n_{1} is a head of G_{1} and in the domain of the cut function, then \overline{n}_{1} is also a head of G_{2}. Suppose e ∈ fn(n_{1}). Then, by the previous argument e ∈ A′ and, by inductive hypothesis, there is a β-reduction P_{1} | P_{2} → →_{β} P′_{1} | P′_{2} with P_{1} → →_{β} P′_{1} and P_{2} → →_{β} P′_{2} with e ∈ AN_{−}(P′_{1}) ∩ AN_{+}(P′_{2}). Therefore, P′_{1} | P′_{2} ≡ (c̃)(ex.R_{1} | \overline{e}v.R_{2} | R_{3}) →_{β} (c̃)(R_{1}\{v/x\} | R_{2} | R_{3}) in which prefixes “ex” and “\overline{e}v” corresponding to n_{1} and \overline{n}_{1} are eliminated. By applying this to all the nodes n_{i} one by one, noting fn(n_{i}) ∈ A, from i to n, we have P_{1} | P_{2} → →_{β} P′ with Γ ⊢ P′ ▷_{A}G_{1} ⊙ G_{2} and a ∈ AN_{−}(P′), hence done with (in) case. Other cases are just the same.

Appendix E. Basic Properties in Reduction Closed Theories

This appendix collects the proofs of basic properties on reduction closed theories. More development on other calculi is left to [48].

E.1. Proposition. Assume R and R_{0} are reflexive. Then we have:

(i) Φ_{p}(R) ⊂ Φ_{pr}(R) ⊂ Φ_{c}(R). (ii) Φ_{pr}(Φ_{Φ_{c}(R_{0})}(R)) ⊂ Φ_{Φ_{c}(R_{0})}(Φ_{pr}(R)).

Proof. (i) is obvious. For (ii), let Φ_{c}(R_{0}) =^{def}≅, then

P Φ_{pr}(≅ R ≅) Q ⇒ P ≡ C_{r}[P_{0}] ∧ P_{0} ≅ P_{1} R Q_{1} ≅ Q_{0} ∧ C_{r}[Q_{0}] ≡ Q
⇒ P ≡ C_{r}[P_{0}] ≅ C_{r}[P_{1}] ∧ P_{1} R Q_{1} ∧ C_{r}[Q_{0}] ≡ Q
⇒ P ≡ C_{r}[P_{0}] ≅ C_{r}[P_{1}] Φ_{pr}(R) C_{r}[Q_{0}] ≡ Q

Proof of Lemma 6.4

For (i), set S =^{def} Φ(R). Then obviously Φ(R) ↦ Φ(R) with using monotonicity of Φ and identity of Φ. For (ii), firstly for monotonicity, we note: R ↦ S ⇒ Φ′(R) ↦ Φ′(S) ⇒ Φ ∘ Φ′(R) ↦ Φ ∘ Φ′(S) by monotonicity of Φ and Φ′. For identity of Φ ∘ Φ′, the inclusion Φ ∘ Φ′ ∘ Φ ∘ Φ′ ⊃ Φ ∘ Φ′ is obvious with the above result, while the other inclusion Φ ∘ \underline{Φ′ ∘ Φ} ∘ Φ′ ⊂ Φ ∘ Φ′ is proved by applying the condition Φ′ ∘ Φ ⊂ Φ ∘ Φ′ to the underlined part.

Proof of Lemma 6.5

First we note Φ_{p}(R) and Φ_{c}(R) are substitution closed by Proposition 6.2. Then the rest is also by induction on the derivation in Figure 5, using the same reasoning as in the proof in Lemma 3.6 in [20]. Let ≅=^{def} Φ_{c}(R). We establish, for a pair P and Q such that P ≅ Q, the following stronger statement (note ≅ contains ≡ below), we only have to check: for any R, P | R ⟶ P′ implies, for some Q′, we have Q | R ⟶ Q′ with P′ ≅ Q′, assuming P ≅ Q, at each step of derivation. As the proof in Lemma 3.6 in [20], the only interesting case is that ax.P ≅ ax.Q is derived by (in_{i}) at the last step. The case (P | R) ⟶ (P | R′) is trivial. So assume P and R are interacting together. Then for some c̃, \overline{a}v.R_{0} and R_{1}, we can assume

(P | R) ≡ (c̃)(ax.P | \overline{a}v.R_{0} | R_{1}) ⟶ (c̃)(P \{x/v\} | R_{0} | R_{1})

By Lemma 4.12 (iii,vi), we have the following deduction for each i = 1, 2, 3, 4.

(in_{i}) \frac{Γ_{1} ⊢ P ▷_{A_{1}}G′_{1}}{Γ ⊢ ax.P ▷_{A_{1}}G_{1}} (out_{i}) \frac{Γ ⊢ R_{0} ▷_{A′_{2}}G′_{2}}{Γ ⊢ \overline{a}v.R_{0} ▷_{A_{2}}G_{2}}  (E.1)

Note the step E.1 above cannot be done for arbitrary combination of (in_{i}) and (out_{j}) by Combination Lemma (Lemma 4.12(v)). Now we want to prove, if Γ ⊢ ax.P ≅ ax.Q ▷_{A_{1}}G_{1}, then, Γ ⊢ P {v/x} ≅ Q{v/x} ▷_{A_{1}}G′_{1}{v/x} with G′_{1}{v/x}⊙G′_{2} = G_{1}⊙G_{2}. By Lemma B.1, as seen in the proof of Subject Reduction Theorem, we know there exists, the following deduction: Γ{v/x} ⊢ P {v/x} ▷_{A_{1}}G′_{1}{v/x} which satisfies the above graph condition. So we only have to prove P {v/x} ≅ Q{v/x} can be derived, which leads us to the required result: for some Δ, A, G we have the equation Δ ⊢ (c̃)(P {v/x} | R_{0} | R_{1}) ≅ (c̃)(Q{x/v} | R_{0} | R_{1}) ▷_{A′}G′.

We will prove following four cases.

Case i = 1: There are derivations such that

\frac{Γ ⊢ P ▷_{A_{1}}G′_{1}}{Γ ⊢ ax.P ▷_{A_{1}} a↓(x) → G′_{1}}  \frac{Γ ⊢ R_{0} ▷_{A_{2}\\{v\}}G′_{2}}{Γ ⊢ \overline{a}v.R_{0} ▷_{A_{2}} a↑(v) → G′_{2}}  (E.2)

To compose ax.Q with \overline{a}v.R_{0}, there should be a deduction

\frac{Γ ⊢ Q ▷_{A_{1}}G′_{1}}{Γ ⊢ ax.Q ▷_{A_{1}} a↓(x) → G′_{1}}  (E.3)

with Γ ⊢ ax.P ≅ ax.Q ▷_{A_{1}}a↓(x) → G′_{1}. We immediately know v ∉ fn(G′_{1}), hence, by Lemma 4.12 (iii) (renaming lemma), from E.2 and E.3, that

Γ ⊢ P {v/x} ▷_{A_{1}}G′_{1}{v/x} and Γ ⊢ Q{v/x} ▷_{A_{1}}G′_{1}{v/x}  (E.4)

This implies, by substitution closure of ≅, Γ ⊢ P {v/x} ≅ Q{v/x} ▷_{A_{1}} G′_{1}{v/x}, as required.

Case i = 2: We can set Γ = v: α, Γ_{0}. Then v: α, Γ_{0} ⊢ ax.P ≅ ax.Q ▷_{A_{1}}a ↓α → G′_{1} comes from v: α, x: α, Γ ⊢ P ≅ Q ▷_{A_{1}} G_{1}, then we use substitution closure.

Case i = 3: Similar with the case i = 1.

Case i = 4: Similar with the case i = 2.

(ii) is similarly established with the same reasoning: for each derivation P ≅ Q, we prove (P | R) ⇓_{a^{θ}} ⇒ (Q | R) ⇓_{a^{θ}} for all R, noting in particular, ax.P ⇓_{a^{−}}

Rcpt \frac{a: (S_{1}, .., S_{n}), x_{i}: S_{i}, Γ ⊢ P}{a: (S_{1}, .., S_{n}), Γ ⊢ a(x_{1}...x_{n}).P} Emt \frac{a: (S_{1}, .., S_{n}), x_{i}: S_{i}, Γ ⊢ P}{a: (S_{1}, .., S_{n}), x_{i}: S_{i}, Γ ⊢ \overline{a}⟨x_{1}..x_{n}⟩.P}
Comp \frac{Γ ⊢ P Γ ⊢ Q}{Γ ⊢ P | Q}  Scop \frac{Γ ⊢ P}{Γ\\{x\} ⊢ (x)P}
Repl \frac{Γ ⊢ P}{Γ ⊢!P}  Weak \frac{Γ ⊢ P}{a: (S_{1}, .., S_{n}), Γ ⊢ P}  Nil ∅ ⊢ 0

Figure 6. Typing System for Polyadic π-calculus.

⇒ ax.Q ⇓_{a^{−}}.

Proof of Lemma 6.6

By Subject Reduction Theorem, we safely omit the type annotation. For (i), first we show that Φ≅ is r.c. respectable. Suppose R ↦ S. We will establish Φ≅(R) ↦ Φ≅(S). Assume P ≅ P_{0} R Q_{0} ≅ Q. Then whenever P ⟶ P′, there exists P_{0} ⟶ P′_{0} and P_{0} ≅ P′_{0}. Then by assumption R ↦ S , we have Q_{0} ⟶ Q′_{0} with P′_{0} ≅ S ≅ Q′_{0}. By also applying reduction closure property between Q_{0} and Q, we have P′ ≅ P′_{0} ≅ S ≅ Q′_{0} ≅ Q′, which implies P′ Φ≅(S) Q′ by symmetry of ≅. Identity of Φ≅(S) is mechanically calculated by the property ≅ ≅ = ≅. The monotonicity is obvious. For the second case, since the transitive closure of ≅ R ≅ is a reducition-closed p-relation, Φ_{c}(≅ ∪R) is reduction-closed congruence by Lemma 6.5 together with Φ_{c}(≅ ∪R) = Φ_{c}(≅ R ≅).

(ii) is also mechanical.

(iii) First we note by Proposition 6.2, Φ≅(R) and Φ_{pr}(R) are substitution closed, and then Φ_{c}(R∪ ≅) is. Now we use Lemma 6.4 (ii). Let us set Φ≅ to Φ and Φ_{pr} to Φ′ of Lemma 6.4, and then check (1) Φ≅ and Φ_{pr} are r.c. respectable and (2) Φ≅ ∘ Φ_{pr} ⊇ Φ_{pr} ∘ Φ≅. First r.c. respectability of Φ≅ and Φ_{pr} are given by (i) and (ii). The second clause Φ≅ ∘ Φ_{pr} ⊇ Φ_{pr} ∘ Φ≅ is proved by Lemma E.1 (ii).

Appendix F. Typing System and Labeled Transition Relation in Polyadic π-calculus

First we re-introduce the typing system in [43] in Figure 6, essentially equivalent to the system in [26], give the sequent of form ⊢ P ≻ Γ,which we write Γ ⊢ P where Γ is a map from a finite set of names to the set of sortings.

Next we introduce the labels which are same as 2.2.2 in [39]. The set of labels common to two labeled transition relations, ranged over by l, l′, .., is given by:

l = τ | a⟨x_{1}...x_{n}⟩ | (ỹ) \overline{a}⟨v_{1}...v_{n}⟩

where in output {ỹ} ⊆ {ṽ}\{a} bounds the values ṽ. We write n(l), bn(l) and fn(l) for the sets of names, bound and free names in l. Then the transition system is presented as follows.

F.1. Definition. (labeled transition system in polyadic π-calculus) In the following, we sometimes write Γ ⊢ P ⟶_{p}^{l} P′ as Γ ⊢ P ⟶_{p}^{l} Γ ⊢ P′.

inp a: (S_{1}, .., S_{n}), v_{i}: S_{i}, Γ ⊢ a(x_{1}...x_{2}).P ⟶_{p}^{a⟨v_{1}...v_{n}⟩} P {v_{1}...v_{n}/x_{1}...x_{n}}
out a: (S_{1}, .., S_{n}), v_{i}: S_{i}, Γ ⊢ \overline{a}⟨v_{1}...v_{2}⟩.P ⟶_{p}^{\overline{a}⟨v_{1}...v_{n}⟩} P
par  \frac{Γ ⊢ P ⟶_{p}^{l} P′ Γ ⊢ Q}{Γ ⊢ P | Q ⟶_{p}^{l} P′ | Q} (fn(l) ∩ fn(Q)) = ∅)
com  \frac{Γ ⊢ P ⟶_{p}^{(b̃) \overline{a}⟨v_{1}..v_{n}⟩} P′ Γ ⊢ Q ⟶_{p}^{a⟨v_{1}..v_{n}⟩} Q′}{Γ ⊢ P | Q ⟶_{p}^{τ} (b̃)(P′ | Q′)} (\{b̃\} ∩ fn(Q) = ∅)
res  \frac{Γ ⊢ P ⟶_{p}^{l} P′}{Γ\a ⊢ (a)P ⟶_{p}^{l} (a)P′} (a ∉ n(l))
open  \frac{Γ ⊢ P ⟶_{p}^{(b̃) \overline{a}⟨v_{1}..v_{n}⟩} P′}{Γ\c ⊢ (c)P ⟶^{(cb̃)\overline{a}⟨v_{1}..v_{n}⟩} Γ ⊢ P′} (c ≠ a, c ∈ (ṽ\b̃))
weak \frac{Γ_{1} ⊢ P ⟶_{p}^{l} Γ_{2} ⊢ P′ ∧ P ≡_{α} Q ∧ Γ_{i} ≍ Δ_{i} ∧ Γ_{1} ⊢ Q ∧ Γ_{2} ⊢ P′}{Δ_{1} ⊢ Q ⟶_{p}^{l} Δ_{2} ⊢ P′}

where we omit the symmetric version of com and par.