Variations on Mobile Processes ?
Yuxi Fu 1
Department of Computer Science, Shanghai Jiaotong 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 classical proofs. Two bisimilarities, local
bisimilarity and barbed bisimilarity, on chi processes are studied and are shown to becongruence relations. The former equivalence turns out to be strictly stronger thanthe latter. It is shown that chi calculus is capable of modeling sequential computation in that it captures the operational semantics of call-by-name lambda calculus.
A translation from pi calculus to chi calculus is given, demonstrating that, practically speaking, pi is a sublanguage of chi. A higher order version of chi calculus is
proposed and examined. It combines the communication mechanism of chi calculus
and the recursion mechanism of full lambda calculus, and therefore extends both.
Key words: concurrency theory, process algebra, mobile process, bisimulation

1

Introduction

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 ([8]) and is well understood. In retrospect, the λ-calculus can be seen as a fallout of proof theory. The CurryHoward’s proposition-as-type principle allows one to code up constructive
proofs as typed terms (proof-as-term). 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 thesimply typed λ-calculus by removing all typing information. Of course the λcalculus did not come into existence this way. But this way of looking at themodel emphasizes its connection to proof theory ([59]).
? Theoretical Computer Science, 221(1): 327-368, 1999.
1

E-mail: fu-yx@cs.sjtu.edu.cn.

Preprint submitted to Elsevier Preprint

24 January 2004

In recent years, classical proofs have been investigated in a computational setting. Girard proposed proof nets ([22,23,63]) as term representations of classical linear proofs, see also [3]. These classical terms are typed. The conclusionof a proof derivation is the type of the proof net corresponding to that proof
derivation. The computations of these terms are cut eliminations modeled byrewritings of graphs. As the terms are typed, cuts happen between nodes ofcorrelated types. Abramsky’s proof-as-process interpretation ([4,15]) 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 the sequential world.
If one intends to push the analogy between constructive proof/sequential
computation on one hand and classical proof/concurrent computation on theother, one wonders what the computational aspect of classical proofs would
suggest for constructing a model of concurrent computation. This paper investigates a concurrent computation model obtained by reversing the roles of
proofs and processes in Abramsky’s paradigm. That is to say that we regard
communications as cut eliminations. The way to arrive at such a model ofcommunication echoes that in the sequential world. As the ‘minimal logic’ ina classical scenario, we take the multiplicative linear logic. There is nothingcanonical about this choice. As the typed classical terms we take of course theproof nets. Processes are then obtained by, roughly speaking, removing thetyping information.
Ignoring units, the multiplicative linear logic has the following rules:

Γ, A ∆, B
A, A⊥

Axiom

Γ, ∆, A⊗B

Γ, A, B⊗Γ, A℘B

Γ, C℘∆, C ⊥Γ, ∆CutUsing these rules, a sequent might have two derivation trees that differ only
in inessential orders of applications of rules. A proof net is construed as a
canonical representation of proof derivations with inessential differences. The
sequent A⊗B, A⊥ ℘B ⊥ , for instance, has a unique proof net as follows:


A j



A⊥ jPP jB


@
R j
@
)


j
B⊥

PP
P
q j

A⊥ ℘B ⊥A⊗B

The first step towards a concurrent model is to abstract away the logicalaspect of proof nets but keep its proof theoretical content. The above proof
net becomes
2





A j

A⊥ jPP jB


@
R j
@
)


jB ⊥

PP
P
q j

C⊥

C

There are two kinds of edges in the net. So the second step is to transformthe net into a graph in which all edges are directed arrows:
j
j
@
@
R j ⊥
@
R
@
A j A⊥ jPP jB
B

P
@
PP
R j
@
)

q j

C⊥

C

In the third step, we leave out the typing information while recording thecorrelation information by labels on arrows. We thus arrive at an untyped
graph
+ j@-

+ j@-

R j
@
R j
@
j
j
P
P

P
@
+
R j
@
)  + - PPq j-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 theconclusion nodes, the latter representing the conclusions of the corresponding
proof. When forming new nets, it is the conclusion nodes that interact witheach other. In other words, nodes in a proof net can be classified into internal(local) nodes and external (global) nodes. In order to distinguish the two kindsof node in the untyped graph, we label the conclusion nodes with small letters:
+ j@-

+ j@R
@
R j
@
j
j
j
P
P

P
@
+
R aj
@
)  + - PPq bj We call graphs of this kind reaction graphs. The formal definition is as follows,
where N is a set of names ranged over by lower case letters.
Definition 1 A finite directed graph is a quadruple hN, E, d0 , d1 i where both
N and E are finite sets, d0 and d1 are functions from E to N specifying
respectively the source and the target nodes of arrows. A reaction graph is a
sextuple hN, E, d0 , d1 , o, ei where hN, E, d0 , d1 i is a finite directed graph, o isa partial function from N to N that is injective on its domain of definition,and e is a function from E to {−, +}.
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 in3

a generalized and distilled form. The following are two examples of reaction
graphs:
jH
aj
bj
H

H
j j
+ + +H- 6++ + 6+*?? 
?

j
mj
mj
 +
In the above diagrams, a local node is drawn as a cycle while a global node isdrawn with its label inside a cycle.
The labels of the arrows in a reaction graphs indicate the polarities of nodes
with respect to each other. In the above right graph, the node labeled by a(b) shows up negative (positive) polarity to the node labeled m.
Computations with reaction graphs are cut eliminations. A cut elimination
happens between a local node and a global or local node. When they show
up opposite polarities to a same node, they can react by removing the twoarrows indicating the polarities and coalescing the two nodes. We are not going
to define formally cut-eliminations in reaction graphs. The interested reader
is referred to [18]. Here we use an example to illustrate the basic idea. The
following is an example of two consecutive cut-eliminations:
j

mj

6
- 6
+
? +

⇒

j

mj

mj

I
@
6
- @+
⇒
@
j
j


?
j

- j
In the left reaction graph, the two upper nodes show up opposite polarities tothe left bottom node. This cut is eliminated in the first reduction. The twoarrows are removed and the two upper nodes are coerced with the resulting
node labeled by m. In the middle reaction graph, the two bottom nodes withthe arrows pointing to the node labeled m form a cut. The second reduction
eliminates the cut. In the final reaction graph, we can garbage-collect the
detached global node. So a configuration of the form, say,
j
xj
−@
R j+
@
m
in a reaction graph is a cut. It’s elimination deletes the two arrows and coerces
the two source nodes, dragging the remaining arrows all the way. The idea of
this paper is to think of this cut-elimination as a communication in which x
is exported through m to instantiate a local node. To develop the idea, weneed a process-like notation for reaction graphs. Let us define graph terms by
abstract syntax as follows:
G := 0 | m[x] | m[x] | (x)G | G|G0
where 0 is the empty reaction graph; m[x] and m[x] are respectively the fol4

lowing reaction graphs:
xj +- mjxj -- mj(x)G is obtained from the reaction graph G by removing the label x from
G; G|G0 is the amalgamation of G and G0 , coercing nodes with same labels.
For example the amalgamation of the two reaction graphs given right after
Definition 1 is the following reaction graph
j
aj
bj
@
I + 6+ 6@ - +- 6@-@
+
? +
@
+
R
@
j j
j
- m
+
+
In the process-like notation, the two consecutive cut-eliminations in the previous example can 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.
It is clear from the above example that communications in the calculus ofreaction graphs amount to identifications of objects. This deviates from thetraditional view that communications are instantiations of formal parameters.
The calculus of graphs only deals with finite step computations. To achieve
Turing computability, we extend the language with standard process combinators. More specifically, guarded replication is incorporated to admit infinite computation, whereas sequentiality operator is introduced to enhance
the control power of the language. The resultant language will be referred toas χ-calculus, where χ stands for exchange of information. This paper initiates an investigation of this computation model. In Section 2 and Section 3
we examine the semantics of χ-processes. Various possible bisimilarities on
χ-processes are proposed and compared. It is shown that they boil down to
two distinguished congruence relations: local bisimilarity and barbed bisimilarity. The former is strictly finer than the latter. The language is related tothe π-calculus in Section 4. It is argued that in practice one can regard the
π-calculus as a sublanguage of the χ-calculus. In Section 5 it is pointed outthat the operational semantics of the call-by-name λ-calculus can be readily
captured in the χ-calculus. The investigation of the language is continued in
Section 6 by integrating it with λ-calculus. In Section 7 the cut-eliminationas-communication paradigm is recast in an algebraic setting by constructinga ∗-autonomous category of χ-processes. Some final remarks are made in Section 8, where related works are discussed.
Preliminary results of this paper have been announced in [17]. Some resultsfrom [16] have also been incorporated.
5

2

A Model for Concurrent Computation

The χ-calculus is basically the calculus of reaction graphs enriched with thesequentiality operator and recursion found typically in process algebra. The
operational semantics of the language can be defined in terms of a labeledtransition system ([16]). In this paper we give a reductional semantics forχ-calculus in the style of [11,34].
def

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
α to be m (m) if α is m (m). Let C be the set of χ-processes defined by thefollowing abstract syntax:
P := 0 | α[x].P | P |P 0 | (x)P | α(x)∗P.
As usual 0 is the inactive process. A trailing inactive process will be omitted.
m[x].P and m[x].P are processes that must first perform a communication
through name m before enabling P [y/x], where y is the name received incommunication. Here m is in a subject position while x is in an object position.
P |P 0 is a process in parallel composition form, in which P and P 0 can evolve
independently and may communicate during the course of their evolution.
(x)P is a process in which x is local to P , meaning that (x)P is not allowed
to communicate with another process through name x. The x in this process
is called a local name. The guarded recursion α(x)∗P makes a copy of P withinstantiated x whenever it is called upon. The name x in this process is also
regarded as local. The set of local names appeared in P is denoted by ln(P ),whereas the set of global names, or nonlocal names, in P is designated bygn(P ). Set n(P ) is the union of ln(P ) and gn(P ). We adopt the well-known
α-convention saying that a local name in a process can be replaced by a freshname without affecting the syntax of the process.
The notation [y/x] will stand for an atomic substitution. The result of substituting y for x throughout P is denoted by P [y/x]. Local names in P need berenamed to avoid y being captured. A substitution [y1 /x1 ] . . . [yn /xn ] is a concatenation of atomic substitutions. The effect of a substitution on a processdef
def
is defined as follows: P [] = P ; P [y1 /x1 ] . . . [yn /xn ] = (. . . P [y1 /x1 ] . . .)[yn /xn ].
Here [] is the empty substitution. The set of substitutions will be ranged overby σ.
To simplify the algebraic theory of the language, a structural congruence is
imposed on the members of C.
Definition 2 The structural relation = is the least congruence on χ-processes
that contains:6

(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. It follows that we can write P1 |P2 |P3 without ambiguity.
The reductional semantics for χ-calculus can now be defined as follows:(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 → P0P |Q → P 0 |Q(x)P → (x)P 0

The first reduction rule can be replaced by the following two:(x)(R|α[x].P |α[y].Q) → R[y/x]|P [y/x]|Q[y/x], where x 6= y(x)(R|α[x].P |α[x].Q) → (x)(R|P |Q)
As we regard the structural congruence = as a syntactical equality, the following ruleP = P0P →Q

Q = Q0P 0 → Q0
comes for free.
To help understand the communication rules, we give some examples. In thefollowing reductions, 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)(R|m[x].P |m[x].Q) → (x)(R|P |Q).
In the first example, a communication replaces the local name x by the
global name y throughout the process over which the localization operator (x) applies. The global name y in P however remains unchanged. In
other words, global names overwrite. Notice that (x)(R[y/x]|P [y/x]|Q[y/x]) =7

R[y/x]|P [y/x]|Q[y/x]. In the second example the process m[y].P lies outside
the scope of the localization operator (x). So the communication through mdoes not affect P . In order to use the rule, notice that m[y].P |(x)(R|m[x].Q) =m[y].P |(z)(R[z/x]|m[z].Q[z/x]) = (z)(m[y].P |R[z/x]|m[z].Q[z/x]) for a freshz. So m[y].P |(x)(R|m[x].Q) → (P |R[z/x]|Q[z/x])[y/z] = P |R[y/x]|Q[y/x].
The third reduction is obtained from the second by applying the second structural rule. How does the forth reduction come about? Well for a fresh name z,(x)m[x].P |(y)m[y].Q = (z)((x)m[x].P |m[z].Q[z/y]). So the reduction can be
deduced as in the previous case. The final reduction is an example of communication where two processes exchange a same local name. This reduction isan instance of the first reduction rule where y is x.
It is clear from these examples that the localization operator in the χ-calculus
acts as an effect delimiter. A communication either instantiates a local nameby a global name or identifies two local names.
Let →+ (→∗ ) be the transitive (reflexive and transitive) closure of →. We
will denote by ~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 . The length of ~x is denoted by |~x|. If ~a = a1 . . . an then ~a[~x] denotes
a1 [x1 ]| . . . |an [xn ].
Before ending this section, we state a technical lemma to be used later on.
Lemma 3 If P → Q then P [y/x] → Q[y/x].

Proof: By structural induction it is easy to show that P1 = P2 implies
P1 [y/x] = P2 [y/x], from which the result follows. 2

3

Bisimulation Equivalence

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

α(x)(x)P → P 0

8

α(x)

α(x)∗P → α(x)∗P |PδP → P0ln(δ) ∩ gn(Q) = ∅δ

P → P0δ

x 6∈ n(δ)δ

P |Q → P 0 |Q(x)P → (x)P 0

In the rules, ln(δ) is {x} when δ is α(x); it is the empty set otherwise; n(δ) isδδ
the set of names in δ. In sequel, ⇒ denotes the relation →∗ →→∗ .
The properties stated in the following lemma can be easily proved by structural
induction.
α[x]Lemma 4 (i) If P → P 0 then some ~z, P1 and P2 exist such that P =(~z)(P1 |α[x].P2 ), P 0 = (~z)(P1 |P2 ) and x 6∈ {~z}.
αx(ii) If P → P 0 then some ~z, y, P1 and P2 exist such that either
P = (~z)(y)(P1 |α[y].P2 ) and P 0 = (~z)(P1 [x/y]|P2 [x/y])orP = (~z)(P1 |α(y)∗P2 ) and P 0 = (~z)(P1 |P2 [x/y]|α(y)∗P2 ).
α(x)(iii) If P → P 0 then some ~z, P1 and P2 exist such that either
P = (~z)(x)(P1 |α[x].P2 ) and P 0 = (~z)(P1 |P2 )orP = (~z)(P1 |α(x)∗P2 ) and P 0 = (~z)(P1 |P2 |α(x)∗P2 ).
One could have combined the labeled transition system with the reduction
relation → to form a system defining the operational semantics of χ, following
the standard approach.We have however chosen to separate the semantics ofcommunication from that of communicability. In either way, one has to provea number of bookkeeping lemmas. Here are two such lemmas.
Lemma 5 Suppose P, Q ∈ C.
α[x]αx(i) If P → P 0 and Q → Q0 then P |Q → P 0 |Q0 .
α[x]

α[y]

(ii) If P → P 0 and Q → Q0 then (x)(P |Q) → (x)(P 0 [y/x]|Q0 [y/x]).
αx

Proof: Let’s see how to prove (i). Suppose P → P 0 . By Lemma 4 some ~z, y,
P1 and P2 exist such that either
P = (~z)(y)(P1 |α[y].P2 ) and P 0 = (~z)(P1 [x/y]|P2 [x/y])9orP = (~z)(P1 |α(y)∗P2 ) and P 0 = (~z)(P1 |P2 [x/y]|α(y)∗P2 ).
α[x]Similarly Q → Q0 implies that some ~z, Q1 and Q2 exist such that Q =(~z)(Q1 |α[x].Q2 ) and Q0 = (~z)(Q1 |Q2 ). Now either
P |Q = (~z)(y)(P1 |α[y].P2 )|(~z)(Q1 |α[x].Q2 )→ (~z)(P1 [x/y]|P2 [x/y])|(~z)(Q1 |Q2 )= P 0 |Q0
or
P |Q = (~z)(P1 |α(y)∗P2 )|(~z)(Q1 |α[x].Q2 )→ (~z)(P1 |P2 [x/y]|α(y)∗P2 )|(~z)(Q1 |Q2 )= P 0 |Q0 .
The proof of (ii) is similar. 2
The next lemma can be proved by simple induction on derivation.
α(x)

αx

Lemma 6 If P → P 0 and x 6∈ gn(P ) then P → P 0 .
3.1

Local Bisimilarity

A bisimulation equivalence ([44,33]) should be neither too strong nor too weak.
From an algebraic point of view, one looks for a congruence relation. Howevera bisimulation congruence is not always the best equivalence from an observational viewpoint. A bisimulation equivalence for χ-processes 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 familiar ideathat two pieces of program are considered observationally equivalent if andonly if placing them in a same context results in two pieces of observationallyequivalent program. Working explicitly with contexts is unnecessary in our
setting due to the presence of the structural equality =.
Definition 7 Let R be a subset of C×C. The relation R is a local simulation
if P RQ implies that for any process R and any sequence ~x of names it holds
that
δ

δ

if (~x)(P |R) ⇒ P 0 then Q0 exists such that (~x)(Q|R) ⇒ Q0 and P 0 RQ0 .
10

The relation R is a local bisimulation if both R and its inverse are local simulations. The local bisimilarity ≈ is the largest local bisimulation.
Local bisimulations are closed under localization and composition operations
at each bisimulation step. This is not at all a strong requirement. Any usefulbisimulation equivalence should at least be closed under these operations; andif a bisimulation equivalence is closed under a particular operation, it is closed
under that operation at each bisimulation step.
It is clear that ≈ is an equivalence relation. Let’s say that a binary relation R
on C is locally closed if P RQ implies (~x)(P |R)R(~x)(Q|R) for any R ∈ C andany sequence ~x of names. To show that a locally closed relation R is a local
simulation, one only has to show that if P RQ thenδδ

there exists some Q0 such that Q ⇒ Q0 and P 0 RQ0 whenever P ⇒ P 0 .
Local (bi)simulation can be defined in a more familiar way as given in thenext lemma.
Lemma 8 R is a local simulation if and only if P RQ implies that for any
process 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 alternative definition is more useful in practice. The next lemma follows
trivially from the definition. But it will be used again and again.
Lemma 9 The following properties hold:(i) If P ≈ Q and P → P 0 then Q0 exists such that Q →∗ Q0 and P 0 ≈ Q0 .
δδ(ii) If P ≈ Q and P → P 0 then Q0 exists such that Q ⇒ Q0 and P 0 ≈ Q0 .
As usual, local bisimulation up to ≈ is a useful tool for proving two χ-processes
being locally bisimilar ([57]).
Definition 10 Let R be a subset of C×C. The relation R is a local simulation
up to ≈ if P RQ implies that for any process R and any sequence ~x of names
it holds thatδδ

if (~x)(P |R) ⇒ P 0 then there exists some Q0 such that (~x)(Q|R) ⇒ Q0 andP 0 ≈ R ≈ Q0 .
R is a local bisimulation up to ≈ if both R and its inverse are local simulations
up to ≈.
A local bisimulation R up to ≈ satisfies the standard property of being contained in ≈.
11

Lemma 11 Suppose that R ⊂ C × C satisfies the following property: if P RQ,
then for any process R and any sequence ~x of names, it holds that(i) if (~x)(P |R) → P 0 then Q0 and Q00 exist such that (~x)(Q|R) →∗ Q0 ≈ Q00
and P 0 RQ00 ;(ii) if (~x)(Q|R) → Q0 then P 0 and P 00 exist such that (~x)(P |R) →∗ P 0 ≈ P 00
and P 00 RQ0 ;δδ(iii) if (~x)(P |R) → P 0 then Q0 and Q00 exist such that (~x)(Q|R) ⇒ Q0 ≈ Q00
and P 0 RQ00 ;δδ(iv) if (~x)(Q|R) → Q0 then P 0 and P 00 exist such that (~x)(P |R) ⇒ P 0 ≈ P 00
and P 00 RQ0 .
Then R is a local bisimulation up to ≈.

Proof: Using lemma 9, it is easy to show that if P RQ and (~x)(P |R) →∗ Qδδ(or (~x)(P |R) ⇒ Q) then Q0 exists such that (~x)(Q|R) →∗ Q0 (or (~x)(Q|R) ⇒Q0 ) and P 0 ≈ R ≈ Q0 . 2

In the rest of this section, we prove that ≈ is a congruence relation. We
establish a few technical lemmas first.
Lemma 12 If P →∗ P1 ≈ Q and Q →∗ Q1 ≈ P then P ≈ Q.

δ

Proof: Suppose ~x are names and R a χ-process. If for example (~x)(P |R) →δP 0 , then some Q0 exists such that (~x)(Q1 |R) ⇒ Q0 and P 0 ≈ Q0 . But thenδ(~x)(Q|R) ⇒ Q0 . 2

To show that local bisimilarity ≈ is closed under substitution, we need thefollowing auxiliary result.
Lemma 13 Suppose a does not appear in P . If (~x)(P |R) → (x~0 )(P 0 |R0 ) is inay
duced by a communication within P and (x~0 )(P 0 |R0 ) → (x~00 )(P 00 |R00 ) is induceday
by an action from R0 , then x~1 , P1 , R1 exist such that (~x)(P |R) → (x~1 )(P1 |R1 )is induced by the same action and (x~1 )(P1 |R1 ) → (x~00 )(P 00 |R00 ) is induced by
the same communication.

Proof: This is an easy proof using Lemma 4 and Lemma 3. 2

The next lemma is crucial in showing that ≈ is a congruence relation. It is
the first indication that local bisimilarity is algebraically appropriate.

12Lemma 14 If P ≈ Q then P σ ≈ Qσ for an arbitrary substitution σ.

Proof: Suppose P ≈ Q. We only have to show that for two arbitrary names
ayx, y one has that P [y/x] ≈ Q[y/x]. Let a be a fresh name. Then (x)(P |a[x]) →ay
P [y/x]. So Q1 exists such that (x)(Q|a[x]) ⇒ Q1 ≈ P [y/x], which can befactorized as(x)(Q|a[x]) →∗ (x)(Q2 |a[x])ay→ Q2 [y/x]→∗ Q1 .
By Lemma 13, this sequence of actions can be reorganized as follows:ay(x)(Q|a[x]) → Q[y/x]→∗ Q3→∗ Q1 .
Similarly some P1 exists such that P [y/x] →∗ P1 ≈ Q[y/x]. By Lemma 12,
P [y/x] ≈ Q[y/x]. 2

We now come to the main result of the section.
Theorem 15 ≈ is a congruence equivalence: if P ≈ Q and O ∈ C then(i) α[x].P ≈ α[x].Q;(ii) P |O ≈ Q|O;(iii) (x)P ≈ (x)Q;(iv) α(x)∗P ≈ α(x)∗Q.

Proof: We prove only (ii) and (iv). The other two can be proved similarly.
(ii) We show that {(P |O, Q|O) | P ≈ Q ∧ O ∈ C} is a local bisimulation.
Suppose R ∈ C and ~x is a sequence of names. Then clearly (~x)((P |O)|R) =(~x)(P |(O|R)) and (~x)((Q|O)|R) = (~x)(Q|(O|R)). So this case follows immediately from definition. (iv) Let R be the following locally closed relation{((~x)(m(y)∗P |R), (~x)(m(y)∗Q|R)) | P ≈ Q, R ∈ C, m, ~x names}.
Suppose (~x)(m(y)∗P |R)R(~x)(m(y)∗Q|R) and (~x)(m(y)∗P |R) → P 0 . There
are these cases:• (~x)(m(y)∗P |R) → P 0 is induced by a communication within R. Then P 0 =13

(x~0 )(mσ(y)∗P σ|R0 ) for some substitution σ. But then (~x)(m(y)∗Q|R) →(x~0 )(mσ(y)∗Qσ|R0 ). By Lemma 14, P σ ≈ Qσ. Therefore(x~0 )(mσ(y)∗P σ|R0 )R(x~0 )(mσ(y)∗Qσ|R0 ).
• (~x)(m(y)∗P |R) → P 0 is induced by a communication between m(y)∗P and
R. Then P 0 is of the form (~x)(m(y)∗P |P [a/y]|R0 ). Similarly(~x)(m(y)∗Q|R) → (~x)(m(y)∗Q|Q[a/y]|R0 ).
By Lemma 14 P [a/y] ≈ Q[a/y]. By (ii) and (iii), (~x)(m(y)∗Q|P [a/y]|R0 ) ≈(~x)(m(y)∗Q|Q[a/y]|R0 ).
δ
δ• Similarly, if (~x)(m(y)∗P |R) → P 0 , then (~x)(m(y)∗Q|R) → Q0 and P 0 RQ00 ≈Q0 for some Q0 and Q00 .
So the conditions of Lemma 11 are satisfied. It then follows that R is a local
bisimulation up to ≈. 2
The actions of the χ-calculus can be classified into three groups: the input
α[x]αx
actions of the form →, the (free) output actions of the form → and theα(x)restricted output actions of the form → . In defining local bisimilarity, we
assume that all these actions are observable. What if we ignore actions of acertain type. In other words, what bisimilarities do we obtain if only actions in
one or two of the three groups are declared observable? We now look into twobisimulation equivalence relations which distinguish two processes only when
they fail to simulate each other’s free, respectively restricted, output actions.
Definition 16 Suppose R is a binary relation on χ-processes. It is called an
output bisimulation if P RQ implies that for any R and any sequence ~x ofnames it holds that
α[y]
α[y]
(i) if (~x)(P |R) ⇒ P 0 then Q0 exists such that (~x)(Q|R) ⇒ Q0 and P 0 RQ0 ;
α[y]

α[y]

(ii) if (~x)(Q|R) ⇒ Q0 then P 0 exists such that (~x)(P |R) ⇒ P 0 and P 0 RQ0 .
The output bisimilarity ≈o is the largest output bisimulation.
For ≈o the observables are free output actions. A seemingly different bisimilarity is obtained if the observables are confined to restricted output actions.
Definition 17 Suppose R is a binary relation on χ-processes. It is called a
restricted output bisimulation if P RQ implies that for any R and any sequence~x of names it holds that
α(y)
α(y)
(i) if (~x)(P |R) ⇒ P 0 then Q0 exists such that (~x)(Q|R) ⇒ Q0 and P 0 RQ0 ;
α(y)

α(y)

(ii) if (~x)(Q|R) ⇒ Q0 then P 0 exists such that (~x)(P |R) ⇒ P 0 and P 0 RQ0 .
The restricted output bisimilarity ≈ro is the largest restricted output bisimulation.
14

Definition 16 and Definition 17 suggest immediately another bisimilarity which
equates two processes if no environment can tell them apart under the assumption that the only observables are input actions. We will come back to it lateron.
The next theorem renders redundant any further study of the two equivalence
relations just defined. It also implies that the algebraic theory of χ-calculus
would not be affected if restricted output actions are ignored.
Theorem 18 ≈, ≈o and ≈ro are one and the same relation.

Proof: The proof consists of following parts:• It is clear that ≈⊆≈o and ≈⊆≈ro .
αx• Suppose P ≈o Q and P → P 0 . Let a be a fresh name throughout the rest of
a[a]
a[a]
the proof. Now P |α[x].a[a] ⇒ P 0 must be matched up by Q|α[x].a[a] ⇒ Q0
αx
for some Q0 such that P 0 ≈o Q0 . It follows that Q ⇒ Q0 .
α(x)• Suppose P ≈o Q and P → P 0 . As in the previous case one obtains someα(x)αxQ0 such that Q ⇒ Q0 and P 0 ≈o Q0 . By Lemma 6, Q ⇒ Q0 .
α[x]
α(x)
• Suppose P ≈ro Q and P → P 0 . Then (x)(P |a[x]) → P 0 |a[x]. So Q1 exists
α(x)

a(x)

such that (x)(Q|a[x]) ⇒ Q1 and P 0 |a[x] ≈ro Q1 . Moreover (x)(P 0 |a[x]) →a(x)P 0 must be simulated by (x)Q1 ⇒ Q0 ≈ro P 0 for some Q0 . It follows thatα[x]Q1 must be of the form Q01 |a[x] and Q ⇒ Q01 ⇒ Q0 .
We are done by noticing that both ≈o and ≈ro are by definition closed undercomposition and localization operations. 2

3.2

Incremental Bisimilarity

Local bisimulation as defined in Definition 7 is well-motivated. But they
have the obvious problem of being highly intractable. In many circumstances,a much more manageable description is desirable. This section provides a
sharper characterization of local bisimilarity. Let go(P ) be the set of global
objective names appeared in P .
Definition 19 Let R be a subset of C×C. The relation R is an incremental
simulation if P RQ implies that(i) if P → P 0 then there exists some Q0 such that Q →∗ Q0 and P 0 RQ0 ;δδ(ii) if P → P 0 then there exists some Q0 such that Q ⇒ Q0 and P 0 RQ0 ;and if go(P |Q) 6= ∅ then for some fresh name a and each name x in go(P |Q)(iii) if (x)(P |a[x]) → P 0 then Q0 exists such that (x)(Q|a[x]) →∗ Q0 and
15

P 0 RQ0 ;δδ(iv) if (x)(P |a[x]) → P 0 then Q0 exists such that (x)(Q|a[x]) ⇒ Q0 and P 0 RQ0 .
The relation R is an incremental bisimulation if both R and its inverse are
incremental simulations. The incremental bisimilarity ≈r is the largest incremental bisimulation.
It can be easily seen that Lemma 12 and Lemma 14 hold for ≈r as well. The
following is a simple yet useful technical lemma.
Lemma 20 Suppose a 6∈ n(P |Q). Then(i) (x)(P |a[x]) ≈r (x)(Q|a[x]) implies P ≈r Q;(ii) P |a[x] ≈r Q|a[x] implies P ≈r Q.
a(x)

a(x)

Proof: (i) As (x)(P |a[x]) → P , Q1 exists such that (x)(Q|a[x]) ⇒ Q1 ≈ra(x)P . Now (x)(Q|a[x]) ⇒ Q1 implies that Q →∗ Q1 . Similarly P1 exists suchthat P →∗ P1 ≈r Q. By Lemma 12, P ≈r Q. (ii) is proved similarly. 2
Lemma 21 Suppose P, Q and O are χ-processes. Let ~x, ~y and ~a be names
such that ~a are pairwise distinct, |~a| = |~y | and {~a} ∩ ({~x, ~y } ∪ gn(P |Q)) = ∅.
If P ≈r Q then (~x)(P |O|~a[~y ]) ≈r (~x)(Q|O|~a[~y ]).
Proof: Let R be the following relation
















P ≈r Q and O ∈ C













condition of the lemma ((~x)(P |O|~a[~y ]), (~x)(Q|O|~a[~y ])) ~x, ~y and ~a satisfy the.

Suppose (~x)(P |O|~a[~y ])R(~x)(Q|O|~a[~y ]). We examine some major cases:αz• (~x)(P |O|~a[~y ]) → (x~0 )(P1 |O[z/x1 ]|~a[y~0 ]) is induced by an action from P thatαz
substitutes z for some x1 in {~x}. Then (x1 )(P |b[x1 ]) → P1 |b[z] for someαz
new b. So some Q1 exists such that (x1 )(Q|b[x1 ]) ⇒ Q1 |b[z] and P1 |b[z] ≈r
αz ~0Q1 |b[z]. The former implies (~x)(Q|O|~a[~y ]) ⇒ (x )(Q1 |O[z/x1 ]|~a[y~0 ]) and thelatter implies P1 ≈r Q1 by Lemma 20.
• (~x)(P |O|~a[~y ]) → (x~0 )(P1 |O1 |~a[y~0 ]) is induced by a communication within P
in which some x1 ∈ {~x} participates and is replaced by some global z. Letb be a fresh name. Then (x1 )(P |b[x1 ]) → P1 |b[z]. So Q1 exists such that(x1 )(Q|b[x1 ]) →∗ Q1 |b[z] ≈r P1 |b[z]. It follows by Lemma 20 that P1 ≈r Q1 .
Also (~x)(Q|O|~a[~y ]) →∗ (x~0 )(Q1 |O1 |~a[y~0 ]).
• (~x)(P |O|~a[~y ]) → (x~0 )(P1 |O|~a[~y ]) is induced by a communication in P between some α[x1 ].A and α[x1 ].B where x1 ∈ {~x}. Then (x1 )(P |b[x1 ]) →16

(x1 )(P1 |b[x1 ]) for some fresh b. Therefore (x1 )(Q|b[x1 ]) →∗ (x1 )(Q1 |b[x1 ])and (x1 )(P1 |b[x1 ]) ≈r (x1 )(Q1 |b[x1 ]). By Lemma 20, P1 ≈r Q1 . It is also
clear that (~x)(Q|O|~a[~y ]) →∗ (x~0 )(Q1 |O|~a[~y ]).
αz• (~x)(P |O|~a[~y ]) → (x~0 )(P [z/x1 ]|O1 |~a[y~0 ]) is induced by an action in O that
αzreplaces some x1 ∈ {~x} by z. Then (~x)(Q|O|~a[~y ]) → (x~0 )(Q[z/x1 ]|O1 |~a[y~0 ]).
By Lemma 14, P [z/x1 ] ≈r Q[z/x1 ].
• (~x)(P |O|~a[~y ]) → (x~0 )(P1 |O1 |~a[y~0 ]) is induced by a communication between
some α[x1 ].A in P and some α[z].B in O where x1 ∈ {~x}. Then for someαz
αzfresh b, (x1 )(P |b[x1 ]) → P1 |b[z]. So Q1 exists such that (x1 )(Q|b[x1 ]) ⇒Q1 |b[z]. Now P1 ≈r Q1 follows from Lemma 20 and also (~x)(Q|O|~a[~y ]) →∗(x~0 )(Q1 |O1 |~a[y~0 ]).
Conclude that R is an incremental bisimulation. 2
A consequence of this lemma is that ≈r is closed under parallel compositionand localization operation.
Corollary 22 Suppose P, Q, O are χ-processes. If P ≈r Q then P |O ≈r Q|Oand (x)P ≈r (x)Q.
Theorem 23 ≈r is the same as ≈.
Proof: ≈⊆≈r is obvious. The reverse inclusion holds by Corollary 22 andthe definitions of ≈ and ≈r . 2
It follows from Theorem 15 and Theorem 23 that ≈r is closed under all combinators.
Another immediate consequence of Theorem 23 is that one can confine one’s
attention to finite R in Definition 7. This is a handy property when it comes toproving conservativity results. Thus the χ-calculus is a conservative extension
over the subcalculus of finite χ-processes, which is in turn conservative overthe calculus of reaction graphs.

3.3

Barbed Bisimilarity

To study the algebraic property of the χ-calculus, we have introduced local
bisimulations. They are not very tractable technical tool, but seem to be themost reasonable one for χ-like process algebra. Another sensible class of bisimulations is that of barbed bisimulations introduced in [42]. This section takes
a look at barbed bisimilarity on χ-processes.

17δ

Definition 24 A process P is strongly barbed at a, notation P ↓a, if P → P 0
for some P 0 such that the subject name of δ is a. P is barbed at a, notation
P ⇓a, if some P 0 exists such that P →∗ P 0 ↓a. A binary relation R is barbed if∀a ∈ N .P ⇓a ⇔ Q⇓a whenever P RQ.
Our definition of barbed bisimulation is more similar to Honda and Yoshida’s([27]) than to Milner and Sangiorgi’s ([42]).
Definition 25 Suppose R is a barbed relation on χ-processes. It is called abarbed bisimulation if P RQ implies that for any R and any sequence ~x ofnames 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 barbed bisimilarity ≈b is the largest barbed bisimulation.
In the standard definition of barbed bisimulation, contexts of certain typeare added at the beginning. The resulting barbed bisimilarity is closed undercontexts of that type. In our definition, closure of contexts of certain type isrequired at each bisimulation step. The resulting barbed bisimilarity is also
closed under contexts of that type. It is then obvious that the two definitions
give rise to the same barbed bisimilarity, the largest barbed bisimulation, thereason being that if a bisimulation is closed under contexts of certain type
it is closed under contexts of that type at each bisimulation step. Since weare only interested in the largest barbed bisimulation, it makes no difference
which definition is adopted.
The barbed bisimilarity can be defined in a way that does not mention explicitly the notion of barb. We now define another bisimilarity congruence whichturns out to be the same as barbed bisimilarity.
Definition 26 Suppose R is a binary relation on χ-processes. It is called an
input bisimulation if P RQ implies that for any R and any sequence ~x of names
it holds thatαyαy(i) if (~x)(P |R) ⇒ P 0 then Q0 exists such that (~x)(Q|R) ⇒ Q0 and P 0 RQ0 ;αyαy(ii) if (~x)(Q|R) ⇒ Q0 then P 0 exists such that (~x)(P |R) ⇒ P 0 and P 0 RQ0 .
The input bisimilarity ≈i is the largest input bisimulation.
Theorem 27 ≈i is a congruence equivalence.

Proof: If we replace every occurrence of ≈ by ≈i in the proof of Lemma 14,
we obtain a proof of the following fact: If P ≈i Q then P σ ≈i Qσ for every
substitution σ. So the proof of Theorem 15 actually establishes the congruence
property for ≈i . 2
18

The barbed bisimilarity is a congruence relation. The proof is similar to thatof Theorem 15. Here we give an indirect proof.
Theorem 28 ≈b is the same as ≈i .

Proof: Clearly ≈i is barbed. So ≈i ⊆≈b . Conversely suppose that P ≈b Q andbyby
αx
P → P 0 . Then P |α[x].(y)b[y] ⇒ P 0 for some fresh b. So Q|α[x].(y)b[y] ⇒ Q0
αx
for some Q0 such that P 0 ≈b Q0 . It follows that Q ⇒ Q0 . That is ≈b is an input
bisimulation. 2

For CCS processes, barbed bisimilarity coincides with bisimilarity. For πprocesses with binary choice operator, the problem of whether the two equivalences are the same is still open at the time of writing. The picture in χ-calculus
is different. Local bisimilarity has strictly stronger distinguishing power thanbarbed bisimilarity. Using the choice combinator, we have(x)a[x].(b)(b[x]|b[z]) 6≈ a[z]+(x)a[x].(b)(b[x]|b[z])but(x)a[x].(b)(b[x]|b[z]) ≈b a[z]+(x)a[x].(b)(b[x]|b[z]).
This counter example can be couched in present calculus without the choice
operator:a(x)∗(b)(b[x]|b[z]) 6≈ a[z]|a(x)∗(b)(b[x]|b[z])yeta(x)∗(b)(b[x]|b[z]) ≈b a[z]|a(x)∗(b)(b[x]|b[z]).
On the other hand ≈ is clearly barbed. Therefore one has
Theorem 29 The inclusion ≈⊂≈b is strict.
We have not adopted barbed bisimilarity for a number of reasons. First barbed
bisimulations deal with communications rather than observable actions of processes, which implies that the bisimulation argument is necessary more involved. For one thing, one has to prove that a barbed bisimulation is barbed;
and that is sometimes messy. Second the barbed bisimilarity could be too
weak when comparing χ to other process calculi.
194

Pi Processes as Chi Processes

The χ-calculus can be seen as obtained from the π-calculus ([41]) by replacing the variable names by local names. A question naturally arises as to therelationship between the two languages. We give our answers to the questionin this section.

4.1

Theoretical Result

The χ-calculus we consider in this paper is the minimal χ in the sense that wehave omitted choice and match operators. Consequently we will confine ourattention to π-calculus without these operators. Let P be the set of π-processes
defined as follows:
P := 0 | m(x).P | m[x].P | P |P 0 | (x)P | m(x)∗P.
Here m(x).P and m[x].P are processes of input, respectively output prefix
form. We depart from the standard syntax for output prefix operator of πcalculus purely for the purpose of comparison to the prefix operator in χcalculus. In m(x).P , (x)P and m(x)∗P , the name x is bound. A name isfree if it is not bound. bn(P ), respectively f n(P ), denotes the set of bound,respectively free, names occurred in P . The union of bn(P ) and f n(P ) isdenoted by n(P ). The α-convention is adopted and a structural equality is
imposed on the π-processes in the same way as is done with the χ-processes.
The operational semantics of π-calculus is defined by the following reduction
rules
m(x).P |m[y].Q → P [y/x]|Qm(x)∗P |m[y].Q → m(x)∗P |P [y/x]|Q
mx m[x] m(x)together with the structural rules given in Section 2. Let {→, → , → |m, x ∈δN } be ranged over by →. bn(δ) is {x} if δ = a(x) for some a ∈ N ; it isthe empty set otherwise. n(δ) is the set of names in δ. The labeled transition
system for π-processes is defined as follows:mx

mxm(y).P → P [x/y]m(y)∗P → m(y)∗P |P [x/y]m[x]P → P0m[x]m[x].P → P

m(x)(x)P → P 0

20

m(x)

m(x)∗P → m(x)∗P |PδP → P0bn(β) ∩ f n(Q) = ∅δδP → P0x 6∈ n(β)δ

P |Q → P 0 |Q(x)P → (x)P 0

Many bisimulation equivalences on π-processes have been proposed in literature ([41,51,56,12,24]). What is most relevant in this section is the open
bisimilarity defined in [56]. Actually we will use a version of open bisimilarity
stronger than Sangiorgi’s in that it does not have a separate treatment tolocalization operator.
Definition 30 Let R be a binary relation on the set of π-processes. The relation R is an open bisimulation if P RQ implies that for any substitution σ
it holds that(i) if P σ → P 0 then there exists some Q0 such that Qσ →∗ Q0 and P 0 RQ0 ;(ii) if Qσ → Q0 then there exists some P 0 such that P σ →∗ P 0 and P 0 RQ0 ;δδ(iii) if P σ → P 0 then there exists some Q0 such that Qσ ⇒ Q0 and P 0 RQ0 ;δδ(iv) if Qσ → Q0 then there exists some P 0 such that P σ ⇒ P 0 and P 0 RQ0 .
The open bisimilarity ≈o is the largest open bisimulation.
This open bisimilarity is a congruence equivalence and closed under substitution.
A structural translation from π-processes to χ-processes can be defined asfollows:
def(0)◦ = 0,
def(m(x).P )◦ = (x)m[x].P ◦ ,def(m[x].P )◦ = m[x].P ◦ ,def(P |Q)◦ = P ◦ |Q◦ ,def((x)P )◦ = (x)P ◦ ,def(m(x)∗P )◦ = m(x)∗P ◦ .
The following property can be easily verified.
δLemma 31 Suppose P is a π-process. If P ◦ → P 0 (P ◦ → P 0 ) then P1 existsδsuch that P 0 = P1◦ and P ◦ → P1◦ (P ◦ → P1◦ ).
The next theorem shows that the translation is faithful operationally. It is
proved by induction on derivation.
Theorem 32 For P, Q ∈ P, it holds that(i) P → Q if and only if P ◦ → Q◦ ;
21

mx

mx

(ii) P → Q if and only if P ◦ → Q◦ ;
m[x]

m[x]

m(x)

m(x)

(iii) P → Q if and only if P ◦ → Q◦ ;(iv) P → Q if and only if P ◦ → Q◦ .
mx

Proof: We will prove (ii). If P → Q then by structural induction one canshow that some ~z, y, P1 and P2 exist such that either
P = (~z)(P1 |m(y).P2 ) and Q = (~z)(P1 |P2 [x/y])orP = (~z)(P1 |m(y)∗P2 ) and Q = (~z)(P1 |P2 [x/y]|m(y)∗P2 ).
In the former casemx

P ◦ = (~z)(y)(P1◦ |m[y].P2◦ ) → (~z)(P1◦ |P2◦ [x/y]) = Q◦
and in the latter casemx

P ◦ = (~z)(P1◦ |m(y)∗P2◦ ) → (~z)(P1◦ |P2◦ [x/y]|m(y)∗P2◦ ) = Q◦ .
mx

mx

Suppose now P ◦ → Q◦ . If P is of the form P1 |P2 and P1◦ → Q◦1 then bymx
mx
induction on derivation P1 → Q1 . So P = P1 |P2 → Q1 |P2 = Q. Other casesmx
mx
are equally simple. Conclude that P ◦ → Q◦ always implies P → Q. 2
The translation is also faithful algebraically. The next two lemmas are usedin proving this fact.
Lemma 33 Suppose P is a π-process, R is a χ-process and ~x is a sequenceof names. If (~x)(P ◦ |R) → P 0 is induced by a communication within P ◦ thenP 0 = (~x)(P1◦ |R) and P → P1 .
Proof: If (~x)(P ◦ |R) → P 0 is induced by a communication within P ◦ thenP ◦ → P 00 for some P 00 . This is because all object names in input prefixes inP ◦ are local in P ◦ . By Lemma 31, P ◦ → P1◦ for some P1 such that P1◦ = P 00 .
By Theorem 32, P → P1 . 2
Lemma 34 Suppose P, Q ∈ P, P ≈o Q, R ∈ C and ~x is a sequence of names.
The following properties hold:(i) If (~x)(R|P ◦ ) → P 0 , then x~0 , R0 , P1 and Q1 exist such that P 0 = (x~0 )(R0 |P1◦ ),22

Q →∗ (x~0 )(R0 |Q◦1 ) and P1 ≈o Q1 .
δ(ii) If (~x)(R|P ◦ ) → P 0 , then x~0 , R0 , P1 and Q1 exist such that P 0 = (x~0 )(R0 |P1◦ ),δ
Q ⇒ (x~0 )(R0 |Q◦1 ) and P1 ≈o Q1 .
Proof: The proof of (ii) is simpler than that of (i). So we concentrate on (i).
There are three cases:• (~x)(R|P ◦ ) → P 0 is induced by a communication within R. Then P 0 =(x~0 )(R0 |P ◦ σ). So (~x)(R|Q◦ ) → (x~0 )(R0 |Q◦ σ) and P σ ≈o Qσ.
• (~x)(R|P ◦ ) → P 0 is induced by a communication in P ◦ . Then by Lemma 33,
P 0 = (~x)(R|P1◦ ) and P → P1 . So Q1 exists such that Q →∗ Q1 and P1 ≈o Q1 .
By Theorem 32, (~x)(R|Q◦ ) →∗ (~x)(R|Q◦1 ).
• (~x)(R|P ◦ ) → P 0 is induced by a communication between R and P ◦ . Without
losing any generality, assuming ~x is just x. There are several subcases:· R = (~a)(S|m[y].T ), P ◦ = (~b)(A◦ |(z)m[z].B ◦ ) and(x)(R|P ◦ ) → (x)(~a)(S|T |(~b)(A◦ |B ◦ [y/z]))
myis induced by the communication through m. Then P ◦ → (~b)(A◦ |B ◦ [y/z]).
my
By Theorem 32, P → (~b)(A|B[y/z]). As P ≈o Q, Q1 exists such thatmymy
Q ⇒ Q1 and (~b)(A|B[y/z]) ≈o Q1 . So Q◦ ⇒ Q◦1 . Hence (x)(R|Q◦ ) →∗(x)(~a)(S|T |Q◦1 ) by Lemma 5.
· R = (~a)(y)(S|m[y].T ), P ◦ = (~b)(A◦ |m[z].B ◦ ) and(x)(R|P ◦ ) → (x)(~b)((~a)(S[z/y]|T [z/y])|A◦ |B ◦ )is induced by the communication through m. The argument is similar tothe one in the above case.
· R = (~a)(S|m[y].T ), P ◦ = (~b)(A◦ |m[x].B ◦ ) and (x)(R|P ◦ ) → P 0 is(x)(R|P ◦ ) → (~a)(S[y/x]|T [y/x]|(~b)(A◦ [y/x]|B ◦ [y/x])).
m[x]
m[x]
Then P → (~b)(A|B). It follows that Q1 exists such that Q ⇒ Q1 ≈o(~b)(A|B). So Q1 [y/x] ≈o (~b)(A[y/x]|B[y/x]). By Lemma 5 and Lemma 3,
one has (x)(R|Q◦ ) →∗ (~a)(S[y/x]|T [y/x]|Q1 [y/x]◦ ).
· R = (~a)(S|m[x].T ), P ◦ = (~b)(A◦ |m[y].B ◦ ) and (x)(R|P ◦ ) → P 0 is(x)(R|P ◦ ) → (~b)((~a)(S[y/x]|T [y/x])|A◦ [y/x]|B ◦ [y/x]).
The proof is similar to that in the previous case.
This completes the proof. 2
Theorem 35 For P, Q ∈ P, P ≈o Q if and only if P ◦ ≈ Q◦ .
23

Proof: ⇒: Let R be {((~x)(P ◦ |R), (~x)(Q◦ |R)) | P ≈o Q, P, Q ∈ P, R ∈C and ~x names}. Suppose (~x)(P ◦ |R)R(~x)(Q◦ |R) and (~x)(P ◦ |R) → P 0 . By
Lemma 34, x0 , R0 , P1 and Q1 exist such that P 0 = (x~0 )(P1◦ |R0 ), (~x)(Q◦ |R) →∗δ(x~0 )(Q◦1 |R0 ) and P1 ≈o Q1 . So P 0 R(x~0 )(Q◦1 |R0 ). The case when (~x)(P ◦ |R) → P 0
is similar. Conclude that R is a local bisimulation.
⇐: Let S be {(P σ, Qσ) | P ◦ ≈ Q◦ , P, Q ∈ P, σ substitution}. Suppose P σSQσand P σ → P1 . Then P ◦ σ → P1◦ by Theorem 32. By Lemma 9 and Lemma 31,
Q1 exists such that (Qσ)◦ →∗ Q◦1 and P1◦ ≈ Q◦1 . So Qσ →∗ Q1 by Theorem 32.
Other cases are similar. It follows that S is an open bisimulation. 2

4.2

Pragmatics

In the formulation of χ-calculus, we use the same set of names for both global
names and local names. Theoretically this is justified by the fact that if P → Q
then (x)P → (x)Q and more importantly by the fact that if P ≈ Q then(x)P ≈ (x)Q. The same can be said about π-calculus. But conceptually theidentification is not always helpful. The standard bisimilarity ([41]) for the
π-processes is not closed under input prefixing operation. This is because thevariable names and the free names are regarded as semantically different in
the approach. Sangiorgi’s open bisimilarity is congruent. But still the local
names are treated differently from the free names. In the χ-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. Pragmatically one definitely needs
constant names! This is clear from the mobile process interpretation of object
oriented languages ([65,66]). The usual practice is to identify some names asconstant. This is the same as to say that N consists of two parts: a set Nv ofvariable names and a set Nc of constant names. We can now define χ-processes
to be those in which all variable names are localized. Now 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 bya local or global constant name. A communication between two local constantnames is prohibited. Bisimulation equivalence for χ-processes can be definedin a way similar to the standard bisimulation equivalence for π-processes.
Assume that Nc is ranged over by a, b, c and Nc ∪ Nc by α.
Definition 36 Let R be a binary relation on the set of χ-processes. R is asimulation if P RQ implies(i) if P → P 0 then there exists some Q0 such that Q →∗ Q0 and P 0 RQ0 ;αaαa(ii) if P → P 0 then there exists some Q0 such that Q ⇒ Q0 and P 0 RQ0 ;
α[a]

α[a]

(iii) if P → P 0 then there exists some Q0 such that Q ⇒ Q0 and P 0 RQ0 ;
24

α(a)

α(a)

(iv) 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.
To know if two processes are locally bisimilar, one needs to examine their
behaviour in all local contexts. To know if they are bisimilar, all one has to do
is to see if they can simulate each other’s observable actions; no contexts arenecessary to make the judgement. For this reason, ≈χ is much more tractable
than ≈.
The π-calculus can be reexamined in this new setting. The input prefix operation restricts variable names whereas the localization operation always restricts constant names. The latter is due to the fact that in π-calculus a local
name is never changed. π-processes are now defined to be those processes inwhich all variable names are restricted by input prefixes. The standard bisimilarity can be defined for these π-processes as follows:
Definition 37 Let R be a binary relation on the set of π-processes. R is asimulation if P RQ implies(i) if P → P 0 then there exists some Q0 such that Q →∗ Q0 and P 0 RQ0 ;caca(ii) if P → P 0 then there exists some Q0 such that Q ⇒ Q0 and P 0 RQ0 ;
c[a]

c[a]

c(a)

c(a)

(iii) if P → P 0 then there exists some Q0 such that Q ⇒ Q0 and P 0 RQ0 ;(iv) 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.
Both ≈χ and ≈π can be extended to process expressions with unrestrictedvariable names. For instance, if P and Q are two open χ-processes, then P ≈χ
Q if and only if P σ ≈χ Qσ for all substitution σ that replaces all the variablenames in P |Q by constant names.
The translation given in Section 4.1 works in this new framework. It establishes an operational correspondence in the sense of Theorem 32. In addition
we have the following full abstraction result with respect to the bisimilarity
equivalence.
Theorem 38 For π-processes P and Q, P ≈π Q if and only if P ◦ ≈χ Q◦ .

Proof: The proof is similar to that of Theorem 35. 2

So practically speaking, π is a subcalculus of χ. Anything one can do using
π-calculus can be done with χ-calculus. The converse problem has not been
investigated. We believe that the two languages are equally expressive.
25

5

Lambda Calculus via Chi Calculus

A concurrent computation model has to answer the question of whether it
captures sequential computation successfully. The issue is often addressed byrelating variants of λ-calculus to the model. Milner’s encodings ([34,53,54]) of
the lazy λ-calculus ([1,43]) and the weak call-by-value λ-calculus carry over tothe present calculus. There is no point in repeating the programme. Our focus
in this section will be on the call-by-name λ-calculus ([50]), whose semantics
is defined by the following rules:(λx.M )N → M [N/x]

M → M0M → M0M N → M 0N

λx.M → λx.M 0

Let Λ denote the set of λ-terms. The set of free variables in a term M isdenoted by f v(M ).
The following translation, which is Milner’s encoding of the lazy λ-calculus
with slight modification, serves as an encoding of the call-by-name λ-calculusin χ-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 parallel composition of u[x].u[v] and [[M ]]v allows [[M ]]v to evolve independently, thus modeling reduction under λ-abstraction. Let us see an example:[[λx.(λy.y)N ]]o= (u)(x)(o[x].o[u]|(v)(z)((w)(y)(v[y].v[w]|[[y]]w)|v[z].v[u].z(w)∗[[N ]]w))→ (u)(x)(o[x].o[u]|(v)(y)((w)(v[w]|y[w])|v[u].y(w)∗[[N ]]w))→ (u)(x)(o[x].o[u]|(y)(y[u]|y(w)∗[[N ]]w))→ (u)(x)(o[x].o[u]|(y)([[N ]]u|y(w)∗[[N ]]w))≈ (u)(x)(o[x].o[u]|[[N ]]u)= [[λx.N ]]o.
The computation is of a call-by-need nature. The following definition is takenfrom [34]. Here we have to deal with open λ-terms.
Definition 39 Let the relation / ⊂ Λ×C contain all the pairs (L, P ) such thatfor some k ≥ 0, some M, N1 , . . . , Nk ∈ Λ and distinct variables x1 , . . . , xk :(i) f v(Ni ) ∩ {x1 , . . . , xi } = ∅ for all 1 ≤ i ≤ k;26

(ii) L ≡ M [N1 /x1 ] . . . [Nk /xk ];(iii) P = (~x)([[M ]]u|x1 (w)∗[[N1 ]]w| . . . |xk (w)∗[[Nk ]]w).
Intuitively M /P means that the process P codes up the operational behaviourof λ-term M . In particular M / [[M ]]u. As a matter of fact P1 ≈ P2 wheneverM / P1 and M / P2 . To prove that, we need the following lemma. Its proof
idea can be found in [35].
Lemma 40 Suppose every occurrence of a in P , Q and R is in negative subject position. Then(i) (a)(α[x].P |a(w)∗R) ≈ α[x].(a)(P |a(w)∗R) if a 6∈ {x, α, α};(ii) (a)(P |Q|a(w)∗R) ≈ (a)(P |a(w)∗R)|(a)(Q|a(w)∗R);(iii) (a)(m(x)∗P |a(w)∗Q) ≈ m(x)∗(a)(P |a(w)∗Q).
The following proposition can be proved by induction using Lemma 40.
Proposition 41 If M / P then [[M ]]u ≈ P .
Proof: Suppose P = (~x)([[M0 ]]u|x1 (w)∗[[N1 ]]w| . . . |xk (w)∗[[Nk ]]w) and M ≡M0 [N1 /x1 ] . . . [Nk /xk ]. The following argument is carried out by induction on
the size of M .
• M0 ≡ xi for i ∈ {1, . . . , k}. Then
P = (~x)([[xi ]]u|x1 (w)∗[[N1 ]]w| . . . |xk (w)∗[[Nk ]]w)
≈ (~x)([[Ni ]]u|x1 (w)∗[[N1 ]]w| . . . |xk (w)∗[[Nk ]]w)
≈ [[M ]]uby induction hypothesis.
• M0 ≡ λx.A. Then
P = (~x)((v)(x)(u[x].u[v]|[[A]]v)|x1 (w)∗[[N1 ]]w| . . . |xk (w)∗[[Nk ]]w)
= (v)(x)(u[x].u[v]|(~x)([[A]]v|x1 (w)∗[[N1 ]]w| . . . |xk (w)∗[[Nk ]]w))≈ (v)(x)(u[x].u[v]|[[A[N1 /x1 ] . . . [Nk /xk ]]]v)= [[M ]]uby induction hypothesis.
• M0 ≡ AB. Then
P = (~x)((v)(x)([[A]]v|v[x].v[u].x(w)∗[[B]]w)|x1 (w)∗[[N1 ]]w| . . . |xk (w)∗[[Nk ]]w)
≈ (v)(x)((~x)([[A]]v|x1 (w)∗[[N1 ]]w| . . . |xk (w)∗[[Nk ]]w)|(~x)(v[x].v[u].x(w)∗[[B]]w|x1 (w)∗[[N1 ]]w| . . . |xk (w)∗[[Nk ]]w))≈ (v)(x)([[A[N1 /x1 ] . . . [Nk /xk ]]]v|v[x].v[u].x(w)∗[[B[N1 /x1 ] . . . [Nk /xk ]]]w)
27

= [[M ]]u
by Lemma 40 and induction hypothesis.
We are done. 2
The next theorem relates the operational behaviour of P to that of L wheneverL / P.
Theorem 42 Suppose L / P . Then(i) if L → L0 then P 0 exists such that P →+ P 0 and L0 / P 0 ;(ii) if P → P 0 then either L / P 0 or P 0 →+ P 00 for some P 00 and L → L0 forsome L0 such that L0 / P 00 .

Proof: Suppose L/P . The general form of L is λz1 . . . . .λzn .A1 A2 . . . Am . The
proof of (i) is routine. The proof of (ii) goes by examining two possible cases
for A1 : (a) A1 is an abstraction term; (b) A1 is one of the variables x1 , . . . , xk .
Suppose P is (~x)([[λz1 . . . . .λzn .A01 A02 . . . A0m ]]u|x1 (w)∗[[N1 ]]w| . . . |xk (w)∗[[Nk ]]w)
and P → P 0 .
• A01 is an abstraction term. Then P 0 →+ P 00 for some P 00 and L → L0 forsome L0 such that L0 / P 00 .
• A01 is one of the variables x1 , . . . , xk . Then L / P 0 .
The details of proof is very much the same as the proof of the corresponding
result in [34]. 2
So the operational semantics of the call-by-name λ-calculus can be simulated
within χ.

6

Towards an Integration of Chi and Lambda

Can χ-calculus simulate the operational semantics of the full λ-calculus? The
same question has been asked about the π-calculus. There are two problems
one encounters when trying to answer the question. The first is how to model
reduction under λ-abstraction. The second is how to model reduction M N →M N 0 induced by N → N 0 . The two problems are of different nature. The
former is to do with parallel computation. There is no reason why it shouldpose any problem for concurrent computation. This view is supported by the
result in Section 5. The latter is to do with recursion because the λ-term N
may be duplicated in future reduction. In any structural interpretation, this28

N must be translated into the body of a replicator or guarded replicator. So
if the N induces an infinite reduction, the interpretation of M N would haveno terminating reduction sequence. This would imply that the behaviour ofthe λ-term KIΩ is not faithfully captured by the interpretation. It is our viewthat the second problem is orthogonal to concurrent computation. It is caused
essentially by the operational incompatibility of the two recursion mechanisms.
In this section we take a look at a higher order calculus combining the communication mechanism of the χ-calculus with the recursion mechanism of the
λ-calculus. The purpose of this investigation is to see if the two mechanisms fit
coherently and if local bisimilarity suffices as a tool for studying the algebraic
properties of the resultant language.

6.1

Chi with Call by Name Lambda

Let the set H of higher order χ-processes be defined by the following grammar:
E := 0 | X | α[x].E | E|E 0 | (x)E | α(X)E | α[E],where X is a process variable. E, F, G and H will denote higher order χprocesses. The operational semantics of the higher order χ-calculus is definedby the relevant rules of the first order χ-calculus together with the rules incorporating a call-by-name recursion mechanism:(x)(G|α[x].E|α[y].F ) → (x)(G[y/x]|E[y/x]|F [y/x])
E → E0E → E0E|F → E 0 |F(x)E → (x)E 0
E→Fα(X)E|α[F ] → E[F/X]

α(X)E → α(X)FFree and closed variables are defined in the standard way. Local and global
names are defined as in the first order case with additional postulation thatgn(X) = ln(X) = ∅. We will assume that local names are renamed to avoid
being captured in higher order communications and higher order substitutions.
Usually a bisimulation equivalence for a higher order process calculus is definedfor closed processes. This tractable approach is used by the authors of [60–62,51,52] in studying bisimulation equivalences for CHOCS and higher order29

π-calculus. But the method breaks down in the presence of the reduction rule
E→F
α(X)E → α(X)FA bisimulation equivalence for higher order χ-processes has to be defined on
open processes. For that purpose, let’s say that a binary relation R on H is substitution closed if ERF implies E[E1 /X1 , . . . , Ei /Xi ]RF [E1 /X1 , . . . , Ei /Xi ]for E1 , . . . , Ei ∈ H and process variables X1 , . . . , Xi .
As in the first order case, a labeled transition system is defined. In the following
αx α[x] α(x)rules, δ ranges over {→, → , → |α ∈ N ∪ N , x ∈ N }:αx(y)(R|α[y].P ) → R[x/y]|P [x/y]α[x]P → P0α(x)(x)P → P 0

δδ

P → P0ln(δ) ∩ gn(Q) = ∅δ

P |Q → P 0 |Qα[x]α[x].P → P
δ

P → P0x 6∈ n(δ)δ(x)P → (x)P 0δLet ⇒ denote the relation →∗ →→∗ .
Definition 43 A substitution closed binary relation R on H is a local bisimulation if ERF implies that for any higher order process G and any sequence~x of names it holds thatδδ(i) if (~x)(E|G) ⇒ E 0 then F 0 exists such that (~x)(F |G) ⇒ F 0 and E 0 RF 0 ;δδ(ii) if (~x)(F |G) ⇒ F 0 then E 0 exists such that (~x)(E|G) ⇒ E 0 and E 0 RF 0 .
The local bisimilarity ≈ω is the largest local bisimulation on higher order processes.
It should be remarked that ≈ω is by definition substitution closed.
We can define bisimulation up to ≈ω similar to Definition 10. Lemma 8,
Lemma 9 and Lemma 11 through Lemma 14 all hold for ≈ω .
Theorem 44 ≈ω is a congruence equivalence on higher order processes: if
E ≈ω F and G ∈ H then(i) α[x].E ≈ω α[x].F ;(ii) (x)E ≈ω (x)F ;(iii) E|G ≈ω F |G;(iv) α(X)E ≈ω α(X)F ;(v) α[E] ≈ω α[F ].
30

Proof: (ii) and (iii) follow directly from definition. The proof of (i) is thesame as the one in the first order χ.
(iv) Suppose (~x)(R|α(X)E) → (x~0 )(R0 |E[A/X]) is induced by a higher ordercommunication involving α(X)E. Then (~x)(R|α(X)F ) → (x~0 )(R0 |F [A/X]).
As ≈ω is substitution closed, E[A/X] ≈ω F [A/X]. It follows from (ii) and(iii) that (x~0 )(R0 |E[A/X]) ≈ω (x~0 )(R0 |F [A/X]). Other cases are simple. Hence
α(X)E ≈ω α(X)F .
(v) For the sake of this proof, let’s define Ho [X] to be the set of all higher
order processes E such that each occurrence of X is within α[K] for someα ∈ N ∪ N and some K ∈ H. We first point out an auxiliary fact: Assuming
E ∈ Ho [X] and A ≈ω B,• if (~x)E[A/X] → G then (~x)E[B/X] → H such that G = (x~0 )F [A/X] andH ≈ω (x~0 )F [B/X] for some F in Ho [X];δδ• if (~x)E[A/X] → G then (~x)E[B/X] → H such that G = (x~0 )F [A/X] andH ≈ω (x~0 )F [B/X] for some F in Ho [X].
The proof of the fact goes as follows:δ• If (~x)E[A/X] → G is a first order action, then G = (x~0 )F [A/X] for someδF ∈ Ho [X] and (~x)E[B/X] → (x~0 )F [B/X].
• If (~x)E[A/X] → G is a first order communication, then G = (x~0 )F [A/X]
for some F ∈ Ho [X] and (~x)E[B/X] → (x~0 )F [B/X].
• If (~x)E[A/X] → G is a higher order communication, then G = (~x)F [A/X]
for some F ∈ Ho [X]. Now (~x)E[B/X] → H by carrying out the ‘same’communication. If we replace by A all the occurrences of B in H that do
not appear in a subprocess of the form α[K], we get (~x)F [B/X]. By (i)through (iv), (~x)F [B/X] ≈ω H.

This concludes the proof of the auxiliary fact. Let R be the locally closed andsubstitution closed relation{((~x)E[A/X], (~x)E[B/X]) | A ≈ω B, E ∈ Ho [X], ~x names}.
δ

Now suppose (~x)E[A/X]R(~x)E[B/X] and (~x)E[A/X] → G or (~x)E[A/X] →G. Then G = (x~0 )F [A/X] for some F ∈ Ho [X]. By the above fact, we canδfind some H ∈ H such that (~x)E[B/X] → H or (~x)E[A/X] → H with
(x~0 )F [B/X] ≈ω H. It follows from Lemma 11 that R is a local bisimulation
up to ≈ω . Thus α[E] ≈ω α[F ] since α[X] ∈ Ho [X] and E ≈ω F . 2
In the remaining part of Section 6, we justify our claim that the higher orderχ-calculus is a combination of χ and λ.
31

6.2

Recursion

In [61], the general recursion recX.E is defined as follows:defrecX.E = (a)(a?X.(E|a!X)|a!(a?X.(E|a!X))).

One hasrecX.E → (a)(E[a?X.(E|a!X)/X]|a!(a?X.(E|a!X))).

This reduction looks like an operational unfolding of the recursion recX.E.
Unfortunately the equation is not verified by the higher order bisimilarity
defined in [61]. This is because the higher order bisimilarity has too strong a
distinguishing power.
As a test for local bisimilarity, we examine Thomsen’s recursion in this section.
Suppose that E contains free variable X and a does not occur in E. The
following abbreviations will be used:def

WXa (E) = a[a]|a(X)(a[a].E|a[X]),def

recX.E = (a)(WXa (E)|a[WXa (E)]).
We remark that recX.E defined here is slightly different. The idea is to makesure that WXa (E) is inert before being activated. To prove the main property
concerning recX.E, we first establish a useful result.
Lemma 45 Suppose E and F have free variable X and F 0 is obtained fromF [WXa (E)/X] by replacing some of the occurrences of WXa (E) by WXb (E). Then(a)(F [WXa (E)/X]|a[WXa (E)]) ≈ω (a)(b)(F 0 |a[WXa (E)]|b[WXb (E)]). Here a andb are fresh.

Proof: If (~x)(a)(F [WXa (E)/X]|a[WXa (E)]) → P is induced by a higher ordercommunication between F [WXa (E)/X] and a[WXa (E)], then clearlyP ≈ω (~x)(a)(H[WXa (E)/X]|a[WXa (E)])
for some H with free variable X but without a. By carrying out the ‘same’
higher order communication either between F 0 and a[WXa (E)] or between F 0
and b[WXb (E)], we get32

(~x)(a)(b)(F 0 |a[WXa (E)]|b[WXb (E)])→≈ω (~x)(a)(b)(H 0 |a[WXa (E)]|b[WXb (E)])
where H 0 is obtained from H[WXa (E)/X] by replacing some occurrences ofWXa (E) by WXb (E). Conversely, if(~x)(a)(b)(F 0 |a[WXa (E)]|b[WXb (E)])→≈ω (~x)(a)(b)(H 0 |a[WXa (E)]|b[WXb (E)])then(~x)(a)(F [WXa (E)/X]|a[WXa (E)]) →≈ω (~x)(a)(H[WXa (E)/X]|a[WXa (E)])

such that H 0 is obtained from H[WXa (E)/X] by replacing some occurrences ofWXa (E) by WXb (E). If (~x)(a)(F [WXa (E)/X]|a[WXa (E)]) → P by a communicaδ
tion within F [WXa (E)/X] or (~x)(a)(F [WXa (E)/X]|a[WXa (E)]) → P , thenP = (x~0 )(a)(H[WXa (E)/X]|a[WXa (E)])

for some H with free variable X but without a. And by performing the sameaction, we have(~x)(a)(b)(F 0 |a[WXa (E)]|b[WXb (E)]) → (x~0 )(a)(b)(H 0 |a[WXa (E)]|b[WXb (E)])orδ(~x)(a)(b)(F 0 |a[WXa (E)]|b[WXb (E)]) → (x~0 )(a)(b)(H 0 |a[WXa (E)]|b[WXb (E)])

where H 0 is obtained from H[WXa (E)/X] by replacing some occurrences ofWXa (E) by WXb (E). Similar argument can establish the following fact:δQ exists such that (~x)(a)(b)(F 0 |a[WXa (E)]|b[WXb (E)]) ⇒ Q and P ≈ω R ≈ωδ
Q whenever (~x)(a)(F [WXa (E)/X]|a[WXa (E)]) ⇒ P ,33

where R is the following locally closed and substitution closed relation
















 ((~
x)(a)(F [W a (E)/X]|a[W a (E)]),
X

X










~x ∈ N , a, b 6∈ n(E, F ), 






0

F is obtained from

E, F have free X,






(~x)(a)(b)(F 0 |a[WXa (E)]|b[WXb (E)])) F [WXa (E)] by replacing 














some
occurrences
of












a
b
W (E) by W (E)X

X

It follows that R is a local bisimulation up to ≈ω . 2
Theorem 46 If E contains free variable X then recX.E ≈ω E[recX.E/X].
Proof: We show that the locally closed and substitution closed relationE and F contain free variable X, 










 ((~
x)F [recX.E/X],

a 6∈ n(E, F ), gn(E) ∩ ln(F ) = ∅, 

a
a




(~
x
)(a)(F[W(E)/X]|a[W(E)]))


X
X




~x is a sequence of names
is a local bisimulation up to ≈ω . We sketch the general idea. Suppose(~x)(a)(F [WXa (E)/X]|a[WXa (E)]) → P
is induced by a communication between F [WXa (E)/X] and a[WXa (E)]. Without
loss of generality, let F be X|F1 . Then by Lemma 45
P = (~x)(a)(a[a]|a[a].E[WXa (E)/X]|a[WXa (E)]|F1 [WXa (E)/X])≈ω (~x)(a)(E[WXa (E)/X]|a[WXa (E)]|F1 [WXa (E)/X])≈ω (~x)(a)(b)(E[WXb (E)/X]|b[WXb (E)]|F1 [WXa (E)/X]|a[WXa (E)])= (~x)(a)((b)(E[WXb (E)/X]|b[WXb (E)])|F1 [WXa (E)/X]|a[WXa (E)])= (~x)(a)(H[WXa (E)/X]|a[WXa (E)]),
where H = (b)(E[WXb (E)]|b[WXb (E)])|F1 . Correspondingly, we have(~x)F [recX.E/X] = (~x)(recX.E|F1 [recX.E/X])→∗ (~x)((a)(E[WXa (E)/X]|a[WXa (E)])|F1 [recX.E/X])= (~x)H[recX.E/X]
34

to match the previous reduction. The details of the proof are omitted. Hence
recX.E ≈ω (a)(E[WXa (E)/X]|a[WXa (E)]) ≈ω E[recX.E/X].
This completes the proof. 2
6.3

Conservativity

In this section we show that the higher order χ can be seen as an extension of
the first order χ. A fallout of the result is a justification of the claim that thefirst order recursion is completely unnecessary in the higher order χ-calculus.
Let χ+ be the higher order χ-calculus enriched with the guarded replication.
The language χ+ can be investigated along the same line as the higher orderχ has been. H+ and ≈+ are defined accordingly. It can also be shown that ≈+is a congruence relation. The translation b from χ+ -processes to χω -processes
is defined as follows:
def

c=X
X
d def
b Fb
E|F
= E|
def

d = (x)E
b
(x)E
def

d = α[x].Eb
α[x].Edef

d = α(X)E
b
α(X)E
def

d ] = α[Fb ]
α[F
def

d
b
b
α(x)∗E= (a)((x)α[x].(E|a(X)(X|a[X]))|a[(x)α[x].(E|a(X)(X|a[X]))])
where a is fresh.

The translation b projects the guarded replication out, as it were. A χ+ -process
P and its translation can perform same actions in the sense of the following
proposition:
Proposition 47 Let P ∈ H+ . Then
δ
δ c0
c0 );
(i) if P → P 0 (P → P 0 ) then Pb ⇒ P(Pb →+ Pδδ(ii) if Pb → P 00 (Pb → P 00 ) then P → P 0 (P → P 0 ) for some P 0 such thatc0 .
P 00 ≈+ P
Remark : (i) The proof of this proposition is similar to that of Lemma 45. (ii)δδ
As in Lemma 45, if Pb ⇒ P 00 (Pb →+ P 00 ) then P ⇒ P 0 (P →+ P 0 ) for somec0 .
P 0 such that P 00 ≈+ P
Theorem 48 For P ∈ H+ , P ≈+ Pb .
35

Proof: Using Proposition 47, one shows that {(P, Pb )|P ∈ H+ } is a local
bisimulation up to ≈+ . 2
Theorem 49 The following properties hold:(i) Suppose P and Q are in H. Then P ≈+ Q if and only if P ≈ω Q.
b(ii) Suppose P and Q are in H+ . Then P ≈+ Q if and only if Pb ≈ω Q.
δδ(iii) If Pb → P 00 (Pb → P 00 ) then P → P 0 (P → P 0 ) for some P 0 such thatc0 .
P 00 ≈ω P

Proof: (i) Suppose P, Q are in H. P ≈+ Q clearly implies P ≈ω Q. Supposed|R) = (~db and (~
b where R ∈P ≈ω Q. Then (~x)(Px)(P |R)x)(Q|R)= (~x)(Q|R),+++b and (~b It isH . By Theorem 48, (~x)(P |R) ≈ (~x)(P |R)
x)(Q|R) ≈ (~x)(Q|R).
ω+
now easy to see that ≈ is a local bisimulation up to ≈ .
b By (i) Pb ≈+ Q
b if and(ii) By Theorem 48, P ≈+ Q if and only if Pb ≈+ Q.
ω bb
only if P ≈ Q.
c0 with P 00 ≈ω(iii) This is obtained from Proposition 47 by replacing P 00 ≈+ P
c0 . 2P

We now complete the picture by relating the first order χ to χ+ . In terms ofoperational semantics, the former is clearly a sublanguage of the latter. As forthe algebraic semantics, we have the following result.
Theorem 50 ≈ and ≈+ coincide on first order χ-processes.

Proof: For P, Q ∈ C, the implication from P ≈+ Q to P ≈ Q is trivial. To
establish the other half of the theorem, it suffices to show that ≈ is a local
bisimulation in χ+ -calculus. Suppose P ≈ Q and G ∈ H+ . Let ~x be a sequenceδ
of names. If (~x)(P |G) → (x~0 )(P 0 |G0 ) or (~x)(P |G) → (x~0 )(P 0 |G0 ) by a first ordercommunication, then using the technique employed in the proof of Lemma 21,δone shows that some Q0 exists such that P 0 ≈ Q0 and (~x)(Q|G) ⇒ (x~0 )(Q0 |G0 )δ
or (~x)(Q|G) →∗ (x~0 )(Q0 |G0 ). If (~x)(P |G) → (x~0 )(P 0 |G0 ) is induced by a higher
order communication, then (x~0 )(P 0 |G0 ) must be of the form (~x)(P |G0 ) and
G → G0 . But then (~x)(Q|G) → (~x)(Q|G0 ). 2

From Theorem 49 and Theorem 50, we conclude that P ≈ Q if and only ifb for first order χ-processes P and Q. In other words, the higher orderPb ≈ω Qχ-calculus can be seen as a conservative extension of the first order χ-calculus.
36

6.4

Full Integration

The higher order calculus investigated so far is the combination of the χcalculus and the call-by-name λ-calculus. An integration of χ with the full
λ-calculus is the higher order calculus extended with the following rule
E→F
α[E] → α[F ]Definition 43 now gives rise to an equivalence relation on the set of all processesof the fully integrated calculus. The results in Section 6.2 and Section 6.3 holdfor this language. The (i) through (iv) of Theorem 44 also hold. But so far
we haven’t been able to prove the (v) of Theorem 44 for the fully integrated
calculus. Although we believe that ≈ω is a congruence equivalence in the fully
integrated language, we also think its proof will turn out to be hard.
The operational semantics of the full λ-calculus can be simulated in the fully
integrated calculus. The following is one possible encoding:def[[x]]u = x[u]|Xxdef[[λx.M ]]u = (x)(v)(u[v].u[x]|x(Xx )[[M ]]v )def[[M N ]]u = (x)(v)([[M ]]v |v[u].v[x]|x[(w)(x[w]|[[N ]]w )])where the subscript of Xx indicates the correlation between the lambda variable x and the process variable.
Theorem 51 Suppose M is a λ-term. If M → N then [[M ]]u →+ [[N ]]u .
Proof: Consider the reduction (λx.A)B → A[B/x]. In the encoding it issimulated as follows:[[(λx.A)B]]u= (x)(v)((x)(w)(v[w].v[x]|x(Xx )[[A]]w )|v[u].v[x]|x[(w)(x[w]|[[B]]w )])→ (x)(v)((x)(v[x]|x(Xx )[[A]]u )|v[x]|x[(w)(x[w]|[[B]]w )])→ (x)(x(Xx )[[A]]u |x[(w)(x[w]|[[B]]w )])→ (x)(. . . x[a1 ]|(w)(x[w]|[[B]]w ) . . . x[ai ]|(w)(x[w]|[[B]]w ) . . .)→∗ (x)(. . . [[B]]a1 . . . [[B]]ai . . .)= [[A[B/x]]]u .
This is enough to prove the theorem. 2
37

The above encoding is operationally sound. But it does not preserve algebraic
equality: M =β N does not imply [[M ]]u ≈ω [[N ]]u . For λ-terms M and N ,[[M ]]u ≈ω [[N ]]u implies [[λx.M ]]u ≈ω [[λx.N ]]u . Conversely, suppose [[λx.M ]]u ≈ω[[λx.N ]]u . Then it can be easily seen that some E and F exists such that[[M ]]u →∗ E ≈ω [[N ]]u and [[N ]]u →∗ F ≈ω [[M ]]u . It follows from Lemma 12that [[M ]]u ≈ω [[N ]]u . So we are forced to deal with open λ-terms. Now[[(λx.x)y]]u= (x)(v)([[λx.x]]v |v[u].v[x]|x[(w)(x[w]|y[w]|Yy )])= (x)(v)((x)(w)(v[w].v[x]|x(Xx )[[x]]w )|v[u].v[x]|x[(w)(x[w]|y[w]|Yy )])→∗ (x)(x(Xx )[[x]]u |x[(w)(x[w]|y[w]|Yy )])→ (x)(x[u]|(w)(x[w]|y[w]|Yy ))→ y[u]|Yy= [[y]]u .
Obviously (x)(x[u]|(w)(x[w]|y[w]|y[y])) → (x)(x[u]|x[y]) is not matched byany derivative of y[u]|y[y]. It follows that (x)(x[u]|(w)(x[w]|y[w]|Yy )) is notbisimilar to [[y]]u . But [[(λx.x)y]]u is bisimilar to (x)(x[u]|(w)(x[w]|y[w]|Yy )).
Consequently [[(λx.x)y]]u ≈ω [[y]]u is false.
We need to search for an alternative that verifies β-equality. Here is a modification of the above interpretation:

def[[x]]u = (a)(x[a].a[u].a[0])|Xx
def[[λx.M ]]u = (x)(v)(u[v].u[x]|x(Xx )[[M ]]v )def[[M N ]]u = (x)(v)([[M ]]v |v[u].v[x]|x[(a)(w)(x[a].a[w]|a(Y )[[N ]]w )])where a is fresh and Y does not appear in [[N ]]w .
Theorem 51 holds for this new encoding. In addition the interpretation maps
β-equal terms to bisimilar processes. To justify this claim we need to establish
an auxiliary result.
A process Q is akin to a process P if (i) P → Q (ii) ∀a ∈ N .¬(P ↓a) and (iii)
if P → P 0 then either P 0 = Q or Q →∗ Q0 for some Q0 such that Q0 is akin to
P 0.
Lemma 52 Suppose E is a process with at least process variables X1 , . . . , Xk .
Qi is akin to Pi for each i ∈ {1, . . . , k}. Then E[P1 /X1 , . . . , Pk /Xk ] ≈ωE[Q1 /X1 , . . . , Qk /Xk ].
38

Proof: First observe the following facts:• If E[Q1 /X1 , . . . , Qk /Xk ] → F then E[P1 /X1 , . . . , Pk /Xk ] →∗ F .
• If E[P1 /X1 , . . . , Pk /Xk ] → F [P1 /X1 , . . . , Pk /Xk ] is induced by a communication within E then E[Q1 /X1 , . . . , Qk /Xk ] → F [Q1 /X1 , . . . , Qk /Xk ].
• If E[P1 /X1 , . . . , Pk /Xk ] → E[P10 /X1 , . . . , Pk /Xk ] is induced by P1 → P10
with ¬(P10 = Q1 ), then E[Q1 /X1 , . . . , Qk /Xk ] →∗ E[Q01 /X1 , . . . , Qk /Xk ] forsome Q01 such that Q1 →∗ Q01 and P10 is akin to Q01 .
The rest of the proof is a matter of formality. 2
Theorem 53 Suppose M and N are two λ-terms. Then M =β N implies[[M ]]u ≈ω [[N ]]u .
Proof: By Church-Rosser property, one only has to prove that [[M ]]u ≈ω
[[N ]]u whenever M → N . Suppose M → N is induced by (λx.A)B → A[B/x].
Then
def

[[M ]]u = P0 = . . . (x)(v)((x)(w)(v[w].v[x]|x(Xx )[[A]]w )|v[o].v[x]|x[(a)(w)(x[a].a[w]|a(Y )[[B]]w )]) . . .
def→ P1 = . . . (x)(v)((x)(v[x]|x(Xx )[[A]]o )|v[x]|x[(a)(w)(x[a].a[w]|a(Y )[[B]]w )]) . . .
def→ P2 = . . . (x)(x(Xx )[[A]]o |x[(a)(w)(x[a].a[w]|a(Y )[[B]]w )]) . . .
def→ P3 = . . . (x)(. . . (a)(x[a].a[a1 ].a[0])|(a)(w)(x[a].a[w]|a(Y )[[B]]w ). . . (a)(x[a].a[ai ].a[0])|(a)(w)(x[a].a[w]|a(Y )[[B]]w ) . . .) . . .
def→∗ P4 = . . . [[B]]a1 . . . [[B]]ai . . .
= [[N ]]u .
By constructing appropriate bisimulations, one can prove that Pi ≈ω Pi+1 fori ∈ {0, 1, 2} using Lemma 52. To show P3 ≈ω P4 , notice that P3 is bisimilar
to P30 which is. . . (x)((a)(x[a].a[a1 ].a[0])|(a)(w)(x[a].a[w]|a(Y )[[B]]w )). . . (x)((a)(x[a].a[ai ].a[0])|(a)(w)(x[a].a[w]|a(Y )[[B]]w )) . . . .
This is established in a similar way as the (ii) of Lemma 40. Then prove
P30 ≈ω P4 using Lemma 52. 2
Notice that a congruence result would make the proof of Theorem 53 a little
bit easier.
39

7Category of Chi Processes

Abramsky’s proof-as-process approach is one of the motivations for present
work. In this section we come back to the issue to see how Abramsky’s interpretation looks like using χ-calculus. We do this by casting the interpretation
in a categorical framework.
A χ-process is linear if it is of the form(~x)(a1 [y1 ]| . . . |am [ym ]|P |b1 [z1 ]| . . . |bn [zn ])for some natural numbers m and n satisfying the following conditions:(1) a1 , . . . , am , b1 , . . . , bn are pairwise distinct;(2) {a1 , . . . , am , b1 , . . . , bn } ∩ {y1 , . . . , ym , z1 , . . . , zn } = ∅;(3) {y1 , . . . , ym , z1 , . . . , zn } = {~x};(4) gn(P ) ⊆ {y1 , . . . , ym , z1 , . . . , zn }.
In what follows, we abbreviate, say, the above linear process to (~x)(~a[~y ]|P |~b[~z]).
For two linear χ-processes (~x)(~a[~y ]|P |~b[~z]) and (x~0 )(~c[y~0 ]|P 0 |~d[z~0 ]), define(~x)(~a[~y ]|P |~b[~z])  (x~0 )(~c[y~0 ]|P 0 |~d[z~0 ])if ~y = y~0 , ~z = z~0 and P ≈ P 0 .  is obviously an equivalence relation. Let I(a, b)
denote the linear χ-process (x)(a[x]|b[x]).
Lemma 54 Suppose (~x)(a[y]|P |b[z]) is a linear χ-process. Then for a freshname c, the following holds: (a)(I(c, a)|(~x)(a[y]|P |b[z]))  (~x)(c[y]|P |b[z]) and(b)((~x)(a[y]|P |b[z])|I(b, c))  (~x)(a[y]|P |c[z]).
The category P has natural numbers as objects. Objects of P are denoted by
0, 1, 2 and so on. A morphism from m to n is a -equivalence class of linear
χ-processes of the form(~x)(a1 [y1 ]| . . . |am [ym ]|P |b1 [z1 ]| . . . |bn [zn ]).
We confuse notationally a -equivalence class with one of its members. The
composition of morphisms (~x)(~a[~y ]|P |~b[~z]) : l → m and (x~0 )(~c[y~0 ]|P 0 |~d[z~0 ]) :m → n is(~e)((~x)(~a[~y ]|P |~e[~z])|(x~0 )(~e[y~0 ]|P 0 |~d[z~0 ])) : l → n
40for fresh ~e. It is clearly well defined. Associativity of composition obviously
holds. By Lemma 54 the identity morphism on m can be defined asI(a1 , b1 )| . . . |I(am , bm )where a1 , . . . , am , b1 , . . . , bm are pairwise distinct. In particular the identity
morphism on 0 is the inactive process 0.
Given morphisms φ = (~x)(~a[~y ]|P |~b[~z]) : m → n and ψ = (x~0 )(~c[y~0 ]|P 0 |~d[z~0 ]) :m0 → n0 such that ~a, ~b, ~c, d~ are all different, define φ ⊗ ψ to be φ|ψ : m+m0 →n+n0 . This gives rise to a symmetric monoidal category, the unit of the tensor
product being 0.
For a χ-processes P , P ⊥ denotes the process obtained by replacing every positive (negative) occurrence of a name in P by a negative (positive) occurrenceof the same name. For instance, ((x)(m[a]|b[x]|x[m]))⊥ is (x)(m[a]|b[x]|x[m]).
Clearly (P ⊥ )⊥ = P . ( )⊥ extends to a functor from P to Pop if we defineψ⊥ψm⊥ to be m for m ∈ ω. As (m → n)⊥ is n → m, ( )⊥ is an involution. Letm℘n be (m⊥ ⊗ n⊥ )⊥ = m ⊗ n and let m −◦n be m⊥ ℘n = m ⊗ n. With these
constructions, P becomes a ∗-autonomous category ([9]). A bijective correspondence between P(l ⊗ m, n) and P(l, m −◦n) sends (~x)(~a[~l]|~b[m]|P~|~c[~n]) to~~ ~c[~n]). As a matter of fact P is a compact closed category as(~x)(~a[~l]|P |b[m]|the functor ( )⊥ is self-dual ([10,6]).
It is well-known that a ∗-autonomous category is a model of the multiplicative
linear logic ([58,10]).

8

Final Remark

Proof theory turns out to be helpful in constructing models for concurrent
computation. The χ-calculus designed with proofs in mind subsumes the πcalculus. It is worth remarking that the extension is not achieved by adding
extra operators but by unifying two combinators in π-calculus. If we can simplify a formalism without sacrificing its expressive power, we go ahead withthe simplification.
As mentioned previously, there are two kinds of restricted name in π-calculus.
For a basic model of concurrent computation, two is probably too many. The
χ-calculus is what one gets when one tries to unify the two classes of restrictednames. The payoff is that one has to adjust his familiar perception of communication as value-passing operation. In χ, the distinction between global
names and local names are made minimal. It is not too exaggerating to say
41

that in χ there is no difference between these two kinds of names. If one adopts
a closed-world viewpoint, then global names are local names seen from within
local declarations.
Usually a process calculus consists of two parts, a communication mechanism
defining the operational behaviour of the system and a recursion mechanism
giving the language the Turing computability. The χ-calculus differs from the
π-calculus mainly in the effect of communication. π adopts a value-passing
mechanism inherited from a functional framework. A communication in πcalculus can be seen as a concurrent functional application. The fact thatthe language as defined in [34] is capable of encapsulating the lazy λ-calculus([34,53,54]), which is a model for functional programming, but not the full λcalculus can be seen as an indication that it is a model of concurrent functional
computation. The χ-calculus deviates from the π-calculus by removing somefunctionality away. To communicate is to share information. In (x)(R|m[x].P )and (y)(S|m[y].Q), the local x and y are two secrets known only to the respective communities they belong to. The two communities share the secrets
as a result of the following communication:(x)(R|m[x].P )|(y)(S|m[y].Q) → (z)(R[z/x]|P [z/x]|S[z/y]|Q[z/y]) (1)In a basic model of concurrent computation, there ought not to be operations
like ‘putting two pieces of information together’. Our solution has been to use
a fresh name to denote the resulting information. In the following communication(x)(R|m[x].P )|(S|m[y].Q) → R[y/x]|P [y/x]|S|Q(2)

the process (x)(R|m[x].P ) has to reveal the secret to public. Once a secret is
known to everybody, it is no more a secret. This is the intuition behind theabove reduction. A stronger justification of (2) is that it is consistent with(1). (1) is a global view of an exchange while (2) is a local description of thecommunication.
A pleasant feature of χ-calculus is its symmetry. Other symmetric systems
have been proposed in the literature. Sangiorgi’s πI is one example ([55,13]).
It has been observed that πI has almost all the expressive power of π. From the
π-calculus point of view, πI is obtained from π by making the output prefixes
the same as the input prefixes, whereas χ is what one gets by forcing the input
prefixes to be the same as the output prefixes. The syntax of πI introduces
a distinction between local names and variable names, although the latter
appear pseudo. In χ, however, the distinction completely vanishes. Anothervariant of π-calculus is the so-called asynchronous π-calculus ([25,14,26,7]).
Like πI, the asynchronous π-calculus is a sublanguage of π. The former can
42simulate the latter at least from an operational point of view. It is remarkablethat the proposed sublanguages of π do not sacrifice the expressive power of π
in any essential way. This seems to suggest that the idea of name manipulation
is a robust one. In this paper we have shown that χ has at least the expressive
power of π. Whether it is strictly more powerful is left for further study. If π
and χ turn out to be equally expressive, then there ought to be a translationfrom χ to πI or a symmetric version of the asynchronous π-calculus that preserves expressive power. This is an important question that certainly deserves
investigation. To some degree, one hopes that the answer is positive as thatwould add force to our belief that calculi of mobile processes are the right tool
to describe concurrent computation.
As we said before, the basic reduction rule of χ-calculus(x)(R|α[x].P |α[y].Q) → (x)(R[y/x]|P [y/x]|Q[y/x])
can be split into two:(x)(R|α[x].P |α[y].Q) → R[y/x]|P [y/x]|Q[y/x], where x 6= y

(3)(x)(R|α[x].P |α[x].Q) → (x)(R|P |Q)(4)

Rule (3) is the essence of communication in χ-calculus. On the other hand,(4) is open for modification. Two possibilities arise. One is to remove rule (4)completely. The other is to replace it with the following
α[x].P |α[x].Q → P |Q

(5)

Both modifications result in calculi that have simpler labeled transition systems than the χ of this paper. Conceptually we prefer (4) to (5) as the former
keeps the uniformity of communication.
The Church-Turing thesis is supported by the fact that all proposed models
for computable operations are equally expressive in the sense that they cansimulate each other’s operational behaviour. In the study of concurrent computation models, expressive power ought to be an important issue. But unlike
the situation of sequential computation, there does not seem to be any consensus on criteria for one concurrent computation model being more expressive
than another. How do we mean, for example, that one calculus is a subcalculus of another? Do we mean that the syntax of one is part of the syntax ofthe other with operational semantics inherited? Or do we mean that there is atranslation from one to the other that preserves operational semantics? Should
the translation be fully abstract with respect to some observable equivalence?
If full abstraction is required, then which observational equivalence are we43talking about? Can it be any observational equivalence that happens to enjoya full abstraction property? The answers may well depend on what one doeswith these models.
There could be some questions concerning some of the design decisions ofthe χ-calculus. One is that the guarded replication introduces extra restrictednames. This is not in line with our starting point that in a basic computation
model there should be only one kind of restricted names. The second is thatthe second order communication is not symmetric, which seems to destroy the
integrity of the first order communication. The first question can be easily
avoided by using unguarded replication. Guarded replication m(x)∗P , which
can be seen as an abbreviation of !(x)(m[x].P ), is better behaved and is easier
to implement. The higher order communication mechanism used in this paper
could be made symmetric, but there is nothing to be gained from that. In
this paper we see higher order feature as providing a recursion mechanism
rather than as an extension of communication mechanism. The essence of aconcurrent computation model is defined by its communication mechanism,
upon which one can introduce whatever recursion mechanism to fulfill one’s
purpose.
The χ-calculus has its motivation from reaction graphs ([18]), which is related
to Lafont’s interaction nets ([28,29]), Parrow’s interaction diagrams ([45]) and
Milner’s π-nets ([37]). It would be interesting to investigate χ-calculus in thegeneral framework of action calculus ([39,36,40,38]).
Does the translation [[ ]] defined in Section 5 preserve the algebraic semantics
in the sense that M =β N implies [[M ]]u ≈ [[N ]]u? The answer is negative.
Now[[(λx.y)x]]u = (v)(x)((o)(x)(v[x].v[o]|y[o])|v[x].v[u].x(w)∗x[w])→ (v)(x)((o)(v[o]|y[o])|v[u].x(w)∗x[w])→ (x)(y[u]|x(w)∗x[w])≈ [[y]]u.
It is easily seen that [[(λx.y)x]]u ≈ (v)(x)((o)(v[o]|y[o])|v[u].x(w)∗x[w]). But(v)(x)((o)(v[o]|y[o])|v[u].x(w)∗x[w])|y[a] → (v)(x)(v[a]|v[u].x(w)∗x[w])is not matched by anything from (x)(y[u]|x(w)∗x[w])|y[a]. Hence [[(λx.y)x]]u 6≈[[y]]u. Moreover [[M ]]u ≈ [[N ]]u if and only if [[λy.M ]]u ≈ [[λy.N ]]u. It follows
that [[λy.(λx.y)x]]u 6≈ [[λy.y]]u.
The category defined in Section 7 is an example of compact closed category. Weak product, and therefore coproduct, exists for objects m and n with44

m+n 6= 0. Does the category have enough structure to model the modalities
of linear logic? Or does it have the essential structures to be an interaction
category ([2,5,21,6])? These are interesting questions.
The syntax of χ-calculus suggests another variant of π-calculus. It is a symmetric presentation of π-calculus, in which communications are exchange of
information. Its abstract syntax is the same as that of χ-calculus. Let’s denote
this language by Π. One nice thing about the symmetric presentation is that it
renders unnecessary abstract names as x in m(x).P in the asymmetric version.
In other words, the names in symmetric π-calculus is more homogeneous in thesense that if we replace the guarded recursion m(x)∗R by replicator !P thenthere is only one kind of restricted names. The communication mechanism of
Π can be defined by a single rulea[x].P |a[y].Q → P [y/x]|Q[x/y]together with the structural rules
P → P0P → P0P |Q → P 0 |Q(x)P → (x)P 0

Here are some examples of reduction in Π-calculus:
R|m[x].P |m[y].Q → R|P [y/x]|Q[x/y],(x)(R|m[x].P )|m[y].Q → (x)(R|P [y/x]|Q[x/y]),(x)(R|m[x].P )|(y)(S|m[y].Q) → (x)(y)(R|P [y/x]|S|Q[x/y]).
There is a structural translation from π to Π defined as follows:def(0) = 0,
def(m(x).P ) = (x)m[x].P  ,def(mx.P ) = (s)(m[x].s[s]|s[s].P  ), where s is fresh,def(P |Q) = P  |Q ,def((x)P ) = (x)P  ,def(α(x)∗P ) = α(x)∗P  .
In [19] it is shown that the translation preserves both operational and algebraic
semantics.
After the publication of [17], Parrow and Victor proposed a language theycall Update Calculus ([47]), which is just an asymmetric version of χ-calculus.
45

More recently they have related Fusion Calculus, which is a polyadic versionof χ-calculus, to concurrent constraint programming ([48,64]).
Axiomatizations of π-processes have been intensively studied. A couple ofcomplete systems have been obtained. These include those for early and latecongruence relations ([41,46,24,30]), for open bisimulation congruence ([56]),
for finite control π-processes ([31,32]), and for asynchronous π-calculus ([7]). In
χ-calculus, early and late bisimilarities coincide. In π-calculus, axiomatizations
are complicated by the fact that there are two kinds of restricted names.
In χ-calculus this complication is absent. Parrow and Victor have studiedcomplete systems for weak hyperequivalence on Fusion processes ([49]). Fu
has in [20] worked out complete axiom systems for both local congruence andbarbed congruence. We believe that Fu’s system for barbed congruence on
χ-processes can be generalized to a complete system for barbed congruenceon finite Fusion processes. More recently Fu has worked out complete systems
for all the eighteen L-congruences on asymmetric χ-calculus and discovered a
mistake made in both [49] and [20].
We have considered in this paper essentially two distinct bisimulation congruences on χ-processes. Are there any other reasonable bisimulation congruenceson χ-processes? In [20] a possible classification of bisimilarities on χ-processes
is given. A uniform definition of dozens of bisimilarities, called L-bisimilarities,
is introduced. It is pointed out that these L-bisimilarities collapse into a number of distinct equivalence relations. Ordered by set inclusion, they form alattice called bisimulation lattice. The local bisimilarity and the barbed bisimilarity studied in this paper are respectively the bottom and the top of thelattice. In [20] bisimulation lattices for asymmetric χ-processes, asynchronous
χ-processes, asymmetric and asynchronous χ-processes are also discovered.

Acknowledgements

I have had the pleasure to discuss the material covered in this paper with G.
Boudol, W. Chen, Y. Chen, L. Du and E. Shen. F. Song has proof-read thepaper. B. Victor pointed out to me that the / of Definition 39 ought to be a
relation from the set of open λ-terms to the set of χ-processes. Two anonymousreferees’ comments have helped improve the quality of the paper. The editorsof the special issue have put a lot of care into my final presentation of thematerial covered in the paper. My thanks to all of them.
The work reported here has been supported by the National Nature Science
Foundation of China, grant number 69873032, and by the National 863 HighTech Project, grant number 863-306-ZT06-02-2.
46

References[1] S. Abramsky, The Lazy Lambda Calculus, in: D. Turner, eds., Declarative
Programming (Addison-Wesley, 1988) 65–116.
[2] S. Abramsky, Interaction Categories, in: G. Burn, S. Gay and M. Ryan, eds.,
Proceedings of the First Imperial College Department of Computing Workshop
on Theory and Formal Methods (Springer-Verlag, 1993) 57–70.
[3] S. Abramsky, Computational Interpretations of Linear Logic, TheoreticalComputer Science, 111 (1993) 3–57.
[4] S. Abramsky, Proofs as Processes, Theoretical Computer Science, 135 (1994)
5–9.
[5] S. Abramsky, Interaction Categories and Communicating Sequential Processes,
in: A. Roscoe, eds., A Classical Mind: Essays in Honour of C.A.R. Hoare(Prentice Hall, 1994) 1–15.
[6] S. Abramsky, S. Gay and R. Nagarajan, Interaction Categories and theFoundations of Typed Concurrent Programming, Proceedings of the 1994
Marktoberdorf Summer School on Deductive Program Design, NATO ASI, Series
F (Springer-Verlag, 1996).
[7] R. Amadio, I. Castellani and D. Sangiorgi, On Bisimulations for the
Asynchronous π-Calculus, CONCUR ’96, Lecture Notes in Computer Science
1119 (Springer-Verlag, 1996) 146–162.
[8] H. Barendregt, The Lambda Calculus: Its Syntax and Semantics, Studies in
Logic and Foundations of Mathematics (North-Holland, 1984).
[9] M. Barr, ∗-Autonomous Categories, Lecture Notes in Mathematics 752(Springer-Verlag, 1979).
[10] M. Barr, ∗-Autonomous Categories and Linear Logic, Mathematical Structuresin Computer Science, 1 (1991) 159–178.
[11] G. Berry and G. Boudol, The Chemical Abstract Machine, TheoreticalComputer Science, 96 (1992) 217–248.
[12] M. Boreale and R. DeNicola, Testing Equivalence for Mobile Processes,
CONCUR ’92, Lecture Notes in Computer Science 630 (Springer-Verlag, 1992)
2–16.
[13] M. Boreale, On the Expressiveness of Internal Mobility in Name-Passing Calculi,
CONCUR ’96, Lecture Notes in Computer Science 1119 (Springer-Verlag, 1996)
161–178.
[14] G. Boudol, Asynchrony and π-Calculus, Research Report 1702 (INRIA, SophiaAntipolis, 1991).
[15] G. Bellin and P. Scott, On the π-Calculus and Linear Logic, TheoreticalComputer Science, 135 (1994) 11–65.

47

[16] Y. Fu, The χ-Calculus, Proceedings of the International Conference on Advances
in Parallel and Distributed Computing (March 19th-21th, Shanghai, IEEE
Computer Society Press, 1997) 74–81.
[17] Y. Fu, A Proof Theoretical Approach to Communications, ICALP ’97, Lecture
Notes in Computer Science 1256 (July 7th-11th, Bologna, Italy, Springer-Verlag,
1997) 325–335.
[18] Y. Fu, Reaction Graphs, Journal of Computer Science and Technology, 13(1998) 510–530.
[19] Y. Fu, Symmetric π-Calculus, Journal of Computer Science and Technology, 13(1998) 202–208.
[20] Y. Fu, Bisimulation Lattice of Chi Processes, ASIAN ’98, Lecture Notes in
Computer Science 1538 (December 8-10, Manila, The Philippines, SpringerVerlag, 1998) 245–262.
[21] S. Gay, Linear Types for Communicating Processes, PhD thesis (Departmentof Computing, Imperial College, 1995).
[22] J. Girard, Linear Logic, Theoretical Computer Science, 50 (1987) 1–102.
[23] J. Girard, Towards a Geometry of Interaction, in: J.W. Gray and A. Scedrov,
eds., Categories in Computer Science and Logic, Contemporary Mathematics,
92 (AMS, 1989) 69–108.
[24] M. Hennessy and H. Lin, Symbolic Bisimulations, Theoretical Computer
Science, 138 (1995) 353–389.
[25] K. Honda and M. Tokoro, An Object Calculus for Asynchronous Communication, ECOOP ’91, Lecture Notes in Computer Science 512 (Springer-Verlag,
1991) 133–147.
[26] K. Honda and M. Tokoro, On Asynchronous Communication Semantics,
Object-Based Concurrent Computing, Lecture Notes in Computer Science 612(Springer-Verlag, 1991) 21–51.
[27] Honda and Yoshida, On Reduction Based Process Semantics, TheoreticalComputer Science, 152 (1995) 437–486.
[28] Y. Lafont, Interaction Nets, POPL ’90 (ACM, 1990) 95–108.
[29] Y. Lafont, Interaction Combinators, Information and Computation, 137 (1997)
69–101.
[30] H. Lin, Complete Inference Systems for Weak Bisimulation Equivalences in theπ-Calculus, Proceedings of Sixth International Joint Conference on the Theory
and Practice of Software Development, Lecture Notes in Computer Science 915(Springer-Verlag, 1995) 187–201.
[31] H. Lin, Unique Fixpoint Induction for Mobile Processes, CONCUR ’95, Lecture
Notes in Computer Science 962 (Springer-Verlag, 1995) 88–102.

48

[32] H. Lin, Complete Proof Systems for Observation Congruences in Finite-Control
π-Calculus, ICALP ’98, Lecture Notes in Computer Science 1443 (SpringerVerlag, 1998) 443–454.
[33] R. Milner, Communication and Concurrency (Prentice Hall, 1989).
[34] R. Milner, Functions as Processes, Mathematical Structures in Computer
Science, 2 (1992) 119–146.
[35] R. Milner, The Polyadic π-Calculus: a Tutorial, Proceedings of the 1991
Marktoberdorf Summer School on Logic and Algebra of Specification, NATO
ASI, Series F (Springer-Verlag, 1993).
[36] R. Milner, Action Calculi, or Syntactic Action Structure, MFCS ’93, Lecture
Notes in Computer Science 711 (Springer-Verlag, 1993) 105–121.
[37] R. Milner, π-Nets: a Graphical Form of π-Calculus, ESOP ’94, Lecture Notes
in Computer Science 788 (Springer-Verlag, 1994) 26–42.
[38] R. Milner, Calculi for Interaction, Acta Informatica, 33 (1995) 707–737.
[39] R. Milner, Action Structures and the π-Calculus, Proceedings of the 1993
Marktoberdorf Summer School on Proof and Computation, NATO ASI, Series
F (Springer-Verlag, 1995).
[40] A. Mifsud, R. Milner and J. Power, Control Structure, LICS ’95 (IEEE
Computer Society Press, 1995) 188–198.
[41] R. Milner, J. Parrow and D. Walker, A Calculus of Mobile Processes,
Information and Computation, 100 (1992) 1–40 (Part I), 41–77 (Part II).
[42] R. Milner and D. Sangiorgi, Barbed Bisimulation, ICALP ’92, Lecture Notes in
Computer Science 623 (Springer-Verlag, 1992) 685–695.
[43] L. Ong, The Lazy Lambda Calculus: An Investigation into the Foundationsof Functional Programming, PhD thesis (Imperial College of Science andTechnology, University of London, 1988).
[44] D. Park, Concurrency and Automata on Infinite Sequences, Lecture Notes in
Computer Science 154 (Springer-Verlag, 1981) 561–572.
[45] J. Parrow, Interaction Diagrams, A Decade of Concurrency, Lecture Notes in
Computer Science 803 (Springer-Verlag, 1993) 477–508.
[46] J. Parrow and D. Sangiorgi, Algebraic Theories for Name-Passing Calculi,
Information and Computation, 120 (1995) 174–197.
[47] J. Parrow and B. Victor, The Update Calculus, AMAST ’97, Lecture Notes
in Computer Science 1119 (Sydney, December 13-17, Springer-Verlag, 1997)
389–405.
[48] J. Parrow and B. Victor, The Fusion Calculus: Expressiveness and Symmetryin Mobile Processes, LICS ’98 (IEEE Computer Society, 1998) 176–185.

49

[49] J. Parrow and B. Victor, The Tau-Laws of Fusion, CONCUR ’98, Lecture Notes
in Computer Science 1466, (Springer-Verlag, 1998) 99–114.
[50] G. Plotkin, Call-by Name, Call-by-Value and the λ-Calculus, TheoreticalComputer Science, 1 (1975) 125–159.
[51] D. Sangiorgi, Expressing Mobility in Process Algebras: First-Order and HigherOrder Paradigms, PhD thesis (Department of Computer Science, University of
Edinburgh, 1993).
[52] D. Sangiorgi, From π-Calculus to Higher Order π-Calculus—and Back,TAPSOFT ’93, Lecture Notes in Computer Science 668 (Springer-Verlag, 1993)
151–166.
[53] D. Sangiorgi, The Lazy Lambda Calculus in a Concurrency Scenario,
Information and Computation, 111 (1994) 120–153.
[54] D. Sangiorgi, Lazy Functions and Mobile Processes, Technical Report RR-2515(INRIA, 1995).
[55] D. Sangiorgi, π-Calculus, Internal Mobility and Agent-Passing Calculi,
Theoretical Computer Science, 167 (1996) 235–274.
[56] D. Sangiorgi, A Theory of Bisimulation for π-Calculus, Acta Informatica, 3(1996) 69–97.
[57] D. Sangiorgi and R. Milner, Techniques of “Weak Bisimulation Up To”,
CONCUR ’92, Lecture Notes in Computer Science 630 (Springer-Verlag, 1992).
[58] R. Seely, Linear Logic, ∗-Autonomous Categories and Cofree Coalgebras,
in: J.W. Gray and A. Scedrov, Categories in Computer Science and Logic,
Contemporary Mathematics, 92 (AMS, 1989) 371–382.
[59] G. Takeuti, Proof Theory, Studies in Logic 81 (North-Holland, 1975).
[60] B. Thomsen, A Calculus of Higher Order Communicating Systems, POPL ’89(ACM, 1989) 143–154.
[61] B. Thomsen, Plain CHOCS—A Second Generation Calculus for Higher Order
Processes, Acta Informatica, 30 (1993) 1–59.
[62] B. Thomsen, A Theory of Higher Order Communicating Systems, Information
and Computation, 116 (1995) 38–57.
[63] A. Troelstra, Lectures on Linear Logic, CSLI Lecture Notes (1992).
[64] B. Victor and J. Parrow, Concurrent Constraints in the Fusion Calculus,
ICALP ’98, Lecture Notes in Computer Science 1443 (Springer-Verlag, 1998)
455–469.
[65] D. Walker, π-Calculus Semantics for Object-Oriented Programming Languages,
TACS ’91, Lecture Notes in Computer Science 526 (Springer-Verlag, 1991) 532–
547.
[66] D. Walker, Objects in the π-Calculus, Information and Computation, 116(1995) 253–271.

50