Chi Calculus with Mismatch?
Yuxi Fu??

Zhenrong Yang

Department of Computer Science
Shanghai Jiaotong University, Shanghai 200030, China

Abstract. The theory of chi processes with the mismatch operator isstudied. Two open congruence relations are investigated. These are weak
early open congruence and weak late open congruence. Complete systems
are given for both congruence relations. These systems use some newtau laws. The results of this paper correct some popular mistakes inliterature.

1

Introduction

In recent years several publications have focused on a class of new calculi ofmobile processes. These models include χ-calculus ([1–4]), update calculus ([7])
and fusion calculus ([8, 10]). In a uniform terminology they are respectively χcalculus, asymmetric χ-calculus and polyadic χ-calculus. The χ-calculus has its
motivations from proof theory. In process algebraic model of classical proofs
there has been no application of mismatch operator. The χ-calculus studied so
far contains no mismatch operator. On the other hand the update and fusion
calculi have their motivations from concurrent constraint programming. When
applying process calculi to model real programming problems one finds very
handy the mismatch operator. For that reason the full update and fusion calculi
always have the mismatch combinator. Strong bisimulation congruence has been
investigated for each of the three models. It is basically the open congruence.
A fundamental difference between χ-like calculi and π-like calculi ([5]) is that
all names in the former are subject to update whereas local names in the latterare never changed. In terms of the algebraic semantics, it says that open stylecongruence relations are particularly suitable to χ-like process calculi. Several
weak observational equivalence relations have been examined. Fu studied in [1]weak open congruence and weak barbed congruence. It was shown that a sensible bisimulation equivalence on χ-processes must be closed under substitution
in every bisimulation step. In χ-like calculi closure under substitution amounts
to the same thing as closure under parallel composition and localization. Thisis the property that led Fu to introduce L-congruences ([2]). These congruence relations form a lattice under inclusion order. It has been demonstrated?
??

CONCUR 2000 , Lecture Notes in Computer Science 1877, 596-610, 2000.
The author is funded by NNSFC (69873032) and the 863 Hi-Tech Project (863-306ZT06-02-2). He is also supported by BASICS, Center of Basic Studies in Computing
Science, sponsored by Shanghai Education Committee. BASICS is affiliated to the
Department of Computer Science at Shanghai Jiaotong University.

that L-congruences are general enough so as to subsume familiar bisimulation
congruences. The open congruence and the barbed congruence for instance arerespectively the bottom and the top elements of the lattice. This is also true
for asymmetric χ-calculus ([4]). Complete systems have been discovered for Lcongruences on both finite χ-processes and finite asymmetric χ-processes ([4]).
An important discovery in the work of axiomatizing χ-processes is that Milner’s
tau laws are insufficient for open congruences. Another basic tau law called T4
τ.P = τ.(P +[x=y]τ.P )is necessary to deal with the dynamic aspect of name update. Parrow and Victor
have worked on completeness problems for fusion calculus ([8]). The systemthey provide for the weak hypercongruence for sub-fusion calculus without themismatch operator is deficient because it lacks of the axiom T4. However theirmain effort in the above mentioned paper is on the full fusion calculus withthe mismatch operator. This part of work is unfortunately more problematic. To
explain what we mean by that we need to take a closer look at hyperequivalence.
Process equivalence is observational in the sense that two processes are
deemed to be equal unless a third party can detect a difference between thetwo processes. Usually the third party is also a process. Now to observe a process is to communicate with it. In process calculi the communication happens
if the observer and the observee are composed via a parallel operator. It follows that process equivalences must be closed under parallel composition. Weak
hyperequivalence is basically an open equivalence. This relation is fine with the
sub-fusion calculus without the mismatch combinator. It is however a bad equivalence for the full fusion calculus for the reason that it is not closed under composition. A simple counter example is as follows: Let ≈h be the hyperequivalence.
Now for distinct names x, y it holds that(x)ax.[x6=y]τ.P ≈h (x)ax.[x6=y]τ.P +(x)ax.Pa(x)This is because the transition (x)ax.[x6=y]τ.P +(x)ax.P −→ P can be simulateda(x) τ

by (x)ax.[x6=y]τ.P −→−→ P . Howeveray|(x)ax.[x6=y]τ.P 6≈h ay|((x)ax.[x6=y]τ.P +(x)ax.P )τfor ay|((x)ax.[x6=y]τ.P +(x)ax.P ) −→ 0|P [y/x] can not be matched up by any
transitions from ay|(x)ax.[x6=y]τ.P . For similar reason
ax.[x6=y]τ.P ≈h ax.[x6=y]τ.P +[x6=y]ax.P
but
ay|ax.[x6=y]τ.P 6≈h ay|(ax.[x6=y]τ.P +[x6=y]ax.P )So the theory of weak equivalences of fusion calculus need be overhauled.
In the above counter examples the mismatch operator plays a crucial part.
From a programming point of view the role of the mismatch combinator is toterminate a process at run time. This is a useful function in practice and yet
realizable in neither CCS nor calculi of mobile processes without the mismatch
combinator. The problem caused by the mismatch combinator is mostly operational. A well known fact is that transitions are not stable under name instantiations, which render the algebraic theory difficult. The mismatch operator often
creates a ‘now-or-never’ situation in which if an action does not happen rightnow it might never be allowed to happen. In the calculi with the mismatch operator processes are more sensible to the timing of actions. This reminds one ofthe difference between early and late semantics.
The early/late dichotomy is well known in the semantic theory of π-calculus.
The weak late congruence is strictly contained in the weak early congruence in
π-calculus whether the mismatch combinator is present or not. For some time
it was taken for granted that there is no early and late distinction in weak
open congruence. At least this is true for the calculus without the mismatch
combinator. Very recently the present authors discovered to their surprise thatearly and late approaches give rise to two different weak open congruences inthe π-calculus in the presence of the mismatch combinator. This has led themto realize the problem with the weak hyperequivalence.
In this paper we study early and late open congruences for χ-calculus withthe mismatch operator. The main contributions of this paper are as follows:– We point out that there is an early/late discrepancy in the open semantics
of calculi of mobile processes with the mismatch combinator.
– We provide a correct treatment of open semantics for χ-calculus with mismatch. Our definitions of early and late congruences suggest immediately
how to generalize them to fusion calculus.
– We propose two new tau laws to handle free prefix operator and one to deal
with update prefix combinator. These tau laws rectify the mistaken tau laws
in [8]. We point out that the new tau laws for free prefix operator subsume
the corresponding laws for bound prefix operator.
– We give complete axiomatic systems for both early open congruence and late
open congruence. These are the first completeness result for weak congruences on χ-like processes with the mismatch operator.
The structure of the paper is as follows: Section 2 summarizes some background material on χ-calculus. Section 3 defines two weak open congruences.
Section 4 proves completeness theorem. Some comments are made in the final
section.

2

The χ-Calculus with Mismatch

The π-calculus has been shown to be a powerful language for concurrent computation. From the algebraic point of view, the model is slightly inconvenient due
to the presence of two classes of restricted names. The input prefix operator a(x)introduces the dummy name x to be instantiated by an action induced by theprefix operator. On the other hand the localization operator (y) forces the namey to be local, which will never be instantiated. Semantically these two restrictednames are very different. The χ-calculus can be seen as obtained from the πcalculus by unifying the two classes of restricted names. The calculus studied inthis paper is the χ-calculus extended with the mismatch operator. This language
will be referred to as the χ6= -calculus in the rest of the paper.
We will write C for the set of χ6= -processes defined by the following grammar:
P := 0 | α[x].P | P |P | (x)P | [x=y]P | [x6=y]P | P +P
where α ∈ N ∪ N . Here N is the set of names ranged over by small case letters.
The set {x | x ∈ N } of conames is denoted by N . We have left out replication
processes since we will be focusing on axiomatization of equivalences on finite
processes. The name x in (x)P is local. A name is global in P if it is not local
in P . The global names, the local names and the names of P , as well as thenotations gn(P ), ln(P ) and n(P ), are used in their standard meanings. In sequel
we will use the functions gn( ), ln( ) and n( ) without explanation. We adopt
the α-convention widely used in the literature on process algebra.
The following labeled transition system defines the operational semantics:
Sequentialization
α[x]α[x].P −→ P

Sqn

Composition[y/x]

P −→ P 0ν

P −→ P 0 bn(ν) ∩ gn(Q)=∅Cmp0
ν
P |Q −→ P 0 |Q

[y/x]

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

Communication
α[y]

α(x)

α(x)

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

α[y]

Q −→ Q0

P −→ P 0α[x]x 6= yα[x]P −→ P 0 Q −→ Q0
Cmm3
τP |Q −→ P 0 |Q0

Cmm2

[y/x]

P |Q −→ P 0 [y/x]|Q0 [y/x]α(x)P −→ P 0 Q −→ Q0
Cmm1
τP |Q −→ (x)(P 0 |Q0 )Localization
λP −→ P 0

α[x]P −→ P 0

x 6∈ n(λ)λ(x)P −→ (x)P 0

Loc0

[y/x]

x 6∈ {α, α}
Loc1

α(x)

(x)P −→ P 0

P −→ P 0
Loc2
τ(x)P −→ P 0

ConditionλλP −→ P 0λ[x=x]P −→ P

P −→ P 0
0 M tchx6=y
λ[x6=y]P −→ P 0

Summation
λP −→ P 0λ

P +Q −→ P 0

Sum

M ismtchWe have omitted all the symmetric rules. In the above rules the letter ν ranges
over the set {α(x), α[x] | α ∈ N ∪ N , x ∈ N } ∪ {τ } of actions and the letter λover the set {α(x), α[x], [y/x] | α ∈ N ∪ N , x, y ∈ N } ∪ {τ } of labels. The symbols α(x), α[x], [y/x] represent restricted action, free action and update action
respectively. The x in α(x) is local.
A substitution is a function from N to N . Substitutions are usually denotedby σ, σ 0 etc.. The empty substitution, that is the identity function on N , iswritten as []. The result of applying σ to P is denoted by P σ. Suppose Y is a finite
set {y1 , . . . , yn } of names. The notation [y6∈Y ]P stands for [y6=y1 ] . . . [y6=yn ]P ,where the order of the mismatch operators is immaterial. We will write φ and ψ tostand for sequences of match and mismatch combinators concatenated one after
another, µ for a sequence of match operators, and δ for a sequence of mismatch
operators. Consequently we write ψP , µP and δP . When the length of ψ (µ,δ) is zero, ψP (µP , δP ) is just P . The notation φ ⇒ ψ says that φ logically
implies ψ and φ ⇔ ψ that φ and ψ are logically equivalent. A substitution σagrees with ψ, and ψ agrees with σ, when ψ ⇒ x=y if and only if σ(x)=σ(y).
λ̂The notations =⇒ and =⇒ are used in their standard meanings. A sequencex1 , . . . , xn of names will be abbreviated to x̃.
The following lemma is useful in later proofs.
λLemma 1. If P σ −→ P1 then there exists some P 0 such that P1 ≡ P 0 σ.
Notice that a substitution σ may disable an action of P . So one can not concludeλσ
λP σ −→ P 0 σ from P −→ P 0 . But the above lemma tells us that we may writeλP σ −→ P 0 σ once we know that P σ can induce a λ transition.

3

Open Bisimilarities

In our view the most natural equivalence for mobile processes is the open equivalence introduced by Sangiorgi ([9]). Technically the open equivalence is a bisimulation equivalence closed under substitution of names. Philosophically the open
approach assumes that the environments are dynamic in the sense that they areshrinking, expanding and changing all the time. After the simulation of eachcomputation step, the environment might be totally different. As a matter offact the very idea of bisimulation is to ensure that no operational difference canbe detected by any dynamic environment. So closure under substitution is areasonable requirement.
A simple minded definition of weak open bisimulation would go as follows:
A binary relation R on C is a weak open bisimulation if it is symmetric
λand closed under substitution such that whenever P RQ and P −→ P 0b
λthen Q =⇒ Q0 RP 0 for some Q0 .
As it turns out this is a bad definition for processes with the mismatch operator.
Counter examples are given in the introduction. The problem here is that theinstantiation of names is delayed for any period of time. This is not always
possible in χ6= -calculus. To correct the above definition, one should adopt theapproach that name instantiations should take place in the earliest possible
occasion. This brings us to the familiar early and late frameworks.
Definition 2. Let R be a binary symmetric relation on C. It is called an early
open bisimulation if it is closed under substitution and whenever P RQ then thefollowing properties hold:τ(i) If P −→ P 0 then Q0 exists such that Q =⇒ Q0 RP 0 .
[y/x]

[y/x]

(ii) If P −→ P 0 then Q0 exists such that Q =⇒ Q0 RP 0 .
α[x]

α[x]

α(x)

α(x)

(iii) If P −→ P 0 then for every y some Q0 , Q00 exist such that Q =⇒−→ Q00 and
Q00 [y/x] =⇒ Q0 RP 0 [y/x].
(iv) If P −→ P 0 then for every y some Q0 , Q00 exist such that Q =⇒−→ Q00 and
Q00 [y/x] =⇒ Q0 RP 0 [y/x].
The early open bisimilarity ≈eo is the largest early open bisimulation.
The clause (iv) is easy to understand. Its counterpart for weak bisimilarity of
π-calculus is familiar. The clause (iii) calls for some explanation. In χ6= -calculus
α[x]free actions can also incur name updates in suitable contexts. Suppose P −→
τP 00 . Then (x)(P |α[y].Q) −→ P 00 [y/x]|Q[y/x]. Even if P 00 =⇒ P 0 , one does not00
necessarily have P [y/x] =⇒ P 0 [y/x]. Had we replace clause (iii) by
α[x]

α[x]

(iii’) If P −→ P 0 then some Q0 exists such that Q =⇒ Q0 RP 0then we would have obtained a relation to which the second counter example
in the introduction applies. The similarity of clause (iii) and clause (iv) exhibits
once again the uniformity of the names in χ-like calculi.
Analogously we can introduce late open bisimilarity.
Definition 3. Let R be a binary symmetric relation on C. It is called a late
open bisimulation if it is closed under substitution and whenever P RQ then thefollowing properties hold:τ(i) If P −→ P 0 then Q0 exists such that Q =⇒ Q0 RP 0 .
[y/x]

[y/x]

(i) If P −→ P 0 then Q0 exists such that Q =⇒ Q0 RP 0 .
α[x]

α[x]

α(x)

α(x)

(iii) If P −→ P 0 then Q00 exists such that Q =⇒−→ Q00 and for every y some
Q0 exists such that Q00 [y/x] =⇒ Q0 RP 0 [y/x].
(iv) If P −→ P 0 then Q00 exists such that Q =⇒−→ Q00 and for every y some
Q0 exists such that Q00 [y/x] =⇒ Q0 RP 0 [y/x].
The late open bisimilarity ≈lo is the largest late open bisimulation.
It is clear that ≈lo ⊆≈eo . The following example shows that inclusion is strict:a[x].[x=y]τ.P +a[x].[x6=y]τ.P ≈eo a[x].[x=y]τ.P +a[x].[x6=y]τ.P +a[x].P but nota[x].[x=y]τ.P +a[x].[x6=y]τ.P ≈lo a[x].[x=y]τ.P +a[x].[x6=y]τ.P +a[x].P .
The lesson we have learned is that we should always check if an observational
equivalence is closed under parallel composition. The next lemma makes surethat this is indeed true for the two open bisimilarities.

Lemma 4. Both ≈eo and ≈lo are closed under localization and composition.
Both open bisimilarities are also closed under the prefix and match combinators. But neither is closed under the summation operator or the mismatch
operator. For instance [x6=y]P ≈eo [x6=y]τ.P does not hold in general. To obtainthe largest congruence contained in early (late) open bisimilarity we follow thestandard approach: We say that two processes P and Q are early open congruent, notation P 'eo Q, if P ≈eo Q and for each substitution σ a tau action of P σmust be matched up by a non-empty sequence of tau actions from Qσ and viceversa. Clearly 'eo is a congruence. Similarly we can define 'lo .

4

Axiomatic System

In [2] completeness theorems are proved for L-bisimilarities on χ-processes without mismatch operator. The proofs of these completeness results use essentiallythe inductive definitions of L-bisimilarities. In the presence of the mismatch operator, the method used in [2] should be modified. The modification is done byincorporating ideas from [6]. In this section, we give the complete axiomatic systems for early and late open congruences using the modified approach. First weneed to define two induced prefix operators, tau and update prefixes, as follows:def[y|x].P = (a)(a[y]|a[x].P )def

τ.P = (b)[b|b].P
where a, b are fresh. The following are some further auxiliary definitions.
Definition 5. Let V be a finite set of names. We say that ψ is complete on V
if n(ψ) ⊆ V and for each pair x, y of names in V it holds that either ψ ⇒ x=yor ψ ⇒ x 6= y.
Suppose ψ is complete on V and n(φ) ⊆ V . Then it should be clear that eitherψφ ⇔ ψ or ψφ ⇔ ⊥. In sequel this fact will be used implicitly.
Lemma 6. If φ and ψ are complete on V and both agree with σ then φ ⇔ ψ.
Definition 7. A substitution σ is induced by ψ if it agrees with ψ and σσ = σ.
Let AS denote the system consisting of the rules and laws in Appendix A
plus the following expansion law:
πi =ai [xi ]P |Q =XiX

φi (x̃)πi .(Pi |Q) +φi ψj (x̃)(ỹ)[ai =bj ][xi |yj ].(Pi |Qj ) +γj =bj [yj ]πi =ai [xi ]Xjψj (ỹ)γj .(P |Qj ) +X
γj =bj [yj ]φi ψj (x̃)(ỹ)[ai =bj ][xi |yj ].(Pi |Qj )PPwhere P is i φi (x̃)πi .Pi and Q is j ψj (ỹ)γj .Qj , πi and γj range over {α[x] |α ∈ N ∪ N , x ∈ N }. In the expansion law, the summand
πi =ai [xi ]X

φi ψj (x̃)(ỹ)[ai =bj ][xi |yj ].(Pi |Qj )γj =bj [yj ]contains φi ψj (x̃)(ỹ)[ai =bj ][xi |yj ].(Pi |Qj ) as a summand whenever πi = ai [xi ]and γj = bj [yj ].
We write AS ` P = Q to indicate that the equality P = Q can be inferredfrom AS. Some important derived laws of AS are given in Appendix A.
Using axioms in AS, a process can be converted to a process that contains
no occurrence of the composition operator, the latter process is of special form
as defined below.
Definition 8. A process
P is in normal form
P
P
P on V ⊇ f n(P ) if P is of the formi∈I1 φi αi [xi ].Pi +i∈I2 φi (x)αi [x].Pi +i∈I3 φi [zi |yi ].Pi such that x does notappear in P , φi is complete on V for each i ∈ I1 ∪ I2 ∪ I3 , Pi is in normal formon V for i ∈ I1 ∪ I3 and is in normal form on V ∪ {x} for i ∈ I2 . Here I1 , I2
and I3 are pairwise disjoint finite indexing sets.
Notice that if P is in normal form and σ is a substitution then P σ is in normalform.
The depth of a process measures the maximal length of nested prefixes in theprocess. The structural definition goes as follows: (i) d(0) = 0; (ii) d(α[x].P ) =1+d(P ); (iii) d(P |Q) = d(P )+d(Q); (iv) d((x)P ) = d(P ); (v) d([x=y]P ) = d(P );(vi) d(P +Q) = max{d(P ), d(Q)}.
Lemma 9. For a process P and a finite set V of names such that f n(P ) ⊆ V
there is a normal form Q on V such that d(Q) ≤ d(P ) and AS ` Q = P .
It can be shown that AS is complete for the strong open bisimilarity on χ6= processes. This fact will not be proved here. Our attention will be confined tothe completeness of the two weak open congruences. The tau laws used in thispaper are given in Figure 1. Some derived tau laws are listed in Figure 2. In
what follows, we will write ASol for AS ∪ {T 1, T 2, T 3a, T 3b, T 3d, T 4} and ASoe
for AS ∪ {T 1, T 2, T 3a, T 3c, T 3d, T 4}.
The next lemma discusses some relationship among the tau laws.
Lemma 10. (i) ASoe ` T D5. (ii) ASol ` T D6. (iii) AS ∪ {T 3c} ` T 3b.
Proof. (i) By T3c and C2, we get:ASoe ` Σ(a(x), P, Q, δ) = (x)(Σ(a[x], P, Q, δ)+[x6∈n(δ)]δa[x].Q)= Σ(a(x), P, Q, δ)+(x)[x6∈n(δ)]δa[x].Q
LD3= Σ(a(x), P, Q, δ)+(x)δa[x].Q

LD2= Σ(a(x), P, Q, δ)+δ(x)a[x].Q

The proofs of (ii) and (iii) are omitted.

t
u

T1
α[x].τ.P = α[x].P
T2
P +τ.P = τ.PT3aα[x].(P +τ.Q) = α[x].(P +τ.Q)+α[x].Q
T3bα[x].(P +δτ.Q) = α[x].(P +δτ.Q)+[x6∈n(δ)]δα[x].Q
x 6∈ n(δ)
T3cΣ(α[x], P, Q, δ) = Σ(α[x], P, Q, δ)+[x6∈n(δ)]δα[x].Q
x 6∈ n(δ)
T3d[y|x].(P +δτ.Q) = [y|x].(P +δτ.Q)+ψδ[y|x].Q
T4
τ.P = τ.(P +ψτ.P )In T3d, if δ ⇒ [u6=v] then either ψ ⇒ [x=u][y6=v] or ψ ⇒ [x=v][y6=u]or ψ ⇒ [y=u][x6=v] or ψ ⇒P[y=v][x6=u] or ψ ⇒ [x6=u][x6=v][y6=u][y6=v].
In T3c, Σ(α[x], P, Q, δ) is
α[x].(Py +δ[x=y]τ.Q)+α[x].(P +δ[x6∈Y ]τ.Q).
y∈Y
Fig. 1. The Tau Laws
TD1[x|y].τ.P = [x|y].P
TD2
τ.τ.P = τ.PTD3[x|y].(P +τ.Q) = [x|y].(P +τ.Q)+[x|y].Q
TD4
τ.(P +τ.Q) = τ.(P +τ.Q)+τ.Q
TD5(x)α[x].(P +δτ.Q) = (x)α[x].(P +δτ.Q)+δ(x)α[x].Q
x 6∈ n(δ)
TD6Σ(α(x), P, Q, δ) =PΣ(α(x), P, Q, δ)+δ(x)α[x].Q
x 6∈ n(δ)
In TD6, Σ(α(x), P, Q, δ) is(x)α[x].(Py +δ[x=y]τ.Q)+(x)α[x].(P +δ[x6∈Y ]τ.Q).
y∈Y
Fig. 2. The Derived Tau Laws

To establish the completeness theorem, some properties of AS and the open
bisimilarities must be established first. The next three lemmas describe theseproperties.
Lemma 11. Suppose Q is in normal form on V , φ is complete on V , and σ isa substitution induced by φ. Then the following properties hold:τ(i) If Qσ =⇒ Q0 then AS ∪ {T 1, T 2, T 3a} ` Q = Q+φτ.Q0 .
α[x](ii) If Qσ =⇒−→ Q0 then AS ∪ {T 1, T 2, T 3a} ` Q = Q+φα[x].Q0 .
α(x)(iii) If Qσ =⇒−→ Q0 then AS ∪ {T 1, T 2, T 3a} ` Q = Q+φ(x)α[x].Q0 .
[y/x](iv) If Qσ =⇒ Q0 then AS ∪ {T 1, T 2, T 3a, T 3d} ` Q = Q+φ[y|x].Q0 .
[y/x]

Proof. (iv) If Qσ −→ Q0 then AS ∪ {T 1, T 2, T 3a, T 3d} ` Q = Q+φ[y|x].Q0 .
τ

[y/x]

τ

Suppose for example Qσ =⇒ Q1 σ −→ Q2 =⇒ Q0 . It is easy to see that Q2 ≡Q02 σ[y/x]. Let ψ be a complete condition on f n(Q02 ) that induces σ[y/x]. Supposeψ ⇔ µδ. Clearly µσ[y/x] is true. Therefore
AS ∪ {T 1, T 2, T 3a, T 3d} ` Q = Q+φ[y|x].Q2= Q+φ[y|x].Q02 σ[y/x]= Q+φ[y|x].Q02= Q+φ[y|x].(Q02 +ψτ.Q0 )= Q+φ[y|x].(Q02 +µδτ.Q0 )= Q+φ[y|x].(Q02 +δτ.Q0 )= Q+φ([y|x].(Q02 +δτ.Q0 )+θδτ.Q0 )= Q+φθδ[y|x].Q0
in which θ is defined as in T 3d. First of all it is easy to see that φ ⇒ δ for φ iscomplete on V . So φδ ⇔ φ. Second we need to explain how to construct θ. It
should be constructed in such a way that φθ ⇔ φ. Suppose δ ⇒ [u6=v]. There
are five possibilities:– φ ⇒ x=u. Then we let θ contain [x=u][y6=v]. If φ ⇒ y=v then σ is induced by[x=u][y=v]. It follows that σ[y/x] is induced by [u=v], which is impossible.
Hence φ ⇒ y6=v.
– φ ⇒ y=u or φ ⇒ x=v or φ ⇒ y=v. These cases are similar to previous case.
– φ ⇒ [x6=u][x6=v][y6=u][y6=v]. Simply let θ contain [x6=u][x6=v][y6=u][y6=v].
It is clear from the construction that φ ⇒ θ. Therefore AS∪{T 1, T 2, T 3a, T 3d} `Q = Q+φθδ[y|x].Q0 = Q+φ[y|x].Q0 .
tuLemma 12. Suppose Q is a normal form on some V = {y1 , . . . , yk } ⊇ f n(Q),ψ is complete on V , and σ is a substitution induced by ψ. Ifα(x)Qσ=⇒ −→ Q01 σ, Q01 σ[y1 /x] =⇒ Q1 ,α(x)Qσ=⇒ −→ Q02 σ, Q02 σ[y2 /x] =⇒ Q2 ,
..
.
α(x)

Qσ=⇒ −→ Q0k σ, Q0k σ[yk /x] =⇒ Qk ,α(x)Qσ =⇒−→ Q0k+1 σ =⇒ Qk+1
then the following properties hold:Pk
1. AS ∪ {T 1, T 2, T 3a} ` Q = Q + ψ j=1 (x)α[x].(τ.Q0j + ψ[x=yj ]τ.Qj ) +0
ψ(x)α[x].(τ.Qk+1 + ψ[x6∈V ]τ.Qk+1 )).
Pk
2. If Q01 ≡ Q0 , . . . , Q0k+1 ≡ Q0 , then Q + ψ(x)α[x].(τ.Q0 + ψ j=1 [x=yj ]τ.Qj +φ[x6∈V ]τ.Qk+1 ) is provably equal to Q in AS ∪ {T 1, T 2, T 3a}.
The proof of the above lemma is similar to that of Lemma 11.
Lemma 13. In χ6= -calculus the following properties hold:(i) If P ≈eo Q then ASoe ` τ.P = τ.Q.
(ii) If P ≈lo Q then ASol ` τ.P = τ.Q.
Proof. By Lemma 9 we may assume that P and Q are in normal form on V =f n(P |Q) = {y1 , y2 , . . . , yk }. Let P beXXX
φi αi [xi ].Pi +φi (x)αi [x].Pi +φi [zi |yi ].Pi
i∈I1

i∈I2

i∈I3

and Q beXψj αj [xj ].Qj +

X
j∈J2

j∈J1

X

ψj (x)αj [x].Qj +ψj [zj |yj ].Qjj∈J3

We prove this lemma by induction on the depth of P |Q.
(i) Suppose φi πi .Pi is a summand of P and σ is induced by φi . There areseveral cases:[y/x]– πi σ is an update action [y|x]. It follows from P ≈eo Q that Qσ =⇒ Q0 ≈eo
Pi [y/x]σ. By induction we have ASoe ` Q0 = Pi σ[y/x]. By (iv) of Lemma 11
ASoe ` Q = Q+φi [y|x].Q0= Q+φi [y|x].Pi [y/x]σ= Q+φi [y|x].Pi σ= Q+φi πi σ.Pi σ= Q+φi πi .Pi– πi σ is a restricted action α(x). Since P ≈eo Q one has the following cases:α(x)• For each l ∈ {1, . . . , k}, Q0il and Qil exist such that Qσ=⇒ −→ Q0il σ andQ0il σ[yl /x] =⇒ Qil ≈eo Pi σ[yl /x].
α(x)• Q0ik+1 and Qik+1 exist such that Qσ=⇒ −→ Q0ik+1 σ =⇒ Qik+1 ≈eo Pi σ.
By Lemma 12
ASoe ` Q = Q+kX

φi (x)a[x].(τ.Q0il +φi [x=yl ]τ.Qil )l=1+φi (x)a[x].(τ.Q0ik+1 +φi [x6∈V ]τ.Qik+1 )
= Q+

k
X

φi (x)a[x].(τ.Q0il +φi [x=yl ]τ.Pi σ[yl /x])l=1+φi (x)a[x].(τ.Q0ik+1 +φi [x6∈V ]τ.Pi σ)= Q+φ(x)a[x].Pi= Q+φi πi .Pi– πi σ is a free action α[x]. Using the fact P ≈eo Q one has the following cases:α[x]• For each l ∈ {1, . . . , k}, Q0il and Qil exist such that Qσ=⇒ −→ Q0il σ andQ0il σ[yl /x] =⇒ Qil ≈eo Pi σ[yl /x].
α[x]• Q0ik+1 and Qik+1 exist such that Qσ=⇒ −→ Q0ik+1 σ =⇒ Qik+1 ≈eo Pi σ.
Since φi is complete on V , it groups the elements of V into several disjointclasses. Assume that these classes are [x], [a1 ], . . . , [ar ]. Let φ=i be the sequence of match operators induced by the equivalence classes [a1 ], . . . , [ar ].
Let φ=x
be the sequence of match operators induced by the equivalenceiclass [x]. Let φ6=i be the sequence of mismatch combinators constructed asfollows: For 1 ≤ p, q ≤ r and a ∈ [ap ], b ∈ [aq ], a6=b is in φ6=
i . And let
x
φ6=
be
the
sequenceofmismatchcombinators
constructedasfollows:Fori6=x= =x 6= 6=xa ∈ [a1 ] ∪ . . . ∪ [ar ], a6=x is in φi . It is clear that φi ⇔ φi φi φi φi . Now
def

V can be divided into two subsets: V =x = {y | y ∈ V, φi ⇒ y=x}; anddefx
V 6=x = {y | y ∈ V, φi ⇒ y6=x} = [a1 ] ∪ . . . ∪ [ar ]. Clearly φ6=⇔ [x6∈V 6=x ].
i
6=x
6=x
• If yl ∈ Vthen we define φi\[yl ] as follows: For a ∈ ([a1 ] ∪ . . . ∪ [ar ]) \
x
6=x
6=x
[yl ], a6=x is in φ6=\ [yl ])].
i\[yl ] . It is easy to see that φi\[yl ] ⇔ [x6∈(V=x 6= 6=xNow φ=i φi φi φi\[yl ] [x=yl ] is complete on V and induces σ[yl /x]. By
Lemma 11Q = Q + φi α[x].Q0il= Q + φi α[x].τ.Q0il=x 6= 6=x
= Q + φi α[x].(τ.Q0il + φ=i φi φi φi\[yl ] [x=yl ]τ.Qil )6=x= Q + φi α[x].(τ.Q0il + φ6=i φi\[yl ] [x=yl ]τ.Qil )6=x= Q + φi α[x].(τ.Q0il + φ6=\ [yl ])][x=yl ]τ.Qil )i [x6∈(V
6=x= Q + φi α[x].(τ.Q0il + φ6=\ [yl ])][x=yl ]τ.Qil )i [yl 6∈(V

= Q + φi α[x].(τ.Q0il + φ6=i [x=yl ]τ.Qil )=x 6= 6=x
• It is clear that φ=is complete on V and induces σ. One hasi φi φi φiby Lemma 11 that

Q = Q + φi α[x].Q0ik= Q + φi α[x].τ.Q0ik=x 6= 6=x
= Q + φi α[x].(τ.Q0ik + φ=i φi φi φi τ.Qik+1 )6=x= Q + φi α[x].(τ.Q0ik + φ6=i φi τ.Qik+1 )6=x= Q + φi α[x].(τ.Q0ik + φ6=]τ.Qik+1 )i [x6∈V

Now
ASoe ` Q = Q+X

φi α[x].(τ.Q0il +φ6=i [x=yl ]τ.Qil )yl ∈V 6=x6=x+φi α[x].(τ.Q0ik+1 +φ6=
]τ.Qik+1 )i [x6∈VX
6=0= Q+
φi α[x].(τ.Qil +φi [x=yl ]τ.Pi σ[yl /x])yl ∈V 6=x6=x+φi α[x].(τ.Q0ik+1 +φ6=
]τ.Pi σ)i [x6∈V= Q+φi [x6∈n(φ6=i )]α[x].Pi= Q+φi α[x].Piτ– πi σ is a tau action. If the tau action is matched by Qσ =⇒ Q0 then it is easy
to prove that ASoe ` Q = Q+φi πi .Pi . If the tau action is matched vacuously
then ASoe ` Q+φi πi .Pi = Q+φi τ.Q.

In summary, we have ASoe ` P +Q = Q+Σi∈I 0 φi τ.Q for some I 0 ⊆ I. So by T4
we get ASoe ` τ.(P + Q) = τ.(Q + Σi∈I 0 φi τ.Q) = τ.Q. Symmetrically, we canprove ASoe ` τ.(P +Q) = τ.P . Hence ASoe ` τ.P = τ.Q.
(ii) The proof is similar to that for ≈eo . We consider only one case:– πi σ is a restricted action α(x). It follows from P ≈lo Q that some Q0 exists
such that the following holds:α(x)• For each l ∈ {1, . . . , k}, Q0 , Qil exists such that Qσ=⇒ −→ Q0 σ andQ0 σ[yl /x] =⇒ Qil ≈lo Pi σ[yl /x].
α(x)• Qik+1 exists such that Qσ=⇒ −→ Q0 σ =⇒ Qik+1 ≈lo Pi σ.
By (ii) of Lemma 12 we get
ASol ` Q = Q+φi (x)α[x].(τ.Q0 +φikX[x=yl ]τ.Qil +φi [x6∈V ]τ.Qik+1 )l=1= Q+φi (x)α[x].(τ.Q0 +φikX[x=yl ]τ.Pi σ[yl /x]+φi [x6∈V ]τ.Pi σ)

l=1= Q+φi (x)α[x].(τ.Q0 +φi τ.Pi )= Q+φi (x)α[x].Pi
Then by a similar argument as in (i), we get ASol ` τ.P = τ.Q.

t
u

6=

Theorem 14. In χ -calculus the following completeness results hold:(i) If P 'eo Q then ASoe ` P = Q.
(ii) If P 'lo Q then ASol ` P = Q.
Proof. By Lemma 11 and Lemma 13, one can prove the theorem in very muchthe same way as the proof of Lemma 13 is done.
tu5Historical Remark

The first author of this paper has been working on χ-calculus for some years. His
attention had always been on the version of χ without mismatch combinator.
By the end of 1999 he started looking at testing congruence on χ-processes.
In order to axiomatize the testing congruence he was forced to introduce themismatch operator. This led him to deal with open congruences on χ6= -processes,
which made him aware of the fact that the open semantics for the π-calculus
with the mismatch combinator has not been investigated before. So he, together
with the second author, began to work on the problem for the π-calculus withthe mismatch combinator. Their investigation showed that the simple-mindeddefinition of open bisimilarity is not closed under parallel composition. It is thena small step to realize the problem of the weak hyperequivalence.
It has come a long way to settle down on the axiom T4. The first solution,
proposed by the first author in an early version of [4], is the following rule:
P +Σi∈I ψi τ.P = Q+Σj∈J ψj τ.Q
τ.P = τ.Q

The premises of the rule is an equational formalization of P ≈ Q. In the final
version of [4] he observed that the rule is equivalent to the following law:
τ.P = τ.(P +Σi∈I ψi τ.P )
Later on he realized that the above equality can be simplified to T4.
In [8] two tau laws are proposed for fusion calculus. Using the notations of [8]they can be written as follows:α.(P + M̃ 1.Q) = α.(P + M̃ 1.Q) + M̃ α.Q(1)
ι.(P +M̃ ρ.Q) = ι.(P +M̃ ρ.Q)+M̃ ι ∧ ρ.Q if ∀x, y.(M̃ ⇒x6=y)⇒¬(xιy) (2)where α is a communication action, ι and ρ are fusion actions, and M̃ is asequence of match/mismatch operators. Neither (1) nor (2) is valid. The counterexample to (1) is given in the introduction. The problem with (2) is that it is
not closed under substitution. The following is an instance of (2) since the side
condition is satisfied:{x=y}.(P +[u6=v]1.Q) = {x=y}.(P +[u6=v]1.Q)+[u6=v]{x=y}.Q
But if we substitute u for x and v for y we get{x=y}.(P +[x6=y]1.Q) = {x=y}.(P +[x6=y]1.Q)+[x6=y]{x=y}.Q
This equality should not hold. Our T3b is the correction of (1) while our T3d is
a special case of the correct version of (2). In order for (2) to be valid, the side
condition has to be internalized as it were.

References
1. Y. Fu. A Proof Theoretical Approach to Communications. ICALP’97 , Lecture
Notes in Computer Science 1256, Springer, 325–335, 1997.
2. Y. Fu. Bisimulation Lattice of Chi Processes. ASIAN’98 , Lecture Notes in Computer Science 1538, Springer, 245–262, 1998.
3. Y. Fu. Variations on Mobile Processes. Theoretical Computer Science, 221: 327368, 1999.
4. Y. Fu. Open Bisimulations of Chi Processes. CONCUR’99 , Lecture Notes in Computer Science 1664, Springer, 304-319, 1999.
5. R. Milner, J. Parrow, D. Walker. A Calculus of Mobile Processes. Information andComputation, 100: 1-40 (Part I), 41-77 (Part II), Academic Press.
6. J. Parrow, D. Sangiorgi. Algebraic Theories for Name-Passing Calculi. Journal of
Information and Computation, 120: 174-197, 1995.
7. J. Parrow, B. Victor. The Update Calculus. AMAST ’97, Lecture Notes in Computer Science 1119, Springer, 389–405, 1997.
8. J. Parrow, B. Victor. The Tau-Laws of Fusion. CONCUR ’98, Lecture Notes in
Computer Science 1466, Springer, 99–114, 1998.
9. D. Sangiorgi. A Theory of Bisimulation for π-Calculus. CONCUR 93 , Lecture
Notes in Computer Science 715, Springer, 1993.
10. B. Victor, J. Parrow. Concurrent Constraints in the Fusion Calculus. ICALP ’98,
Lecture Notes in Computer Science 1443, Springer, 455–469, 1998.

A

Axiomatic System for the Strong Open Congruence

E1
P =P
E2
P =Q
if Q = P
E3
P =R
if P = Q and Q = R
C1
α[x].P = α[x].Q
if P = Q
C2(x)P = (x)Q
if P = Q
C3a[x=y]P = [x=y]Q
if P = Q
C3b[x6=y]P = [x6=y]Q
if P = Q
C4
P +R = Q+R
if P = Q
C5
P0 |P1 = Q0 |Q1
if P0 = Q0 and P1 = Q1
L1(x)0 = 0L2(x)α[y].P = 0x ∈ {α, α}L3(x)α[y].P = α[y].(x)Px 6∈ {y, α, α}L4(x)(y)P = (y)(x)PL5(x)[y=z]P = [y=z](x)Px 6∈ {y, z}L6(x)[x=y]P = 0x6=yL7(x)(P +Q) = (x)P +(x)QL8(x)[y|z].P = [y|z].(x)Px 6∈ {y, z}L9(x)[y|x].P = τ.P [y/x]y 6= xL10(x)[x|x].P = τ.(x)P
M1
φP = ψP
if φ ⇔ ψM2[x=y]P = [x=y]P [y/x]M3a [x=y](P +Q) = [x=y]P +[x=y]Q
M3b [x6=y](P +Q) = [x6=y]P +[x6=y]QM4
P = [x=y]P +[x6=y]PM5[x6=x]P = 0
S1
P +0 = P
S2
P +Q = Q+P
S3
P +(Q+R) = (P +Q)+R
S4
P +P = PU1[y|x].P = [x|y].P
U2[y|x].P = [y|x].[x=y]P
U3[x|x].P = τ.PLD1(x)[x|x].P = [y|y].(x)Pby U3 and L8LD2(x)[y6=z]P = [y6=z](x)Pby L5, L7 and M4LD3(x)[x6=y]P = (x)Pby L6, L7 and M4
MD1[x=y].0 = 0
by S1, S4 and M4
MD2[x=x].P = P
by M1
MD3
φP = φ(P σ) where σ agrees with φ
by M2
SD1
φP +P = P
by S-rules and M4
UD1[y|x].P = [y|x].P [y/x]by U2 and M2