Theory by Process
Yuxi Fu
BASICS, Department of Computer Science
Shanghai Jiaotong University, Shanghai 200240
MOE-MS Key Laboratory for Intelligent Computing and Intelligent Systems

Abstract. Theories defined in a process model are formalized and studied. A theory in a process calculus is a set of perpetually available processes with finite interactability, each can be regarded as a service, anagent behind the scene or an axiom. The operational and observationalsemantics of the theories are investigated. The power of the approach isdemonstrated by interpreting the asynchronous π-calculus as a theory,
the asynchronous theory, in the π-calculus. A complete axiomatic system
is constructed for the asynchronous theory, which gives rise to a proof
system for the weak asynchronous bisimilarity of the asynchronous π.

1

Introduction

In a network computing environment, how do we evaluate the capacities of two
service providers S1 and S2 ? Suppose we place a request to both the providers.
One, say S1 , finds the appropriate service in its repertoire and immediately
delivers the service. The other provider S2 does not specialize in the kind ofservice we are interested in. But since it has a strong search ability, it simply
redirects our request to a third party who can offer the service we want for free.
Moreover S2 does it in such a manner that we are not aware of the existence ofthe third party at all. If S1 and S2 can always supply the services with similar
qualities, we are led to believe that they are equally powerful. The point isthat in a distributed computing environment, we are not testing S1 and S2 inisolation. That is clearly impossible. No one can stop S1 and S2 from exploring
the resources freely available on the network. Although we can pretend that
we are testing S1 , what we are really doing is to test S1 plus all the resources
accessible by S1 . Worse still S1 is often blurred with the environment so that
we are not always able to tell precisely which is which. The service providers S1and S2 could have quite different capacities when isolated. They can be however
equivalent in a resource rich network environment.
We would like to formalize the above scenario in interaction models. Our basic
idea is to regard the services available on the network as a set S = {S1 , S2 , . . .} ofprocesses. We shall always assume that each member of the set is well-founded.
It’s no good to have a service that never delivers anything. A one-shot service
is not of much use as a piece of resource. So the actual services distributed overdifferent locations are perceived as the processes !S1 , !S2 , . . .. The finite behavior

of a process P sitting among !S1 , !S2 , . . . can always be inspected by considering
the finite action sequences of the shape
λ

λ

n
1
P0
P | Si1 | . . . | Sik −→. . . −→

since in a finite number of steps, the process P may only consult a finite numberof service providers. If we consider a single step action of P , we only have to focus
λon the actions of the form P | S 0 −→ P 0 for S 0 ∈ S. Now the crucial point is thatλthe services really stay invisibly in the background. So an action P | S 0 −→ P 0
λwould appear to us as the action P −→ P 0 . This is the starting point for thesemantics of a theory.
From a model theoretical point of view, sometimes we need to work with anopen system within a closed world. The idea is best explained by the notion ofasynchrony. The asynchronous π-calculus [Bou92,HT91a,HT91b,HY95,ACS98]
is obtained from the synchronous π-calculus by detaching the output prefixes
from any continuations. At first look it appears a bit simplistic since asynchrony
can not be a syntactical issue. In reality asynchrony is implemented by extra
mechanism which we choose to ignore. In a closed model like π-calculus, thedetachment between the prefix and the continuation is the only sensible thing
to do to achieve asynchrony without introducing any additional gadgets.
There ought to be an alternative treatment to the asynchrony in π-calculusthat does not resort to any syntactical manipulation. An output process ac.P
may communicate to a background environment. The latter picks up the namec and sends it to an input process in a later time. The background environment consists of a bunch of processes of the form !a(x).ax. These processes aresupposed to be hidden from the users. They form a theory in the above sense.
One may also study (constructive) logics in process models. Abramsky’s
work [Abr93] and a number of related works have shown how to model a logic ina process calculus. But how about a logic theory, say the Peano theory, definedin a logic? From our perspective, a particular logical theory can be formulated
as a theory defined in a process model. An element of the theory codes up anaxiom of the logic theory. In the process approach to logic, a proposition is interpreted as a process of the form !A. To make use of the axiom, an environment
has to interact with a copy of A. When the verification (proof) is complete, theenvironment has gathered enough evidence for the validity of the proposition.
In a similar fashion to the interpretations of logics, programs in different
styles have been translated into the π-model [Wal95,HO95,Mil92,CF10]. Whatis lacking in this research field is any idea about implementations of programming languages. Again the notion of theory is in sight. The implementation of aprogramming language amounts to defining a theory that codes up the system
functions or routines that come with the definition of the language.
The motivation for this paper is that the notion of theory defined by processes
arises naturally in many applications of process models. It is worthwhile to give
an application independent study of the problems pertaining to such theories.
Formal studies in this area are likely to shed new light on some familiar topics.

2

Pi Calculus

The π-calculus of Milner, Parrow and Walker [MPW92] has been widely studied
in both theory and in practice. Our presentation of the model is slightly different
from the standard one. The main difference is that we draw a firm line between
the names and the name variables. The reader is advised to consult [FZ10]
for the discussion why the distinction between the two categories is important.
Throughout the paper the following notational convention will be observed:– The set N of the names is ranged over by a, b, c, d, e, f, g, h.
– The set Nv of the name variables is ranged over by u, v, w, x, y, z.
– The set N ∪ Nv is ranged over by l, m, n, o, p, q.
An assignment ρ is a partial function from Nv to N whose domain of definition
is cofinite. A condition is a finite conjunction of atomic propositions. An atomic
proposition is either a match [m=n] or a mismatch [m6=n]. We always omit the
conjunction operator. The set of the conditions is ranged over by φ, ϕ, ψ. We
write ϕ ⇔ > (ϕ ⇔ ⊥) if ϕ is evaluated to the true value > (the false value ⊥)no matter how the name variables appearing in the condition are instantiated.
Similarly we can define ϕ ⇒ ψ and ϕ ⇔ ψ.
Our definition of the π-calculus is influenced by the results obtained in [FL10].
It is equivalent to the standard presentation in terms of expressiveness and it
has better algebraic property. The set of terms is inductively constructed fromthe following grammar:XT :=ϕi λi .Ti | T | T 0 | (c)T | !π.T,
i∈I

where λi ∈ {n(x), nm, n(c)} ∪ {τ } and π ∈ {n(x), nm, n(c)}; they are prefixes.
Here τ indicates an interaction, ab, ab, a(c) denote respectively an input
action,Pan output action and a bound output action. In the guarded choice i∈I ϕi λi .Ti
the P
indexing set I must be finite. We shall often write ϕ1 λ1 .T1 + . . . + ϕn λn .Tn
for i∈{1,..,n} ϕi λi .Ti . We write 0 for the guarded choice whose indexing set isthe empty set. Due to the set theoretical nature the guarded choice ϕ1 λ1 .T1 +. . . + ϕi λi .Ti + ϕi+1 λi+1 .Ti+1 + . . . + ϕn λn .Tn is the same as ϕ1 λ1 .T1 + . . . +ϕi+1 λi+1 .Ti+1 + ϕi λi .Ti + . . . +Pϕn λn .Tn . Sometimes we will abuse notation by
writing for instance ϕ0 λ0 .T0 + i∈{1,2} ϕi λi .Ti for ϕ0 λ0 .T0 + ϕ1 λ1 .T1 + ϕ2 λ2 .T2 .
PP
We will also abbreviate [>]λ.T + i∈I ϕi λi .Ti to λ.T + i∈I ϕi λi .Ti . A namec appearing underneath the localization operator (c) or a bound output prefixa(c) is local. A name is global if it is not local. A name variable x is bound if it isunderneath an input prefix, say n(x). A name variable is free if it is not bound.
Both local names and bound name variables are subject to α-conversion. We will
use the functions gn( ), ln( ), n( ), f v( ), bv( ), v( ) with the obvious meanings. A
process is a term in which all the name variables are bound. Let T denote the setof the terms, ranged over by R, S, T , and P the set of the processes, ranged overby A, B, C, . . . , O, P, Q. The term !π.T is in replication form. A term without
any occurrence of the replication operator is called finite.

The operational semantics of this π-calculus is defined by the labeled transition system generated inductively from the following rules.
Actionϕi ⇔ >,
λi = a(x).

aci∈I ϕi λi .Ti −→ Ti {c/x}P

λii∈I ϕi λi .Ti −→ TiPϕi ⇔ >,
λi is notan input.

Composition
ab

λ

ab

S −→ S 0
T −→ T 0
τS | T −→ S 0 | T 0

T −→ T 0
λS | T −→ S | T 0

a(c)

ac

S −→ S 0
T −→ T 0
τS | T −→ (c)(S 0 | T 0 )Localizationac

λT −→ T 0

T −→ T 0a(c)(c)T −→ (c)T 0(c)T −→ T 0

λc 6∈ n(λ)

Replicationab!a(x).T −→ T {b/x} | !a(x).Tπ!π.T −→ T | !π.T

if π is not an input.

We have omitted all the symmetric rules. There is a side condition ln(λ) ∩gn(T ) = ∅ on the first composition rule. These remarks also apply to the labeledtransition systems defined later. Let =⇒ be the reflexive and transitive closurebλλτ
of −→. Let =⇒ be =⇒ if λ = τ and =⇒−→=⇒ otherwise. These notations allow
us to define Milner and Park’s bisimulation equality [Mil89].
b
λDefinition 1. A symmetric relation R on P is a weak bisimulation if Q =⇒λ
Q0 RP 0 whenever QRP −→ P 0 . The weak bisimilarity ' is the largest weakbisimulation.
We write S ' T if Sρ ' T ρ for every assignment ρ whose domain of definition is disjoint from bv(S | T ). An example of bisimulation equality is !π.T 'π.(T | !π.T ). For the particular π-calculus of this paper, ' is closed under all theoperators.
Theorem 1. The relation ' is both an equivalence and a congruence on T .
PTheorem
1 relies on the fact that in the guarded choice i∈I ϕi λi .Ti the operatorP
is i∈I ϕi λi . . From τ ' [x=y]τ we may derive aa + τ.τ ' aa + τ.[x=y]τ ; but
we may not derive aa + τ ' aa + [x=y]τ .
λ1
A process P is well-founded if there is no infinite action sequence P −→λi
. . . −→
. . . starting from P . It is a process with finite interactability if it is
λ1
well-founded and there is a number k 6= 0 such that no action sequence P −→λi
P1 . . . −→Pi of P contains more than k non-τ actions. A process P is functionalλλ0

if every maximal action sequence of P is of the form P −→=⇒−→ P 0 , where λis an input action and λ0 an output action.

3

TheoryUpon request, a service provider should deliver the service in a short time. In
a similar token, a proposition should have a finite description so that its validity can be verified in a finite number of steps. These observations lead to thefollowing definition.
Definition 2. A theory A is a nonempty set of processes of the form π.T withfinite interactability. These processes are called axioms.
The intuition behind a theory is that it provides a set of eternal truths within
a closed world. The finite interactability condition ensures that a service must
be delivered within an expected number of interactions. Operationally an axiom
A can be identified to the process !A. Every proof in the closed world can makeinquiry into these laws. Propositions valid in the model are all relative to the setof the eternal truths. By definition every axiom A is nontrivial in the sense that
A 6' 0. A theory A is finite if it is a finite set. It is finitely presentable if it canbe generated from a finite theory. By A being generated from B, we mean that
A = {Bα | B ∈ B, and α is an injective function from N to N }.
A theory is functional if all its axioms are functional. A theory is recursive if it
is a recursive set of finite processes.
Let’s see some examples.
Example 1. The asynchronous theory Asy is defined by the finitely presentable
theory {a(x).ax | a ∈ N }. In the presence of Asy communications are asynchronous. An output process ac.P does not have to interact with the target
process. It could interact with the axiom a(x).ax and let the latter pass theinformation to the target. Using the same idea, one may define the finite theory
AB = {a(x).bx, b(x).ax} that essentially identifies the names a and b.
Example 2. The natural numbers can be coded up in the following fashion:def

J0Kp = p⊥,def

Ji+1Kp = (q)(pq | JiKq ).
Here p is the access name for a number. The notation ⊥ is a name that denotes
false; similarly the name > denotes true. The natural numbers are underlined to
avoid any confusion. For simplification the following derived prefix is introduced:
defa(i).T = a(p).(T | JiKp ).

(1)

It is routine to define processes SU CCa , ADDa , M U La , EQa and La that
implement the successor function, the addition, the multiplication, the equality
predicate and the linear order predicate on the natural numbers. The process
La for example inputs a local name at a; and then uses that local name to getthree more local names, say b, c, d. It continues to input a number i at b and anumber j at c. Finally it returns > at d if i < j; otherwise it returns ⊥ at d. Let
Pa be the following theory{p0 (0), . . . , pi (i), . . .} ∪ {SU CCa , ADDa , M U La , EQa , La | a ∈ N }.
It is an implementation of the Peano arithmetic in π-calculus. For details of theencodings the reader could consult [FZ10].
Example 3. The theory Crp is given by the union of Pa with the following set{e(v).v(y).Enc, d(v).v(z).Dec}.
The action sequences of the encryption function e(v).v(y).Enc are all of the form
ec

cf

τ

c(g)

e(v).v(y).Enc −→−→=⇒−→' JiKg

for some number i. After receiving a local name c, it inputs at c a name thatpoints to a number, the plain text, and then outputs at c a name that points
to the number i, the encrypted text, after completing a sequence of internal
computations. The decryption function d(v).v(z).Dec has the dual semantics.
The theory Crp provides an encryption/decryption facility every process canmake use of. A complete specification of Crp depends on the choice of theencryption and decryption functions.
Example 4. Suppose that we would like to define a random number generator
that provides perpetual service on network. It appears at first sight that thetheory Ran can be defined by extending Pa with the processa(v).(c)(c(0) | !c(x).(c(d).dx + vx)).

(2)

Upon receiving a private channel provided by a user, the process (2) randomly
generates a number and sends it to the user through the private channel. However
process (2) may diverge. So it is not an axiom according to our definition. The
theory Ran can be defined by the finite set {g(0), g(x).g(p).px)}. It can also be
defined by the infinite set {g(0), g(1), . . . , g(i), . . .}. It is worth remarking thatthe randomness is achieved by the nondeterminism. There is no other way.
Example 5. The π-calculus has been used both as a specification language anda machine language. The rational behind these practices is that π is expressive
enough to qualify for a machine model. Now if we think of π-calculus as amachine model, we can talk about programming in π-calculus. This is precisely
what is done in [Wal95]. Formally what is then an interpreter of a higher orderprogramming language on π? Whatever the interpreter is, it must give an accountof the standard routines and packages supplied by the programming language.
In our opinion these routines and packages are best interpreted as a theory Prg.
Two programs defined according to the grammar of the language are equivalent
if they are so in the presence of Prg. Let O be a program that invokes a systemroutine and P be a user defined program that achieves the same functionality.
Conceptually O and P are equivalent. But they are not bisimilar since the former
may interact at a name which P does not know. The notion of theory is a starting
point to address issues of this kind.

3.1

Semantics

To investigate the algebraic properties of the theories, we need to define theoperational semantics of the theories first. The power of a theory A is duly
exhibited by the ‘process’
Y
!A,
A∈A

which is not always admissible at the syntactical level since it makes use of a
possibly infinite composition. A process P under theory A can be imagined asa fixpoint in the following sense:
Q
Operationally P is the same as P | A∈A !A.
But notice that P | A, forQ each A ∈ A, is also a fixpoint
Q of the same nature. By
exploring the fact that A∈A !A is equivalent to A | A∈A !A, one sees that P | A
is operationally the same as P . The semantics of the theory A, or the semanticsof the πA -calculus, extends the operational semantics of the π-calculus with thefollowing rule:λP | A −→ P 0
A ∈ A.
(3)
λP −→ P 0
Definition 1 can be immediately applied to the πA -calculus.
b
λDefinition 3. A symmetric relation R on P is a weak A-bisimulation if Q =⇒λ
Q0 RP 0 in πA whenever QRP −→ P 0 in πA . The weak A-bisimilarity 'A is thelargest weak A-bisimulation.
The proof of Theorem 1 can be repeated to show that 'A is both an equivalence and a congruence on T .
Since every axiom in a theory is nontrivial, the fact stated in the next proposition is apparent.
Proposition 1. The strict inclusion '⊂'A holds for every theory A.
Proof. Using the fact that ' is closed under composition, it is easy to show that' is an A-bisimulation. The inclusion is strict since A is nonempty.
tu
The next lemma is a generalization of Proposition 1.
Lemma 1. If A ⊆ B then 'A ⊆'B .
By abusing the notation again, one could describe the relationship between
0 and the theory A by the following statement:
Q
Operationally 0 is the same as A∈A !A.
The equivalence has been exploited to define the semantics of the asynchronous
π-calculus. Honda and Tokoro introduce the following rule in [HT91a,HT91b].
ac

0 −→ ac
It is evident that (4) is essentially (3) applied to Asy.

(4)

3.2

KernelA theory A is consistent if 'A is not P×P; it is inconsistent otherwise. The
next proposition is useful.
Proposition 2. The following statements are equivalent:(i) A is consistent;(ii) ∃P ∈P.P 6'A 0;(iii) ∃P ∈P.∀A∈A.P 6'A A.
Proof. If (ii) did not hold, then every process would be equated by theory A,
contradicting (i). Hence (i) implies (ii). If ∀P ∈P.∃A∈A.P 'A A, then every
process is equated to 0. So (ii) implies (iii). Finally (iii) trivially implies (i). tu
The above proposition indicates that there is a distinguishing line between
the processes equal to 0 in the equational theory of A and those that are not.
This motivates the following definition: The kernel Aker of the theory A is theset of the processes equal to 0 under the theory A, i.e.
Aker = {A | A 'A 0}.
By Proposition 2, a theory is consistent if and only if its kernel is not P.
Proposition 3. The A-bisimilarity equals the B-bisimilarity iff Aker = Bker .
Proof. It is clear that Aker ⊆ Bker if and only if 'A ⊆'B .

tu

A corollary of Proposition 3 is that the power of a theory is essentially determined by its kernel. One could define for instance that A is a subtheory of B
if A ⊆ Bker , and that A is essentially in A if A ∈ Aker .
Although it is easy to see that Asy is consistent, it is generally a tricky job toestablish the consistency of a theory. Let F be the recursive theory consisting of
all the finite processes. For each process P , let P ¬(!) denote the process obtained
from P by removing all the occurrences of the replication operator and the
localization operator. It is not difficult to see that P 'F P ¬(!) 'F 0. So Fker =P. Therefore F is inconsistent. For a positive result, we remark that all functional
theories are consistent. In a functional theory the process aa is never equal to 0.

4

Asynchronous Theory and Asynchronous π

We prove in this section that Asy provides a faithful account of the asynchronous π-calculus. We adopt the following grammar for the asynchronous
π-calculus, which summarizes the essential feathers of the calculi defined in literature [Bou92,HT91a,HT91b,HY95,ACS98].
X
ni (x).Ti | T | T | (c)T | !n(x).T.
T := 0 | nm |i∈INotice that the above grammar maintains a distinction between the names andthe name variables. There are basically two ways to formulate the semantics ofthe asynchronous π-calculus. Honda and Tokoro’s semantics makes use of therule (4). The notion of theory is lurking in their framework. Amadio, Castellani
and Sangiorgi’s approach takes a more traditional view on the asynchronous π.
Their operational semantics is defined by the following rules.
Actionai ci∈I ai (x).Ti −→ Ti {c/x}abPab −→ 0Composition
ab

λ

ab

S −→ S 0
T −→ T 0
τS | T −→ S 0 | T 0

T −→ T 0
λS | T −→ S | T 0

ac

a(c)

S −→ S 0
T −→ T 0
τS | T −→ (c)(S 0 | T 0 )Localizationac

λT −→ T 0

T −→ T 0a(c)(c)T −→ (c)T 0

λ(c)T −→ T 0

c 6∈ n(λ)

Replicationac!a(x).T −→ T {c/x} | !a(x).T
In Honda and Tokoro’s treatment the asynchronous π differs from the synchronous π at the operational level, whereas in Amadio, Castellani and Sangiorgi’s approach it is at the observational level. The definition of the asynchronous bisimilarity [ACS98] appears odd from the point of view of interaction.
Definition 4. A symmetric relation R on the asynchronous π-processes is anasynchronous bisimulation if the following statements are valid whenever P RQ:τ

1. If Q −→ Q0 then P =⇒ P 0 RQ0 for some P 0 .
abab
2. If Q −→ Q0 then P =⇒ P 0 RQ0 for some P 0 .
a(b)
a(b)
3. If Q −→ Q0 then P =⇒ P 0 RQ0 for some P 0 .
abab
4. If Q −→ Q0 then either P =⇒ P 0 RQ0 for some P 0 or P =⇒ P 0 for some P 000such that P | ab R Q .
The asynchronous bisimilarity 'a is the largest asynchronous bisimulation.
The asynchronous π is a syntactic subcalculus of π. It is also an operationalvariant of π according to Honda and Tokoro’s formulation. Amadio, Castellani
and Sangiorgi have proved that 'a coincides with Honda and Tokoro’s bisimulation equivalence, called HT-bisimilarity in [ACS98]. Their proof can be extended
to produce a proof of the following theorem.
Theorem 2. Let S, T be asynchronous π-terms. Then S 'a T iff S 'Asy T .
Theorem 2 can be interpreted as saying that the asynchronous π is a syntactical simplification of πAsy . It perceives πAsy as a submodel of the π-calculus.
It can also be seen as a justification of the asynchronous π as defined by Honda
and Tokoro, as well as the variant defined by Amadio, Castellani and Sangiorgi.

L1(c)0 = 0L2(c)(d)T
P = (d)(c)TP
L3(c)([x=c]ϕλ.T + P) = (c)PL4(c)([x6=c]ϕλ.T + P) = (c)(ϕλ.TP + )L5(c)(ϕλ.T + P) = (c)if ∃d ∈ N .λ = cd ∨ λ = c(d)PL6(c)(ϕnc.T+ ) = (c)(ϕn(c).T+ )if c ∈/ gn(ϕ) ∧ c 6= nPPL7(c) i∈I ϕi λi .Ti = i∈I ϕi λi .(c)Ti
if ∀i ∈ I.c ∈/ gn(ϕi , λi )P P
M1[⊥]λ.T + P =P
M2
ϕλ.T + P = ψλ.T +if ϕ ⇔ ψP
M3[x=p]ϕλ.T+=[x=p](ϕλ.T){p/x}
+
P0 P
P0 P
M4
[x6=p]ϕλ.
+ P = [x6=p]ϕλ.[x6=p] P+
S1
ϕλ.T + P = ϕλ.T + ϕλ.T +P
S2
ϕλ.T + P = [x=p]ϕλ.T + [x6=p]ϕλ.T +P
S3 ϕn(x).S + ϕn(x).T + P = ϕn(x).S+ ϕn(x).T + ϕn(x).([x=p]τ.S + [x6=p]τ.T ) +P
T1
P ϕτ. P = ϕP
T2P+ϕτ.P0 =P
P0T3
φλ.(ϕτ.T + ) += φλ.(ϕτ.T + ) + φϕλ.T +Fig. 1. Axioms for the Weak Bisimilarity.

5

Proof System

A complete equational system for the strong asynchronous bisimilarity is given
in [ACS98]. Such a system for the weak asynchronous bisimilarity has not been
available. The problem in generalizing a result from the strong case to the weakcase could be an indication that something is not quite right. The difficulty indesigning an equational system for the weak asynchronous bisimilarity is dueto the lack of the output prefix operator. This is unfortunate since the role ofthe output prefix operation is to impose orders on interactions. Its relationshipto asynchrony, or synchrony for that matter, was not intended. Our approachdisowns this problem.
The expansion law plays a crucial role in proof systems. It is about how
to convert two concurrent choicePterms to one choice
P term. Suppose S, T are
respectively the guarded choices i∈I ϕi λi .Si and j∈J ψj λj .Tj . Thenλi =m(x),λj =np

S |T =

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

ϕi ψj [m=n]τ.(Si {p/x} | Tj )i∈I,j∈Ji∈I

λj =m(x),λi =np

+

X
j∈J

ψj λj .(S | Tj ) +X

ϕi ψj [m=n]τ.(Si | Tj {p/x}).

i∈I,j∈J

Let AS be the equationalPsystem definedlaw.
P in Figure 1 plus
P0the expansion
P
In Figure 1 thePnotation
stands for i∈I
ϕ
λ
.T
and
for
ψ
λ
j∈J j j .Tj .
P i i i
Accordingly ϕ should be understood as i∈I ϕϕi λi .Ti . Our axiomatic systemdiffers from the standard one in that it is defined in terms of the guarded choice
operator rather than the unguarded choice operator.

In AS we may rewrite terms to normal forms, whose definition is given next.
Definition
P 5. Let F be gn(T ) ∪ f v(T ). A finite π-term T is a normal form on
F if T ≡ i∈I ϕi λi .Ti such that for each i ∈ I one of the followings holds.
1. If λi = τ then Ti is a normal form on F.
2. If λi = nm then Ti is a normal form on F.
cc/
3. If λi = n(c) then Ti ≡ [c∈F]Ti for some normal form Ti on F ∪ {c}.
4. If λi = n(x) then Ti is of the formX6=[x∈F]T/[x=m]Timi +m∈F
6such that Ti=
is a normal form on F ∪{x} and, for each m ∈ F, x ∈/ f v(Tim )mand Ti is a normal form on F.

For the motivation of the above definition and the proof of the next lemma,
the reader is referred to [FZ10].
Lemma 2. If T is finite, then a normal form T 0 exists such that AS ` T = T 0 .
AS is sound and complete for the weak bisimilarity on the finite π-terms.
Theorem 3. Suppose S, T are finite. Then S ' T iff AS ` S = T .
Complete systems have been discussed in literature [MPW92,PS95,Lin95,FY03].
A recent account that fits more into the present context can be found in [FZ10].
Notice that our formulation of T2 is crucial for the completeness proof.
We now turn to 'Asy . Let ASAsy be AS together with the following law
a(x).ax = 0.

(5)

Apparently ASAsy is sound for 'Asy . The first indication that (5) is complete
is the validity of the saturation property.
Lemma 3 (saturation). Suppose that T is a normal form. The following statements are valid in the πAsy -calculus for every assignment ρ whose domain of
definition is disjoint from bv(T ).
λ

1. If T ρ =⇒ T 0 and λ is not an input action, then ASAsy ` T = T + ϕλ0 .T 0
for some ϕ, λ0 such that ϕρ ⇔ > and λ0 ρ = λ.
ae
2. If T ρ =⇒ T 0 , e ∈/ n(T ρ) and z ∈/ v(t), then ASAsy ` T = T + ϕn(z).T 0 {z/e}for some ϕ, n such that ϕρ ⇔ > and ρ(n) = a.
λProof. If T =⇒ T 0 makes use of the rule (3) k times, then it is easy to see
λthat T | a1 (x).a1 x | . . . | ak (x).ak x =⇒ T 0 . By Lemma 2 there is some normal
form T1 such that AS ` T1 = T | a1 (x).a1 x | . . . | ak (x).ak x. By the standard
approach it is easy to establish that ASAsy ` T1 = T1 + λ.T 0 . Thus ASAsy `T = T | a1 (x).a1 x | . . . | ak (x).ak x = T1 = T1 + λ.T 0 = T + λ.T 0 . Notice that
according to (5) the equality T = T | a(x).ax follows from T = T | 0, which inturn follows from the expansion law.
This simple argument should be enough for an informed reader.
tuThe proof of the completeness theorem is an induction on the complexity of
the normal forms. The depth dep(T ) of a normal form T is defined as follows:def

dep(0) = 0,
defdep(ϕn(x).T ) = dep(T ) + 2,
defdep(ϕλ.T ) = dep(T ) + 1, if λ is not an input,
X
def
dep(
ϕi λi .Ti ) = max{dep(ϕi λi .Ti )}i∈I .
i∈I

For a finite term T , dep(T ) is defined by dep(T 0 ), where T 0 is a normal form of
T . It is worth remarking that the depth for input prefix is greater than that for
output, bounded output and tau prefixes. This is important to the next proof.
Theorem 4 (completeness). For finite S, T , S 'Asy T iff ASAsy ` S = T .
PP
Proof. Suppose P ≡ i∈I ϕi λi .Si and Q ≡ j∈J ψj λj .Tj are normal forms suchacthat P 'Asy Q. If a(x).Si is a summand of P , then P −→ Si {c/x}. The processac
Q has to simulate this action in the following manner Q =⇒ Q1 −→ Q2 =⇒ Q0 .
ac
0
It is easy to see that dep(Q1 ) ≤ dep(Q) and dep(Q ) ≤ dep(Q2 ). If Q1 −→ Q2
is not derived from the rule (3), then clearly dep(Q2 ) < dep(Q1 ). If it is derived
from the rule (3), then AS ` Q2 = Q02 for some normal form Q02 , using the
expansion law. It is obvious that dep(Q2 ) = dep(Q02 ) ≤ dep(Q1 ) + 1 by thedefinition of the depth function. But dep(Si {c/x}) ≤ dep(P ) − 2 by definition.
Hence dep(Q0 ) + dep(Si {c/x}) < dep(Q) + dep(P ). So ASAsy ` Q0 = Si {c/x}by induction hypothesis.
The above oversimplified account is meant to bring out the fact that thedepth function dep( ) does allow the standard inductive proof to go through.
Consult [FZ10] for the general idea of the completeness proof.
tu

6

Conclusion

The notion of theory probably should have been introduced long time ago. A
theory is essentially an implementation. In practice it is one of the most important concepts to start with. Theories can be defined for process calculi otherthan the π-calculus. The most interesting theories are defined in complete process calculi [Fu10]. In a complete model the Peano arithmetic can be defined ina robust manner. Example 2 through Example 5 of Section 3 would not makea lot of sense for incomplete models like CCS (the incompleteness of CCS isestablished in [Fu10]).
There are several directions one can pursue to further the study of theories. Let’s mention a couple of them. Firstly it is worthwhile to carry out acomparative research into theories. Honda and Yoshida [HY95] have introduced
a different notion of theory. They extended the notion of λ-theory [Bar84] tothe framework of process models. A theory in their sense is a set of equalities

closed under the process operations of the frame calculus. Their starting point
is more algebraic than logical, whereas our motivation is less algebraic than logical. It is apparent that a theory in the present setting is a theory of Honda andYoshida. Unlike in their treatment, the algebraic property of our theories comesfor free. It would be interesting to investigate the relationship between these two
approaches.
Secondly it is interesting to look for complete proof systems for general theories. Suppose A is a theory. Let ASA be obtained by combining AS with thefollowing laws for A.
A = 0, for every A ∈ A.

(6)

For which recursive theories for instance is ASA complete? It is easy to come up
with theories for which ASA does not appear to be complete. Take for instancethe theory Aa = {a(c).a(c)}. It is unlikely that ASAa ` a(c) = 0. In fact itfollows from Sewell’s nonaxiomatisability result [Sew97] that it must be incomplete if the frame calculus is CCS. It remains to check if this negative result
is also valid when the frame calculus is π. A more difficult task is to answer
the question if there exists a recursive theory A such that 'A , when restricted
to the finite terms, has no complete recursive equational systems whatsoever.
These are issues to be investigated in future.
Acknowledgments
This work has been supported by NSFC (60873034). The author is gratefulto the anonymous referees for their comments and suggestions.

References[Abr93]

S. Abramsky. Computational interpretations of linear logic. TheoreticalComputer Science, 111:3–57, 1993.
[ACS98] R. Amadio, I. Castellani, and D. Sangiorgi. On bisimulations for the asynchronous π-calculus. Theoretical Computer Science, 195:291–324, 1998.
[Bar84] H. Barendregt. The Lambda Calculus: Its Syntax and Semantics. NorthHolland, 1984.
[Bou92] G. Boudol. Asynchrony and the π-calculus. Technical Report RR-1702,
INRIA Sophia-Antipolis, 1992.
[CF10]
X. Cai and Y. Fu. The λ-calculus in the π-calculus, 2010.
[FL10]
Y. Fu and H. Lu. On the expressiveness of interaction. Theoretical Computer
Science, 411:1387–1451, 2010.
[Fu10]
Y. Fu. Theory of interaction, 2010.
[FY03]
Y. Fu and Z. Yang. Tau laws for pi calculus. Theoretical Computer Science,
308:55–130, 2003.
[FZ10]
Y. Fu and H. Zhu. The name-passing calculus, 2010.
[HO95] M. Hyland and L. Ong. Pi-calculus, dialogue games and pcf. In Proc.
7th ACM Conference on Functional Programming Languages and Computer
Architecture (FPCA 1995), pages 96–107, 1995.

[HT91a] K. Honda and M. Tokoro. An object calculus for asynchronous communications. In Proc. ECOOP’91, volume 512 of Lecture Notes in Computer
Science, pages 133–147, Geneva, Switzerland, 1991.
[HT91b] K. Honda and M. Tokoro. On asynchronous communication semantics. In
Proc. Workshop on Object-Based Concurrent Computing, volume 615 of Lecture Notes in Computer Science, pages 21–51, 1991.
[HY95] K. Honda and M. Yoshida. On reduction-based process semantics. Theoretical Computer Science, 151:437–486, 1995.
[Lin95] H. Lin. Complete inference systems for weak bisimulation equivalences inthe π-calculus. In Proceedings of Sixth International Joint Conference on the
Theory and Practice of Software Development, volume 915 of Lecture Notes
in Computer Science, pages 187–201, 1995.
[Mil89] R. Milner. Communication and Concurrency. Prentice Hall, 1989.
[Mil92] R. Milner. Functions as processes. Mathematical Structures in Computer
Science, 2:119–146, 1992.
[MPW92] R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes. Information and Computation, 100:1–40 (Part I), 41–77 (Part II), 1992.
[PS95]
J. Parrow and D. Sangiorgi. Algebraic theories for name-passing calculi.
Information and Computation, 120:174–197, 1995.
[Sew97] P. Sewell. Nonaxiomatisability of equivalence over finite state processes.
Annals of Pure and Applied Logic, 90:163–191, 1997.
[Wal95] D. Walker. Objects in the π-calculus. Information and Computation,
116:253–271, 1995.