A Concurrent System of Multi-ported Processes
with Causal Dependency
Tatsuya Abe
December 18, 2004
Abstract
The pi-calculus is a concurrent system invented by Milner et al. in which concurrent
computation is expressed as interaction of processes through name-passing. Buildingon the concept of name-passing, we propose a new concurrent system based on multiports, whereas the pi-calculus is based on single-ports. Although our trial is not the firstone in constructing a concurrent system based on multi-ports, ours is unique in that it is
only extended in terms of multi-ports. This simplicity makes it possible to control selfcommunication of processes. Besides, it is an extension of the pi-calculus, because asingle-port can be expressed as a restriction in our system. These suggest that the conceptof multi-ports is natural. Furthermore, it is more expressive than other calculi including
the original pi-calculus in spite of this simplicity. Even the strong call-by-name lambdacalculus can be embedded into our system with respect to convergence and divergence,
while it has not been successfully done into the original pi-calculus.

1

Introduction

The pi-calculus was invented by Milner et al. as a model for expressing concurrent computation [16]. It has been studied actively in the field of concurrency due to its simplicity. As
a result, it has turned out that it can be extended in various directions and that it is far more
expressive than initially considered. In this paper we propose a new concurrent system, which
is built on the notion of name-passing as in the original pi-calculus. However, it is essentiallydifferent from previous approaches for extending the pi-calculus. We claim that our system ismore fundamental than the original one. The reason is that it is not only an extension of theoriginal pi-calculus but it can express the original one as syntax sugar. This is different fromother approaches, which tend to complicate the original pi-calculus by adding extra rules.
The most distinguishing feature of our system is that it is based on the concept of multiports. To make this point clear, we explain computation of the original pi-calculus. In theoriginal pi-calculus, a process transits to another by consuming a prefix of the process. For
instance,xy

xy.P −→ P .
Informally, xy.P means “send the name y along the link named x, and then enact P”. Here,xy.P is said to be an output process, and xy an output action. Similarly, x(y).P means “receive
some name z along the link named x, and then enact [z/y]P”. Here, [z/y]P denotes the resultof replacing occurrences of y with z in P. We call x(y).P an input process, and x(y) an input
action.

1Computation of the original pi-calculus is realized as interaction. An output process and an
input process which possess the same link name interact. The rule which expresses interaction
is as follows:
x(y)

xz

P −→ P0Q −−−→ Q0

.

τ

P|Q →
− P0 |[z/y]Q0
Here, P|Q stands for the parallel composition of two processes P and Q. The process P|Q cantransit as P or Q, and when the transition occurs in P, it is independent of Q, and vice versa.
Moreover, interaction between P and Q can occur when one is an output process and the otheris an input process which possess the same link name. In the case of internal interaction,τ
we use →− , where τ means an internal action. In the above rule, P can transit to P0 sending
the message z along the link named x, and Q can transit to [z/y]Q0 receiving the message z
along the link named x. Therefore, interaction can occur in P|Q, and P|Q itself can transit toP0 |[z/y]Q0 .
Let us now go back to the input processes, in which our system essentially differs from theoriginal pi-calculus. Milner explained the meaning of x(y).P as “receive any name along thelink named x, and then enact [z/y]P” [14]. However, one may observe that another meaning
is implicitly attached to it. That is temporal precedence. In addition to Milner’s explanation,
it is implicitly assumed that the x(y).P does nothing until it receives something along the link
named x. In other words, in the original pi-calculus a prefix of a process can be interpreted as
capsuling the process inside as follows:

vw
P

'$
v(w)

τ
Q
−
 →
&%
x(y)

R


P
xy

Q


P

τ

Q

→
−

x(y)

R


R

where double lines denote interactions. The interaction along the link named v strips theoutermost layer v(w) of the process v(w).xy.Q, and the layer xy appears. Once xy becomes
observable, an interaction occurs between xy.Q and x(y).R. Syntactically,ττ

vw.P|v(w).xy.Q|x(y).R →− P|xy.Q|x(y).R →− P|Q|R .
We claim that this idea restricts behavior of processes and interaction between processes. In
the above example, the interaction along the link named x does not affect the interaction along
the link named v if w is neither x nor y. There exists no a priori reason why we have to impose
the restriction that the interaction of v should be ahead of that of x. However, there exist
indeed some occasions where we have to impose an ordering on prefixes. A typical situation
is when a prefix binds a name occurring in some succeeding prefixes: for instance, consider
the process x(y).yz.0 where the first prefix binds a name in the second prefix. In this case, it is
impossible to have interaction for the second prefix first. This kind of precedence is essential.
We improve this point and design a new concurrent system, where the temporal precedence
in the original pi-calculus is replaced by causal dependency. In our system, interaction does2

not depend on the order of prefixes; interaction may occur as long as the causality conditionis satisfied. Interpreting a prefix of a process as a port along which it can interact, we regard
the original pi-calculus as a concurrent system in which a process has only one port. On theother hand, our system allows a process to have several ports, each of which can interact. In
this sense, processes in our system can be seen as multi-ported.
Let us now illustrate causality of prefixes visually. For instance, consider the processu(v):w(x):x(y):zx.0
in our system, where the names u, w, z, v, and x are distinct from one another. We use colon
notation x(y):P as an input prefix instead of dot notation x(y).P to stress that our input prefix
is different from that of Milner et al. It incorporates the capsuling facility intrinsically. The
following illustrates the causality relation among the prefixes of this process, where causalityof prefixes is denoted by edges.
u(v)

x(y)

w(x)

0
zx

As a matter of fact, both u(v) and w(x) are considered to be outermost prefixes while u(v) is
the only prefix in its counterpart of the original pi-calculus: u(v).w(x).x(y).zx.0. Returning to
the process vw.P|v(w):xy.Q|x(y):R, we can see that an interaction along the port x can precede
one along the port v while capsuling interpretation cannot be realized.
Causal dependency might be reminiscent of the notion of delayed input [23, 12], which isdifferent from ours in terms of self-communication. For instance, the delayed input processx(y):xz.P can transit to [z/y]P while it cannot in our system. However, we can express any
delayed input process, i.e., a process which can perform self-communication in different way
as described in Section 3. As a result, our system has the advantage that we can control
permission of self-communication.
In this paper, we also show that our system is more expressive than the original one.
Although it is known that the call-by-name, the call-by-value, and the strong call-by-value
lambda-calculi1 can be embedded into the original pi-calculus [14], we prove the fact that
not only those but also the strong call-by-name lambda-calculus can be embedded into oursystem naturally. In particular, it is remarkable that our embedding of the strong call-by-namelambda-calculus is complete with respect to convergence and divergence.
We use the following notation throughout this paper, for convenience. For any relation R,
the relations R∗ , R? , and R+ denote the reflexive and transitive closure, the reflexive closure,and the transitive closure of R, respectively. For any relations R and S, the relation R · S is
defined as follows:{ (P, R) | there exists Q such that (P, Q) ∈ R and (Q, R) ∈ S } .
Furthermore, we often use an infix notation for short, e.g., P → P0 denotes (P, P0 ) ∈ →.
This is a revised and expanded version of the work presented at the 2nd Asian Symposiumon Programming Languages and Systems [2].
1 Called the weak call-by-value lambda-calculus in the paper [14], in which evaluation strategy is more loose thanthat of the call-by-value lambda-calculus.

3

2

Syntax and Semantics

In this section, we introduce a concurrent system called Mpi-calculus. The Mpi-calculus isa modification of the pi-calculus, which is meant to capture the notion of multi-port. The
main difference from the pi-calculus is that single-ported input prefixes of the pi-calculus are
replaced by the multi-ported ones.
The Mpi-calculus is a concurrent system where processes interact through passing names
just as the pi-calculus. We presuppose an infinite set of names, and that x, y, . . . range over it.
The Mpi-calculus consists of a set of processes. The set of processes is defined as follows:
P, Q, . . . F 0 | τ.P | xy.P | x(y):P | P|Q | (νx)P | !P
where τ is a special constant which is distinct from the others. Unary connectives bind morestrongly than binary ones.
A process transits to another by consuming a prefix of the process. For instance,xy

xy.P −→ P .
Let us regard xy.P as a process which sends the name y along the link named x, and thenenact P. The process xy.P is said to be an output process, and xy an output prefix of theoutput process. Symmetrically, let us regard x(y):P as a process which receives some namez along the link named x, and then enact [z/y]P. Here, [z/y]P denotes the result of replacing
occurrences of y with z in P. We give the formal definition after we define substitution ofnames. We call x(y):P an input process, and x(y) an input prefix of the input process. Since
the occurrences of y in P of x(y):P only point at the locations into which a name received
along x passes, they are defined to be bound in x(y):P.
The connective | composes two processes in parallel in the Mpi-calculus. Two processes
connected by the parallel composition connective transit independently, and can interact if one
is an output process and the other is an input process which possess the same link name.
We explain the other connectives below. The process τ.P transits to P by performing anunobservable action τ. The process (νx)P is a process P whose port (or message) x is closed(or localized). Since this name x only points at the port (or message) which should be closed(or localized), the xs in P are bound just as in an input process. The process !P is a process
which is allowed to be copied arbitrarily many times.
The set of actions is defined as follows:α F τ | xy | x(y) | x(y) .
We define free names, and bound names of an action:
fn τ = ∅fn xy = {x, y}

fn x(y) = {x}fn x(y) = {x}bn τ = ∅bn xy = ∅bn x(y) = {y}bn x(y) = {y} .

The set n α of names, called names of α, is defined as fn α ∪ bn α. The set fn P consists of freenames of P out of the scopes of input prefixes and restriction connectives. A function σ fromnames to names is said to be a substitution if its support, written supp σ = { x | σx , x }, isfinite. The cosupport of a substitution, written cosupp σ, is defined as the image of its support.
The set n σ of names is supp σ ∪ cosupp σ. Naturally, any substitution can be extended on anaction. Formally,
σ(τ) = τσ(xy) = σxσy

σ(x(y)) = σx(y)4

σ(x(y)) = σx(y) .

In a similar way, a substitution replaces free occurrences in a process such that a new bindingαdoes not occur. We define a relation on processes, written →− , which we consider to be aαtransition. For instance, P →− P0 denotes that P transits to P0 by invoking an action α. We
define this by the notion of inference. Transition rules are as follows:
τ

xy

τ.P →
− P
α

xy.P −→ P

x < bn αP→− P0

z < (fn P \ {y}) ∪ {x}y < nααx(z)x(y):P →− x(y):P0
α

P→
− P0
α

x(y):P −−→ [z/y]Pxyx < nαz < fn P \ {y}

x(z)

0

(νx)P →− (νx)Pαx,yP −→ P0(νy)P −−→ [z/y]P0

bn α ∩ fn Q = ∅

P→
− P0

α

P|Q →
− P0 |Qx(y)xz

P −→ P0x(y)Q −−−→ Q0

P −−−→ P0τx(y)Q −−−→ Q0

τP|Q →− P0 |[z/y]Q0

P|Q →− (νy)(P0 |Q0 )

α

P→
− P0
α

!P →
− P0 |!Pxz

P −→ P0
τ

x(y)

x(y)

P −−−→ P00

P −−−→ P0
τ!P →− P0 |[z/y]P00 |!Px(y)P −−−→ P00!P →− (νy)(P0 |P00 )|!P

where symmetric and transitive ones are omitted. The annotation on a transition arrow is theaction which is performed. The output action x(y) is invoked by the process P when y is boundin P. The notion of output action of bound name realizes a natural interaction such that:τ(νy)xy.P|x(y):Q →− (νy)(P|Q) .
Let us consider the process v(w):x(y):wy.0 where the names are distinct from one another,in order to see that computation in our system differs from that of the original pi-calculus. The
two prefixes v(w) and x(y) in this process are independent. This process receives a name along
the link v as a name of its port and another name along the link x as a message along the link
not named yet. It is, therefore, natural that the order of interactions does not depend on thedenotation: v(w):x(y):wy.0. Indeed, the deduction:y < ({w, y} \ {y}) ∪ {x}x(y)x(y):wy.0 −−−→ wy.0

v,y
x(y)

w < {x, y}v(w):x(y):wy.0 −−−→ v(w):wy.0
ensures a transition on the basis of causal dependency.
αProposition 2.1. Suppose that P →− P0 .
1. bn α ∩ fn P = ∅ and (fn P0 \ bn α) ∪ fn α ⊆ fn P.
5

x(z)

2. α = x(y) and z < n P imply P −−→ [z/y]P0 .
x(z)3. α = x(y) and z < n P imply P −−→ [z/y]P0 .
σα

4. bn α ∩ (fn σP ∪ n σ) = ∅ implies σP −−→ σP0 .
α

Proof. By induction on P →− P0 .
We define an equational relation between processes that we would like to identify in the
concurrent system. The set of contexts is defined as follows:
C F [·] | τ.C | xy.C | x(y):C | C|P | P|C | (νx)C | !C
where [·] is a symbol denoting a hole of the process. When C is a context and P is a process,C[P] denotes the result of replacing P with the hole [·] in C.
Definition 2.2. A relation R on processes is called compatible if (P, Q) ∈ R implies (C[P], C[Q]) ∈R for every context C. An equivalence relation R on processes is said to be a congruence relation if R is compatible.
The structural congruence relation, written ≡, is defined as the smallest congruence relation that satisfies
1. P|0 ≡ P, P|Q ≡ Q|P, (P|Q)|R ≡ P|(Q|R),
2. (νx)(P|Q) ≡ P|(νx)Q if x < fn P, (νx)0 ≡ 0, (νx)(νy)P ≡ (νy)(νx)P,
3. !P ≡ P|!P.
Namely, the set of processes is a monoid with an operation | and a unit 0. In addition, the orderof closing ports are ignored, and closing a port is done only where the port exists. The rule 3means that the process !P is a process P which is allowed to be copied arbitrarily many times,
as already described.

3

ConservativenessIn the previous section, we constructed a concurrent system based on the notion of causality.
Recall that we have adopted unguarded input processes of the form x(y):P instead of guarded
processes of the form x(y).P. The Mpi-calculus does not have guarded input processes syntactically. However, guarded processes are expressed as macros of Mpi-processes as seen inthis section. In this sense, the Mpi-calculus does not abandon temporal precedence.
First, we define a concurrent system (indeed, Milner’s original pi-calculus) by replacing
input processes and their two rules with the ones of the form x(y).P and the following rule:z < (fn P \ {y}) ∪ {x}x(z).

x(y).P −−→ [z/y]PSecond, we define a translation h|·|i from pi-processes into Mpi-processes. With respect toguarded processes, it is as follows:h|x(y).P|i = (νu)(x(y):uy.h|P|i|u(y):0)
where u is fresh. The rest is the same as the original pi-calculus, i.e.,
h|0|i = 0h|τ.P|i = τ.h|P|i6h|xy.P|i = xy.h|P|i

h|P|Q|i = h|P|i|h|Q|ih|(νx)P|i = (νx)h|P|i

h|!P|i = !h|P|i .

Clearly, this translation preserves the free names of a process, and commutes with substitutions, that is, h|σP|i and σh|P|i are alpha-equivalent: they only differ from each other in the
choice of bound names. We often write P ≡α Q when P and Q are alpha-equivalent. Third, therelation 7→ is defined as the reflexive and transitive closure of the smallest compatible relationthat satisfies
1. P|0 7→ P, 0|P 7→ P,
2. (νx)P 7→ P if x < fn P.
The relation 7→ is as trivial as contained properly by the structural congruence relation ≡, andττcommutes internal actions, that is, P 7→ · →− P0 implies P →− · 7→ P0 . Finally, we give someτ
notion. It turns out that any internal transition →− is produced by a primitive action τ or aninteraction through a port. Now we annotate τ which is produced by an interaction througha port x as in xτ. Moreover, h|P|iτ is defined as the set of fresh names produced by h|P|i.
Sometimes, h|P|iτ denotes some element of h|P|iτ for short.
ααh|P|iτ

Theorem 3.1. If P →− P0 , then h|P|i →− · −−−→? · 7→ h|P0 |i.
αProof. By induction on P →− P0 it suffices to prove:xy

xy

1. If P −→ P0 , then h|P|i −→ h|P0 |i.
αh|P|iτ

α

2. If P →− P0 where α is x(y) or τ, then h|P|i →− · −−−→? · 7→ h|P0 |i.
x(z)Consider the case that x(y):P1 −−→ [z/y]P1 is inferred from z < (fn P1 \ {y}) ∪ {x}. Then,z < (fn uy.h|P1 |i \ {y}) ∪ {x}x(z)x(y):uy.h|P1 |i −−→ uz.[z/y]h|P1 |iz < {u}x(z)u < {x, y}x(y):uy.h|P1 |i|u(y):0) −−→ uz.[z/y]h|P1 |i|u(y):0)x(z)(νu)(x(y):uy.h|P1 |i|u(y):0)) −−→ (νu)(uz.[z/y]h|P1 |i|u(y):0))andy < (fn 0 \ {y}) ∪ {u}
u(y)

uz

uz.[z/y]h|P1 |i −→ [z/y]h|P1 |iu(y).0 −−−→ 0uτuz.[z/y]h|P1 |i|u(y):0 −→ [z/y]h|P1 |i|0uτ(νu)(uz.[z/y]h|P1 |i|u(y):0) −→ (νu)([z/y]h|P1 |i|0)
suffice to show the case since(νu)([z/y]h|P1 |i|0) 7→ [z/y]h|P1 |i ≡α h|[z/y]P1 |i .
τ

xz

x(y)

Next, consider the case that P1 |Q1 →− P01 |[z/y]Q01 is inferred from P1 −→ P01 and Q1 −−−→
x(y)

xz

h|Q1 |iτ

Q01 . By induction hypothesis, we have h|P1 |i −→ h|P01 |i and h|Q1 |i −−−→ R −−−−→? S 7→ h|Q01 |i forsome R and S . We therefore have:
x(y)

xz

h|P1 |i −→ h|P01 |ih|Q1 |i −−−→ Rτh|P1 |i|h|Q1 |i →− h|P01 |i|[z/y]R7.

h|Q1 |iτ

By Proposition 2.1.4, we have [z/y]R −−−−→? [z/y]S . Then,h|Q1 |iτ∅ ∩ fn[z/y]R = ∅[z/y]R −−−−→? [z/y]Sh|Q1 |iτ ?

.

h|P01 |i|[z/y]R −−−−→ h|P01 |i|[z/y]S
Since 7→ is closed under substitutions, we have:h|P01 |i|[z/y]S 7→ h|P01 |i|[z/y]h|Q01 |i ≡α h|P01 |[z/y]h|Q01 |i|i .
The other cases are trivial or similar to the above case.
This
claims that the Mpi-calculus is an extension of the original pi-calculus. Furthermore, we canknow the extension to be conservative2 by the following theorem.
αh|P|iτ

αLemma 3.2. If h|P|i →− P0 , then there exists P00 such that P →− P00 and P0 −−−→? · 7→ h|P00 |i.
αProof. By induction on h|P|i →− P0 , it is sufficient to prove:xy

xy

1. If h|P|i −→ P0 , then there exists P00 such that P −→ P00 and P0 = h|P00 |i.
αh|P|iτ

α

2. If α is x(y) or τ and h|P|i →− P0 , then there exists P00 such that P →− P00 and P0 −−−→? · 7→00
h|P |i.
x(z)Consider the case that h|x(y).P1 |i = (νu)(x(y):uy.h|P1 |i|u(y):0) −−→ (νu)(uy.h|P1 |i|u(y):0). By thedefinition,z < (fn P1 \ {y}) ∪ {x}x(z)x(y).P1 −−→ [z/y]P1
is inferred. Moreover,y < (fn 0 \ {y}) ∪ {u}
u(y)

uz

uz.[z/y]h|P1 |i −→ [z/y]h|P1 |iu(y):0 −−−→ 0uτuz.[z/y]h|P1 |i|u(y):0 −→ [z/y]h|P1 |i|0

u<∅

uτ

(νu)(uz.[z/y]h|P1 |i|u(y):0) −→ (νu)([z/y]h|P1 |i|0)and(νu)([z/y]h|P1 |i|0) 7→ [z/y]h|P1 |i|0 7→ [z/y]h|P1 |i ≡α h|[z/y]P1 |iτ

suffice to show the case. Consider the case that h|!P1 |i =!P2 →− P†2 |[z/y]P‡2 |!P2 is inferred from
xz

x(y)

P2 −→ P†2 and P2 −−−→ P‡2 . By induction hypothesis,xzP†2 = h|P††
1 |i

x(y)

P‡2 →
− ? 7→ h|P‡‡
1 |i

P1 −→ P††1τP1 −−−→ P‡‡1‡‡for some P††
1 and P1 . Then, we have:
x(y)

xz

P1 −→ P††
1

P1 −−−→ P‡‡
1

τ

‡‡
!P1 →
− P††
1 |[z/y]P1 |!P1
2 This terminology is proof-theoretically incorrect. It should be said that the translation h| · |i is complete. However,
we adopted it in order to emphasize regarding the original pi-calculus as a subsystem of the Mpi-calculus.

8

and
τ

‡
‡‡
††
‡‡
P†2 |[z/y]P‡2 |!P2 = h|P††− ? · 7→ h|P††
1 |i|[z/y]P2 |!P2 →1 |i|[z/y]h|P2 |i|!P2 ≡α h|P1 |[z/y]P1 |!P1 |i .

The other cases are trivial or similar to the above case.
α1

α2

αn

α1 ?

α2 ?

αn ?

Theorem 3.3. If h|P|i −−→ Q1 −−→ · · · −−→ Qn , then there exist P −−→ P1 −−→ · · · −−→ Pn andui τu1 , . . . , un ∈ h|P|iτ such that Qi −−→? · 7→ h|Pi |i for any i.
τProof. It follows from Lemma 3.2 and the commutativity of 7→ and →−.
Thesetwo theorems show that a process which has temporal precedence can be expressed in theMpi-calculus up to internal transitions and the relation 7→.
Fu [9], Parrow and Victor [17, 18], and other researchers studied causality of processes,
in particular van Breugel [23], and Merro and Sangiorgi [12] dealt with modifications of the
pi-calculus. Input processes can make the same transition as ours in their system. However,their systems have a rule which corresponds to the rule:xz

y < {x, z}

P −→ P0τ

.

x(y):P →− [z/y]P0This rule amounts to admitting self-communication of processes. Such an input process is said
to be a delayed input process. We cannot understand why they expressed causal dependency bydelayed input, since we do not know why self-communication is primitive and whether the delayed input can express a process without self-communication whose outermost prefixes havethe same link name. Here, we claim that our formalization of input processes is more naturalthan delayed input for the following reasons. First, consider the case where two identical processes on network are serving each other (as in peer-to-peer applications). In our system, they
can be naturally expressed as x(y):xz.P. Since self-communication is forbidden, the parallel
composition x(y):xz.P|x(y):xz.P can only transit to xz.[z/y]P|x(y):P (or the symmetric one)and then to [z/y]P|[z/y]P. On the other hand, in Merro and Sangiorgi’s system the problem isthat x(y):xz.P can transit to [z/y]P, that is, the process serves itself since self-communication
is primitive. In the case where each of the processes is also allowed to serve itself, they canbe expressed as x(y):P|xz.0 in our system (and also in Merro and Sangiorgi’s system). These
examples suggest that our system is more expressive than Merro and Sangiorgi’s, because
self-communication can be controlled by the form of processes. Second, we express a process
which can interact through outermost ports named x as x(y).P|xz.0 in our system (using thetranslation h|·|i). This fact suggests that our system has delayed input processes. Finally, Merroand Sangiorgi discovered that a delayed input process could be expressed as syntax sugar in
the localized asynchronous pi-calculus [12]. This fact claims that the localized asynchronouspi-calculus has causal dependency now that they realize causal dependency by delayed input. However, it appears that self-communication is admitted as a by-product—that a process
based on the notion of a single-port is forced to be multi-ported. In contrast, our system has
the advantage that we ourselves can choose whether to allow self-communication or not.3 On
the basis of these discussions, we cannot escape the conclusion that our formalization of input
processes is more natural than that of delayed input.
At the last of this section, we refer to other concurrent systems except the Mpi-calculus
with respect to controlling self-communication. As described above, we sometimes require a
3 Controlling self-communication of processes is one of the reasons that we do not construct a concurrent system
built on the notion of abstraction and concretion, for such a system forces x(y).(P|Q) ≡ P|x(y).Q whenever y < fn P.
Then, it is natural that the process x(y).xz.0 can be related to 0|0 by the relation → mentioned in Section 5. Such asystem is, therefore, not suitable for controlling self-communication of processes.

9

process which sends a message at one time, or receives a message at other times. We checked
it impossible to make such a process to avoid self-communication on many concurrent systems
without the nondeterministic choice operator + except the Mpi-calculus, for instance, the picalculus without +, pi-epsilon calculus [23], and localized asynchronous pi-calculus [12].
Formally, we proved:
Theorem 3.4. In the pi-calculus without +, pi-epsilon calculus, or localized asynchronous
xz

τ

x(y)

− P000 .
pi-calculus, if P −→ P0 and P −−−→ P00 , then there exists P000 such that P →4

Equivalence on Processes

In this section we introduce a notion of equivalence on processes. Our notion of equivalence
amounts to the so-called open bisimilarity.
The notion of equivalence is very important. For instance, let us think about the casewhere one part of a process needs to be replaced. Although it goes without saying that we
can replace it with the same one, there exist several situations where we would like to replace
it with something else which is equivalent to the original one, namely which has the same
capability as the original one. In order to formalize the notion of equivalence of processes
properly, we must consider what it means for two processes to have the same capability. Our
solution here is that two processes have the same capability when they behave in the sameway. The equivalence which we define in this section is based on this intuition; it is surely anequivalence on processes (i.e., a congruence relation on processes) as we prove later.

4.1

The Open Bisimilarity

The following notion of bisimulation is well-known.
Definition 4.1. A relation R on processes is said to be an open simulation if σ is a substitution,αα
σP →− P0 , (P, Q) ∈ R, and bn α ∩ (fn σP ∪ fn σQ) = ∅, then there exists Q0 such that σQ →− Q0and (P0 , Q0 ) ∈ R.
A relation R on processes is said to be an open bisimulation if R is an open simulation andso is R−1 . Two processes P and Q are said to be open bisimilar, written P ∼o Q, if (P, Q) ∈ R
for some open bisimulation R.
On the other hand, we define the following notion of bisimulation ad hoc (in fact, easierthan an open bisimulation to deal with at this time).
Definition 4.2. A relation R on processes is a hypersimulation whenever
1. R is closed under substitutions,α2. P →− P0 , bn α ∩ (fn P ∪ fn Q) = ∅, and (P, Q) ∈ R imply that there exists Q0 such thatαQ→
− Q0 and (P0 , Q0 ) ∈ R.
A relation R on processes is said to be a hyperbisimulation if R is a hypersimulation andso is R−1 . Two processes P and Q are said to be hyperbisimilar, written P ∼ Q, if (P, Q) ∈ R
for some hyperbisimulation R.
The following fact ensures that the relation ∼ is less of a trivial one.
Proposition 4.3. The relation ≡ is a hyperbisimulation.

10

Obviously, ∼ itself is a hyperbisimulation. It is, therefore, the greatest hyperbisimulation.
The notion of hyperbisimulation is different from that of open bisimulation; although any
hyperbisimulation is an open bisimulation, the converse does not hold, as we have a counterexample {(xy.0, xy.0), (0, 0)}. It is, however, not our intention to introduce a new notion ofequivalence. Indeed, it turns out that the notion of the hyperbisimilarity, which is the greatest
hyperbisimulation, coincides with that of the open bisimilarity:
Proposition 4.4. P ∼o Q if and only if P ∼ Q.
Proof. To prove that ∼o is contained in ∼, it is enough to show that for every open bisimulationO, its substitution closure O0 defined by{ (σR, σS ) | σ is arbitrary and (R, S ) ∈ O }is a hyperbisimulation. Let (P, Q) belong to some open bisimulation O. It is clear that O0 isαclosed under substitutions by the definition. Now suppose that (σR, σS ) ∈ O0 , σR →− R0 , and0bn α ∩ (fn σP ∪ fn σQ) = ∅. By the definition of O , we have (R, S ) ∈ O. It follows thatασS →− S 0 and (R0 , S 0 ) ∈ O since O is an open bisimulation. We therefore have (R0 , S 0 ) ∈O0 , which means that O0 is a hypersimulation. Similarly, we can check that O0 −1 is also a
hypersimulation.
To show the converse, it is enough to show that any hyperbisimulation is an open bisimuα
lation. Let R be a hyperbisimulation and suppose (P, Q) ∈ R, σP →− P0 , and bn α ∩ (fn σP ∪fn σQ) = ∅. Since R is closed under substitutions, we have (σP, σQ) ∈ R. Furthermore, there
αexists Q0 such that σQ →− Q0 and (P0 , Q0 ) ∈ R since R is a hyperbisimulation. This showsthat R is an open bisimulation. Similarly, we can check that R−1 is also an open bisimulation.
Now that we may discuss ∼ only. The following theorem is one part of main
theorem in this section.
Theorem 4.5. The relation ∼ is an equivalence relation.
Proof. Reflexivity and symmetricity are trivial. To show transitivity, it is sufficient to checkthat whenever R and S are hyperbisimulations, R · S is also a hyperbisimulation.
It is obvious that R · S is closed under substitutions. Now, suppose that (P, R) ∈ R · S,x(y)P −−−→ P0 and y < fn P∪fn R. There exists Q such that (P, Q) ∈ R and (Q, R) ∈ S. Without lossof generality, we may assume that y < fn Q; otherwise, let σ be a substitution which replaces
y with a fresh name y0 . Note that σP = P and σR = R. Since R and S are hyperbisimulations,
we have (P, σQ) ∈ R and (σQ, R) ∈ S, and clearly y < fn σQ. Now, there exists Q0 such that
x(y)

x(y)

Q −−−→ Q0 (or σQ −−−→ Q0 in case y ∈ fn Q) and (P0 , Q0 ) ∈ R. Similarly, there exists R0 suchx(y)that R −−−→ R0 and (Q0 , R0 ) ∈ S. We can therefore conclude that (P0 , R0 ) ∈ R · S.
αOther cases where P →− P0 with α not an input action are similar.

4.2Up-to TechniqueIn this subsection we prove several lemmata which are useful for showing that two processes
are hyperbisimilar. In general, how to prove whether two processes are bisimilar is one of themost interesting topics in concurrency field. The first approach was done by Milner against
a concurrent system called Calculus of Communication System [13]. The method is called
up-to ∼ technique, in which the closure of a bisimulation is achieved up to the bisimilarity
itself. The method was spread to the weak bisimilarity version [20]. While these methods
are compositional to the original relation in a sense, up-to restriction technique [16] and up-to11

injection technique [7, 16] are contextual. Extending these techniques, Sangiorgi succeededin establishing a series of lemmata to prove two processes related contextually to be bisimilar[19]. The content of this subsection is largely due to Sangiorgi’s up-to context technique[19, 21], though accommodated to our notion of hyperbisimulation.
Definition 4.6. A relation R progresses to a relation S, written R  S, if R and S are closed
under substitutions and whenever (P, Q) ∈ R and bn α ∩ (fn P ∪ fn Q) = ∅,
α

α

α

α

1. P →− P0 implies there exists Q0 such that Q →− Q0 and (P0 , Q0 ) ∈ S.
2. Q →− Q0 implies there exists P0 such that P →− P0 and (P0 , Q0 ) ∈ S.
We emphasize that when we write R  S, it is assumed that R and S are closed undersubstitutions. This is an accommodation to our notion of hyperbisimulation and the only
different point from existing works.
Proposition 4.7. If R progresses to a hyperbisimulation, then R is contained in ∼.
Proof. Let S be a hyperbisimulation such that R  S. It is sufficient to show that R ∪ S is a
hyperbisimulation. Notice that the hypothesis forces R ∪ S closed under substitution. Supposeαthat P →− P0 , bn α ∩ (fn P ∪ fn Q) = ∅, and (P, Q) ∈ R ∪ S. In the case of (P, Q) ∈ R, there
αexists Q0 such that Q →− Q0 and (P0 , Q0 ) ∈ S by R  S. On the other hand, in the case of(P, Q) ∈ S, it also holds since S is a hypersimulation. Hence, R ∪ S is a hypersimulation.
Similarly, (R ∪ S)−1 is also a hypersimulation.

Lemma 4.8. Let R, S, T , Ri , and S j be relations.
1. Suppose that R is closed under substitutions. Then R ⊆ S and S  T imply R  T .
2. Suppose that T is closed under substitutions. Then R  S and S ⊆ T imply R  T .
3. Suppose that S j is closed under substitutions for any j ∈ J, and for each i ∈ I there
S
S
exists j ∈ J such that Ri  S j . Then { Ri | i ∈ I }  { S j | j ∈ J }.
S
4. Suppose that for each i ∈ I there exists i0 ∈ I such that Ri  Ri0 . Then { Ri | i ∈ I } isa hyperbisimulation.
α

Proof. 1. The hypothesis makes T closed under substitutions. Suppose that P →− P0 andα00(P, Q) ∈ R. We have (P, Q) ∈ S by R ⊆ S. There exists Q such that Q →− Q and (P0 , Q0 ) ∈ T
αby S  T . It is similar in the case of Q →− Q0 .
2. It is easy to check.
S
S
3. It is obvious that { S j | j ∈ J } is closed under substitutions. Let (P, Q) ∈ { Ri | i ∈ I }.
Then, there exists i ∈ I such that (P, Q) ∈ Ri . By the hypothesis, there exists j ∈ J such thatααRi  S j . Suppose that P →− P0 , then there exists Q0 such that Q →− Q0 and (P0 , Q0 ) ∈ S j .
S
αHence, (P0 , Q0 ) ∈ { S j | j ∈ J }. It is similar in the case of Q →− Q0 .


4. This is a special case of 3.

Definition 4.9. A function F on relations on processes is said to be monotonic if R  S
implies F(R)  F(S).

12Proposition 4.10. A monotonic function F preserves closure property under substitution, thatis, if R is closed under substitutions, then F(R) is closed under substitutions.
Proof. Since R is closed under substitutions, we have ∅  R. Hence, it turns out that F(∅) 
F(R), especially that F(R) is closed under substitutions.

Proposition 4.11. If F is a monotonic function such that R  F(R), then R ⊆ ∼.
Proof. We define the relations Rn (0 ≤ n ≤ ω) as follows:
R0 = R
Rn+1 = Rn ∪ F(Rn )[Rω ={ Ri | 0 ≤ i < ω } .
We first show Rn  Rn+1 for any n by induction on n. Suppose n = 0. The hypothesis derives
R0  F(R0 ) ⊆ R1 . Since R1 is closed under substitutions, Lemma 4.8.2 induces R0  R1 .
Suppose n > 0. Induction hypothesis and the monotonicity of F derive F(Rn−1 )  F(Rn ) .
Hence Rn  Rn+1 holds by Lemma 4.8.3.
By Lemma 4.8.4, it follows that Rω is a hyperbisimulation. Moreover, we obtain R  Rω
by applying Lemma 4.8.2 to R  R1 ⊆ Rω . As a consequence, we have R ⊆ ∼ by Proposition
4.7.
Next, let us describe several ways to construct new monotonic functions from givenSones. The composition F · G and the union { Fi | i ∈ I } are defined as follows:(F · G)(R) = F(R) · G(R)[[
( { Fi | i ∈ I })(R) ={ Fi (R) | i ∈ I } .
Lemma 4.12. Let F, G, and Fi be monotonic.
1. F · G is monotonic.
S
2. { Fi | i ∈ I } is monotonic.
Proof. Suppose R  S.
1. Let (P, R) ∈ (F·G)(R). Since F(R) and G(R) are closed under substitutions, so are (F·G)(R)αand (F · G)(S). Let P →− P0 , bn α ∩ (fn P ∪ fn R) = ∅, and (P, R) ∈ (F · G)(R). By the definition,
there exists Q such that (P, Q) ∈ F(R) and (Q, R) ∈ G(R). Without loss of generality, we may
assume that bn α and fn Q are disjoint (otherwise, let σ be a substitution which replaces bn αwith a fresh name and consider σQ as in the proof of Theorem 4.5). Then, there exists Q0 suchααthat Q →− Q0 and (P0 , Q0 ) ∈ F(R). Thus, there exists R0 such that R →− R0 and (Q0 , R0 ) ∈ G(S).
α− R0 .
The existence of Q0 ensures (P0 , R0 ) ∈ (F · G)(S). It is similar in the case of R →2. By Lemma 4.8.3.
Finally, let us give some concrete examples of monotonic functions, which are useful when
confirming that two processes are hyperbisimilar. First of all, let K be a constant function to∼, i.e., K(R) = ∼ for any R. Next, define N as follows:
N(R) = { ((νy)P, (νy)Q | (P, Q) ∈ R and y is arbitrary } .
Two processes (νy)P and (νy)Q are said to be hyperbisimilar up to restriction when P and
Q are hyperbisimilar. The importance of the monotonicity of this function N depends on theexistence of the rule:
13

x(y)

P −−−→ P0x(y)Q −−−→ Q0

τ

.

P|Q →
− (νy)(P0 |Q0 )In general, we expect that two processes hyperbisimilar up to context are hyperbisimilar. Unfortunately, however, the following function is not monotonic:
O(R) = { (C[P], C[Q]) | C is a context and (P, Q) ∈ R } .
The failure is due to replication, i.e., copying processes. To see this, let P be xy.0 and Q be
xy.0|0, and the relation R be{(0, 0|0)} ∪ { (xy.0, xy.0|0) | x and y are arbitrary } .
xyIt immediately turns out that R  R, (!P, !Q) ∈ O(R) and !P −→ 0|!xy.0. However, the onlytransitions from !Q is the following:xy!Q −→ 0|0|!(xy.0|0) C Q0 .
Obviously, there exist no context C and (R, S ) ∈ R such that P0 = C[R] and Q0 = C[S ].
Therefore, it follows that (P0 , Q0 ) < O(R), and thus O is not monotonic.
It is nevertheless possible to maintain our intuition that two processes should be hyperbisimilar whenever they are hyperbisimilar up to context. The idea is to extend the previous
definition of O based on single-hole contexts to a more general one based on multi-hole contexts.
A multi-hole context is a process which has some indexed holes. More precisely, the setof multi-hole contexts is defined by
C, D, . . . F P | [·]i | τ.C | xy.C | x(y):C | C|D | (νx)C | !C
where i is a natural number. Let C be a multi-hole context with its maximal index n. Let P
denote a sequence P1 , . . . , Pn of processes. Then C[P] denotes the result of substituting Pi for[·]i for every i ≤ n. Note that a multi-hole context is allowed to have several occurrences ofa hole [·]i with the same index i. In such a case, C[P] is obtained by substituting Pi for all
occurrences of [·]i .
Define M by
M(R) = { (C[P], C[Q]) | C is a multi-hole context and (P, Q) ∈ R } .
Proposition 4.13. K and M are monotonic.
Proof. First, K is monotonic since it is a constant function and ∼ is a hyperbisimulation.
Next, we show that M is monotonic. Suppose R  S. Obviously, M(R) and M(S) areclosed under substitutions. It is therefore left to check that whenever (P, Q) ∈ R , ∅ andααC[P] →− P0 where bn α ∩ (fn C[P] ∪ fn C[Q]) = ∅, there exists Q0 such that C[Q] →− Q0 and(P0 , Q0 ) ∈ M(S). We prove this by induction on multi-hole context C.
Case 1. It is obvious in case there exists no hole.
Case 2. Suppose that C is [·]i . Then C[P] and C[Q] are Pi and Qi , respectively. Sinceα(Pi , Qi ) ∈ R  S, there exists Q0 such that Qi →− Q0 and (P0 , Q0 ) ∈ S ⊆ M(S).

14αCase 3. Suppose that C is α.C 0 . Then the only possible transition is α.C 0 [P] →− C 0 [P]. In this
α
0
0
0
0
case, we have α.C [Q] →− C [Q]. It follows that (C [P], C [Q]) ∈ M(R) ⊆ M(S).
Case 4. C is x(y):C 0 . Let us write x(y):C 0 [P] and x(y):C 0 [Q] to be x(y):P and x(y):Q, respecx(z)tively. The proof is similar to the above when x(y):P −−→ [z/y]P since M(R) is closed underααsubstitution. So, suppose that x(y):P →− x(y):P0 is inferred from P →− P0 , x < bn α and y < n α.
Clearly bn α and fn P ∪ fn Q are disjoint. By induction hypothesis, there exists Q0 such thatααQ→
− Q0 and (P0 , Q0 ) ∈ M(S). Hence, x(y):Q →− x(y):Q0 and (x(y):P0 , x(y):Q0 ) ∈ M(S), since
M(S) is closed under the input prefixes x(y).
Case 5. Suppose that C is !C 0 . Let us write !C 0 [P] and !C 0 [Q] to be !P and !Q, respectively.
ααThere are three subcases. First, suppose that !P →− P0 |!P is inferred from P →− P0 . Byαinduction hypothesis, there exists Q0 such that Q →− Q0 and (P0 , Q0 ) ∈ M(S). Hence, it can beαinferred that !Q →− Q0 |!Q. Furthermore, we have (P0 |!P, Q0 |!Q) ∈ M(S).
τ

x(y)

xz

Next, !P →− P1 |[z/y]P2 |!P is inferred from P −→ P1 and P −−−→ P2 . Without loss ofgenerality, we may assume that y < fn Q (otherwise, choose an alpha-convertible variant of Q
which does not contain y as bound name). By induction hypothesis, there exist Q1 and Q2 such
x(y)

xz

that Q −→ Q1 , (P1 , Q1 ) ∈ M(S), Q −−−→ Q2 , and (P2 , Q2 ) ∈ M(S). Hence it can be inferredτthat !Q →− Q1 |[z/y]Q2 |!Q. Furthermore, we have (P1 |[z/y]P2 |!P, Q1 |[z/y]Q2 |!Q) ∈ M(S). The
last subcase is similar to this case.
The other cases are similar, too (apply the alpha-conversion argument used in Case 5, if
necessary).


4.3

Main Theorems

Having developed some useful lemmata, we are now ready to prove:
Theorem 4.14. The relation ∼ is a congruence relation.
Proof. First, we show that ∼ is closed under the non-input prefixes α. Let R be
∼ ∪ { (β.R, β.S ) | R ∼ S and β is the same prefix form as α } .
It is sufficient to show that R progresses to ∼; then it follows from Proposition 4.7 that R ∼ S
implies (α.R, α.S ) ∈ R ⊆ ∼. Clearly R is closed under substitution. Let (P, Q) ∈ R. WhenβP ∼ Q, it follows from the definition of ∼ that whenever P →− P0 and bn β ∩ (fn P ∪ fn Q) = ∅,βthere exists Q0 such that Q →− Q0 and P0 ∼ Q0 . Otherwise, P and Q are of the form β.R andββ.S , respectively. Note that the only possible transition from β.R is β.R →− R, and similarly theβonly possible transition from β.S is β.S →− S . Furthermore, R ∼ S by the definition of R. This
(as well as the symmetric case) shows that R progresses to ∼.
Second, we show that ∼ is closed under the input prefixes x(y). Let R be
∼ ∪ { (v(w):R, v(w):S ) | R ∼ S and v and w are arbitrary } .
It is sufficient to show that R is a hyperbisimulation; then R ∼ S implies (x(y):R, x(y):S ) ∈R ⊆ ∼.
Clearly R is closed under substitutions. Let (P, Q) ∈ R. The case P ∼ Q is similar to theabove. Otherwise, P and Q are of the form v(w):R and v(w):S , respectively. The proof is alsov(z)similar to the above in the case of v(w):R −−→ [z/w]R. Consider
15

α

R→
− R0

v < bn ααw < nαv(w):R →− v(w):R0

We may suppose that bn α and fn v(w):R ∪ fn v(w):S are disjoint. The definition of R derives
R ∼ S . Furthermore, it is clear that bn α and fn R∪fn S are disjoint. Hence there exists S 0 suchααthat S →− S 0 and R0 ∼ S 0 , so it can be inferred that v(w):S →− v(w):S 0 and (v(w):R0 , v(w):S 0 ) ∈R. This (as well as the symmetric case) shows that R is a hyperbisimulation.
Finally, we show that ∼ is closed under parallel compositions. Other cases are easier than
this case. Let R be
∼ ∪ { (P|R, Q|R) | P ∼ Q and R is arbitrary } .
It is sufficient to show that R progresses to M(R); then it follows from Proposition 4.11 thatP ∼ Q implies (P|R, Q|R) ∈ R ⊆ ∼.
Let (P|R, Q|R) ∈ R with P ∼ Q. There are six subcases.
ααFirst, suppose that P|R →− P0 |R is inferred from P →− P0 and bn α ∩ fn R = ∅. We may alsoαassume that bn α ∩ (fn P|R ∪ fn Q|R) = ∅. Since P ∼ Q, there exists Q0 such that Q →− Q0 and0000
P ∼ Q . Hence, (P |R, Q |R) ∈ R ⊆ M(R).
ααSecond, suppose that P|R →− P|R0 is inferred from R →− R0 and bn α ∩ fn P = ∅. We stressαthat we may assume that bn α ∩ (fn P|R ∪ fn Q|R) = ∅. Then, it is easy to see that Q|R →− Q|R000and (P|R , Q|R ) ∈ R ⊆ M(R).
τ

x(y)

xz

Third, suppose that P|R →− P0 |[z/y]R0 is inferred from P −→ P0 and R −−−→ R0 . Sinceτxz

P ∼ Q, there exists Q0 such that Q −→ Q0 and P0 ∼ Q0 . Therefore, we have Q|R →− Q0 |[z/y]R00000
and (P |[z/y]R , Q |[z/y]R ) ∈ R ⊆ M(R).
τ

x(y)

xz

Fourth, suppose that P|R →− [z/y]P0 |R0 is inferred from P −−−→ P0 and R −→ R0 . Let w bex(w)a fresh name. Proposition 2.1.3 induces P −−−→ [w/y]P0 . Since P ∼ Q, there exists Q0 suchτx(w)that Q −−−→ Q0 and [w/y]P0 ∼ Q0 . It follows that Q|R →− [z/w]Q0 |R0 . Since ∼ is closed under00
substitutions, [z/w]([w/y]P ) ∼ [z/w]Q . Therefore, ([z/y]P0 |R0 , [z/y]Q0 |R0 ) ∈ R ⊆ M(R).
τ

x(y)

x(y)

Fifth, suppose that P|R →− (νy)(P0 |R0 ) is inferred from P −−−→ P0 and R −−−→ R0 . As before,
we may assume that y < fn P ∪ fn Q without loss of generality. Since P ∼ Q, there exists Q0τx(y)− (νy)(Q0 |R0 ) and ((νy)(P0 |R0 ), (νy)(Q0 |R0 )) ∈such that Q −−−→ Q0 and P0 ∼ Q0 . Hence, Q|R →
M(R).
τ

x(y)

x(y)

Sixth, suppose that P|R →− (νy)(P0 |R0 ) is inferred from P −−−→ P0 and R −−−→ R0 . As before,x(y)we may assume that y < fn P ∪ fn Q. Since P ∼ Q, there exists Q0 such that Q −−−→ Q0 andτ
P0 ∼ Q0 . Hence, Q|R →− (νy)(Q0 |R0 ) and ((νy)(P0 |R0 ), (νy)(Q0 |R0 )) ∈ M(R).

We have succeeded in defining a notion of equivalence on processes with causal dependency. Thus v(w):x(y):P ∼ x(y):v(w):P claims that these two input prefixes are independent.
Remarkably, two processes identified under considering causal dependency are exactly equivalent.
Next, we show an important property for concurrent systems. The following statement iscalled the replication theorem:(νx)(P|Q|!x(y).R) ∼ (νx)(P|!x(y).R)|(νx)(Q|!x(y).R) .
This statement is intuitively interpreted as follows. Let R be a resource which is used byother processes. It is natural to think of R as replicable since it is expected to be invoked out
arbitrarily many times. On the left-hand side, P and Q share R, while on the right-hand side, P
and Q have their own copies of R. The above statement thus claims that whenever a resource16

is shared by two processes, the resource may be distributed to each of the processes. However,this does not hold in general. Typically it does not hold when the processes involved send x as
message. Since the name x is expected to serve as a “guard” for the resource R, we restrict it
used only for the purpose. This is also why we do not use colon prefixes but dot prefixes.
A process P is said to be x-negative if x occurs in P only in the form xy. A process whichis alpha-convertible to an x-negative process is also considered to be x-negative.
Theorem 4.15. Let P, Q, and R be x-negative.
1. (νx)(P|Q|!x(y).R) ∼ (νx)(P|!x(y).R)|(νx)(Q|!x(y).R).
2. (νx)(!P|!x(y).R) ∼ !(νx)(P|!x(y).R).
Theorem 4.15 is used in the later section, where we consider convergence and divergenceof processes. In the section, resources are considered to be environments in which a programis evaluated.
So far, we have been mainly interested in symmetric relations. However, the following
relation, which may also be considered to be a sort of “equivalence” in some weak sense, isasymmetric. More precisely, it is a hypersimulation and the inverse of it is a hypersimulation
up to internal actions.
Definition 4.16. A relation R is an expansion if R is closed under substitutions and whenever(P, Q) ∈ R and bn α ∩ (fn P ∪ fn Q) = ∅,
α

α

α

b
α

1. P →− P0 implies that there exists Q0 such that Q ⇒ Q0 and (P0 , Q0 ) ∈ R,
2. Q →− Q0 implies that there exists P0 such that P →− P0 and (P0 , Q0 ) ∈ R,
α

b
τ

τ

α

τ

τ

b
α

α

where ⇒ and →− denote →
−∗ ·→
− ·→
− ∗ and →− ? respectively, and →− denotes →− for α , τ.
We say that Q expands P, written Q  P, if (P, Q) ∈ R for some expansion R.
Definition 4.17. A reflexive and transitive relation R on processes is said to be a precongruence relation if R is compatible.
Theorem 4.18. The relation  is a precongruence relation.

5

Correspondences to Functional Languages

The call-by-name and the call-by-value lambda-calculi are lambda-calculi whose evaluation
strategies are fixed. It is important to gain knowledge of these calculi since strictness of theirevaluation strategies makes them pragmatic. As part of it, Milner discovered that the call-byname, the call-by-value, and the strong call-by-value lambda-calculi can be embedded into
his original pi-calculus with the construction [14]. Here, it is of theoretical interest to bringup the strong call-by-name lambda-calculus whose evaluation strategy is more loose than thatof the call-by-name lambda-calculus, for the following facts are well-known: (1) lambdadefinable functions in the lambda-calculus with full reductions are computable and vice versa(Church’s thesis); (2) the definition of lambda-definability depends on whether can be reacheda normal form in the lambda-calculus with full reductions, called normalizability; and (3) anormalizable term is also normalizable in the strong call-by-name lambda-calculus but not inother three ones (the standardization theorem [8]).
In the following, our goal is that not only the three calculi as described but also the strong
call-by-name lambda-calculus can be embedded into the Mpi-calculus. The achievement immediately induces:17

1. name-passing: the fundamental operation on concurrent systems is so expressive as tosimulate the so-called beta-reduction on lambda calculi;
2. the expressive power of the Mpi-calculus is equal to or more than that of Turing machine.
In fact, it is obvious that the call-by-name, the call-by-value, and the strong call-by-value
lambda-calculi can be embedded into our system with respect to convergence and divergence
between reaction and reduction, since Milner has already shown that these three calculi can beembedded into his original pi-calculus and we have already proved that our system is conservative to Milner’s original pi-calculus in Section 3. Therefore, only the strong call-by-namelambda-calculus remains.

5.1

The Strong Call-by-Name Lambda-Calculus

We define lambda-terms and reduction rules in the strong call-by-name lambda-calculus asfollows:
M, N, . . . F x | λx.M | MN
M →λ M 0
M →λ M 0(λx.M)N →λ [N/x]M0λx.M →λ λx.M
MN →λ M 0 N
and borrow various notation and terminology of lambda-calculi from Barendregt’s encyclopedic book [3]. The difference from the call-by-name lambda-calculus is the existence of thesecond rule. The rule permits a function to reduce to one which returns the same output as it
for any input, that is, it enforces extensionality of functions. We prove the following lemma in
advance.
Lemma 5.1. If M →λ M 0 , then [N/x]M →λ [N/x]M 0 .
Proof. By induction on M →λ M 0 .
Next, we introduce a translationfrom lambda-terms into Mpi-processes. This translation reflects the lambda-reduction to theτrelation →− up to the structural congruence relation ≡, which is called reaction and denoted by→. To show this, we assume that the Mpi-calculus has polyadicity [15], that is, it permits afixed number of names along one port. For instance,
xyz.P|x(vw):Q → P|[y/v, z/w]Q
where it is assumed that [y/v, z/w] is not sensitive to the order of substitutions.
We give a translation from lambda-terms into Mpi-processes:~xu = xu.0
~λx.Mu = u(xv):~Mv~MNu = (νv)(~Mv |(νv0 )(vv0 u|~v0 B N))~v0 B N = !v0 (v00 ).~Nv00
which is a modification of Milner’s call-by-name translation [14]. Both translations are basedon the notion that functions are programs and their arguments are environments in which they
are evaluated. These ones translate a function (i.e., a body of a program) and its argument into
an input process and its resource, respectively. Ours differs from Milner’s only in lambdaabstraction. We adopt input processes under consideration of causal dependency while Milner
did guarded input processes. The reader sees that unguardedness of our input processes tointernal actions makes it to simulate extensionality of functions.
In the following, we often omit an index of translations when it is clear from the context.
18

Lemma 5.2. ~(λx.M)N → ·  ~[N/x]M.
Proof. We may assume x < fv N. Since we have:~(λx.M)Nu = (νv)(v(xv00 ):~Mv00 |(νv0 )(vv0 u|~v0 B N))→ (νx)(~Mu |~x B N) ,it is enough to prove:(νx)(~Mu |~x B N)  ~[N/x]Mu .
We show the above by induction on the structure of M.
Case 1. Suppose that M is x. We have:(LHS) = (νx)(xu.0|~x B N)→ (νx)(~Nu |~x B N)≡ ~Nu |(νx)~x B N ∼ (RHS) .
Case 2. Suppose that M is y distinct from x. We have:(LHS) = (νx)(yu|~x B N)≡ yu.0|(νx)~x B N ∼ (RHS) .
Case 3. Suppose that M is λy.M0 where y , x. We have:(LHS) = (νx)(u(yv):~M0 v |~x B N)∼ u(yv):(νx)(~M0 v |~x B N) u(yv):~[N/x]M0 v(∵ induction hypothesis)= ~λy.[N/x]M0 u = (RHS) .
Case 4. Suppose that M is M1 M2 . Theorem 4.15 induces:(LHS) = (νx)((νv)(~M1 v |(νv0 )(vv0 u|~v0 B M2 ))|~x B N)∼ (νv)((νx)(~M1 v |~x B N)|(νx)(νv0 )(vv0 u|~v0 B M2 )|~x B N)∼ (νv)((νx)(~M1 v |~x B N)|(νv0 )(vv0 u|!(νx)(v0 (v00 ).~M2 v00 |~x B N)))∼ (νv)((νx)(~M1 v |~x B N)|(νv0 )(vv0 u|!v0 (v00 ).(νx)(~M2 v00 |~x B N))) (νv)(~[N/x]M1 u |(νv0 )(vv0 u|!v0 (v00 ).~[N/x]M2 v00 ))(∵ induction hypothesis)= ~[N/x]M1 [N/x]M2 u = (RHS) .
Theorem 5.3. If M →λ M 0 , then ~M → ·  ~M 0 .
Proof. By induction on M →λ M 0 .
Case 1. The base step has already proved by Lemma 5.2.
Case 2. Suppose that λx0 .M0 →λ λx0 .M00 is inferred from M0 →λ M00 . Induction hypothesis
derives ~M0 v → ·  ~M00 v . Then,~Mu = u(x0 v):~M0 v→ ·  u(x0 v):~M00 v = ~M 0 u .
19

Case 3. Suppose M1 M2 →λ M10 M2 is inferred from M1 →λ M10 . By induction hypothesis, weget ~M1 v → ·  ~M10 v . Then,~Mu = (νv)(~M1 v |(νv0 )(vv0 u|~v0 B M2 ))→ ·  (νv)(~M10 v |(νv0 )(vv0 u|~v0 B M2 )) = ~M 0 u .
For convenience, we adopt the following notation. A term M is said to be a normal form,
written M 6→λ , if there exists no term to which M reduces. A term M converges on M 0 ,written M ↓λ M 0 , if M reduces to M 0 in arbitrary finite steps and M 0 is a normal form. A
term M converges if there exists a term on which M converges. A term M diverges if there
exists an infinite reduction sequence from M. We also use similar terminology and notation
for processes and reactions →.
The above definitions immediately derive the following simple proposition as a corollaryof Theorem 5.3.
Corollary 5.4. If M diverges, then ~M also diverges.
This corollary claims that the strong call-by-name lambda-calculus to be sound to the
Mpi-calculus in divergence. Although this says nothing in convergence, we have:
Theorem 5.5. If M is a normal form, so is ~M.
There exists a correspondence once it becomes a normal form. It is, therefore, natural that
we introduce a relationship between reduction and reaction connected more directly. This isdone in Subsection 5.3.

5.2

Explicit Environment

In the previous subsection we saw that lambda-reduction →λ reflects to reaction →. However,it has indeed a gap of . For the purpose of looking for the source of this gap, we treat
lambda-reduction more delicately.
A function f receives an argument a for a parameter x in f , and becomes an output itself.
In more detail, when it is decided that f receives a for x, an environment that evaluate x in f
as a is constructed, and f is evaluated in the environment until an output is needed. A lambdacalculus in which these are built is said having explicit environment, and was first considered
by Abadi et al. [1]. Many lambda-calculi have been considered since the seminal work of
Abadi et al. For instance, λexp, λxgc, λs, λν, and λε, see [10, 5], [6], [11], [4], and [22]respectively.
We define the simplest strong call-by-name lambda-calculus with explicit environment asfollows:
M, N, . . . F x | λx.M | MN | {N/x}M
M →β M 0
M →β M 0(λx.M)N →β {N/x}M0λx.M →β λx.M
MN →β M 0 N{M/x}x →ε M

x < {y} ∪ fv N
{N/y}λx.M →ε λx.{N/y}M{N/x}(M1 M2 ) →ε {N/x}M1 {N/x}M2

x < fv M{N/x}M →ε M

M →ε M 0
λx.M →ε λx.M 0

M →ε M 0
MN →ε M 0 N
20

M →ε M 0
N M →ε N M 0.

Ordinary lambda-calculi with explicit environment have reductions for environment, e.g. forcombining two environments into one environment. Here, explicit environments are used
only as a buffer between lambda-reducible terms. It is, therefore, obvious that there exists no
infinite sequence of →ε . Notice that {N/x}M is not [N/x]M but one expression of such a form.
We extend the previous translation for a term with environment:~{N/x}Mu = (νx)(~Mu |~x B N) .
These notions divide Theorem 5.3 into the following two theorems.
Theorem 5.6. If M →β M 0 , then ~M → ~M 0 .
Theorem 5.7. If M →ε M 0 , then ~M  ~M 0 .
Since we regard a reaction as a transition performed automatically in the concurrent system, Theorem 5.6 suggests that the Mpi-calculus has a mechanism that assigns an argument toan address of a function. However, we consider  to be a meta-relation on processes. The Mpicalculus, therefore, distinguishes a function with an environment from the result of evaluating
the function in the environment.

5.3

Full Correspondence

So far, we gave a translation from lambda-terms into Mpi-processes and extended it to one
from lambda-terms with explicit environment to Mpi-processes. Notice that we can rewrite alambda-term to some lambda-terms with explicit environment equal to it; for instance, λx.y
can be expressed as [y/z](λx.z), [λx.y/z]z, and so on. Therefore, the translation ~· fromlambda-terms into Mpi-processes can be extended to a multi-valued function. Formally, ~Lu
is defined as the set:
{ (νx)(~Mu |~x B N) | fv Ni ∩ {x1 , . . . , xi } = ∅ for 1 ≤ i ≤ n, and [N/x]M = L }where (νx), ~x B N, and [N/x]M denote (νx1 ) · · · (νxn ), ~x1 B N1 | · · · |~xn B Nn , and[Nn /xn ] · · · [N1 /x1 ]M respectively. In the sequel, when we say ~L, we refer to some elementof ~L.
Lemma 5.8. If ~L ∼ P and L →λ L0 , then P →+ · ∼ ~L0 .
Proof. By induction on derivation of lambda-reduction.
Case 1. Suppose that L is [N/x]((λx0 .M0 )M1 ) and L0 is [[N/x]M1 /x0 ][N/x]M0 . We remarkthat [[N/x]M1 /x0 ][N/x]M0 is [N/x][M1 /x0 ]M0 since we may assume x0 < fv N.
~Lu = (νx)(~(λx0 .M0 )M1 u |~x B N)→+ (νx)((νx0 )(~M0 u |~x0 B M1 )|~x B N)= ~[N/x][M1 /x0 ]M0 u = ~L0 u .
Case 2. Suppose that L is [N/x](xi M1 ) and L0 is [[N/x]M1 /x0 ][N/x]M0 where Ni is λx0 .M0 .
Notice that [[N/x]M1 /x0 ][N/x]M0 is [N/x][M1 /x0 ]M0 since x0 < fv N.
~Lu = (νx)(~xi M1 u |~x B N)= (νx)((νv)(xv|(νv0 )(vv0 u|~v0 B M1 ))|~x B N)→+ (νx)((νv)(~λx0 .M0 v |(νv0 )(vv0 u|~v0 B M1 ))|~x B N)21

= (νx)((νv)(v(x0 v00 ):~M0 v00 |(νv0 )(vv0 u|~v0 B M1 ))|~x B N)→ (νx)(νx0 )((~M0 u |~x0 B M1 )|~x B N)= ~[N/x][M1 /x0 ]M0 u = ~L0 u .
Case 3. Suppose that L is [N/x]xi and L0 is[[ti+1 , . . . , tn /xi+1 , . . . , xn ]M1 /x0 ][ti+1 , . . . , tn /xi+1 , . . . , xn ]M0 .
where Ni is (λx0 .M0 )M1 . Notice that L0 is [N/x][M1 /x0 ]M0 since x0 < fv N and {x1 , . . . , xi } ∩(fv M0 ∪ fn(M1 )) = ∅~Lu = (νx)(~xi u |~x B N)= (νx)(xi u|~x B N)→+ (νx)(~(λx0 .M0 )M1 u |~x B N)= (νx)((νv)(v(x0 v00 ):~M0 v00 |(νv0 )(vv0 u|~v0 B M1 ))|~x B N)→ (νx)((νx0 )(~M0 u |~x0 B M1 )|~x B N)= ~[N/x][M1 /x0 ]M0 u = ~L0 u .
Case 4. Suppose that L →λ L0 is inferred from [N/x]Mi →λ Mi0 where L, L0 , and Ni are[N/x]xi , λx0 .Mi0 , and λx0 .Mi , respectively.
~Lu = (νx)(~xi u |~x B N)= (νx)(xi u|~x B N)→ (νx)(~λx0 .Mi u |~x B N)= (νx)(u(x0 v):~Mi v |~x B N)∼ u(x0 v):(νx)(~Mi v |~x B N)→+ · ∼ u(x0 v):~Mi0 v= ~λx0 .Mi0  = ~L0 u(∵ induction hypothesis).

Case 5. Suppose that L →λ L0 is inferred from [N/x]M1 →λ M10 where L, L0 , and Ni are[N/x]xi , M10 [N/x]M2 , and M1 M2 . Notice that [N/x](M10 M2 ) is M10 [N/x]M2 since x∩fv M10 =∅.
~Lu = (νx)(~xi u |~x B N)= (νx)(xi u|~x B N)→ (νx)(~M1 M2 u |~x B N)= (νx)((νv)(~M1 v |(νv0 )(vv0 u|~v0 B M2 ))|~x B N)∼ (νv)((νx)(~M1 v |~x B N)|(νx)((νv0 )(vv0 u|~v0 B M2 )|~x B N))→+ · ∼ (νv)(~M10 v |(νx)((νv0 )(vv0 u|~v0 B M2 )|~x B N)) (∵ induction hypothesis)≡ (νx)(νv)(~M10 v |(νv0 )((vv0 u|~v0 B M2 )|~x B N))
= ~[N/x](M10 M2 ) = ~L0 u .
Case 6. Suppose that L →λ L0 is inferred from [N/x]M0 →λ s00 where L is [N/x]λx0 .M0 and
L0 is λx0 .s00 .
~Lu = (νx)(u(x0 v):~M0 v |~x B N)∼ u(x0 v):(νx)(~M0 v |~x B N)
22

→+ · ∼ u(x0 v):~s00 v= ~λx0 .s00  = ~L0 u(∵ induction hypothesis).

Case 7. Suppose that L →λ L0 is inferred from [N/x]M1 →λ M10 where L is [N/x](M1 M2 )and L0 is M10 [N/x]M2 . Notice that [N/x](M10 M2 ) is M10 [N/x]M2 ) since x ∩ fv M10 = ∅.
~Lu = (νx)((νv)(~M1 v |(νv0 )(vv0 u|~v0 B M2 ))|~x B N)∼ (νv)((νx)(~M1 v |~x B N)|(νx)((νv0 )(vv0 u|~v0 B M2 )|~x B N))→+ · ∼ (νv)(~M10 v |(νx)((νv0 )(vv0 u|~v0 B M2 )|~x B N))(∵ induction hypothesis)≡ (νx)(νv)(~M10 v |(νv0 )((vv0 u|~v0 B M2 )|~x B N))
= ~[N/x](M10 M2 ) = ~L0 u .
Lemma 5.9. Let α be the first action except τ with which ~Lu transits. Then u belongs tofn(α). Moreover if L is not an abstraction, then α is an output action.
Proof. Let L be [N/x]M. By induction of the structure of L. By cases on the form of M.
Case 1. It is obvious in case M is a variable.
Case 2. Suppose that M is λx0 .M0 . ~Lu is (νx)(u(x0 v):~M0 v )|~x B N). By induction hypothesis, ~M0 v cannot transits without invoking an action related to v except τ. Therefore, itholds in this case.
Case 3. Suppose that M is M1 M2 . Then ~Lu is(νx)((νv)(~M1 v |(νv0 )(vv0 u|~v0 B M2 ))|~x B
N). By induction hypothesis, ~M1 v cannot transits without invoking an action related tov except τ. Therefore, it also holds in this case. The second assertion also depends on thisproof.

Lemma 5.10. If ~L → P, then L →λ ∗ L0 and ~L0  = P for some L0 .
Proof. Let L be [N/x]M. By induction on the inference of ~L → P.
Case 1. Suppose that M is λx0 .M0 . Then P is (νx)(u(x0 v):P0 |~x B N) where ~M0 v → P0 by
Lemma 5.9. By induction hypothesis, there exists L0 such that M0 →λ ∗ L0 and ~L0 v = P0 .
By Lemma 5.1, we have L →λ ∗ [N/x]λx0 .L0 . It is sufficient since ~[N/x]λx0 .L0 u = P.
Case 2. Suppose that M is M1 M2 and P is (νx)((νv)(P1 |(νv0 )(vv0 u|~v0 B M2 ))|~x B N) where~M1 v → P1 . By induction hypothesis, there exists L1 such that M1 →λ ∗ L1 and ~L1 v = P1 .
The rest is similar to Case 1.
Case 3. Suppose that M is (λx0 .M0 )M2 and P is (νx)((νx0 )(~M0 u |~x0 B M2 )|~x B N). We
have L →λ [t/x][M2 /x0 ]M0 by applying Lemma 5.1 to (λx0 .M0 )M2 →λ [M2 /x0 ]M0 . It issufficient since x0 < fn(N) implies ~[N/x][M2 /x0 ]M0 u = P.
Case 4. Suppose that M is xi M1 · · · Mm (m ≥ 1) and P is(νx)((νvm )(· · · (~Ni v1 | · · · |(νv0m )(vm v0m u|~v0 B Mm )))|~x B N) .
Since L is also [N/x](Ni M1 · · · Mm ), we have ~Lu = P. This suffices to check this case.
Case 5. The case of M = x is similar to Case 4 since this is is the one of m = 0 in Case 4.
23

Lemma 5.11. If ~L ∼ P and L 6→λ , then P ↓ P0 for some P0 .
Proof. Let L be [N/x]M. We prove this lemma by double induction of the structure of L andthe number of substitutions.
Case 1. Suppose that M is xi . We immediately get~Lu → (νx)(~Ni u |~x B N) C Q .
Since L = [Nn /xn ] · · · [Ni+1 /xi+1 ]Ni , there exists Q0 such that Q ↓ Q0 by induction hypothesis.
Therefore, there exists P0 such that P ↓ P0 .
Case 2. It is obvious when M is a variable distinct from x.
Case 3. Suppose that M is λx0 .M0 . By induction hypothesis, there exists Q such that ~M0 v ↓Q. Then~Lu = (νx)(u(x0 v):~M0 v |~x B N) →∗ (νx)(u(x0 v):Q|~x B N) C Q0 .
By Lemma 5.9, this Q0 is a normal form. Therefore, there exists P0 such that P ↓ P0 .
Case 4. Suppose that M is M1 M2 . By induction hypothesis, there exists Q such that ~M1 v ↓Q. Then~Lu = (νx)((νv)(~M1 v |(νv0 )(vv0 u|~v0 B M2 ))|~x B N)→∗ (νx)((νv)(Q|(νv0 )(vv0 u|~v0 B M2 ))|~x B N) C Q0 .
Since M is a normal form, M1 is not an abstraction. Then Q0 is a normal form by Lemma 5.9.
Therefore, there exists P0 such that P ↓ P0 .

Theorem 5.12. Let L and L0 be lambda-terms, and P and P0 be Mpi-processes.
1. If L ↓λ L0 , then for each element P of ~L there exists P0 such that P ↓ P0 .
2. If ~L ↓ P, then L ↓λ L0 for some L0 .
3. L converges if and only if ~L does.
4. L diverges if and only if ~L does.
Proof. First, there exists P0 such that ~L →+ P0 and ~L0  ∼ P0 by Lemma 5.8. There exists P
such that P0 ↓ P by Lemma 5.11. Hence, 1 holds. Secondly, there exists L00 such that L →∗λ L00
and ~L0  = P by Lemma 5.10. Since P is a normal form, L0 is a normal form by Lemma 5.8.
Hence, 2 holds. Finally, 3 and 4 follow from 1, 2, and the proof of Lemma 5.10.

Notice that all the processes which belong to ~L coincide in terms of termination property,
and as a result L and ~L in Subsection 5.1 converge or diverge simultaneously. It is, however,not surprising since we have extended Milner’s call-by-name translation into the multi-valued
function for this purpose.
The accordance in convergence and divergence claims that the Mpi-calculus contains thestrong call-by-name lambda-calculus as a subsystem. Moreover, we can give an intuitive
explanation to Milner’s call-by-name translation, because extensionality of lambda-terms istranslated into optimization of Mpi-processes, i.e.,24

M →λ M 0
corresponds to
λx.M →λ λx.M 0τ~Mv →− ~M 0 v{u} ∩ ∅ = ∅τ

{x, v} ∩ ∅ = ∅.

0

u(xv):~Mv →− u(xv):~M v

In addition, generality of the Mpi-calculus enables it to have various lambda-calculi: threecalculi except the strong call-by-name lambda-calculus as described in Subsection 5.1. We
conclude that the Mpi-calculus is not only simple and natural but also expressible and general.
Fu [9], Merro and Sangiorgi [12], Parrow and Victor [17, 18], and other researchers havegiven sound embeddings of the strong call-by-name lambda-calculus into their systems, andmost of them have not showed their embeddings to be complete. In contrast, Parrow andVictor designed a concurrent system called fusion calculus using unique ideas, and showedthat their embedding is not only sound but also complete to the strong call-by-name lambdacalculus [18]. Their system is based on the notion of equations of names, and properly includes
the pi-calculus. Their system also has an advantage in the way that they deal with names.
In their system, there exists no concept of binding names on input actions. As a result, it
can avoid troublesome procedures for dealing with bound names, which can become tedious.
Certainly, their system is simple and expressive. However, their study on concurrency does
not directly give insights into the pi-calculus, the de facto standard concurrent system, since
their system is quite unique. On the other hand, our system is directly connected to the picalculus with which many researchers are familiar. We could thus give them a lot of intuitive
ideas. For instance, we can claim that “environments in functional languages are resources ina concurrent system” in Subsection 5.2 and that “a concurrent system can have the notion of
application and extensionality of functions” in this subsection.

6

Conclusion and Future Work

We have introduced a concurrent system based on the concept of multi-ports, and have defined
various equivalences on processes. Our system is an extension of the pi-calculus, in the sensethat the pi-calculus can be obtained from ours by restricting the number of ports. It is noteworthy that we extend the pi-calculus to our system not by adding but by replacing a rule, andthat a process with only one port can be expressed as syntax sugar for a multi-ported process.
Moreover, our system has the advantage that we can control permission of self-communication
as described in detail in Section 3. Although we have given examples of this, it is left as future
work to find various useful applications of multi-ported processes which cannot communicate
with themselves.
Our system is more expressive than the original pi-calculus. As a witness, even the strong
call-by-name lambda-calculus can be embedded into our system, while Milner embedded only
lambda-calculi which do not have the extensional rule into the original pi-calculus. We treated
reductions of lambda-calculi carefully in this paper. As a consequence, our embedding of thestrong call-by-name lambda-calculus has resulted in a complete one with respect to convergence and divergence. To our knowledge, our system is the first one that is a natural extensionof the pi-calculus and that achieves completeness of the above kind.
Although we have succeeded in giving a complete embedding of the strong call-by-namelambda-calculus, it remains an open question whether it is possible to give a complete embedding of the lambda-calculus with full reductions. Our success is partly due to the fact that
there exists no reduction which applies to arguments:
M →λ M 0
N M →λ N M 0

25

in the strong call-by-name lambda-calculus. Since our translation translates arguments into
resources, it is necessary to add a rule which corresponds to optimization of resources in the
pi-calculus. A candidate for such a rule would be the following:
τ

P→
− P0
τ

!P →
− !P0
as some researchers indicate (and write off). However, it does not seem to be easy to introduce
a notion of equivalence on processes in this system since this transition, that a process offinite copying transits to an optimized one trained infinitely, is essentially different from theothers. We could think behavioral equivalence up to infinite internal transitions as a candidateof equivalence.

Acknowledgments
I would like to express my deepest gratitude to Masami Hagiya, Daisuke Kimura, Takafumi
Sakurai, Izumi Takeuti, Makoto Tatsuta, Kazushige Terui, and Mitsuharu Yamamoto, whohave worked closely with me on this paper. I am also very grateful to Carl Christian Frederiksen, Masahito Hasegawa, Kohei Honda, Yoshihiko Kakutani, Akitoshi Kawamura, andRichard Potter for providing useful advice.

References[1] M. Abadi, L. Cardelli, P.-L. Curien, and J.-J. Lévy. Explicit substitutions. In Proceedingsof POPL’90: the 17th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 31–46, 1990.
[2] T. Abe. A concurrent system of multi-ported processes with causal dependency. In
Proceedings of APLAS’04: the 2nd Asian Symposium on Programming Languages andSystems, volume 3302 of Lecture Notes in Computer Science, pages 146–162. SpringerVerlag, 2004.
[3] H. P. Barendregt. The Lambda Calculus: Its Syntax and Semantics. North-Holland,
revised edition, 1984.
[4] Z.-E.-A. Benaissa, D. Briaud, P. Lescanne, and J. Rouyer-Degli. λν, a calculus of explicit
substitutions which preserves strong normalisation. Journal of Functional Programming,
6(5):699–722, 1996.
[5] R. Bloo. Preservation of strong normalisation for explicit substitution. Computer Science
Report 95-08, Eindhoven University of Technology, 1995.
[6] R. Bloo and K. H. Rose. Preservation of strong normalisation in named lambda calculi
with explicit substitution and garbage collection. In Proceedings of CSN’95: Computer
Science in the Netherlands, 1995.
[7] M. Boreale and R. De Nicola. Testing equivalence for mobile processes. Information
and Computation, 120:279–303, 1995.
[8] H. B. Curry, R. Feys, and W. Craig. Combinatory Logic, volume 1. North-Holland,
1958.

26

[9] Y. Fu. A proof-theoretical approach to communication. In Proceedings of ICALP’97:
the 24th International Colloquium on Automata, Languages, and Programming, volume
1256 of Lecture Notes in Computer Science, pages 325–335. Springer-Verlag, 1997.
[10] F. Kamareddine and R. Nederpelt. On stepwise explicit substitution. International Journal of Foundations of Computer Science, 4(3):197–240, 1993.
[11] F. Kamareddine and A. Rios. A lambda-calculus à la De Bruijn with explicit substitutions. In Proceedings of PLILP’95: the 7th International Symposium on Programming
Languages, Implementations, Logics, and Programs, volume 982 of Lecture Notes in
Computer Science, pages 45–62. Springer-Verlag, 1995.
[12] M. Merro and D. Sangiorgi. On asynchrony in name-passing calculi. In Proceedings of
ICALP’98: the 25th International Colloquium on Automata, Languages, and Programming, 1998.
[13] R. Milner. Communication and Concurrency. Prentice Hall, 1989.
[14] R. Milner. Functions as processes. Journal of Mathematical Structures in Computer
Science, 2(2):119–141, 1992.
[15] 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, 1993.
[16] R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes. Information andComputation, 100(1):1–77, 1992.
[17] J. Parrow and B. Victor. The update calculus. In Proceedings of AMAST’97: the 6thInternational Conference on Algebraic Methodology and Software Technology, volume1349 of Lecture Notes in Computer Science, pages 409–423. Springer-Verlag, 1997.
[18] J. Parrow and B. Victor. The fusion calculus: Expressiveness and symmetry in mobile
processes. In Proceedings of LICS’98: the 13th IEEE Symposium on Logic in Computer
Science, 1998.
[19] D. Sangiorgi. On the bisimulation proof method. Journal of Mathematical Structures in
Computer Science, 8(5):447–479, 1998.
[20] D. Sangiorgi and R. Milner. The problem of ‘weak bisimulation up to’. In Proceedingsof CONCUR’92: the 3rd International Conference on Concurrency Theory, volume 630
of Lecture Notes in Computer Science, pages 32–46. Springer-Verlag, 1992.
[21] D. Sangiorgi and D. Walker.
The π-calculus: a Theory of Mobile Processes.
Cambridge University Press, 2001.
This book has a list of errata:
http://www.cs.unibo.it/˜sangio/BOOK/errata.html.
[22] M. Sato, T. Sakurai, and R. Burstall. Explicit environments. In Proceedings of TLCA’99:
the 4th International Conference on Typed Lambda Calculi and Applications, volume1581 of Lecture Notes in Computer Science, pages 340–354. Springer-Verlag, 1999.
[23] F. van Breugel. A labelled transition system for pi-epsilon-calculus. In Proceedingsof TAPSOFT’97: the 7th International Joint Conference on the Theory and Practiceof Software Development, volume 1214 of Lecture Notes in Computer Science, pages
312–336. Springer, 1997.

27