Polarized Name Passing

Martin Odersky

Department of Computer Science University of Karlsruhe 76128 Karlsruhe, Germany odersky@ira.uka.de

to appear in Proc. FST & TCS 15, Springer LNCS ???

Abstract. We study a refinement of name passing in a process calculus, where names have input and output polarities. Building on a simple asynchronous reduction semantics, we develop a notion of polarized bisimulation and show that it is a congruence. We then give an encoding of Moggi’s computational lambda calculus in polarized π which preserves all of Moggi’s observational equivalences except the η-value rule.

1 Introduction

Modern process calculi are centered around name passing as the fundamental principle of interaction [10]. Name passing, first proposed by Engberg and Nielsen [3], was studied in depth in the Chemical Abstract Machine [1] and particularly in the π-calculus [11, 8]. It is at the same time simple and expressive enough for representing a wide range of computation and interaction patterns. Consequently, there has also been much work in using a name passing process calculus as the target of encodings of traditional functional and imperative languages, which pass structures as arguments [9, 20, 6]. However, it has turned out to be surprisingly difficult to capture observational equalities of those languages as process equivalences. For instance, one of Milner’s original encodings of the call-by-value λ-calculus [7] did not validate the β-value reduction rule. The reason for some of these difficulties becomes clear if we look at the operations that can be performed on a name.

One can do three things with a name: Read from it, write to it or test two names for equality. The last operation is sometimes missing from the term language, but it is certainly a capability of an observing environment. Now consider encodings of functions. The standard call-by-value encoding of an abstraction λx.M introduces a fresh anonymous handle name, say a, and composes it with a reader agent ∗a?x.M (where the ∗ signifies that the reader may be used arbitrarily often). A function call then involves writing an argument name to the handle a. But a process context may manipulate the handle arbitrarily; it could equally well install a competing reader, say ∗a?y.N, or it could test the handle for equality to itself or to some other handle. These added capabilities can invalidate common laws of functional programming, since the duplication of lambda abstractions in substitutions is not observable while the duplication of handles is.

Indeed, this discrepancy points to a general problem with unrestricted name passing: it fails to validate many seemingly reasonable equivalences which involve duplication of subterms. As an example, consider a worker agent, which reads data items from channel a and processes them.

WORK(a) =^{def} ∗a?x.HANDLE(x)

(Here, ∗ means replication and a?x.... is an input term). Intuitively, we should be able to have several workers instead of one without changing the semantics of a program. That is, we would like the following equivalence to hold, for any process P:

P | WORK(a) | WORK(b) = P [a := c, b := c] | WORK(c).

However, such an equivalence would hold only for “well-behaved” clients P, which use the communication channels a and b only for writing. If P would contain a comparison of the channels a and b, say, then the two sides would clearly be not equivalent. Even if comparison of channel names were not available as a primitive, a process P could still distinguish the two sides by sending to channel a and reading from channel b. On the left-hand side, the read would surely be blocked, but on the right-hand side it might succeed.

This paper is motivated by the observation that unrestricted reading, writing, and comparison of names might be too powerful a capability (meaning too many laws are broken). We therefore discriminate between the three operations by associating polarities with names. A name with output polarity can used for writing but not for reading. Conversely, a name with input polarity can used for reading but not for writing. Finally, an equality test succeeds only if both polarities of a name are supplied. The rest of this paper formalizes this idea and studies its ramifications. In particular:

– We define a reduction system for a process calculus with polarized names. The polarized π-calculus builds on a simple asynchronous process calculus, similar to systems developed independently by Boudol [2] and by Honda [5], with the addition of polarities for names.

– We define polarized bisimulation, a new notion of process equivalence for polarized π-terms. We show that polarized bisimulation is a congruence, that it is reductionclosed and that it preserves output events.

– We give a new encoding of the call-by-value λ-calculus with let’s into the π-calculus. We show that this encoding satisfies all equalities of Moggi’s computational λcalculus [13, 14], except the η-value equality. We also discuss why it is unreasonable to expect η-value to hold in a process calculus. Computational λ-calculus is an interesting test case for an encoding, since it embodies a complete set of laws for reasoning about functions in a sequential environment.

Polarities in message exchanges are also found in the PICT programming language [17] which is based π-calculus. They have been studied in detail by Pierce and Sangiorgi [16], albeit with a slightly different motivation. Pierce and Sangiorgi consider only sorted systems, while we concentrate on the unsorted version of polarized π. They add a neutral polarity, which allows unrestricted use of a name. We do not, since such a capability can always be modeled by passing both polarities of a name. Omitting the

Constants a, b, c ^{∈} C_{a}
Variables x, y, z ^{∈} V
Names  u, v, w = a | x
Terms P, Q, R = uv Application (Output)
| ux.P  Abstraction (Input)
| ∗ux.P  (Eager) Replication
| νa.P  Restriction
| P |Q  Parallel Composition
| 0  Identity
| [u ˆ= v]P  Match

Fig. 1. Names and terms in asynchronous π.

neutral polarity makes polarized π quite a bit simpler than their system, both in the structural and reduction rules and in the type system, where no subtyping is required. We can thus study process equivalence in considerably more detail, coming up with a tractable definition of bisimulation congruence for processes with polarized names. By contrast, Pierce and Sangiorgi use barbed bisimulation and barbed congruence [12] as process equivalences. Barbed congruence is more general, but also considerably harder to use than polarized bisimulation since it requires an argument over program contexts that comprise a parallel composition with terms of arbitrary complexity instead of just parallel compositions with atomic outputs a!b.

Sangiorgi [19] has also explored an alternative treatment of the problem of preserving equivalences from functional programming. His technique relies on translating λ to π in such a way that sharing can never be observed outside of a translated term. This is achieved by “padding” the translation with forwarding terms that transmit arguments in only one direction. Thus, all translations interact with their environment only via fresh anonymous names. One disadvantage of this technique is the additional bulk introduced by the translation. Another problem is that, due to the complete elimination of sharing, constants in a functional language cannot be translated to names in the πcalculus — if they were, all comparisons between constants would show inequality. Instead, his translation maps constants to terms of a particular form called “triggers” [18].

The rest of this paper is organized as follows. Section 2 reviews Honda’s formulation of asynchronous π-calculus. Section 3 discusses what changes when polarities are added to that calculus. Section 4 defines polarized bisimulation and shows that it is a congruence. Section 5 studies an encoding of the computational λ-calculus in polarized π. Section 6 concludes.

2 Asynchronous π-calculus

Asynchronous π-calculus is a general concept rather than a fixed set of rules. One instance was developed by Boudol [2], another, with a slightly different set of rules, by Honda and Tokoro [5, 4]. Honda’s version, also called the ν-calculus, distinguishes between input-bound and ν-bound identifiers, while Boudol’s version doesn’t. In this section, we review and place in context transition relation and bisimulation theories of asynchronous π-calculus. We use in general Honda’s formulation, but stick sometimes to the more conventional syntax of Boudol.

Figure 1 illustrates the term language of asynchronous π-calculus. We distinguish between an alphabet for constants, ranged over by a, b, c and an alphabet for variables, ranged over by x, y, z. Names are either constants or variables; they are ranged over by u, v, w. Term forms include application uv, abstraction ux.P, parallel composition P | Q, the inert term 0 and name restriction νa.P. Replication ∗ux.P is restricted to abstraction terms. Replication is eager; that is, ∗ux.P is equivalent to arbitrarily many copies of ux.P executed in parallel. This is a minor deviation from the treatment of Honda and Yoshida, who consider lazy replication. As another minor change, we include a name matching construct [u ˆ= v]P. Honda and Yoshida also study this construct, but introduce it as an extension of ν-calculus proper.

The free names fn(P), and, analogously, the free constants fc(P) and free variables fv(P) of a term are defined as usual. We assume the following structural equivalences.

1. α-renaming:

νa.P ≡ νb.P [a := b] if b ^{∉} fc(P) ux.P ≡ uy.P [x := y] if y ^{∉} fv(P)

2. Abelian monoid laws for parallel composition:

P | Q ≡ Q | P,  (P | Q) | R ≡ P | (Q | R),  P | 0 ≡ P

3. Scope extrusion:

P | νa.Q ≡ νa.(P | Q) if a ^{∉} fc(P)

4. (Eager) input-replication:

∗ux.P ≡ ux.P | ∗ ux.P

5. The name matching law:

[a ˆ= a]P ≡ P

Reduction involves passing a name u from an output term au to an input term a?x.P. Reduction is asynchronous, i.e. , processes do not block on output:

(COM)  ax.P | au → P [x := u].

Reduction is considered modulo syntactic equivalence. Reduction can be applied anywhere in a term except under an abstraction or a matching:

(STR)  \frac{P′ ≡ P P → Q Q ≡ Q′}{P′ → Q′} ,
(NU)  \frac{P → Q}{νa.P → νa.Q} ,
(PAR)  \frac{P → Q}{P | R → Q | R} .

Let → → be the reflexive, transitive closure of reduction.

Starting with the definition of an observable action, we now adapt Honda’s formulation of asynchronous bisimulation to the reduction-based context that we follow here.

Definition 2.1 An output action α is one of ab, a(b) where a and b are names. A labeled transition relation ⟹^{α} is given by the rules:

(a) P ⟹^{ab} P′ if P → → ab | P′,

(b) P ⟹^{a(b)} P′ if P → → νb.(ab | P′).

Definition 2.2 A symmetric relation ∼ over closed terms is a (weak) asynchronous bisimulation if

P ∼ Q and P ⟹^{α} P′ implies Q ⟹^{α} Q′ for some term Q′ such that P′ ∼ Q′,

and

P ∼ Q implies P | ab ∼ Q | ab, for all names a, b.

Let asynchronous bisimilarity ≈_{a} be the maximal asynchronous bisimulation relation (which is shown to exist by a standard argument). Bisimilarity is extended to open terms by defining P ≈_{a} Q if P σ ≈_{a} Qσ, for all closing substitutions σ.

Theorem 2.3 (Honda) ≈_{a} is a congruence.

In fact, asynchronous bisimulation can be characterized as the largest congruence that satisfies the following two properties, see [4] for details.

(a) It is reduction closed: If P ≈_{a} Q and P → → P′ then there is a Q′ such that Q → → Q′ and P′ ≈_{a} Q′.

(b) It is sound: If P and Q are both insensitive (that is, neither can interact with its environment), then P ≈_{a} Q.

3 From asynchronous to polarized π.

We add polarities to the asynchronous π-calculus by introducing for every (unpolarized) constant a ^{∈} C_{a} an input constant a? and an output constant a!. Let C? be the set of all input constants and let C! be the set of all output constants. Then the set of all polarized constants C is C? ∪ C!.

In a slight misuse of notation, we also let letters a, b, c denote arbitrary (input or output) constants. Let a^{⊥} denote the complement of a constant a, that is, (a!)^{⊥} = a? and (a?)^{⊥} = a!.

Names and terms are defined as in asynchronous π, with the clarification that in the term νa.P, a is understood to be an unpolarized constant.

Syntactic Domains

Unpolarized Constants a, b, c ^{∈} C_{a}
Variables  x, y, z ^{∈} V
Names  u, v, w = a? | a! | x
Terms  P, Q, R = uv | ux.P | ∗ux.P | νa.P | P |Q | 0 | [u ˆ= v]P

Structural Equivalences

(α)  νa.P ≡ νb.P [a? := b?, a! := b!]  if b!, b? ^{∉} fc(P)
ux.P ≡ uy.P [x := y]  if y ^{∉} fv(P)
( | )  P | Q ≡ Q | P
(P | Q) | R ≡ P | (Q | R)
P | 0 ≡ P
(ν)  P | νa.Q ≡ νa.P | Q  if a ^{∉} fc(P)
(∗)  ∗ux.P ≡ ux.P | ∗ ux.P
( ˆ= )  [a! ˆ= a?]P ≡ P

Reduction

(COM)  a?x.P | a!u → P [x := u]

Fig. 2. The polarized π calculus

Alpha renaming is adapted to polarities as follows:

νa.P ≡ νb.P [a? := b?, a! := b!]  if b!, b? ^{∉} fc(P)
ux.P ≡ uy.P [x := y]  if y ^{∉} fv(P).

The other structural equivalences are as in asynchronous π, with the exception of name matching, which now requires both polarities of a name to be present:

[a! ˆ= a?]P ≡ P.

Reduction is sharpened by requiring the proper polarities in the terms that take part in a reduction:

(COM)  a?x.P | a!u → P [x := u].

The resulting calculus is summarized in Figure 2.

Examples.

1. A forwarder

F W D(a, b) =^{def} ∗a?x.b!x.

This term transmits all messages received from channel a to channel b.

2. An input term with wrong polarity a!x.0. This term is inactive; it can never react with its environment.

3. An inactive output term a?b, again with wrong polarity.

4. An identity tester

TEST(x, y).P =^{def} νc.(x(c!) | yz.P).

When applied to a constant and its negation — as in TEST(a!, a?).P — this construct enables execution of the term P, provided there are no other terms in the environment reading or writing a. The name matching construct [x ˆ= y]P has the same effect, but without the restrictions on the environment.

5. A bidirectional forwarder

EQ(a, b) =^{def} ∗a?x.b!x | ∗ b?x.a!x,

which, when present, would “fool” the identity tests TEST(a!, b?).P or TEST(b!, a?).P, but would not fool the matchings [a! ˆ= b?]P or [b! ˆ= a?]P.

4 Polarized Bisimulation

In this section, we develop a definition of process equivalence in polarized π. The equivalence is based on a refined notion of bisimulation. Asynchronous bisimulation is too discriminating for polarized π, since it assumes that the identity of all names passed out of a tested process can be determined. We do not want to make the environment more powerful than what can be expressed in a process context. Hence we insist that the identity of a name a be known to the environment only if the environment has knowledge of both polarities of a.

In the absence of full knowledge about the identity of names, the environment needs to carry along a hypothesis that describes what it knows about the names that take part in interactions. We formalize this idea as follows.

Definition 4.1 A correspondence hypothesis (or just correspondence) H is a finite relation over (C! × C!) ∪ (C? × C?) that satisfies

(a) if a! H b! and a? H c? then b = c,

(b) if b! H a! and c? H a? then b = c.

Let H be the set of all correspondence hypotheses. Let dom(H) be the set of polarized constants that are related on either side by H.

Essentially, a correspondence hypothesis records what an experimenter learns about anonymous names passed from the tested processes. In a bisimulation between P and Q, if process P passes out a constant a while process Q passes out b, then the correspondence (a, b) is added to the hypothesis. A hypothesis H is consistent if and only if every constant that exists in both polarities on one side of H corresponds precisely to another such constant on the other side. Consistency is enforced by the two conditions in the definition of correspondence hypotheses above.

Note the duality of correspondences to distinctions [11]: A correspondence records which names are surely equal, whereas a distinction records which names are surely different.

We now duplicate our development from Section 2 in working toward a definition of polarized bisimulation.

Definition 4.2 An output action α is one of ab, a(b), where a and b are constants. Given a hypotheses H, a labeled transition relation ⟹^{α}_{H} is defined as follows.

(a) P ⟹^{ab}_{H} P′ if P → → a!b | P′.

(b) P ⟹^{a(b)}_{H} P′ if P → → νb.(a!b | P′) and b, b^{⊥} ^{∉} dom(H).

Definition 4.3 Two output actions α_{1}, α_{2} are consistent with a correspondence H, in symbols α_{1} ↔_{H} α_{2}, if one of the following cases applies

\begin{matrix}a_{1}b_{1} & ↔_{H} & a_{2}b_{2} \\ a_{1}(b_{1}) & ↔_{H} & a_{2}b_{2} \\ a_{1}b_{1} & ↔_{H} & a_{2}(b_{2}) \\ a_{1}(b_{1}) & ↔_{H} & a_{2}(b_{2}) \end{matrix}

where a_{1}! H a_{2}! and H ∪ (b_{1}, b_{2}) is a correspondence. The refinement H.(α_{1}, α_{2}) of H by actions α_{1} and α_{2} is in each case H ∪ (b_{1}, b_{2}).

Definition 4.4 A family of relations {∼_{H} | H ^{∈} H} over closed terms is a polarized simulation if

P ∼_{H} Q and P ⟹^{α}_{H} P′ implies Q ⟹^{α′}_{H} Q′, for some action α′ such that
α ↔_{H} α′ and some term Q′ such that P′ ∼_{H.(α,α′)} Q′,

and

P ∼_{H} Q implies P | a_{1}!b_{1} ∼_{H∪(b_{1},b_{2})} Q | a_{2}!b_{2}, for all names a_{i}, b_{i} such that
a_{1} H a_{2} and b_{1} (H ∪ =) b_{2}.

{∼_{H} | H ^{∈} H} is a bisimulation iff {∼_{H} | H ^{∈} H} and {∼_{H}^{−1} | H ^{∈} H} are simulations.

We usually write just ∼ for the family {∼_{H} | H ^{∈} H}.

Definition 4.5 Two closed terms P, Q are bisimilar under a correspondence H, written P ≈_{H} Q, if there is a stable polarized bisimulation ∼ such that P ∼_{H} Q. Two open terms P, Q are bisimilar under H iff P σ_{1} ≈_{H} Qσ_{2} for all closing substitutions σ_{1}, σ_{2} such that (xσ_{1}) H (xσ_{2}), for all variables x.

Given a finite set of unpolarized constants A ⊆ C_{a}, let δ_{A} be the correspondence {(a, a) | a ^{∈} A! ∪ A?}. The full correspondence H(P_{1}, …, P_{n}) for terms P_{1}, …, P_{n} is given by

H(P_{1}, ..., P_{n}) = δfc(P_{1}, ..., P_{n}).

Definition 4.6 Two closed terms P, Q are bisimilar, written P ≈ Q, if P ≈_{H(P,Q)} Q. Two open terms P, Q are bisimilar iff P σ ≈ Qσ for all closing substitutions σ.

To distinguish between the versions of ≈ with and without a hypothesis index we will use the notation ≈ for the former. We now show some important properties of polarized bisimulations.

Lemma 4.7 Let a be a polarized constant such that a, a^{⊥} ^{∉} fc(P, Q) ∪ dom(H). Then

P ≈_{H} Q ⇔ P ≈_{H∪{(a,a)}} Q.

Proposition 4.8 The indexed relation ≈ is a polarized bisimulation.

Proof: Assume that P ≈_{H} Q and P ⟹^{α}_{H} P′. Then there exists a bisimulation ∼ such that P ∼_{H} Q. It follows that Q ⟹^{α′}_{H} Q′, for some action α′ such that α ↔_{H} α′ and some term Q′ such that P′ ∼_{H.(α,α′)} Q′. But then also P′ ≈_{H.(α,α′)} Q′. □

Proposition 4.9 ≈ is consistent: There are terms P, Q such that P ≉ Q.

Proof: Pick P ≡ 0, Q ≡ a!(a!). Then a!(a!) ⟹^{a!(a!)}_{H(0,a!(a!))} 0 but 0 ≠⟹^{a!(a!)}_{H(0,a!(a!))}.

Hence there is no polarized bisimulation ∼ such that P ∼_{H(0,a!(a!))} Q. □

The usefulness of ≈ for reasoning about process equivalences largely stems from the next result.

Theorem 4.10 The binary relation ≈ is a congruence.

Proof sketch: See appendix A. □

Like asynchronous bisimulation and barbed bisimulation, polarized bisimulation is reduction-closed:

Proposition 4.11 Let {∼_{H} | H ^{∈} H} be a polarized bisimulation. If P ∼_{H} Q and P → → P′ then there exists a term Q′ such that Q → → Q′ and P′ ∼_{H} Q′.

Proof: Let ∼ be a polarized simulation and let P, Q, H be such that P ∼_{H} Q and P → → P′. Pick a constant a such that a?, a! ^{∉} fc(P, Q). Then P | a!(a!) → → P′ | a!(a!),

hence P | a!(a!) ⟹^{a(a!)} P′. By the definition of polarized bisimulation, Q | a!(a!) ⟹^{α′} Q′, for some action α′ such that a(a!) ↔_{H} α′, and term Q′ such that P′ ∼_{H.(a(a!),α′)} Q′. The only such action is again a!(a!). That is, Q | a!(a!) → → Q′ | a!(a!). This implies with a! ^{∉} fc(Q) that Q → → Q′. □

Corollary 4.12 ≈ is reduction-closed: if P ≈ Q and P → → P′ then there exists a term Q′ such that Q → → Q′ and P′ ≈ Q′.

Proof: Assume P ≈ Q and P → → P′. By definition of ≈, P ≈_{H(P,Q)} Q. Since ≈ is a bisimulation, it follows with Proposition 4.11 that there is a term Q′ with Q → → Q′ and P′ ≈_{H(P,Q)} Q′. Since fc(P′, Q′) ⊆ fc(P, Q) the proposition then follows with Lemma 4.7. □

Definition 4.13 A term P can be observed at a constant a ^{∈} fc(P), written P ⇓_{a}, if P → → (a!u | P′) or P → → νu.(a!u | P′), for some name u and term P′. A term is insensitive, if it can be observed at no constant a.

Proposition 4.14 Let a be a constant. If P ⇓_{a} and P ≈ Q then Q ⇓_{a}.

Proof: Immediate from the definition of polarized bisimulation. □

Corollary 4.15 [12] Let P be an insensitive process. Then

P ≈ Q ⇔ Q is insensitive.

Hence, polarized bisimulation is a sound equivalence, in the sense of Honda and Yoshida. Proposition 4.14 also gives us a link to the other most important notion of process equivalence for polarized calculi, barbed bisimulation [12].

Definition 4.16 A symmetric relation ∼_{b} between polarized π terms is a (weak) barbed bisimulation if ∼_{b} is reduction-closed and P ∼_{b} Q and P ⇓_{a} implies Q ⇓_{a}, for all terms P, Q and constants a. Let ˙≈_{b} be the largest barbed bisimulation.

Unlike polarized bisimulation, barbed bisimulation is not a congruence. One therefore defines barbed congruence ≈_{b} to be the largest congruence contained in ˙≈_{b}. The next proposition states that polarized bisimulation is a barbed bisimulation, and therefore is finer than barbed congruence.

Proposition 4.17 ≈ is a barbed bisimulation.

Proof: By Corollary 4.12, ≈ is reduction-closed, and by Proposition 4.17 it preserves output events. □

In summary, we have arrived at a tractable definition of a congruence for processes that captures the notion of polarity in name accesses — “tractable” in that no quantification over all possible contexts is needed in proofs. In this sense, ≈ is the analogue of Honda and Yoshida’s asynchronous bisimulation [4], with which it also shares the properties of soundness and reduction-closedness.

A currently open question is whether, analogously to asynchronous bisimulation, polarized bisimulation is maximal among all consistent, sound and reduction-closed congruences for polarized π, or equivalently, whether polarized bisimulation and barbed bisimulation coincide.

5 Encoding of Computational λ-Calculus

In this section, we give an encoding of a sequential program calculus into polarized π, and study what happens to the program equalities in the translation. As the source of our translation, we use Moggi’s computational λ-calculus, λ_{c}. We concentrate on λ_{c}’s laws for function application and local definitions, which hold for a wide class of sequential programming languages, including languages with side-effects or non-determinism.

Terms  L, M, N ::= V | E
Values  V  ::= x | λx.M
Non-Values  E  ::= M N | let x = M in N

Equivalences

(β_{V})  (λx.M)V  = M[x := V]
(η_{V})  λx.V x  = V  (x ^{∉} fv(V))
(let_{V})  let x = V in M  = M[x := V]
(id)  let x = M in x  = M
(comp)  let y = let x = L in M in N = let x = L in let y = M in N
(let.1)  E M  = let x = E in xM  (x ^{∉} fv(M))
(let.2)  V E  = let x = E in V x  (x ^{∉} fv(V))

Encoding in π-Calculus

[[x]]k  = kx
[[λx.M]]k = νa.(k(a!) | ∗ a?(x, l).[[M]]l) (a fresh)
[[M N]]k  = νa.([[M]](a!) | ∗ a?x.νb.([[N]](b!) | ∗ b?y.x(y, k))) (a, b fresh)
[[let x = M in N]]k = νa.([[M]](a!) | ∗ a?x.[[N]]k)

Fig. 3. Moggi’s computational lambda calculus, λ_{c}.

By translating λ_{c} to polarized π we hope to find out which of these properties continue to hold in a process calculus. This stands in contrast to encodings such as Milner’s [9], Boudol’s [2], or Sangiorgi’s [19], which have worked with pure λ-calculi.

Figure 3 describes our source calculus and the encoding function. We work with the untyped version of λ_{c}, which is presented in Moggi’s technical report [13] but is omitted from his conference paper [14].

The encoding [[·]] of λ_{c} in polarized π takes an additional variable k as parameter, which determines where the result of a λ_{c}-term should be sent to. It differs from previous work [9, 19] in that the function and argument part of an application are evaluated in sequence. We will show below that this is necessary for preserving the (let.1) equivalence. The target language of the encoding is a polyadic calculus, where messages can be tuples of names. Tuples can be expanded out using the translations below.

\begin{aligned}a!(u, v) & = & νb.(a!b | b?x . (x!u | b?x . x!v)) \\ a?(x, y).M & = & a?z.νc.(z!c | c?x . (z!c | c?y.M)) \end{aligned}

This translation of pairs is a slight variation of Honda and Tokoro’s “zip-lock” technique^{1} [5]. We add an additional message exchange at the beginning of the communication, in order to keep the direction in which messages are sent over the common channel, a (in

1 Parallel compositions in the input term correspond to input prefixes in the output term and vice versa.

Honda and Tokoro’s original proposal this direction is reversed compared to single-name message exchanges).

Our first task will be to prove that the encoding maps the β-value reduction relation to a process equivalence. An important step on this way is the following contraction lemma.

Lemma 5.1 For all terms P, Q and constants a, b, c, d such that a?, b?, c!, c? ^{∉} fn(P, Q),

\begin{aligned}(i) & νa.νb.(P | ∗ a?x.Q | ∗ b?x.Q) & ≈ & νc.(P [a, b := c] | ∗ c?x.Q[a, b := c]) \\ (ii) & νa.(∗d?y.P | ∗ a?x.Q) & ≈ & ∗d?y.νa.(P | ∗ a?x.Q). \end{aligned}

Proof sketch: (i) Abbreviate the sides of the equation by defining R = P | ∗ a?x.Q | ∗b?x.Q and R′ = P [a, b := c] | ∗ c?x.Q[a, b := c]. Let

∼_{H} =^{def} \{ \begin{matrix}\{(νa.νb.R, νc.R′) & |a?, b?, c!, c? ^{∉} fn(P, Q)\}  if a! H̸c!, b! H̸c! \\ \{(νa.R, R′) & |a?, b?, c!, c? ^{∉} fn(P, Q)\}  if a! H̸c!, b!Hc! \\ \{(νb.R, R′) & |a?, b?, c!, c? ^{∉} fn(P, Q)\}  if a!Hc!, b! H̸c! \\ \{(R, R′) & |a?, b?, c!, c? ^{∉} fn(P, Q)\}  if a!Hc!, b!Hc! \end{matrix}

An analysis of possible reductions shows that {∼_{H} | H ^{∈} H} is a polarized bisimulation. This implies νa.νb.R ≈ νc.R′. An analogous proof shows (ii). □

Definition 5.2 Let =_{c} be the smallest congruence over λ_{c}-terms that contains the equalities (β_{V}), (let_{V}), (id), (comp), (let.1), (let.2).

Theorem 5.3 For any λ_{c} terms M, N and any constant a, if M =_{c} N then [[M]](a!) ≈ [[N]](a!).

Proof sketch: One shows that each of the generating equalities of =_{c} is a bisimulation. The proof for (β_{V}) makes use of the following equality, which relates substitutions in λ_{c} and polarized π:

[[M[x := λy.N]]](a!) ≈ νb.([[M]](a!)[x := b!] | ∗ b?(y, k).[[N]]k),

This equality is shown by a structural induction on M, using Lemma 5.1 for the steps that deal with parallel composition and replicated input. □

Note that the (let.1) equality requires a sequential left-to-right encoding of function application. If function-application was encoded as in [9, 19], where both function and argument evaluate in parallel, then E M and let x = E in xM would not have equivalent encodings. (To see why, substitute a non-terminating computation for E).

Note also that Theorem 5.3 does not extend to the η_{V} equality. A counterexample is:

[[λx.yx]](a!) ≈ νb.(a!(b!) | ∗ b?(x, k).y(x, k)) ≉ a!y = [[y]](a!)

The inequality can be observed by placing both sides in the context

c!(d!) | c?y.([ ] | a?z.[z ˆ= d?]e!(e!).

Why does η_{V} fail to hold? Essentially η_{V} is a completeness property; it states that every value is either a function or a variable that can be substituted only with functions. But a process context might substitute arbitrary names, including ones which can be tested for identity (and therefore cannot model a function).

6 Conclusion

We have proposed a refinement of name passing in the π-calculus where names carry polarities. We have shown that this refinement has a useful notion of bisimulation congruence which validates all observational equivalences of computational λ-calculus except η-value. An interesting topic for future work are encodings of other sequential constructs, such as those discussed in [20, 15]. In particular, we hope to find out more about which observational equivalences translate to polarized bisimulations between encoded terms.

Another open question concerns the relationship of polarized bisimulation with other notions of process equivalences. For the case without polarities, Honda and Yoshida have shown that asynchronous bisimulation includes all other consistent, sound and reduction-closed congruences. It remains to be seen whether a similar characterization holds for polarized bisimulation.

Acknowledgments

Thanks to John Maraist, David N. Turner and the anonymous referees for detailed and helpful comments.

References

1. Gérard Berry and Gérard Boudol. The chemical abstract machine. In Proc. 17th ACM Symposium on Principles of Programming Languages, pages 81–94, January 1990.

2. Gérard Boudol. Asynchrony and the pi-calculus. Research Report 1702, INRIA, May 1992.

3. U. Engberg and M. Nielsen. A calculus of communicating systems with label-passing. Report DAIMI PB-208, Computer Science Department, Aarhus University, 1986.

4. Keiho Honda and Nobuko Yoshida. On reduction-based process semantics. In Proc. 13th Conf. on Foundations of Softawre Technology and Theoretical Computer Science, pages 373–387, December 1993.

5. Kohei Honda and Mario Tokoro. An object calculus for asynchronous communication. In Proc. 5th European Conference on Object-Oriented Programming, pages 133–147, July 1991. Springer LNCS 512.

6. C.B. Jones. Process-algebraic foundations for an object-based design notation. Technical Report UMCS-93-10-1, University of Manchester, 1993.

7. Robin Milner. Functions as processes. Rapport de Recherche 1154, INRIA Sophia-Antipolis, February 1990.

8. Robin Milner. The polyadic π-calculus: A tutorial. Report ECS-LFCS-91-180, Laboratory for Foundations of Computer Science, Edinburgh University, October 1991.

9. Robin Milner. Functions as processes. Mathematical Structures in Computer Science, 2(2):119–141, 1992.

10. Robin Milner. Elements of interaction. Communications of the ACM, 36(1):78–89, January 1993. Turing Award lecture.

11. Robin Milner, Joachim Parrow, and David Walker. A calculus of mobile processes, part I and II. Report ECS-LFCS-89-85/86, Laboratory for Foundations of Computer Science, Edinburgh University, 1989.

12. Robin Milner and Davide Sangiorgi. Barbed bisimulation. In Automata, Languages, and Programming, 19th International Colloquium, 1992. Lecture Notes in Computer Science 623.

13. Eugenio Moggi. Computational lambda-calculus and monads. LFCS Report ECS-LFCS-88-66, University of Edinburgh, October 1988.

14. Eugenio Moggi. Computational lambda-calculus and monads. In Proceedings 1989 IEEE Symposium on Logic in Computer Science, pages 14–23. IEEE, June 1989.

15. Martin Odersky. Applying π: Towards a basis for concurrent imperative programming. In Proc. 2nd ACM SIGPLAN Workshop on State in Programming Languages, January 1995.

16. Benjamin Pierce and Davide Sangiorgi. Typing and subtyping for mobile processes. In IEEE Symposium on Logic in Computer Science, June 1993.

17. Benjamin C. Pierce, Didier Rémy, and David N. Turner. A typed higher-order programming language based on the Pi-calculus. Draft report; available in the PICT distribution, July 1993.

18. Davide Sangiorgi. Expressing Mobility in Process Algebras: First-Order and Higher-Order Paradigms. PhD thesis, Department of Computer Science, University of Edinburgh, 1992.

19. Davide Sangiorgi. An investigation into functions as processes. In Proc. 9th International Conference on the Mathematical Foundation of Programming Semantics, New Orleans, Louisana, pages 143–159, April 1993.

20. David Walker. π-calculus semantics of object-oriented programming languages. In Takayasu Ito and Albert R. Meyer, editors, Proc. Theoretical Aspects of Computer Software, pages 532–547. Springer-Verlag, September 1991. LNCS 526.

A Polarized Bisimulation is a Congruence

We sketch a proof of Theorem 4.10, which states that ≈ is a congruence. The proof is largely, but not completely, along the lines of [11].

We start with showing that ≈ is an equivalence relation. Given two bisimulations ∼^{1}, ∼^{2}, define their composition by

∼^{1} · ∼^{2} = {{(P, Q) | ∃H_{1}, H_{2}, R. H = H_{1} · H_{2}, P ∼_{H_{1}}^{1} R ∼_{H_{2}}^{2} Q} | H ^{∈} H}

Proposition A.1 The composition ∼^{1} · ∼^{2} of two polarized bisimulations ∼^{1} and ∼^{2} is a polarized bisimulation.

Proof sketch: A straightforward verification of closure properties. □

Proposition A.2 The binary relation ≈ is an equivalence relation.

Proof sketch: Only transitivity is nontrivial. Assume that P ≈_{H(P,R)} R and R ≈_{H(R,Q)} Q. Let H′ = H(P, Q, R). By Lemma 4.7, P ≈_{H′} R and R ≈_{H′} Q. Then by the definition of composition for bisimulations, P (≈ · ≈)_{H′} Q. By the other direction in Lemma 4.7, P (≈ · ≈)_{H(P,Q)} Q. Since ≈ · ≈ is a bisimulation, it follows that P ≈ Q. □

Proposition A.3 If P ≈ Q then

\begin{aligned}(a) & νa.P & ≈ & νa.Q \\ (b) & P | R & ≈ & Q | R \\ (c) & ux.P & ≈ & ux.Q \\ (c) & ∗ux.P & ≈ & ∗ux.Q \\ (e) & [u ˆ= v]P & ≈ & [u ˆ= v]Q. \end{aligned}

Proof sketch: (a) We show by an analysis of possible reductions that

∼ =^{def} {{(νa.P, νa.Q) | a!, a? ^{∉} dom(H) ∧ P ≈_{H∪δ_{{a}}} Q} | H ^{∈} H}

is a bisimulation.

(b) For sets of constants A = {a_{1}, ..., a_{n}}, let νA.P = νa_{1}…. νa_{n}.P. Using (a), we show by an analysis of possible reductions that

\begin{aligned}∼ & =^{def} & \{\{(νA.(P | R), νA.(Q | R′)) \\ & & | (A! ∪ A?) ∩ dom(H) = ∅ ∧ P ≈_{H∪δ_{A}} Q ∧ R ≈_{H∪δ_{A}} R′\} | H ^{∈} H\} \end{aligned}

is a bisimulation.

(c) We distinguish according to the kind of the name u. If u is a constant with output polarity, then ux.P ≈ 0 ≈ ux.Q. Assume now that u = a?, for some constant a. Let a state S be a parallel composition of zero or more output terms u_{1}v_{1} | … | u_{n}v_{n}. We show that

\begin{aligned}∼ & =^{def} & \{\{(a?x.P | S, a?x.Q | S′) \\ & & | S ≈_{H} S′ ∧ ∀u, v.uHv ⇒ P [x := u] ≈_{H} Q[x := u]\} | H ^{∈} H\} \end{aligned}

is a bisimulation, which implies the result. For variables u the result follows from the previous discussion and the definition of bisimilarity on open terms.

(d) The result follows from (b), (c) and the observation that, if ∗ux.P | Q → → R then there exist a number n ≥ 0 and a term R′ such that (ux.P)^{n} | Q → → R′ and R ≡ ∗ux.P | R′.

(e) If u = a! and v = b?, the result follows directly from the name matching law. If u and v are different constants, or constants with the wrong polarities, we have [u ˆ= v]P ≈ 0 ≈ [u ˆ= v]Q.. If u or v is a variable, the result follows from the previous discussion and the definition of bisimilarity on open terms. □

Proposition A.4 If P ≈ Q then P [x := u] ≈ Q[x := u].

Proof: Direct from the definition of ≈ for open terms. □

Theorem 4.10 ≈ is a congruence.

Proof: From Proposition A.2, Proposition A.3 and Proposition A.4. □