Thesis for Interaction
Yuxi Fu
BASICS, Shanghai Jiao Tong University
fu-yx@cs.sjtu.edu.cn

Abstract—A thesis for interaction model is proposed as afoundation for interactive solvability. It formulates the minimal
content computability and the maximal channel computability of
all interaction models by fixing a minimal model and a maximal
model. It is shown that the interactive extensions of the recursivefunction model, the Turing machine model and the λ-calculus
model all fall within the realm of the thesis. A major technicalcontribution is the design, in the maximal model, of interpreters
for the models that fit in the thesis.

I. Introduction“The theory of computation has traditionally been studied
almost entirely in the abstract, as a topic in pure mathematics.
This is to miss the point of it. Computers are physical objects,
and computations are physical processes. What computers canor cannot compute is determined by the laws of physics alone,and not by pure mathematics.” — David Deutsch
Physical implementability is the very foundation of computer science. Church-Turing Thesis states that the functions
implementable by physical devices are precisely those definable by the mathematical models of computation [12], [3],[36], [16]. The thesis has two sides of a story. One is about
definability, pointing out that the mathematical models offer
a formulation of the minimal capacity of computing devices.
Digital computers built with von Neumann structure are physical devices that enjoy the minimal computing power. The otheris to do with unsolvability, postulating that the mathematicalmodels characterize the maximal power of computing devices
in all shapes and forms. There has been an increasing interestin the mathematical model of computation based on quantum
mechanics [22]. Leaving the implementation detail aside, it has
been shown that such a model is equivalent to Turing machinemodel as far as computability is concerned. All experiments
indicate that the world is quantum mechanical in that all physical phenomena can be explained by quantum mechanics. If webelieve what physicists believe, then the unsolvability theory
based on Church-Turing Thesis is a consequence of the laws ofphysics. Many other mathematical models of computation havebeen studied. The probabilistic Turing machine model [32]for example, believed by many to give a broader picture ofefficient computation [10], is equivalent to Turing machinemodel in computability. Physical implementability emphasizes
another property of computation, that of observability. For acomputing device to be useful, it should be able to fetch input
data from some medium and make the result of computationdeliverable. In other words both inputs and outputs ought tobe observable. The observability rules out models that deal
with general functions on the field of real number.

The physical implementability remains a fundamental constraint if one switches from models of computation to models
of interaction. In a concurrent system processes communicate
through channels; and channels are of physical nature. A
frequently asked question about interaction models is if they
are more powerful than computation models. What is theexpressiveness of distributed computing? How about Internet computing? For closed systems of interactive processes
Church-Turing Thesis already provides the answer to thesequestions, even though our everyday encounter with modern
computing technology prompts us to think otherwise. The
point is that a model is meant to define closed systems, andthat if one is interested in open systems, there is a standard
approach using oracles. Human interventions in Internet computing for example are best explained as interactions withoracles. Let’s see an example. Is there a process that admits
the following deterministic interactive behaviour
a

a

b

a

a

b

−→ {z
. . . −→O −→. . . −→
} −→ . . . .
| {z} −→ |i1(1)

i2

such that i1 < i2 < . . . and {i1 , i2 , . . .} is the set of total
recursive functions? For a closed system that is immune fromany external force (1) is an impossibility for otherwise there
would be a process that answers deterministically if an input
function is total. We can of course think of O as an oracle andstudy the consequence of admitting it into our system. Fromthe point of view of Church-Turing Thesis there is nothing
new about interaction models. What is new is that processes
have access to channels. They can choose to communicate, or
not to communicate at a particular channel. They can also send
the identify of a channel to other processes. To what extent
manipulations on channels should be allowed? It is this aspectof interaction that has not been under scrutiny in the lightof Church-Turing Thesis. But once we have raised the issue,
we immediately know the answer. Because the computational
behaviour of a process is constrained by Church-Turing Thesis,a process can only make reference to channels in a computablemanner. This strongly suggests, according to the discussion in
the previous paragraph, to define a mathematical model thatformalizes the maximal capacity of channel manipulation.
Channels are meant to be vehicles for messages. ChurchTuring Thesis implies that the messages produced by processes
are all encodable by natural numbers, no matter how themessages may look like. Once again some kind of maximality
emerges. There are two points need be discussed here. One isabout the rational behind our design decision to take as atomic
a communication of a number whose size is unbounded. Ob-

serve that this is consistent with the design of Turing machines.
The input and the output tapes of a machine are unbounded
in length. This is so because a machine is able to take inputsof any length and may output a string of any length. When
we turn Turing machines into interactive machines, the input
and output tapes become channels. But isn’t it more natural
to take the token-by-token communications as atomic? In theinteractive machine example, is it better to let the content of
a communication be just a symbol from an alphabet? The
answer is definitely negative. In an interleaving semantics
there is no guarantee that a piece of information can reach its
destination in integrity if it is broken down into packets. At
the theoretical level a process calculus with a token-passing
communication mechanism is not very much different from
CCS, and runs the risk of not being a complete model [8].
It is at the right level of abstraction that a complete piece of
information is transmitted in an atomic interaction. The second
point is concerned with dynamic creation of private channels.
Since we cannot restrict the number of global channels aprocess need to make use of, it is again at the right level ofabstraction to assume the availability of a potentially infinite
number of global channels. How about private channels? Takea look at the process !a(x).(p)(p(y).S | b(z).p[z].T ). Every time
an interaction with the process occurs, a new private channel
p is generated. If p is a physical wire, it would mean thatcomputation can cause the creation of a new physical wire.
From a physical implementation point of view, the idea that asingle process is always in need of a new private channel isdebatable. Fortunately there is an alternative interpretation ofprivate channel. In (p)(p(y).S | b(z).p[z].T ) the scope operator(p) translates to saying that “it does not matter which channelp(y).S and p[z].T are going to use to interact, neither of themis allowed to communicate with anybody else in the next step”.
This is the view we shall adopt in our universal model.
After fifty years of concurrency theory [25], we are stillin a situation where we are expected to define everythingfrom scratch. We cannot go very far that way. The lack ofa definability/unsolvability theory of processes is the prime
reason. Ultimately this is due to the absence of a fundamental
thesis for theory of interaction. Our understanding of concurrency theory must reach to a stage when new results are built
from known results and the whole theory is based upon a firm
foundation. In this paper we attempt to postulate such a thesis
with the motivation described in the above.
The rest of the paper is organized as follows. Section II
defines the principal model of the paper, a functional model for
concurrency. Section III reviews the preliminaries of the theoryof interaction developed in [8], and apply them to the principal
model. Section IV defines the minimal model and the maximal
model and postulates a thesis for interaction models in terms ofthe two models. It is pointed out that the interactive versions of
the recursive function model and the Turing machine models
are admitted by the thesis. In Section V and Section VI it isproved that the functional model and the π-calculus fall within
the reign of the thesis. A theory of definability/unsolvability
is outlined in Section VII. Section VIII concludes.

II. A Concurrent Functional Model
Church’s λ-calculus [1] is a prototypical higher order model
for functional computation. It is of higher order in the sensethat both an input and an output of a λ-term are themselves
λ-terms. In concurrency theory an important issue has been
to look for the model that plays the role of being the “λcalculus” for concurrent computation. Early works [21], [2],[34], [35] addressed this issue by introducing the higher ordermechanism into CCS [17]. A crucial shift from the functional
paradigm to an object-oriented paradigm, initiated by the workof [4], was fully investigated by Milner, Parrow and Walker
with the π-calculus [19]. The model is a channel-passing
calculus. Our presentation of the model distinguishes syntactically private channels from global channels. The following
notational convention will be maintained throughout the paper.
Cg is the set of global channels. The elements of Cg aredenoted by a, b, c, d, e, f, g, h.
• C p is the set of private channels. The elements of C p aredenoted by l, m, n, o, p, q.
• Cv is the set of channel variables. The elements of Cg aredenoted by u, v, w, x, y, z.
•

We write for example ep for a finite sequence of private
channels. The set Cg ∪ C p ∪ Cv will be ranged over by µ, ν,and the set Cg ∪ C p by α, β.
We start by fixing the grammar of the minimal π-calculus.
T

0 | µ(x).T | µµ0 .T | T | T 0 | (p)T | !µ(x).T.

:=

We will use the standard abbreviation µ(p).T ≡ (p)µp.T . The
labeled transition semantics is defined by the following rules.
αp

T −→ T 0
αα0

αα0 .T −→ T

αα0

αα0

T 1 −→ T 10

T 0 −→ T 00

α(p)

αα0

α(x).T −→ T {α0 /x}τ(p)T −→ T 0αp

T 0 −→ T 00

α(p)T 1 −→ T 10

τ

T 0 | T 1 −→ T 00 | T 10

T 0 | T 1 −→ (p)(T 00 | T 10 )αα0!α(x).T −→ T {α0 /x} | !α(x).Tλ

T 0 −→ T 00
λT 0 | T 1 −→ T 00 | T 1

λT −→ T 0
λp is not in λ.

(p)T −→ (p)T 0

The symmetric rules are systematically omitted. The last two
rules are structural rules. They are common to all models andwill be omitted in the definition of a new model. We shall use
λλ1 ...λkstandard notations like =⇒, =⇒ and −→ .
The π-calculus has been successful for many reasons. It
is powerful enough to simulate many process calculi and iscapable of modelling a wide range of phenomena arisingfrom concurrent programming [39], [29], [30], [37]. Milner’s
encoding of the lazy λ-calculus into the π-calculus [18]confirms that the object-oriented paradigm is powerful enoughto encapsulate the functional computation. The relationship tothe λ-calculus is seen as a qualification test for a model toclaim the “λ-calculus” status. The object-oriented style of πprogramming is evident from the following encoding of thelazy λ-calculus given by Milner:
~xu

=

xu,

~λx.Mu=u(x).u(v).~Mv ,

~MNu

=

(p)(~M p | p(w).pu.!w(z).~Mz ).

Every λ-term in the π-calculus is accessible at some channel.
A term is invoked only when it is needed, and the simulation
is indirect. A natural question asks if there is a more directinterpretation of the λ-calculus in a concurrent model?
We propose in this section an alternative candidate for the“λ-calculus” of concurrent computation. It is a higher orderfunctional model, denoted by F, with a direct interpretationof the lazy λ-calculus. The following syntactical class isnecessary for the definition of the model.
• V is the set of abstraction variables. The elements of Cg
are denoted by U, V, W, X, Y, Z.
The set of F-terms is generated by the following grammar:
T
A

:=
:=

0 | γ.T | T | T | (p)T | A(µ, ν),X | (x, y)T, where f c(T ) ⊆ {x, y} ∧ oc(T ) = ∅,γ:=µ(X) | µ[A].

An abstraction is either an abstraction variable or of theform (x, y)T . In (x, y)T the channel variables x, y are bound.
A channel variable is free if it is not bound. We write
f c(T ) for the set of the free channel variables appearing
in T . If y does not appear in S , we abbreviate (x, y)T to(x)T . If A = (x, y)T , then the instantiation of A at µ, ν is
A(µ, ν) = T {µ/x, ν/y}. If A = (x)T , then the instantiation A(µ)
of A at µ is A(µ, µ) = T {µ/x}. We will write Aµν for A(µ, ν)
and Aµ for A(µ) to improve readability. The set of abstractions
will be ranged over by A, B, C, D. The nil process 0 and thecomposition term T | T 0 are standard. A trailing 0 is often
omitted. A prefix term γ.T is either an input term of the formµ(X).T or an output term of the form µ[A].T . The abstraction
variable X in µ(X).T is bound. A (abstraction) variable isfree if it is not bound. We write f v(T ) for the set of freevariables appearing in T . We shall abbreviate µ(X).T to µ.T if
X does not appear in T . Similarly we shall abbreviate p[A].T
to p.T in a context where A can never be received by others.
We will abbreviate for example a(X).a(Y).T to a(X, Y).T anda[A].a[B].T to a[A, B].T . We will call a(X) a global input
guard, a[A] a global output guard, p(X) a local input guard,
and p[A] a local output guard. A τ prefix term τ.t can be
defined by (p)(p.T | p) where p < f c(T ). In localization term(p)T the private channel p is localized. A private channel isopen if it is not localized. We write oc(T ) for the set of theopen private channels appearing in T .
An F-process is an F-term in which all channel variables
are bound, all private channels are local, and all abstraction
variables are bound. We write L, M, N, O, P, Q for processes.
We try to keep the model as small as possible. The composition and localization are basic operations necessary in all

interaction models. Prefix terms introduce sequential actions.
We insist that all abstractions have two parameter variables.
We think of an abstraction as a concurrent generalizationof function. Two parameters are necessary and sufficient tospecify the input and the output interface of a function. We
believe that the model would be far less expressive if allabstractions have only one parameter, although currently wehave not formally proved this. Working with fixed number
parameter abstractions saves us from introducing a type systemfor channels. Abstraction-passing higher order calculi havebeen studied in literature [30], [37]. It is a more faithfulextension of the higher order mechanism of the λ-calculus thanstrict process-passing calculi. Strict process-passing calculi are
not expressive enough since a receiving process has no control
over a received process [8]. One can enhance the expressive
power of process-passing calculi by introducing relabeling
operator. The problem with the relabeling operator is that itinterferes with congruence property.
Using the action set {α(A), | α ∈ Cg ∪ C p } ∪ {τ}, where τ is alabel for all internal actions, the simple operational semantics
of F can be defined by the prefix rules
α(A)

α(A)

α(X).T −→ T {A/X}

α[A].T −→ T

and the interaction rule
α(A)

α(A)

T 0 −→ T 00

T 1 −→ T 10
τ

T 0 | T 1 −→ T 00 | T 10

The side condition on the grammar of abstraction simplifies
the operational semantics. There is no name extrusion.
We need to make sure that the side condition on abstraction
is maintained.
λLemma 1. If T is an F-term and T −→ T 0 , T 0 is an F-term.
Proof: Suppose λ = a(A). If A lands in an output prefix,
then speaking from that output position it can be instantiatedby neither a free variable channel nor an open private channel.
Let’s see how recursion is defined in F. The counterpartof the λ-term xx is (p)(p[X] | X p). The infinite behaviour of(λx.xx)(λx.xx) is simulated by the process
def

Ω

=

(p)(p[D] | Dp)

where the abstraction D is (z)z(Z).(p[X] | X p). A term that
inputs an abstraction at µ and then immediately outputs
it at ν can be defined as (p)(p[C] | C p)), where C =(z)µ(X).ν[X].z(Z).(z[Z] | Zz). This example can be generalized.
We will use the following guarded recursion throughout the
paper.
!γ1 . . . γk †T=

γ1 . . . γk . (T | (p)(p[C] | C p)) ,(2)

where C = (z)γ1 . . . γk .z(Z).(T | z[Z] | Zz) and p does not appear
in T . Intuitively !γ1 . . . γk †T is a recursively defined procedure,each recursive call of the body T must be preceded by actionsprescribed by γ1 , . . . , γk . We will abbreviate !γ1 . . . γk †0 to!γ1 . . . γk .

III. Equality and Submodel
Milner-Park’s bisimulation approach [17], [24] to observational equivalence has been a standard in concurrency theory.
Two refinements of the idea have played an important role inrecent studies of interaction models. The branching bisimulation of van Glabbeek and Weijland [38] imposes the condition
that a change-of-state internal action must be bisimulated. The
barbed bisimulation of Milner and Sangiorgi [20] provides forthe first time a model independent equivalence for processes.
Central to barbed bisimulation is the requirement that it isclosed under composition and that it preserves observability.
λDefinition 2. P is observable at a, notation P⇓a , if P −→ P0
for some P0 and some action λ at channel a.
In addition to the bisimulation property we shall pay particular attention to divergence. Our translations between models
are supposed to be divergence sensitive. The criterion we adopt
for divergence sensitivity was introduced by Priese [27].
Definition 3. A symmetric relation R on processes is a bisimλulation if one of the following is valid whenever Q R P −→ P0 :1) λ = τ and Q =⇒ Q0 R P and Q0 R P0 for some Q0 ;λ2) Q =⇒ Q00 R P and Q00 −→ Q0 R P0 for some Q00 , Q0 .
τ

τ

τ

τ

It is codivergent if P R Q −→ Q1 −→ . . . −→ Qi −→ . . .
τimplies that P =⇒ P0 R Qk for some k ≥ 1 and some process
P0 . It is extensional if (P | P0 ) R (Q | Q0 ) whenever P R Q and
P0 R Q0 . It is equipollent if P R Q implies P⇓a ⇔ Q⇓a for alla ∈ Cg .
The four properties defined in Definition 3 apply to allmodels. This is because they do not refer to any particularityof external actions. Internal actions are basically the same inall models [7] and is therefore model independent.

by the proof of a number of general results. See [8] for asystematic study.
A number of equivalences for higher order calculi have been
proposed and studied, notably by Thompsen [34], [35] andSangiorgi [29], [30]. These are weak bisimilarities without
any consideration to divergence. Divergence is important for
us since we shall discuss divergence sensitive interpretation
between models. Divergence is also important for the interpretation of computational models, say the lazy λ-calculus.
Proving that two processes are absolutely equal is often not
so straightforward. In many places of this paper we can use
the stronger but much easier equality defined next.
Definition 5. A symmetric codivergent bisimulation R is a
T-bisimulation if the following hold whenever PRQ:
a(A)

a(A)

1) If P −→ P0 , then Q =⇒ Q00 −→ Q0 for some Q0 , Q00
such that Q00 RP and Q0 RP0 .
a(A)
a(B)
2) If P −→ P0 , then Q =⇒ Q00 −→ Q0 for some Q0 , Q00
such that Q00 RP and Q0 RP0 and A(a, b) R B(a, b) for alla, b ∈ Cg .
The T-bisimilarity 'T is the largest T-bisimulation.
The proof that 'T is included in =F is not difficult.
B. Direct Interpretation of λ-Calculus
The syntax of the λ-calculus is given by
M

Definition 4. The equality =M on M-processes is the largest
reflexive, codivergent, extensional, equipollent bisimulation.
It is a standard exercise to show that the largest reflexive, codivergent, extensional and equipollent bisimulation exists [8],hence the well-definedness of =M . Notice that we need thereflexivity for the proof of the existence of =M . Without thereflexivity the binary relation {(!τ | !a, !τ | !a) | a ∈ Cg } would bea codivergent, extensional, equipollent bisimulation. We shalloften omit the subscript in =M . The equality =M is introduced
in [8], based on previous studies on the relative expressivenessof CCS variants and π variants [9]. In [8] the private channels
and the global channels are syntactically the same, following
the standard practice in process algebra [17], [19], [31].
Consequently the extensionality condition is supposed to beclosed under localization operator. In the present paper this is
unnecessary since all private channels in processes are bound.
The effectiveness of the equality =M has been demonstratedx | λx.M | MM 0 .

A λ-term is either a variable x, or an abstraction term λx.M,
or an application term MM 0 . The variable x in λx.M is bound.
A variable is free if it is not bound. A term is closed if all
variables appearing in it are bound. The operational semanticsof the lazy λ-calculus is defined by the following two rules:(λx.M)N→

M{N/x},MN→

M 0 N, if M → M 0 .

A. Process Equality
Putting together all the conditions introduced in Definition 3, we get the process equality we shall use in this paper.

:=

The equivalence closure of the one step lazy reduction → isthe β-conversion =β . The lazy reduction of a λ-term is unique.
It either terminates in an abstraction term, or terminates in aterm of the form xM1 . . . Mk , or diverges.
Given an injective function from the set of λ variables tothe set V of abstraction variables, a λ-term M is interpreted
as an abstraction according to the following definition.
~x

=

X,

~λx.M

= (uv)u(X).v[~M],

~MN

=

(uv)(mq)(~Mm,q | m[~N].q(Z).Zu,v ).

The process ~Ma,b is a “function” that inputs a “λ-term” atchannel a and output the result “λ-term” at channel b. The
correctness of the interpretation is guaranteed by the following
lemmas and corollary. We omit the routine proofs.
Lemma 6. If ~x = X then ~M{~N/X} = ~M{N/x}.
Lemma 7. M → N if and only if ~Ma,b →→ =F ~Na,b .
Corollary 8. For closed M, N, M =β N implies ~M =F ~N.

C. Relative Expressiveness
Another fundamental relationship in computer science isthe relative expressiveness between models. For such a relationship to be useful at all it must be defined in a model
independent way. Intuitively we regard M as a submodel of N
if for every process P of the former there is some process Q
of the latter such that Q is equal to P as it were; and moreover
the equality =M should be a subrelation of the equality =N . At
the technical level the definition of the expressiveness should
be a routine once the definition of equality has been fixed.
The reflexivity condition of Definition 4 must be generalized
to conditions on processes from two different models.
Definition 9. A binary relation ∝ from M-processes to Nprocesses is total if for every M-process P there is an Nprocess Q such that P ∝ Q. It is sound if P ∝ Q, P0 ∝ Q0 and
P =M P0 imply Q =N Q0 .
The soundness condition refers to both the equality of thesource model M and the equality of the target model N. For
the condition to make the best sense of it the two equalities
ought to be the same as it were. In our situation they are thesame equality on two different models. The basic idea of thenext definition is that the expressiveness relation is also thesame equality, albeit on the processes of two models.
Definition 10. A binary relation ∝ from M-processes to Nprocesses is a subbisimilarity if it is a total, sound, codivergent, extensional, equipollent bisimulation.
We write M v N if there is a subbisimilarity from M to N.
The notation M v N stands for the formal statement that M isa submodel of N. For example it is easy to see that CCS v π.
We write M @ N if M v N and N @ M. In [8] the subbisimilarity relationship has been used to classify the relative
expressiveness of several well-known models. Our criteria arestronger than most criteria proposed in literature [23], [11].
IV. Thesis on Interaction
With the requirement on physical implementability comes
the spatial operator “|”, the concurrent composition operator,that allows processes to interact on shared channels. This is
a let-it-happen combinator to which we do not and should
not assign any extra computational meaning. The semanticsof this operator is fixed; it is model independent. In literature
one sees several variants of this combinator. We take theview that there variants are all derived operators. This will beformalized in our thesis. Without any hierarchical structure inspace the spatial operator would be much less useful, hence theprivate channels and the localization operator. The localization
operator is a scope operator without any extra computational
meaning either. Its semantics is essentially model independent.
The other operators of an interaction model are intensional.
They define computational features pertain to particular models. An interaction model differs from another interaction
model in that they have different set of intensional operators.
These are the principles for the introduction of the absoluteequality and the subbisimilarity.

Following these principles it is easy to extend a computation
model to an interaction model. Suppose we would like todefine interactive Turing machine model. We let each machine
to have the capacity to input and output data at a finite
number channels. There could be many variations on the
choice of instruction set. But the model is basically thesame. In this model we can form systems by composing
individual machines. For instance we have a system or aprocess of the form (p)(M0 | (q)(M1 | M2 )) where M0 , M1 , M2
are interactive machines. The particularity of this model is thatthe configuration of a system never changes. For a particularformalization of the model, the reader is referred to [8]. We
shall denote this model by T.
The contents of communications in T are numbers. Formally
we use Presburger Arithmetic to reason about numbers. Presburger Arithmetic [26] is the first order theory of arithmetic
with three functional constructors (the nullary function “0”,the unary function successor “+1”, and the binary function
addition “+”) and two relations (“=” and “<”). We will always
abbreviate say “((0 + 1) + 1) + 1” to “3”. We will write` ϕ to mean that the Presburger formula ϕ is provable. It
is well known that the provability of the first order formula in
Presburger Arithmetic is decidable [26]. Throughout the paperi, j, k stand for natural numbers.
A. Computability Model
The starting point to formulate a thesis for interaction is toturn the computable functions into an interaction model. Thismodel is called computability model and denoted by C. The
C-processes are generated from the following grammar.
P:=

0 | Ω | Fab (f(x)) | a(i) | P | P.

The process Ω can only diverge. The functional process
Fab (f(x)) inputs a number, say i, at channel a, carries out thecomputation of f(i), and outputs the result at channel b if thecomputable function f is defined at i. The output process a(i)simply outputs i at channel a. The semantics is defined by thefollowing rules, in which f(i)↑ means f is undefined on i.
if f(i) = ja(i)Fab (f(x)) −→ b( j)if f(i)↑

a(i)

a(i)

a(i) −→ 0τΩ −→ Ω

Fab (f(x)) −→ Ω
a(i)

a(i)

P −→ P0

Q −→ Q0
τ(3)

P | Q −→ P0 | Q0

Definition 4 can be readily applied to the C-processes. The
equality =C has a simple characterization. Let the structuralcongruence ≡C be the least equivalent and congruent relationthat satisfies the following equalities: (i) 0 | P ≡C P, (ii)P | Q ≡C Q | P, (iii) O | (P | Q) ≡C (O | P) | Q, (iv) Ω | Ω ≡C Ω,
0and (v) Fab (f(x)) = Fab (f(x)) if f(x) is nowhere defined. The
following lemma is from [8].
Lemma 11. The two equalities =C and ≡C coincide.

B. Universal Model
The model C introduces a minimal expressive power on theinteraction models, the content computability. In the other direction our universal interaction model imposes a constraint on
all interaction models, which we call channel computability.
The model is an extension of the value-passing calculus VPCof Hoare [15] and Milner [17]. To understand the role of VPC
it suffices to say that VPC is to the recursion theory what F
is to the λ-calculus. The syntax of the model is given byT:=

0 | α(x).T | α(t).T | T | T | (p)T | if ϕ then T | !α(x).T.

In the conditional term if ϕ then T the expression ϕ is a
Presburger formula. The replication operator “!” only applies
to input terms. We may define !α(x).T by (p)(p | !p.α(x).p.T ).
The semantics is standard. In addition to the concurrent
composition rules defined in (3) there are following rules.
λT −→ T 0α(i)α(x).T −→ T {i/x}
α(i)

`t=i

α(t).T −→ Tλ`ϕ

if ϕ then T −→ T 0α(i)!α(x).T −→ T {i/x} | !α(x).T

A detailed exposure of VPC can be found in [6].
The universal model V differs from VPC in that the former
has a naming function µ : N → Cg that assigns a distinct
number to each global channel. For a number i we will write µi
for µ(i). The bijective function is meant to capture the intuition
that global channels can and must be accessed in a computableway. The function µ gives rise to an enumeration µ0 , µ1 , . . . of
the global channels. When we write a global channel a forexample we mean that a = µk for some number k. The syntax
of V is almost the same as VPC, except that the former has
additional prefix terms of the form µz (x).T and µz (t).T . The
semantics of V is the same as that of VPC. The processa(x).if decode(x) = k then µk (t) for instance decodes thenumber received at channel a and if the decoded number is the
key then it outputs t at the secret channel. We will prove thatthe processes definable in V can simulate the channel-passing
communication mechanism. We get a better understanding of
the channel computability from the following abbreviation.
µ s (x).T=(p)(p(s) | p(z).µz (x).T ),µ s (t).T=(p)(p(s) | p(z).µz (t).T ).

In V there is a maximal process 1 as it were defined by I | O,
where
I =

(p)(p(0) | !p(x).p(x + 1) | p(y).(p(0) | µy (z))),=(pq)(p(0) | !p(x).p(x + 1) | q(0) | !q(x).q(x + 1)
| p(y).q(z).(p(0) | q(0) | µy (z))).

O

Intuitively 1 is the process that can do any input action andany output action in a perpetual fashion.
The two-leg conditional term if ϕ then S else T is definedby if ϕ then S | if ¬ϕ then T . For clarity the term
if t = i0 then T 0 else if . . . else if t = ik then T kwill be written as case t of i0 ⇒ T 0 ; . . . ; ik ⇒ T k end case.

C. Models of Interaction
We have said enough motivations for the thesis, and wehave defined the minimal model C and the maximal model V.
Let’s spell it out without further ado.
Thesis on Interaction. ∀ M. C v M v V.
The formulation of the thesis depends crucially on the model
independence of the absolute equality and the subbisimilarity
relationship. One may cast doubt on the thesis by pointing outthat there are other model independent equalities and submodel
relationships. Does that mean that there are many theses forinteraction? Our answer has to be that for mathematical models
of interaction the equality and the submodel relationship are
unique for the reason that the observability of numbers is amodel independent notion. The definition of =, and that ofv as well, is discovered; it is not invented. This remark also
applies to Church-Turing Thesis. There has been no dispute
about the extensional equality of function to which ChurchTuring Thesis refers.
We call M complete if C v M and sound if M v V.
Intuitively a complete model is Turing powerful, and a complete and sound model is Turing equivalent, if one ignores theinteractional aspect of the model. The model C is the starting
point for the theory of definability of M, and V provides thetheory of unsolvability for all interaction models.
In [8] we established the completeness of T and VPC,
exploiting the simplification offered by Lemma 11.
Theorem 12. C v T v V and C v VPC v V.
Proof: The embedding function from VPC to V witnesses
VPC v V. The validity of T v V is due to the fact that Turingmachines can be interpreted by recursive functions.
We will prove in the following section that the functionalmodel F is also complete and sound. So our most influential
computation models can all be lifted to interaction models.
We will also show that the π-calculus satisfies the Thesis on
Interaction.
V. Completeness of Functional Model
We prove in this section that F is complete. The proof istypical of the completeness proofs. We shall explain it in somedetail. The reader should pay attention to the role played by
Lemma 11.
The first step to define the computable functions in F is
to fix an encoding in F of the natural numbers. Let A+
abbreviate (xy)x[A]. The numbers are defined by the following
abstractions:
b
0 =
k[
+1 =

(xy)y,(bk)+ .

If we try to code up the recursive functions in F, we soon
realize that we need to define in F the conditional term
if ϕ then T else T 0 ,(4)where the validity of ϕ is decidable. This is where the
Presburger Arithmetic comes into the picture.

A. Definability of Presburger Condition
In this subsection we look at the case where ϕ is a
Presburger formula containing no occurrences of quantifier. In
other words, ϕ is either an atomic formula of the form s = t,or an atomic formula of the form s < t, or φ ∧ ψ, or φ ∨ ψ or
¬φ inductively. The general definition of (4) in which ϕ is a
decidable predicate will follow from Theorem 15.
The process if ϕ ∧ ϕ0 then T else T 0 can be defined by
if ϕ then (if ϕ0 then T else T 0 ) else T 0 .
Similarly if ϕ ∨ ϕ0 then T else T 0 and if ¬ϕ then T else T 0
can be defined by conditional processes involving simpler
boolean formulae. It is therefore sufficient to define (4) for
atomic formulae. Firstly we define the auxiliary process if A =B then T else T 0 by(lm)(l[A].m[B] | !l(X).m(Y)†(nopq)T ? ).
where T ? stands for
Xno | Y pq | n(U).(p(V).l[U].m[V] | q.T 0 ) | o.(p(V).T 0 | q.T ) .
So if A and B are abstractions encoding the same number, thenif A = B then T else T 0 is equal to T , otherwise it is equal toT 0 . Secondly we interpret Presburger arithmetic term t as ~towhich is supposed to release the value of t at channel o. The
structural definition of ~to is given in Fig. 1. To define ~xo
we fix a bijective correspondence between the term variablesof the Presburger Arithmetic and the abstraction variables. We
assume that the capital X corresponds to the small x. Finally
we define the process if s = t then T else T 0 by(pq)(~s p | ~tq | p(X).q(Y).if X = Y then T else T 0 ).
The conditional process if s < t then T else T 0 is defined insimilar fashion.
B. Interpretability of Recursive Functions
With the help of the conditional processes, we are now able
to fix an interpretation of the recursive functions. To start with
we define copy process Cµν by the following process
µ(X).(mno) m[b0] | !o(X)†m[X] | (l)(l[X] | C) ,where
C = !l(X)†(pq)(X pq | m(Z).(p(Y).o[Z + ].l[Y] | q.ν[Z])).

(5)

The process Cab intends to input an abstraction, which is
supposed to be a number, at channel a and to output the
number at channel b. If the imported number is corrupted,
the copy process either terminates or interprets the imported
abstraction as some number and outputs it. It is typicallyused as a prefix operation. Let the notation Cµν .T stand forthe process obtained from Cµν by substituting q.(T | ν[X]) forq.ν[X] in (5). The role of Cµν in Cµν .T is to prevent malicious
code from ever getting into T .

We define a map ~ c that interprets every recursive function by an abstraction. Constant function λx1 . . . λxk .i, successor function λx.x+1 and projection function λx1 . . . λxk .xi areinterpreted respectively by the following abstractions.
Cnik=(uv)(p1 . . . pk )(Cup1 . . . Cupk | pi (X).v[bi]),Sr=(uv)(p)(Cup | p(X).v[X + ]),

P jik

=

(uv)(p1 . . . pk )(Cup1 . . . Cupk | pi (X).v[X]).

Suppose G0 = ~g0 c for an i-ary recursive function g0 and
G = ~g1 c , . . . , Gi = ~gi c for some k-ary recursive functions
g1 , . . . , gi . Let1

T j = p1 (X1 ) . . . pk (Xk ).(p1 [X1 ] . . . pk [Xk ] | G j (X1 , . . . , Xi )),jwhere G j (X1 , . . . , Xk ) = (q)(q[X1 ] . . . q[Xk ] | Gqo). The term T jiinputs the numbers at channels p1 , . . . , pk consecutively andthen must release these numbers in the same order so that they
can be used elsewhere. Let CPG0 ,G1 ,...,Gi be defined by(o1 . . . oi )(T 1 | . . . | T i | o1 (Z1 ) . . . oi (Zi ).(n)(n[Z1 ] . . . n[Zi ] | G0nv )).
The interpretation ~g0 (g1 , . . . , gi )c of the composition function g0 (g1 , . . . , gi ) is defined by(uv)(p1 . . . pk )(Cup1 . . . Cupk | CPG0 ,G1 ,...,Gi ).
Next we consider recursion and minimization. Let g, h, f be
respectively a (k+2)-ary recursive function, a k-ary recursivefunction, and a (k+1)-ary recursive function, and let G, H, F be
their interpretations. The recursion function rec(g, h) definedfrom g and h is calculated by the following equations:rec(g, h)(i1 , .., ik , 0)=h(i1 , .., ik ),rec(g, h)(i1 , .., ik , i + 1)=g(i1 , .., ik , i, rec(g, h)(i1 , .., ik , i)).

The interpretation ~rec(g, h)c defined in Fig. 2 uses an inductive algorithm. In the recursive call of !o(Y, Z, V)† ( ), theparameter records the intermediate value rec(g, h)(i1 , . . . , ik , y);Z is the (k+1)-th input; Y is y when the algorithm calculates rec(g, h)(i1 , . . . , ik , y). The inductive algorithm terminates
when Y reaches the (k+1)-th input value. The interpretation of
the minimization function mu(f), given in Fig. 2, makes use of
the standard algorithm. The definition of all recursive functions
is now complete.
The minimization function introduces undefinedness. Ourinterpretation treats undefinedness as divergence. The soundness of our interpretation is the following lemma.
Lemma 13. Suppose f is a k-ary recursive function. For all
i1 , . . . , ik , (p)(p[bi1 , . . . , b
ik ] | ~fc (p, ν)) =F ν[bj] if f(i1 , . . . , ik ) = j,bband (p)(p[i1 , . . . , ik ] | ~fc (p, ν)) =F Ω if f(i1 , . . . , ik )↑.
Proof: The notation Ω stands for the divergent process(p)(p | !p†p). The proof is by simple structural induction. Theinternal manipulations are all state preserving.

~ko

=

o[b
k],

~xo

=

(pq)(X pq | (p(U).o[U + ] | q.o[b0])),~t+1o=(p)(~t p | p(U).o[U + ]),~s+to=(pq)(~s p | ~tq | p(X).q(Y).(ln)(l[Y].n[X] | !l(V)†(pq)(V pq | (p(U).n(Z).l[U].n[Z + ] | q.n(W).o[W])))).
Fig. 1.

~rec(g, h)c=

~mu(f)c=

Encoding of Presburger Terms.

e | o[b(uv)(p1 . . . pk )(Cup1 . . . Cupk .Cup | (no)p1 (X1 ) . . . pk (Xk ).p(Z).(n[X]0, Z, b0]
| !o(Y, Z, V)† if Y = b
0∧Z =b0 then Hnv
else if Y = b0 ∧b
0 < Z then (l)(Hnl | l(V).o[b1, Z, V])bee | (lq)(q[X,e Y, V] | Gql | l(V).o[Y + , Z, V]))else if Y > 0 ∧ Y < Z then n(X).(n[X]ee | (q)(q[X,e Y, V] | Gqv )).
else if Y > b
0 ∧ Y = Z then n(X).(n[X]be(uv)(p1 . . . pk )(Cup1 . . . Cupk .Cup | (no)p1 (X1 ) . . . pk (Xk ).p(Z).(n[X] | o[0]ee | (l)(l[X,e Z] | Flq | q(V).if V = b| !o(Z)† n(X).(n[X]
0 then v[Z] else o[Z + ])))).
Fig. 2.

Encoding of Recursion and Minimization Functions.

C. Completeness and Definability
We need another technical lemma for the main result of thesection.
Lemma 14. Suppose f, g are equivalent recursive processes.
Then ~fc (ab) =F ~gc (ab) for all a, b.
Proof: In the light of Lemma 13, we only have to looka(A)at the case ~fc ab −→ L where A is not a number. This has
been taken care of because the copy process will check if A
is a number, and if not it will not proceed. And ~gc ab does
the same.
Every computable function corresponds to an infinite number of equal recursive functions. For each computable function
f(x) let’s fix a recursive function fr (x) that computes it. We now
define a straightforward encoding ~ ~ of C into F.
~0~
~Ω~
b
~Fa (f)~

= 0,
=

Ω,

~a(i)~= ~fr c (ab),= a(bi),~P | Q~= ~P~ | ~Q~ .

(6)

According to Lemma 13, the encoding is independent of the
choice of the recursive functions. Let ∝~ be the compositionof ~ ~ followed by =F . More specifically∝~ = (P, Q) | P is a C process, and ~P~ =F Q .
It is a subbisimilarity from the C-processes to the F-processes.

VI. V-Interpreter
This section serves two purposes. One is to show how toconstruct a V-process that acts as an interpreter for F. The
other is to prove the soundness of F by exploiting the powerof the interpreter. For the interpreter to work, there should bea way to translate an F-process to a number, and vice versa.
This is what Gödel encoding is about.
A. Gödel Index
For each k let h , . . . , i : N... × N| × {z} → N be an| {z }k

The Gödel encoding is based on two bijective functions.
The function ς : V → N provides a countable enumeration{X0 , X1 , . . .} of the abstraction variables. The bijective map
σ : Cv ∪ C g ∪ C p → N
is defined by

Theorem 15. C v F.
Proof: The total relation ∝~ is extensional by (6). It is anequipollent, codivergent bisimulation according to Lemma 13.
Suppose P =C Q, P ∝~ P0 and Q ∝~ Q0 . By Lemma 11,
one has P ≡C Q. It follows from the definition of ≡C , (6),the definition of ∝~ and the equivalence property of =F that
P0 =F Q0 .

keffective tupling function, where N denotes the set of natural
numbers. The corresponding projection functions are denotedby ( )k0 , . . . , ( )kk−1 . We often write zi for the j-th projection
when k is understood from context. For notational clarity we0even abbreviate ((z)ki )kj to zi, j . For every k we define rk , dk by(
0, if z = 0,
defrk (z) =i,
if 1 ≤ i ≤ k and ∃ j.z = k ∗ j + i,(0, if z = 0,defdk (z) =j, if z = k ∗ j + rk (z).

σ(µ)

=



3(i − 1) + 3, if µ = xi ,

3i + 1,
if µ = µi , 3i + 2,
if µ = pi ,(7)

assuming an enumeration {p0 , p1 , . . .} of the private channels
and an enumeration {x0 , x1 , . . .} of the channel variables, andmaking use of the naming function µ.

The encoding function ~ f for terms is defined below.
~0f~µ(X).T f~µ[A].T f0~T | T f~(p)T f
~A(µ, ν)f

def

=

0,

def

=

5 ∗ hσ(µ), ς(X), ~T f i + 1,

def=

5 ∗ hσ(µ), ~Af , ~T f i + 2,

def=

5 ∗ h~T f , ~T 0 f i + 3,

def=

5 ∗ hσ(p), ~T f i + 4,def

5 ∗ hσ(µ), σ(ν), ~Af i + 5,

=

and
~Af

def

(

=

2 ∗ (ς(X) − 1) + 2,
if A = X,
2 ∗ hσ(x), σ(y), ~T f i + 1, if A = (x, y)T.

Given an F-term T , we call ~T f the Gödel index of T .
Similarly we call ~Af the Gödel index of A. For the interpreter
to work properly, every natural number is understood as theindex of some abstraction. If k is not ~Af for any abstraction
A, it is deemed as an index of (x0 , x1 )0.
B. Interpreter
An interpreter Iα at α inputs a number at channel α,interprets it as the Gödel index of some F-process, and thensimulates the F-process. The process Iα consists of a parser
and a simulator. It is the process
α(x).(li lo l1 l0 mi mo mno) (Pn (x) | S n | mi (0) | mo (0) | m(k x ) | Li | Lo ) .
The locks Li , Lo are necessary to prevent the simulator fromrunning into deadlock. The processes mi (0), mo (0), m(k x ) provide the initial values of three counters accessible at mi , mo , mrespectively. The symbol k x stands for the maximum of theindices of private channels appearing in x. The parser Pn (x)parses a number imported at channel α to see if it is a Gödelindex of some F-process. It needs to check the following:1) Are all channel variables bound?
2) Are all private channels localized?
3) Are all abstraction variables bound?
If the input number is the Gödel index of some F-process P,
Pn (x) sends the index to the simulator through channel n. The
operations performed by Pn (x) are arithmetical. So it must be
definable by the completeness of F.
The simulator S n defined in Fig. 3 receives the index atchannel n and simulates the operations of P on-the-fly. For
clarity the recursive definition of In(y) and Out(y) are definedrecursively. They can be easily implemented in terms of thereplication operator. The simulator makes use of the naming
function to simulate transmissions at global channels. The
simulation of an interaction at a private channel is a bit
involved. Each process of the form (q)T is translated to a
V-process, called a dominion, of the form(o) In(u) | Out(u) | n [u/ς(q)]~T f ,where [u/ς(q)]~T f denotes the result obtained by substituting
u for ς(q) in ~T f . Different dominions make use of thesame symbol o for private channels with disjoint scopes. In

other words all private channels of an F-process are translated
syntactically to o. Since the simulator S n can only refer to a
finite number of symbols, this is essentially the only choice.
The component n([u/ς(q)]~T f ) invokes the simulator S nrecursively, which may take [u/ς(q)]~T f out of the dominion
it initially stays. The continuation of [u/ς(q)]~T f typicallywanders through different dominions. The question is then
how to ensure that the private channel q appearing in T and its
continuations is correctly interpreted. Our solution is to attach
to every dominion a distinct number u. If a continuation of[u/ς(q)]~T f tries to communicate at the private channel q, it
must first of all move to the dominion where n([u/ς(q)]~T f )originally stays before the action can be enabled. The movements have to be regulated so that no deadlock can occur.
We now explain the execution of S n in some detail. After
receiving the index z of an F-process, S n checks the type of
the process.
1) If r5 (z) = 1 then the number codes up an input process.
There are two subcases:(a) r3 (d5 (z)0 ) = 1. That is the process intends to input
something at the global channel µd3 (d5 (z)0 ) . If h is received
at channel µd3 (d5 (z)0 ) , then S n simulates the process with
the index [h/d5 (z)1 ]d5 (z)2 obtained by replacing d5 (z)1by h throughout the index d5 (z)2 .
(b) r3 (d5 (z)0 ) = 2. This is the process ready to input
a channel at the private channel with code number
d3 (d5 (z)0 ). This is reciprocal to Case 2(b).
2) If r5 (z) = 2, it is an output process. There are two cases:(a) r3 (d5 (z)0 ) = 1. In this case the process is ready to
output the index of an abstraction at the global channelµd3 (d5 (z)0 ) . After simulating this action, S n is invoked with
the index d5 (z)2 .
(b) r3 (d5 (z)0 ) = 2. In this case a private channel is used
to communicate a piece of information. The simulator
sets the output lock Locko and then starts locating thedominion in which the private channel gets interpreted.
Before the output lock is released no other output actionsat any private channel will be considered by the simulator. This is perfectly fine in an interleaving semantics.
The locating procedure interacts with a process of theform Out(u), where u is the number associated to adominion and it appears as an index for a distinct private
channel. The simulator checks if Out(u) is in the rightdominion. If not S n continues to interact with anotherprocess of the form Out( ). This procedure should beneither divergent nor deadlocked. The guard l0 blocks
Out(u) with wrong u once it has been examined. Thatremoves the possibility of generating infinite loops. The
right Out( ) must be eventually reached. When that
happens, the blocked Out( )’s are freed. The number
stored at mo indicates how many Out( )’s are still
blocked. The lock Locko is released at the same time
the last blocked Out( ) is released. Had Locko beenreleased while some Out( )’s are blocked, it would bepossible that a deadlock occurs. After the right dominionSn=(pq)!n(z). case r5 (z) of
1 ⇒ case r3 (d5 (z)0 ) of 1 ⇒ µd3 (d5 (z)0 ) (x).n([x/d5 (z)1 ]d5 (z)2 ); 2 ⇒ li .p(z) end case;2 ⇒ case r3 (d5 (z)0 ) of 1 ⇒ µd3 (d5 (z)0 ) (d3 (d5 (z)1 )).n(d5 (z)2 ); 2 ⇒ lo .q(z) end case;3 ⇒ n(d5 (z)0 ) | n(d5 (z)1 );4 ⇒ m(u). (m(u + 3) | (o)(In(u) | Out(u) | n([u/d5 (z)0 ]d5 (z)1 )));
5 ⇒ n ([d5 (z)0 /d2 (d5 (z)2 )0 , d5 (z)1 /d2 (d5 (z)2 )1 ] d2 (d5 (z)2 )2 );end case;
p(z). if d5 (z)0 = y then mi (v). if v > 0 then l1 .mi (v).In(y) else li .(I(z) | In(y))
else mi (v).pz.mi (v+1).l1 .mi (v). if v > 1 then l1 .mi (v−1).In(y) else li .(I(z) | In(y)) ,

In(y)

=

I(z)

=

o(x).n([x/d5 (z)1 ]d5 (z)2 );Out(y)=


q(z). if d5 (z)0 = y then mo (v). if v > 0 then l0 .m0 (v).Out(y) else lo .(O(z) | Out(y))
else mo (v).qz.mo (v+1).l0 .mo (v). if v > 1 then l0 .m0 (v−1).Out(y) else lo .(O(z) | Out(y)) ,

O(z)

=

o(d5 (z)1 ).n(d5 (z)2 ).

Li=li .li .Li ,Lo=

lo .lo .Lo ;Fig. 3.

Simulator S n .

is found the simulator can simulate the output action by
performing o(d5 (z)1 ) in that dominion.
3) If r5 (z) = 4 then the number codes up a localization
process. A dominion is declared to which is attacheda number larger than any number associated to any
dominion created so far. In this way it is guaranteedthat every dominion gets a distinguished number.
This completes the explanation of the simulator.
C. Correctness
An output action say a[A] of an F-process is bisimulatedby the output action a(~Af ) of the interpretation. Once thedeadlock prevention mechanism defined by Out(y) and In(y) is
understood, the interpretation is easy to justify. It is sufficient
to give an outline of how a subbisimilarity from F to V isconstructed using the interpretation.
A local context C[. . .] is defined as follows:
1) A hole [ ] is a local context;2) (p)C[. . .] is a local context if C[. . .] is;3) C0 [. . .] | C1 [. . .] is a local context if C0 [. . .], C1 [. . .] are.

2) Q = (li lo l1 l0 mi mo mno) (S n | mi (h) | mo (h) | m(g) | Li | Lo | O),
where O = (pq)D[T k1 , . . . , T k j ], for some local context
D[ ] in V and some V-terms T k1 , . . . , T k j .
3) D[. . .] is obtained from C[. . .] as follows: If C[. . .] =(q0 )C 0 [. . .] then D[. . .] = (o)(In(ki0 ) | Out(ki0 ) | D0 [. . .])for some ki0 ∈ {i1 , . . . , i j } and D0 [. . .] is obtained fromC 0 [. . .] in the same way. If C[. . .] = C0 [. . .] | C1 [. . .]then D[. . .] = D0 [. . .] | D1 [. . .] and D0 [. . .], D1 [. . .] areobtained from C0 [. . .], C1 [. . .] in the same way.
4) For each ki0 ∈ {k1 , . . . , k j }, T ki0 = n[[ki0 /σ(q0 )]~S ki0 f ]with appropriate q0 .
Now let R= be the composition R; =V . The relation R= isequipollent because the capacity to perform actions at aparticular global channel is preserved by the relation. Since
all arithmetic calculations are state-preserving operations andthe encoding does not introduce any new divergence, it
is both codivergent and bisimular. It is also extensional
because ( )( | mi (h) | mo (h) | O) | ( )( | mi (h0 ) | mo (h0 ) | O0 ) =( )( | mi (h+h0 +1) | mo (h+h0 +1) | O00 ) for a suitable term O00 .
The soundness condition is also met because every number isthe index of some abstraction. Hence the soundness of F.
Theorem 16. F v V.

If C[. . .] is a local context with k holes, C[T 1 , . . . , T k ] is theterm obtained by filling the holes by terms T 1 , T 2 , . . . , T k . We
define inductively a binary relation R between the set of Fprocesses and the set of V-processes in terms of local contexts.
Starting from the empty set, we throw a pair (P, Q) into R if
the following statements are valid:

Formally an interpretation ~ V of F-processes in V is afunction from the F-processes to the V-processes such that it
is contained in a subbisimilarity from F to V. By letting

1) P = C[S k1 , . . . , S k j ] for some local context C[ ] in F
and some F-terms S k1 , . . . , S k j .

we get an interpretation such that PR= ~PV . In other words
I p is an interpreter of F at channel p.

~PV = (p)(p[~Pf ] | I p ),

D. Soundness of Mobile Calculus
The completeness of the π-calculus is proved in [8]. The
soundness of the π-calculus can be established in similar way
the soundness of F is proved.
Using the bijective function defined in (7), the Gödel index
of a π-term is defined routinely as follows.
~0π~µ(x).T π~µµ .T π00~T | T π~(p)T π~!µ(x).T π

def

λ

0,

def

=

5 ∗ hσ(µ), σ(x), ~T π i + 1,

def=

5 ∗ hσ(µ), σ(µ ), ~T π i + 2,

def=

5 ∗ h~T π , ~T 0 π i + 3,

def=

5 ∗ hσ(p), ~T π i + 4,def

5 ∗ hσ(µ), σ(x), ~T π i + 5.

0

Using this Gödel encoding a V-interpreter of the π-calculus
can be constructed by basically recycling the idea of thealgorithm defined in Fig. 3. The so called name extrusion does
not cause any problem. Hence the following.
Theorem 17. C v π v V.

We call D(t1 , . . . , tk ) the instantiation of the parametric definition at t1 , . . . , tk . The unfolding of a parametric definition
admits dynamic binding in the sense that a private channel
may be captured by a localization operator. The so called αconversion is disowned in our setting. Two k-ary parametric definitions D(x1 , . . . , xk ) and D0 (x1 , . . . , xk ) are equal if
D(i1 , . . . , ik ) =V D0 (i1 , . . . , ik ) for all numbers i1 , . . . , ik .
Replication can be defined in terms of parametric definition.
Using the encoding of parametric terms defined in [5] and thetechnique of Section VI, we can prove the following resultthat provides a positive answer to the question left in [5].
Theorem 21. VPC with parametric definition can be interpreted in VPC with replication.

VII. Towards a Theory of Definability
The existence and the power of universal processes were
investigated in [5]. The study was carried out in VPC withparametric definition. For the universal model V we can domuch better.
Definition 18. Fix a Gödel encoding of V-terms, a universal
process Ua for V at a is a V-process such that (i) Ua cana(i)only perform input actions at a; and (ii) whenever Ua −→ P,then P =V Pi , where Pi is the V-process with Gödel index i.
The uniqueness of the universal process is an obvious
corollary of the definition. Its existence can be demonstratedusing the techniques developed in Section VI.
Theorem 19. There is a unique universal process at a.
Proof: If Ua and Ua0 are two universal processes accessible at a, then Ua =V Ua0 by definition. This is the uniqueness.
The construction of Ua is similar to the construction of theinterpreter Iα .
An interesting corollary of Theorem 19 is the following.
Corollary 20. V is equivalent to a submodel of V with a finite
set of symbols for private channel.
While we are on the subject we point out that the techniques
used in the construction of the universal process can be used
to answer a question posed in [5]. It asks if the valuepassing calculus with parametric definition is strictly stronger
than the value-passing calculus with replication. A parametricdefinition is defined by an equation
D(x1 , . . . , xk ) = T,λT {t1 /x1 , . . . , tk /xk } −→ T 0
D(t1 , . . . , tk ) −→ T 0==

say that D(x1 , . . . , xk ) is a k-ary parametric definition definedby (8). A parametric definition is a parameterized process.
The parameters can be values, as in our case, or channels.
In the presence of the naming function the former subsumes
the latter. The semantics of D(x1 , . . . , xk ) is defined by thefollowing.

(8)

where x1 , . . . , xk are variables for natural numbers. T contains no more free variables than x1 , . . . , xk and may containinstantiated occurrences of D of the form D(t1 , . . . , tk ). We

A posteori Theorem 21 has to be true if V is a universal
model. Extending V with parametric definition adds no additional power to V for the same reason.
Corollary 22. Parametric definition is admissible in V.
Theorem 19 lays down the foundation for a theory ofdefinability of V. We now give an outline of the theory.
By Corollary 22 we may as well let parametric definitions
be the first class citizens in V. In a straightforward manner
we define for each k > 0 a Gödel encoding for the k-ary
parametric definitions. Using standard technique it is routine toprove the V-version of the fundamental theorems of recursion
theory [28], [33].
1) Enumeration Theorem. There is a k+1-ary parametricdefinition Dk (x, x1 , . . . , xk ) such that Dk (i, x1 , . . . , xk ) isequal to the i-th k-ary parametric definition for all i.
2) S-m-n Theorem. There is an injective primitive recursive
k+1-ary function s such that Dk (x1 , . . . , xm , . . . , xm+n ) isequal to D s(k,x1 ,...,xm ) (xm+1 , . . . , xm+n ).
3) Recursion Theorem. Let f be a total computable function. There is a number n such that Dn (x) = D f (n) (x).
Using these theorems a familiar argument shows that there
exists a V-process that outputs at a particular channel theGödel index of itself. This example brings back one of thestarting points of this paper. In a majority of cases we do
not care about the explicit definition of a process of certain
functionality. All we need to know is the existence of such a
process. The theory of definability, which can be developed in
the spirit of recursion theory, is concerned with what can be
defined by interaction models.
Thesis on Interaction provides the foundation for the theoryof nondefinability of interaction models. No process can
exhibit the behavior specified in (1) in any interaction modelbecause such a process can not be defined in V. Nondefinability or unsolvability is an avenue of research that calls forfurther efforts.
We may extend V to a formalism that admits nondefinable processes. Let C be an m-ary parametric definition and D be an n-ary parametric definition. We saythat C is D-definable if there is a V-term T such thatC =V (x1 . . . xm )(q1 . . . qn )(T | D(q1 , . . . , qn )), where q1 , . . . , qn
are private channels that do not appear in D. In other words,
C is reducible to D. As another direction for future study
one may look for a theory of degrees of unsolvability in theinteractive framework.
VIII. Conclusion
Axiom of Completeness (∀M. C v M) was proposed asa foundational postulate in [8]. However a model satisfying
Axiom of Completeness could be too powerful to be implementable. This open-ended view is replaced by a closed world
view in present paper. Thesis on Interaction prevents us fromintroducing models that are not physically implementable.
What we have done in this paper is to provide evidence for theuniversal validity of the thesis. The three classical computation
models can all be lifted to interaction models in a naturalway. The λ-calculus can be promoted in two different ways,
resulting in a functional model and an object oriented one.
Needless to say the thesis need be further examined.
Being a very powerful model, V has very few primitives.
The prefix operator is necessary to define (sequential) computation. The concurrent composition operator is a let-ithappen extensional combinator that disowns any intensional
meaning. The localization operator goes with the composition
operator. The conditional operator is a natural programming
construct. In V nondeterminism is solely due to interaction. No
intensional nondeterminism is admitted in any form. It is easy
to convince oneself that a guarded choice, say a(0).P + b(1).Q,
cannot be defined in V without introducing divergence. This is
not to say that V is not universal enough. What it really indicates is that the guarded choice operator is not implementable.
The match and the mismatch operators in the π-calculus are
implementable. Our V-interpreter of the minimal π-calculus
can be easily extended to account for these operators.
From a programming language viewpoint a subbisimilarity
M v N is often given by an encoding. Formally an encoding
from M to N is an effective function e from the M-processes to
the N-processes such that e; vN is a subbisimilarity. Let’s write
M ve N if there is an encoding from M to N. A programming
practitioner would believe the following.
Effective Thesis on Interaction. ∀ M. C ve M ve V.
This is the extension of the Effective Church-Turing Thesis.
Now suppose there is an encoding e from a complete model
M to V. Then there is a V-process that translates the index
of an M-process to the index of a V-process. Composing thistranslation with the universal process for V one gets a Vinterpreter of M. So in the programming world a complete
model is sound if and only if it has a V-interpreter.

Acknowledgment
The support from the National Science Foundation of China(61472239, ANR 61261130589, 91318301) is acknowledged.
References[1] H. Barendregt. The Lambda Calculus: Its Syntax and Semantics. NorthHolland, 1984.
[2] G. Boudol. Towards a Lambda Calculus for Concurrent and Communicating Systems. TAPSOFT’89, Lecture Notes in Comuter Science 351,
149-161, 1989.
[3] A. Church. An Unsolvable Problem of Elementary Number Theory.
American Journal of Mathematics, 58:345-363, 1936.
[4] U. Engberg and M. Nielsen. A Calculus of Commincating Systems with
Label Passing, Report DAIMI PB-208, Computer Science Department,
University of Aarhus, 1986.
[5] Y. Fu. The Universal Process. To appear in Logical Methods in Computer
Science, 2017.
[6] Y. Fu. The Value-Passing Calculus. In Theories of Programming andFormal Methods, Lecture Notes in Computer Science 8051, 166-195, 2013.
[7] Y. Fu. Nondeterministic structure of computation. Mathematical Structures in Computer Science, 25:1295-1338, 2015.
[8] Y. Fu. Theory of Interaction. Theoretical Computer Science, 611:1-49,
2016.
[9] Y. Fu and H. Lu. On the Expressiveness of Interaction. TheoreticalComputer Science, 411:1387-1451, 2010.
[10] J. Gill. Computational Complexity of Probabilistic Turing Machines.
SIAM Journal Computing, 6:675-695, 1977.
[11] D. Gorla. Towards a unified approach to encodability and separation
results for process calculi. In: CONCUR 2008. Lecture Notes in Computer
Science 5201, 492-507, 2008.
[12] K. Gödel. Über Formal Unentscheidbare Sätze der Principia Mathematica und Verwandter Systeme. Monatshefte für Mathematik und Verwandter
Systeme I, 38:173-198, 1931.
[13] M. Hennessy and A. Ingólfsdóttir. A theory of communicating processes
with value-passing. Information and Computation 107, 202-236, 1993.
[14] Hennessy, M., Lin, H. Symbolic bisimulations. Theoretical Computer
Science 138, 353-369, 1995.
[15] C. Hoare. Communicating Sequential Processes. Prentice Hall, 1985.
[16] S. Kleene. General Recursive Functions of Natural Numbers. Mathematicsche Annalen, 112:727-742, 1936.
[17] R. Milner. Communication and Concurrency. Prentice Hall, 1989.
[18] R. Milner. Functions as Processes. Mathematical Structures in Computer
Science, 2:119-146, 1992.
[19] 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.
[20] R. Milner and D. Sangiorgi. Barbed bisimulation. In: ICALP’92, Lecture
Notes in Computer Science 623. 685-695, 1992.
[21] F. Nielsen. The Typed λ-Calculus with First Class Processes, Report
ID-TR:1988-43, Institute for Datateknik, Tekniske Hojskole, Denmark,Computer Science Department, University of Aarhus, 1986.
[22] M. Nielsen and I. Chuang. Quantum Computation and Quantum Information. Cambridge University Press, 2000.
[23] Palamidessi, C. Comparing the expressive power of the synchronousand the asynchronous π-calculus. Mathematical Structures in Computer
Science 13:685-719, 2003.
[24] D. Park. Concurrency and Automata on Infinite Sequences. In Theoretical Computer Science, Lecture Notes in Computer Science 104, 167-183,
1981.
[25] C. Petri. Communication with Automata. Dissertation, Darmstadt Technical University, 1962.
[26] M. Presburger. Über die Vollständigkeit eines Gewissen Systems derArithmetik Ganzer Zahlen, in welchem die addition als einzige operation
hervortritt. In Warsaw Mathematics Congress, 395:92-101, 1929.
[27] L. Priese. On the Concept of Simulation in Asynchronous, Concurrent
Systems. Progress in Cybernatics and Systems Research, 7:85-92, 1978.
[28] H. Rogers. Theory of Recursive Functions and Effective Computability.
MIT Press, 1987.
[29] D. Sangiorgi. Expressing mobility in process algebras: First order andhigher order paradigm. Ph.D. thesis, Department of Computer Science,
University of Edinburgh, 1992.

[30] D. Sangiorgi. From π-Calculus to Higher Order π-Calculus – and Back.
In Proc. TAPSOFT’93, Lecture Notes in Computer Science668, 151-166,
1993.
[31] D. Sangiorgi and D. Walker. The π Calculus: A Theory of Mobile
Processes. Cambridge University Press, 2001.
[32] E. Santos. Computability by Probabilistic Turing Machines. Trans.
American Mathematical Society, 159:165-184, 1971.
[33] R. Soare. Recursively Enumerable Sets and Degrees: A Study ofComputable Functions and Computably Generated Sets. Springer-Verlag,
Heidelberg, 1987.
[34] B. Thomsen. A calculus of higher order communicating systems. In:
Proc. POPL’89. 143-154, 1989.
[35] B. Thomsen. A theory of higher order communicating systems. Information and Computation 116, 38-57, 1995.
[36] A. Turing. On Computable Numbers, with an Application to the
Entsheidungsproblem. Proceedings of the London Mathematical Society,
42:230-265, 1936.
[37] X. Xu. Distinguishing and relating higher-order and first-order processes
by expressiveness. Acta Informatica, 49:445-484, 2012.
[38] R. van Glabbeek and W. Weijland. Branching Time and Abstractionin Bisimulation Semantics. In Information Processing’89, pages 613-618.
North-Holland, 1989.
[39] D. Walker. Objects in the π-calculus. Information and Computation,
116:253-271, 1995.