The χ-Calculus∗
Yuxi Fu†‡§

Abstract

are restricted. We might as well change the syntax ofa(x).P to (x)ax.P , where x is free in ax.P . With thischange, we would have

The paper proposes a new process algebra, called χcalculus. The language differs from π-calculus in several aspects. First it takes a more uniform view on
input and output. Second, the closed names of the language is homogeneous in the sense that there is only
one kind of bound names. Thirdly, the effects of communications in χ-calculus are delimited by localization
operators, not by sequentiality combinator. Finally, thelanguage cherishes more freedom of parallelism than πcalculus. The algebraic properties of χ-processes arestudied in terms of local bisimulation. It is shownthat local bisimilarity is a congruence equivalence on
χ-processes.

τ(x)(ax|(y)xy)|(v)(av|vw) −→ (u)((y)uy|uw).
This is an example of communication of local names.
How do we extend this communication mechanism to communications with free outputs?
It might well be that there are more than one answers
to the question.
What then is information? The simplest answer isthat information is the content of communication. It isonly through communication that a piece of information asserts itself. In value-passing CCS, the contentsof communications are extralogical entities. Althougha translation into the basic CCS is possible, such anenterprise relies on heavy mathematical assumptions.
The greatest achievement of the π-calculus is that itpresents itself, in a concise way, as a closed model for
concurrent computations. But is there any room for
improvement on π-calculus as far as the closedness isconcerned? This brings us to a somewhat unpleasantfeature of the π-calculus. In π there are two kinds ofclosed names. There are local names like y in (y)P and
there are abstract names like x in m(x).P . For a basicmodel of concurrent computations, two kinds of closed
names are probably too more.

Key Words: Bisimulation, π-Calculus

1. Questions on π-calculus
Communication is exchange of information. Twoparties involved in a communication are in reciprocal
positions. Symmetry of communications is a conspicuous feature of the basic CCS. When moving to valuepassing calculi, symmetry is lost. The π-calculus ([4])
is but one such a language. Consider the process(a)(a(x).x(y)|(v)av.vw).
Operationally, (a)(a(x).x(y)|(v)av.vw) is no differenceto (a)((x)ax.x(y)|a(v).vw). Moreover, both processes
are equivalent to (a)(a(x).x(y)|(v)(av|vw)) and respectively (a)((x)(ax|x(y))|a(v).vw). What do all theseequivalences suggest? Well, they seem to indicate that
there is little need to draw a clear-cut line between input actions and output actions when the output names

Can we eliminate the abstract names from πcalculus in favour of the local names?
A conceivable solution is to regard the abstract names
as special local names.
Often, information is used to control computations
whereas communications, or the lack of them, make thecontrol happen. When designing a process calculus,
there are two complementary issues. One is to introduce a parallel mechanism so that events can happen
in parallel to full extent. The other is to have a control
mechanism to curb unwanted parallelism and to placeorder on life. The π-calculus, as well as most other process calculi, has a parallel mechanism that is beyond∗ Proceedings of the International Conference on Advances in
Parallel and Distributed Computing, March 19-21, 1997, Shanghai, China, IEEE Computer Society Press, 74–81.
† Supported by the National Nature Science Foundation ofChina, grant number 69503006.
‡ Department of Computer Science, Shanghai Jiao Tong University, 1954 Hua Shan Road, Shanghai 200030, China.
§ E-mail: fu-yx@cs.sjtu.edu.cn.

1question. The parallel combinator ‘|’ intends to permit full-scale parallelism and to allow controls to havetheir ways. But are there any situations in π-calculus
in which the orders of computations are always preordained? Suppose two processes P and Q share an
abstract name x. The situation can be described asin m(x).(P |Q). What if we want P to evolve independently from the instantiation of x through m? In π
there is no way to do that. For a language that deals
with concurrency, the requirement of this example is
not over-demanding. A good control mechanism exerts controls, not unintended restrictions.

based upon that of sequentiality. Without sequential
computations, there is no way to talk about concurrent
computations. This is the background against which
the sequentiality operator is introduced. An alternative view is that sequential computations are special
concurrent computations. For those of us who take thissecond attitude, we need a process calculus to back up
our viewpoint.
In this paper, we propose a new process algebra, χcalculus, that gives our answers to the first four questions. By omitting the sequentiality operator of thecalculus, question 5 can also be investigated.

How do we eliminate the restriction imposedby the control mechanism of the π-calculus?

2. Communication via information exchange

Searching for an answer to the question is one of the
motivations for the study carried out in this paper.
The restriction mentioned above is to do with thesequentiality operator1 of the π-calculus. Let’s take aclose look at the combinator. The process mn.P emitsn through medium m and then proceeds as P . The
sequentiality appeared here is nice and simple. On theother hand, the behaviour of m(x).P is different. After
receiving a name n through m, the process continues to
evolve as P [n/x]. From a purely set theoretical point ofview, m(x).P is nothing but a function. The functionality of m(x).P has serious implication: the effect ofany communication m(x).P to participate is restricted
to the body of the function, that is to P . In otherwords, the sequentiality operator also acts as an effectdelimiter. But if the operator is to prescribe orders ofactions, then why should it have anything to do withthe scope of the effect of a communication?

This section introduces a new process calculus. Syntactically, the language differs from the π-calculus by
unifying input and output prefixes. Semantically, it
represents a more drastic departure. The value-passing
communication mechanism of the π-calculus is replacedby an information exchange communication mechanism. The language will be called χ-calculus, whereχ stands for exchange of information.
Let N be a set of names ranged over by lower caseletters, Pχ the set of χ-processes defined as follows:
P := 0 | mi [x].P | P |P | (x)P | [x=y]P |!P,
where i ∈ {−1, 1}. Here m−1 and m1 are the twoends of channel m. As usual 0 is the inactive process.
A trailing inactive process will be omitted. mi [x].P
is a process that must first perform a communication
through channel m and then enacts P [y/x], where yis the name received in the communication. P |Q is aprocess of parasition form. Here P and Q can evolve
independently and may communicate during the courseof their evolution. (x)P is a process where x is local to
P , meaning that (x)P is not allowed to communicate
with another process through channel x. The conditional process [x=y]P behaves the same as P if x=y,or it is the same as the inactive process 0. The replication process !P provides potentially infinite copies of
P . The set of local names appeared in P is denoted byln(P ). The set of global names, or nonlocal names, in
P is designated by gn(P ). The set n(P ) is the unionof ln(P ) and gn(P ). We adopt the α-convention saying that a local name in a process can be replaced by afresh name without changing the syntax of the process.
The following rules define the operational semanticsof χ-calculus. Notice that we have left out all the sym-

What if we, and how do we, free the sequentiality combinator from the duty of delimiting
the effects of communications?
It would be a bad idea to introduce a completely new
combinator to fulfill the role of effect delimiter. We
already have in π-calculus a combinator that defines
the scope of a name. It appears more sensible to let
the localization operator play the role because that iswhat it is meant to be—a scope delimiter.
There is however a more dramatic question about
the sequentiality combinator:
Is sequentiality operator necessary for a concurrent computation model?
The answer depends to a large extent on how we see therelationship between sequential and concurrent computations. One view is that the notion of concurrency is
1 We call the dot in α.P a sequentiality combinator.

2

metric rules.

The operational rules are simpler than they appear to be. To help understand the communication
rules, we now give some examples. In the process(x)(R|(m−1 [n].P |m1 [x].Q)), a communication via m ispossible. The effect of the communication is to replace
the local name x by the global name n throughout theterm over which the localization operator (x) applies.
The global name n in P however remains unchanged.
In other words, global information overwrites. The reduction

Sequention
mi [x].PS0

mi hy/xi−→ P [y/x]Parasition
mi hy/xi

Q −→ Q0τ

Q −→ Q0PτP |Q −→ P |Q0 0
mi hxiτ

hy/xi

Q −→ Q0
mi hxiP1

mi hy/xi

P |Q −→ P [y/x]|Q0(x)(R|(m−1 [n].P |m1 [x].Q)) −→ (R|(P |Q))[n/x]Q −→ Q0

P |Q −→ P |Q0

P2

hy/xi

P |Q −→ P [y/x]|Q0

P3

is not derivable by a single rule. The only communication rule applicable here is C1 . But C1 does only part of
the job. The result is a labeled reduction representing
an incomplete action:

CommunicationPP

m−i hxi

mi hx/xi−→ P 0 Q −→ Q0
C0τ
P |Q −→ P 0 |Q0mi hy/yi−→ P 0Qm−i hy/xi−→

Q0

P |Q −→ P 0 [y/x]|Q0
P −→ P 0

To continue, we use the rule P3 to get
C1

hy/xi

mi hxihn/xi

m−1 [n].P |m1 [x].Q −→ P [n/x]|Q[n/x].

hn/xi

R|(m−1 [n].P |m1 [x].Q) −→ R[n/x]|(P |Q)[n/x].

m−i hxi

Q −→ Q0 x 6∈ gn(P, Q)
C2
τP |Q −→ (x)(P 0 |Q0 )An application of L1 then finishes the job. Another situation arises if we modify the example tom−1 [n].P |(x)(R|m1 [x].Q). The difference is that here
the term m−1 [n].P lies outside the scope of the localization operator (x). This time we need to use C0 . But
before that an application of rule L2 is necessary. Next
consider the following reduction:

Localization
hy/xi

α

P −→ P 0 x 6= yL1τ(x)P −→ P 0

P −→ P 0 x 6∈ n(α)L0α(x)P −→ (x)P 0Pmi hy/xi−→ P 0P −→ P 0Lτ(x)P −→ (x)P 0 3

L2

mi hyi(x)P −→ P 0
Replication

τ

hx/xi

x 6= m(x)m−1 [x].P |(y)m1 [y].Q −→ (z)(P [z/x]|Q[z/y]).
It is an example of communications between local
names. The communication rule applied is C2 . A rulethat also calls for explanation is L3 . It is necessary
when two processes exchange a same local name. For
example the reduction

ConditionααP −→ P 0Rα!P −→ P 0 |!P

P −→ P 0Cα[x=x]P −→ P 0τ(x)(m−1 [x].P |m1 [x].Q) −→ (x)(P |Q)

In the above rules, α ranges over the set {τ } ∪{mi hy/xi, mi hxi, hy/xi | m, x, y ∈ N }. The notation[y/x] stands for an atomic substitution. The result of
substituting y for x throughout P is denoted by P [y/x].
Local names in P need be renamed to avoid y being
captured. A substitution [y1 /x1 ] . . . [yn /xn ] is a concatenation of atomic substitutions. The effect of applying a substitution to a process is defined as follows:
P []P [y1 /x1 ] . . . [yn /xn ]

def

=

def

=

hx/xi

is obtained from m−1 [x].P |m1 [x].Q −→ P |Q by applying L3 .
We will denote by ~x a sequence x1 , . . . , xn of names.
We will also abbreviate (x1 ) . . . (xn )P to (~x)P . Whenthe length of the sequence ~x is zero, (~x)P is just P .
Let SC be the set of contexts of the form
(x~n )(. . . (x~1 )( |R1 ) . . . |Rn ),P

where n ≥ 1 and R1 , . . . , Rn ∈ Pχ . Notice that thelength of x~i , for i ≤ n, could be zero. An element of
SC is called a static context. One useful property of astatic context C[] is that any derivative of C[P ] is of
the form C 0 [P 0 ], where C 0 [] is static and P 0 is what P
has turned into.

(. . . P [y1 /x1 ] . . .)[yn /xn ],where [] is the empty substitution. Substitutions will
be ranged over by σ. The reflexive and transitive cloτsure of −→ is denoted by =⇒. For α 6= τ , the notationαα=⇒ stands for =⇒−→=⇒.
3

a1 hzi(~x)(P |(R|(y)a1 [y])) =⇒ (x~0 )(P 0 |(R0 |0)). In order tomatch this action, we must have

3. Bisimulation congruence
A difficulty with the bisimulation equivalence for χprocesses is to do with the incomplete actions. Sup-a1 hzi(~x)(Q|(R|(y)a1 [y])) =⇒ (x~00 )(Q0 |(R00 |0))hy/xipose P and Q are bisimilar, should we require P −→such that (x~0 )(P 0 |(R0 |0)) ≈ (x~00 )(Q0 |(R00 |0)). It follows easily that (x~0 )(P 0 |R0 ) ≈ (x~00 )(Q0 |R00 ). But then(~x)(Q|R) =⇒ (x~00 )(Q0 |R00 ). Done. (ii) is a special caseof (i) and (iii) can be proved similarly.
2

hy/xi

be matched by Q −→ ? If incomplete actions are completely ignored, the bisimilarity would not be closed
under localization. But if we treat them the same as
the other actions, the resulting equivalence would be
difficult to analyze. We propose to use local bisimulation as a tool to study the algebraic properties ofχ-processes. Throughout this paper, we concentrateon weak equivalences.

Theorem 3.6 The following properties hold:(i) (m)mi [x].P ≈ 0;(ii) (x)mi [y].P ≈ mi [y].(x)P, where x 6∈ {m, y};(iii) (x)0 ≈ 0;(iv) (x)(y)P ≈ (y)(x)P ;(v) (x)(P |Q) ≈ P |(x)Q, where x 6∈ gn(P );(vi) P |0 ≈ P ;(vii) P1 |P2 ≈ P2 |P1 ;(viii) P1 |(P2 |P3 ) ≈ (P1 |P2 )|P3 ;(ix) [x=x]P ≈ P ;(x) (x)[y=z]P ≈ [y=z](x)P, where x 6∈ {y, z};(xi) (x)[y=z]P ≈ 0, where x ∈ {y, z} and y 6= z;(xii) [x=y][v=w]P ≈ [v=w][x=y]P .

Definition 3.1 Suppose R ⊂ Pχ ×Pχ . The relation
R is a local simulation if whenever P RQ, then for any
χ-process R and any sequence ~x of names it holds thatmi hxiif (~x)(P |R) =⇒ P 0 , then Q0 exists such thatmi hxi(~x)(Q|R) =⇒ Q0 and P 0 RQ0 .
R is a local bisimulation if both R and R−1 are local
simulations. P is locally bisimilar to Q, notation P ≈Q, if P RQ for some local bisimulation R.

The proof of the theorem is standard. Notice that ingeneral (x)(R|[x=a]P ) is not locally bisimilar to (x)R.
This is one of the differences between χ-calculus andπ-calculus. The next lemma is crucial to showing that≈ is a congruence relation.

Theorem 3.2 ≈ is an equivalence relation.
Definition 3.3 Suppose R ⊂ Pχ ×Pχ . The relation R
is a local simulation up to ≈ if P RQ implies that forany process R and sequence ~x of names it holds that

Lemma 3.7 If P ≈ Q, then P [y/x] ≈ Q[y/x].
Proof: Let R be the union of ≈ and the followingP ≈ Q, C[] ∈ SC,(C[P σ], C[Qσ]) σ ≡ [y1 /x1 ] . . . [yn /xn ],.
~x pairwise distinct

mi hxiif (~x)(P |R) =⇒ (~y )P 0 , then Q0 exists suchmi hxithat (~x)(Q|R) =⇒ (~y )Q0 and P 0 ≈R≈Q0 .
R is a local bisimulation up to ≈ if both R and R−1
are local simulations up to ≈.

mi hai

Suppose P ≈ Q and C[P σ] =⇒ S. Two cases:
Theorem 3.4 If R is a local bisimulation up to ≈,then R ⊂≈.

• P σ does not participate in the sequence of acmi hai

tions C[P σ] =⇒ S. Then S must be of theform C 0 [P σσ 0 ], where σ 0 is some substitution[y10 /x01 ] . . . [yn0 0 /x0n0 ]. Notice that x01 , . . . , x0n0 werelocal names. So by α-convention we can assume
that x1 , . . . , xn , x01 , . . . , x0n0 are pairwise distinct.

The proof of this theorem uses the next result.
Proposition 3.5 If P ≈ Q, then(i) for any χ-process R and any sequence ~x of names, if(~x)(P |R) =⇒ P 0 then Q0 exists such that (~x)(Q|R) =⇒Q0 and P 0 ≈ Q0 ;(ii) if P =⇒ P 0 then Q =⇒ Q0 for some Q0 such thatP 0 ≈ Q0 ;mi hximi haiBut then we have C[Qσ] =⇒ C 0 [Qσσ 0 ] with
SRC 0 [Qσσ 0 ].
• P σ does participate in the sequence of actions

mi hxi(iii) if P =⇒ P 0 then Q =⇒ Q0 for some Q0 suchthat P 0 ≈ Q0 .

mi haiC[P σ] =⇒ S. As the process C[P σ|(0|0)] is locally bisimilar to C[P σ], some S 0 exists such thatmi hai

Proof: (i) Suppose (~x)(P |R) =⇒ P 00 . Then P 00 must
be of the form (x~0 )(P 0 |R0 ). If a 6∈ {~x} ∪ n(P, Q), thenC[P σ|(0|0)] =⇒ S 0 and S ≈ S 0 . Suppose σ isthe substitution [y1 /x1 ] . . . [yn /xn ] and o is not in4n(C[P ], C[Q]) ∪ {x1 , . . . , xn } ∪ {y1 , . . . , yn }. Let
D[] be the static context C[(~x)( |A)] where A iso−1 [x1 ]. · · · .o−1 [xn ]|o1 [y1 ]. · · · .o1 [yn ]. Now(1)

It is worth remarking that the lemma does not hold for
π-calculus. Therefore local bisimilarity for π-processes
is not closed under input prefixing operation.

mi haiτ

D[P ] =⇒ C[P σ|(0|0)] =⇒ S 0 .

Theorem 3.8 ≈ is a congruence equivalence:(i) mi [x].P ≈ mi [x].Q whenever P ≈ Q;(ii) P |O ≈ Q|O whenever P ≈ Q;(iii) (x)P ≈ (x)Q whenever P ≈ Q;(iv) [x=y]P ≈ [x=y]Q whenever P ≈ Q;(v) !P ≈!Q whenever P ≈ Q.

By assumption, P ≈ Q. So T 0 exists such thatmi haiD[Q] =⇒ T 0(2)

and S 0 ≈ T 0 . For (2) to match (1), all actions ofo−1 [x1 ]. · · · .o−1 [xn ] must have reacted upon thecorresponding actions of o1 [y1 ]. · · · .o1 [yn ] when
D[Q] has evolved to T 0 , or S 0 ≈ T 0 would not
hold. Next we show that (2) can be factorized as(3)τ

Proof: (i) The proof is easy.
(ii) It suffices to show that {(P |O, Q|O) | P ≈ Q ∧ O ∈Pχ }∪ ≈ is a local bisimulation up to ≈. Suppose
R ∈ Pχ and ~x is a sequence of names. It is rather
easy to show that (~x)((P |O)|R) ≈ (~x)(P |(O|R)) andmi haiD[Q] =⇒ C[Qσ|(0|0)] =⇒ T 0 .

For simplicity, we assume that (2) is(4)

mi hai−→τ−→

mi hyiC[(x1 )(Q|(o−1 [x1 ]|o1 [y1 ]))](~x)((Q|O)|R) ≈ (~x)(Q|(O|R)). If (~x)((P |O)|R) =⇒P 0 , then by (ii) of proposition 3.5 P 00 exists such thatC 0 [(x1 )(Q0 |(o−1 [x1 ]|o1 [y10 ]))](~x)(P |(O|R)) =⇒ P 00 and P 0 ≈ P 00 . So by definition,

T 0,

Q00 exists with (~x)(Q|(O|R)) =⇒ Q00 and P 00 ≈ Q00 .
Using proposition 3.5 again, one has Q0 such thatmi hyimi hyiand we need to prove thatmi hyi(~x)((Q|O)|R) =⇒ Q0 and Q00 ≈ Q0 .
(iii) The proof is similar to that of (ii).
(iv) {(C[[x=y]P ], C[[x=y]Q]) | P ≈ Q ∧ C[] ∈ SC} is alocal bisimulation. If x=y, then the result follows from(ix) of theorem 3.6, (ii) and (iii). So assume x 6= y andC[(x1 )(Q|(o−1 [x1 ]|o1 [y1 ]))]
(5)

τ

−→

C[Q[y1 /x1 ]|(0|0)]

mi haiT 0.

−→

mi hzi

The general case can be proved by induction. (4)can be rewritten asC[[x=y]P ] =⇒ P 0 . Consider only one case. Supposemi hziC[[x=y]P ] =⇒ C 0 [([x=y]P )σ] for some static context
C 0 [] and some substitution σ such that xσ = yσ. Cor-C[(x1 )(Q|(o−1 [x1 ]|o1 [y1 ]))]mi hai−→τ−→≡

mi hzi

respondingly we have C[[x=y]Q] =⇒ C 0 [([x=y]Q)σ].
By lemma 3.7, P σ ≈ Qσ. The rest of the argument issimilar to that when x = y.
def(v) R = {(C[!P ], C[!Q]) | P ≈ Q ∧ C[] ∈ SC} is alocal bisimulation up to ≈. Consider only one case. If

C 0 [(x1 )(Qσ|(o−1 [x1 ]|o1 [y1 σ]))]C 0 [Qσ[y1 σ/x1 ]|(0|0)]
C 0 [Q[y1 /x1 ]σ|(0|0)].

If the first action doesn’t have any effect on(x1 )(Q|(o−1 [x1 ]|o1 [y1 ])), then σ is []. If it does
affect the process (x1 )(Q|(o−1 [x1 ]|o1 [y1 ])), then σmust be [a/z] such that x1 , a and z are pairwise
distinct. In either case, the syntactical equality
holds. On the other hand, (5) ismi hxi−→C[Q[y1 /x1 ]|(0|0)]

mi haiC 0 [Q[y1 /x1 ]σ|(0|0)].

−→mi hxiQ =⇒ Q0 with P 0 ≈ Q0 by proposition 3.5.

So

mi hxiC[!Q] =⇒ C[Q0 |!Q]. Now by (vii) of theorem 3.6, (ii)and (iii), C[P 0 |!P ] ≈ C[Q0 |!P ] ≈ C[!P |Q0 ]RC[!Q|Q0 ] ≈C[Q0 |!Q].
2
In [5] barbed bisimulation is proposed as a universal
tool applicable to a variety of process calculi. Let ≈bbe the barbed bisimilarity on χ-processes.
Theorem 3.9 ≈b is the same as ≈.

So we have proved that (2) can be rearranged
mi haimi hxi

C[!P ] =⇒ C[P 0 |!P ] is induced by P =⇒ P 0 , thenC[(x1 )(Q|(o−1 [x1 ]|o1 [y1 ]))]
τ

2

So R is a local bisimulation.

0

as (3). Now C[Qσ|(0|0)] =⇒ T implies that

The proof of the theorem consists of two parts. In one
direction, one shows that ≈b is a local bisimulation.
In the other direction, one proves that ≈ is a barbed
bisimulation. Both are straightforward.

mi haisome T exists such that C[Qσ] =⇒ T withT 0 ≈ T . So S ≈ T . This closes up the bisimulation game.
54. Higher order χ-calculus

Sequention
gn(A) ∩ ln(P ) = ∅There are two typical kinds of recursion mechanisms
employed in process algebras. In CCS the recursion
mechanism consists of the fix-expressions and the rule

mi [A]

mi [A].P −→ P

mi hAimi (X).P −→ P [A/X]

S2Parasition
mi hAiQ −→ Q0α

E[fix(E)/X] −→ E 0
rec.
αfix(E) −→ E 0

mi hAiP |Q −→ P |Q0
QWhat one should notice about the rule is that it adds
nothing to the communication mechanism. What therule really says is that E[fix(E)/X] and fix(E) can be
regarded as syntactically the same. The same can besaid about the recursion mechanism via the duplicatorin π-calculus. So the first order approach essentiallyadmits infinite long expressions that can be coded up
by finite number of symbols. In a first order calculus, the recursion power is achieved syntactically. The
other approach is the higher order one which allows aprocess to be the content of a communication. In ahigher order process calculus, unlike in the first ordercase, the recursion and the communication mechanisms
are intertwined; the former is part of the latter. That
is to say that the recursion power is achieved semantically. The two methods are not unrelated. The higher
order one can code up the first order one, whereas thefirst order one, in case of the higher order polyadic πcalculus ([6]) and the (Plain) CHOCS ([7, 8]), is able
to imitate the higher order one.
We now take a look at χω , the higher order χcalculus. Part of the agenda in this section is todemonstrate that local bisimulation is the right technical tool for proving equivalence of higher order processes. Let V be the set of process variables, ranged
over by X, Y, Z, . . .. The set E of process expressions
is the least set consisting of the expressions defined by
the following abstract syntax:
E

S1

(~
x)mi [A]

−→

Q0

P |Q

P4

{~x} ∩ gn(P ) = ∅(~x)mi [A]

−→

P5

P |Q0

Communication
P(~x)mi [A]−→P0m−i hAi

Q −→ Q0 {~x} ∩ gn(Q) = ∅C3
τP |Q −→ (~x)(P 0 |Q0 )Localization
mi hAiP −→ P 0

x 6∈ gn(A)mi hAi(x)P −→ (x)P 0
P(~x)mi [A]

−→

P0

(y)P
P

(~
x)mi [A]−→(y)Py ∈ gn(A) \ {~x}(y)(~x)mi [A]

−→

P0

L4

P0

L5

y 6∈ gn(A) \ {~x}(~x)mi [A]−→(y)P 0

L6

In the rules, α ranges over all actions. Notice that inthis language, the replicator is unnecessary, a fact tobe justified below. Algebraic equivalences for higher
order processes are more interesting than those in thefirst order case. Again the difficulty is to do with thetreatment of output actions. When comparing for example ai [A].P and ai [B].Q, it is much too strong torequire A and B be syntactically the same in order
for ai [A].P and ai [B].Q to be equivalent. A refinedtreatment allows us to regard the processes as equivalent whenever A and B, P and Q are equivalent. The
higher order bisimilarities used in [7, 8] are precisely
equivalences of this kind. But still, these equivalences
are too strong. The reason is that when comparing
ai [A].P and ai [B].Q in this approach, the processes A
and P , respectively B and Q, are considered separately.
This overlooks any possible localization operators thatmight surround ai [A].P . To take this into account,context bisimilarity is proposed in [6]. It is shown in
the paper that context bisimilarity coincides with thebarbed bisimilarity on higher order π-processes.
Our approach to the equivalence of higher order χprocesses is similar to that based on context bisimulations. The definition of local bisimulation for higher order χ-processes is completely the same as definition 3.1;:= 0 | X | mi [n].E | E|E | (x)E| mi (X).E | mi [E].E,

where i ∈ {−1, 1}. For a subset V of V, let E[V ] denote the set of process expressions whose free variables
are all in V . When V is a finite set {X1 , . . . , Xn },we write E[X1 , . . . , Xn ] for E[{X1 , . . . , Xn }]. A higher
order χ-process is a process expression that does notcontain any variables. The set of all higher order χprocesses is denoted by Pχω , which will be ranged
over by P, Q, R, . . .. The operational semantics for thehigher order χ-calculus is defined by the operationalrules of the first order χ-calculus together with the following rules, noticing that we have again left out all
the symmetric rules:
6and the notion of local bisimulation up to ≈ can besimilarly defined as in 3.3. It follows that the results intheorem 3.2, theorem 3.4, proposition 3.5, theorem 3.6,
and lemma 3.7 all hold for higher order χ-processes.
The proofs of them are just as simple.

bisimulation up to ≈. The result follows by observing
that (mi [A].P )R(mi [B].P ).
2

Theorem 4.1 ≈ is preserved by all combinators:(i) mi [x].P ≈ mi [x].Q whenever P ≈ Q;(ii) P |O ≈ Q|O whenever P ≈ Q;(iii) (x)P ≈ (x)Q whenever P ≈ Q;(iv) [x=y]P ≈ [x=y]Q whenever P ≈ Q;(v) !P ≈!Q whenever P ≈ Q;(vi) mi [A].P ≈ mi [A].Q whenever P ≈ Q;(vii) mi [A].P ≈ mi [B].P whenever A ≈ B.

Corollary 4.2 Suppose E ∈ E[X]. If A ≈ B, thenE[A/X] ≈ E[B/X].

Let E, F ∈ E[X1 , . . . , Xn ]. Define E ≈ F if for any~ ≈processes P1 , . . . , Pn ∈ Pχω , it holds that E[P~ /X]~~
F [P /X].

5. General recursion in χωIn [7], the general recursion recX.E is defined asfollows:
def

recX.E = (a)(a?X.(E|a!X)|a!(a?X.(E|a!X))).

Proof: We only prove (vii). For the sake of this proof,
let’s define Eo [X] to be the set of all process expressions
E in E[X] such that each occurrence of X is within
ai [F ] for some a ∈ N and some process expression F .
We first prove an auxiliary fact: Suppose E ∈ E0 [X].
Thenmi hxiOne hasτ

recX.E −→ (a)(E[a?X.(E|a!X)]|a!(a?X.(E|a!X))).
This reduction looks like an operational simulation of
the recursion equation recX.E = E[recX.E/X]. Unfortunately the equation is not verified by the higher order bisimilarity. This is because the higher order bisimilarity has too strong a distinguishing power. However,
the encoding per se is good, a fact we are going toprove.
Suppose E ∈ E[X] and a does not occur in E. The
following abbreviations will be used:

mi hxi• if E[A/X] −→ P , then E[B/X] −→ Q suchthat P ≡ F [A/X] and Q ≡ F [B/X] for some F
in Eo [X];ττ• if E[A/X] −→ P , then E[B/X] −→ Q such thatP ≡ F [A/X] and Q ≈ F [B/X] for some F in
Eo [X].

Wa (E)The proof of the fact goes as follows:

recX.Emi hxi• If E[A/X] −→ P , then clearly P ≡ F [A/X] for

def

=

def

=

a1 (X).(E|a−1 [X]),(a)(Wa (E)|a−1 [Wa (E)]).

Before proving the property concerning recX.E, we
first establish a useful result. Let F [ΩE ] denote theexpression (a)(F [Wa (E)/X]|a−1 [Wa (E)]) where a isfresh.

mi hxisome F ∈ Eo [X] and E[B/X] −→ F [B/X].
τ• If E[A/X] −→ P is a first order communication, then P ≡ F [A/X] for some F ∈ Eo [X] andτ
E[B/X] −→ F [B/X].

Lemma 5.1 Suppose E, F ∈ E[X], b is fresh and F 0
is obtained from F [Wa (E)/X] by replacing some occurrences of Wa (E) by Wb (E). Then F [ΩE ] is locallybisimilar to (a)(b)(F 0 |(a−1 [Wa (E)]|b−1 [Wb (E)])).

τ• If E[A/X] −→ P is a higher order communication, then P ≡ F [A/X] for some F ∈ Eo [X]. Nowτ
E[B/X] −→ Q by carrying out the ‘same’ communication. If we replace by A all the occurrences of
B in Q that do not appear in an output expression,
we get F [B/X]. By (i) through (vi), F [B/X] ≈ Q.

τ

Proof: Suppose (a)(F [Wa (E)/X]|a−1 [Wa (E)]) −→P is caused by a higher order communication between
F [Wa (E)/X] and a−1 [Wa (E)]. Then clearlyP ≈ (a)(H[Wa (E)/X]|a−1 [Wa (E)])

This concludes the proof of the auxiliary fact. Let R
be {(E[A/X], E[B/X]) | A ≈ B ∧ E ∈ Eo [X]}. Now

for some H ∈ E[X]. By carrying out essentially thesame higher order communication between either F 0
and a−1 [Wa (E)] or F 0 and b−1 [Wb (E)], we get, forsome Q ∈ Pχω ,mi hxisuppose E[A/X]RE[B/X] and E[A/X] =⇒ P . ThenP ≡ F [A/X] for some F ∈ Eo [X]. By the above fact,
we can find, by repeatedly using (ii) of proposition 3.5,(a)(b)(F 0 |(a−1 [Wa (E)]|b−1 [Wb (E)]))mi hxisome Q such that E[B/X] =⇒ Q and F [B/X] ≈ Q.
This should be enough of an evidence that R is a localτ−→≈ (a)(b)(H 0 |(a−1 [Wa (E)]|b−1 [Wb (E)]))7

where H 0 is obtained from H[Wa (E)/X] by replacingsome occurrences of a−1 [Wa (E)] by b−1 [Wb (E)]. From
this example, it is easy to see that((~x)(a)(F [Wa (E)/X]|a−1 [Wa (E)]),φ(~x)(a)(F 0 |(a−1 [Wa (E)]|b−1 [Wb (E)])))

6. Conclusion
There are several questions one usually asks about amathematical model for concurrent computations. One
is concerned with the primitivity of the model. Doesit capture the essence of concurrent computations in
a simple yet elegant way? The χ-calculus is grammatically simple and conceptually coherent. Anotherquestion is to do with concurrency degree. To what
extent does the model permit parallelism? There islittle doubt that the χ-calculus allows more freedom
than the π-calculus in this respect. A manifestation ofthis fact is that the operational semantics of the callby-name λ-calculus can be imitated in χ-calculus in astraightforward manner.
The paper has just begun the study of χ-like process
algebras. Quite a lot of interesting questions await tobe answered. It is hoped that further research will tell
us more about what χ really differs from π and will
eventually lead us to a canonical process calculus that
encapsulates concurrent computations, object-oriented
programming ([9]), full λ-calculus ([1, 3]) and proofs oflinear logic ([2]).

is a local bisimulation up to ≈, where φ is
E, F ∈ E[X], a, b 6∈ n(E, F ), x1 , . . . , xn ∈ N ,and F 0 is obtained from F [Wa (E)/X] by replacing some occurrences of a−1 [Wa (E)] by
b−1 [Wb (E)].
2

Details are omitted.

Theorem 5.2 recX.E ≈ E[recX.E/X] provided thatE ∈ E[X].
Proof: We show that the following relation
gn(E) ∩ ln(F ) = ∅,(F [ΩE ], F [recX.E])
E ∈ E[X], F ∈ E[X]
is a local bisimulation up to ≈. Let R be a process and~x a sequence of names. Supposeτ(~x)((a)(F [Wa (E)/X]|a−1 [Wa (E)])|R) −→ P.

References

The most interesting case is when a higher ordercommunication between F [Wa (E)/X] and a−1 [Wa (E)]happen. Without loss of generality, let F be X|F1 .
ThenP[1] H. Barendregt, 1984. The Lambda Calculus: Its Syntax
and Semantics. Studies in Logic and Foundations ofMathematics, North-Holland.

≡ (~x)((a)(((E[Wa (E)/X]|a−1 [Wa (E)])|F1 [Wa (E)/X])|0)|R)≈ (~x)((a)(b)(((E[Wb (E)/X]|b−1 [Wb (E)])|F1 [Wa (E)/X])|a−1 [Wa (E)])|R)≈ (~x)(a)((((b)(E[Wb (E)/X]|b−1 [Wb (E)])|R)|F1 [Wa (E)/X])|a−1 [Wa (E)])≡ (~x)H[ΩE ],[2] G. Bellin and P. Scott, 1992. On the π-Calculus andLinear Logic. Technical Report, LFCS, Department ofComputer Science, University of Edinburgh.
[3] R. Milner, 1992. Functions as Processes. Journal of
Mathematical Structures in Computer Science, 2, 119–141, Cambridge University Press.
[4] R. Milner, J. Parrow and D. Walker, 1992. A Calculusof Mobile Processes. Information and Computation,
100, Part I:1–40, Part II:41–77, Academic Press.

where H≡((b)(E[Wb (E)/X]|b−1 [Wb (E)])|R)|F1 ∈E[X].
Correspondingly, we have≡[5] R. Milner and D. Sangiorgi, 1992. Barbed Bisimulation, 19th ICALP, LNCS 623, W. Knich ed. 685–695,
Springer Verlag.

(~x)(F [recX.E/X]|R)(~x)((recX.E|F1 [recX.E/X])|R)[6] D. Sangiorgi, 1993. Expressing Mobility in Process
Algebras: First-Order and Higher-Order Paradigms.
PhD thesis, Department of Computer Science, University of Edinburgh.

τ−→ (~x)(((a)(E[Wa (E)/X]|a−1 [Wa (E)])|F1 [recX.E/X])|R)≈ (~x)(H[recX.E/X])[7] B. Thomsen, 1993. Plain CHOCS—A Second Generation Calculus for Higher Order Processes. Acta Informatica, 30, 1–59, Springer Verlag.

to match the previous reduction. The details of theproof are omitted. So
recX.E[8] B. Thomsen, 1995. A Theory of Higher Order Communicating Systems. Information and Computation, 116,
38–57, Academic Press.

≈ (a)(E[Wa (E)/X]|a−1 [Wa (E)])≈ E[recX.E/X],

which completes the proof.

[9] D. Walker, 1995. Objects in the π-Calculus. Information and Computation, 116, 253–271, Academic Press.

28