Axiomatization without Prefix Combinator
Yuxi Fu?
Department of Computer Science
Shanghai Jiaotong University, Shanghai 200030, China
E-mail: fu-yx@cs.sjtu.edu.cn

Abstract. The chi calculus proposed several years ago enjoys someproperties unknown from the experience with pi calculus, one of whichis the ability to model concurrent computation without the use of prefixcombinator. The atomic chi calculus studied in this paper is obtained
from polyadic chi calculus by leaving out the prefix operator. This omission is impossible in the pi framework because it would render the input
actions of pi useless. This paper focuses on complete systems of strong
equivalence relations on finite atomic chi processes. The two equivalence
relations investigated in this paper are strong bisimilarity and strong
asynchronous bisimilarity. These bisimilarities are required to be closed
under substitution on each bisimulation step. By exploring some properties enjoyed by the atomic chi calculus, it is shown that they coincide
respectively with their ground counterparts. In the definitions of strong
ground bisimilarity and strong asynchronous ground bisimilarity closure
under substitution is not explicitly required. Based upon this fact complete systems are given for both relations. The axiomatic systems arenovel in that they use none of the prefix, choice and match combinators.

Key Words: Process Algebra, Bisimulation, Axiomatization

1

Introduction

Operationally computations are achieved by substitutions. This is clear from
λ-calculus, the canonical model for functional computation, and π-calculus, amodel for concurrent computation. An abstraction term in λ-calculus is of theform λx.t. Semantically it is a function that yields t[s/x], the result of substituting s for x throughout t, when given s. This operational behaviour is formalized
in the following β-reduction rule:(λx.t)s → t[s/x]The variable x in λx.t is bound. A bound name in a term can be replaced by afresh name without affecting the meaning of the term. The input prefix operationof π-calculus ([19]) takes similar form as a(x).P . This is the process that can?

Proceedings of the International Symposium on Domains and Processes ’99 , K.
Keimel et al eds., Kluwer Academic Publishers, 245-273, 2001.

receive a channel name y through x and then proceeds as P [y/x]. The channelname x in a(x).P is bound. The semantics of a π-process in output prefix form
ax.Q is different in that it is ready to emit a channel name x through a and thenevolve as Q. In a(x).P and ax.Q we say that P and Q are the continuations of
the processes. As opposed to the x in a(x).P , the channel name x in ax.Q isfree. A communication between input prefix process and output prefix process
can happen when they share common channel. Communications are formalized
by labeled transitions as in the following example:
τa(x).P |ay.Q −→ P [y/x]|Q
The input and output processes differ in another aspect. In ax.Q the prefix
operator act as a sequential combinator. It has no other function. On the other
hand the prefix operator of a(x).P plays a double role. It is both a sequential
operator and a binding combinator. Another binding combinator in π-calculus
is the localization operator. In (x)P the component (x) localizes x to process P ,meaning that the channel x can only be used within P . The localization operator
adds a great deal of power to π-calculus.
The π-calculus is also called monadic π-calculus. The phrase ‘monadic’ indicates the fact that in a communication a process can emit or input only one
channel at a time. In practice there is a need for processes to be able to send
and receive a number of channels in one communication. The polyadic π-calculus
extends the monadic π-calculus with this capacity ([18]). The input and output
processes of the latter become respectively a(x̃).P and aỹ.Q in the former, wherex̃ and ỹ stand for finite sequences of channel names. A communication in thepolyadic version looks as follows:τa(x̃).P |aỹ.Q −→ P [ỹ/x̃]|Qin which [ỹ/x̃] is a simultaneous substitution of ỹ for x̃.
One of the applications of the polyadic π-calculus is in the computational
interpretation of classical proof theory. Girard was the first to point out possible
connections between classical linear logic and parallelism ([13]). Abramsky madean important step in relating cut eliminations in linear logic to communicationsin π-calculus ([1]). It was discovered in his work that the prefix operator plays norole in modeling the dynamics of the proof theory. This raises the question of if
prefix operators are really necessary in a model for concurrent computation. The
asynchronous π-calculus can be seen as a partial answer to the question ([15, 3,2]), in which output actions do not have continuations. It has been shown thatthe language has enough expressive power to do what π-calculus can do. The
algebraic theory of the asynchronous π-calculus is slightly different from that of
π-calculus. For one thing the standard definition of barbed bisimilarity need bemodified to take into account the asynchronous nature of the language. In some
aspects the algebraic theory is also a little harder. For example axiomatization of
weak equivalence on asynchronous π-processes is unknown. In the asynchronous
π-calculus the input prefix operator remains the same as in the π-calculus. Thereis absolutely no way to remove the continuations away from the processes in input

prefix form for that would have rendered the resultant language totally useless.
The failure is due to the double role of the prefix operator mentioned above. The
binding power of the operator would be reduced to none if there is nothing tobind over.
One solution to the problem is to disassociate the binding ability of the prefix
operator from the sequentialization ability of the combinator. The χ-calculus
proposed by present author ([4–12]) is a process calculus that achieves just that.
The processes in input and the output forms are unified as α[x].P , where α
could be either a or a and x is global. The binding power of the language isprovided solely by the localization operator. So for instance the channel namex in (x)α[x].P is local. A communication in χ-calculus amounts to instantiating
a local channel name by a global channel name or identifying two local channel
names. The following two examples of reduction should provide some intuition:
τa[y].Q|(x)a[x].P −→ Q|P [y/x]τ(y)a[y].Q|(x)a[x].P −→ (z)(Q[z/y]|P [z/x])
Now in χ-calculus one can give up on continuations altogether. The language
one obtains has the following abstract grammar:
P := 0 | α[x] | P |P | (x)P |!P
in which !P is a replication process that provides potentially infinite copies of
P . Unfortunately this language is too weak, the reason being that it lacks theability to control the order of computations. A communication of the languagetransports only one token, which can be used either as a value or as control
information but not both. This immediately suggests a solution: To abandon
the prefix operator, one should work with a polyadic calculus. The polyadic χcalculus has been studied by Parrow and Victor ([21–24]). They call it Fusion
Calculus.
The atomic χ-calculus studied in this paper is obtained from the polyadic χcalculus by leaving out the prefix operator. The abstract syntax of the language
is as follows:
P := 0 | α[x̃] | P |P | (x)P |!P
The atomic χ-calculus has a great deal of control power. The following example
suffices to demonstrate this point:τ(x)(y)(z)((a[x, y]|a[b, b])|(x[z]|y[c])) −→ (z)((0|0)|(b[z]|b[c]))τ−→ (0|0)|(0|0)
It is apparent that the order of the two communications can not be swapped.
Using ideas embodied in the above example, one can show that the lazy λcalculus can be interpreted in the atomic χ-calculus. This calculus was proposedby Laneve and Victor ([16]). They call it Solos. However we will refer to thecalculus as the atomic χ-calculus in the rest of the paper.

The theory of process calculus is mainly about algebraic properties of processes. Algebraic studies are based on equivalence relations, of which the mostimportant ones are observational equivalences. The most well known observational equalities are the bisimulation equalities. Two processes are bisimilar ifthey can simulate each other’s actions and evolve to two bisimilar processes.
Bisimilarity equalities differ from one another in the extent actions can be observed. Another aspect of algebraic theory of process calculus is about axiomatic
systems for congruence relations on processes. Each system consists of a set of
conditional equations. A system should be both sound and complete in the sensethat it derives equivalent and only equivalent processes with respect to the intended equality.
The focus of this paper is on algebraic theory of the atomic χ-calculus. Twobisimulation equivalence relations are investigated. They are strong bisimilarity and strong asynchronous bisimilarity. Like the situation in the asynchronous
π-calculus the asynchronous bisimilarity takes care of some very special operational properties of the atomic χ-calculus. Let’s see a typical example. The twoprocesses (x)(a[x]|a[x]) and (a)(x)(a[x]|a[x]) are not bisimilar in the synchronous
sense but are equivalent in the asynchronous view. The role of (x)(a[x]|a[x]) is
to absorb an atomic process of the form a[b] or a[b] as in the following communicationτa[x]|(x)(a[x]|a[x]) −→ 0|(0|a[b])The process (a)(x)(a[x]|a[x])|a[b] can emulate the above reduction by performing an internal communication. This example should convince the reader that(x)(a[x]|a[x]) and (a)(x)(a[x]|a[x]) are observationally equivalent.
Both bisimilarities are closed under substitution of channel names. Closure
under substitution of channel names is a reasonable requirement in order toguarantee congruence property because channel names in a mobile process do
get changed as results of process interactions. If one does not insist on the closure
property, one gets what we call ground bisimilarity. Usually the ground bisimilarity is a much weaker relation. We will prove however that in atomic χ-calculus
strong bisimilarity and strong asynchronous bisimilarity coincide respectively
with strong ground bisimilarity and strong asynchronous ground bisimilarity.
This is anticipated by the work of Amadio, Castellani and Sangiorgi on asynchronous π-calculus. This fact is then explored to study axiomatization problem
for the two bisimilarities. Usually complete systems for congruence relations onmobile processes make heavy use of choice and match combinators, not to mention prefix operator. We give in this paper complete systems for the two strong
bisimilarities. These systems are novel in that none of the prefix combinator, thechoice combinator and the match combinator is used.
In [16] Laneve and Victor have shown how to encode some well-known process
combinators in the atomic χ-calculus. These encodings are faithful with respect
to some particular algebraic equivalences. Their results demonstrate to someextent the expressive power of the calculus. While we should emphasize theimportance of the work of Laneve and Victor, we would also like to point out
that the study in this paper is neither about the language per se nor about its

expressiveness. It is about axiomatization of algebraic congruences with neither
the choice combinator nor the prefix operator. Since the atomic χ-calculus, orSolos, is the only process calculus without the prefix combinator at the time ofwriting, it is the only framework one can work with at the moment.
The structure of the paper is as follows: Section 2 lays down some preliminaries. Section 3 introduces polyadic χ-calculus and some technical lemmas.
The reason to go through the polyadic χ-calculus first is that most account ofpolyadic χ-calculus and the atomic χ-calculus are the same. The time spent on
the former is worth the effort. Section 4 defines the semantics of the atomic
χ-calculus and proves some crucial lemmas. Section 5 simplifies the definitionof open bisimilarity by providing an alternative formulation in terms of groundbisimulation. Section 6 makes use of this result and gives a complete system forstrong ground bisimilarity. Section 7 concludes with some final remarks.

2

Preliminaries

A process calculus needs to deal with substitutions. In polyadic calculus morecare is called for since one has to use simultaneous substitutions. Also in polyadic
calculus a channel must be assigned a sort to prevent confusion. This section introduces some notations and preliminary definitions for substitution and sorting.
2.1

Normal Substitution

All process calculi proposed so far are based upon the notion of channels. Processes communicate through channels. Usually a channel is used only as a token.
Its sole identity is that it is distinct from any other channel. For this reason one
often talks about channel names or simply names. Let N be a set of names,
ranged over by lower case letters. Let N be the set of conames {x | x ∈ N }.
Names and conames can be understood as the two ends of channels. Two processes can communicate if they are connected to the two ends of a same channel.
The union N ∪ N will be ranged over by α.
A sequence of names is often abbreviated by x̃. Accordingly (x1 ) · · · (xn )P
is abbreviated by (x̃)P . The length of x̃ is denoted by |x̃|. A name might occur
more than once in a name sequence. For example x, y, x is a name sequence.
But when used as in (x̃)P , we always assume that all names occurring in x̃ arepairwise distinct. Occasionally we think of a sequence x̃ = x1 , . . . , xn as themulti-set {x1 , . . . , xn }. This is the case when we apply set theoretical operations
on sequences of names. We will write {x̃} for the set that contains precisely theelements appeared in x̃. For instance if x̃ = yzy then {x̃} = {y, z}. When theelements of x̃ are pairwise distinct, the set {x̃} is also abbreviated to x̃.
A substitution σ is a function from N to N such that the set {x | x ∈N , σ(x) 6= x} is finite. The domain of a substitution σ, denoted by dom(σ),
is the set {x | x ∈ N , σ(x) 6= x}. The range of σ, rng(σ), is defined as theimage of dom(σ). A substitution σ is often written as [y1 /x1 , . . . , yn /xn ] whendom(σ) = {x1 , . . . , xn } and rng(σ) = {y1 , . . . , yn }. This is the function defined
as follows:
y1 , if x = x1



 ..
σ(x) = .
y , if x = xn
 nx, if x 6∈ {x1 , . . . , xn }The identity function is the vacuous substitution. It will be denoted by []. The
composition of two substitutions σ1 and σ2 , notation σ1 σ2 , is defined in terms offunction composition: σ1 σ2 is function σ1 followed by σ2 . So P σ1 σ2 is (P σ1 )σ2 .
For a set of names S, write σ −1 (S) for the set {x|σ(x) ∈ S}.
Definition 1. A substitution σ is normal if dom(σ) ∩ rng(σ) = ∅.
Suppose σ 0 is defined as follows: y, if a = xdef
σ 0 (a) = x, if a = y
a, if otherwise
Then σ 0 is typically not normal as dom(σ 0 ) ∩ rng(σ 0 ) = {x, y} =6 ∅.
Suppose σ = [y1 /x1 , . . . , yn /xn ] is a normal substitution. Define σ↑z to be
the following function:
yi , if x = xi ∧ x 6= z ∧ (1 ≤ i ≤ n)σ(x) =
x, if otherwise
For instance [u/x, v/y, w/z]↑y = [u/x, w/z]. It is clear that σ↑z is a normal
substitution. We will write σ↑{z1 , . . . , zn } for (. . . (σ↑z1 ) . . .)↑zn .
Composition of two normal substitutions is not necessarily normal. A counterexample is as follows: Both σ1 : [x → a, y → b] and σ2 : [a → y, b → x] arenormal. But neither σ1 σ2 nor σ2 σ1 is normal. The next lemma gives a sufficientcondition under which normal substitutions compose.
Lemma 2. If σ1 and σ2 are normal substitutions and dom(σ1 ) ∩ rng(σ2 ) = ∅then σ1 σ2 is normal.
Proof. dom(σ1 σ2 ) is obviously finite.
dom(σ1 σ2 ) ∩ rng(σ1 σ2 )⊆ (dom(σ1 ) ∪ dom(σ2 )) ∩ ((rng(σ1 ) ∪ rng(σ2 )) \ (rng(σ1 ) ∩ dom(σ2 )))= dom(σ1 ) ∩ rng(σ1 ) ∪ dom(σ1 ) ∩ rng(σ2 ) ∪ dom(σ2 ) ∩ rng(σ1 ) ∪dom(σ2 ) ∩ rng(σ2 ) \ ((dom(σ1 ) ∪ dom(σ2 )) ∩ (rng(σ1 ) ∩ dom(σ2 )))= (rng(σ1 ) ∩ dom(σ2 )) \ (rng(σ1 ) ∩ dom(σ2 ))=∅So dom(σ1 σ2 ) ∩ rng(σ1 σ2 ) = ∅.

tu

On the other hand, the effect of a general substitution [y1 /x1 , . . . , yn /xn ]on a term is the same as that of the composition of a finite number of normal
substitutions as [z1 /x1 ] . . . [zn /xn ][y1 /z1 ] . . . [yn /zn ] where z1 , . . . , zn are freshnames that do not occur in the term the substitution is applied to. Substitutionsof the form [y/x] are called atomic substitutions.
Suppose x̃ = x1 , . . . , xn and ỹ = y1 , . . . , yn are two name sequences of lengthn. Then x̃=ỹ, which denotes x1 = y1 , . . . , xn = yn , induces an equivalence
relation on N . Let σx̃=ỹ denote any chosen substitution that maps all elementsof an equivalence class of the equivalence relation to a specific element of thatclass. Obviously σx̃=ỹ is a normal substitution.
Suppose x1 , . . . , xn and y1 , . . . , yn are name sequences of length n. We saythat x1 , . . . , xn and y1 , . . . , yn are consistent if ∀i, j ∈ {1, . . . , n}.xi =xj ⇔ yi =yj
and that x1 , . . . , xn are replaceable by y1 , . . . , yn if ∀i, j ∈ {1, . . . , n}.xi =xj ⇒yi =yj . When {x1 , . . . , xn } ∩ {y1 , . . . , yn } = ∅ and x1 , . . . , xn are replaceable byy1 , . . . , yn , [y1 /x1 , . . . , yn /xn ] is a normal substitution.
2.2

Sorting

To avoid communication confusion, a name must be of some sort. The sort of aname indicates both the number of names it carries when communicating andthe sorts of these names. The set N is partitioned into an infinite number ofcollections of names, each of which contains an infinite number of names. Eachcollection is called a subject sort. We write a : S to mean that a is of sort S.
A nonempty tuple of sorts hS1 , . . . , Sn i is called an object sort. A sorting is afunction Sort from the set of subject sorts to the set of object sorts. For eachsubject sort S the object sort Sort(S) declares the sorts of names associated tosort S. In the rest of this paper we fix a sorting function Sort.

3

Polyadic χ-Calculus

Parrow and Victor formulate the operational semantics in a late style. In thispaper we use an early semantics.
The abstract syntax of polyadic χ-processes is given by the following BNF:
P := 0 | α[x̃].P | P |P 0 | (x)P | !P
As usual 0 is the nil process that can do nothing. We will omit a trailing 0. P |Q
is the process of composition form, where P and Q can evolve independently andcommunicate if they want to. In (x)P the name x is local, meaning that it can
not been seen from outside. We will adopt the α-convention saying that a local
name in a term can be replaced by a fresh name without changing its syntax. Let
gn(P ) denote the set of global names, or nonlocal names, in P . The processesa[x̃].P and a[x̃].P are in prefix form. Roughly they have to perform the prefix
actions and then act as P . Both a[x1 , . . . , xn ].P and a[x1 , . . . , xn ].P must be wellsorted in the sense that x1 : S1 , . . . , xn : Sn whenever Sort(a) = hS1 , . . . , Sn i.
The set of polyadic χ-processes will be denoted by P.

In the labeled transition semantics two kinds of labels are used: the set of
output actions is the set{(ỹ)α[x̃] | ỹ ⊆ x̃ where ỹ are pairwise distinct}
and the set of updates{σx̃=ỹ | |x̃| = |ỹ|}
The latter set contains the empty substitution [] which will be denoted by τ .
We now define formally the operational semantics. In the following formulation, symmetric rules have been omitted.
Sequentialization
Sqn

α[x̃]

α[x̃].P −→ P
Composition(ỹ)α[x̃]P −→ P 0

σx̃=ỹỹ ∩ gn(Q) = ∅P −→ P 0
Cmp1
P |Q −→ P 0 |Qσx̃=ỹ

Cmp0(ỹ)α[x̃]P |Q −→ P 0 |Qσx̃=ỹ

Communication(ũ)α[x̃]P −→ P 0
P |Q ũ ∩ ṽ = ∅w̃ = rng(σx̃=ỹ ) ∩ ũṽ(σx̃=ỹ )−1 (w̃) ⊆ ũṽ(ṽ)α[ỹ]Q −→ Q0σx̃=ỹ ↑ũṽ

−→

Cmm

(w̃)(P 0 σx̃=ỹ |Q0 σx̃=ỹ )Localization
δP −→ P 0

σx̃=ỹ

P −→ P 0

z 6∈ n(δ)δ(z)P −→ (z)P

Loc0

0

(ỹ)α[x̃]P −→ P 0(z)P −→ P 0

z ∈ {x̃} \ ỹ(z)Pz ∈ dom(σx̃=ỹ )σx̃=ỹ ↑z(z)(ỹ)α[x̃]

−→

Loc1

α 6∈ {z, z}
Loc2

P0

Replication
δP |!P −→ P 0
δ!P −→ P 0

Rpl

The side condition on Cmm is a bit involved. Here is an example of applying
the rule:P(c)(x)a[c,x,x,u]

−→

P0

Q

(d)(v)a[d,y,w,v]

−→

Q0

[y/w]

P |Q −→ (c)(P [c/d, y/x, y/w, u/v]|Q[c/d, y/x, y/w, u/v])
where ũ = cx, x̃ = cxxu, ṽ = dv, ỹ = dywv, w̃ = c and σx̃=ỹ is chosen to be[c/d, y/x, y/w, u/v].

[]

In what follows, σx̃=ỹ will often be abbreviated to σ and −→ will always beτsimplified to −→. In other words τ is identified to [] when used as a label in thetransitional semantics.
Two processes are strongly bisimilar if they can simulate each other’s actions
and evolve into processes that are still strongly bisimilar. In this approach allactions, whether they are internal or external, are treated with equal importance. The relation introduced in the following definition would be called strong
open bisimilarity by some researchers. We will however simply call it strong
bisimilarity.
Definition 3. Suppose R is a symmetric binary relation on A. The relation R
is a strong bisimulation if whenever P RQ then the following properties hold:
σx̃=ỹ
(i) If P σ −→ P 0 (including the case when σx̃=ỹ = τ ) for a substitution σ thenσx̃=ỹ
some Q0 exists such that Qσ −→ Q0 and P 0 RQ0 .
(ỹ)α[x̃](ii) If P σ −→ P 0 for a substitution σ then some Q0 and y˜0 exist such that˜0(y )α[x̃]Qσ −→ Q0 , {ỹ} = {y˜0 } and P 0 RQ0 .
The strong bisimilarity ∼ is the largest strong bisimulation.

The closure under substitution ensures that ∼ is a congruence relation. The
proof of this fact is routine. The two processes (x)(y)a[x, y].P and (y)(x)a[x, y].P
are bisimilar. The transition (x)(y)a[x, y].P(x)(y)a[x,y]−→P is matched up by(y)(x)a[x,y](y)(x)a[x, y].P−→
P . In the two actions the order of the appearancesof (x) and (y) are not the same. This explains the side condition in (ii) of theabove definition.
Theorem 4. The strong bisimilarity is congruent.
In the rest of the section, we introduce some lemmas necessary to the development of the remaining paper.
Lemma 5. Suppose σ is a normal substitution. The following properties hold:(ỹ)α[x̃](ỹ)α[x̃σ](i) If P −→ P 0 and ỹ ∩ (dom(σ) ∪ rng(σ)) = ∅ then P σ −→ P 0 σ.
0
σx̃=
ỹ

0
σx̃σ=
ỹσ

0
0
(ii) If P −→ P 0 then P σ −→ P 0 σσx̃σ=ỹσ
for some chosen σx̃σ=ỹσ.

Proof. Both (i) and (ii) are proved by induction on the height of derivation.
(i) Suppose the last rule applied is Loc2 . By induction hypothesisPσ(ỹ)ασ[x̃σ]

−→

P 0σ

Using the condition {z ỹ}∩(dom(σ)∪rng(σ)) = ∅ one obtains that z ∈ {x̃σ}\{ỹ}and ασ 6∈ {z, z}. Using Loc2 , one has that(z)P σ(z)(ỹ)ασ[x̃σ]

−→

P 0σ

(ii) Suppose the last rule applied is Cmm. By α-convention and (i)PσQσ(ṽ)ασ[x̃σ]

−→

P 0σ

(ũ)ασ[ỹσ]

Q0 σ

−→

By Cmm, one has
0
σx̃σ=
ỹσ

0
0
0
(P |Q)σ ≡ P σ|Qσ −→ (w̃)(P 0 σσx̃σ=ỹσ|Q0 σσx̃σ=ỹσ) ≡ (w̃)(P 0 |Q0 )σσx̃σ=ỹσ
0
σx̃σ=
ỹσ

0
Suppose the last rule applied is Loc1 . Then P σ −→ P 0 σσx̃σ=ỹσ
by induction
0σx̃σ=ỹσ ↑z0
hypothesis. Applying Loc1 one obtains that (z)P σ −→ P 0 σσx̃σ=ỹσ. We are0000
˜
done by observing that σx̃σ=ỹσ ↑z = σx̃0 σ=y˜0 σ for some x̃ and y and some chosen0tu= P 0 σσx̃0 0 σ=y˜0 σ .
σx̃0 0 σ=y˜0 σ . As z 6∈ gn(P 0 σ), P 0 σσx̃σ=ỹσ

The reverse of the above lemma also holds.
Lemma 6. Suppose σ is a normal substitution. The following properties hold:(ỹ)α[x̃](i) If P σ −→ P 0 and ỹ ∩ (dom(σ) ∪ rng(σ)) = ∅ then there exist some α0 , x̃0(ỹ)α0 [x̃0 ]and P1 such that P −→ P1 and α = α0 σ, x̃ = x̃0 σ and P 0 ≡ P1 σ.
σx̃=ỹ
σ1(ii) If P σ −→P 0 is caused by a communication through a local name then P −→P1 for some x̃, ỹ, σx̃=ỹ and P1 such that σ1 = σx̃σ=ỹσ and P 0 ≡ P1 σσx̃σ=ỹσ forsome chosen σx̃σ=ỹσ .
Proof. This is a simple proof by induction on the height of derivation.
τtu[ỹ/x̃]Lemma 7. Suppose a 6∈ gn(P ). If (x̃)(P |a[x̃]) −→ P 0 |a[ỹ] then P −→ P 0 .
τProof. It is obvious that (x̃)(P |a[x̃]) −→ P 0 |a[ỹ] is obtained by applying Loc1[ỹ/x̃][ỹ/x̃]several times. So P |a[x̃] −→ P 0 |a[ỹ], which must follows from P −→ P 0 .

4tu

A Process Calculus without Precedence

Almost all process calculi has prefix operator. But the role of the combinator
has not been clarified. The main objective of having prefix operator is to impose
causal dependency which is important to all computation models. Apart fromusing prefix operator, causality can be achieved by other means such as mobility.
In the rest of the paper we investigate a process calculus without prefix operator.
This model is obtained from the polyadic χ-calculus by simply removing theprefix operator. Its abstract syntax is as follows:
P := α[x̃] | P |P 0 | (x)P | !PThe operational semantics is that of the polyadic χ-calculus minus those concerned with the prefix combinator. In addition one needs th following rule:α[x̃]

α[x̃] −→ 0

Act

where 0 is defined as (a)a[a] for some a of suitable sort.
We will call this language atomic χ-calculus. The set of atomic χ-processes
is denoted by A.
The atomic χ-calculus enjoys some properties not satisfied by the (polyadic)
χ-calculus. For instance the two actions ofa[x,y,z][y/x](w)(a[x, y, z]|(b)(b[x, z]|b[y, w])) −→ −→ 0|(b)(0|0)
can be swapped as[y/x]a[y,y,z](w)(a[x, y, z]|(b)(b[x, z]|b[y, w])) −→ −→ 0|(b)(0|0)
After reordering the two actions are not necessarily the same as the originalones. Some modifications are necessary. But the actions are incurred by thesame components, so to speak, as the original ones. For another example one
notices that(x)(y)a[x,y,z][y/x,y/z]−→(x)(y)(a[x, y, z]|(b)(b[x, z]|b[y, y]))−→0|(b)(0|0)

can be reordered asτ a[z,z,z](x)(y)(a[x, y, z]|(b)(b[x, z]|b[y, y])) −→ −→ 0|(b)(0|0)
The drop of prefix operator allows one to rearrange the order of actions in manyoccasions. The next lemma deals with two situations.
Lemma 8. The following properties hold:σ↑ỹ (y˜0 )α[x̃σ](ỹ)α[x̃] σ(i) If P −→ −→ P 0 and σ −1 (ỹ ∩ rng(σ)) ⊆ ỹ then P −→ −→y˜0 = ỹ \ dom(σ).
(ỹ)α[x̃](y˜0 )α0 [x̃0 ](ii) If P −→ −→and z̃ = ỹ \ {x̃0 }.

P 0 then P

P 0 , where(z˜0 )α0 [x̃0 ](z̃)α[x̃]−→−→ P 0 such that z˜0 = y˜0 ∪ ({x̃0 } ∩ ỹ)

Proof. The proof is carried out by induction on the height of derivation. There
are several cases:– P is α[z̃]. Impossible.
– P is of form P1 |P2 . If the two actions are caused solely by either P1 or P2
individually then apply the induction hypothesis. Otherwise ỹ ∩ (dom(σ) ∪(ỹ)α[x̃](ỹ)α[x̃] σσ

rng(σ)) = ∅. Suppose P1 −→ P10 , P2 −→ P20 and P −→ −→ P 0 is(ỹ)α[x̃]σP ≡ P1 |P2 −→ P10 |P2 −→ P10 σ|P20 ≡ P 0
Thenσ

P ≡ P1 |P2 −→ P1 σ|P20
by Lemma 5.

(ỹ)α[x̃σ]−→ P10 σ|P20 ≡ P 0

– P is of the form (v)P1 . There are several subcases:
1. P(ỹ)α[x̃] σ(ỹ)α[x̃] σ−→ −→ P 0 is caused by P1 −→ −→ P10 such that v 6∈ {x̃} andσ↑ỹ (y˜0 )α[x̃σ]v 6∈ dom(σ) ∪ rng(σ). By induction hypothesis, P1 −→ −→P10 , where˜0σ↑ỹ (y )α[x̃σ]y˜0 = ỹ \ dom(σ). So P −→ −→ P 0 .
(ỹ)α[x̃] σ 0(ỹ)α[x̃] σ

2. P −→ −→ P 0 is caused by P1 −→ −→ P10 such that v 6∈ {x̃}, v ∈dom(σ 0 ) and σ = σ 0 ↑v. By assumption σ −1 (ỹ∩rng(σ)) ⊆ ỹ. So (σ 0 )−1 (ỹ∩rng(σ 0 )) ⊆ ỹv. There are two further subcases:(a) (σ 0 )(v) 6∈ ỹ. Then (σ 0 )−1 (ỹ ∩ rng(σ 0 )) ⊆ ỹ. By induction hypothesis,
0

0

˜0

0

˜0

0

σ ↑ỹ (y )α[x̃σ ]σ ↑ỹ↑v (y )α[x̃σ ]P1 −→ −→ P10 such that y˜0 = ỹ\dom(σ 0 ). Hence P −→ −→P 0 . Now y˜0 = ỹ \ dom(σ 0 ) = ỹ \ dom(σ), σ 0 ↑ỹ↑v = σ 0 ↑v↑ỹ = σ↑ỹ andσ↑ỹ (y˜0 )α[x̃σ]x̃σ 0 = x̃σ as v 6∈ {x̃}. So P −→ −→ P 0 , where y˜0 = ỹ \ dom(σ).
(b) (σ 0 )(v) ∈ ỹ. Suppose (σ 0 )(v) is z. Let σ1 be defined as follows: 0
σ (x) x ∈ dom(σ 0 ) \ (σ 0 )−1 (z)vx ∈ (σ 0 )−1 (z) \ {v}def
σ1 (x) =
v
x=z



x
otherwise(ỹ)α[x̃] σ

1
By Lemma 5, P1 −→ −→P10 [v/z]. Clearly σ −1 (ỹ ∩ rng(σ)) ⊆ ỹ−1
implies that σ1 (ỹ ∩ rng(σ1 )) ⊆ ỹ. It follows by induction thatσ1 ↑ỹ

P1 −→ P100
By Loc0 ,(y˜0 )α[x̃σ1 ]−→P10 [v/z] for some P100 such that y˜0 = ỹ \ dom(σ1 ).
σ1 ↑ỹ

(v)P1 −→ (v)P100(v)(y˜0 )α[x̃σ1 ]−→P10 [v/z]

By α-conversion and Lemma 5, one obtains
σ1 ↑ỹ

(v)P1 −→ (z)P100 [z/v](z)(y˜0 )α[x̃σ 0 ]

−→

P10

Now σ↑ỹ = (σ 0 ↑v)↑ỹ = σ1 ↑ỹ and x̃σ 0 = x̃σ. Thereforeσ↑ỹ (z)(y˜0 )α[x̃σ](v)P1 −→−→

P10

It also follows from y˜0 = ỹ \ dom(σ1 ) that z y˜0 = ỹ \ dom(σ).
˜0(ỹ)α[x̃] σ(y )α[x̃] σ
3. P −→ −→ P 0 is caused by P1 −→ −→ P 0 such that ỹ = y˜0 v andv 6∈ dom(σ) ∪ rng(σ). The assumption σ −1 (ỹ ∩ rng(σ)) ⊆ ỹ and thecondition v 6∈ dom(σ) ∪ rng(σ) imply that σ −1 (y˜0 ∩ rng(σ)) ⊆ y˜0 . Byσ↑y˜0 (y˜00 )α[x̃σ]induction hypothesis P1 −→ −→σ↑y˜0 (v)(y˜00 )α[x̃σ]P 0 such that y˜00 = y˜0 \ dom(σ). So

P 0 . Clearly v y˜00 = v y˜0 \ dom(σ) = ỹ \ dom(σ).
(ỹ)α[x̃] σ(y˜0 )α[x̃] σ
4. P −→ −→ P 0 is caused by P1 −→ −→ P 0 such that ỹ = y˜0 v and v ∈dom(σ). By assumption σ −1 (ỹ ∩ rng(σ)) ⊆ ỹ. So σ −1 (y˜0 ∩ rng(σ)) ⊆ ỹ.
The rest of the proof is similar to the subcase 2.
(v)P1 −→−→

(y˜0 )α[x̃] σ(ỹ)α[x̃] σ

5. P −→ −→ P 0 is caused by P1 −→ −→ P 0 such that ỹ = y˜0 v andv ∈ rng(σ). The assumption σ −1 (ỹ ∩ rng(σ)) ⊆ ỹ implies σ −1 (y˜0 ∩σ↑y˜0 (y˜00 )α[x̃σ]rng(σ)) ⊆ y˜0 . By induction hypothesis P1 −→ −→ P 0 such thaty˜00 = y˜0 \ dom(σ). It follows from the assumption σ −1 (ỹ ∩ rng(σ)) ⊆ ỹ˜0˜00σ↑y (v)(y )α[x̃σ]that v 6∈ dom(σ↑y˜0 ) ∪ rng(σ↑y˜0 ). So (v)P1 −→ −→P 0 . That isσ↑y˜0 v (v)(y˜00 )α[x̃σ](v)P1 −→

P 0 . It is clear that v y˜00 = y˜0 v \ dom(σ).

−→(ỹ)α[x̃] σ– P is of the form !P1 . Then P1 |!P1 −→ −→ P 0 and σ −1 (ỹ ∩ rng(σ)) ⊆ ỹ.
σ↑ỹ (y˜0 )α[x̃σ]By induction hypothesis P1 |!P1 −→ −→σ↑ỹ (y˜0 )α[x̃σ]Therefore P −→ −→P 0 such that y˜0 = ỹ \ dom(σ).

P 0.

This completes the proof of (i).
(ii) The proof is similar.

tu(ỹ)α[x̃] ττ (ỹ)α[x̃]Corollary 9. If P −→ −→ P 0 then P −→ −→ P 0 .
tu

Proof. This is a special case of Lemma 8.
(x)a[x] a[y]τ

In polyadic χ-calculus P −→ −→ P 0 does not imply P −→ P 0 [y/x]. Takefor example P to be (x)a[x].a[y]. In the atomic χ-calculus however one can(x)a[x] a[y]τ

conclude P −→ P 0 [y/x] from P −→ −→ P 0 . This is one of the virtues of working
τwithout prefix operator. On the other hand if the communication P −→ P 0 takes
place through a global name a then it can be decomposed as it were into two
output actions with both subject names being a. The next lemma generalizes
this observation to updates.
Lemma 10. The following properties hold:(i) If P(ũ)a[x̃](ṽ)a[ỹ]−→ P1 −→ P10 then there exist some w̃, σx̃=ỹ and P 0 such thatσx̃=ỹ ↑ũṽ

P −→ P 0 , (w̃)(P10 σx̃=ỹ ) ∼ P 0 , w̃ = rng(σx̃=ỹ ) ∩ ũṽ and (σx̃=ỹ )−1 (w̃) ⊆ ũṽ.
σ(ii) If P −→ P 0 is caused by a communication through a global name a then(ũ)a[x̃](ṽ)a[ỹ]

there exist some x̃, ỹ, ũ, ṽ, w̃, σx̃=ỹ , P1 and P10 such that P −→ P1 −→ P10 ,σ = σx̃=ỹ ↑ũṽ, (w̃)(P10 σx̃=ỹ ) ∼ P 0 , w̃ = rng(σx̃=ỹ ) ∩ ũṽ and (σx̃=ỹ )−1 (w̃) ⊆ ũṽ.
(ũ)a[x̃](ṽ)a[ỹ]Proof. Suppose P −→ P1 −→ P10 . We prove by induction on the height ofderivation.
– P is of the form α[z̃]. This case is impossible.
(ũ)a[x̃](ṽ)a[ỹ]σx̃=ỹ ↑ũṽ

– P is of the form A1 |A2 . If A1 −→ −→ A01 then A1 −→ A0 for somechosen σx̃=ỹ and A0 and (w̃)(A01 σx̃=ỹ ) ∼ A0 for some w̃ such that w̃ =rng(σx̃=ỹ ) ∩ ũṽ and (σx̃=ỹ )−1 (w̃) ⊆ ũṽ. Then A1 |A2Therefore

σx̃=ỹ ↑ũṽ

−→A0 |A2 σx̃=ỹ ↑ũṽ.

A0 |A2 σx̃=ỹ ↑ũṽ ∼ (w̃)(A01 σx̃=ỹ )|A2 σx̃=ỹ ↑ũṽ ∼ (w̃)(A01 σx̃=ỹ |A2 σx̃=ỹ )because ũṽ ∩ gn(A2 ) = ∅.

(ũ)a[x̃](ṽ)a[ỹ](ũ0 )a[x̃](ṽ)a[ỹ]– P is of the form A1 |A2 and the two consecutive actions P −→ P1 −→ P10
are performed by A1 and A2 respectively. We are done by applying Cmm.
– P is of the form (z)A and z 6∈ x̃ỹ. This case is simple.
– P is of the form (z)A and z ∈ x̃. Let ũ0 be ũ \ z. Then A −→ P1 −→ P10 .
σx̃=ỹ ↑ũ0 ṽ

By induction hypothesis, A −→ P 0 and (w̃)(P10 σx̃=ỹ ) ∼ P 0 for some chosen σx̃=ỹ and for some w̃ such that w̃ = rng(σx̃=ỹ ) ∩ ũṽ and (σx̃=ỹ )−1 (w̃) ⊆ũṽ. There are two subcases:
σx̃=ỹ ↑ũṽ(ũ)a[x̃](ṽ)a[ỹ]• z ∈ dom(σx̃=ỹ ). Then P −→ P1 −→ P10 and P −→ P 0 . There isnothing more to be proved.
(ũ)a[x̃]σx̃=ỹ ↑ũṽ(ṽ)a[ỹ]• z ∈ rng(σx̃=ỹ ). Then P −→ P1 −→ P10 and P −→ (z)P 0 . Now
clearly (w̃z)(P10 σx̃=ỹ ) ∼ (z)P 0 . So this case is fine as well.
– P is of the form (z)A and z ∈ ỹ. The situation is similar to the above case.
– P is of the form !P1 . Use induction hypothesis.
σSuppose P −→ P 0 is caused by a communication through a global name a.
The the following proof goes by structural induction.
– P is of the form α[z̃]. This case is impossible.
– P is of the form A1 |A2 . If the update action is caused solely by either A1or A2 , then apply induction hypothesis. If the update action is caused by(ũ)a[x̃](ṽ)a[ỹ]A1 −→ A01 and A2 −→ A02 , then ũ ∩ ṽ = ∅ by α-convention. We are done
by applying Cmm-rule.
– P is of the form (z)A1 . There are two subcases:σσ• If P −→ P 0 is obtained from A1 −→ A01 such that P ≡ (z)A1 , P 0 ≡ (z)A01
and z 6∈ dom(σ) ∪ rng(σ). By induction hypothesis, there exist some a,(ũ)a[x̃](ṽ)a[ỹ]x̃, ỹ, ũ, ṽ, w̃, σx̃=ỹ , B1 and B10 such that A1 −→ B1 −→ B10 , σ =σx̃=ỹ ↑ũṽ, (w̃)(B10 σx̃=ỹ ) ∼ A01 , w̃ = rng(σx̃=ỹ ) ∩ ũṽ and (σx̃=ỹ )−1 (w̃) ⊆(ũ)a[x̃](ṽ)a[ỹ]ũṽ. It follows that P −→ (z)B1 −→ (z)B10 and(w̃)((z)B10 σx̃=ỹ ) ∼ (z)A01 ≡ P 0
σ0σ• If P −→ P 0 is obtained from A1 −→ P 0 such that P ≡ (z)A1 , z ∈dom(σ 0 ) and σ = σ 0 ↑z. By induction hypothesis, there exist some a, x̃, ỹ,(ũ)a[x̃](ṽ)a[ỹ]ũ, ṽ, w̃, σx̃=ỹ , B1 and B10 such that A1 −→ B1 −→ B10 , σ 0 = σx̃=ỹ ↑ũṽ,(w̃)(B10 σx̃=ỹ ) ∼ P 0 , w̃ = rng(σx̃=ỹ ) ∩ ũṽ and (σx̃=ỹ )−1 (w̃) ⊆ ũṽ. Then(z)(ũ)a[x̃](ṽ)a[ỹ](ũ)a[x̃](z)(ṽ)a[ỹ]either P −→ B1 −→ B10 or P −→ (z)B1 −→ B10 . In eithercase σ = σ 0 ↑z = σx̃=ỹ ↑ũṽz. It is also obvious that w̃ = rng(σx̃=ỹ ) ∩ ũṽzand (σx̃=ỹ )−1 (w̃) ⊆ ũṽz.
– P is of the form !P1 . Use induction hypothesis.
This completes the proof.

tu

The next lemma spells out another property enjoyed by atomic χ-calculus.
It is not satisfied by the polyadic χ-calculus.

(ỹ)α[x̃]Lemma 11. If P −→ P 0 then P ∼ (ỹ)(α[x̃]|P 0 ).
Proof. The proof is carried out by structural induction.
– P is of the form α[x̃]. Then P ∼ α[x̃]|0 ≡ α[x̃]|P 0 .
(ỹ)α[x̃]– P is of the form P1 |P2 and P −→ P 0 is caused by P1
induction hypothesis P1 ∼ (ỹ)(α[x̃]|P10 ). Hence(ỹ)α[x̃]−→ P10 . By

P ∼ (ỹ)(α[x̃]|P10 )|P2 ∼ (ỹ)(α[x̃]|(P10 |P2 ))(ỹ)α[x̃](ỹ)α[x̃]– P is of the form (z)P1 . If P −→ P 0 is caused by P1 −→ P10 such that z 6∈x̃. Then P 0 ≡ (z)P10 and P1 ∼ (ỹ)(α[x̃]|P10 ). Therefore P ∼ (z)(ỹ)(α[x̃]|P10 ) ∼(ỹ)α[x̃](y˜0 )α[x̃](ỹ)(α[x̃]|(z)P10 ) ≡ (ỹ)(α[x̃]|(z)P 0 ). If P −→ P 0 is caused by P1 −→ P 0such that z ∈ x̃ and ỹ = z y˜0 . Then P1 ∼ (y˜0 )(α[x̃]|P 0 ). Consequently P ∼(ỹ)(α[x̃]|P 0 ).
(ỹ)α[x̃]– P is of the form !P1 . Then P1 |!P1 −→ P 0 . So P ∼ P1 |!P1 ∼ (y˜0 )(α[x̃]|P 0 ).
This completes the proof.

5tu

Ground Bisimilarity for Atomic χ-Calculus

In the study of asynchronous π-calculus it was observed that ground bisimilarity is closed under substitution and therefore is a congruence relation. This issignificant in view of the fact that the ground bisimilarity for the π-calculus is
not closed under substitution. This closure property is essentially due to threefacts for the asynchronous language. The first is that a communication througha global name can be decomposed into an output action followed immediately
by an input action. The second is that the ability to communicate through a
local name is not affected by substitution. And the third is the property thatδδσP −→ P 0 implies P σ −→ P 0 σ for all substitution σ. All the three properties
hold of the atomic χ-calculus. Therefore it should not come as a surprise thatstrong bisimilarity is equivalent to its ground counterpart. Compared with thesituation in the asynchronous π-calculus, additional attention should be paid to
update actions in atomic χ-calculus.
Definition 12. Suppose R is a symmetric binary relation on A. The relation R
is a strong ground bisimulation if whenever P RQ then the following propertieshold:
σx̃=ỹ
(i) If P −→ P 0 (including the case when σx̃=ỹ = τ ) then some Q0 exists suchσx̃=ỹ
that Q −→ Q0 RP 0 .
(ỹ)α[x̃](y˜0 )α[x̃](ii) If P −→ P 0 then some Q0 exists such that Q −→ Q0 RP 0 and {ỹ} = {y˜0 }.
The strong ground bisimilarity, notation ∼g , is the largest strong ground bisimulation.
The next result is crucial to axiomatization of the strong bisimilarity.

Theorem 13. ∼g is the same as ∼.
Proof. It is obvious that ∼⊆∼g . For the reverse inclusion we prove thatdef

R = {(P σ, Qσ) | P ∼g Q and σ is a substitution}
is a strong bisimulation. Since a substitution is the composition of a finite numberof normal substitutions, we may consider normal substitutions only. SupposeP ∼g Q and σ is a normal substitution. There are three cases:(ỹ)a[x̃]– P σ −→ P 0 . By Lemma 10, there must exist some b, x̃0 and P1 such that(ỹ)b[x̃0 ]P −→ P1 , bσ = a, x̃0 σ = x̃ and P1 σ = P 0 . By definition some Q1 and y˜0
˜0

˜0

0

(y )b[x̃ ](y )a[x̃]
exist such that Q −→ Q1 ≈g P1 and {ỹ} = {y˜0 }. By Lemma 5, Qσ −→Q1 σ.
σ1P 0 is caused by an interaction through global name a. By Lemma 10,– P σ −→(ũ)a[x̃](ṽ)a[ỹ]

there exist some x̃, ỹ, ũ, ṽ, w̃, σx̃=ỹ , P1 and P10 such that P σ −→ −→ P10 ,σ1 = σx̃=ỹ ↑ũṽ, (w̃)(P10 σx̃=ỹ ) ∼ P 0 , w̃ = rng(σx̃=ỹ ) ∩ ũṽ and (σx̃=ỹ )−1 (w̃) ⊆(ũ)a0 [x̃0 ](ṽ)a00 [y˜0 ]ũṽ. It follows from Lemma 6 that P −→ −→ A01 for some a0 , a00 , x̃0 andy˜0 such that x̃0 σ = x̃, y˜0 σ = ỹ, a = a0 σ = a00 σ and P10 ≡ A01 σ. By definition(ũ)a0 [x̃0 ](ṽ)a00 [y˜0 ]some ũ0 , v˜0 , B1 and B10 exist such that Q −→ −→ B10 ∼g A01 , {ũ} =(ũ)a[x̃](ṽ)a[ỹ]{ũ0 } and {ṽ} = {v˜0 }. Using Lemma 5 one gets that Qσ −→ −→ B10 σ. By
σx̃=ỹ ↑ũṽ

Lemma 9, Qσ −→ Q0 for some Q0 such that Q0 ∼ (w̃)(B10 σσx̃=ỹ ). Noticethat P 0 ∼ (w̃)(A01 σσx̃=ỹ ) ≡ (w̃)(P10 σx̃=ỹ ).
σ1– P σ −→
P 0 is caused by an interaction through a local name. By Lemma 6,σx̃=ỹ
P −→ P1 for some σx̃=ỹ and P1 such that σx̃σ=ỹσ = σ1 and P1 σσx̃σ=ỹσ ≡ P 0 .
σx̃=ỹ
By definition some Q1 exists such that Q −→ Q1 ∼g P1 . By (iii) of Lemma 5,σx̃σ=ỹσQσ −→ Q1 σσx̃σ=ỹσ .
Conclude that R is a strong bisimulation up to ∼ and localization. It is theneasy to show that R is included in the strong bisimilarity.
tuSimilarly one can introduce strong asynchronous ground bisimilarity. Thisbisimilarity formalizes the intuition that (x̃)(a[x̃]|a[x̃]) should be equivalent to(a)(x̃)(a[x̃]|a[x̃]).
Definition 14. Suppose R is a symmetric binary relation on A. The relation R
is a strong asynchronous ground bisimulation if it satisfies the following property:σσ(i) If P −→ P 0 then Q0 exists such that Q −→ Q0 RP 0 .
(ỹ)α[x̃](y˜0 )α[x̃](ii) If P −→ P 0 and |ỹ| < |x̃| then Q0 and y˜0 exist such that Q −→ Q0 RP 0
and {ỹ} = {y˜0 }.
(ỹ)α[x̃](iii) If P −→ P 0 and |ỹ| = |x̃| then Q0 exists such that one of the following
properties holds:

˜0(y )α[x̃]– y˜0 exist such that Q −→ Q0 RP 0 and |y˜0 | = |x̃|.
α[x̃]

τ

– Q −→ Q0 and some P 00 exists such that P 0 −→ P 00 RQ0 .
The strong asynchronous ground bisimilarity, notation ∼ag , is the largest strong
asynchronous ground bisimulation.
Theorem 15. ∼ag is closed under substitution.
Proof. The proof is similar to that of Theorem 13.

tu

It follows that ∼ag is a congruence relation. If in Definition 14 we have required
the relation to be closed under substitution we would get strong asynchronousbisimilarity ∼a . Theorem 15 says that the strong asynchronous bisimilarity is
the same as the strong asynchronous ground bisimilarity.

6

Axiomatization in the Absence of Prefix, Summationand Match Combinators

The problems of axiomatization for equivalences on mobile processes are much
more interesting than those in CCS. Extra effort is necessary to deal with mobility in an interleaving scenario. For that purpose match combinator is introducedin π-calculus. Together with the prefix and the summation combinators, thematch operator retains the mobility when converting a concurrent process to anondeterministic process. All the three operators, prefix, summation and match
combinators, play crucial role in axiomatic treatment of π-calculus.
In [2] the authors have given a complete system for strong ground bisimilarity
on finite asynchronous π-processes. The axiomatization uses restricted forms ofprefix and summation operators. The match operator is not necessary.
In this section we make an initial step towards an axiomatic theory of atomic
χ-calculus. We will be focusing on the strong bisimilarity and strong asynchronous bisimilarity. Our treatment is novel in that it uses none of the prefixcombinator, the summation combinator and the match combinator.
Let P1 , . . . , Pn be n atomic χ-processes. We will write
n
Y
i=1

Pi or

Y

Pi

i∈{1,...,n}Qnfor (. . . ((P1 |P2 )|P3 ) . . .)|Pn . When n = 0, i=1 Pi is just 0. We say that x̃
are the global name occurrences in P if the sequence of all the occurrencesof global names appeared in P from left to right is x̃. We say that x̃ are thelocal name occurrences in P if the sequence of all the occurrences of local
names appeared in P from left to right is x̃. Local name occurrences ignore
the names appeared in localization operators. For instance the global name occurrences of (x)(a[x]|(y)(a[y]|c[c, x])) are aacc and the local name occurrences

of (x)(a[x]|(y)(a[y]|c[c, x])) are xyx. Suppose x˜1 , . . . , x˜n are the global name occurrences in P1 , . . . , Pn respectively and b˜1 , . . . , b˜n are the local name occurrences in P1 , . . . , Pn respectively. Suppose further that z˜1 , . . . , z˜n and d˜1 , . . . , d˜nare pairwise distinct fresh names such that |z˜1 | = |x˜1 |, . . . , |z˜n | = |x˜n | and|d˜1 | = |b˜1 |, . . . , |d˜n | = |b˜n |. Let c˜i , for each i ∈ {1, . . . , n}, be obtained fromb˜i by removing repetitive occurrences. It follows that {c˜i } = {b˜i } and c˜i are
pairwise distinct. Abbreviate x˜1 . . . x˜n , b˜1 . . . b˜n , z˜1 . . . z˜n , d˜1 . . . d˜n and c˜1 . . . c˜nby x̃, b̃, z̃, d˜ and c̃ respectively. Let v˜1 , . . . , v˜n and w˜1 , . . . , w˜n be sequences ofnames such that |v˜1 | = |w˜1 |, . . . , |v˜n | = |w˜n | andPlet v˜1 . . . v˜n , w˜1 . . . w˜n be abbren
viated respectively by ṽ and w̃. We will write i=1 [v˜i =w̃i ].Pi for the following
atomic χ-process:(e)(a)(nY˜(z̃)(d)(a[ez̃d˜w˜1 . . . wi−1
˜ v˜i wi+1
˜ . . . w˜n ]|Pi [z˜i d˜i ])|(c̃)a[ex̃b̃w̃])i=1where e is a fresh name, a is fresh with suitable sort and Pi [z˜i d˜i ], for i ∈{1, . . . , n}, is Pi obtained by removing all the localization operators in Pi andreplacing the global name occurrences x̃i by z˜i and local name occurrences b˜i byd˜i . Let’s see one example. Suppose P1 is (a)(z)(a[x]|(a[z]|b[b])) and P2 is c[y]|d[d].
P2Suppose further that v˜1 = b, w˜1 = c, v˜2 = cd and w˜2 = ef . Then i=1 [v˜i =w̃i ].Pi
denotes the following process(t)(s)(((z̃)(b̃)(s[tz̃bef ]|b1 [z1 ]|(b2 [b3 ]|z2 [z3 ]))|(z̃)(s[tz̃ccd]|(z4 [z5 ]|z6 [z7 ])))|A)
where A stands for (a)(z)s[txbbcyddaazcef ], z̃ stands for z1 z2 z3 z4 z5 z6 z7 and b̃
stands for b1 b2 b3 .
Pn
We call [v˜i =w̃i ].Pi a summand of i=1 [v˜i =w̃i ].Pi and [v˜i =w̃i ] an update prefix and Pi the corresponding continuation. We call [v˜i =w̃i ] a P
tau prefix, writtennτ , if both v˜i and w̃i are empty. When n = 1 we abbreviate i=1 [v˜i =w̃i ].Pi to[v˜1 =w˜1 ].P1 , which will be further abbreviated to [v˜1 =w˜1 ] if P1 is 0.
Pn
The reason to introduce a lot of fresh names in i=1 [v˜i =w̃i ].Pi is to makesure thatnX
σv˜i =w˜i∼g Pi σv˜i =w̃i[v˜i =w̃i ].Pi −→i=1

Pn

and that i=1 [v˜i =w̃i ].Pi can not perform
Pn any other actions. To conform to thestandard notation we will often write i=1 [v˜i =w̃i ].Pi alternatively as[v˜1 =w˜1 ].P1 + . . . + [v˜n =w˜n ].Pn
We write . . . +P
Pi + . . . for instance when we want to emphasize particularnsummand(s) of i=1 [v˜i =w̃i ].Pi .
For update prefix [ṽ=w̃] let [(ṽ=w̃) \ x] denote any update prefix [ỹ=z̃] suchthat ∀a, b.(a 6= x) ∧ (b 6= x) ⇒ ((ṽ=w̃ ⇒ a = b) ⇔ (ỹ=z̃ ⇒ a = b)). For example[(xy=yw) \ y] can be [x=w].

E1
P =P
E2
P = Q if Q = P
E3
P = R if P = Q and Q = R
E4
P |R = Q|R if P = Q
E5(x)P = (x)Q if P = Q
C1
P |0 = P
C2
P |Q = Q|PC3
P |(Q|R) = (P |Q)|R
L1(x)0 = 0L2(x)(y)P = (y)(x)P
L3(x)(P |Q) = P |(x)Q if x 6∈ gn(P )S1 . . . +[ṽ=w̃].P +[v˜0 =w̃0 ].P 0 + . . . = . . . +[v˜0 =w̃0 ].P 0 +[ṽ=w̃].P + . . .
S2 . . . +[ṽ=w̃].P +[ṽ=w̃].P + . . . = . . . +[ṽ=w̃].P + . . .
S3. . . +[ṽ=w̃].P + . . . = . . . +[ṽ=w̃].P [wi /vi ]+ . . .
if vi is the i-th component of ṽ and wi is thei-th component of w̃
S4. . .P+[ṽ=w̃].P + . . . = P. . . +[v˜0 =w̃0 ].P + . . . if ṽ=w̃ ⇔ v˜0 =w̃0nnS5(x) i=1 [v˜i =w̃i ].Pi = i=1 [(v˜i =w̃i ) \ x].(x)Pi [xi /x]
where, for each i ∈ {1, . . . , n}, v˜i =w̃i ⇒ x = xi
and xi = x only if ∀y.y 6= x ⇒ (v˜i =w̃i 6⇒ x = y)A(x̃)(a[x̃]|a[x̃]) = τ
Fig. 1. Axioms for ∼g and ∼ag

Let ASA be the set of axioms given in Figure 1 together with the following
expansion law
(x̃)(

Y

αi [v˜i ]) = (x̃)

1≤i<j≤nXαi =αji∈{1,...,n}Y[v˜i =v˜j ].

αk [v˜i ]k∈{1,...,n}\{i,j}where for each i ∈ {1, . . . , n} either αi ∈ x̃ or αi ∈ x̃. Let AS be ASA \ {A}. We
will write AS ` P = Q to mean that the equality P = Q is derivable from therules and axioms of AS. When no confusion arises, we simply write P = Q. We
R
will also write P = Q to indicate that R is the major axiom applied to derive
P = Q. The meaning of ASA ` P = Q is similar.
(ỹ)α[x̃]

Lemma 16. If P is finite and P −→ P 0 then AS ` (ỹ)(α[x̃]|P 0 ) = P .
Proof. This is a simple proof by structural induction.
A process P is in normal form if it is of the form
(x̃)(

n
Y

i=1

αi [b˜i ]|

m
X
j=1

such that the following conditions hold:[v˜j =w̃j ].Pj )tu1. Each Pj , for 1 ≤ j ≤ m, is in normal form.
Qn
2. x̃ ⊆ gn( i=1 αi [b˜i ]).
3. There is an enumeration i1 , . . . , in of {1, . . . , n} such that
(x̃)(

n
Y

αi [b˜i ]|

i=1

m
X

[v˜j =w̃j ].Pj )(y˜1 )αi1 [b˜
i1 ]

−→

...

(y˜n )αin [bi˜n ]

−→

∼g

m
X

[v˜j =w̃j ].Pj

j=1

j=1

for some y˜1 , . . . , y˜n with x̃ = y˜1 . . . y˜n . When |x̃| = 0 and m = n = 0 the normal
form is 0.
Lemma 17. Every finite atomic χ-process is provably equal in AS to a normal
form process.
(y˜1 )α1 [b1 ](y˜n )αn [bn ]Proof. Suppose P is a finite atomic χ-process. Then P −→ . . . −→ P 0 ,for n ≥ 0, such that all subject names in P 0 are local. By (ii) of Lemma 8 theprocess P 0 is not affected if (y˜1 )α1 [b1 ], . . . , (y˜n )αn [bn ] are performed in a different
order as long as it is legal. By C-axioms, L-axioms and Lemma 16, one derivesthatAS ` P = (y˜1 . . . y˜n )(α1 [b˜1 ]| . . . |αn [b˜n ]|P 0 )When y ∈ {y˜1 . . . y˜n } \ gn(α1 [b˜1 ]| . . . |αn [b˜n ]), we can use the L-laws and S5 topush (y) inwards. So we may assume that {y˜1 . . . y˜n } ⊆ gn(α1 [b˜1 ]| . . . |αn [b˜n ]).
Apply the expansion law and S5 to P 0 , one gets
AS ` P = (y˜1 . . . y˜n )(nYαi [b˜i ]|mX[v˜j =w̃j ].Pj )

j=1

i=1

For each j ∈ {1, . . . , m}, Pj is structurally simpler than P . So we can use induction hypothesis on Pj .
tu
We are now in a position to prove completeness theorems.
Theorem 18. AS is sound and complete for ∼g .
Proof. The soundness can be easily verified. Suppose P ∼g Q. By Lemma 17,
we can assume that both P and Q are in normal form. Let P be
(x̃)(

n
Y

αi [b˜i ]|

i=1

m
X

[v˜j =w̃j ].Pj )j=1

and Q be0

(x̃0 )(nY0αi0 [b˜0i ]|

i=1

m
X

[v˜j0 =w̃j0 ].Qj )j=1

By definition there is an enumeration i1 , . . . , in of {1, . . . , n} such that
(x̃)(

n
Y

i=1

αi [b˜i ]|

m
X
j=1

[v˜j =w̃j ].Pj )(y˜1 )αi1 [b˜
i1 ]

−→

...

(y˜n )αin [bi˜n ]

−→

=

m
X
j=1

[v˜j =w̃j ].Pj

for some y˜1 , . . . , y˜n with x̃ = y˜1 . . . y˜n . Now Q has to match up the above sequenceof actions by0(x̃0 )(nY00αi0 [b˜0i ]|

i=1

m
X

˜0

˜

˜

˜0

(y )αi1 [bi1 ](y )αin [bin ]. . . n −→=[v˜j0 =w̃j0 ].Qj ) 1 −→mX[v˜j0 =w̃j0 ].Qj

j=1

j=1

Pm
Pm0 ˜00˜0such that j=1 [v˜j =w̃j ].Pj ∼g
j=1 [vj =w̃j ].Qj and {yi } = {y˜i } for each i ∈{1, . . . , n}. This says that by using C-laws, L-laws and α-conversion one canrewrite Q asnm0YX(x̃)( αi [b˜i ]|[v˜j0 =w̃j0 ].Qj )
i=1

j=1

So we only have to show that
AS `

m
X

0

[v˜j =w̃j ].Pj =

j=1

m
X

[v˜j0 =w̃j0 ].Qj

(1)

j=1

Now for each j ∈ {1, . . . , m} one has thatmX

σv˜j =w˜j[v˜j =w̃j ].Pj −→ = Pj σv˜j =w˜j

(2)

j=1

for any chosen σv˜j =w˜j . To match up there must exist some j 0 ∈ {1, . . . , m0 } suchthatm0
σv˜0 =w˜0
Xjj[v˜j0 =w̃j0 ].Qj −→ = Qj 0 σv˜0 =w˜0 ∼g Pj σv˜j =w˜j
j0

j=1

j0

and σv˜0 =w˜0 = σv˜j =w˜j . The latter implies v˜j0 0 =w˜j0 0 ⇔ v˜j =w̃j . It is clear thatj0

j0

Pj σv˜j =w˜j and Qj 0 σv˜0 =w˜0 are structurally simpler than P and Q respectively.
j0

j0

By induction hypothesis
AS ` Pj σv˜j =w˜j = Qj 0 σv˜0 =w˜0
j0

j0

Now
0

m
X

[v˜j0 =w̃j0 ].Qj ≡ . . . + [v˜j0 0 =w˜j0 0 ].Qj 0 + . . .

j=1
S3= . . . + [v˜j0 0 =w˜j0 0 ].Qj 0 σv˜0 =w˜0 + . . .
j0

j0= . . . + [v˜j0 0 =w˜j0 0 ].Pj σv˜j =w˜j + . . .
S4= . . . + [v˜j =w̃j ].Pj σv˜j =w˜j + . . .

S3= . . . + [v˜j =w̃j ].Pj + . . .

Pm0For each j ∈ {1, . . . , m} we consider all the summands of j=1 [v˜j0 =w̃j0 ].Qj thatcan match the action in (2) and carry out the transformation. In this way we
Pm0
can rewrite j=1 [v˜j0 =w̃j0 ].Qj into a form each of its summands is syntacticallyPmidentical to a summand of j=1 [v˜j =w̃j ].Pj . Then use S1 and S2 to get (1). ut
Theorem 19. ASA is sound and complete for ∼ag .
Proof. Suppose P ∼ag Q. Let P be
(x̃)(

n
Y

m
X

αi [b˜i ]|i=1[v˜j =w̃j ].Pj )j=1

and Q be0

(x̃0 )(nY0αi0 [b˜0i ]|

i=1

If
(x̃)(

n
Y

m
X

[v˜j0 =w̃j0 ].Qj )j=1

αi [b˜i ]|

i=1

m
X

(b˜0 )α[b˜i ]i[v˜j =w̃j ].Pj ) −→P0

j=1

where {b˜0i } = {b˜i } and |b˜0i | = |b˜i |, is matched up by0(x̃0 )(nY0αi0 [b˜0i ]|

i=1

m
X

τ

[v˜j0 =w̃j0 ].Qj ) −→ Q0

j=1

for some Q0 such thatα[b˜i ]

P 0 −→ P 00 ∼ag Q0
Then b˜i ∩ gn(Q0 ) = ∅ and b˜i ∩ gn(P 00 ) = ∅ for otherwise P 00 can perform asequence of actions which Q0 can not simulate. Using L-laws, one shows thatAS ` P = (b˜i )(α[b˜i ]|α[b˜i ])|P1
for some normal form process P1 . Consequently
ASA ` P = τ |P1
by induction hypothesis. If on the other hand
(x̃)(

n
Y

αi [b˜i ]|

i=1

m
X

(b˜0 )α[b˜i ]α[b˜i ]i[v˜j =w̃j ].Pj ) −→P 0 −→ P 00

j=1

such that b˜i ∩ gn(P 00 ) 6= ∅, then by the above analysis
(x̃)(

n
Y

i=1

αi [b˜i ]|

m
X
j=1

(b˜0 )α[b˜i ]i[v˜j =w̃j ].Pj ) −→P0

(3)

must be simulated by0(x̃0 )(nY0αi0 [b˜0i ]|

i=1

m
X

[v˜j0 =w̃j0 ].Qj )(b˜00)α[b˜i ]
i

−→

Q0

j=1

for some Q0 and b˜00i such that {b˜00i } = {b˜i } and |b˜00i | = |b˜i |.
To continue observe that, by expansion law,
ASA ` τ |mX[v˜j =w̃j ].Pj =

j=1

m
X

[v˜j =w̃j ].(τ |Pj ) + τ.

j=1

m
X

[v˜j =w̃j ].Pj

j=1

Here the right hand side stands for
m+1
X[v˜j0 =w̃j0 ].Pj0

j=1
0˜
0˜
are empty
and wm+1
where v˜j0 = v˜j , w̃j0 = w̃j , Pj0 ≡ Pj , for j ∈ {1, . . . , m}, vm+1
Pm
sequence, and Pm+1 is j=1 [v˜j =w̃j ].Pj . So we can now assume that P is of thenormal formnmYX(x̃)( αi [b˜i ]|[v˜j =w̃j ].Pj )
i=1

j=1

such that b˜i ∩ gn(P 00 ) 6= ∅ whenever (3) holds. Similar assumption can be madefor Q.
The rest of the proof is similar to that of Theorem 18.
tu7

Final Remarks

The popular way of defining the operational semantics of the Fusion Calculus is
to impose a structural congruence on processes. This approach makes it easy todefine communications. In this paper we have adopted a pure labeled transition
semantics. In our view this latter approach simplifies rather than complicatesthe algebraic investigation.
Complete systems for weak congruences are much more difficult than thosefor strong congruences. In CCS ([14, 17]) it is well known that complete system
for weak equivalence can be obtained from that for strong equivalence by adding
three famous tau laws of Milner’s. For some time it had been conjectured thatthe situation in π-calculus is similar. It was pointed out recently by the present
author ([10]) however that in general Milner’s tau laws fail to lift a complete
system for a strong congruence on finite mobile processes to a complete system
for the corresponding weak congruence. A fourth tau law is necessary to deal
with mobility. Axiomatization for asynchronous π-calculus is more difficult thanfor π-calculus. Weak congruence for finite asynchronous π-processes has not beenaxiomatized. As atomic χ-calculus shares properties with the asynchronous πcalculus one expects that its axiomatization problem for weak congruence isequally difficult. This seems to be the most important question about atomic
χ-calculus. Until we have answered this question, we can’t really say that weunderstand the algebraic theory of the calculus.
Acknowledgement The author is supported by the NNSFC (69873032), the863 Hi-Tech Project (863-306-ZT06-02-2), the Young Scientist Research Fundand the University Scholar Funding Scheme. He is also supported by BASICS,
Center of Basic Studies in Computing Science, sponsored by Shanghai Education
Commission. BASICS is affiliated to the Department of Computer Science of
Shanghai Jiaotong University.

References
1. S. Abramsky, Proofs as Processes, Theoretical Computer Science, 135, 5–9, 1994.
2. R. Amadio, I. Castellani, D. Sangiorgi. On Bisimulation for the Asynchronous πCalculus. CONCUR’96 , Lecture Notes in Computer Science 1119, Springer, 1996.
3. G. Boudol. Asynchrony and the π-calculus. Research Report 1702, INRIA, SophiaAntipolis, 1992.
4. Y. Fu. The χ-Calculus. Proceedings of the International Conference on Advances
in Parallel and Distributed Computing, 74-81, March 19th-21th, Shanghai, IEEE
Computer Society Press, 1997.
5. Y. Fu. A Proof Theoretical Approach to Communications. ICALP’97 , 325–335,
July 7th-11th, Bologna, Italy, Lecture Notes in Computer Science 1256, Springer,
1997.
6. Y. Fu. Symmetric π-Calculus. Journal of Computer Science and Technology, 13:
202–208, 1998.
7. Y. Fu. Reaction Graphs. Journal of Computer Science and Technology, 13: 510–
530, 1998.
8. Y. Fu. Bisimulation Lattice of Chi Processes. ASIAN’98 , December 8-10, Manila,
The Philippines, Lecture Notes in Computer Science 1538, Springer, 245–262, 1998.
9. Y. Fu. Variations on Mobile Processes. Theoretical Computer Science, Vol. 221,327-368, 1999.
10. Y. Fu. Open Bisimulations of Chi Processes. CONCUR’99 , Eindhoven, The
Netherlands, August 24-27, Lecture Notes in Computer Science 1664, 304-319,
Springer, 1999.
11. Y. Fu, Z. Yang. Chi Calculus with Mismatch. CONCUR 2000, 22-25 August, Pennsylvenia, USA, Lecture Notes in Computer Science 1877, 596-610, Springer, 2000.
12. Y. Fu, Z. Yang. The Ground Congruence for Chi Calculus. FST&TCS 2000, December, India, Lecture Notes in Computer Science, Springer, 2000.
13. J. Girard. Linear Logic, Theoretical Computer Science, 50, 1–102, 1987.
14. M. Hennessy, R. Milner. Algebraic Laws for Nondeterminism and Concurrency.
Journal of ACM , 67: 137–161, 1985.
15. K. Honda, M. Tokoro. An Object Calculus for Asynchronous Communication. Proc.
ECOOP ’91 , Geneve, 1991.
16. C. Laneve, B. Victor. Solos in Concert. ICALP’99 , July 11th-15th, Prague, Hungary, Lecture Notes in Computer Science, Springer, 1999.
17. R. Milner. Communication and Concurrency. Prentice Hall, 1989.

18. 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, 1993.
19. R. Milner, J. Parrow, D. Walker. A Calculus of Mobile Processes. Information andComputation, 100: 1–40 (Part I), 41–77 (Part II), Academic Press.
20. M. Merro, D. Sangiorgi. On Asynchrony in Name-Passing Calculi. ICALP’98 , Lecture Notes in Computer Science 1443, Springer, 1998.
21. J. Parrow, B. Victor. The Update Calculus. AMAST’97, Sydney, December 13-17,
1997.
22. J. Parrow, B. Victor. The Fusion Calculus: Expressive and Symmetry in Mobile
Processes. LICS’98 , 1998.
23. J. Parrow, B. Victor. The Tau-Laws of Fusion. CONCUR’98 , Lecture Notes in
Computer Science, 1998.
24. B. Victor, J. Parrow. Concurrent Constraints in the Fusion Calculus. ICALP ’98,
Lecture Notes in Computer Science 1443, 455–469, Springer, 1998.