BRICS RS-98-26 Quaglia & Walker: On Encoding pπ in mπ BRICS

Basic Research in Computer Science

On Encoding pπ in mπ

Paola Quaglia David Walker BRICS Report Series RS-98-26 ISSN 0909-0878 October 1998 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1998, BRICS, Department of Computer Science

University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent BRICS Report Series publications. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK–8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@brics.dk

BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:

http://www.brics.dk
ftp://ftp.brics.dk

This document in subdirectory RS/98/26/

On encoding pπ in mπ

Paola Quaglia^{∗} ^{1} David Walker ^{2}

1 BRICS^{∗∗}, Aarhus University 2 Oxford University Computing Laboratory, U.K.

Abstract

This paper is about the encoding of pπ, the polyadic π-calculus, in mπ, the monadic π-calculus. A type system for mπ processes is introduced that captures the interaction regime underlying the encoding of pπ processes respecting a sorting. A full-abstraction result is shown: two pπ processes are typed barbed congruent iff their mπ encodings are monadic-typed barbed congruent.

1 Introduction

The π-calculus is a model of computation in which one can naturally express systems where the inter-connection structure among the parts changes during evolution. Its basic entities are names. They may be thought of as names of communication links. Processes, terms expressing systems, use names to interact, and pass names to one another by mentioning them in interactions. Names received by a process may be used and mentioned by it in further interactions.

In mπ, the monadic π-calculus [MPW92], an interaction between processes involves the transmission of a single name. In pπ, the polyadic π-calculus [Mil92], a tuple of names is passed in an interaction. As shown in [MPW92] atomic communication of tuples of names is expressible in the monadic calculus. Using standard notation (a reader unfamiliar with π-calculus may care to refer to Section 2) the key clauses in an inductively-defined translation [[·]] from polyadic processes to monadic processes are

[[x(z_{1} … z_{n}). P]] = x(w). w(z_{1}). . . . . w(z_{n}). [[P]]

and

[[\overline{x}⟨a_{1} … a_{n}⟩. Q]] = νw \overline{x}w. \overline{w}a_{1}. . . . . \overline{w}a_{n}. [[Q]]

where in each case w is a fresh name, i.e. is not free in the translated process. The transmission of a tuple a⃗ = a_{1} … a_{n} is expressed by

∗Funded by the EU, under the Marie Curie TMR Programme.

∗∗Basic Research in Computer Science, Centre of the Danish National Research Foundation.

[[x(z_{1} … z_{n}). P | \overline{x}⟨a_{1} … a_{n}⟩. Q]]
=  [[x(z_{1} … z_{n}). P]] | [[\overline{x}⟨a_{1} … a_{n}⟩. Q]]
⟶ νw (w(z_{1}). . . . . w(z_{n}). [[P]] | \overline{w}a_{1}. . . . . \overline{w}a_{n}. [[Q]])
⟶^{n} [[P]]{a⃗/z⃗} | [[Q]]
=  [[P {a⃗/z⃗} | Q]]

where z⃗ = z_{1} … z_{n}. Although communication of an n-tuple is represented using n + 1 interactions, it can be considered atomic since

νw (w(z_{1}). . . . . w(z_{n}). [[P]] | \overline{w}a_{1}. . . . . \overline{w}a_{n}. [[Q]]) ≈ [[P]]\{a⃗/z⃗\} | [[Q]]

where ≈ is (weak) barbed congruence. The first interaction creates a private link; the subsequent semantically-inert communications transfer the names a_{1} … a_{n} from sender to receiver via that link.

In the polyadic calculus there is a pressing need for some kind of typing discipline, as among the processes are terms – w(v). v(yz). 0 | \overline{w}⟨x⟩. \overline{x}⟨abc⟩. 0 is an example – where the components disagree on the length of the tuple to be passed – in the second communication in the example. Even on well-typed processes, however, the translation [[·]] is not fully abstract when barbed congruence is adopted as process equivalence. If P and Q are well-typed polyadic processes then the equivalence of [[P]] and [[Q]] implies that of P and Q, but the converse does not hold, the reason being, briefly, that there are monadic contexts that do not conform to the interaction regime that underlies the translation. A simple example is P = \overline{x}y. \overline{x}y. 0 and Q = \overline{x}y. 0 | \overline{x}y. 0: the monadic processes K[[[P]]] and K[[[Q]]] are not barbed bisimilar where K is the monadic context [·] | x(z). x(w). a(v). 0.

In this paper we introduce a typing system for monadic processes that captures the interaction regime underlying the translation, and use it to obtain a full-abstraction result. The following informal and incomplete account is filled out in the paper. Fix a set S of sorts and a polyadic sorting λ, a partial function from S to S^{+}, essentially of the kind introduced in [Mil92]. Write Ψ ⊢_{λ} P if P is well-typed under λ assuming its free names have the sorts recorded in Ψ, a finite partial function from names to S-sorts. Write P ≈_{λ} Q if P and Q are mutually well-typed and C[P] ≈^{·} C[Q] for every suitably well-typed context C, where ≈^{·} is barbed bisimilarity. We construct a set S^{m} of monadic sorts and a monadic sorting λ^{m} expressed using a graph. We give a typing system for inferring judgments of the form Ψ; Δ; Γ ⊢_{λ}^{m} M where M is a monadic process and Δ, Γ are finite partial functions from names to S^{m}-sorts. One property of the system is that Ψ ⊢_{λ} P iff Ψ; ∅; ∅ ⊢_{λ}^{m} [[P]]. As a guide, in a judgment Ψ′; Δ; Γ ⊢_{λ}^{m} M appearing in an inference of a judgment Ψ; ∅; ∅ ⊢_{λ}^{m} [[P]], the functions Δ and Γ will record the monadic sorts of the monadic names introduced in translating P that are free in M and that M may use immediately for receiving and for sending, respectively. The sort of name that M may receive or send via a monadic name w is determined by λ^{m}; in general, that sort changes from one use of w to the next. Using the typing system we define ≈_{λ}^{m} on monadic processes by setting M ≈_{λ}^{m} N if M and N are mutually well-typed in the monadic system and K[M] ≈^{·} K[N] for every suitably well-typed monadic context K. The main theorem is that if P and Q are well-typed polyadic processes then

P ≈_{λ} Q iff [[P]] ≈_{λ}^{m} [[Q]].

Thus the monadic typing system captures the interaction regime that underlies the polyadic-monadic translation. The main theorem is not easy to prove. The proof, however, sheds light on an important class of monadic processes, and several of the techniques used in it may be useful in other situations.

There has been much work on typing for π-calculus processes; a sample of papers is [Hon93, Kob97, KPT96, LW95, Mil92, NS97, PS93, PS97, San97, Tur96, VH93]. The work to which that presented here is most closely related is [Yos96]. We will explain the relationship at the end of the paper. In Section 2 we recall necessary background material, in Section 3 we introduce the typing system for monadic processes, and in Section 4 we prove the main theorem.

2 Background

In this section we recall necessary definitions and notations. We refer to the papers cited in the Introduction for further explanation and detailed proofs.

We presuppose a countably-infinite set of names, ranged over by lower-case letters. We write x⃗ for a tuple x_{1} … x_{n} of names.

The prefixes are given by

π ::= \overline{x}y⃗ | x(z⃗)

where y⃗ and z⃗ are nonempty and z⃗ is a tuple of distinct names.

The processes are given by

P ::= 0 | π. P | P | P′ | νz P | !P.

We write P for the set of processes; P, Q, R range over P.

A context is an expression obtained from a process by replacing an occurrence of ‘0’ by the hole [·]; C ranges over contexts. We write C[P] for the process obtained by replacing the occurrence of the hole in C by P.

We sometimes refer to processes and contexts collectively as terms and use T to range over terms. A term is monadic if for each subterm \overline{x}y⃗. T or x(y⃗). T of it, | y⃗ |= 1. We write M for the set of monadic processes; M, N, K range over M. Also, K, H range over monadic contexts.

In x(z⃗). P and in νz P the displayed occurrences of z⃗ and z are binding with scope P. An occurrence of a name in a term is free if it is not within the scope of a binding occurrence of the name. We write fn(P) for the set of names that have a free occurrence in P, and fn(P, Q, …) for fn(P) ∪ fn(Q) ∪ . . .. We write also bn(P) for the set of names that have a binding occurrence in P.

A substitution is a function on names that is the identity except on a finite set. We use θ to range over substitutions, and write xθ for θ applied to x. The support of θ, supp(θ), is {x | xθ ≠ x}, and the cosupport is cosupp(θ) = {xθ | x ∈ supp(θ)}. If supp(θ) = {x_{1}, …, x_{n}} and x_{i}θ = y_{i} for each i, we write {y^{1} … y^{n}/x_{1} … x_{n}} for θ. If X is a set of names we write Xθ for {xθ | x ∈ X}. We write P θ for the process obtained by replacing each free occurrence of each name x in P by xθ, with change of bound names to avoid captures.

We adopt the following conventions. We identify processes that differ only by change of bound names. Further, when considering a collection of processes and substitutions we tacitly assume that the free names of the processes are different from their bound names, that no name has more than one binding occurrence, and that no bound name is in the support or cosupport of any of the substitutions. This convention is referred to as the non-homonymy condition.

Definition 1 Structural congruence is the smallest congruence, ≡, on processes such that

1. P_{1} | (P_{2} | P_{3}) ≡ (P_{1} | P_{2}) | P_{3}, P_{1} | P_{2} ≡ P_{2} | P_{1}, P | 0 ≡ P

2. νz νw P ≡ νw νz P, νz 0 ≡ 0

3. νz (P_{1} | P_{2}) ≡ P_{1} | νz P_{2} provided z ∉ fn(P_{1})

4. !P ≡ P |!P.

An occurrence of one term in another is unguarded if it is not underneath a prefix.

Lemma 2 If P ≡ Q then P θ ≡ Qθ and fn(P) = fn(Q) and for each unguarded π. P′ in P there is an unguarded π. Q′ in Q with P′ ≡ Q′.

Proof: The assertions follow easily from the definitions. □

Definition 3 Intraaction is the smallest relation, ⟶, on processes such that

1. \overline{x}y⃗. P | x(z⃗). Q ⟶ P | Q\{y⃗/z⃗\} provided |y⃗ |=|z⃗ |

2. P ⟶ P′ implies P | Q ⟶ P′ | Q

3. P ⟶ P′ implies νz P ⟶ νz P′

4. P ≡ Q ⟶ Q′ ≡ P′ implies P ⟶ P′.

We write ⟹ for the reflexive and transitive closure of ⟶.

Lemma 4 If P ⟶ Q then fn(Q) ⊆ fn(P).

Proof: The proof is by induction on the inference of P ⟶ Q. It uses Lemma 2. □

In writing terms we assume composition associates to the left. Any intraaction arises from two complementary unguarded prefixes not underneath replications:

Lemma 5 If P ⟶ Q then P ≡ P′ = νw⃗ (\overline{x}y⃗. P_{1} | x(z⃗). P_{2} | P_{3}) where | y⃗ |=| z⃗ | and Q ≡ Q′ = νw⃗ (P_{1} | P_{2}{y⃗/z⃗} | P_{3}) and P′ ↦ Q′, i.e. P′ ⟶ Q′ may be inferred without use of the structural rule (rule 4).

Proof: The proof is by induction on the inference of P ⟶ Q. □

If x is a name then \overline{x} is a co-name. We use μ to range over names and co-names. The observability predicates, ↓_{μ}, are defined by: P ↓_{x} if P has an unguarded subterm

x(z⃗). Q and x ∈ fn(P); and P ↓\overline{x} if P has an unguarded subterm \overline{x}y⃗. Q and x ∈ fn(P). Further, ⇓_{μ} is ⟹↓_{μ}.

Lemma 6 The relations ↓_{μ} are closed under ≡, and P ↓_{x} iff P ≡ νw⃗ (x(z⃗). Q | Q′) where x ∉ w⃗, and P ↓\overline{x} iff P ≡ νw⃗ (\overline{x}y⃗. Q | Q′) where x ∉ w⃗.

Proof: The assertions follow easily from the definitions and Lemma 2. □

Definition 7 Barbed bisimilarity is the largest symmetric relation, ˙≈, such that if P ˙≈ Q then P ↓_{μ} implies Q ⇓_{μ}, and P ⟶ P′ implies Q ⟹ ˙≈ P′.

Definition 8 Monadic processes M and N are monadic barbed congruent, M ≈^{m} N, if K[M] ˙≈ K[N] for every monadic context K.

A simple but important observation is

Lemma 9 If w ∉ fn(M, N, y⃗) and y⃗ = y_{1} … y_{n} and z⃗ = z_{1} … z_{n}, then

νw (\overline{w}y_{1}. . . . . \overline{w}y_{n}. M | w(z_{1}). . . . . w(z_{n}). N) ≈^{m} M | N\{y⃗/z⃗\}.

Proof: The simplest way to prove this is to appeal to the account of process behaviour given by the labelled transition relations (which is not given in this paper). The two processes in question are clearly congruent and hence monadic barbed congruent.

Alternatively, consider the relation containing all pairs of processes of the forms

K[K_{1}, …, K_{m}] and K[K′_{1}, …, K′_{m}]

where K is an m-ary monadic context for some m ≥ 0, and for each i the process K_{i} is of the form

νw (\overline{w}y_{1}. . . . . \overline{w}y_{n}. M | w(z_{1}). . . . . w(z_{n}). N)

and the process K′_{i} of the form

M | N{y⃗/z⃗}

where K_{i} and K′_{i} satisfy the conditions of the lemma. It can be shown that this relation is a barbed bisimulation up to ≡. □

Definition 10 The translation [[·]] from terms to monadic terms is defined as follows:

\begin{aligned}[[\overline{x}⟨y_{1} … y_{n}⟩. T]] & = & νw \overline{x}w. \overline{w}y_{1}. . . . . \overline{w}y_{n}. [[T]] \\ [[x(z_{1} … z_{n}). T]] & = & x(w). w(z_{1}). . . . . w(z_{n}). [[T]] \end{aligned}

and [[[·]]] = [·], [[0]] = 0, [[T | T′]] = [[T]] | [[T′]], [[νz T]] = νz [[T]], and [[ !T]] = ![[T]].

The translation enjoys the following properties.

Lemma 11 fn([[P]]) = fn(P) and [[P θ]] = [[P]]θ.

Proof: The proof is by induction on the structure of P. □

Lemma 12 If P ≡ Q then [[P]] ≡ [[Q]].

Proof: The assertion follows directly from the definitions. □

Lemma 13 P ↓_{μ} iff [[P]] ↓_{μ}.

Proof: The proof is by induction on the structure of P. □

Lemma 14 If P ⟶ Q then [[P]] ⟶ M ⟹ [[Q]] with M ≈^{m} [[Q]].

Proof: The proof uses Lemmas 5, 9, 11, and 12. □

We now consider typing of polyadic processes. Fix a set S of sorts, ranged over by s, t, and a sorting λ : S ⇀ S^{+}.

We use Ψ to range over finite partial functions from names to sorts. We write n(Ψ) for the domain of Ψ. If n(Ψ) = {x_{1}, …, x_{n}} and Ψ(x_{i}) = s_{i} for each i, we write {x_{1} : s_{1}, …, x_{n} : s_{n}} for Ψ. We write Ψ(x) ≃ s to mean ‘if x ∈ n(Ψ) then Ψ(x) = s’. Ψ and Ψ′ are compatible if x ∈ n(Ψ) ∩ n(Ψ′) implies Ψ(x) = Ψ′(x). If Ψ and Ψ′ are compatible we write Ψ, Ψ′ for Ψ ∪ Ψ′, and we abbreviate Ψ, {x : s} to Ψ, x : s. We write Ψθ for {xθ : s | x : s ∈ Ψ}. We say θ respects Ψ if x, y ∈ n(Ψ) and xθ = yθ implies Ψ(x) = Ψ(y).

Definition 15 P is a λ-process if Ψ ⊢ P may be inferred for some Ψ using the rules in Table 1, where the side conditions are

1. z ∉ n(Ψ),

2. λ(s) = (t_{1} … t_{n}), Ψ(x) ≃ s, Ψ(y_{i}) ≃ t_{i}, x = y_{i} implies s = t_{i}, and y_{i} = y_{j} implies t_{i} = t_{j},

3. λ(s) = (t_{1} … t_{n}), Ψ(x) ≃ s, and z_{i} ∉ n(Ψ).

Ψ ⊢ 0  {Ψ ⊢ P \atop Ψ ⊢!P}  {Ψ ⊢ P_{1} Ψ ⊢ P_{2} \atop Ψ ⊢ P_{1} | P_{2}}  Ψ, z : s ⊢ P ; (1) ; Ψ ⊢ νz P

Ψ ⊢ P

(2)

Ψ, x : s, y_{1} : t_{1}, …, y_{n} : t_{n} ⊢ \overline{x}⟨y_{1} … y_{n}⟩. P

Ψ, z_{1} : t_{1}, …, z_{n} : t_{n} ⊢ P

(3)

Ψ, x : s ⊢ x(z_{1} … z_{n}). P

Table 1: The polyadic typing rules

The type system enjoys the following properties.

Lemma 16 If Ψ ⊢ P then fn(P) ⊆ n(Ψ) and bn(P) ∩ n(Ψ) = ∅. Proof: The proof is by induction on the inference of Ψ ⊢ P. □ In view of the last assertion, when we write a judgment Ψ ⊢ P we tacitly assume that the bound names of P are chosen not to be in n(Ψ). Lemma 17 If Ψ ⊢ P and n(Ψ′) ∩ n(Ψ) = ∅, then Ψ, Ψ′ ⊢ P. Proof: The proof is by induction on the inference of Ψ ⊢ P. □ Lemma 18 If Ψ ⊢ P and Ψ′ ⊆ Ψ and fn(P) ⊆ n(Ψ′), then Ψ′ ⊢ P. Proof: The proof is by induction on the inference of Ψ ⊢ P. □ Lemma 19 If Ψ ⊢ P and Q ≡ P, then Ψ ⊢ Q. Proof: The assertion follows from the definitions using Lemmas 17 and 18. □ Lemma 20 If Ψ ⊢ P and θ respects Ψ, then Ψθ ⊢ P θ. Proof: The proof is by induction on the inference of Ψ ⊢ P. □ Lemma 21 If Ψ ⊢ P and P ⟶ P′, then Ψ ⊢ P′. Proof: The assertion follows from the definitions using Lemmas 19 and 20. □ Lemma 22 If P is a λ-process and P ⟹ Q ≡ νw⃗(\overline{x}y⃗. Q_{1} | x(z⃗). Q_{2} | Q_{3}), then |y⃗ |=|z⃗ |. Proof: The assertion follows from the definitions and Lemma 21. □

We write Ψ ⊢ P, Q if Ψ ⊢ P and Ψ ⊢ Q. The rules for typing contexts are like the rules for typing processes, with the addition of the rule: Ψ ⊢ [·] for any Ψ. A context C is a λ(Ψ)-context if using the rule-instance Ψ ⊢ [·] we can infer Ψ′ ⊢ C for some Ψ′. If Ψ ⊢ P and C is a λ(Ψ)-context, then C[P] is a λ-process. Definition 23 P and Q are barbed λ-congruent, P ≈_{λ} Q, if there is Ψ such that Ψ ⊢ P, Q and C[P] ˙≈ C[Q] for every λ(Ψ)-context C.

3 The monadic type system

We now introduce the monadic type system and establish some of its properties. Fix a set S of sorts and a sorting λ.

Definition 24 The set of m-sorts, ranged over by σ, τ, is

S^{m} = {∘, •} ∪ {s^{i} | 1 ≤ i ≤ |λ(s)|, s ∈ S}.

For example, if S = {s, t, r} and λ(s) = (t r), λ(t) = (s) and λ(r) = (r), then S^{m} = {∘, •, s^{1}, s^{2}, t^{1}, r^{1}}.

Definition 25 The labelled directed graph G_{λ} has nodes S^{m}, labels S, and arrows

∘ ⟶^{s} s^{1} ⟶^{t_{1}} s^{2} ⟶^{t_{2}} … ⟶^{t_{n−1}} s^{n} ⟶^{t_{n}} •

if λ(s) = (t_{1} … t_{n}).

For the example sorting above the arrows are

∘ ⟶^{s} s^{1} ⟶^{t} s^{2} ⟶^{r} • and ∘ ⟶^{t} t^{1} ⟶^{s} • and ∘ ⟶^{r} r^{1} ⟶^{r} •.

We use Δ, Γ to range over finite partial functions from names to S^{m} − {•}, and use analogous notations to those mentioned earlier in connection with functions Ψ.

The following notion will be important in typing compositions.

Definition 26 Suppose Δ_{1} and Γ_{1} are compatible, and Δ_{2} and Γ_{2} are compatible. Then Δ_{1}, Γ_{1} and Δ_{2}, Γ_{2} are complementary if n(Δ_{1})∩n(Δ_{2}) = ∅, n(Γ_{1})∩n(Γ_{2}) = ∅, and Δ_{1}, Δ_{2} and Γ_{1}, Γ_{2} are compatible.

Definition 27 A monadic process M is a λ^{m}-process if Ψ; Δ; Γ ⊢ M may be inferred for some Ψ, Δ, Γ using the rules in Table 2.

We write ⟨Ψ; Δ; Γ ⊢ M⟩ for an inference of the judgment Ψ; Δ; Γ ⊢ M. We say w is monadic in ⟨Ψ; Δ; Γ ⊢ M⟩ if for some judgment Ψ′; Δ′; Γ′ ⊢ M′ in ⟨Ψ; Δ; Γ ⊢ M⟩ we have w ∈ n(Δ′, Γ′).

In the premises of the rules for prefixes, {w : •} is read as ∅. This saves writing, as illustrated in the root of the left branch of the following sample inference, where ∅; ∅; ∅ ⊢ 0 stands for ∅; ∅; {w : •} ⊢ 0.

Note that in the rules for input prefix, z ≠ x by the convention on free and bound names.

The rules are best understood via an example. Assuming the example sorting above, let P = !νa (Q | R) where Q = \overline{a}⟨bc⟩. 0 and R = a(uv). 0. Then

[[P]] = !νa ((νw \overline{a}w. \overline{w}b. \overline{w}c. 0) | a(z). z(u). z(v). 0)

and we have, in full,

nil Ψ; ∅; ∅ ⊢ 0

out_{1} \begin{matrix}Ψ; ∅; \{y : σ\} ⊢ M \\ Ψ, x : s; ∅; \{y : ∘\} ⊢ \overline{x}y. M \end{matrix} ∘ ⟶^{s} σ and Ψ(x) ≃ s and y ∉ n(Ψ, x)

out_{2} \begin{matrix}Ψ; ∅; \{x : τ\} ⊢ M \\ Ψ, y : s; ∅; \{x : σ\} ⊢ \overline{x}y. M \end{matrix} ∘ ≠ σ ⟶^{s} τ and Ψ(y) ≃ s and x ∉ n(Ψ, y)

inp_{1} \begin{matrix}Ψ; \{z : σ\}; ∅ ⊢ M \\ Ψ, x : s; ∅; ∅ ⊢ x(z). M \end{matrix} ∘ ⟶^{s} σ and Ψ(x) ≃ s and z ∉ n(Ψ)

inp_{2} \begin{matrix}Ψ, z : s; \{x : τ\}; ∅ ⊢ M \\ Ψ; \{x : σ\}; ∅ ⊢ x(z). M \end{matrix} ∘ ≠ σ ⟶^{s} τ and x, z ∉ n(Ψ)

par Ψ; Δ_{1}; Γ_{1} ⊢ M_{1}  Ψ; Δ_{2}; Γ_{2} ⊢ M_{2} Ψ; Δ_{1}, Δ_{2}; Γ_{1}, Γ_{2} ⊢ M_{1} | M_{2} Δ_{1}, Γ_{1} and Δ_{2}, Γ_{2} are complementary

res_{1} \begin{matrix}Ψ, z : s; Δ; Γ ⊢ M \\ Ψ; Δ; Γ ⊢ νz M \end{matrix} z ∉ n(Ψ, Δ, Γ) res_{2} \begin{matrix}Ψ; Δ; Γ, z : ∘ ⊢ M \\ Ψ; Δ; Γ ⊢ νz M \end{matrix} z ∉ n(Ψ, Δ, Γ)

res_{3} \begin{matrix}Ψ; Δ, z : σ; Γ, z : σ ⊢ M \\ Ψ; Δ; Γ ⊢ νz M \end{matrix} z ∉ n(Ψ, Δ, Γ) and σ ≠ ∘  rep \begin{matrix}Ψ; ∅; ∅ ⊢ M \\ Ψ; ∅; ∅ ⊢!M \end{matrix}

Table 2: The monadic typing rules

\begin{matrix}\begin{matrix}∅; ∅; ∅ ⊢ 0 \\ \{c : r\}; ∅; \{w : s^{2}\} ⊢ \overline{w}c. 0 \end{matrix} ; \{b : t, c : r\}; ∅; \{w : s^{1}\} ⊢ \overline{w}b. \overline{w}c. 0 ; \{a : s, b : t, c : r\}; ∅; \{w : ∘\} ⊢ \overline{a}w. \overline{w}b. \overline{w}c. 0 ; \{a : s, b : t, c : r\}; ∅; ∅ ⊢ [[Q]] & \begin{matrix}\{u : t, v : r, b : t, c : r\}; ∅; ∅ ⊢ 0 \\ \{u : t, b : t, c : r\}; \{z : s^{2}\}; ∅ ⊢ z(v). 0 \end{matrix} ; \{b : t, c : r\}; \{z : s^{1}\}; ∅ ⊢ z(u). z(v). 0 ; \{a : s, b : t, c : r\}; ∅; ∅ ⊢ [[R]] \\ \{a : s, b : t, c : r\}; ∅; ∅ ⊢ [[Q]] | [[R]] \end{matrix} ; \{b : t, c : r\}; ∅; ∅ ⊢ νa ([[Q]] | [[R]]) ; \{b : t, c : r\}; ∅; ∅ ⊢ [[P]]

Note that in the judgment

\{a : s, b : t, c : r\}; ∅; \{w : ∘\} ⊢ \overline{a}w. \overline{w}b. \overline{w}c. 0

the name w is recorded in the Γ-component with m-sort ∘, and that the second of the restriction rules is applied to infer

{a : s, b : t, c : r}; ∅; ∅ ⊢ [[Q]].

In the judgment

\{b : t, c : r\}; ∅; \{w : s^{1}\} ⊢ \overline{w}b. \overline{w}c. 0

w is ascribed m-sort s^{1}, indicating that the process can immediately send on w. The graph G_{λ} stipulates that the name which can be sent via w must be of sort t. In the judgment

\{c : r\}; ∅; \{w : s^{2}\} ⊢ \overline{w}c. 0

w has m-sort s^{2} and c sort r as given by G_{λ}. After being used for sending for the second and last time, w disappears from the Γ-component.

In a complementary way, m-sorts are ascribed to z in the Δ-components of the judgments involving subterms of R to indicate how they use the name for receiving.

We now state some properties of the type system.

Lemma 28 Suppose Ψ; Δ; Γ ⊢ M. Then

1. Δ and Γ are compatible.

2. n(Ψ) ∩ n(Δ, Γ) = ∅.

3. fn(M) ⊆ n(Ψ, Δ, Γ).

4. n(Δ, Γ) ⊆ fn(M).

5. ∘ ∉ cosupp(Δ).

6. Γ(x) = ∘ implies x ∉ n(Δ).

7. bn(M) ∩ n(Ψ, Δ, Γ) = ∅.

Proof: All the items are proved by induction on the derivation of Ψ; Δ; Γ ⊢ M. Each rule is considered in turn as the last rule applied. Only a few issues are worth commenting on.

• The proof of (2), relatively to the prefix cases, appeals to the side conditions of the corresponding rules.

• In the proof of (6), the case of the par rule is carried out as follows. Suppose that Ψ; Δ; Γ ⊢ M_{1} | M_{2} with x : ∘ ∈ Γ. Assume that x ∈ n(Δ). Then, from Δ and Γ compatible, it follows x : ∘ ∈ Δ. Absurd by (5).

• As for the proof of (7), by (4) and the non-homonymy condition it is sufficient to prove that bn(M) ∩ n(Ψ) = ∅.

□

In view of the last part, when we write a judgment Ψ; Δ; Γ ⊢ M we tacitly assume that the bound names of M are chosen not to be in n(Ψ, Δ, Γ).

We write | T | for the number of operators in the term T. The reason the following lemma takes the form it does is that to carry out later arguments by induction on type inference, a handle on the size of terms is needed.

Lemma 29 If Ψ; Δ; Γ ⊢ M then there is M′ ≡ M such that | M′ | ≤ | M | and:

1. If w : ∘ ∈ Γ then M′ = νw⃗ \overline{x}w. N or M′ = νw⃗ (\overline{x}w. N | K) where w ∉ w⃗.

2. If w : σ ∈ Γ and σ ≠ ∘, then M′ = νw⃗ \overline{w}x. N or M′ = νw⃗ (\overline{w}x. N | K) where w ∉ w⃗.

3. If w : σ ∈ Δ then M′ = νw⃗ w(z). N or M′ = νw⃗ (w(z). N | K) where w ∉ w⃗.

4. If w : σ ∈ Δ∩Γ then M′ = νw⃗(\overline{w}x. N | w(z). N′) or M′ = νw⃗(\overline{w}x. N | w(z). N′ | K) where w ∉ w⃗.

Proof: The proof of the four items is by simulataneous induction on the derivation of Ψ; Δ; Γ ⊢ M. We show in the following the case when the last rule applied is the par rule. The other cases are easier.

[par] M = M_{1} | M_{2} and Ψ; Δ_{j}; Γ_{j} ⊢ M_{j} with Δ_{1} ∪ Δ_{2} = Δ and Γ_{1} ∪ Γ_{2} = Γ and Δ_{1}, Γ_{1} and Δ_{2}, Γ_{2} complementary.

1. As n(Γ_{1}) ∩ n(Γ_{2}) = ∅, from w : ∘ ∈ Γ it follows that w : ∘ ∈ Γ_{i} and w : ∘ ∉ Γ_{j} for i ≠ j. Let us assume i = 1. Then w : ∘ ∈ Γ_{1} and by inductive hypothesis (1) there is some M′_{1} ≡ M_{1} such that | M′_{1} | ≤ | M_{1} | and either M′_{1} = νw⃗ \overline{x}w. N or M′_{1} = νw⃗ (\overline{x}w. N | K) where w ∉ w⃗. Note that by the non-homonymy condition we can assume w⃗ ∉ fn(M_{2}). Then:

• If M′_{1} = νw⃗ \overline{x}w. N set M′ = νw⃗ (\overline{x}w. N | M_{2}).

• If M′_{1} = νw⃗ (\overline{x}w. N | K) set M′ = νw⃗ (\overline{x}w. N | (K | M_{2})).

In both cases M′ ≡ M′_{1} | M_{2} ≡ M and | M′ | ≤ | M |.

2. If w : σ ∈ Γ with σ ≠ ∘ then the proof is analogous to the above case. It only requires appealing to the inductive hypothesis (2) rather than to the inductive hypothesis (1).

3. If w : σ ∈ Δ then from n(Δ_{1})∩n(Δ_{2}) = ∅ it follows that w : σ ∈ Δ_{i} and w : σ ∉ Δ_{j}. Then the thesis follows from inductive hypothesis (3), analogously to the proof of (1).

4. From n(Δ_{1})∩n(Δ_{2}) = ∅ and the hypothesis w : σ ∈ Δ∩Γ it follows that w ∈ n(Δ_{i}) and w ∉ n(Δ_{j}) for i ≠ j. Analogously, w ∈ n(Γ_{h}) and w ∉ n(Γ_{k}) for h ≠ k, from n(Γ_{1}) ∩ n(Γ_{2}) = ∅. Note that σ ≠ ∘ from w ∈ n(Δ) and Lemma 28(5). We distinguish two cases depending on whether or not i = h.

• Suppose w ∈ n(Δ_{i}) ∩ n(Γ_{i}) and set, say, i = 1. Then by inductive hypothesis (4) there is M′_{1} ≡ M_{1} such that | M′_{1} | ≤ | M_{1} | and either M′_{1} = νw⃗(\overline{w}x. N | w(z). N′) or M′_{1} = νw⃗ (\overline{w}x. N | w(z). N′ | K). Note that in either case we can assume w⃗ ∉ fn(M_{2}). Then:

– If M′_{1} = νw⃗ (\overline{w}x. N | w(z). N′) set M′ = νw⃗ (\overline{w}x. N | w(z). N′ | M_{2}).

– If M′_{1} = νw⃗ (\overline{w}x. N | w(z). N′ | K) set M′ = νw⃗ (\overline{w}x. N | w(z). N′ | K | M_{2}).

In each of the above cases M′ ≡ M′_{1} | M_{2} ≡ M and | M′ | ≤ | M |.

• Suppose now that w ∈ n(Δ_{i}) ∩ n(Γ_{j}) and that i = 1. Then by inductive hypothesis (2) and inductive hypothesis (3) there are M′_{1} ≡ M_{1} and M′_{2} ≡ M_{2} such that | M′_{1} | ≤ | M_{1} | and | M′_{2} | ≤ | M_{2} | and

M′_{1} = νw⃗_{1} w(z). N_{1}  or  M′_{1} = νw⃗_{1} (w(z). N_{1} | K_{1})
M′_{2} = νw⃗_{2} \overline{w}x. N_{2}  or  M′_{2} = νw⃗_{2} (\overline{w}x. N_{2} | K_{2})

where w ∉ w⃗_{1}, w⃗_{2} and we can assume w⃗_{1} ∉ fn(M′_{2}) and w⃗_{2} ∉ fn(M′_{1}). Then, analogously to the previous cases for each of the possible four combinations we can find M′ so that M′ ≡ M′_{1} | M′_{2} ≡ M and | M′ | ≤ | M |.

□

Lemma 30 If Ψ; Δ; Γ ⊢ M and Ψ′ ⊆ Ψ and n(Ψ) ∩ fn(M) ⊆ n(Ψ′), then Ψ′; Δ; Γ ⊢ M.

Proof: By induction on the derivation of Ψ; Δ; Γ ⊢ M. □

Lemma 31 If Ψ; Δ; Γ ⊢ M and n(Ψ′) ∩ n(Ψ; Δ; Γ) = ∅, then Ψ, Ψ′; Δ; Γ ⊢ M.

Proof: By induction on the derivation of Ψ; Δ; Γ ⊢ M. □

Typing is, as would be expected, invariant under structural congruence:

Lemma 32 If Ψ; Δ; Γ ⊢ M and N ≡ M, then Ψ; Δ; Γ ⊢ N.

Proof: Note that M ≡ N iff M ≡_{1}^{∗} N, where M′ ≡_{1} N′ if there are a context K and processes M′′, N′′ comprising an instance of one of the axioms of structural congruence such that M′ = K[M′′] and N′ = K[N′′].

The proof is by induction on the length of the proof M = N_{1} ≡_{1} N_{2} ≡_{1} … ≡_{1} N_{n} = N. The inductive base is void, since M = N. As for the inductive step:

Assuming Ψ; Δ; Γ ⊢ N_{n−1} we show that N_{n−1} ≡_{1} N_{n} implies Ψ; Δ; Γ ⊢ N_{n}.

In the case when N_{n−1} = K[N′_{n−1}] ≡_{1} K[N′_{n}] = N_{n} and N′_{n−1} ≡_{1} N′_{n} is an instance of one of the axioms in Def. 1, the statement is a consequence of the following lemma:

Lemma 33 If Ψ; Δ; Γ ⊢ K with Ψ′; Δ′; Γ′ ⊢ [·] and Ψ′; Δ′; Γ′ ⊢ M then Ψ; Δ; Γ ⊢ K[M].

Proof: By induction on the structure of K. □

It remains to show that the statement holds when N_{n−1} ≡_{1} N_{n} is itself an axiom instance. We work out the most interesting cases. Those omitted do not present difficulties.

[νz (M_{1} | M_{2}) ≡ (M_{1} | νz M_{2}) provided z ∉ fn(M_{1})] We distinguish three cases depending on the last typing rule applied to derive

Ψ; Δ; Γ ⊢ N_{n−1} = νz (M_{1} | M_{2}).

Note that in each case z ∉ n(Ψ, Δ, Γ).

- [res_{1}] In this case we have: Ψ, z : s; Δ; Γ ⊢ M_{1} | M_{2} and Ψ, z : s; Δ_{j}; Γ_{j} ⊢ M_{j} with Δ_{1} ∪ Δ_{2} = Δ and Γ_{1} ∪ Γ_{2} = Γ. Then from z ∉ fn(M_{1}) and Lemma 30:

Ψ; Δ_{1}; Γ_{1} ⊢ M_{1} Ψ, z : s; Δ_{2}; Γ_{2} ⊢ M_{2}

with z ∉ n(Ψ, Δ_{2}, Γ_{2}). Hence the thesis by res_{1} and par.

- [res_{2}] From typing: Ψ; Δ; Γ, z : ∘ ⊢ M_{1} | M_{2} and Ψ; Δ_{j}; Γ_{j} ⊢ M_{j} with Δ_{1} ∪ Δ_{2} = Δ and Γ_{1} ∪ Γ_{2} = Γ ∪ {z : ∘}. Note that it cannot be that z ∈ n(Γ_{1}) because this, by Lemma 28(4), would contradict the hypothesis z ∉ fn(M_{1}). Then:

Ψ; Δ_{1}; Γ_{1} ⊢ M_{1} Ψ; Δ_{2}; Γ′_{2}, z : ∘ ⊢ M_{2}

with z ∉ n(Ψ, Δ_{2}, Γ′_{2}). Hence the thesis by res_{2} and par.

- [res_{3}] Now we have: Ψ; Δ, z : σ; Γ, z : σ ⊢ M_{1} | M_{2} and Ψ; Δ_{j}; Γ_{j} ⊢ M_{j} with Δ_{1} ∪ Δ_{2} = Δ ∪ {z : σ} and Γ_{1} ∪ Γ_{2} = Γ ∪ {z : σ}. Note that z ∈ n(Δ_{2}) ∩ n(Γ_{2}). In fact from z ∉ fn(M_{1}) and Lemma 28(4), it follows that z ∉ n(Δ_{1}, Γ_{1}). Hence:

Ψ; Δ_{1}; Γ_{1} ⊢ M_{1} Ψ; Δ′_{2}, z : σ; Γ′_{2}, z : σ ⊢ M_{2}

with z ∉ n(Ψ, Δ′_{2}, Γ′_{2}). Then the thesis by res_{3} and par.

[(M_{1} | νz M_{2}) ≡ νz (M_{1} | M_{2}) provided z ∉ fn(M_{1})] Here we assume that:

Ψ; Δ; Γ ⊢ N_{n−1} = M_{1} | νz M_{2}

and show that Ψ; Δ; Γ ⊢ νz (M_{1} | M_{2}). From typing we have:

Ψ; Δ_{1}; Γ_{1} ⊢ M_{1} Ψ; Δ_{2}; Γ_{2} ⊢ νz M_{2}

with Δ_{1} ∪ Δ_{2} = Δ and Γ_{1} ∪ Γ_{2} = Γ and z ∉ n(Ψ, Δ_{2}, Γ_{2}). Note that z ∉ n(Δ_{1}, Γ_{1}) from z ∉ fn(M_{1}) and Lemma 28(4). In the cases when the last rule applied to infer Ψ; Δ_{2}; Γ_{2} ⊢ νzM_{2} is either res_{2} or res_{3}, i.e. it is either Ψ; Δ_{2}; Γ_{2}, z : ∘ ⊢ M_{2} or Ψ; Δ_{2}, z : σ; Γ_{2}, z : σ ⊢ M_{2}, the thesis is an immediate consequence of the above observation. So, the most interesting case to deal with is when the last rule applied to type νz M_{2} is res_{1} and hence: Ψ, z : s; Δ_{2}; Γ_{2} ⊢ M_{2}. In that case, from the hypothesis z ∉ fn(M_{1}) and Lemma 31 we get: Ψ, z : s; Δ_{1}; Γ_{1} ⊢ M_{1}. Then Ψ, z : s; Δ_{1}, Δ_{2}; Γ_{1}, Γ_{2} ⊢ M_{1} | M_{2} and hence the thesis. □

The final result in this section shows how typing changes under intraaction. To prove the lemma it is necessary to examine the effects of substitution on typing.

Lemma 34 If Ψ; Δ; Γ ⊢ M and θ = {y/z} and y, z ∉ n(Δ, Γ) and θ respects Ψ, then Ψθ; Δ; Γ ⊢ Mθ.

Proof: By induction on the derivation of Ψ; Δ; Γ ⊢ M. Each typing rule is considered in turn as the last rule applied. We report in the following the most interesting cases.

[nil] M = 0 then Mθ = M and Ψθ; ∅; ∅ ⊢ Mθ where Ψθ = Ψ if z ∉ n(Ψ) and Ψθ = Ψ′ ∪ {y : s} if Ψ = Ψ′ ∪ {z : s}.

[out_{1}] M = \overline{x}w. M′ and Ψ = Ψ′ ∪ \{x : s\} for s such that ∘ ⟶^{s} σ and

Ψ′, x : s; ∅; \{w : ∘\} ⊢ \overline{x}w. M′ Ψ′; ∅; \{w : σ\} ⊢ M′

with Ψ′(x) ≃ s and w ∉ n(Ψ′, x). Note that w ≠ z, y from the hypothesis y, z ∉ n(Δ, Γ). Then Mθ = \overline{xθ}w. M′θ. By inductive hypothesis:

Ψ′θ; ∅; {w : σ} ⊢ M′θ

Moreover Ψ′θ(xθ) ≃ s from Ψ′θ(xθ) = Ψ′(x), and w ∉ n(Ψ′θ, xθ) ⊆ n(Ψ′, y, x) from w ∉ n(Ψ′, x) and w ≠ y. Then from out_{1}:

Ψ′θ, xθ : s; ∅; \{w : ∘\} ⊢ Mθ = \overline{xθ}w. M′θ

[out_{2}] M = \overline{x}w. M′ and Ψ = Ψ′ ∪ \{w : s\} for s such that ∘ ≠ σ ⟶^{s} τ and

Ψ′, w : s; ∅; \{x : σ\} ⊢ \overline{x}w. M′ Ψ′; ∅; \{x : τ\} ⊢ M′

with Ψ′(w) ≃ s and x ∉ n(Ψ′, w). Note that x ≠ z, y, so Mθ = \overline{x}wθ. M′θ and by inductive hypothesis:

Ψ′θ; ∅; {x : τ} ⊢ M′θ

We have also: Ψ′θ(wθ) = Ψ′(w) ≃ s, and x ∉ n(Ψ′θ, wθ) ⊆ n(Ψ′, y, w) from x ∉ n(Ψ′, w) and x ≠ y. Then from out_{2}:

Ψ′θ, wθ : s; ∅; \{x : σ\} ⊢ Mθ = \overline{x}wθ. M′θ

[inp_{1}] M = x(w). M′ and Ψ = Ψ′ ∪ {x : s} for s such that ∘ ⟶^{s} σ and

Ψ′, x : s; ∅; ∅ ⊢ x(w). M′ Ψ′; {w : σ}; ∅ ⊢ M′

with Ψ′(x) ≃ s and w ∉ n(Ψ′). Note that we can assume w ≠ y, z. In fact, if w = z then from the non-homonymy condition z ∉ fn(M′), hence Mθ = M. On the other hand, if w = y then w is renamed into a fresh w′ in Mθ = xθ(w′). M′{w′/w}{w/z} in order to avoid captures. From w ≠ y, z and Ψ′; {w : σ}; ∅ ⊢ M′ we deduce by inductive hypothesis:

Ψ′θ; {w : σ}; ∅ ⊢ M′θ

It also holds: Ψ′θ(xθ) = Ψ′(x) ≃ s, and w ∉ n(Ψ′θ) ⊆ n(Ψ′, y). Hence:

Ψ′θ, xθ : s; ∅; ∅ ⊢ Mθ = xθ(w). M′θ

[inp_{2}] M = x(w). M′ and

Ψ; {x : σ}; ∅ ⊢ x(w). M′ Ψ, w : s; {x : τ}; ∅ ⊢ M′

for s such that ∘ ≠ σ ⟶^{s} τ and with x, w ∉ n(Ψ). As in the above case we can assume w ≠ y, z. Also note that by hypothesis y, z ≠ x. Then Mθ = x(w). M′θ and by inductive hypothesis:

Ψθ, w : s; {x : τ}; ∅ ⊢ M′θ

with x, w ∉ n(Ψθ) ⊆ n(Ψ, y) from x, w ∉ n(Ψ) and x ≠ y and w ≠ y. Hence from inp_{2}:

Ψθ; {x : σ}; ∅ ⊢ Mθ = x(w). M′θ

[par] M = M_{1} | M_{2} and Δ = Δ_{1}∪Δ_{2}, Γ = Γ_{1}∪Γ_{2} with Δ_{1}, Γ_{1} and Δ_{2}, Γ_{2} complementary and Ψ; Δ_{j}; Γ_{j} ⊢ M_{j}. Note that y, z ∉ n(Δ_{j}, Γ_{j}) from the hypothesis y, z ∉ n(Δ, Γ). Then by inductive hypothesis: Ψθ; Δ_{j}; Γ_{j} ⊢ M_{j}θ and hence: Ψθ; Δ; Γ ⊢ Mθ = M_{1}θ | M_{2}θ. □

Lemma 35 If Ψ; Δ; Γ ⊢ M and θ = {y/z} and z : σ ∈ Δ and z ∉ n(Γ) and y ∉ n(Ψ, Δ) and (y : τ ∈ Γ implies σ = τ), then Ψ; Δθ; Γ ⊢ Mθ.

Proof: By induction on the derivation of Ψ; Δ; Γ ⊢ M.

[inp_{2}] M = z(w). M′ and

Ψ; {z : σ}; ∅ ⊢ z(w). M′ Ψ, w : s; {z : τ}; ∅ ⊢ M′

for s such that ∘ ≠ σ ⟶^{s} τ and with z, w ∉ n(Ψ). Note that y ∉ n(Ψ, z) by hypothesis. We can also assume y, z ≠ w (for details see the inp_{1} case of the proof of Lemma 34). Then Mθ = zθ(w). M′θ = y(w). M′θ and by y ∉ n(Ψ, w, z) and inductive hypothesis:

Ψ, w : s; {y : τ}; ∅ ⊢ M′θ

Since y, w ∉ n(Ψ), from inp_{2} we have:

Ψ; {y : σ}; ∅ ⊢ Mθ = y(w). M′θ

[par] M = M_{1} | M_{2} and Δ = Δ_{1}∪Δ_{2}, Γ = Γ_{1}∪Γ_{2} with Δ_{1}, Γ_{1} and Δ_{2}, Γ_{2} complementary and

Ψ; Δ_{j}; Γ_{j} ⊢ M_{j}

From z : σ ∈ Δ and the complementarity condition it follows that z ∈ n(Δ_{i}) and z ∉ n(Δ_{j}) with i ≠ j. Moreover z ∉ n(Ψ) by Lemma 28(2). Then z ∉ fn(M_{j}) from z ∉ n(Γ) and Lemma 28(3). Hence Mθ ≡ M_{i}θ | M_{j}. By inductive hypothesis:

Ψ; Δ_{i}θ; Γ_{i} ⊢ M_{i}θ

Note that Δ_{i}θ, Γ_{i} and Δ_{j}, Γ_{j} are complementary. In fact:

• n(Δ_{i}θ) ∩ n(Δ_{j}) ⊆ n(Δ_{i}, y) ∩ n(Δ_{j}) = {y} ∩ n(Δ_{j}) = ∅ from y ∉ n(Δ);

• Δ_{i}θ, Δ_{j} and Γ_{i} ∪ Γ_{j} are compatible from the hypothesis that y : τ ∈ Γ implies

σ = τ. Hence we have:

Ψ; Δ_{i}θ, Δ_{j}; Γ_{i}, Γ_{j} ⊢ M_{i}θ | M_{j}

[res_{1}, res_{2}, res_{3}] M = νwM′. As for the above input prefix case we can assume z, y ≠ w. Hence in each of the three cases for restriction the thesis is an immediate consequence of the inductive hypothesis. □

Lemma 36 If Ψ; Δ; Γ ⊢ M and M ⟶ M′, then Ψ; Δ′; Γ′ ⊢ M′ where 1. Δ′ = Δ and Γ′ = Γ, or

2. Δ′ = Δ ∪ {y : σ} and Γ′ = Γ − {y : ∘} ∪ {y : σ} where y : ∘ ∈ Γ and ∘ ⟶^{s} σ, or 3. Δ′ = Δ − {y : σ} ∪ {y : τ} and Γ′ = Γ − {y : σ} ∪ {y : τ} where y : σ ∈ Δ ∩ Γ and

∘ ≠ σ ⟶^{s} τ.

Proof: From the hypothesis that Ψ; Δ; Γ ⊢ M ⟶ M′ and Lemma 5, we have:

\begin{aligned}M & ≡ & νw⃗ N & = & νw⃗ (\overline{x}y. M_{1} | x(z). M_{2} | M_{3}) \\ M′ & ≡ & νw⃗ N′ & = & νw⃗ (M_{1} | M_{2}\{y/z\} | M_{3}) \end{aligned}

Then Ψ; Δ; Γ ⊢ νw⃗ N from Lemma 32. Assume that in ⟨Ψ; Δ; Γ ⊢ νw⃗ N⟩ the typing judgment for (\overline{x}y. M_{1} | x(z). M_{2} | M_{3}) is

Ψ′; Δ′; Γ′ ⊢ (\overline{x}y. M_{1} | x(z). M_{2} | M_{3})

and is derived from Ψ′; Δ_{1}; Γ_{1} ⊢ (\overline{x}y. M_{1} | x(z). M_{2}) and Ψ′; Δ_{2}; Γ_{2} ⊢ M_{3}. We distinguish two cases depending on the structure of ⟨Ψ′; Δ_{1}; Γ_{1} ⊢ \overline{x}y. M_{1} | x(z). M_{2}⟩.

1. Suppose that the last rule applied to type \overline{x}y. M_{1} is out_{1}.

Then y ∉ n(Ψ′) and x : s ∈ Ψ′ for s such that ∘ ⟶^{s} σ. So the last rule applied to type x(z). M_{2} is inp_{1} and we have:

Ψ′, x : s; ∅; \{y : ∘\} ⊢ \overline{x}y. M_{1} Ψ′, x : s; ∅; ∅ ⊢ x(z). M_{2}
Ψ′; ∅; {y : σ} ⊢ M_{1} Ψ′; {z : σ}; ∅ ⊢ M_{2} (1)

Hence Δ′ = Δ_{2} and Γ′ = Γ_{2} ∪ {y : ∘} and we have:

Ψ′; Δ_{2}; Γ_{2}, y : ∘ ⊢ (\overline{x}y. M_{1} | x(z). M_{2} | M_{3})  (2)

Note that y ∉ n(Ψ′, z), since y ≠ z from the non-homonymy condition. Also note that from typing z ∉ n(Ψ′). Then from (1) and Lemma 35:

Ψ′; {y : σ}; ∅ ⊢ M_{2}{y/z}  (3)

From the complementarity of Δ_{1}, Γ_{1} and Δ_{2}, Γ_{2} and from y : ∘ ∈ Γ_{1} it follows that y ∉ n(Γ_{2}). Also, y ∉ n(Δ_{2}) from y : ∘ ∈ Γ′ and Lemma 28(5). Then ({y : σ}, {y : σ}) and (Δ_{2}, Γ_{2}) are complementary and from (1) and (3) we get:

Ψ′; Δ_{2}, y : σ; Γ_{2}, y : σ ⊢ (M_{1} | M_{2}{y/z} | M_{3})  (4)

We can now compare the type inference for νw⃗ N′ rooted in (4) with the type inference for νw⃗ N rooted in (2). From this comparison and Lemma 32 we have the following two possible typing judgments for M′:

• If y ∉ w⃗ then Ψ; Δ, y : σ; Γ − {y : ∘}, y : σ ⊢ M′.

In fact the sequence of restriction rules applied in the type inference rooted in (4) is the same as the sequence of restriction rules applied in the type inference rooted in (2).

• If y ∈ w⃗ then Ψ; Δ; Γ ⊢ M′.

In this case res_{3} is applied correspondingly to νy in the inference rooted in (4) instead of the rule res_{2} applied in the inference rooted in (2). The sequence of restriction rules applied in the two type inferences is otherwise the same.

2. Now suppose that the last rule applied to type \overline{x}y. M_{1} is out_{2}. Then y : s ∈ Ψ′ for s such that ∘ ≠ σ ⟶^{s} τ. So the last rule applied to type x(z). M_{2} is inp_{2} and we have:

Ψ′, y : s; ∅; \{x : σ\} ⊢ \overline{x}y. M_{1} Ψ′; \{x : σ\}; ∅ ⊢ x(z). M_{2}
Ψ′; ∅; {x : τ} ⊢ M_{1}  Ψ′, z : s; {x : τ}; ∅ ⊢ M_{2}  (5)

Note that from the non-homonymy condition and typing z, y ≠ x and z ∉ n(Ψ′). Then from (5) and Lemma 34:

Ψ′, y : s; {x : τ}; ∅ ⊢ M_{2}{y/z}  (6)

Under the above hypotheses Δ′ = Δ_{2} ∪ {x : σ} and Γ′ = Γ_{2} ∪ {x : σ}. Hence:

Ψ′; Δ_{2}, x : σ; Γ_{2}, x : σ ⊢ (\overline{x}y. M_{1} | x(z). M_{2} | M_{3})  (7)

From the complementarity of ({x : σ}, {x : σ}) and (Δ_{2}, Γ_{2}), the complementarity of ({x : τ}, {x : τ}) and (Δ_{2}, Γ_{2}) follows. Hence from (5) and (6) we have:

Ψ′; Δ_{2}, x : τ; Γ_{2}, x : τ ⊢ (M_{1} | M_{2}{y/z} | M_{3})  (8)

The type inference for νw⃗ N′ rooted in (8) is now compared to the type inference for νw⃗ N rooted in (7), leading to the following two cases.

• If x ∉ w⃗ then Ψ; Δ − {x : σ}, x : τ; Γ − {x : σ}, x : τ ⊢ M′.

• If x ∈ w⃗ then Ψ; Δ; Γ ⊢ M′.

Hence the thesis, from the possible typing judgments for M′ collected above. □

The rules for typing monadic contexts are like the rules in Tab. 2, with the addition of the rule: Ψ; Δ; Γ ⊢ [·] for any Ψ, Δ, Γ. A monadic context K is a λ^{m}(Ψ, Δ, Δ′)-context if assuming Ψ; Δ; Δ ⊢ [·] we can infer Ψ′; Δ′; Δ′ ⊢ K for some Ψ′.

Definition 37 M and N are barbed λ^{m}-congruent, M ≈_{λ}^{m} N, if there are Ψ, Δ such that Ψ; Δ; Δ ⊢ M, N and K[M] ˙≈ K[N] for every λ^{m}(Ψ, Δ, ∅)-context K.

Recalling the counterexample P = \overline{x}y. \overline{x}y. 0 and Q = \overline{x}y. 0 | \overline{x}y. 0 to full abstraction of the translation, and the monadic context K = [·] | x(z). x(w). a(v). 0 such that K[[[P]]] ˙≉ K[[[Q]]], note that K is not a λ^{m}(Ψ, Δ, ∅)-context for any Ψ and Δ.

4 Main results

In this section we prove the main results. We begin by relating typing of P under λ and typing of [[P]] under λ^{m}. First, typing is preserved by the translation:

Lemma 38 If Ψ ⊢ P then Ψ; ∅; ∅ ⊢ [[P]].

Proof: The proof is by induction on the inference of Ψ ⊢ P.

Suppose Ψ ⊢ P where P = \overline{x}y⃗. Q and y⃗ = y_{1} … y_{n}. Then Ψ′ ⊢ Q and Ψ = Ψ′, x : s, y_{1} : t_{1}, …, y_{n} : t_{n} where λ(s) = (t_{1}, …, t_{n}) and Ψ′(x) ≃ s and Ψ′(y_{i}) ≃ t_{i}. By assumption, Ψ′; ∅; ∅ ⊢ [[Q]]. Now [[P]] = νw \overline{x}w. \overline{w}y_{1}. . . . . \overline{w}y_{n}. [[Q]] where w ∉ n(Ψ). Hence as ∘ ≠ s^{n} ⟶^{t_{n}} • and Ψ′(y_{n}) ≃ t_{n},

Ψ′, y_{n} : t_{n}; ∅; \{w : s^{n}\} ⊢ \overline{w}y_{n}. [[Q]]

and by similar reasoning, as ∘ ≠ s^{1} ⟶^{t_{1}} s^{2} and Ψ′(y_{1}) ≃ t_{1},

Ψ′, y_{1} : t_{1}, …, y_{n} : t_{n}; ∅; \{w : s^{1}\} ⊢ \overline{w}y_{1}. . . . . \overline{w}y_{n}. [[Q]].

Hence since ∘ ⟶^{s} s^{1} and Ψ′(x) ≃ s,

Ψ′, x : s, y_{1} : t_{1}, …, y_{n} : t_{n}; ∅; \{w : ∘\} ⊢ \overline{x}w. \overline{w}y_{1}. . . . . \overline{w}y_{n}. [[Q]]

and hence

Ψ′, x : s, y_{1} : t_{1}, …, y_{n} : t_{n}; ∅; ∅ ⊢ νw \overline{x}w. \overline{w}y_{1}. . . . . \overline{w}y_{n}. [[Q]]

i.e. Ψ; ∅; ∅ ⊢ [[P]].

Suppose Ψ ⊢ P where P = x(z⃗). Q and z⃗ = z_{1} … z_{n}. Then Ψ′, z_{1} : t_{1}, …, z_{n} : t_{n} ⊢ Q and Ψ = Ψ′, x : s where λ(s) = (t_{1}, …, t_{n}) and Ψ′(x) ≃ s and z_{i} ∉ n(Ψ′). By assumption, Ψ′, z_{1} : t_{1}, …, z_{n} : t_{n}; ∅; ∅ ⊢ [[Q]]. Now [[P]] = x(w). w(z_{1}). . . . . w(z_{n}). [[Q]] where w ∉ n(Ψ′, x, z⃗). Hence as ∘ ≠ s^{n} ⟶^{t_{n}} •,

Ψ′, z_{1} : t_{1}, …, z_{n−1} : t_{n−1}; {w : s^{n}}; ∅ ⊢ w(z_{n}). [[Q]]

and by similar reasoning, as ∘ ≠ s^{1} ⟶^{t_{1}} s^{2},

Ψ′; {w : s^{1}}; ∅ ⊢ w(z_{1}). . . . . w(z_{n}). [[Q]].

Hence since ∘ ⟶^{s} s^{1} and Ψ′(x) ≃ s,

Ψ′, x : s; ∅; ∅ ⊢ x(w). w(z_{1}). . . . . w(z_{n}). [[Q]]

i.e. Ψ; ∅; ∅ ⊢ [[P]].

The other cases are straightforward. For instance suppose Ψ ⊢ P where P = !Q. Then Ψ ⊢ Q and so by assumption Ψ; ∅; ∅ ⊢ [[Q]] and so Ψ; ∅; ∅ ⊢![[Q]], i.e. Ψ; ∅; ∅ ⊢ [[P]].

□

Secondly, if the translation of a process can be typed, then the process itself can be typed:

Lemma 39 If Ψ; Δ; Γ ⊢ [[P]] then Δ = Γ = ∅ and Ψ ⊢ P.

Proof: The proof is by induction on the structure of P.

Suppose Ψ; Δ; Γ ⊢ [[P]] where P = \overline{x}y⃗. Q with y⃗ = y_{1} … y_{n}, so

Ψ; Δ; Γ ⊢ νw \overline{x}w. \overline{w}y_{1}. . . . . \overline{w}y_{n}. [[Q]]

where w ∉ n(Ψ, Δ, Γ).

Suppose Ψ; Δ; Γ ⊢ [[P]] is inferred from

Ψ, w : s; Δ; Γ ⊢ \overline{x}w. \overline{w}y_{1}. . . . . \overline{w}y_{n}. [[Q]].

Then it must be that Δ = ∅ and Γ = \{x : σ\} and Ψ; ∅; Γ′ ⊢ \overline{w}y_{1}. . . . . \overline{w}y_{n}. [[Q]] where ∘ ≠ σ ⟶^{s} τ and Γ′ = {x : τ} and Ψ(w) ≃ s. But this is impossible by the form of the typing rules for output prefixes and the facts that σ, τ ≠ ∘.

So suppose Ψ; Δ; Γ ⊢ [[P]] is inferred from

Ψ; Δ′; Γ′ ⊢ \overline{x}w. \overline{w}y_{1}. . . . . \overline{w}y_{n}. [[Q]]

where Δ′ = Δ, w : σ and Γ′ = Γ, w : σ where σ ≠ ∘. Then it must be that Δ′ = ∅ and so σ = •. Hence Γ = ∅. But this is impossible by the form of the typing rules for output prefixes by reasoning similar to that above.

Hence Ψ; Δ; Γ ⊢ [[P]] is inferred from

Ψ; Δ; Γ, w : ∘ ⊢ \overline{x}w. \overline{w}y_{1}. . . . . \overline{w}y_{n}. [[Q]].

So Δ = Γ = ∅ where w ∉ n(Γ), and

Ψ_{1}; ∅; \{w : σ_{1}\} ⊢ \overline{w}y_{1}. . . . . \overline{w}y_{n}. [[Q]]

where Ψ = Ψ_{1}, x : s and Ψ_{1}(x) ≃ s and ∘ ⟶^{s} σ_{1}. In turn,

Ψ_{2}; ∅; \{w : σ_{2}\} ⊢ \overline{w}y_{2}. . . . . \overline{w}y_{n}. [[Q]]

where Ψ_{1} = Ψ_{2}, y_{1} : t_{1} and Ψ_{2}(y_{1}) ≃ t_{1} and σ_{1} ⟶^{t_{1}} σ_{2}. By similar reasoning,

Ψ_{n}; ∅; \{w : σ_{n}\} ⊢ \overline{w}y_{n}. [[Q]]

where Ψ_{n−1} = Ψ_{n}, y_{n−1} : t_{n−1} and Ψ_{n}(y_{n−1}) ≃ t_{n−1} and σ_{n−1} ⟶^{t_{n−1}} σ_{n}, and hence

Ψ_{n+1}; ∅; {w : σ_{n+1}} ⊢ [[Q]]

where Ψ_{n} = Ψ_{n+1}, y_{n} : t_{n} and Ψ_{n+1}(y_{n}) ≃ t_{n} and σ_{n} ⟶^{t_{n}} σ_{n+1}. By assumption {w : σ_{n+1}} = ∅, so σ_{n+1} = •, and Ψ_{n+1} ⊢ Q. Hence

∘ ⟶^{s} σ_{1} ⟶^{t_{1}} … ⟶^{t_{n−1}} σ_{n} ⟶^{t_{n}} •

so λ(s) = (t_{1} … t_{n}). Further, if x = y_{i} then s = t_{i} because Ψ_{i+1}(y_{i}) ≃ t_{i}, and similarly if y_{i} = y_{j} then t_{i} = t_{j}. Hence Ψ ⊢ P. So in summary, Δ = Γ = ∅ and Ψ ⊢ P.

The case P = x(z⃗). Q is similar and slightly simpler. The remaining cases are straightforward. For instance P = !Q and Ψ; Δ; Γ ⊢ [[P]] then Δ = Γ = ∅ and Ψ; ∅; ∅ ⊢ [[Q]]. Hence by assumption Ψ ⊢ Q, and so Ψ ⊢ P. □

This lemma does not hold if we admit prefixes of the forms \overline{x}⟨⟩ and x(). For example if λ(s) = (s), then ∅; ∅; x : s^{1} ⊢ [[\overline{x}⟨⟩. 0]], [[x(). 0]].

We now prove that the translation is sound.

Theorem 40 If [[P]] ≈_{λ}^{m} [[Q]] then P ≈_{λ} Q.

Proof: Consider first B = {(R, [[R]]) | R a λ-process}. We noted in Section 2 that

1. R ↓_{μ} iff [[R]] ↓_{μ}, and

2. if R ⟶ R′ then [[R]] ⟶ N ⟹ [[R′]] with N ≈^{m} [[R′]].

We show that

if [[R]] ⟶ N then N ≈^{m} [[R′]] where R ⟶ R′.  (9)

Assertion (9) does not hold without the assumption that R is a λ-process: consider for instance R = \overline{a}⟨bc⟩. 0 | a(z). 0. Assertion (9) is harder to prove than it may at first sight appear. The reason is that the structural rule may be applied arbitrarily in inferring [[R]] ⟶ N, and it takes some work to see that a suitable R′ can always be found. The monadic type system plays a key role in carrying out that work.

We write M ⇝ M′ if there are ⟨Ψ; Δ; Γ ⊢ M⟩ and w monadic in it such that M′ is obtained from M by replacing a subterm N by N′ where

1. N = νw νz K and N′ = νz νw K where z is not monadic in ⟨Ψ; Δ; Γ ⊢ M⟩, or

2. N = νw (K | K′) and N′ = K | νw K′ where w ∉ fn(K), or

3. N = νw (K | K′) and N′ = νw K | K′ where w ∉ fn(K′).

Note that M ⇝ M′ implies M′ ≡_{1} M. In a structural manipulation of [[R]], a ⇝- transformation involving νw changes the term structure in such a way as to move the restriction towards the prefix of the form \overline{x}w introduced in translating R. The ⇝- transformations and their inverses have no direct counterparts in a manipulation of R. We have, however, Lemma 41 If [[R]] ≡ M then M ⇝^{∗} [[R′′]] where R′′ ≡ R.

Proof: Since ≡ is ≡_{1}^{∗}, it suffices to show that

if M ⇝^{∗} [[R′′]] and M ≡_{1} M′, then either M′ ⇝^{∗} [[R′′]], or M′ ⇝^{∗} [[R′]] where
R′ ≡_{1} R′′.

If M′ ⇝ M then clearly M′ ⇝^{∗} [[R′′]]. Further, if M ⇝ M′ then again M′ ⇝^{∗} [[R′′]], since the ⇝-transformations commute with one another. So suppose the transformation between M and M′ is not of these kinds. The proof is then a case analysis on the axiom of structural congruence applied in the transformation. We give just one case. Suppose M is K[ !N] and M′ is K[N |!N]. In M ⇝^{∗} [[R′′]], each restricted monadic name is reunited with its partner via ⇝-transformations. The same (fourth) axiom of structural congruence can then be applied to the corresponding subterm of R′′ to yield R′. Then using ⇝^{−1}-transformations, the term M′ can be obtained from [[R′]]. A more formal proof can be given by appealing to a notion of embedding of an inference of Ψ ⊢ R in an inference of Ψ; ∅; ∅ ⊢ [[R]]. This makes precise the notion of ‘corresponding subterm’ referred to above. □

Now returning to the proof of (1), suppose [[R]] ≡ M = νw⃗ (\overline{x}w. M_{1} | x(z). M_{2} | M_{3}) and M ↦ M′ = νw⃗ (M_{1} | M_{2}{w/z} | M_{3}) ≡ N. Then R ≡ R′′ where M ⇝^{∗} [[R′′]]. By the form of M, R′′ = νv⃗ (\overline{x}y⃗. P_{1} | x(z⃗). P_{2} | P_{3}) and R′′ ↦ R′ = νv⃗ (P_{1} | P_{2}\{y⃗/z⃗\} | P_{3}) where νw \overline{x}w. M_{1} ⇝^{∗} [[\overline{x}y⃗. P_{1}]], x(z). M_{2} ⇝^{∗} [[x(z⃗). P_{2}]], and νu⃗ M_{3} ⇝^{∗} [[P_{3}]] where w⃗ is a permutation of v⃗wu⃗. Further N ⟹ [[R′]] and [[R′]] ≈^{m} N as required. By 1, 2 and (9) we have

Corollary 42 If R is a λ-process then [[R]] ˙≈ R.

To complete the proof of the theorem, suppose [[P]] ≈_{λ}^{m} [[Q]] and Ψ is such that Ψ; ∅; ∅ ⊢ [[P]], [[Q]] and K[[[P]]] ˙≈ K[[[Q]]] for every λ^{m}(Ψ, ∅, ∅)-context K. Then Ψ ⊢ P, Q and if C is a λ(Ψ)-context then [[C]] is a λ^{m}(Ψ, ∅, ∅)-context and so

C[P] ˙≈ [[C[P]]] = [[C]][[[P]]] ˙≈ [[C]][[[Q]]] = [[C[Q]]] ˙≈ C[Q].

Hence P ≈_{λ} Q. □

We now prove that the translation is complete.

Theorem 43 If P ≈_{λ} Q then [[P]] ≈_{λ}^{m} [[Q]].

Proof: Suppose P ≈_{λ} Q and Ψ_{0} is such that Ψ_{0} ⊢ P, Q and C[P] ˙≈ C[Q] for every λ(Ψ_{0})-context C. Then Ψ_{0}; ∅; ∅ ⊢ [[P]], [[Q]]. Suppose K is a λ^{m}(Ψ_{0}, ∅, ∅)-context. The crucial fact is:

There is a λ(Ψ_{0})-context C such that K[[[P]]] ˙≈ [[C]][[[P]]] and K[[[Q]]] ˙≈ [[C]][[[Q]]]. (10)

From this, using Corollary 42 we have

K[[[P]]] ˙≈ [[C]][[[P]]] = [[C[P]]] ˙≈ C[P] ˙≈ C[Q] ˙≈ [[C[Q]]] = [[C]][[[Q]]] ˙≈ K[[[Q]]].

To establish (10) we show Lemma 44 Suppose Ψ; Δ; Δ, w⃗ : ∘ ⊢ K assuming Ψ_{0}; Δ_{0}; Δ_{0}, w⃗_{0} : ∘ ⊢ [·]. Then there exists C such that

1. Ψ ⊢ C assuming Ψ_{0} ⊢ [·], and

2. if Ψ_{0}; Δ_{0}; Δ_{0}, w⃗_{0} : ∘ ⊢ M then νv⃗w⃗ K[M] ≈_{λ}^{m} [[C]][νv⃗_{0}w⃗_{0} M] where v⃗ = n(Δ) and v⃗_{0} = n(Δ_{0}).

Proof: By induction on the derivation of Ψ; Δ; Δ, w⃗ : ∘ ⊢ K. Note that the assertion concerns ≈_{λ}^{m} and not ˙≈; this is important in the induction.

The most difficult cases are the prefixes. Of these, we only show the argument for the input prefix; the argument for output prefix is dual to it.

[inp_{1}] K = x(z). K_{0} and by the typing rules Ψ = Ψ′ ∪ {x : s} and Δ, w⃗ = ∅ and Ψ′; {z : s^{1}}; ∅ ⊢ K_{0} (where ∘ ⟶^{s} s^{1}). For clarity we assume that λ(s) = (t_{1}t_{2}) – this retains the essence of the problem. By Lemma 29 we have (in the most complicated of the four possible combinations):

K ≡ K′ = x(z). νu⃗_{1} (z(z_{1}). νu⃗_{2} (z(z_{2}). K_{3} | K_{2}) | K_{1})

with | K′ | ≤ | K |. (We abuse notation here: each K_{i} is a term, i.e. a process or a context. We may also omit sorts when they are not important.) From the typing rules, setting u⃗_{3} = ∅, in ⟨Ψ; ∅; ∅ ⊢ K′⟩ the judgment for K_{i} is of the form

Ψ_{i}, x⃗_{1}, x⃗_{2}; Δ_{i}; Δ_{i}, w⃗_{i} : ∘ ⊢ K_{i} where n(Δ_{i}) = v⃗_{i} and x⃗_{i}v⃗_{i}w⃗_{i} = u⃗_{i}.

By the inductive hypothesis there are C_{1}, C_{2}, C_{3} such that Ψ_{i}, x⃗_{1}, x⃗_{2} ⊢ C_{i} assuming Ψ_{0} ⊢ [·], and if Ψ_{0}; Δ_{0}; Δ_{0}, w⃗_{0} : ∘ ⊢ M then νv⃗_{i}w⃗_{i} K_{i}[M] ≈_{λ}^{m} [[C_{i}]][νv⃗_{0}w⃗_{0} M]. Then set

C = x(z_{1}z_{2}). νx⃗_{1}x⃗_{2} (C_{3} | C_{2} | C_{1}).

We show that for every M such that Ψ_{0}; Δ_{0}; Δ_{0}, w⃗_{0} : ∘ ⊢ M,

K′[M] ≈_{λ}^{m} [[C]][νv⃗_{0}w⃗_{0} M].  (11)

As an aside, note here the fundamental role of typing in the inductive argument. It is not in general the case that K′[M] ≈^{m} [[C]][νv⃗_{0}w⃗_{0} M]. For example if νu⃗_{1} K_{1} ↓_{μ} for some μ then H′[K′[M]] ˙≉ H′[[[C]][νv⃗_{0}w⃗_{0} M]] where H′ is [·] | νw \overline{x}w. 0.

Returning to the main proof, if Ψ_{0}; Δ_{0}; Δ_{0}, w⃗_{0} : ∘ ⊢ M then K′′[M] ≈_{λ}^{m} [[C]][νv⃗_{0}w⃗_{0} M] where

K′′ = x(z). z(z_{1}). z(z_{2}). νu⃗_{1}u⃗_{2} (K_{3} | K_{2} | K_{1}).

So assertion (11) follows from

K′[M] ≈_{λ}^{m} K′′[M].

This in turn follows from

Lemma 45 Suppose Ψ; ∅; ∅ ⊢ K′, K′′ where

\begin{aligned}K′ & = & x(z). νu⃗_{1} (z(z_{1}). νu⃗_{2} (z(z_{2}). K_{3} | K_{2}) | K_{1}) \\ K′′ & = & x(z). z(z_{1}). z(z_{2}). νu⃗_{1}u⃗_{2} (K_{3} | K_{2} | K_{1}). \end{aligned}

Then K′ ≈_{λ}^{m} K′′.

Proof: Let Θ = {θ | θ respects Ψ}. We show that

R = {(H[K′θ], H[K′′θ]) | θ ∈ Θ and H is a λ^{m}(Ψθ, ∅, ∅)-context} ∪ ˙≈

is a barbed bisimulation up to ≈^{m}. Then for any λ^{m}(Ψ, ∅, ∅)-context H we have H[K′] ˙≈ H[K′′], and hence K′ ≈_{λ}^{m} K′′.

Let (H[K′θ], H[K′′θ]) ∈ R. The two processes H[K′θ] and H[K′′θ] have the same observables. Assume now that H[K′θ] ⟶ X. Then from Lemma 5:

H[K′θ] ≡ νw⃗ (\overline{z}y. T_{1} | z(u). T_{2} | T_{3}) ⟶ X ≡ νw⃗ (T_{1} | T_{2}\{y/u\} | T_{3})  (12)

From this and definition of K′, K′′ and ≡, we have:

H[K′′θ] ≡ νw⃗ (\overline{z}y. T′_{1} | z(u). T′_{2} | T′_{3}) ⟶ Y ≡ νw⃗ (T′_{1} | T′_{2}\{y/u\} | T′_{3})  (13)

where T′_{j} = T_{j} if T_{j} does not contain a copy of K′θ which comes from filling the hole in H. Note that by definition of λ^{m}(Ψθ, ∅, ∅)-context, there exist Ψ′, Ψ′′ such that Ψ′; ∅; ∅ ⊢ H[K′θ] and Ψ′′; ∅; ∅ ⊢ H[K′′θ]. From this and Lemma 36, it follows that:

Ψ′; ∅; ∅ ⊢ X  Ψ′′; ∅; ∅ ⊢ Y  (14)

We distinguish two cases:

[case 1] If the intraaction does not involve a copy of K′θ which comes from filling the hole in H, then we can further distinguish the following two subcases.

1. If T_{2} does not contain a copy of K′θ then:

X ≡ H′[K′θ] Y ≡ H′[K′′θ]

and from (14) H′ is a λ^{m}(Ψθ, ∅, ∅)-context. Hence (X, Y) ∈ R.

2. If T_{2} does contain a copy of K′θ then:

X ≡ H′[K′θ{y/u}] Y ≡ H′[K′′θ{y/u}]

We show that θ\{y/u\} ∈ Θ by investigating on the typing of (\overline{z}y. T_{1} | z(u). T_{2}).

• If the last rule applied in the typing judgment for z(u). T_{2} is inp_{1} then Ψ_{1}; {u : σ}; ∅ ⊢ T_{2} for some Ψ_{1} such that u ∉ n(Ψ_{1}). Suppose that u ∈ n(Ψθ). From the non-homonymy condition no binder on u can occur in T_{2}. Then, since the only rules that can decrement the size of the first component of a typing judgment are inp_{2} and res_{1}, the contradiction u ∈ n(Ψ_{1}) follows. Hence u ∉ n(Ψθ), namely u ∉ cosupp(θ) and either u ∉ n(Ψ) or (u ∈ n(Ψ) and θ = θ′{w/u}), i.e. θ{y/u} = θ. In each case θ{y/u} ∈ Θ.

• If the last rule applied in the typing judgment for z(u). T_{2} is inp_{2} then the last rule applied to type \overline{z}y. T_{1} is out_{2} and hence Ψ_{1}, u : s; \{z : τ\}; ∅ ⊢ T_{2} for some Ψ_{1} such that Ψ_{1}(y) ≃ s. Then u : s ∈ Ψθ and Ψθ(y) ≃ s. Hence the thesis simply noting that (w : s ∈ Ψθ implies Ψ(w) ≃ s).

From θ{y/u} ∈ Θ and Lemma 34 we have: Ψθ{y/u}; ∅; ∅ ⊢ K′θ{y/u}, K′′θ{y/u}.

Then H′ is a λ^{m}(Ψθ{y/u}, ∅, ∅)-context from (14), and hence (X, Y) ∈ R.

[case 2] If the intraaction does involve a copy of K′θ which comes from filling the hole then in (12) and (13) the following holds: z(u). T_{2} ≡ K′θ and z(u). T′_{2} ≡ K′′θ and T_{1} = T′_{1}.

Note that, since Ψθ; ∅; ∅ ⊢ K′θ, the typing judgment for \overline{z}y. T_{1} must have been inferred from out_{1}, namely:

Ψθ; ∅; \{y : ∘\} ⊢ \overline{z}y. T_{1} Ψθ; ∅; \{y : σ\} ⊢ T_{1}

with ∘ ⟶^{s} σ and z : s ∈ Ψθ. From Ψθ; ∅; \{y : ∘\} ⊢ \overline{z}y. T_{1} and Ψ′; ∅; ∅ ⊢ H[K′θ] it follows that y ∈ w⃗. Also, from Ψθ; ∅; {y : σ} ⊢ T_{1} and applying twice Lemma 29 we have that, in the most complicated of the four possible cases, T_{1} ≡ νw⃗_{1} (\overline{y}x_{1}. νw⃗_{2} (\overline{y}x_{2}. N_{3} | N_{2}) | N_{1}) with y ∉ w⃗_{1}, w⃗_{2}. Hence:

X ≡ νw⃗ ( νw⃗_{1} (\overline{y}x_{1}. νw⃗_{2} (\overline{y}x_{2}. N_{3} | N_{2}) | N_{1}) |
νu⃗_{1} (y(z_{1}). νu⃗_{2} (y(z_{2}). K_{3}θ′ | K_{2}θ′) | K_{1}θ′) |
T_{3} )

where θ′ = θ{y/u} and where z_{2} ∉ fn(K_{2}θ′) and z_{1}, z_{2}, u_{2} ∉ fn(K_{1}θ′) from the nonhomonymy condition. Analogously:

Y ≡ νw⃗ ( νw⃗_{1} (\overline{y}x_{1}. νw⃗_{2} (\overline{y}x_{2}. N_{3} | N_{2}) | N_{1}) |
y(z_{1}). y(z_{2}). νu⃗_{1}u⃗_{2} (K_{3}θ′ | K_{2}θ′ | K_{1}θ′) |
T′_{3} )

Then, letting θ_{1} = {x^{1}/z_{1}} and θ_{2} = {x^{1}x^{2}/z_{1}z_{2}}, we have:

X ⟶^{2} X′′ ≡ νw⃗ ( νw⃗_{1} (νw⃗_{2} (N_{3} | N_{2}) | N_{1}) |
νu⃗_{1} (νu⃗_{2} (K_{3}θ′θ_{2} | K_{2}θ′θ_{1}) | K_{1}θ′) |
T_{3} )
Y ⟶^{2} Y′′ ≡ νw⃗ ( νw⃗_{1} (νw⃗_{2} (N_{3} | N_{2}) | N_{1}) |
νu⃗_{1}u⃗_{2} (K_{3}θ′θ_{2} | K_{2}θ′θ_{2} | K_{1}θ′θ_{2}) |
T′_{3} )

Noting that X ≈^{m} X′′ by y ∈ w⃗, we can conclude the proof by the following argument. If the hole in H is not underneath a replication then z(u). T_{2} ≡ K′θ and z(u). T′_{2} ≡ K′′θ are the only copies of K′θ and K′′θ which come from filling the hole in H. Then T_{3} ≡ T′_{3} and hence:

X ≈^{m} X′′ ≡ Y′′.

If the hole in H is underneath a replication then X′′ and Y′′ differ in that the used K′θ and K′′θ are expanded copies of replications that still occur in T_{3} and in T′_{3} respectively. Then X′′ ≡ H′[K′θ] and Y′′ ≡ H′[K′′θ] where, from (14) and Lemma 36, H′ is a λ^{m}(Ψθ, ∅, ∅)-context. Then:

X ≈^{m} X′′ ≡ H′[K′θ] R H′[K′′θ] ≡ Y′′.
□

[par] K = K_{1} | K_{2} and we can distinguish the following cases.

• If Δ = ∅ then by typing

Ψ; ∅; w⃗_{i} : ∘ ⊢ K_{i} where w⃗_{1}w⃗_{2} = w⃗.

Then by the inductive hypothesis there are C_{1}, C_{2} such that Ψ ⊢ C_{i} assuming Ψ_{0} ⊢ [·], and if Ψ_{0}; Δ_{0}; Δ_{0}, w⃗_{0} : ∘ ⊢ M then νw⃗_{i} K_{i}[M] ≈_{λ}^{m} [[C_{i}]][νv⃗_{0}w⃗_{0} M]. Then the thesis, upon setting C = C_{1} | C_{2}.

• If Δ ≠ ∅ then z : σ ∈ Δ for some z. Then by Lemma 29 we have, in the most complicated case,

K ≡ K′ = νu⃗ (\overline{z}z_{1}. K′_{1} | z(z_{2}). K′_{2} | K′_{3})

with | K′ | ≤ | K |. From the typing rules we have

Ψ, x⃗_{1}; Δ_{1}; Δ_{1}, w⃗_{1} : ∘, w⃗ : ∘ ⊢ (\overline{z}z_{1}. K′_{1} | z(z_{2}). K′_{2} | K′_{3})

where n(Δ_{1}) = n(Δ) ∪ {z, v⃗_{1}} and x⃗_{1}zv⃗_{1}w⃗_{1} = u⃗. Moreover:

Ψ, x⃗_{1}; \{z : σ\}; \{z : σ\} ⊢ (\overline{z}z_{1}. K′_{1} | z(z_{2}). K′_{2}) = K′′_{1}
Ψ, x⃗_{1}; Δ, v⃗_{1}; Δ, v⃗_{1}, w⃗_{1} : ∘, w⃗ : ∘ ⊢ K_{3} = K′′_{2}

Then by the inductive hypothesis there are C_{1}, C_{2} such that Ψ, x⃗_{1} ⊢ C_{i} assuming Ψ_{0} ⊢ [·], and if Ψ_{0}; Δ_{0}; Δ_{0}, w⃗_{0} : ∘ ⊢ M then νz K′′_{1}[M] ≈_{λ}^{m} [[C_{1}]][νv⃗_{0}w⃗_{0} M] and νv⃗v⃗_{1}w⃗w⃗_{1}K′′_{2}[M] ≈_{λ}^{m} [[C_{2}]][νv⃗_{0}w⃗_{0}M]. Then the thesis, upon setting C = νx⃗_{1}(C_{1} | C_{2}).

[res_{1},res_{2},res_{3}] K = νz K_{1} and, depending on the typing rule under consideration, by the inductive hypothesis K_{1} is appropriately related to a certain C_{1}. In each case the thesis is then an immediate consequence of the inductive hypothesis, setting C = νz C_{1} if Ψ, z : s; Δ; Δ, w⃗ : ∘ ⊢ K_{1} (rule res_{1}), and C = C_{1} otherwise. □

This completes the proof of Theorem 43. □

A final remark: in the translation the clause for output prefix could alternatively be

[[\overline{x}⟨a_{1} … a_{n}⟩. Q]] = νw \overline{x}w. (\overline{w}a_{1}. . . . . \overline{w}a_{n}. 0 | [[Q]]).

The same results hold in this case, the type system and Lemma 9 showing clearly why the two translations are in essence the same.

As mentioned in the Introduction, the work to which that presented here is most closely related is [Yos96]. There a notion of graph type for monadic processes is introduced and studied. Nodes of a graph type represent atomic actions, and edges an activation ordering between them. Among other results, a full abstraction theorem for the translation of polyadic processes to monadic processes is shown. The present paper is not, therefore, the first to prove such a result. We believe, however, that the approach introduced in this paper is considerably simpler and clearer. The type system is of a kind which is well understood, and its rules are very natural, given the idea of the graph G_{λ} arising from a polyadic sorting λ. We found the ability to argue by induction on type inference invaluable to the proof of full abstraction. We believe the techniques introduced here may be useful in other circumstances.

References

[Hon93] K. Honda. Types for Dyadic Interaction. In E. Best, editor, Proc. 4th Conf. CONCUR, volume 715 of LNCS, pages 509–523. Springer-Verlag, 1993.

[Kob97] N. Kobayashi. A partially deadlock-free typed process calculus. In Proc. 12th IEEE Symp. LICS, pages 128–139, 1997.

[KPT96] N. Kobayashi, B.C. Pierce, and D.N. Turner. Linearity and the Pi-Calculus. In Proc. 23rd ACM Symp. POPL, pages 358–371, 1996.

[LW95] X. Liu and D. Walker. A Polymorphic Type System for the Polyadic πcalculus. In I. Lee and S.A. Smolka, editors, Proc. 6th Conf. CONCUR, volume 962 of LNCS, pages 103–116. Springer-Verlag, 1995.

[Mil92] R. Milner. The Polyadic π-Calculus: a Tutorial. In F.L. Bauer, W. Brauer, and H. Schwichtenberg, editors, Logic and Algebra of Specification, pages 203– 246. Springer-Verlag, 1992.

[MPW92] R. Milner, J. Parrow, and D. Walker. A Calculus of Mobile Processes, Part I and II. Information and Computation, 100(1):1–77, 1992.

[NS97] U. Nestmann and M. Steffen. Typing Confluence. In S. Gnesi and D. Latella, editors, Proc. 2nd Int. ERCIM Workshop on Formal Methods in Industrial Critical Systems, pages 77–101, 1997.

[PS93] B.C. Pierce and D. Sangiorgi. Typing and Subtyping for Mobile Processes. In Proc. 8th IEEE Symp. LICS, pages 376–385, 1993.

[PS97] B.C. Pierce and D. Sangiorgi. Behavioral Equivalence in the Polymorphic Pi-Calculus. In Proc. 24th ACM Symp. POPL, pages 242–255, 1997.

[San97] D. Sangiorgi. The name discipline of uniform receptiveness. In P. Degano, R. Gorrieri, and A. Marchetti-Spaccamela, editors, Proc. 24th ICALP, volume 1256 of LNCS, pages 303–313. Springer, 1997.

[Tur96] D.N. Turner. The Polymorphic Pi-Calculus: Theory and Implementation. PhD thesis, Comp. Sc. Dep., Edinburgh University, 1996. Report ECS-LFCS-96-345.

[VH93] V.T. Vasconcelos and K. Honda. Principal typing schemes in a polyadic πcalculus. In E. Best, editor, Proc. 4th Conf. CONCUR, volume 715 of LNCS. Springer-Verlag, 1993.

[Yos96] N. Yoshida. Graph Types for Monadic Mobile Processes. In Proc. 16th Conf. FST&TCS, volume 1180 of LNCS, pages 371–386. Springer, 1996.

Recent BRICS Report Series Publications

RS-98-26 Paola Quaglia and David Walker. On Encoding pπ in mπ. October 1998. 27 pp. Full version of paper to appear in Foundations of Software Technology and Theoretical Computer Science: 18th Conference, FCT&TCS ’98 Proceedings, LNCS, 1998.

RS-98-25 Devdatt P. Dubhashi. Talagrand’s Inequality in Hereditary Settings. October 1998. 22 pp.

RS-98-24 Devdatt P. Dubhashi. Talagrand’s Inequality and Locality in Distributed Computing. October 1998. 14 pp.

RS-98-23 Devdatt P. Dubhashi. Martingales and Locality in Distributed Computing. October 1998. 19 pp.

RS-98-22 Gian Luca Cattani, John Power, and Glynn Winskel. A Categorical Axiomatics for Bisimulation. September 1998. ii+21 pp. Appears in Sangiorgi and de Simone, editors, Concurrency Theory: 9th International Conference, CONCUR ’98 Proceedings, LNCS 1466, 1998, pages 581–596.

RS-98-21 John Power, Gian Luca Cattani, and Glynn Winskel. A Representation Result for Free Cocompletions. September 1998. 16 pp.

RS-98-20 Søren Riis and Meera Sitharam. Uniformly Generated Submodules of Permutation Modules. September 1998. 35 pp.

RS-98-19 Søren Riis and Meera Sitharam. Generating Hard Tautologies Using Predicate Logic and the Symmetric Group. September 1998. 13 pp.

RS-98-18 Ulrich Kohlenbach. Things that can and things that can’t be done in PRA. September 1998. 24 pp.

RS-98-17 Roberto Bruni, José Meseguer, Ugo Montanari, and Vladimiro Sassone. A Comparison of Petri Net Semantics under the Collective Token Philosophy. September 1998. 20 pp. To appear in 4th Asian Computing Science Conference, ASIAN ’98 Proceedings, LNCS, 1998.

RS-98-16 Stephen Alstrup, Thore Husfeldt, and Theis Rauhe. Marked Ancestor Problems. September 1998.