A Proof Theoretical Approach toCommunication
Yuxi Fu?
Department of Computer Science, Shanghai Jiao Tong University
1954 Hua Shan Road, Shanghai 200030, China

Abstract. The paper investigates a concurrent computation model, chi
calculus, in which communications resemble cut eliminations for classicalproofs. The algebraic properties of the model are studied. Its relationshipto sequential computation is illustrated by showing that it incorporates
the operational semantics of the call-by-name lambda calculus. Practically the model has pi calculus as a submodel.

1

Communication as Cut Elimination

Concurrent computation is currently an open-ended issue. The situation is incontrast with sequential computation whose operational semantics is formalized
by, among others, the λ-calculus ([2]). In retrospect, the λ-calculus can be seen
as a fallout of proof theory. Curry-Howard’s proposition-as-type principle allows
one to code up constructive proofs as typed terms. At the core of the constructive logic is the minimal logic, whose type theoretical formulation gives rise to,roughly, the simply typed λ-calculus. Now the untyped λ-calculus is obtained
from the simply typed λ-calculus by removing all the typing information.
In recent years, classical proofs have been investigated in a computational setting. Girard proposed proof nets ([4]) as term representations of classical linear
proofs. These classical terms are typed. The conclusion of a proof derivation is thetype of the proof net corresponding to that proof derivation. The computationsof these terms are cut eliminations modeled by rewritings of graphs. As the terms
are typed, cuts happen between nodes of correlated types. Abramsky’s proofas-process interpretation ([1, 3]) relates proof nets to processes. At operational
level, this interpretation is supported by a cut-elimination-as-communication
paradigm. It looks like a type-erasing interpretation similar to the one found in
a constructive world.
This paper investigates a concurrent computation model obtained by reversing the roles of proofs and processes in Abramsky’s paradigm. That is to saythat we regard communications as cut eliminations. The way to arrive at such amodel of communication echoes that in the sequential world. First we take themultiplicative linear logic as the ‘minimal logic’ in a classical framework. Thereis nothing canonical about this choice. As the typed classical terms we take the?

ICALP’97 , Lecture Notes in Computer Science 1256, 325-335, 1997.

proof nets. The following left diagram is a proof net:




⊥ j
jB B ⊥ jj
jA A⊥ j
jA A⊥ j


P
P

PP
PP B B


@
@
PP
PP
R j
@
R j
@
q j
q j
)

)

⊥
⊥
A ℘B
C⊥
A⊗B
C
The first step towards the model is to abstract away the logical aspect of proof
nets but keep its proof theoretical content. The above proof net becomes theright diagram in the above. There are two kinds of edge in the net. So the second step is to transform the net into a graph with only directed arrows:
j
j
@
@
R j ⊥
@
R
@
 jB
P
B
A j
A⊥ j
P

P
@
PP
R j
@
q j
)

C⊥
C
We then forget about the typing information while recording positive and negative information by labels on arrows, arriving at an untyped graph (left below).
j
j
j
j
+
+
+
+
@
@
@
@
R j
@
R j
@
R j
@
R j
@
j
j
j
j

P

P
PP
 PP

@
@
+
- PP
+
- PP
R j
@
R aj
@
q jq bj ) +) +This is the untyped version of the original classical typed term. Notice that there
are two kinds of node in the proof net: the internal nodes and the conclusion
nodes. In order to distinguish them in the untyped graph, we label the conclusion nodes with small letters (above right). We call graphs of this kind reaction
graphs. In a reaction graph, a node without (with) a label is called local (global).
Reaction graphs can be seen as the underlying graphs of proof derivations in a
generalized and distilled form. Computations with reaction graphs are cut eliminations. Here is an example of two consecutive cut-eliminations:
j
mj
mj
mj
I
@
6
- @+
- 6
- + 6
+
⇒
⇒

?
@
?
j
j
j
j
j
In the left graph, the two upper nodes show up opposite polarities to the left
bottom node. This cut is eliminated in the first reduction. The two arrows are
removed and the two upper nodes are coerced with the resulting node labeled by
m. In the middle graph, the two bottom nodes with the arrows pointing to thenode labeled m form a cut. The second reduction eliminates the cut. The idea of
this paper is to think of these cut-eliminations as communications. To develop
the idea, we need a process-like notation for reaction graphs. Let us define graphterms by abstract syntax as follows: G := 0 | m[x] | m[x] | (x)G | G|G0 . Here 0 is
the empty reaction graph; m[x] and m[x] are respectively the following graphs:
xj +- mj
xj - - mj(x)G is obtained from G by removing the label x from G; G|G0 is the amal-

gamation of G and G0 , coercing nodes with same labels. The two consecutive
cut-eliminations in the above can now be described by the following reductions:(x)(y)(z)(m[x]|y[x]|y[m]|y[z]|z[y]) → (x)(y)(m[x]|y[x]|m[y]) → (x)(x[x]).
This term representation gives rise to a calculus of reaction graphs.
The calculus of graphs only deals with finite computations. To achieve Turingcomputability, we extend the language with standard process combinators. The
resulting language will be referred to as χ-calculus, where χ stands for exchange
of information. The paper initiates a study of this computation model.

2

A Model for Concurrent Computationdef

Let N be a set of names ranged over by lower case letters and N = {a | a ∈ N }be the set of conames. The union N ∪ N will be ranged over by α. Define α tobe m (m) whenever α is m (m). Let T be the set of χ-terms defined as follows:
P := 0 | α[x].P | P |P 0 | (x)P | α(x)∗P.
Here m[x].P and m[x].P are terms that must first perform a communication
through name m and then enacts P [y/x], where y is the name received in thecommunication. In (x)P , the (x)-part is a localization combinator. In both (x)Pand α(x)∗P , x is local. The set of local names appeared in P is denoted byln(P ), whereas the set of global names, or non local names, in P is designatedby gn(P ). Set n(P ) is the union of ln(P ) and gn(P ). We adopt the α-convention
saying that a local name in a term can be replaced by a fresh name withoutchanging its syntax.
The effect of a substitution [y1 /x1 ] . . . [yn /xn ] on a term is defined as follows:def

P [y1 /x1 ] . . . [yn /xn ] = (. . . P [y1 /x1 ] . . .)[yn /xn ]. Substitutions will be ranged
over by σ.
For simplicity, a structural congruence is imposed on the members of T .
Definition 1. The relation = is the least congruence on χ-terms that contains:(i) P |0 = P , P1 |P2 = P2 |P1 , and P1 |(P2 |P3 ) = (P1 |P2 )|P3 ;(ii) (x)0 = 0, (x)(y)P = (y)(x)P , and (x)(P |Q) = P |(x)Q if x 6∈ gn(P );(iii) P = Q if P and Q are α-convertible.
We regard = as a grammatic equality. So P = Q means that P and Q are syntactically the same. The operational semantics of the language can be defined interms of a labeled transition system. We prefer however a reductional semantics
for χ-calculus in the style of [5]:(x)(R|α[x].P |α[y].Q) → (x)(R[y/x]|P [y/x]|Q[y/x])α(x)∗P |α[y].Q → α(x)∗P |P [y/x]|Q
P → P0P |Q → P 0 |Q

P → P0(x)P → (x)P 0

To help understand the communication rules, we now give some examples, assuming x and y are distinct:(x)(R|m[y].P |m[x].Q) → R[y/x]|P [y/x]|Q[y/x]m[y].P |(x)(R|m[x].Q) → P |R[y/x]|Q[y/x](y)(m[y].P |(x)(R|m[x].Q)) → (y)(P |R[y/x]|Q[y/x])(x)m[x].P |(y)m[y].Q → (z)(P [z/x]|Q[z/y]), where z is fresh(x)(m[x].P |m[x].Q) → (x)(P |Q).
It is clear from these examples that the localization operator in χ-calculus acts
as an effect delimiter. A communication either instantiates a local name by aglobal name or identifies two local names.
Let →+ (→∗ ) be the (reflexive and) transitive closure of →. We will denoteby x a sequence x1 , . . . , xn of names. We will also abbreviate (x1 ) . . . (xn )P to(x)P . When the length of the sequence x is zero, (x)P is just P .

3

Algebraic Properties

To study the algebraic semantics of χ-terms, a labeled transition system is deαx α[x] α(x)fined as follows, where δ ranges over {→, → , → |α ∈ N ∪ N , x ∈ N }:αx(y)(R|α[y].P ) → (R|P )[x/y]α[x]P → P0α[x]αxα(y)∗P → α(y)∗P |P [x/y]δ

α[x].P → P

δ

P → P 0 ln(δ) ∩ gn(Q) = ∅P → P 0 x 6∈ n(δ)δ(x)P → (x)P 0

α(x)(x)P → P 0

δP |Q → P 0 |Q.

In the rules, ln(δ) is {x} when δ is α(x); it is the empty set otherwise. n(δ) isδδ

the set of names in δ. Let ⇒ denote relation →∗ →→∗ .
A bisimulation equivalence for χ-terms should take into account the distinguished feature of the localization operators of the language. The equivalence
we introduce in this section is based upon the old idea that two terms are considered observationally equivalent if and only if placing them in a same context
results in two observationally equivalent terms. Working explicitly with contexts
is unnecessary in our setting due to the presence of the structural equality =.
Definition 2. Suppose R ⊆ T ×T . The relation R is a local simulation if whenever P RQ then for any term R and any sequence x of names it holds that(i) if (x)(P |R) → P 0 then Q0 exists such that (x)(Q|R) →∗ Q0 and P 0 RQ0 ;δδ(ii) if (x)(P |R) → P 0 then Q0 exists such that (x)(Q|R) ⇒ Q0 and P 0 RQ0 .
The relation R is a local bisimulation if both R and its inverse are local simulations. The local bisimilarity ≈ is the largest local bisimulation.
As usual, local bisimulation up to ≈ is a useful tool for proving two χ-terms
being locally bisimilar. We omit the standard definition.

In the rest of this section, we prove that ≈ is a congruence relation. The factthat ≈ is closed under parasition and localization combinators can be proved
already at this point.
Proposition 3. If P ≈ Q then (i) P |O ≈ Q|O and (ii) (x)P ≈ (x)Q.
The next lemma is crucial in showing that ≈ is a congruence relation. It is thefirst indication that local bisimilarity is algebraically appropriate. The property
is not enjoyed by local bisimilarity for π-processes.
Lemma 4. If P ≈ Q then P σ ≈ Qσ for an arbitrary substitution σ.
Proof. Let R be the union of ≈ and the followingP ≈ Q, R ∈ T , z a sequence of names, ((z)(P σ|R), (z)(Qσ|R)) σ a substitution [y1 /x1 ] . . . [yn /xn ] such .
that x1 , . . . , xn are pairwise distinct
δSuppose (z)(P σ|R)R(z)(Qσ|R) and (z)(P σ|R) → P 0 , where σ is the substitution [y1 /x1 ] . . . [yn /xn ] with x1 , . . . , xn being pairwise distinct. Let a and b be
fresh names. Then for the sequence z of names(z)((x)(a)(b)(b[b].P |a[x1 ]. . . . .a[xn ]|a[y1 ]. . . . .a[yn ].b[b])|R) →∗ (z)(P σ|R)δ

→ P 0.
As b 6∈ gn(P, Q), b[b].P ≈ b[b].Q follows easily. By Proposition 3,(x)(a)(b)(b[b].P |a[x1 ]. . . . .a[xn ]|a[y1 ]. . . . .a[yn ].b[b])≈ (x)(a)(b)(b[b].Q|a[x1 ]. . . . .a[xn ]|a[y1 ]. . . . .a[yn ].b[b]).
So by definition, there exists some Q0 such that P 0 ≈ Q0 andδ(z)((x)(a)(b)(b[b].Q|a[x1 ]. . . . .a[xn ]|a[y1 ]. . . . .a[yn ].b[b])|R) ⇒ Q0 .
During the above reduction every a[xi ] must have reacted upon a[yi ], for 1 ≤i ≤ n, and b[b] upon b[b]. It can be easily proved that all the communications
through a and that through b can happen in the very beginning. That is(z)((x)(a)(b[b].Q|a[x1 ]. . . . .a[xn ]|a[y1 ]. . . . .a[yn ].b[b])|R) →∗ (z)(Qσ|R)δ⇒ Q0 .
δδSo (z)(P σ|R) → P 0 is matched by (z)(Qσ|R) ⇒ Q0 . The case when (z)(P σ|R) →P 0 is similar. So R is a local bisimulation. It follows that P ≈ Q implies
P [y/x] ≈ Q[y/x]. Therefore P ≈ Q implies P σ ≈ Qσ for a substitution σ.
tu
We now come to the main result of the section.
Theorem 5. ≈ is a congruence equivalence: if P ≈ Q and O ∈ T then(i) α[x].P ≈ α[x].Q;(ii) P |O ≈ Q|O;(iii) (x)P ≈ (x)Q;(iv) α(x)∗P ≈ α(x)∗Q.

Proof. We sketch the proof of (iv). The proof of (i) is simpler. Let R be{((x)(m(y)∗P |R), (x)(m(y)∗Q|R)) | P ≈ Q, R ∈ T , m, x names}.
Suppose (x)(m(y)∗P |R) → P 0 and that (x)(m(y)∗P |R) → P 0 is caused by
a communication between m(y)∗P and R. Then P 0 is (x)(m(y)∗P |P [a/y]|R0 ).
Similarly (x)(m(y)∗Q|R) → (x)(m(y)∗Q|Q[a/y]|R0 ). By Lemma 4, P [a/y] ≈Q[a/y]. By Proposition 3, (x)(m(y)∗Q|P [a/y]|R0 ) ≈ (x)(m(y)∗Q|Q[a/y]|R0 ). It
is then easy to see that R is a local bisimulation up to ≈.
tu4π-Processes as χ-Terms

A question naturally arises as to the relationship between π-calculus and χcalculus. We give a first answer in this section. Let P be the set of π-processes
defined as follows: P := 0 | m(x).P | mx.P | P |P 0 | (x)P | m(x)∗P . We refer
the reader to [6] for background material on π-calculus.
There are many bisimulation equivalences on π-processes. What is most relevant in this section is the open bisimilarity defined in [8]. Actually we will use
a version of open bisimilarity stronger than Sangiorgi’s.
Definition 6. Let R be a binary relation on the set of π-processes. The relation
R is an open bisimulation if whenever P RQ then for any π-process R, any
sequence x of names and any substitution σ it holds thatββ(i) if (x)(P σ|R) ⇒ P 0 then Q0 exists such that (x)(Qσ|R) ⇒ Q0 and P 0 RQ0 ;ββ(ii) if (x)(Qσ|R) ⇒ Q0 then P 0 exists such that (x)(P σ|R) ⇒ P 0 and P 0 RQ0 .
The open bisimilarity ≈o is the largest open bisimulation.
≈◦ is a congruence equivalence and is closed under substitution.
A structural translation from π to χ has as nontrivial clauses the following:def(m(x).P )◦ = (x)m[x].P ◦ ,def(mx.P )◦ = m[x].P ◦ .
Imposing on P a same structural congruence as given in Definition 1, one has
Theorem 7. For P, Q ∈ P, it holds thatmxmx(i) P → Q iff P ◦ → Q◦ ;(ii) P → Q iff P ◦ → Q◦ ;
mx

m[x]

(iii) P → Q iff P ◦ → Q◦ ;

m(x)

m(x)

(iv) P → Q iff P ◦ → Q◦ .

Theorem 8. For P, Q ∈ P, P ≈o Q iff P ◦ ≈ Q◦ .

5

Call-by-Name in χ-Calculus

A concurrent computation model has to answer the question of whether it captures sequential computation successfully. The issue is often addressed by relating variants of λ-calculus to the model. Our focus in this section is on thecall-by-name λ-calculus ([7]), whose semantics is defined by the following rules:(λx.M )N → M [N/x]

M → M0M N → M 0N

M → M0.
λx.M → λx.M 0

The following translation, which is Milner’s encoding of the lazy λ-calculus withmodification, serves as an encoding of the call-by-name λ-calculus in χ-calculus:
def[[x]]u = x[u]def[[λx.M ]]u = (v)(x)(u[x].u[v]|[[M ]]v)
def[[M N ]]u = (v)(x)([[M ]]v|v[x].v[u].x(w)∗[[N ]]w).
The parasition of u[x].u[v] and [[M ]]v in [[λx.M ]]u allows [[M ]]v to evolve independently, thus modeling reduction under λ-abstraction. The encoding preserves
the operational semantics of the call-by-name λ-calculus in the sense the operational semantics of the lazy λ-calculus is preserved by Milner’s encoding ([5]).
A formal treatment is omitted in this extended abstract.
The call-by-name λ-calculus is one example which can not be treated successfully in π-calculus.

6

Towards an Integration of χ and λThere are two problems one encounters when trying to simulate the operationalsemantics of the full λ-calculus. The first is how to model reduction under λabstraction. The second is how to model reduction M N → M N 0 caused by
N → N 0 . The former is to do with parallel computation. There is no reason why
it should pose any problem for concurrent computation. This view is supportedby the result in Sect. 5. The latter is to do with recursion because the λ-term N
may be duplicated in future reduction. In any structural interpretation, this N
must be translated into the body of a replicator or guarded recursion. So if the
N induces an infinite reduction, the interpretation of M N would have no terminating reduction sequences. It is our view that the second problem is orthogonal
to concurrent computation. It is caused essentially by the incompatibility of thetwo recursion mechanisms.
In this section we take a look at a higher order calculus combining the communication mechanism of the χ-calculus and the recursion mechanism of the
λ-calculus. The purpose of this investigation is to see if the two mechanisms fit
coherently and if local bisimulation suffices as a tool for studying the algebraic
properties of the language.
6.1

χ with Call-by-Name λLet the set H of higher order χ-terms be defined by the following abstract syntax:
E := X | α[x].E | E|E 0 | (x)E | α(X)E | α[E],where X is a term variable. Let 0 abbreviate (a)a(X)X. The semantics of thehigher order χ-calculus is defined by the relevant rules of the first order χ-calculus
together with the following rules incorporating a call-by-name mechanism:
α(X)E|α[F ] → E[F/X]

E→F
α(X)E → α(X)FA structural equality is imposed on the members of H, whose definition is thesame as Definition 1. Usually a bisimulation equivalence for a higher order process calculus is defined for closed processes. This is a tractable approach. But inthe presence of the second reduction rule given above, the method breaks down.
A bisimulation equivalence for higher order χ-calculus has to be defined on all
terms. For that purpose, let’s say that a binary relation R on H is substitution
closed if whenever ERF then E[E1 /X1 , . . . , Ei /Xi ]RF [E1 /X1 , . . . , Ei /Xi ] forE1 , . . . , Ei ∈ H and X1 , . . . , Xi that are among the free variables of E|F .
Definition 9. A substitution closed binary relation R on H is a local bisimulation if whenever ERF then for any H ∈ H and {x} ⊆ N it holds that
δ

δ

δ

δ

(i) if (x)(E|H) ⇒ E 0 then F 0 exists such that (x)(F |H) ⇒ F 0 and E 0 RF 0 ;(ii) if (x)(F |H) ⇒ F 0 then E 0 exists such that (x)(E|H) ⇒ E 0 and E 0 RF 0 .
The local bisimilarity ≈ω is the largest local bisimulation on higher order terms.
The above definition is given in terms of a labeled transition system on H thatis defined by the relevant rules in Sect. 3. It should be remarked that ≈ω is bydefinition substitution closed.
Theorem 10. ≈ω is a congruence equivalence: if E ≈ω F and G ∈ H then(i) α[x].E ≈ω α[x].F ;(ii) E|G ≈ω F |G;(iii) (x)E ≈ω (x)F ;ωω(iv) α(X)E ≈ α(X)F ; (v) α[E] ≈ α[F ].
Proof. We only prove (v). For the sake of this proof, let’s define Ho [X] to be theset of all higher order terms E such that each occurrence of X is within α[G] forsome α ∈ N ∪ N and some G ∈ H. Let R be{(E[A/X], E[B/X]) | A ≈ω B, E ∈ Ho [X], X a variable}.
Suppose E[A/X] → G. Then G ≡ F [A] for some F ∈ Ho [X]. It can be easily
shown that some H ∈ H exists such that E[B/X] → H and F [B/X] ≈ω H.
It follows that R is a local bisimulation up to ≈ω . Thus α[E] ≈ω α[F ] since
α[X] ∈ Ho [X].
tu
In the remaining of the section, we justify our claim that the higher order
calculus is a combination of χ and λ.
6.2

Recursion

As a test for local bisimilarity, we examine Thomsen’s recursion ([9]) in thissection. Suppose that E contains free variable X and a does not occur in E. The

following abbreviations will be used:
def

a
WX
(E) = a[a]|a(X)(a[a].E|a[X]),defaa(E)]).
recX.E = (a)(WX(E)|a[WX

We remark that recX.E defined here is slightly different from Thomsen’s. Theaidea is to make WX(E) inert. Before proving the main property concerning
recX.E, we first establish the following result.
aaab
Lemma 11. (a)(F [WX(E)/X]|a[WX(E)]) ≈ω (a)(b)(F 0 |a[WX(E)]|b[WX(E)]),
0awhere E and F have free variable X and F is obtained from F [WX (E)/X] byab
replacing some occurrences of WX(E) by WX(E). Here a and b are fresh.

Theorem 12. Suppose E contains free X. Then recX.E ≈ω E[recX.E/X].
Proof. Suppose E and F contain free variable X, a 6∈ n(E, F ) and gn(E) ∩aa(E)]) ≈ln(F ) = ∅. Using Lemma 11, one proves that (a)(F [WX(E)/X]|a[WXωaaωF [recX.E/X]. So recX.E ≈ (a)(E[WX (E)/X]|a[WX (E)]) ≈ E[recX.E/X],
which is what we are after.
tu
6.3

Projecting Out Guarded Recursion

In this section we show that the higher order χ can be seen as an extensionof the first order χ. A fallout of the result is a justification of the claim thatthe guarded recursion is completely unnecessary in the higher order χ-calculus.
Let χ+ be the higher order χ-calculus enriched with the guarded recursion. The
language χ+ can be investigated along the same line as the higher order χ hasbeen. H+ and ≈+ are defined accordingly. It can also be shown that ≈+ is acongruence relation. The definition of a structural translation b from χ+ -terms
to χω -terms is nontrivial only on guarded recursion:
d def
b
b
E|a(X)(X|a[X]))]).
α(x)∗E= (a)((x)α[x].(E|a(X)(X|a[X]))|a[(x)α[x].(The translation b projects the guarded recursion out, as it were.
Theorem 13. For P ∈ H+ , P ≈+ Pb.
Theorem 14. (i) Suppose P and Q are in H. Then P ≈+ Q iff P ≈ω Q.
b(ii) Suppose P and Q are in H+ . Then P ≈+ Q iff Pb ≈ω Q.
δ
δ
0
0
00 b
00
b
c0 ;
(iii) (a) if P → P (P → P ) then P → P (P → P ) such that P 00 ≈ω Pδδc0 .
(b) if Pb → P 00 (Pb → P 00 ) then P → P 0 (P → P 0 ) such that P 00 ≈ω P

Proof. (i) Suppose P, Q are in H. P ≈+ Q clearly implies P ≈ω Q. Supposed|R) ≡ (x)(P |R)db and (x)(Q|R)
b where R ∈ H+ .
P ≈ω Q. Then (x)(P≡ (x)(Q|R),++bb It is now
By theorem 13, (x)(P |R) ≈ (x)(P |R) and (x)(Q|R) ≈ (x)(Q|R).
ω+
easy to see that ≈ is a local bisimulation up to ≈ .
b By (i) Pb ≈+ Q
b iff Pb ≈ω Q.
b(ii) By theorem 13, P ≈+ Q iff Pb ≈+ Q.
tu
As χ+ extends the first order χ, so does the higher order χ-calculus in viewof Theorem 13 and Theorem 14.

6.4

Full Integration

An integration of χ with the full λ is the higher order calculus extended with
E→F.
α[E] → α[F ]The operational semantics of the full λ-calculus can be simulated in the fully
integrated calculus. The encoding is the following:def[[x]]u = x[u]|Xdef[[λx.M ]]u = (x)(v)(u[v].u[x]|x(X)[[M ]]v )def[[M N ]]u = (x)(v)([[M ]]v |v[u].v[x]|x[(w)(x[w]|[[N ]]w )]).
Theorem 15. Suppose M is a λ-term. If M → N then [[M ]]u →+ [[N ]]u .
Definition 9 now gives rise to an equivalence relation on the set of all termsof the fully integrated calculus. The results in Sect. 6.2 and Sect. 6.3 also holdfor this language. The (i) through (iv) of Theorem 10 also hold. But so far wehaven’t been able to prove the (v) of Theorem 10 for the fully integrated calculus.

7

Remark on Pragmatics

In the formulation of χ-calculus, we use the same set of names for both global
and local names. But conceptually the identification is not always helpful. The
standard bisimilarity ([6]) for the π-processes is not closed under input prefixing
operation. This is because the variable names and the free names are regarded
as semantically different in this approach. Sangiorgi’s open bisimilarity is congruent. But in that approach local names are treated differently. In χ-calculus,
both local and global names are variable names, which is what local bisimilarity assumes. The situation is similar to that in λ-calculus, where both free andclosed variables are, well, variables that can be instantiated by any λ-terms.
But variable names alone do not suffice in practice. This is clear from themobile process interpretation of object oriented languages ([10]). The usual practice is to postulate that N consists of two parts: a set Nv of variable names anda set Nc of constant names. We can now define a χ-process to be a χ-term inwhich all variable names are localized. So in χ-processes there are two kinds of
local names: local variable names and local constant names. A communication
either identifies two local variable names or replaces a local variable name by alocal or global constant name. A communication between two constant names is
αa α[a] α(a)prohibited. Let β range over {→, →, → , → | a ∈ Nc , α ∈ Nc ∪ Nc }.
Definition 16. Let R be a binary relation on the set of χ-processes. R is aβsimulation if P RQ implies that if P → P 0 then there exists some Q0 such thatβ̂Q ⇒ Q0 and P 0 RQ0 . The relation R is a bisimulation if both R and its reverse
are simulations. The bisimilarity ≈χ is the largest bisimulation.

The π-calculus can be reexamined in this new setting. The input prefix operation restricts variable names whereas the localization operation always restricts constant names. π-processes are now defined to be those processes inwhich all variable names are restricted by input prefixes. Let γ range overca ca c(a){→, →, →, → | a, c ∈ Nc }.
Definition 17. Let R be a binary relation on the set of π-processes. R is aγ
simulation if P RQ implies that if P → P 0 then there exists some Q0 such thatγ̂Q ⇒ Q0 and P 0 RQ0 . The relation R is a bisimulation if both R and its inverse
are simulations. The bisimilarity ≈π is the largest bisimulation.
The translation given in Sect. 4 works in this practical setting. It establishes anoperational correspondence in the sense of Theorem 7. In addition one has
Theorem 18. For π-processes P and Q, P ≈π Q if and only if P ◦ ≈χ Q◦ .
So practically speaking, π is a subcalculus of χ.

References
1. Abramsky, S.: Proofs as Processes. Theoretical Computer Science 135 (1994) 5–9
2. Barendregt, H.: The Lambda Calculus: Its Syntax and Semantics. 1984
3. Bellin, G., Scott, P.: Remarks on the π-Calculus and Linear Logic. TheoreticalComputer Science 135 (1994) 11–65
4. Girard, J.: Linear Logic. Theoretical Computer Science 50 (1987) 1–102
5. Milner, R.: Functions as Processes. Journal of Mathematical Structures in Computer Science 2 (1992) 119-141
6. Milner, R., Parrow, J., Walker, D.: A Calculus of Mobile Processes. Information
and Computation 100 (1992) 1–40 (Part I), 41–77 (Part II)
7. Plotkin, G.: Call-by-Name, Call-by-Value and the λ-Calculus. Theoretical Computer Science 1 (1975) 125-159
8. Sangiorgi, D.: A Theory of Bisimulation for π-Calculus. Proc. CONCUR 93, LNCS
715 (1993) 127–142
9. Thomsen, B.: Plain CHOCS—A Second Generation Calculus for Higher Order
Processes. Acta Informatica 30 (1993) 1–59
10. Walker, D.: Objects in the π-Calculus. Information and Computation 116 (1995)
253–271