The Value-Passing Calculus
Yuxi Fu
BASICS, Department of Computer Science, Shanghai Jiaotong University
MOE-MS Key Laboratory for Intelligent Computing and Intelligent Systems

Abstract. A value-passing calculus is a process calculus in which thecontents of communications are values chosen from some data domain,
and the propositions appearing in the conditionals are formulas constructed from a logic. Previous studies treat the domain models, as wellas the logic theories, as unspeciﬁed oracles. The open-ended approachleaves open some fundamental issues unanswered. The paper provides
a more formal account of the value-passing calculi. The new treatment
is self-contained in that the logic theory a value-passing calculus refers
to is formally deﬁned. A value-passing calculus consists of a complete
ﬁrst order theory with an operational model that makes use of the terms
and the boolean expressions of the theory. A systematic investigation
into the theory of the value-passing calculi is carried out. A particularvalue-passing calculus, VPC, is shown to be the least expressive among
all Turing complete value-passing calculi.

1

Introduction

Process calculus oﬀers one approach to study interactions between computing objects. The process models can be classiﬁed by the type of the entities exchanged
over interactions. The pioneering process calculus, the CCS of Milner [Mil89a],
abstracts away the contents of communications. For this reason, it serves as abenchmark model for process. Although the pure CCS falls short of being avery interesting model from the point of view of expressiveness [Fu12b], the basic theory of CCS does generalize to many process calculi. The value-passing
CCS [Mil89a] adds to CCS the capacity to pass data values between processes.
In addition to the simple mechanism of synchronization, communications of values render it possible to control the interaction ﬂow by testing the received data
values. This additional control power signiﬁcantly enhances the expressive powerof the value-passing calculi. The name-passing calculus of Milner, Parrow andWalker [MPW92], the π-calculus, adopts the policy that the messages sent andreceived in communications can only be channel names. The exclusive focus on
the names has achieved both simplicity and expressiveness. It is diﬃcult to extend the name-passing mechanism to get a strictly stronger model. The processpassing calculi, or the higher order calculi [San93, Tho89, Tho93, Tho95], havetypically processes as the contents of communications. This seemingly powerful communication mechanism turns out to be much less expressive than the
Z. Liu, J. Woodcock, and H. Zhu (Eds.): He Festschrift, LNCS 8051, pp. 166–195, 2013.
c Springer-Verlag Berlin Heidelberg 2013


The Value-Passing Calculus

167

π-calculus [Fu12b]. To make use of what have been received through communications, variables (value variables, name variables, process variables) have to be
introduced to act as placeholders.
From a logic point of view, the name-passing calculi and the process-passing
calculi are preferable since they are closed models in the sense that the syntax
and the semantics of these calculi are independent of any models or logics. In
contrary the value-passing calculi, with strong motivation from practice, aredistinguished by the fact that they must refer to an ‘oracle’, be it a domain
model or a logic theory. The traditional treatment to the value-passing calculi
are not self-contained. The attentions have largely been on the process aspect of
the story. The oracles have never been formally deﬁned. The under-speciﬁcationof the value domain is not welcome from a foundational viewpoint, nor is it really
useful in practice.
The lightweight treatment of the oracle models/logics is an obstacle to boththeoretical study and application. We mention three immediate consequences.
1. Deep theoretical investigations are inevitably hindered by the open-ended
approach. For example it is not always possible to compare the expressivenessof a value-passing calculus to another concurrent model. An encoding of
the former into the latter would require that the value terms and the logic
expressions be fully speciﬁed.
2. For the same reason there is no way to implement a value-passing calculus,
no matter what is meant by an implementation.
3. An equivalence checking algorithm is out of the question since the existenceof such an algorithm depends on the algorithmic aspect of the oracle model
and/or the oracle logic, which is not available in the open-ended framework.
Apart from these problems, there are also a number of related subtleties thathave to be taken into account when designing a value-passing calculus. Let’s
illustrate these points by scrutinizing the process M (x) deﬁned by the following
recursive equality.
M (x) = if ϕ(x) then a(f (t)) else M (x + 1).

(1)

There are at least ﬁve questions one may ask about the process deﬁned in (1).
The ﬁrst is concerned with the nature of the oracle. Where are ϕ(x) and t coming
from? There are basically two answers.
1. The ﬁrst answer is model theoretical. The value term t and the logical expression ϕ(x) are constructed from the elements of the universe of a model,
the functions and the relations on the universe, and the variables that range
over the universe. The logical expression ϕ must be evaluated in the model
before process (1) ﬁres an action. If ϕ contains free variables, the evaluation
is done with respect to an assignment. Under the model theoretical interpretation, one expects that the process expression if y = y then P else Q can be
immediately put into action. On the other hand the behavior of the processexpression if y = z then P else Q depends on particular assignments.

168

Y. Fu

2. The second answer is proof theoretical. The value term t is deﬁned inductively from a vocabulary and the logical expression ϕ is legitimate in a ﬁrst
order theory on top of the vocabulary. The process expression in (1) can ﬁreif ϕ is a theorem of the theory.
In principle, a proof theoretical approach to oracle design should deﬁnitely be
preferred. The point is that all implementations of an oracle are proof theoreticalin nature. As the Incompleteness Theorem of Gödel [G3̈1] tells us, the set ofthe statements true in a model is far from being recursively enumerable. But animplemented system can only generate a recursively enumerable set of theorems.
The proof theoretical approach ﬁts very well with the operational nature ofprocess calculi.
The second question is about the expressiveness of the logical expressions
appearing in the value-passing processes. Since the set of the theorems of aﬁrst order theory is typically creative [Cut80], there is in general no eﬀective
procedure to decide the theoremhood of a formula. If a theory is reasonably
expressive, there exists some ﬁrst order logical expression ψ such that neither ψ
nor ¬ψ is provable. This is deﬁnitely unacceptable from a programming pointof view. To avoid the embarrassment caused by the Incompleteness Theorem,
one looks for decidable theories in which a sentence is either provably true orprovably false. In implementation one actually asks for more than decidability.
It has been shown that validity checking for a decidable theory could be super
exponential in complexity [FR74, Opp78]. So normally the logical expressions
admitted in a value-passing calculus are conﬁned to the quantiﬁer free formulas.
But this restriction does not entirely eliminate the problem. If ϕ contains the freevariables x1 , . . . , xn , then proving ϕ is equivalent to proving ∀x1 . . . . ∀xn .ϕ. There
are situations, for example in equivalence checking algorithm, where formulaswith free variables must be dealt with. This suggests to look for ﬁrst ordertheories that are considerably weaker than say Peano Arithmetic.
The third question is about the expressive power of the value terms admitted
in a value-passing calculus. Our value-passing calculus would be too strong if
the f appearing in (1) could be a non-computable function. The Church-Turing
Thesis asserts that all the functions deﬁnable in a value-passing calculus arecomputable functions if the functions produced by the oracles are computable.
It would be reasonable to disown those oracles that are capable of delivering noncomputable functions. Now here is the twist, if all the recursive functions canbe deﬁned within a value-passing calculus, is it necessary to have an oracle that
produces functions short-cutting the role of the deﬁnable functions? A negative
answer would imply that the oracle should only supply constructors for the value
terms; it should not introduce any functions that compute on the value terms.
The fourth question is about the functional separation between the calculi andthe oracles. The standard semantics of the value-passing calculi demands that thevalue term f (t) must be calculated to a canonical value before it is exported at
the name a. This additional calculating machinery is not very appealing from thepoint of view of an interaction model. In process calculi all calculations shouldbe achieved by interactions. In other words, the procedure of the calculation

The Value-Passing Calculus

169

should be explicitly speciﬁed in a process, not implicitly done by an oracle. It
is interesting to notice that the negative answer to the previous question is also
an answer to the present question since it trivializes the issue.
The ﬁfth question is about the level of abstraction of the value-passing calculi.
If n is the least natural number such that ϕ(n) holds according to an oracle,
then M (0) emits f (t) at the channel named a; otherwise M (0) is inactive. If
M (0) ever interacts, it need to consult the oracle for a ﬁnite number of times. If
M (0) never interacts, it must consult the oracle to evaluate ϕ(0), ϕ(1), ϕ(2), . . .
consecutively in a non-stop fashion. This phenomenon is familiar to higher orderprogramming languages, it is however alien to process calculi. The process M (0)has abstracted away too many computational and interactional activities, theexplicit descriptions of which are precisely what is expected of a process calculus.
If M (0) never interacts, the execution of M (0) in a higher order programming
language would result in a loop, a computational behaviour that is quite diﬀerent
from that of the command skip. However in the standard semantics of the valuepassing calculi M (0) is strongly bisimilar to 0. In a basic model processes like(1) should be banned.
The above discussions lead to the following design principle. A value-passing
calculus consists of a ﬁrst order theory and a labeled transition system. The
former provides both the value terms and the boolean expressions. The latter
deﬁnes the semantics of the value-passing processes. The calculus is designed bytaking the following into consideration.
1. To make sure that the ﬁrst order theory provides a right support to theoperational semantics, the theory is supposed to be complete for the set ofthe quantiﬁer free theorems.
2. To guarantee that the ﬁrst order theory does not interfere with the computations/interactions deﬁned by the labeled transition system, the formulas
admissible in a value-passing calculus should only contain constructors thatgenerate the universe of values; they should not contain any functions thatcompute on the elements of the universe.
3. To keep the value-passing calculi at the right level of abstraction, it would
be better not to deﬁne recursions by recursive deﬁnitions parameterized overvalue variables. The replication operator is suﬃcient.
The aim of this paper is to develop a rigid theory of the value-passing calculi
designed with the above remarks in mind. The theory is general enough so thatit can be readily applied to any particular value-passing calculus. It is also formal
enough so that many questions about the value-passing calculi can be addressed.
The paper is structured as follows. Section 2 reviews the relevant terminologies
in mathematical logic. Section 3 studies the operational and the observationalsemantics of the value-passing calculi. Section 4 takes a look at symbolic approximation to the absolute equality. Section 5 provides a proof system for the ﬁnite
terms. Section 6 discusses the expressiveness requirement for the value-passing
calculi. Section 7 applies the methodology to the value-passing calculus VPC deﬁned over the Peano Arithmetics. Section 8 concludes with discussions on future
research.

170

Y. Fu
BA
P {P1 /X1 , . . . , Pn /Xn }P is a tautology
EQ1
t=t
EQ2
s=t⇒t=s
EQ3
r =s∧s=t ⇒r =t

CG1 ki=1 ti = ti ⇒ f(t1 , . . . , tk ) = f(t1 , . . . , tk ) f is a k-ary function
k
CG2 i=1 ti = ti ⇒ r(t1 , . . . , tk ) ⇒ r(t1 , . . . , tk ) r is a k-ary relation
FO1∀x.φ ⇒ φ{t/x}FO2
φ ⇒ ∀x.φ
x not in φFO3(∀x.(ϕ ⇒ ψ)) ⇒ (∀x.ϕ ⇒ ∀x.ψ)Fig. 1. Logical Axioms of Σ

2

Decidable Theory

Let N be the set of natural numbers. A vocabulary Σ = (F, R, a) consists of two
disjoint nonempty countable sets and one function: F is a ﬁnite set of function
symbols; R is a ﬁnite set of relation symbols; and a : F ∪ R → N is an arity
function that maps an element of F onto a natural number and an element of R
onto a nonzero natural number. A symbol in F ∪ R is k-ary if it is mapped onto
k under a. A constant is a 0-ary function symbol. It is always assumed that F
contains at least one constant and that R contains the equality relation =.
For each vocabulary Σ there is a countable set VΣ = {x, y, z, . . .} of Σvariables. The set TΣ of Σ-terms, ranged over by r, s, t, is deﬁned as follows:– VΣ ⊆ TΣ .
– If f is a k-ary function symbol and t1 , . . . , tk are Σ-terms, then f(t1 , . . . , tk )is a Σ-term.
A Σ-term is closed if it does not contain any Σ-variable, it is open otherwise.
The set of closed Σ-terms is denoted by T0Σ .
The set EΣ of Σ-expressions, ranged over by φ, ϕ, ψ, is deﬁned as follows:– The logical false ⊥ is a Σ-expression.
– If r is a k-ary relation symbol and t1 , . . . , tk are Σ-terms, then r(t1 , . . . , tk )is an atomic Σ-expression.
– If ϕ, ψ are Σ-expressions, then ϕ ⇒ ψ is a Σ-expression.
– If φ is a Σ-expression and x is a Σ-variable, then ∀x.φ is a Σ-expression,
where ∀ is the universal quantifier.
The Σ-variable x in ∀x.φ is bound. A Σ-variable is free if it is not bound. A
Σ-sentence is a Σ-expression that does not contain any free Σ-variables. The
set of Σ-sentences is denoted by E0Σ . A boolean Σ-expression is a quantiﬁer
free Σ-expression. In sequel we shall freely use the derived logical connectives
, ¬, ∧, ∨, ⇔, ∃.
The first order logic over Σ is the recursive set of the first order logical axioms
deﬁned in Fig. 1. The axiom schema BA actually stands for a recursive set ofboolean axioms, each obtained from a boolean tautology by instantiating all the
propositional variables. The EQ-axioms are about the equivalence property, andThe Value-Passing Calculus

171

PA1
∀x.(s(x) = 0)
PA2∀xy.(s(x) = s(y) ⇒ x = y)PA3∀x.(x = 0 ∨ ∃y.s(y) = x)PA4∀x.(x < s(x))
PA5∀xy.(x < y ⇒ s(x) ≤ y)PA6∀xy.(¬(x < y) ⇔ y ≤ x)
PA7 ∀xy.((x < y) ∧ (y < z) ⇒ x < z)
Fig. 2. First Order Theory PA

the CG-axioms formalize the congruence property. The FO-axioms state theprovability of the universally quantiﬁed Σ-expressions. In both BA and FO1 themeta operation substitution is used.
Given a recursive set Γ of Σ-expressions, a proof of ψ from Γ is a ﬁnite
sequence (φ1 , . . . , φn ) of Σ-expressions such that φn is ψ and one of the following
properties holds for each i ≤ n:
– φi is a logical axiom;– φi ∈ Γ ;– There are two Σ-expressions ϕ and ϕ ⇒ φi in the proof (φ1 , . . . , φi−1 ).
A Σ-expression ψ is a Γ -theorem, notation Γ  ψ, if there is a proof of ψ from Γ ,and it is a theorem, notation  ψ, if Γ is the empty set. A set Γ of Σ-expressions
is inconsistent if Γ  ⊥; it is consistent otherwise. We sometimes write s =Γ t
for Γ  s = t.
A first order theory over Σ is a consistent recursive set Th of Σ-sentences, theelements of Th are called nonlogical axioms.
In the context of present paper the most useful ﬁrst order theory is Presburger
Arithmatic [Pre29]. This is what one gets if the multiplication operator ‘×’ isremoved from the Peano Arithmetic. For the reasons explained in Section 1 weshall also leave out the addition operator ‘+’. The axioms of our theory PA are
given in Fig. 2, in which x = y stands for ¬(x = y) and x ≤ y for x = y ∨ x < y.
For a natural number i, let i denote the numerals(s(. . . s(0) . . .)).
  
i times

Similarly we write si (x) for the open ΣPA -terms(s(. . . s(x) . . .)).
  
i times

Presburger [Pre29] proved that remarkably his arithmetic, and consequently thetheory PA deﬁned in Fig. 2, is decidable. This is the foundation for the valuepassing calculi studied in the rest of the paper.
Theorem 1. PA is decidable.

172

3

Y. Fu

Value-Passing Calculus

According to our discussions in Section 1, we shall focus on the value-passing
calculi deﬁned in terms of decidable ﬁrst order theories. Throughout this paper
we assume that Th is a decidable ﬁrst order theory of type Σ. The value-passing
calculus deﬁned on top of Th is denoted by VPCTh . If Th is PA, the subscript in
VPCTh is omitted. The abbreviation will be justiﬁed in Section 7.
All process calculi are deﬁned in terms of names. The set N of names isranged over by a, b, c, d, e, f, g, h. The set N of conames is {a | a ∈ N }. A
TΣ whose domain of deﬁnition is ﬁnite.
substitution is a partial map σ : VΣ
An assignment is a partial map ρ : VΣT0Σ whose domain of deﬁnition is
coﬁnite. A substitution is often denoted explicitly by {t1 /x1 , . . . , tn /xn }. The
notations ρ[x←t] and σ[x←t] are understood in the standard interpretation.
The set TVPCTh of the VPCTh -terms, ranged over by R, S, T and their decorated
forms, is deﬁned by the following BNF:T :=ϕi a(x).Ti |ϕi a(ti ).Ti | T | T  | (c)T | ϕT | !a(x).T | !a(t).T,
i∈I

i∈I

set. The notawhereϕi is a boolean Σ-expression, andI is a ﬁnite indexingtion i∈{1,...,n} ϕi λi .Ti stands for either i∈I ϕi a(x).Ti or i∈I ϕi a(ti ).Ti . The
preﬁx a(x) is an input primitive that binds the Σ-variable (henceforth just variable) x, and the preﬁx a(t) is an output primitive. We write f v( ), respectively
bv( ), for the function that returns the set of the free variables, respectively thebound variables; and let v( ) be f v( ) ∪ bv( ). A VPCTh -term is closed if it does
not contain any free variables. Otherwise it is called an open VPCTh -term. A
closed VPCTh -term is also called a VPCTh -process. We write PVPCTh for the set of
the VPCTh -processes, ranged over by L, M, N, O, P, Q. For clarity we shall writedefA(x, y) = T for instance to indicate that A(x, y) is a shorthand for T with x, yas the only free variables. The notation A(s, t) denotes T {s/x, t/y}. The composition T | T  and the localization (c)T are standard constructions.
 We write

T
for
the
composition
T
|
T
|
.
.
.
|
T
.
The
VPC
-term
i
1
2
n
Th
1≤i≤n
i∈I ϕi λi .Ti
is a conditional guarded choice, and for each i ∈ I the component ϕi λi .Ti isa summand. The condition ϕi is often omitted if it is . There is essentially aunique guarded choice, noted 0, whose index set is the empty set. Often we write
ϕ1 λ1 .T1 + . . . + ϕn λn .Tn for i∈{1,...,n} ϕi λi .Ti . It should be remarked that ini∈I ϕi λi .Ti the constructor isi∈I ϕi λi . . The conditional ϕT is often written
as if ϕ then T . The two leg conditional if ϕ then S else T can be deﬁned by
ϕS | ¬ϕT . The VPCTh -term !ν.T is a guarded replication. We shall freely use theguarded ﬁxpoint terms of the form μX.E where X is a process variable whose
occurrences in E are all under some preﬁxes. The ﬁxpoint construction μX.E
can be encoded by (c)(E{c(z).0/X} | !c(r).E{c(z).0/X}), where c is fresh andr is a closed term. So the guarded ﬁxpoint operator does not introduce extra
expressive power [FL10]. A VPCTh -term is finite if it does not contain any occurrences of the replication operator; it is a finite control term if it contains only
the conditional guarded choice operator and the ﬁxpoint operator.

The Value-Passing Calculus

173

Actioni ∈ I,t ∈ T0Σ ,Th ϕi .

a(t)i∈I ϕi a(x).Ti −→ Ti {t/x}

a(ti )i∈I ϕi a(ti ).Ti −→ Ti

i ∈ I,ti ∈ T0Σ ,Th ϕi .

Compositiona(t)λS −→ S λS | T −→ S  | T
Localizationa(t)T −→ T 
S −→ S τS | T −→ S  | T 

λT −→ T λ(c)T −→ (c)T 
Condition

λT −→ T 
λϕT −→ T 

c is not in λ.

Th

ϕ.

Recursiona(t)!a(x).T −→ T {t/x} | !a(x).Tt ∈ T0Σ .

a(t)!a(t).T −→ T | !a(t).Tt ∈ T0Σ .

Fig. 3. Concrete Semantics

3.1

Concrete Semantics

In this section we deﬁne the so-called concrete semantics, which is given by thelabeled transition system in Fig. 3, where the symmetric versions of two composition rules have been omitted. Although the semantics is deﬁned for all VPCTh terms, only the behaviors of the VPCTh -processes are completely characterized.
If Th is the Peano Arithmetic PA, then under our semantics the VPCTh -term
if 0 ≤ x then a(0) can perform an action, but the obviously equivalent VPCTh term if x = 0 then a(0) else a(0) cannot do anything.
The reader must have noticed that the rule for the output preﬁx in our concrete semantics appears diﬀerent from the standard treatment. In the valuepassing calculi deﬁned in terms of a model [Mil89a], the term in an output preﬁx
must be calculated to a value, an element of the universe, before it is exported.
In our approach however the Σ-term is exported as it is. There are two reasons.
One is that at our abstract model, there is no way to talk about calculation ofterms. But the much more important reason, alluded in Section 1, is that thefunctional power of the oracle is undesirable. The ﬁrst order theory provides auniverse of values, whereas the value-passing calculus does the calculation. If wemaintain a separation between the Σ-terms and the calculations of the Σ-terms,
there is no need to calculate any closed Σ-terms since every closed Σ-term isalready a ‘value’.

174

Y. Fu

Let us see two examples. Let A be (a)(a(0) | μX.a(x).(a(s(x)) | (τ.X + b(x)))).
τ

τ

τ

τ

b(n)

A typical action sequence of A is A−→. . −→−→ −→ 0, where n ≥ 0. As
 −→ .
2n+1 times

this example shows, the calculation of the numeral is explicitly demonstrated.
The second example is about the encoding of the minimization operator. It is
given by (a)(a(0) | μX.a(x).(a(s(x)) | if ϕ then b(x) else τ.X)). Notice that if nonumerals satisfy ϕ then the process diverges.
τλWe write =⇒ for the reﬂexive and transitive closure of −→, and =⇒ for the
λcomposition =⇒−→=⇒.
3.2

Absolute Equality

A ﬁrst attempt to deﬁne the bisimulations for VPCTh is to reiterate the deﬁnition
λfrom the theory of CCS for all VPCTh -terms. This would require that S −→ S λshould be bisimulated by T =⇒ T  whenever S is bisimilar to T . Consider
however the VPC-terms a(0).S and if x = 0 then a(0).S else a(0).S. Intuitivelya(0)these two VPC-terms are equivalent. But the action a(0).S −→ S cannot be
simulated by any action of if x = 0 then a(0).S else a(0).S. There are two ways
to bypass the problem. One is to conﬁne our attention to processes. This would
be a reasonable choice if the operational semantics is formulated in a concretemanner. The other is to apply a symbolic approach, which would of course ﬁtvery well with the symbolic operational semantics. Before we take a look atthese two solutions, we shall apply to VPCTh the model independent approachdeveloped in [Fu12b]. The equality so obtained provides not only the intuition,
but also a standard to compare against.
Process equivalences are observational. A process is observable if it may interact with another process.
λDefinition 1. A process P is observable, notation P ⇓, if ∃λ, P  . P =⇒−→ P  .
Now whatever an observational equivalence is, it must not identify an observable
process with an unobservable process. Hence the next deﬁnition.
Definition 2. A binary relation R is equipollent if P ⇓ ⇔ Q⇓ whenever P RQ.
Now suppose two processes P, Q are observationally equivalent. A third process,say O, cannot detect any diﬀerence between P, Q by interacting with them. If
we think of it, the fact that O cannot tell P, Q apart is best interpreted assaying that P | O and Q | O are observationally equivalent. Now trivially, P and
Q cannot be distinguished by any process that does not interact at a particularchannel name, say c. If one looks at the same thing from another angle, one
easily sees that (c)P must be observationally equivalent to (c)Q as well.
Definition 3. A relation R is extensional if the following hold: (i) If LRM andP RQ then (L | P ) R (M | Q). (ii) If P RQ then (c)P R (c)Q for all c ∈ N .

The Value-Passing Calculus

175

If two processes are equivalent, they should be able to maintain the equivalence
after one thousand years. The minimal condition making sure that this canbe achieved is the bisimulation property of Milner [Mil89a] and Park [Par81].
Following the idea of Fu [Fu12b], we actually will use a stronger version of
the bisimulation introduced by van Glabbeek and Weijland [vGW89]. In thefollowing deﬁnition, the notation R−1 stands for the inverse of R.
Definition 4. A binary relation is a bisimulation if the following hold:τ

1. If QR−1 P −→ P  then one of the following statements is valid.
(a) Q =⇒ Q R−1 P  and Q R−1 P for some Q .
τ(b) Q =⇒ Q R−1 P for some Q such that Q −→ Q R−1 P  for some Q .
τ
2. If P RQ −→ Q then one of the following statements is valid.
(a) P =⇒ P  RQ and P  RQ for some P  .
τ(b) P =⇒ P  RQ for some P  such that P  −→ P  RQ for some P  .
A basic assumption in the theory of computation is that a divergent computation
is diﬀerent from a computation that terminates. Often time the probability fora real program to diverge is zero. For such a program, divergence is a potential,
not an inevitability. A condition that takes into account of this potentiality while
upholding the bisimulation property is what we call codivergence requirement.
It was ﬁrst proposed by Priese [Pri78].
Definition 5. A relation R is codivergent if the following statements are valid:
τ

τ

τ

τ

– If P RQ −→ Q1 −→ · · · −→ Qn −→ · · · is an infinite internal actionτsequence, then there must be some k ≥ 1 and P  such that P =⇒ P  R Qk .
τ
τ
τ
τ
−1
– If QR P −→ P1 −→ · · · −→ Pn −→ · · · is an infinite internal actionτsequence, then there must be some k ≥ 1 and Q such that Q =⇒ Q R Pk .
We have introduced four conditions for the equivalences on evolving processes,
which are minimal from the point of view of interaction and computation. We
turn these minimal conditions into deﬁning properties of process equality.
Definition 6. The absolute equality =Th is the largest reflexive, equipollent,
extensional, codivergent bisimulation on PVPCTh .
The well-deﬁnedness of Deﬁnition 6 is due to the fact that its deﬁning properties are stable under set unions. The deﬁnition is completely model independent
as long as we only consider those models that have the composition and localization operators and enjoy a dichotomy between the internal actions and theexternal interactions. From the point of view of equality reasoning, the absoluteequality is too abstract. It would be very helpful to work out an external characterization of the absolute equality. This is what we are going to do next for
VPCTh . Before that, we state a useful lemma about computation, the Bisimulation Lemma [Fu12b]. The property stated in the lemma is called X-property by
De Nicola, Montanari and Vaandrager [DNMV90].
Lemma 1. If P =⇒ P  =Th Q and Q =⇒ Q =Th P , then P =Th Q.

176

Y. Fu

Once the equality relation has been deﬁned, a formal classiﬁcation of the internal
actions can be given. We say that S evolves to T in a computation step, notation
τS → T , if S −→ T and S =Th T , and that S evolves to T in a change-of-stateιτinternal action, notation S −→ T , if S −→ T and S =Th T . The reﬂexive andtransitive closure of → will be denoted by →∗ .
The bisimulation property can now be deﬁned in a more informative way.
τ
If P =Th Q −→ Q , then the simulation by P could be vacuous if Q =Th Q ;ιotherwise it must take the form P →∗ P  −→ P  such that P  =Th Q anda(t)P  =Th Q . Similarly if P =Th Q −→ Q , then the simulation of the outputa(t)action must take the form P →∗ P  −→ P  such that P  =Th Q and P  =Th Q .
This is the external bisimulation property we shall deﬁne in the next section.
3.3

External Bisimulation

External bisimulations are meant to give an alternative characterization of theabsolute equality in terms of explicit simulation of every action. In addition
to the property of Deﬁnition 4, external bisimulations must explain how theexternal actions are bisimulated.
Definition 7. A codivergent bisimulation R on PVPCTh is a VPCTh -bisimulation
if the following statements are valid for every λ = τ .
λλ

1. If QR−1 P −→ P  then Q =⇒ Q −→ Q R−1 P  and P RQ for some Q , Q .
λλ2. If P RQ −→ Q then P =⇒ P  −→ P  RQ and P  RQ for some P  , P  .
The VPCTh -bisimilarity Th is the largest VPCTh -bisimulation.
By constructing the relation inductively from Th that closes up under composition and localization, one can easily prove the following lemma.
Lemma 2. The external bisimilarity Th is extensional.
The above lemma and the Bisimulation Lemma is the only thing we need toestablish Proposition 1, which proves the correctness of Deﬁnition 7.
Proposition 1. The relation Th coincides with the absolute equality =Th .
Proof. The inclusion Th ⊆=Th is immediate from Lemma 2. The proof of thereverse inclusion is standard using Bisimulation Lemma. Processes of the forma(x).if x = then c( ) else d( ) and of the form a( ) + a( ).c( ), with the namesc, d chosen properly, are crucial to deriving the external bisimulation property.
A detailed proof of a similar result in π-calculus is given in [FZ11].

Both the absolute equality and the external bisimilarity are relations on theprocesses. They can be extended to the VPCTh -terms in the standard manner.
Definition 8. S Th T if and only if Sρ Th T ρ for every assignment ρ whose
domain of definition is disjoint from bv(S | T ).
A standard argument suﬃces to show that the relation Th , and consequently
the relation =Th as well, is closed under all the process operations.
Proposition 2. The absolute equality is equivalent and congruent.

The Value-Passing Calculus
Actionλii∈I ϕi λi .Ti −→ϕi Ti

177

i ∈ I.

Composition
a(x)

a(t)

λ

S −→ϕ S λS | T −→ϕψ S  {t/x} | T 

S −→ϕ S τS | T −→ϕ S  | T
Localization

T −→ψ T 

λT −→ϕ T λ(c)T −→ϕ (c)T 
Conditionc is not in λ.

λT −→ϕ T 
λφT −→φϕ T 
Recursiona(x)!a(x).T −→ T | !a(x).Ta(t)!a(t).T −→ T | !a(t).T

Fig. 4. Symbolic Semantics

4

Symbolic Semantics

The absolute equality is not very convenient. Hennessy and Lin [HL95] address
the issue by introducing symbolic bisimulations. The advantage of the symbolic
approach is that it allows one to make full use of the decidable fragments of
the logics of the value-passing calculi when constructing equivalence checking
algorithms. In [HL95] the symbolic bisimilarity is deﬁned as general as possible
so that a coincidence result could be achieved. We shall be less ambitious in thispaper. Symbolic bisimilarity is in our opinion a decidable approximation of theabsolute equality. Our motivation for the symbolic bisimilarity is two folds: (i)the symbolic bisimilarity should be sound, meaning that it should be a subsetof the absolute equality; (ii) ideally the symbolic bisimilarity is complete on thedecidable subsets of the absolute equality. The latter is much more diﬃcult tocome by than the former.
To deﬁne the symbolic bisimulations, we need to introduce the symbolic operational semantics. This would not be a big issue had we dropped the conditionals. So the key is to deﬁne for instance the semantics of the VPCTh -term
if ϕ then a(0) else b(0) where the boolean Σ-expression ϕ contains free variables.
The symbolic semantics [HL95, HL96] solves the problem by introducing conditional actions. The syntax of a transition in the symbolic semantics is a tuple
λof the form T −→ϕ T  , formalizing the idea that T may perform the action λ

178

Y. Fu

under the condition that the boolean Σ-expression ϕ is a Th-theorem. The setof the action labels for the symbolic semantics is{a(x), a(t) | a ∈ N , x ∈ VΣ , t ∈ TΣ } ∪ {τ },also ranged over by λ. The labeled transition system is deﬁned in Fig. 4. Again
the symmetric versions of the composition rules have been omitted. The treatment of the input preﬁx is in a late style, which is better suited for algorithmic
investigations. The symbolic semantics is stable under substitution in the senseof the following lemma.
λλσ

Lemma 3. If S −→ϕ T then Sσ −→ϕσ T σ for every substitution σ. On theλother hand, if Sσ −→ϕ T  for some substitution σ, then there must exist someλλ, ϕ, T such that λ = λσ, ϕ = ϕσ, T  ≡ T σ and S −→ϕ T .
ττλWe will abbreviate −→ϕ1 . . . −→ϕn to =⇒ϕ1 ...ϕn , and =⇒ϕ −→ϕ =⇒ϕ toλ=⇒ϕϕ ϕ . We remark that T =⇒ T .
It’s time to look at some examples. The following three terms are in VPC:
def

L(y) = if 0 ≤ y then b(0),def

M (y) = (a)(a(0) | μX.a(x).(a(s(x)) | (τ.X + if y = x then b(0)))),def

N (y) = (a)(a(0) | μX.a(x).(a(s(x)) | (τ.X + if y = x then b(y)))).
b(0)The process L(y) may perform only one action L(y) −→0≤y 0. The process M (y)τb(0)

has an interesting action sequence M (y) =⇒ −→y=n 0. Similarly N (y) has aτb(y)similar action sequence N (y) =⇒ −→y=n 0. In the second and third examples
the set of possible conditions is {y=0, y=1, y=2, . . . , y=n, . . .}. What the second
example tells us is that even with a ﬁnite description and a ﬁnite set of potential
external actions, the set of the conditions that enable an action of a VPC-term,
like b(0), could be inﬁnite.
The symbolic semantics is a correct extension of the concrete semantics. Thisis established in the next two lemmas whose proofs are simple induction onderivation.
Lemma 4. The symbolic semantics is sound with respect to the concrete semantics in the following sense:ττ(i) If S −→ϕ T for some Th-theorem ϕ then S −→ T .
a(t)

a(t)

(ii) If S −→ϕ T for some Th-theorem ϕ and some t ∈ T0Σ then S −→ T .
a(x)

a(t)

(iii) If S −→ϕ T for some Th-theorem ϕ then S −→ T {t/x} for every t ∈ T0Σ .
Lemma 5. The symbolic semantics is complete with respect to the concrete semantics in the following sense:ττ(i) If S −→ T then S −→ϕ T for some Th-theorem ϕ.

The Value-Passing Calculus
a(t)

179

a(t)

(ii) If S −→ T then S −→ϕ T for some Th-theorem ϕ.
a(t)

a(x)

(iii) If S −→ T then S −→ϕ T  for some Th-theorem ϕ and some x, T  suchthat T ≡ T  {t/x}.
4.1

Symbolic BisimulationτIn the symbolic approach, is it reasonable to require that S −→ϕ S  be simulated
by T =⇒ϕ T  for bisimilar S and T such that Th  ϕ ⇒ ϕ ? Again let’s take alook at the VPC-terms ϕτ.S and if x = 0 then ϕτ.S else ϕτ.S, where x ∈ f v(ϕ).
τ
The two VPC-terms are equivalent by all reasonable criteria. But ϕτ.S −→ϕ S
cannot be simulated by if x = 0 then ϕτ.S else ϕτ.S in the above requiredmanner since in the latter term the τ -action can only be ﬁred under a condition
strictly stronger than ϕ. But notice that (x = 0) ∧ ϕ ∨ (x = 0) ∧ ϕ ⇔ ϕ is aPA-theorem. Under either (x = 0) ∧ ϕ or (x = 0) ∧ ϕ the VPC-term if x =0 then ϕτ.S else ϕτ.S may evolve into S. This leads to the idea of ﬁnding acollection of boolean expressions such that the disjunction of the collection is
weaker than ϕ. If under each of the conditions the simulation can be done, thenthere is a simulation. A ﬁrst attempt to deﬁne a symbolic counterpart of theMilner-Park bisimilarity could be as follows:
A symmetric relation R on TVPCTh is a ?-bisimulation if the following
condition is met whenever SRT :λiλIf S −→ϕ S  then there is a class {T =⇒ϕi Ti }i∈I such thatTh  ϕϕi ⇒ λ = λi and (ϕϕi S , ϕϕi Ti ) ∈ R for every i ∈ I.
Let ? be the largest ?-bisimulation.
In the above deﬁnition, λ = λi stands for  if λ, λi are syntactically the same;
it is t = t if λ ≡ a(t) and λi ≡ a(t ) for some name a; otherwise λ = λistands for ⊥. The relation ? is not very useful. Consider the VPC-processes
R(y), S(y), T (y) deﬁned as follows:def

R(y) = (b)(b(y) | μX.b(z).r(z).if 0 < z then (b(p(z)) | X)),
def

S(y) = τ.T (y) + if 0 ≤ y then τ.R(y),def

T (y) = (a)(a(0) | μX.a(x).(a(s(x))| (τ.X + if 0 ≤ y ≤ x then τ.(if y = x then τ.R(y) else e(0))))).
In the deﬁnition of R(y) the term p(z) is the predecessor of z. The predecessor
function can be implemented in VPC. The details can be found in Section 6.
The behavior of R(y) is captured by the following action sequence:
τ

r(n)

τ

r(n−1)

ττr(1)R(n) −→ −→ =⇒0<n −→  =⇒0<n−1 . . . =⇒0<1 −→ . . . .
It is obvious that R(n) and R(n ) are inequivalent whenever n = n . The proτcesses S(y) and T (y) are bisimilar since the action S(y) −→0≤y R(y) can be

180

Y. Fu

def

U (y) = τ.W (y) + if 0 ≤ y ≤ m then τ.R(y),def

V (y) = τ.W (y) + if y = 0 then τ.R(y) + . . . + if y = m then τ.R(y),def

W (y) = if 0 = y then τ.(if y = 0 then τ.R(y) else e(0))+ if 0 ≤ y ≤ 1 then τ.(if y = 1 then τ.R(y) else e(0))+ ...
+ if 0 ≤ y ≤ m then τ.(if y = m then τ.R(y) else e(0)).
Fig. 5. Non-transitivity of?

simulated by T (y) as long as y is instantiated by a numeral. On the other hand
it is easy to see that S(y) ? T (y). The only way to simulate the action is byτ
the collection {T (y) =⇒0≤y≤n if y = n then τ.R(y) else e(0)}n∈N . But noticethat if 0 ≤ y ≤ n then R(y) is not bisimilar to if 0 ≤ y ≤ n then (if y =n then τ.R(y) else e(0)). The relation ? has to be abandoned because it is
not transitive! Fig. 5 oﬀers a counter example. One has U (y) ? V (y) andV (y) ? W (y) but not U (y) ? W (y). It follows that U (y) ? W (y).
The symbolic bisimulations need be deﬁned in a more subtle way. The key ideaof Hennessy and his collaborators is that the partition of the condition underwhich the simulated action is ﬁred should not depend on the conditions underwhich the simulations are done. In their deﬁnition a partition of ψ is a collection{ψi }i∈I such that ψ ⇔ i∈I ψi , where the indexing set I could be as large as thesize of the model. The reason that they may resort to the all-powerful operator
is that they are using a meta logic about the oracle model. We will use a more
restricted approach. We insist that the symbolic semantics of a value-passing
calculus should only make use of the ﬁrst order logic by which the logical theoryof the calculus is deﬁned.
Definition 9. Suppose Th is a theory over Σ, V is a finite set of variables,and f v(ϕ) ⊆ V . A boolean Th-partition of ϕ on V is a finite set of boolean
Σ-expressions {ϕi }i∈I such that f v( i∈I ϕi ) ⊆ V , Th  ϕi ∧ ϕj ⇒ ⊥ if i = j,
and Th  ϕ ⇔ i∈I ϕi .
Let K(y) = (a)(a(0) | μX.a(x).(X | if x ≤ y then a(s(x)))). It admits the followingττττ
inﬁnite sequence K(y) −→ −→0≤y −→1≤y . . . −→n≤y . . .. Although every ﬁnite
subset of {, 0 ≤ y, 1 ≤ y, . . . , n ≤ y, . . .} is consistent, the inﬁnite sequence is a
fake. For every numeral n the process K(n) terminates. From the point of view ofthe model N, no assignment can satisfy all the ΣPA -expressions in {, 0 ≤ y, 1 ≤y, . . . , n ≤ y, . . .}. From the point of view of the ﬁrst order logic, no satisﬁable ΣPA expression implies all the ΣPA -expressions in {, 0 ≤ y, 1 ≤ y, . . . , n ≤ y, . . .}.
A faithful symbolic interpretation of divergence would make use of the inﬁnite
conjunction, which as we have argued, is not in line with the philosophy of thesymbolic approach. To get a glimpse of the complication of codivergence, take alook at H(y) = (a)(a(0) | μX.a(x).(X | if y ≤ x then a(s(x)))), which is a slight
modiﬁcation of the previous VPC-term. This term also admit an inﬁnite sequence

The Value-Passing Calculus
τ

τ

τ

181

τ

of τ -actions H(y) −→ −→y≤0 −→y≤1 . . . −→y≤n . . .. The inﬁnite sequence is notreal for H(1), H(2), H(3), . . . . But it is real for H(0). These examples suggest that
it is diﬃcult to give a nice symbolic description of the codivergence property ata general level. It should be remarked though that divergence is intrinsicallyan undecidable property. If our interest in symbolic semantics is conﬁned toautomatic veriﬁcation, the codivergence condition has to be dropped.
Definition 10. A symmetric relation R on TVPCTh is a symbolic bisimulation if
the following hold whenever SRT and V = f v(S | T ):τ

1. If S −→ϕ S  and Th∪{ϕ} is consistent, then there are a boolean Th-partition{ϕi }i∈I of ϕ on V and a collection {T =⇒ψi Ti }i∈I such that, for each i ∈ I,
Th  ϕi ⇒ ψi and ϕi S R ϕi Ti , and one of the following properties holds:(a) ϕi S  R ϕi Ti ;τ(b) Ti −→ψi Ti for some ψi , Ti such that Th  ϕi ⇒ ψi , and ϕi S  R ϕi Ti .
a(t)2. If S −→ϕ S  and Th∪{ϕ} is consistent, then there are a boolean Th-partitiona(ti ){ϕi }i∈I of ϕ on V and a collection {T =⇒ψi Ti −→ ψi Ti }i∈I such thatTh  (ϕi ⇒ ψi ψi ) ∧ (ϕi ⇒ t = ti ), and moreover ϕi SRϕi Ti and ϕi S  Rϕi Ti
for every i ∈ I.
a(x)3. If S −→ϕ S  and Th∪{ϕ} is consistent, then there are a boolean Th-partition{ϕi }i∈I of ϕ on V ∪{x} and a collectiona(x)T =⇒ψi Ti −→ψi Ti

Th  ϕi ⇒ ψi ψi , ϕi SRϕi Ti and ϕi S  Rϕi Ti for all i ∈ I.

such thati∈I

The symbolic bisimilarity sTh is the largest symbolic bisimulation.
In the above deﬁnition the requirement that Th ∪ {ϕ} being consistent is important. Without the condition the VPC-term if x = x then a(0) would bewrongfully distinguished from 0.
The main algebraic properties of sTh are summarized in the next proposition.
Proposition 3. The following statements about sTh are valid.
1. The relation sTh is an equivalence.
2. The relation sTh is a congruence.
3. If S sTh T then Sσ sTh T σ for every substitution σ.
Proof. (1) The proof of transitivity is routine and tedious. (2) The proof of thecongruence property is standard after demonstrating that, for every boolean
expression ϕ, S sTh T implies ϕS sTh ϕT . (3) Using Lemma 3 it is easy toshow that {(Sσ, T σ) | S sTh T } is a symbolic bisimulation. We need to makeuse of a meta theoretical result asserting that Th  ϕσ for every substitution σwhenever Th  ϕ, which is an easy consequence of FO1 and FO2.
The next technical lemma, whose simple proof is omitted, helps understandthe above deﬁnition. It is the symbolic version of the Stuttering Lemma of van
Glabbeek and Weijland [vGW89].

182

Y. Fu
τ

τ

τ

Lemma 6. Suppose T −→ϕ1 T1 −→ϕ2 T2 . . . −→ϕn Tn and ϕ ⇒ ϕ1 . . . ϕn .
Then ϕT sTh ϕTn implies ϕT1 sTh ϕT2 sTh . . . sTh ϕTn .
Now let’s take a look at some examples. Consider the following VPC-terms:
defE(y) = μX.if y = 0 ∨ y = 1 then b(y).X,
def

A(y) = E(y) | if y = 0 then b(y),def

B(y) = E(y) | if y = 1 then b(y).
b(y)

It is clear that A(y) sTh B(y). The action A(y) −→y=0 E(y) is simulated byb(y)the single action B(y) −→y=0∨y=1 E(y) | if y = 1 then b(y). This example showsthat the condition Th  ϕi ⇒ ψi in say (1) of Deﬁnition 10 should not be
strengthened to Th  ϕi ⇔ ψi .
The ﬁniteness of partition is a genuine restriction. Let’s see a counter example.
Consider the following VPC-terms:
def

F (y) = μX.a(x).(a(s(x)) | if y=x then b(x) else X),
defC(y) = if 0 ≤ y then b(y),def

D(y) = (a)(a(0) | F (y)).
b(n)τ

Typically D has the action sequence D(y) =⇒y=0∧...∧y=n−1 −→y=n . It is notb(y)diﬃcult to see that C(y) =Th D(y). The action C(y) −→0≤y 0 is simulated byb(n)τ

the infinite collection {D(y) =⇒y=0∧...∧y=n−1 −→y=n }n∈N . There is no ﬁniteb(y)collection that can simulate C(y) −→0≤y 0. So the symbolic bisimilarity sThcannot coincide with the absolute equality =Th even if divergence is ignored. It
is however a correct approximation of the absolute equality.
Theorem 2. Let S, T be finite VPCTh -terms. Then S =Th T if S sTh T .
Proof. Let R be the following binary relation(Sρ, T ρ)

S, T are ﬁnite, S sTh T andρ is an assignment such that bv(S | T ) ∩ dom(ρ) = ∅

.

a(t)

Suppose S sTh T and Sρ −→ P for some t ∈ T0Σ and some assignment ρ sucha(x)that bv(S | T ) ∩ dom(ρ) = ∅. Let V be f v(S | T ). By Lemma 5, Sρ −→ϕ S 
for some Th-theorem ϕ and some x, S  such that P ≡ S  {t/x}. By Lemma 3,a(x)there exist some ϕ, S1 such that ϕ ≡ ϕρ, S  ≡ S1 ρ and S −→ϕ S1 . By thedeﬁnition of symbolic bisimulation there are a boolean Th-partition {ϕi }i∈I of ϕa(x)on V ∪{x} and a collection T =⇒ψi Ti −→ψi Ti

such that Th  ϕi ⇒ ψi ψi ,i∈I

The Value-Passing Calculus

183

ϕi SRϕi Ti and ϕi S  Rϕi Ti for all i ∈ I. Now Th  ϕi ρ[x ← t] for some i ∈ I,
which in turn implies Th  ψi ψi ρ[x ← t], SρRTi ρ and S  ρ[x ← t] R Ti ρ[x ← t].
a(t)At the meantime notice that T ρ =⇒ Ti ρ −→ Ti ρ[x ← t] by Lemma 3 andLemma 4. Conclude that R is a bisimulation. The relation is also extensional by
Proposition 3. It is equipollent since the external actions are bisimulated.


5

Proof System

When conﬁned to the ﬁnite VPCTh -processes, one expects that the equality
can be mechanically checked. Often such an algorithm is based on a complete
equational system. For most value-passing calculi deﬁned in literature a selfcontained decidable procedure for equivalence checking is out of the question
since the logics/models are undecidable. For example, to check if ϕa(t).S =ϕa(t ).S holds, one has to check if ϕ ⇒ t = t is valid. An algorithm for checking
the equivalence of ﬁnite processes has to make use of an oracle that answers
every question on the validity of a logical formula. For a value-passing calculus
VPCTh studied in this paper, equivalence checking algorithms do exist.
In studying proof systems, a standard treatment is to remove the composition
operator using expansion law [HM85, Mil89a]. This is done at the expense of
introducing the unguarded choice operator ‘+’ whose semantics is deﬁned byλλ

S −→ϕ S 

T −→ϕ T λλS + T −→ϕ S 

S + T −→ϕ T 

The operator destroys the congruence property of process equalities. As a consequence additional complication is introduced to produce a congruence. We
avoid thecomplication by not using the congruence relation. In this section the
choice [Pal03, FL10].
notation i∈I ϕi λ
i .Si stands for a mixed Suppose S ≡
ϕ
λ
.S
and
T
≡
i∈I i i ij∈J ψj λj .Tj . The expansion law isformulated by the following equality:
S |T =

ϕi λi .(Si | T ) +

i∈I

+



λi =a(x)j∈Jϕi ψj τ.(Si {tj /x} | Tj )λj =a(tj )

λj =b(y)ψj λj .(S | Tj ) +ϕi ψj τ.(Si | Tj {ti /y}).

λi =b(ti )Our equational system ASTh consists of the ﬁrst order logic axioms deﬁned inFig. 1, the nonlogical axioms of Th, the equational axioms deﬁned in Fig. 6 andthe expansion law. We write ASTh  S = T if the equality S = T can be derived
R
within ASTh , and S = T if R is the major law used to derive the equality S = T .
Most of the laws are variants of the axioms proposed in previous studies on
the value-passing calculi [IL01] and the name-passing calculi [PS95]. The law S6
is a generalization of the following law proposed by Parrow and Sangiorgi [PS95]:
a(x).S + a(x).T = a(x).S + a(x).T + a(x).(ϕS + ¬ϕT ).

(2)

184

Y. Fu
S1
T +0 = T
S2
S+T = T +S
S3
R + (S + T ) = (R + S) + T
S4
T +T = TS5 
ϕT + ϕ T = (ϕ ∨ ϕ )T 
S6i∈I φi a(x).(¬ϕi Ti + ϕi τ.T ) = ϕa(x).T +i∈I φi a(x).(¬ϕi Ti + ϕi τ.T )if Th ϕi ⇒
 φi for all i ∈ I and
Th ϕ ⇔ i∈I ϕi .
C1[⊥]T = 0
C2[]T = TC3
ϕa(t).T = ϕa(t ).T , if Th ϕ ⇒ t = tC4
ϕλ.T = ϕλ.ϕT
C5φ(T + T  ) = φT + φT  ,C6
ϕT = ψT , if Th ϕ ⇔ ψ
C7
ϕ(ψT ) = (ϕψ)TL1(c)0 = 0L2(c)λ.T = 0, if c is in λL3(c)λ.T = λ.(c)T , if c is not in λL4(c)(T + T  ) = (c)T + (c)T L5(c)ϕT = ϕ(c)TB
λ.(S + T ) = λ.(τ.(S + T ) + T )Fig. 6. Axiom for Finite VPCTh -Term

As pointed out in [PS95], this is the law that tells apart the early equivalence
and the late equivalence [MPW92]. The combination of the S-laws has powerfulconsequences, two of which are given by the following lemmas.
Lemma 7. ASTh  ψλ.T = ϕλ.T +ψλ.T if Th  ϕ ⇒ ψ.
Lemma 8. ASTh  ϕ(λ.T ){t/x} = ϕ(λ.T ){t /x} if Th  ϕ ⇒ t = t .
The B-law is due to van Glabbeek and Weijland [vGW89]. It implies Milner’s
ﬁrst tau law λ.τ.T = λ.T and a weaker form τ.(T + ϕτ.T ) = τ.T of Milner’s
second tau law [Mil89a].
The veriﬁcation of soundness property of ASTh is routine.
Lemma 9. If ASTh  S = T then S sTh T .
A nice property of a proof system is that it allows one to focus on terms in somespecial form.
Definition
11. A finite VPCTh -term is a normal form if it is either 0 or of theform i∈I ϕi λi .Ti such that Ti is a normal form for every i ∈ I.
Using L4 and L5 one can pull all the localization operations in a term to thevery front. Then one may remove all the composition operations by applying
the expansion law. And ﬁnally one removes the localization operations using theL-axioms. What one gets is a normal form term. Hence the following lemma.

The Value-Passing Calculus

185

Lemma 10. For each finite VPCTh -term T there is some normal form T  suchthat ASTh  T = T  .
In the rest of the section the following Completeness Theorem is proved.
Theorem 3. S sTh T if and only if ASTh  τ.S = τ.T .
τ

Proof. A sequence T =⇒ϕ T  is maximal with regards to φ if (i) Th  φ ⇒ ϕ,τ(ii) φT sTh φT  , and (iii) there does not exist any T  such that T  −→ϕ T  ,τTh  φ ⇒ ϕ and φT sTh φT  . Intuitively T =⇒ϕ T  is maximal if T  cannot
evolve to another state that stays equal to T under the condition φ.
s
We conﬁne our attention
to the normal
 forms. Suppose S Th T and S, T arethe normal forms i∈I ϕi λi .Si and j∈J ψj λj .Tj respectively. We shall provethat the following properties hold for the normal forms:
τ(S) If Th  φ ⇒ ϕ, φT sTh φT  and T =⇒ϕ T  is maximal with regards to φ,then ASTh  τ.T = τ.(T + φT  ).
(P) If φT sTh φS, then ASTh  φτ.T = φτ.(T + S) = φτ.S.
Let’s write dep(T ) for the maximal nested depth of preﬁxing operation of T .
Our proof strategy will be as follows:
1. Prove (S) assuming that (S) and (P) hold for terms with depths less than i.
2. Prove (P) assuming that (P) holds for terms whose depths are less than iand that (S) holds for terms whose depths are less than or equal to i.
The inductive proof of (S) is given as follows: Suppose T is a normal form ofτττ
depth i and T −→ϕ1 T1 −→ϕ2 . . . Tn−1 −→ϕn Tn is maximal with regards tos
ϕ with ϕT1 Th ϕTn and ϕ = ϕ1 . . . ϕn . Then ϕT1 sTh ϕT2 sTh . . . sTh ϕTn
by Lemma 6. By the induction hypothesis on (P), ASTh  ϕτ.T1 = ϕτ.Tn . By
Lemma 7, ASTh  τ.T = τ.(T + ϕ1 τ.T1 ) = τ.(T + ϕτ.T1 ) = τ.(T + ϕτ.Tn ). SinceτττT −→ϕ1 T1 −→ϕ2 . . . Tn−1 −→ϕn Tn is maximal, the action of each summandψj λj .Tj of T can be simulated by a set of summands of Tn using induction
hypothesis, and consequently ψj λj .Tj can be assimilated by Tn . We conclude
that ASTh  ϕτ.Tn = ϕτ.(Tn + T ). Consequently
ASTh  τ.T=

τ.(T + ϕτ.(Tn + T ))S5

ϕτ.(T + ϕτ.(Tn + T )) + ¬ϕτ.(T + ϕτ.(Tn + T ))=C laws=ϕτ.(T + τ.(Tn + T )) + ¬ϕτ.TB=

ϕτ.(T + Tn ) + ¬ϕτ.(T + ϕTn )S5

ϕτ.(T + ϕTn ) + ¬ϕτ.(T + ϕTn )

=

S5

=

τ.(T + ϕTn ).

We turn to the inductive proof of (P). By the C-laws we only have to prove
the special case when φ = . Consider a summand ϕi λi .Si of S. The action

186

Y. Fu


λi
i∈I ϕi λi .Si −→ϕi Si must be simulated by the termj∈J ψj λj .Tj . There arethree cases according to the shape of λi . We only consider the case λi = a(x).
By deﬁnition there are a boolean Th-partition {ϕki }k∈K of ϕi on f v(S | T ) ∪ {x}a(x)and a collection {T =⇒ψk Tk −→ψk Tk }k∈K such that Th  ϕki ⇒ ψk ψk for allk ∈ K, and ϕki S sTh ϕki Tk , ϕki Si sTh ϕki Tk for every k ∈ K. We assume that foreach k ∈ K, T =⇒ψk Tk is maximal with regards to ϕki . By induction on (P),

ASTh  ϕki τ.S = ϕki τ.Tk ,(3)

ASTh  ϕki τ.Si = ϕki τ.Tk

(4)

a(x)

for every k ∈ K. Since {T + S =⇒ψk Tk −→ψk Tk }k∈K , we could have thefollowing rewriting that makes use of the inductive hypothesis on (S).
⎛I.H.

τ.(T + S) = τ. ⎝T + S += τ. ⎝T + S +C5= τ. ⎝T + S +B= τ. ⎝T + S +⎛S5= τ. ⎝T + S +⎛(4)= τ. ⎝T + S +⎛= τ. ⎝T +⎛I.H.

= τ. ⎝T +⎞ψk (Tk + ψka(x).Tk )⎠ψk Tk +

k∈K⎛

= τ. ⎝T +


k∈K

⎛

S6

ψk Tk ⎠

k∈K

⎛

⎛

⎞





⎞




ψk ψk
a(x).Tk ⎠k∈Kψk Tk +



k∈K

k∈K





ψk Tk +k∈Kψk Tk +

i ∈I\{i}i ∈I\{i}i ∈I\{i}

⎞


k
 ⎠
ψk ψk
a(x).(¬ϕki τ.Tk + ϕi τ.Tk )

k∈K

k∈K

⎞

ψk ψk
a(x).τ.Tk ⎠

⎞

k

k
ψk ψk a(x).(¬ϕi τ.Tk + ϕi τ.Si )⎠k∈Kϕi λi .Si +ψk Tk +k∈Kϕi λi .Si +
⎞

⎞



k
⎠
ψk ψk
a(x).(¬ϕki τ.Tk + ϕi τ.Si )k∈Kψk Tk ⎠k∈K

ϕi λi .Si ⎠ .

It follows from induction that τ.(T + S) = τ. T +and soem {φi }i∈I  . Let φ = i∈I  φi . Then
τ.(T + S)

⎞



S5

=

S5,C2

=

C laws,B

=

S5,C2

=



i∈I  φi τ.Tfor some I  ⊆ I

τ. (T + φτ.T )φτ. (T + φτ.T ) + ¬φτ. (T + φτ.T )φτ.T + ¬φτ.T
τ.T.

Symmetrically ASTh  τ.(S + T ) = τ.S. We are done.

The Value-Passing Calculus

6187

Turing CompletenessThe value-passing calculi are rudimentary process models. The question concerning their expressiveness has to be settled. Which value-passing calculi arefor instance complete in the sense that all recursive functions [Rog87] are deﬁnable? To answer the question we need to make it clear how the natural numbers
are deﬁned in a value-passing calculus. From the operational point of view, a natural number system is not just an inﬁnite set of pairwise distinct closed Σ-terms,
but also an eﬀective way of generating these Σ-terms.
Definition 12. A numeric system for VPCTh consists of a countable subset
{
0, 
1, 
2, . . . , n
, . . .} of T0Σ and a VPCTh -term Sd (x) that satisfy the followings:
1. The variable x is the only free variable appearing in Sd (x).
2. Th  p = q for all p, q ∈ N such that p = q.


d(n
+1)

n) is of the form Sd (n) =⇒ −→ =Th 0.
3. Every action sequence of Sd (It is clear from (3) of Deﬁnition 12 that every action sequence of Sd (n) is actuallyd(n+1)n) →∗ −→ =Th 0 and Sd (n) =Th d(n
+ 1).
of the form Sd (Using a numeric system, we may talk about functions in a value-passing calculus. The predecessor function p for instance can be deﬁned in such a calculus.
Suppose we would like to have the VPC-process a(x).b(p(x)). It can be deﬁnedby a(x).(c)(c(0) | !c(y).if x = s(y) then b(y) else c(s(y))). The process diverges
when given the input 0. As is demonstrated by this example, each application of
the predecessor function is implemented by an additional VPC-term. In sequel
we shall make use of the predecessor function without worrying about how aparticular occurrence of the function is implemented.
An n-ary partial function f (x1 , . . . , xn ) is definable in VPCTh with respect tothe numeric system {
0, 
1, 
2, . . . , n
, . . .}, Sd (x) if, for all names a1 , . . . , an , b, there
is a process I(a1 , . . . , an , b) of the form a1 (x1 )....an (xn ).T such that (i) if f (p1 , . . . ,pn ) is deﬁned, then all the action sequences of T {p1/x1 , . . . , pn /xn } are ﬁnite and
b(
p)


are of the following form T {p1 /x1 , . . . , pn /xn } =⇒−→ T =Th 0, where p =f (p1 , . . . , pn ); and (ii) if f (p1 , . . . , pn ) is undeﬁned, then T {p1/x1 , . . . , pn /xn } canonly perform τ -action sequences and all its τ -action sequences are divergent. We
say that f (x1 , . . . , xn ) is deﬁned by I(a1 , . . . , an , b) at a1 , . . . , an , b. A set of partial
functions is deﬁnable with respect to a numeric system if every member of the set
is deﬁnable with respect to the numeric system. A set of partial functions is deﬁnable in VPCTh if it is deﬁnable with respect to some numeric system of VPCTh .
If a function is deﬁnable in VPCTh with respect to {
0, 
1, 
2, . . . , n
, . . .}, Sd (x),we can design a procedure that, upon receiving the natural numbers p1 , . . . , pn ,traverses the derivation tree of T {p1 /x1 , . . . , pn /xn }. This is well deﬁned since
every VPCTh -term is ﬁnite branching. The procedure terminates with the result
 at some b. It diverges otherwise. According
p if T {p1/x1 , . . . , pn /xn } export p
to the Church-Turing Thesis, this procedure deﬁnes a recursive function. We
conclude that all functions deﬁnable in a value-passing calculus are recursive.

188

Y. Fu

The opposite question asks if all the recursive functions can be deﬁned in avalue-passing calculus. This amounts to asking if the value-passing calculus is
Turing complete.
Definition 13. A value-passing calculus VPCTh is Turing complete if all therecursive functions are definable in VPCTh .
The next proposition provides a basic fact about the expressiveness of the valuepassing calculi.
Proposition 4. A value-passing calculus VPCTh is Turing complete if and only
if it has a numeric system.
Proof. The implication in one direction is clear. Now suppose VPCTh has anumeric system {
0, 
1, 
2, . . . , n
, . . .}, Sd (x). We show that the recursive functions [Rog87] are deﬁnable in VPCTh . We consider only two cases.
– Suppose G(c1 , . . . , cn , d, e, b)) and H(c1 , . . . , cn , b) are the interpretations of
two recursive functions. The interpretation F (a1 , . . . , an+1 , b) of the recursion function at a1 , .., an , an+1 , b is
a1 (x1 ). · · · .an+1 (xn+1 ).(f )(f (0, 1, xn+1 , 0) | (c)(!c1 (x1 ) | · · · | !cn (xn ) | Rec)),
where Rec stands for the following process!f (y, y  , z, v).if 
0 = y = z then H(c1 , . . . , cn , b)else if 
0 = y ∧ y  ≤ z then (e)(H(c1 , . . . , cn , e) | e(v).f (0, 1, z, v))else if 0 < y ∧ y = z then (d)(d )(G(c1 , . . . , cn , d, d , b) | d(y) | d (v))
else if 
0 < y ∧ y  < z then (d)(d )(e)(G(c1 , . . . , cn , d, d , e) | d(y) | d (v)| e(v).f (Sd (y), Sd (y  ), z, v).
– Suppose G(a1 , · · · , an+1 , b) is the interpretation of a recursive function. The
minimalization function is interpreted at a1 , .., an , an+1 , b by the process
a1 (x1 ). · · · .an+1 (xn+1 ).(a1 . . . an+1 )(!a1 (x1 ) | · · · | !an (xn ) | f (0) | !f (z).M u),
where M u is the following process
an+1 (z) | (c)(G(a1 , · · · , an+1 , c) | c(v).if v = 
0 then b(z) else f (Sd (z))).
We are done.

Proposition 4 adds weight to Deﬁnition 12 since a numeric system is intuitively
a minimal requirement for a value-passing calculus to simulate all the recursive functions. The VPCTh -term Sd (x) is nothing but an implementation of thesuccessor function.

7

VPC and Recursion Theory

The previous three sections have developed a rigorous theory for the valuepassing calculi. When applied to a particular decidable ﬁrst order theory, thisThe Value-Passing Calculus

189

general theory immediately generates an operational semantics and an observation theory for that calculus. We have studied only one decidable ﬁrst ordertheory, the theory PA deﬁned in Fig. 2. So in this section we take a closer lookat the value-passing calculus deﬁned on top of PA. We will write =VPC for theabsolute equality of VPC and sVPC for the symbolic bisimilarity of VPC.
According to our general setting, VPC should have a number of virtues. Let’ssummarize its key features:– VPC is Turing complete. So it is among the good value-passing calculi.
– The validity of the boolean propositions is known to be decidable. This is
the reason for us to see VPC as a programming language. Our familiarity
with the standard model N helps conﬁdence in programming with VPC.
– The simplicity of our Peano theory oﬀers a nice algebraic theory of VPC.
Formal comparison of VPC against other well known process calculi is not
only possible, but also instructive.
It is diﬃcult to think of a value-passing calculus that is weaker than VPC but
is still expressive enough. We now elaborate on this point.
To start with observe that the binary relation < is not absolutely necessaryfor VPC. The following proposition explains why.
Proposition 5. For each VPC-process P there is some VPC-process P  suchthat P =VPC P  and that P  contains no occurrence of the relation symbol <.
Proof. The basic idea is that the boolean value of a closed atomic ΣPA -expressiont < t can be calculated within VPC. Given a VPC-process P , we can translate
it into an equal VPC-process P  . The encoding is structural on composition,
localization and replication operators. The interpretation of the guarded choice
and the conditional are similar. We take a look at how the latter is translated.
defConsider the VPC-term S = if ϕ then T . The interpretation of S is given by
the following term(c)(ϕc | c(z).if z = 1 then T  )where T  is the interpretation of T and ϕc is structurally deﬁned as follows:– If ϕ is t = t , then ϕc is if t = t then c(1) else c(0).
– If ϕ is t < t , then ϕc is the following termd(t).e(t ) | !d(x).e(y).if y = 0 then c(0) else if x = 0 then c(1) else d(p(x)).e(p(y)).

– If ϕ is ϕ ∧ ϕ , then ϕc is(de)(ϕ d | ϕ e | d(y).e(z).if y = 1 ∧ z = 1 then c(1) else c(0)).
– If ϕ is ϕ ∨ ϕ , then ϕc is(de)(ϕ d | ϕ e | d(y).e(z).if y = 1 ∨ z = 1 then c(1) else c(0)).
The equality P =VPC P  holds in an obvious way.




190

7.1

Y. Fu

Minimality of VPC

In this section we prove that VPC plays an authentic role in all the Turing
complete value-passing calculi. Suppose {
0, 
1, 
2, . . . , n
, . . .}, Sd (x) is a numericsystem of a Turing complete model VPCTh . One could deﬁne a translation  Thfrom VPC to VPCTh using the ideas described in Fig. 7. The translation of theaction labels λTh can be deﬁned by⎧if λ = τ,⎨ τ,defn), if λ = a(n),λTh = a(⎩a(n), if λ = a(n).
Three aspects of the encoding call for explanation.
– One is that we have identiﬁed the set of the term variables of VPCPA withthe term variables of VPCTh .
– The second is that the operation Dc ( ) is deﬁned as follows: for a termt ≡ sk (x) with k > 0, Dc (t) is the following term(c0 )(c0 (x) | c0 (z0 ).(c1 )(Sc1 (z0 ) | c1 (z1 ).(. . . ck−1 (zk−1 ).Sc (zk−1 ) . . .))).
The idea is that the term sk (x), for k > 0, is translated to an elementof the numeric system {
0, 
1, 
2, . . . , n
, . . .}, Sd (x), achieved by counting theelements from x up to k + x using Sd (x).
– The third is that we have not given the encoding of choice term i∈I ϕi λi .Ti .
The reader can readily give it by himself/herself. It is simply a combination ofthe
encodings for the preﬁx terms and the conditional terms. The translationof 1≤i≤k ϕi λi .Ti takes the following form
(
c)(



Dc1 (t1i ) | . . . |i1≤i≤n1

Dck (tki ) | c11 (z11 ) . . . cknk (znkk ).

1≤i≤nkiϕi λi .Ti Th ),1≤i≤kwhere c = c11 . . . cknk .
It is easy to see that the translation is sound and complete with respect to theoperational semantics in the sense of the next proposition.
Proposition 6. Suppose P is a VPC-process that does not contain any occurrences of <. The following correspondences hold:
λTh

λ

(i) If P −→ P  then P Th →∗ −→ P1 =VPCTh P  Th for some VPCTh -process
P1 ;
λ

λ

(ii) If P Th −→ P1 then P −→ P  for some VPC-process P  and some λ suchthat P1 =VPCTh P  Th and λ Th = λ.
It is possible to strengthen Proposition 6. In fact the composition of therelation{(P, P Th ) | P is a VPC process}with =Th is a subbisimilarity. A subbisimilarity is a generalization of the absoluteequality from a binary relation on one model to a binary relation from one
calculus to another. See [Fu12b] for details.

The Value-Passing Calculus

191

def

0Th = 0,
defτ.T Th = τ.T Th ,def

a(x).T Th = a(x).T Th ,⎧if t ≡ n,⎨ a(n).T Th ,defa(x).T Th ,if t ≡ x,
a(t).T Th =⎩(c)(Dc (t) | c(z).a(z).T Th ), if t ≡ sl (x) for some l > 0;
def

S | T Th = STh | T Th ,def

(a)T Th = (a)T Th ,⎛if ϕ then T Th = (c1 . . . ck ) ⎝
def



⎞
Dci (ti ) | c1 (z1 ). · · · ck (zk ).if ϕ then T Th ⎠ ,


1≤i≤k

where ϕ ≡ ϕ {
n1 /n1 , . . . , n
j /nj }, ϕ ≡ ϕ {t1 /z1 , . . . , tk /zk },n1 , . . . , nj are the numerals in ϕ, and t1 , . . . , tk are the terms
in ϕ that are of the form sl (x) for some l > 0; we may regard
if ϕ then T Th as if ϕ then T Th ;def

!a(x).T Th = !a(x).T Th ,⎧if t ≡ n,⎨ !a(n).T Th ,def
if t ≡ x,!a(x).T Th ,!a(t).T Th =⎩(c)(Dc (t) | c(z).!a(z).T Th ), if t ≡ sl (x) for some l > 0.
Fig. 7. Encoding of VPC into Turing Complete VPCTh

Theorem 4. Suppose P, Q are VPC-processes that do not contain any occurrences of <. Then P =VPC Q if and only if P Th =VPCTh QTh .
Proof. In view of Proposition 1, we only have to prove the theorem for theexternal bisimilarities. Let R be the following relation
⎧
⎪
⎪
⎨

⎫
c is c1 , . . . , cj for some j; Pi is neither ⎪⎪⎬a composition nor a localization; and((c)(P1 | . . . | Pk ), (.
c)(Q1 | . . . | Qk ))Pi Th →∗ Qi , where Qi is obtained ⎪
⎪
⎪
⎪
⎩
⎭
from Pi Th by resolving the Dc  s.
Now R is a VPCTh -bisimulation up to strong bisimilarity [Mil89a]. Notice thatevery VPC-process is equal to a process of the form (c)(P1 | . . . | Pk ), where foreach i ∈ {1, . . . , k}, the process Pi is neither a composition nor a localization. So the translation  Th is correct for the VPC-processes that do not refer tothe relation ‘<’. The restriction can be removed according to Proposition 5. We
conclude that VPC is a submodel of every Turing complete VPCTh . In otherwords it is the least expressive among all Turing complete value-passing calculi.

192

8

Y. Fu

Conclusion

The present approach emphasizes that a value-passing calculus should be a selfcontained model of computation and interaction. The formal treatment of thelogic of the model comes with the decidability requirement. It has taken sometime to reach this level of formality. The study of Milner [Mil89a] was conducted
at an ad hoc manner. The semantics of his value-passing CCS is deﬁned bytranslating the model into the pure CCS with arbitrary choice operator. Hoare’s
deﬁnition of his famous CSP [Hoa78, Hoa85], which is a value-passing calculus,
is essentially algebraic. The operational semantics for CSP a la pure CCS is
introduced in [Bro83, BHR84, Ros97]. The labeled transition semantics for thevalue-passing CCS appears in [HI93a, HI93b]. A more serious attempt to study
the operational semantics of the value-passing calculi is reported in the seminal
paper by Hennessy and Lin [HL95]. The signiﬁcance of their work is that it
points out the indispensable role the ﬁrst order logic may play in the study ofthe semantics of the value-passing calculi. The present work can be seen as afurther step that completes the picture outlined by Hennessy and Lin [HL95].
The observational equality of this paper is an application of the universal
equality of Fu [Fu12b] to the value-passing calculi. This is an equality that differs from any equalities that have been proposed for the value-passing calculi.
The algebraic theory of CSP has been extensively studied [BHR84, Ros97], withparticular emphasis on the trace and failure semantics. In the literature on CSP,
it is popular to see a set of algebraic laws as providing an axiomatic semantics. The algebraic theory of the value-passing calculi has been studied withmotivation from the denotational semantics [Hen91, HI93a, HI93b]. The observational equivalence, the weak bisimilarity, and its symbolic characterization
is systematically studied in [HL95]. Proof systems for these equivalences havealso been studied in [Hen91, HI93a, HI93b, HL96]. These systems are parameterized over proof systems for the logics of data domains. The decidability of
our equation system ASTh compares favorably to these systems. The algorithmic aspect of the equivalence checking for the value-passing calculi is elaboratedin [Lin93, Lin96, Lin98]. Our treatment to the value-passing calculi may cast newlight on the equivalence checking algorithms for the value-passing processes. A
survey of the symbolic approach is given by Ingolfsdottir and Lin [IL01].
Our formalization of the value-passing calculi makes it possible to carry out areﬁned study on the expressiveness of these models. There have been early eﬀorts
that attack the expressiveness issue. See for example [Pal03, FL10]. However it isfair to say that none of the results obtained so far is conclusive. In this paper wehave studied the absolute expressiveness of the value-passing calculi by characterizing the Turing complete value-passing calculi in terms of the numeric systems.
We have also studied the relative expressiveness of the value-passing calculi. It
is shown in this paper that VPC is the least expressive value-passing calculus.
The minimality result sheds new light on the value-passing calculi studied byprevious researchers, all of those models being informal variants of VPC. It is
worth remarking that VPC is strictly less expressive than the π-calculus [Fu12b]
and is strictly more expressive than the Interactive Machine Model [Fu12b].

The Value-Passing Calculus

193

We have emphasized the importance of conﬁning our attention to the decidable fragment of the ﬁrst order logic. The tradeoﬀ is that sTh is much stronger
than =Th . A challenging task is to prove or disprove that sTh and =Th coincideon the ﬁnite control VPCTh -terms. But a more urgent problem is the following.
Problem 1. Does sVPC coincide with =VPC on the ﬁnite VPC-terms?
The symbolic bisimilarity studied in this paper is the simplest of its kind. It is too
defstrong for the inﬁnite state processes. Consider for example the process A0 =defa(x).if x is even then b(x) + a(x).if x is odd then b(x) and the process A1 =a(x).b(x) + a(x).if x is even then b(x) + a(x).if x is odd then b(x). An implementation of if x is even then b(x) is (c)(c(0) | !c(y).if x = y then b(x) else c(s(s(y)))).
The term if x is odd then b(x) is deﬁned similarly. It is clear that A0 =VPC A1 .
a(x)On the other hand A0 sVPC A1 . The transition A1 −→ b(x) can be simulated by A0 . There is however no boolean PA-partition on {x} that witnesses
the simulation. If we relax on the boolean restriction, then intuitively the set{∃z.x = 2 ∗ z, ∃z.x = 2 ∗ z + 1} forms a ‘partition’. In order to carry out investigation along this line, the symbolic approach must be modiﬁed in a couple of ways.
Firstly the proper power of the Peano system should be retained. Speciﬁcallythe addition operator ‘+’ and the multiplication operator ‘∗’ are necessary to
produce much more powerful speciﬁcations. Secondly the symbolic bisimilarity
should be deﬁned by a family of relations indexed by the ﬁrst order formulas [HL95, IL01]. The introduction of the arithmetic operators does not change
the grammar of VPC. No VPC-terms would contain any arithmetic operators.
So the logic expressions of VPC are still decidable. The extra expressive power
is only exploited in veriﬁcation. We may ask the following question.
Problem 2. What is the symbolic theory that exploits the richer Peano theory?
The equation system ASTh provides an eﬀective method to check the symbolic
bisimilarity of two ﬁnite VPCTh -terms. A natural question to ask is how to extend
ASTh to a complete system for the ﬁnite control VPCTh -terms. Hennessy, Lin andRathke have discussed the issue in [HL97, Rat97a, Rat97b, HLR97]. It should
be routine to adapt their approach and Milner’s original approach [Mil89b] to
VPCTh . Additional care should be taken to divergence [LDH02, LDH05, Fu12a].
The details are yet to be worked out.
There are other aspects of the value-passing calculi that are worth investigating. One could for example take a look at the box equality introduced by Fu
and Zhu [FZ11]. One could also take a look at the algorithm complexities fora number of decidability problems. The general methodology proposed in thispaper has laid down a ﬁrm foundation for the solutions to these problems.
Acknowledgement. The author would like to thank the members of BASICS, especially to Yijia Chen, Huan Long and Jianxin Xue, for their interest and feedbacks. The support from NSFC (60873034, 61033002) and STCSM(11XD1402800) is gratefully acknowledged.

194

Y. Fu

References[BHR84][Bro83][Cut80][DNMV90][FL10][FR74][Fu12a][Fu12b][FZ11][G3̈1][Hen91][HI93a][HI93b][HL95][HL96][HL97][HLR97][HM85][Hoa78][Hoa85][IL01][LDH02]

Brookes, S., Hoare, C., Roscoe, A.: A theory of communicating sequential
processes. Journal of ACM 31, 560–599 (1984)
Brookes, S.: A Model of Communicating Sequential Processes. PhD thesis, Oxford University (1983)
Cutland, N.: Computability: An Introduction to Recursive Function Theory. Cambridge University Press (1980)
De Nicola, R., Mantanari, U., Vaandrager, F.: Back and forth bisimulations. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS,
vol. 458, pp. 152–165. Springer, Heidelberg (1990)
Fu, Y., Lu, H.: On the expressiveness of interaction. Theoretical Computer Science 411, 1387–1451 (2010)
Fischer, M., Rabin, M.: Super-exponential complexity of presburger arithmetic. In: Karp, R. (ed.) Complexity of Computation, pp. 27–41. American Mathematical Society (1974)
Fu, Y.: Nondeterministic structure of computation (2012)
Fu, Y.: Theory of interaction (2012)
Fu, Y., Zhu, H.: The name-passing calculus (2011)
Gödel, K.: Über formal unentscheidbare sätze der principia mathematica
und verwandter systeme. Monatshefte für Mathematik und verwandter
Systeme I 38, 173–198 (1931)
Hennessy, M.: A proof system for communicating processes with valuepassing. Journal of Formal Aspects of Computer Science 3, 346–366(1991)
Hennessy, M., Ingólfsdóttir, A.: Communicating processes with valuepassing and assignment. Journal of Formal Aspects of Computing 5, 432–
466 (1993)
Hennessy, M., Ingólfsdóttir, A.: A theory of communicating processes
with value-passing. Information and Computation 107, 202–236 (1993)
Hennessy, M., Lin, H.: Symbolic bisimulations. Theoretical Computer
Science 138, 353–369 (1995)
Hennessy, M., Lin, H.: Proof systems for message passing process algebras. Formal Aspects of Computing 8, 379–407 (1996)
Hennessy, M., Lin, H.: Unique ﬁxpoint induction for message-passing process calculi. In: Proc. Computing: Australian Theory Symposium (CAT1997), vol. 8, pp. 122–131 (1997)
Hennessy, M., Lin, H., Rathke, J.: Unique ﬁxpoint induction for messagepassing process calculi. Science of Computer Programming 41, 241–275(1997)
Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. Journal of ACM 32, 137–161 (1985)
Hoare, C.: Communicating sequential processes. Communications of
ACM 21, 666–677 (1978)
Hoare, C.: Communicating Sequential Processes. Prentice Hall (1985)
Ingólfsdóttir, A., Lin, H.: A symbolic approach to value-passing processes.
In: Bergstra, J., Ponse, A., Smolka, S. (eds.) Handbook of Process Algebra, pp. 427–478. North-Holland (2001)
Lohrey, M., D’Argenio, P.R., Hermanns, H.: Axiomatising divergence. In:
Widmayer, P., Triguero, F., Morales, R., Hennessy, M., Eidenbenz, S.,
Conejo, R. (eds.) ICALP 2002. LNCS, vol. 2380, pp. 585–596. Springer,
Heidelberg (2002)

The Value-Passing Calculus[LDH05][Lin93][Lin96][Lin98][Mil89a][Mil89b][MPW92][Opp78][Pal03][Par81][Pre29][Pri78][PS95][Rat97a][Rat97b][Rog87][Ros97][San93][Tho89][Tho93][Tho95][vGW89]195

Lohrey, M., D’Argenio, P., Hermanns, H.: Axiomatising divergence. Information and Computatio 203, 115–144 (2005)
Lin, H.: A veriﬁcation tool for value-passing processes. In: Proceedingsof 13th International Symposium on Protocol Speciﬁcation, Testing andVeriﬁcation, IFIP Transactions (1993)
Lin, H.: Symbolic transition graphs with assignment. In: Sassone, V.,
Montanari, U. (eds.) CONCUR 1996. LNCS, vol. 1119, pp. 50–65.
Springer, Heidelberg (1996)
Lin, H.: “On-the-ﬂy” instantiation of value-passing processes. In: Proc.
FORTH/PSTV 1998 (1998)
Milner, R.: Communication and Concurrency. Prentice Hall (1989)
Milner, R.: A complete axiomatization system for observational congruence of ﬁnite state behaviours. Information and Computation 81, 227–247(1989)
Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes. Information and Computation
100, 1–40 (Part I), 41–77 (Part II) (1992)pn
22
upper bound on the complexity of presburger arithOppen, D.: A 2
metic. Journal of Computer and System Sciences 16, 323–332 (1978)
Palamidessi, C.: Comparing the expressive power of the synchronous andthe asynchronous π-calculus. Mathematical Structures in Computer Science 13, 685–719 (2003)
Park, D.: Concurrency and automata on inﬁnite sequences. In: Deussen,
P. (ed.) GI-TCS 1981. LNCS, vol. 104, pp. 167–183. Springer, Heidelberg(1981)
Presburger, M.: Über die vollständigkeit eines gewissen systems der arithmetik ganzer zahlen, in welchem die addition als einzige operation hervortritt. In: Warsaw Mathematics Congress, vol. 395, pp. 92–101 (1929)
Priese, L.: On the concept of simulation in asynchronous, concurrent
systems. Progress in Cybernatics and Systems Research 7, 85–92 (1978)
Parrow, J., Sangiorgi, D.: Algebraic theories for name-passing calculi.
Information and Computation 120, 174–197 (1995)
Rathke, J.: Symbolic Techniques for Value-Passing Calculi. PhD thesis,
University of Sussex (1997)
Rathke, J.: Unique ﬁxpoint induction for value-passing processes. In:
Proc. LICS 1997. IEEE Press (1997)
Rogers, H.: Theory of Recursive Functions and Eﬀective Computability.
MIT Press (1987)
Roscoe, A.: The Theory and Practice of Concurrency. Prentice Hall
(1997)
Sangiorgi, D.: From π-calculus to higher order π-calculus–and back. In:
Gaudel, M.-C., Jouannaud, J.-P. (eds.)TAPSOFT 1993. LNCS, vol. 668,
pp. 151–166. Springer, Heidelberg (1993)
Thomsen, B.: A calculus of higher order communicating systems. In:
Proc. POPL 1989, pp. 143–154 (1989)
Thomsen, B.: Plain chocs — a second generation calculus for higher orderprocesses. Acta Informatica 30, 1–59 (1993)
Thomsen, B.: A theory of higher order communicating systems. Information and Computation 116, 38–57 (1995)
van Glabbeek, R., Weijland, W.: Branching time and abstraction inbisimulation semantics. In: Information Processing 1989, pp. 613–618.
North-Holland (1989)