Logical Methods in Computer ScienceVol. 13(4:11)2017, pp. 1–23
www.lmcs-online.org

Submitted
Published

Mar. 4, 2016
Nov. 17, 2017

THE UNIVERSAL PROCESSYUXI FU
BASICS, Department of Computer Science, Shanghai Jiaotong University, Shanghai, Chinae-mail address: fu-yx@cs.sjtu.edu.cn

Abstract. A universal process of a process calculus is one that, given the Gödel index of a processof a certain type, produces a process equivalent to the encoded process. This paper demonstrates
how universal processes can be formally defined and how a universal process of the value-passing
calculus can be constructed. The existence of such a universal process in a process model can be
explored to implement higher order communications, security protocols, and programming languages
in the process model. A process version of the S-m-n theorem is stated to showcase how to embed therecursion theory in a process calculus.

1. Introduction
The classic recursion theory [Rog87, Soa87] is based on two fundamental observations. The first isthat there is an effective function φk that enumerates all the k-ary recursive functions. By fixing an
enumeration function we can write φki for φk (i), the i-th k-ary recursive function. The number i iscalled the Gödel number, or the Gödel index of the recursive function. The effectiveness of φki comesin both directions. One can effectively calculate a unique number from a given recursive function.
One can also effectively recover a unique recursive function from a given number. The S-m-n
Theorem states that for all k0 , k1 there is a total (k0 +1)-ary recursive function skk01 (z, x1 , . . . , xk0 ) suchthat φkk0 +k1 (i1 , . . . , ik0 , j1 , . . . , jk1 ) ' φk1k0

sk (k,i1 ,...,ik0 )( j1 , . . . , jk1 ) for all numbers k, i1 , . . . , ik0 , j1 , . . . , jk1 .

1

The equality ' means that either both sides are defined and they are equal or neither side is defined.
The second important observation is that there exists a (k+1)-ary universal function U k that, uponreceiving an index j of a k-ary recursive function f and k numbers i1 , . . . , ik , evaluates f(i1 , . . . , ik ).
In other words, U k ( j, i1 , . . . , ik ) ' φkj (i1 , . . . , ik ). The existence of such a universal function depends
crucially on Gödelization. It is by Gödelization that we can see a number both as a datum and a
program. The S-m-n Theorem and the universal functions are the foundational tools in recursion
theory. The practical counterpart of a universal function is a general purpose computer. The central
idea of the von Neumann structure of such a computer is that of the stored program, which isessentially the same thing as Gödelization. From the point of view of programming, a universal
function is an interpreter that works by interpreting a datum as a program. Again this is the idea ofGödelization.
Key words and phrases: Theory of interaction, recursion theory, Gödel encoding, universal machine.
Work supported by NSFC (61472239, PACE 61261130589).

l

LOGICAL METHODSIN COMPUTER SCIENCEc
DOI:10.23638/LMCS-13(4:11)2017

CC

Y. Fu
Creative Commons

2

Y. FU

Recursion theory plays a foundational role in computation theory and the theory of programming
languages. It makes one think why in the theory of process calculus, or more generally in concurrency
theory, the fundamental technique of Gödelization has not been utilized so far. One possible
explanation is that concurrent computations are often distributed. For processes scattered at different
locations the notion of a centralized universal process may sound alien. In retrospect however, theabsence of any universal process has been unfortunate. The π-calculus [MPW92], and CCS [Mil89]
as well, was proposed with the intention to be the ‘λ-calculus’ for concurrent computation. Yet in
the theory of process calculus there still lacks a notion comparable to that of decidability. There are
now some interesting techniques that allow one to prove negative results in process calculus [BGZ03,
BGZ04, Pal03, GSV04, FL10]. However they do not offer a method as general as the reduction
method in recursion theory. To develop a theory of solvability or definability for process calculus,
the ideas and the techniques of recursion theory are instructive. In programming theory, there
have been quite a few papers on implementing variants of π, or substantial extensions of them, on
current computing platforms. But there has been little discussion on how to implement a concurrent
programming language in the π-calculus. It’s understandably so since the idea of a universal process(or general interpreter) is indispensable in any such implementation. If we are serious about the claimthat the π-calculus is to concurrent computation what the λ-calculus is to functional computation, we
should look at implementation issues of concurrent programming languages in the π-calculus.
The above discussion leads to the conclusion that in both theory and practice there is a genuine
need for a process theory that goes beyond the classic recursion theory of function. The theory ofprocess calculus currently fails to meet that demand. What can we do to improve the situation? A
natural thing to do is to look at how Gödelization can be carried out in process calculi and how
universal processes can be constructed. Gödelization is a problem for a process calculus that cannot
even code up the natural numbers in a way that supports the interpretations of the computablefunctions within the calculus. We need to confine our attention to complete models. Intuitively acomplete process calculus is one that is expressive enough to admit good use of Gödelization. Now
suppose M is a complete model. What does a universal process of M look like? In the general case
it is unlikely that there is a single M-process capable of simulating all M-processes. A π-process
for example only refers to a finite number of global names. From the viewpoint of observational
equality, there is no way for it to simulate a π-process that uses strictly more global names. Ourstrong notion of equality completely rules out such a scenario. A universal process of a process
calculus should consist of a countable family of processes. Luckily we seldom need a single all
powerful universal process. In most applications it suffices to have a collection of processes, eachacting as a universal process for a set of processes of a certain type. A type for example could be a
finite set of names. Then a process is of that type if the names it contains all appear in that set. If
we think of it, having to use a restricted version of universal process does not really stop us fromderiving any definability/undefinability results in M. If something is definable in M, it is definable byan M-process of some type. If it is not definable, it is not defined by any M-process of any type.
We will look at Gödelization and the notion of universal process in VPC, a self-contained
version of the value-passing calculus. The reason to start with this particular model is that it is closer
to recursion theory than all the other process calculi [Fu13]. The contribution of this paper is theintroduction of a formal definition of universal process and the construction of a universal process for
VPC. The significance of the existence of a universal process is emphasized by illustrating a number
of applications. The technique developed in this work is expected to play a key role in the study ofprocess theory and programming theory implemented on process models.
The paper is structured as follows. Section 2 reviews the necessary background on VPC and theobservational theory of processes. Section 3 provides the formal definition of universal process andTHE UNIVERSAL PROCESS

3

demonstrates how to construct a universal process in VPC. Section 4 outlines three major applicationsof universal process. Section 5 formalizes the process version of S-m-n Theorem. Section 6 discusses
some future research topics.
Before engaging in the technicalities in the rest of the paper, we should comment on thepresentation style of this paper. We shall not spell out all technical details of our constructions, andconsequently nor shall we formally establish the correctness of the constructions. We will make fulluse of the fact that VPC is complete. This is very much like what recursion theoreticians make useof Church-Turing Thesis since the publication of Post’s pioneering paper [Pos44]. If one has not
built up enough confidence in exploiting the completeness of process models this way, one is advised
to consult [FL10, Fu13, Fu15, Fu16] in which sufficient technical details can be found.
2. Preliminary
In this section we define the semantics of the value-passing calculus, fix the notion of process equality
used in this paper, and explain in what sense the value-passing calculus is complete.
2.1. VPC. Value-passing calculi [Hoa85, Mil89, HI93a, HI93b, HL95] have been studied in various
contexts. In most of these studies, the value domains are left open-ended. A recent work that provides
a self-contained account of the value-passing calculi is [Fu13]. Since our value-passing calculus
is going to be the source model whose programs are to be interpreted by a universal process, an
open-ended attitude is inadequate. At the same time we hope to avoid the formality of [Fu13] forclarity. Fortunately there is a standard theory we can refer to. The value domain of our value-passing
calculus is taken to be Presburger Arithmetic [Pre29] (an English translation of the original paper
can be found in [Sta84]). This is the sub-theory of Peano Arithmetic defined by the constant 0, theunary function s and the binary function ‘+’. By overloading notations, we shall abbreviate sk (0) to
k and sk (x) to x + k. For our purpose the most attractive property of Presburger Arithmetic is thedecidability of its first order theory. There is a terminating procedure that decides the validity of every
first order formula of Presburger Arithmetic [Pre29, Mon76, End01]. This is a crucial property if avalue-passing calculus is seen as a programming model. The absence of the multiplication operator
does not affect the power of our model since the operator can be implemented in the value-passing
calculus [Fu13].
Let N be the set {0, s(0), s2 (0), . . .}, ranged over by i, j, k, and V be the set of natural number
variables, ranged over by x, y, z. The set T of value terms, ranged over by s, t, is constructed from thenumbers, the variables, and the binary operator ‘+’. The notation T0 stands for the set of closed terms.
The set B of first order logical formulae, ranged over by ϕ, consists of the formulas constructed fromthe terms, the logical operators ⊥, >, ∧, ∨, ⇒, ∃, ∀ and the binary relations <, =. We write ` ϕ if ϕ isa theorem of Presburger Arithmetic.
Let N be the set of names, ranged over by a, b, c, d, e, f, g, h. The set of the finite VPC-terms isdefined by the following BNF:
T:= 0 | a(x).T | a(t).T | T | T | (c)T | if ϕ then T.

4

Y. FU

The VPC-processes, denoted by P, Q, are the VPC-terms that contain no free variables. The namec in (c)T is a local name. A name is global if it is not local. The semantics of the finite VPCterms is given by the following labeled transition system, where α ranges over the action set{a(i), a(i) | a ∈ N, i ∈ N} ∪ {τ}.
Actiona(i)` t = i.

a(i)a(x).T −→ T {i/x}a(t).T −→ T

Compositionαa(i)S −→ S 0α

T −→ T 0
τS | T −→ S 0 | T
Localizationa(i)S −→ S 0

S | T −→ S 0 | T 0αT −→ T 0

c is not in α.

α(c)T −→ (c)T 0
ConditionαT −→ T 0α

if ϕ then T −→ T 0

` ϕ.

α

We shall use standard notations like =⇒ and =⇒. The recursion mechanism of a value-passing
calculus can be defined in a number of ways. They are not completely equivalent in terms ofexpressive power [BGZ03, BGZ04, Pal03, GSV04, FL10]. The infinite behaviors of our model VPC
is introduced by equationally defined terms. A parametric definition is given by the equation
D(x1 , . . . , xk ) = T,

(2.1)

where x1 , . . . , xk are parameter variables. In this paper we require that T does not contain any freevariable not in {x1 , . . . , xk }. The instantiation of D(x1 , . . . , xk ) at value terms t1 , . . . , tk , denoted byD(t1 , . . . , tk ), is T {t1 /x1 , . . . , tk /xk }. In addition to the finite terms, VPC also has instantiated terms of
the form D(t1 , . . . , tk ), where t1 , . . . , tk are value terms. The parametric definition (2.1) is generally
recursive in the sense that T may contain instantiated occurrences of D(x1 , . . . , xk ). It may also
contain instantiated occurrences of some D0 (y1 , . . . , y j ) given by another parametric definition. The
operational semantics of D(t1 , . . . , tk ) is defined by the following rule:α

T {t1 /x1 , . . . , tk /xk } −→ T 0

D(x1 , . . . , xk ) = T.
αD(t1 , . . . , tk ) −→ T 0
Now suppose D(x) = c(0) | (c)(c(x) | c(x) | c(z).D(z+1)). Then the following reductions are admissible:τD(1) −→ c(0) | (c)(c(1) | D(1 + 1))τ−→ c(0) | (c)(c(1) | c(0) | (c)(c(2) | D(2+1))).
In this example the global name c in the component c(0) gets captured every time the parametricdefinition is unfolded.
An alternative to parametric definition is replication. The syntax for the replication terms isgiven byT:= . . . | !a(x).T | !a(t).T.

THE UNIVERSAL PROCESS

5

The operational semantics of the replicator “!” is defined by the following transitions:
a(i)

a(i)

!a(x).T −→ T {i/x} | !a(x).T` t = i.

!a(t).T −→ T | !a(t).T!

We will denote by VPC the value-passing calculus with the replicator.
The replicator is a derived operator in VPC. The terms !a(x).T and !a(t).T are equal to theinstantiations of the following abstractions respectively.
C(x1 , . . . , xk ) = a(x).S | C(x1 , . . . , xk ),D(x1 , . . . , xk ) = a(t).T | D(x1 , . . . , xk ),

(2.2)
(2.3)

where {x1 , . . . , xk } is the set of the free variables appearing in !a(x).T respectively !a(t).T . We shallfreely use the replication operator in VPC. Leaving aside the question if VPC! is as expressive as
VPC for the moment, we point out that all recursive functions can be implemented in VPC! [Fu13].
The following abbreviations will be used
a.T
a.T

def

=

def

=

a(x).T, where x does not appear in T,
a(0).T.

We occasionally write for example t(x) to indicate that t contains the variable x. Accordingly wewrite t(s) for the term obtained by substituting s for x. The notations ϕ(x), ϕ(s) and T (x), T (s) areused similarly. We sometimes use the two leg if command defined as follows:
if ϕ then S else T

def=

if ϕ then S | if ¬ϕ then T.

For clarity we will write
case t of
ϕ0 (z) ⇒ T 0 (z);..
.
ϕk−1 (z) ⇒ T k−1 (z);ϕk (z) ⇒ T k (z)end casefor the nested if statement if ϕ0 (t) then T 0 (t) else if . . . else if ϕk (t) then T k (t). The auxiliary
notation let x = t in T stands for T {t/x}. This is useful when t is a long expression and x occurs in T
multiple times.
For a complete treatment of VPC the reader should consult [Fu13].
2.2. Equality and Expressiveness. The definition of a universal process must refer to a processequality. The choice of such an equality is not entirely orthogonal to the existence of a universal
process. It is conceivable that some sort of universal process exists with respect to a weak equality,
whereas it is impossible to have a universal process with respect to a stronger equality. To present our
result in its strongest form, we shall introduce a number of properties that we believe best describe
the correctness of our universal processes. The following account follows the general methodologyof [Fu16]. The description given here is however self-contained. In this section we assume that M isa process calculus and R is a binary relation on the set of M-processes. The notation R−1 stands forthe reverse relation of R.

6

Y. FU

A universal process is a generalization of a universal Turing machine. Upon receiving a number
the latter simulates the Turing machine encoded by the number. But how about the correctnessof the simulation? The answer is provided by the operational interpretation of the Church-Turing
Thesis [vEB90]. A sound translation of one computation model to another is a bisimulation ofcomputation steps à la Milner [Mil89] and Park [Par81]. Moreover if we take nondeterministic
computation into account the translation ought to be a branching bisimulation of van Glabbeek
and Weijland [vGW89]. The reader is referred to [Fu15] for a formal study of nondeterministic
computation in a process algebraic setting.
Definition 2.1. R is a bisimulation if the following clauses are valid whenever PRQ:
τ(1) If P −→ P0 then one of the following statements is valid:(i) Q =⇒ Q0 for some Q0 such that Q0 R−1 P and Q0 R−1 P0 .
τ(ii) Q =⇒ Q00 R−1 P for some Q00 such that Q00 −→ Q0 R−1 P0 for some Q0 .
τ(2) If Q −→ Q0 then one of the following statements is valid:(i) P =⇒ P0 for some P0 such that P0 RQ and P0 RQ0 .
τ(ii) P =⇒ P00 RQ for some P00 such that P00 −→ P0 RQ0 for some P0 .
A universal process must be sensitive to divergence. It would be unacceptable to interpret all processes
by divergent processes. The following definition is from [Pri78]. It is the best formalization of thetermination preserving property that goes along with the bisimulations [vGLT09, Fu16].
Definition 2.2. R is codivergent if the following statements are valid whenever PRQ:
τ

τ

τ

τ

(1) If there is an infinite internal transition sequence Q −→ Q1 −→ . . . −→ Qi −→ . . . thenτP =⇒ P0 RQk for some P0 and some k ≥ 1.
ττττ(2) If there is an infinite internal transition sequence P −→ P1 −→ . . . −→ Pi −→ . . . thenτ
Q =⇒ Q0 R−1 Pk for some Q0 and some k ≥ 1.
A universal process should also respect interactability. The barbedness of Milner and Sangiorgi [MS92]
αposes a minimal condition. We say that a process P is observable, notation P⇓, if =⇒−→ for some
α , τ. It is unobservable, notation P6⇓, if it is not observable.
Definition 2.3. R is equipollent if P⇓ ⇔ Q⇓ whenever PRQ.
The equipollence condition does not make much sense unless some kind of closure property isavailable. Concurrent composition and localization are the most fundamental operators in concurrency
theory. The former makes global interaction possible while the latter localizes such possibility. Hencethe following definition.
Definition 2.4. R is extensional if the following statements are valid:(1) If PRQ then (c)PR(c)Q for every c ∈ N;
(2) If P0 RQ0 and P1 RQ1 then (P0 | P1 )R(Q0 | Q1 ).
In [Fu16] it is argued that these properties give a model-independent characterization of processequality.
Definition 2.5. The absolute equality =M is the largest relation on the set of the M-processes thatsatisfies the following:(1) It is reflexive;(2) It is extensional, equipollent, codivergent and bisimilar.

THE UNIVERSAL PROCESS

7

It is easy to convince oneself that =M is well defined. So we have =VPC and =VPC! . We willoften omit the subscript.
The abstract definition of =M makes it difficult to work with. We need a characterization of =M
that relies neither on the equipollence condition nor on the extensionality condition. In practice it issufficient to have an external bisimilarity 'M satisfying 'M ⊆ =M .
Definition 2.6. A codivergent bisimulation R is an M-bisimulation if the following statements arevalid whenever PRQ and α , τ:αα(1) If P −→ P0 then Q =⇒ Q00 −→ Q0 R−1 P0 and PRQ00 for some Q0 , Q00 .
αα(2) If Q −→ Q0 then P =⇒ P00 −→ P0 RQ0 and P00 RQ for some P0 , P00 .
The M-bisimilarity 'M is the largest M-bisimulation.
Both 'VPC ⊆ =VPC and 'VPC! ⊆ =VPC! hold. We shall make use of these facts in the correctness
proofs.
By making use of the congruence = we can define semantically the one step deterministic
τcomputation P → P0 as an internal action P −→ P0 such that P0 = P, and the one step nondeterιτ
ministic computation P −→ P0 as an internal action P −→ P0 such that P0 , P. The rich structureof nondeterministic computation is discussed in [Fu15]. The distinction between the two classes
of internal actions is important to appreciate the working mechanism of the universal process. The
reflexive and transitive closure of → is denoted by →∗ .
If we consider interpreter rather than universal process, we need to relate a process of one model
to a process of another model. In other words we need to talk about ‘equality’ between the processes
from two different process calculi. This way of looking at the expressiveness relationship between
two process calculi leads immediately to the notion of subbisimilarity [Fu16]. The reflexivity ofDefinition 2.5 is turned into totality and soundness. Totality means that for each M-process P there
is an N-process Q such that P ∝ Q. Soundness is the condition that Q =N Q0 whenever P =M P0 ,P ∝ Q and P0 ∝ Q0 .
Definition 2.7. A binary relation ∝ from the set of M-processes to the set of N-processes is asubbisimilarity if it renders true the following statements:(1) ∝ is total and sound;(2) ∝ is extensional, equipollent, codivergent and bisimilar.
M is subbisimilar to N, notation M v N or N w M, if there is a subbisimilarity, a witness of M v N,
from M to N.
Intuitively M v N means that N is at least as expressive as M. The existence of a total relation ∝from M to N means that every M-process P gets interpreted by some N-process Q. The condition(2) of Definition 2.7, which is the same as the condition (2) of Definition 2.5, guarantees that P and
Q behave the same in respective models. Furthermore the soundness allows one to see P and Q as
equal as it were. The relation v is stronger than most of the expressiveness relations discussed in
the literature [BGZ03, BGZ04, Gor08, Pal03, Fu16], which makes the correctness of our interpretermore convincing.
2.3. Completeness. Both VPC and VPC! are Turing complete. There are several interpretationsof Turing completeness in the literature on process calculus [BGZ04, MP05, FL10]. The general
requirement on Turing completeness of a process model M can be summarized as follows:• There is an encoding ~  of the natural numbers in M.

8

Y. FU

• There is an interpretation ~  of recursive functions [Rog87] in M such that for every k-ary
computable function f(x1 , . . . , xk ) and all numbers i1 , . . . , ik the following operational property
holds: If f(i1 , . . . , ik ) is defined thenτ~i1  | . . . | ~ik  | ~f(x1 , . . . , xk ) =⇒≈ ~f(i1 , . . . , ik ),ττwhere =⇒ is the transitive closure of −→; if f(i1 , . . . , ik ) is undefined thenτ~i1  | . . . | ~ik  | ~f(x1 , . . . , xk ) =⇒≈ Ω,τwhere Ω is a divergent process whose only action is Ω −→ Ω, and ≈ is one of the termination preserving weak equalities. A criticism to this level of completeness is that the input numbers ~i1 , . . . , ~ik 
are not necessarily picked up properly by ~f(x1 , . . . , xk ), and the result number ~f(x1 , . . . , xk ) is notsent to any intended target. The evolution from ~i1  | . . . | ~ik  | ~f(x1 , . . . , xk ) to ~f(i1 , . . . , ik ) could
be too liberal.
The Turing completeness of an interaction model M means that an outsider can see that therecursive functions can be coded up using M-processes. It is an external completeness. A stronger
notion of completeness, a much more useful one in practice, is internal completeness. Intuitively
the internal completeness of M means that the insiders, the M-processes, are aware of the fact thatthey can compute all the computable functions. A formal treatment of this kind of completenessis provided in [Fu16]. In this paper it suffices to say that the completeness of M boils down to thefollowing:• For each name a and each number i there is an encoding ~ia of i at a.
• For all k ≥ 0 and all names a1 , . . . , ak , b, there is an encoding function ~ ba1 ,...,ak such that for every
k-ary recursive function f(x1 , . . . , xk ) the following statement is valid: For all natural numbers
i1 , . . . , ik , f(i1 , . . . , ik ) is defined if and only ifιι

~i1 a1 | . . . | ~ik ak | ~f(x1 , . . . , xk )ba1 ,...,ak −→. . . −→
| {z} =M ~f(i1 , . . . , ik )b ,k timesand f(i1 , . . . , ik ) is undefined if and only ifιι

. . . −→
~i1 a1 | . . . | ~ik ak | ~f(x1 , . . . , xk )ba1 ,...,ak −→| {z} =M Ω.
k times

The class {~ia }i∈N,a∈N provides an encoding of the natural numbers in M. The process ~ia isready to deliver the number i to a process at channel a. The process ~f(x1 , . . . , xk )ba1 ,...,ak inputs thenumbers i1 , . . . , ik sequentially at a1 , . . . , ak in k steps, after which it becomes some process, say
M, equal to ~f(i1 , . . . , ik )b . The only action of ~f(i1 , . . . , ik )b is to deliver the result to whicheverprocess wants a number at channel b. It should be remarked that M may perform a finite sequence ofdeterministic computations to simulate the computation of f(i1 , . . . , ik ). All the intermediate states ofthis simulation are equal to each other.
Both VPC and VPC! are complete in the above sense [Fu13, Fu16]. In both models the encoding~ia is defined by a(i).
The practical implication of the completeness of VPC and VPC! is that we may make use of aprocess without explicitly defining it. Let’s explain this point by examples. Suppose f(x1 , . . . , xk0 ),g(y1 , . . . , yk1 ) are computable functions. Then we may assume that
if f(x1 , . . . , xk0 ) = g(y1 , . . . , yk1 ) then T
is a VPC-term with the obvious semantics. In fact it can be defined by the following term(c)(d)(~f(x1 , . . . , xk0 )c | ~g(y1 , . . . , yk1 )d | c(x).d(y).if x = y then T ),

THE UNIVERSAL PROCESS

9where ~f(x1 , . . . , xk0 )c is the VPC-process that outputs the value of f(x1 , . . . , xk0 ) at c, whose existence
is guaranteed by the completeness of VPC. The process ~g(y1 , . . . , yk1 )d is similar. In the same
fashion we may think of a(f(x1 , . . . , xk )).T as the VPC-term (c)(~f(x1 , . . . , xk )c | c(z).a(z).T ). Moregenerally let ψ(x1 , . . . , xk ) be a semi-decidable property and χψ (x1 , . . . , xk ) be the partial characteristic
function of ψ. According to definition χψ (x1 , . . . , xk ) is the recursive function that returns ‘1’ at input
sequence i1 , . . . , ik when the property holds and diverges otherwise. Now we may regard if ψ then T
the same as if χψ = 1 then T . If ψ is a decidable property, then if ψ then T else T 0 can be interpretedasif χψ = 1 then T | if χψ , 1 then T 0 .
To simplify notation we shall use more liberal terms likeA( j).if j = 1 then T ( j).

(2.4)

In the above term the generalized prefix operation A( j) is understood as an arithmetic operation. Afterthe result j has been calculated, the process if j = 1 then T ( j) is ready to fire. By the completenessthe process in (2.4) can be implemented in VPC.
In the rest of the paper we shall use the internal completeness of VPC extensively in the mannerjust described.
For a systematic development of the equality theory, the expressiveness theory and the completeness theory from which the definitions given in Section 2.2 and Section 2.3 are imported, the reader
is referred to [Fu16]. The completeness of VPC is formally established in [Fu13].
3. Universal ProcessThis section presents the major contribution of the paper, which is to construct a universal process for
VPC. Since a universal process is a special case of an interpreter, we will first give a formal definitionof the latter. We then define an interpreter of VPC! in VPC. Finally we modify the definition of theinterpreter to produce the desired universal process of VPC. We hope that this two step construction
offers a clearer presentation of our methodology.
Suppose L, M are complete models. We intend to formalize the relationship saying that M
is capable of interpreting all the L-processes within M. Informally an interpreter of L in M is an
M-process such that after inputting a Gödel number of an L-process it behaves like the L-processrepresented by the number. A prerequisite for the existence of such an interpreter is that M should be
at least as expressive as L. This is because if L @ M then there is an L-process whose interactive
behavior cannot be simulated by any M-processes. When this is the case there cannot be any
interpreter of L in M. We conclude that every interpreter of L in M is based on an expressiveness
relation ∝ from L to M.
What is expected of an interpreter? There is no point for it to simulate a term containing
free variables. But it is expected to be able to manipulate bound variables since they only act asplaceholders. An interpreter can deal with a finite number of global names. But no interpreter canstore an infinite number of global names. The issue concerning local names is more tricky. Different
models have different naming policies. Some models admit dynamic creation of local names, others
do not. So in general an interpreter must know the number of distinct local names appearing in aprocess in order to simulate it properly. Talking about the number of distinct names, we would liketo emphasize that (b)(ab.b | (b)(c)ab.ac.b.c) contains two, not three, distinct local names, althoughsemantically there are three local names. This static view is important for Gödelization. Let N ∗ be
the set of finite lists of names, ranged over by . The notation a ∈  means that a appears in . We
have the following description of an interpreter:

10

Y. FU

~0i
~a(x).T i~a(t).T i~T | T 0 i~(c)T i~if ϕ then T i~!a(x).T i~!a(t).T i

def

=

0,

def

=

7 ∗ hς(a), ς(x), ~T i i + 1,

def=

7 ∗ hς(a), ~tς , ~T i i + 2,

def=

7 ∗ h~T i , ~T 0 i i + 3,

def=

7 ∗ hς(c), ~T i i + 4,

def=

7 ∗ h~ϕς , ~T i i + 5,def=

7 ∗ hς(a), ς(x), ~T i i + 6,

def

7 ∗ hς(a), ~tς , ~T i i + 7.

=

Figure 1: Gödel Index of VPC! -Term.
i, An interpreter of L in M is a family {Ic }i∈N, ∈N ∗ ,c<  of M-processes such that, for
all i ∈ N,  ∈ N ∗ and c ∈ N such that c < , after picking up a Gödel number ati, channel c the process Ic can simulate all L-processes that have at most i distinct
local names and contain no more global names than those appearing in .
1 ...ak
We will write Ii,aif  is the list a1 . . . ak . The superscript i is often omitted. The interpretation of
c
i, 
i, 0
a number by Ic differs from the interpretation of the same number by Ic in that they have different
0
i, 
i ,
interfaces. However Ic and Ic may produce the same interpretation of a number if the number
encodes a process that has at most min{i, i0 } local names.
Now suppose k is the Gödel index of an L-process P whose set of global names is a subsetof {a1 , . . . , a j } and whose number of local names is no more than i. Let {~ c }c∈N be an indexed
i,a ...aencoding function of the natural numbers in M. The process Ic 1 j must satisfy the following
property: There exists a unique Q such thati,a ...a j~kc | Ic 1ι−→ Q ∝−1 P,(3.1)

where ∝ is the subbisimilarity the interpretation is based upon and ∝−1 is the inverse relation of ∝.
i,a ...a
After a single step interaction with ~kc the process Ic 1 j becomes an M-version of P under ∝.
Since there may be many subbisimilarities from L to M and possibly infinite number of encodingsof the natural numbers into M, it is more precise to define an interpreter of L in M as the tuplei, h{Ic }i∈N, ∈N ∗ ,c< , ~ , ∝i that satisfies (3.1). This completes the formal definition of interpreter.
Let’s write L ∈ M if there is an interpreter of L in M. We may think of L ∈ M as an internalversion, or a programming version, of L v M. In the terminology of programming language, L ∈ M
says that L can be implemented in M.
The distinction between a translation and an implementation should now be clear. A translation
is a reduction from a source model to a target model. It is a meta theoretical operation. An
implementation is a family of processes in the target model that is capable of reproducing a processof the source model at will.
3.1. Gödel Index. We avail ourselves of an effective bijective function
h , . . . , ik : N... × N| × {z} → N,
k times

whose inverse function is composed of the unary functions ( )0 , . . . , ( )k−1 . For clarity we sometimes
write for instance zi, j for ((z)i ) j when no confusion arises. We assume that h0, 0, . . . , 0ik = 0, and weTHE UNIVERSAL PROCESS

11

often omit the subscript in h , . . . , ik . For convenience we assume that the unary pairing function is
the identity function and the 0-ary pairing function is the constant 0.
By abusing notations, let ς denote both a bijective function from the set N of names to N and abijective function from the set V of variables to N. Using ς as an oracle function, we can define aneffective bijective function from the set T of terms to N and an effective bijective function from theset B of formulas to N. We will denote both by ~ ς and omit the obvious structural definition.
Using the standard technique the Gödel number of a VPC! -term is defined by the function ~ iintroduced in Figure 1. The function ~ i is a bijection between the set of the VPC! -terms and the setof the natural numbers. It should be emphasized that we prohibit the use of α-conversion when we areassigning Gödel numbers to the VPC! -terms. The encodings of say a(x).a(x).b(x) and a(x).a(y).b(y)are different, even though they are treated as syntactically the same term when α-conversion isadmitted.
We get another set of Gödel indices if we use an oracle function different from ς. The definitionof our interpreter does not depend on any particular choice of such a function. For a VPC! -process P
using k global names a1 , . . . , ak and i local names, a normal index of P is the one in which the global
names a1 , . . . , ak are indexed by 1, 2, . . . , k and the local names are indexed by k + 1, k + 2, . . . , k + i.
3.2. A VPC Interpreter. Having fixed the Gödel index for VPC! , we are ready to define an interpreter of VPC! in VPC. The new problem with such an interpretation is how to simulate interactions
properly. The proofs of Turing equivalence in computation theory literature boil down to establishingeffective codivergent bisimulation relations from source models to target models. We extend thisapproach to encodings that take care of equipollence and extensionality. A major difference between
an encoding of one computation model into another and an encoding for interaction models is thatthe former is a translator whereas the latter is an interpreter. Since a process normally receives
messages from environment in its life cycle, and the behaviour of the process after an input action
depends on the information content of received message, the translation of a component of theprocess cannot be fixed in a static fashion. It has to be done during execution, hence the on-the-fly
style of interpretation.
i, 
1 ...ak
The interpreter is a family of processes {Id }i∈N, ∈N ∗ ,d< . The definition of Ii,ais given byd
1 ...akIi,ad= d(z).(h)(Pi (z) | h(z).Si (z)).

(3.2)

The interpreter executes the two subroutines sequentially.
• If z is the Gödel number of a process, say A, whose global names are among a1 . . . ak and thenumber of the local names appearing in it is bounded by i, the parser Pi (z) transforms z to anormal Gödel index z0 that codes up a process α-convertible to A, and then releases z0 through the
1 ...akchannel h. If z is illegitimate the parser aborts the interpretation. In other words Ii,achoosesdto interpret the index of a process of a wrong type as an index for 0.
• The simulator Si (z0 ) operates on the received normal Gödel number and simulates the processindexed by the number.
The interpretation makes use of the following recursive functions r7 , d7 :(0, if z = 0,
def
r7 (z) =i, if 1 ≤ i ≤ 7 and ∃ j.z = 7 ∗ j + i,(0, if z = 0,
def
d7 (z) =j, if ∃i∈{1, . . . , 7}.z = 7 ∗ j + i.

12

Y. FU

case z ofr7 (z)=0 ⇒ c(x).(if x = 1 then e else c(x − 1));r7 (z)=1 ⇒ if L1 (d7 (z)0 ) then Gi (d7 (z)2 , hd7 (z)1 + 1, vi);
r7 (z)=2 ⇒ if L21 (d7 (z)1 ) then if L20 (d7 (z)0 ) then Gi (d7 (z)2 , v);
r7 (z)=3 ⇒ c(x).(c(x + 1) | Gi (d7 (z)0 , v) | Gi (d7 (z)1 , v));r7 (z)=4 ⇒ if L4 (d7 (z)0 ) then Gi (d7 (z)1 , v);
r7 (z)=5 ⇒ if L5 (d7 (z)0 ) then Gi (d7 (z)1 , v);
r7 (z)=6 ⇒ if L6 (d7 (z)0 ) then Gi (d7 (z)2 , hd7 (z)1 + 1, vi);
r7 (z)=7 ⇒ if L71 (d7 (z)1 ) then if L70 (d7 (z)0 ) then Gi (d7 (z)2 , v)
end case.
Figure 2: Grammar Checker Gi (z, v).
The operation carried out by the parser is purely arithmetical. So it can be implemented in VPC.
Let’s however take a look at an outline of the following implementation of Pi (z):(g1 . . . gk+i )(c)(e)(k+iY

g j (0) | c(1) | Gi (z, 0) | e.Ni (z, 0)),

(3.3)

j=1

Q
where k+i
j=1 g j (0) stands for g1 (0) | . . . | gk+i (0). The grammar checker Gi (z, v) is defined in Fig. 2. It
aborts the interpreter if any one of the following happens:• The number of the indices of global names is more than k.
• The number of the indices of local names is more than i.
• There is an index for a free variable.
At the name c is recorded the number of the concurrent components the parser has encountered. Initially there is only one component, which explains the presence of c(1). The parser ends successfully
if in the end the value at c is 0. The names g1 , . . . , gk are used to store the indices for the global names
and the names gk+1 , . . . , gk+i for the local names. If j1 is the first index for a local name Gi (z, v) encounters, the grammar checker stores j1 +1 at gk+1 . This can be done by invoking gk+1 (x).gk+1 ( j1 +1).
Similarly if j2 is the second index of a local name Gi (z, v) encounters, then Gi (z, v) stores j2 + 1 at
gk+2 . In completely the same fashion, the grammar checker stores the Gödel numbers that represent
the global names at g1 , . . . , gk in the order they are discovered. The second parameter v of Gi (z, v)
codes up the bound variables already discovered. If for example the bound variables are x1 , . . . , xk0
encountered in that order then v would be hς(xk0 ) + 1, hς(xk0 −1 ) + 1, . . . , hς(x1 ) + 1, 0i . . .ii. The
Boolean functions L1 , L21 , L20 , L4 , L5 , L6 , L71 , L70 check if the number of names is under the limit or if
all variables are bound. We now explain how Gi (z, v) works.
• r7 (z) = 0. If the number of concurrent components becomes zero, end Gi successfully and initiate
the normalizer Ni (z, 0).
• r7 (z) = 1. The number d7 (z)1 is the index of a bound variable. The process L1 (d7 (z)0 ) needs tomake sure that if d7 (z)0 is neither the index of a local name nor an index of a global name that has
been recorded before, then the number stored at gk must be 0. If L1 (d7 (z)0 ) succeeds, the number
d7 (z)0 + 1 is stored at the least g j that has not been used. After L1 (d7 (z)0 ) has ended successfully,
the number d7 (z)1 + 1 is added to the list of the indices of the bound variables already parsed andis passed down recursively.
• r7 (z) = 2. The subroutine L21 (d7 (z)1 ) checks if the term represented by the number d7 (z)1 contains
an unknown variable. It aborts if it encounters an index that does not appear in the tuple encoded

THE UNIVERSAL PROCESS

13case z ofr7 (z)=0 ⇒ h(0);r7 (z)=1 ⇒ Find(d7 (z)0 , w, y).(b)(b(x).h(7∗hy, d7 (z)1 , xi+1) | (h)(h(u).b(u) | Ni (d7 (z)2 , w)));
r7 (z)=2 ⇒ Find(d7 (z)0 , w, y).(b)(b(x).h(7∗hy, d7 (z)1 , xi+2) | (h)(h(u).b(u) | Ni (d7 (z)2 , w)));
r7 (z)=3 ⇒ (b1 b2 )(b1 (x1 ).b2 (x2 ).h(7∗hx1 , x2 i+3)
| (h)(h(u).b1 (u) | Ni (d7 (z)0 , w)) | (h)(h(u).b2 (u) | Ni (d7 (z)1 , w)));
r7 (z)=4 ⇒ (b)(b(x).h(7∗hd7 (z)0 , xi+4) | (h)(h(u).b(u) | Ni (d7 (z)1 , hd7 (z)0 , wi)));r7 (z)=5 ⇒ (b)(b(x).h(7∗hd7 (z)0 , xi+5) | (h)(h(u).b(u) | Ni (d7 (z)1 , w)));
r7 (z)=6 ⇒ Find(d7 (z)0 , w, y).(b)(b(x).h(7∗hy, d7 (z)1 , xi+6) | (h)(h(u).b(u) | Ni (d7 (z)2 , w)));
r7 (z)=7 ⇒ Find(d7 (z)0 , w, y).(b)(b(x).h(7∗hy, d7 (z)1 , xi+7) | (h)(h(u).b(u) | Ni (d7 (z)2 , w)))end case
Figure 3: Normalizer Ni (z, w).
by v. If L21 (d7 (z)1 ) succeeds, L20 (d7 (z)0 ) checks the legitimacy of the encoding d7 (z)0 . The process
L20 works in the same manner as the process L1 .
• r7 (z) = 3. The counter at c is incremented by 1 since one concurrent component is split into two.
• r7 (z) = 4. The subroutine L4 (d7 (z)0 ) checks if the number d7 (z)0 + 1 is the same as the number
stored at some g j , where k + 1 ≤ j ≤ k + i. If the answer is positive, L4 (d7 (z)0 ) succeeds; otherwise
it checks if the number at gk+i is 0. If the answer to the latter query is negative, it aborts; otherwise
it succeeds after it has stored the number d7 (z)0 + 1 at the appropriate g j .
• r7 (z) = 5. The subroutine L5 (d7 (z)0 ) checks if the number d7 (z)0 codes up a well formed formula.
Specifically it needs to make sure that the formula coded up by the number does not contain any
free variable.
• r7 (z) = 6, r7 (z) = 7. These cases are similar to the cases r7 (z) = 1, r7 (z) = 2 respectively.
After Gi (z, 0) has ended successfully, it starts the process Ni (z, 0).
Using the values stored at g j ’s, Ni (z, 0) transforms Gödel index z to a normal Gödel index z0 andthen releases z0 at h. An implementation of Ni is given in Fig. 3. The operation Find( j, w, y) returns
as the value of y the j0 such that j is the number stored at g j0 . If j appears in w, then look for theindex j0 in {k + 1, . . . , k + i}; otherwise look for the j0 in {1, . . . , k}. In w are stored the local namesthat might appear in the term being processed. This additional complexity is due to the fact that a
number could denote both a local name and a global name. By making use of dynamic binding, arecursive invocation of Ni (z, w) collects through the localized channel h the normal encoding of a
subterm and passes it to its caller using the local channel b.
The simulator Si (z), defined in Fig. 4, simulates the VPC! -process coded up by z in an on-the-fly
fashion. The arithmetical operations referred to in Fig. 4 are described below:• The notation [x/d7 (z)1 ]d7 (z)2 stands for the Gödel number obtained from d7 (z)2 by substituting x,
which must have been instantiated by an input action at the moment this operation is executed, ford7 (z)1 .
• The notation val(d7 (z)1 ) denotes the result of evaluating the term expression coded up by d7 (z)1 .
Similarly val(d7 (z)0 ) denotes the result of evaluating the formula coded up by d7 (z)0 . Notice thatwhen the evaluation operations start, neither d7 (z)0 nor d7 (z)1 contains any variables.
The prefix operation Nth(d7 (z)0 , y) returns j as the value of y if d7 (z)0 is stored at g j , where 1 ≤ j ≤k + i. Some comments on Si (z) are as follows:

14

Y. FU

case z ofr7 (z)=0 ⇒ 0;
r7 (z)=1 ⇒ Nth(d7 (z)0 , y).ay (x).Si ([x/d7 (z)1 ]d7 (z)2 );r7 (z)=2 ⇒ Nth(d7 (z)0 , y).ay (val(d7 (z)1 )).Si (d7 (z)2 );r7 (z)=3 ⇒ Si (d7 (z)0 ) | Si (d7 (z)1 );r7 (z)=4 ⇒ Nth(d7 (z)0 , y).(ay )Si (d7 (z)1 );r7 (z)=5 ⇒ if val(d7 (z)0 ) then Si (d7 (z)1 );r7 (z)=6 ⇒ Nth(d7 (z)0 , y).!ay (x).Si ([x/d7 (z)1 ]d7 (z)2 );r7 (z)=7 ⇒ Nth(d7 (z)0 , y).!ay (val(d7 (z)1 )).Si (d7 (z)2 )end case
Figure 4: Simulator Si (z).
• r7 (z)=1. The continuation ay (x).Si ([x/d7 (z)1 ]d7 (z)2 ) is an abbreviation of
if y=1 then a1 (x).Si ([x/d7 (z)1 ]d7 (z)2 ) | . . . | if y=k then ak (x).Si ([x/d7 (z)1 ]d7 (z)2 ).
We need to know the number of local names in advance in order to define the above process. If we
1 ...ak
hope to drop the superscript i from Ii,adefined in (3.2) we need to look for a very differentdinterpretation. In case r7 (z)=2, the subterm ay (val(d7 (z)1 )).Si (d7 (z)2 ) is defined similarly.
• r7 (z)=4. This case deserves special attention. The simulator makes essential use of the dynamic
binding plus recursive definition. The number in Si (d7 (z)1 ) that encodes ay is decoded into ay , andthe continuation is restricted by the operator (ay ) dynamically. An implementation of the recursive
call of the simulator in VPC! would render the localization operator (ay ) detached from the bodyto which the operator should apply. For this reason the present encoding does not work in VPC! .
It is remarkable that the interpreter uses only one dummy variable x. No confusion among the boundvariables can ever arise.
Although we have not supplied all the details of the interpretation, the key ingredients that
support the following claim have all been spelled out.
Theorem 3.1. VPC! ∈ VPC.
Proof. The argument given here rests on the completeness of VPC [Fu13] and our trust in the
Church-Turing Thesis. We summarize the main points below:• The encoding of the natural numbers is given by the class {a(k)}k∈N,a∈N . This encoding is correctwith respect to the absolute equality =VPC [Fu13].
i, • All the number theoretical operations involved in the definition of Id , specifically the parser
defined in (3.3), are computable. It follows that these operations are all definable in VPC.
• The relation ∝i : VPC! → VPC is basically the structural embedding composed with the equality
relation =VPC , where the replication operator in VPC! is interpreted by the derived replication
operator defined in (2.2) and (2.3).
• Let I denote the composition S; =VPC , where S denotes the following relation
P is a VPC! process, all global names of P 






i, 
(P, (d)(d(k) | Id )) are in , the number of local names of P is 
.







no more than i, k is an index of P, and d < .
To establish (3.1) it is sufficient to demonstrate that I is a subbisimilarity. It is easy to argue
informally that the definition of the simulator in Fig. 4 renders true the following statements:

THE UNIVERSAL PROCESS

15

i, 

– Since all the actions of P are also actions of (d)(d(k) | Id ), the following explicit bisimulation
property is valid whenever PSM =VPC Q:αα∗ If P −→ P0 then Q →∗ −→ Q0 =VPC M 0 S−1 P0 for some Q0 and M 0 .
αα∗ If Q −→ Q0 and α , τ, then P −→ P0 SM 0 =VPC Q0 for some P0 , M 0 .
ιι∗ If Q −→ Q0 then P −→ P0 SM 0 =VPC Q0 for some P0 , M 0 .
∗ If Q → Q0 then either PSM =VPC Q0 or P → P0 SM 0 =VPC Q0 for some P0 , M 0 .
– I is codivergent since the extra number theoretical manipulations do not introduce any divergence.
These properties are enough for us to conclude that I is a subbisimilarity.
This completes the proof sketch.
3.3. Universal VPC Process. A self-interpreter for M is an interpreter of M in M. Such an interpreter is based on a subbisimilarity from M to M. In general there is more than one subbisimilarity
from M to M [Fu16], among which the absolute equality =M offers a canonical relation in the sensethat every process is interpreted by itself. An interpreter of M in M based on the absolute equalityi, =M is called a universal process for M. We will write h{Uc }i∈N, ∈N ∗ ,c< , ~ i for a universal processi, of M. For all i, , c the process Uc must satisfy the following property: If P is of the right type andk is a Gödel index of P then a unique Q exists such thati, ι~kc | Uc −→ Q =M P.

(3.4)

The aim of this subsection is to modify the interpreter constructed in the previous subsection to
obtain a universal process for VPC.
We need to explain how parametric definitions are treated. Now every VPC-term refers to only afinite number of parametric definitions. Suppose the parametric definitions appearing in T are givenby the following equations:D1 (x11 , . . . , x1i1 ) = T 1 ,
..
(3.5)
.
Dk (xk1 , . . . , xkik ) = T k ,for some k ≥ 0. When k = 0 we understand that T contains no occurrence of any parametricdefinition. The Gödel index ~T u of T is defined as follows:def~T u = hk, h~T d , ~T p ii.

(3.6)

The components of (3.6) have the following readings:• k is the number of parametric definitions in (3.5). According to our notational convention ~T d ,which is a k-ary tuple, is 0 when k = 0.
• The index ~T d codes up all the parametric definitions in (3.5). It is given bydef~T d =

h hi1 , hς(x11 ), . . . , ς(x1i1 ), ~T 1 p ii,
..
.

(3.7)

hik , hς(xk1 ), . . . , ς(xkik ), ~T k p ii i.
Notice that this is not a self-referential definition.
• The structural definition of ~ p is given in Fig. 5. The only thing worth mentioning is that theindex of D j (t j1 , . . . , t ji j ) contains the information about the equation in which D j is defined, thenumber of parameters of D j , and all the terms that instantiate the parameters.

16

Y. FU

def

=

0,

def

=

6 ∗ hς(a), ς(x), ~T p i + 1,

def=

6 ∗ hς(a), ~tς , ~T p i + 2,

def=

6 ∗ h~T p , ~T 0 p i + 3,

def=

6 ∗ hς(c), ~T p i + 4,

~if ϕ then T pdef=

6 ∗ h~ϕς , ~T p i + 5,

~D j (t j1 , . . . , t jn j )pdef

6 ∗ h j, hn j , h~t j1 ς , . . . , ~t jn j ς iii + 6.

~0p~a(x).T p~a(t).T p~T | T 0 p~(c)T p=

Figure 5: Gödel Index of VPC-Term.
case z ofr6 (z)=0 ⇒ 0;
r6 (z)=1 ⇒ Nth(d6 (z)0 , y).ay (x).Su ([x/d6 (z)1 ]d6 (z)2 );r6 (z)=2 ⇒ Nth(d6 (z)0 , y).ay (val(d6 (z)1 )).Su (d6 (z)2 );r6 (z)=3 ⇒ Su (d6 (z)0 ) | Su (d6 (z)1 );r6 (z)=4 ⇒ Nth(d6 (z)0 , y).(ay )Su (d6 (z)1 );r6 (z)=5 ⇒ if val(d6 (z)0 ) then Su (d6 (z)1 );r6 (z)=6 ⇒ e(d6 (z))
end case
Figure 6: Simulator Su (z).
At top level the indices of all VPC-terms are of the form (3.6). One may think of ~T p as the main
program and ~T d as the subroutines necessary when executing the program.
i, 
Our universal process {Ud }i∈N, ∈N ∗ ,d<  for VPC is defined as follows:
Udi,a1 ...akdef=d(z).(h)(Pu (z) | h(z).(e)(Du ((z)0 , z1,0 ) | Su (z1,1 )))(3.8)

1 ...akfor all i, a1 , . . . , ak , d such that d < {a1 , . . . , ak }. The process Udi,a1 ...ak is similar to Ii,adefineddin (3.2). We leave out the definition of the parser Pu (z) since it is similar to Pi (z) and it is purely
arithmetical. The process Du ((z)0 , z1,0 ) is an instantiation of the parametric definition Du (x, y) givenby the following equation:

Du (x, y) = !e(v).if 1 ≤ (v)0 ≤ x then let w = (v)0 − 1
in let u = yw,0 in Su ([v1,1,u−1 /yw,1,u−1 ] . . . [v1,1,0 /yw,1,0 ]yw,1,u ).
The first parameter of Du (x, y) indicates the number of the mutually dependent equations. The
second parameter is the Gödel index of these parametric definitions that takes the form of (3.7). The
definition Du (x, y) is essentially the interpretation of ~T d . It is able to simulate all the parametricdefinitions that are encoded in y. Again this is possible because the simulation is on-the-fly. The
simulator Su (z) in (3.8) is defined in Fig. 6. The recursive functions r6 , d6 are similar to those of
r7 , d7 respectively. In case r6 (z) = 6 the subroutine Du ((z)0 , z1,0 ) is invoked with the parameter d6 (z).
By an argument similar to the one given in the proof of Theorem 3.1, one can convince oneselfof the validity of the following result.
Theorem 3.2. VPC ∈ VPC.

THE UNIVERSAL PROCESS

17

4. Application
The existence of a universal process can be seen as an expressiveness criterion. There cannot be
any universal process for CCS [Mil89] or the pure process-passing calculus [San92, Tho95] sinceneither is complete [Fu16]. But once an interaction model does admit some sort of universal process,a whole range of new applications are available. In this section we sketch three of them.
4.1. Process Passing as Value Passing. The most valuable contribution of a universal process isthat it allows a receiving process to interpret a number as a process. This is a very useful property
when applying VPC to tackle practical programming issues. But is it necessary to pass a processfrom one location to another? If the process that appears in the target environment is completely thesame as the one sent from the source environment, a positive answer to the question can hardly beconvincing. What is useful in practice is that the source process sends an abstraction parameterized
over names, and the process on the receiving end instantiates the parameters of the abstraction
by its local names. This way of introducing the higher order feature in the π-calculus is adopted
in [San92, San93]. We follow the same approach to extend VPC. Our higher order VPC has thefollowing grammar:
T := . . . | X(a1 , . . . , a j ) | A(a1 , . . . , a j ) | a(X:hi, ji).T | a(A:hi, ji).T,
where only the higher order terms are indicated. An abstraction A is a term whose global names are
abstracted away. A process with j global names can be turned into an abstraction with j parameters.
If for example T is a term with the global names c1 , . . . , c j then λc1 . . . c j .T is an abstraction. In
the above syntax A : hi, ji indicates that A is an abstraction with i local names and j parameters.
The term a(X:hi, ji).T is a higher order input, in which hi, ji provides the typing information of theabstraction variable X, a(A:hi, ji).T is in higher order output form, X(a1 , . . . , a j ) is an instantiationof the abstraction variable X at a1 , . . . , a j and A(a1 , . . . , a j ) an instantiation of the abstraction A at
a1 , . . . , a j . The instantiation of the abstraction λc1 . . . c j .T at a1 , . . . , a j is syntactically the sameas the term T {a1 /c1 . . . . , a j /c j }. Instantiations must be type correct. Formally the names in thehigher order VPC are typed in the same way as the channels in the higher order π-calculus are
typed [San92, San93]. We ignore the type system in the present light weight treatment. In addition
to the operational semantics of VPC the higher order VPC has the following semantic rules:
a(A)

a(A)

S −→ S 0 T −→ T 0a(A)a(X:hi, ji).T −→ T {A/X}a(A)a(A:hi, ji).T −→ T

τS | T −→ S 0 | T 0

In the higher order input rule A must be of the same type as the variable X.
We can now explain how to simulate the operational semantics of the higher order VPC in thefirst order VPC. Let υ stand for a partial function from the set of abstraction variables to V that is
injective on its finite domain of definition. The notation υ[Z→z] refers to the function that is thesame as υ except that it sends Z onto z. The nontrivial part of the encoding is given below:
i,a ...a~X(a1 , . . . , a j )υ = (d)(d([ς(a1 )/v1 , . . . , ς(a j )/v j ]υ(X)) | Ud 1 j ),~a(X:hi, ji).T υ = a(x).~T υ[X→x] , where x is chosen such that it is not in T,~a(A:hi, ji).T υ = a(~Aυ ).~T υ .
The operation [ς(a1 )/v1 , . . . , ς(a j )/v j ]( ) replaces in υ(X) the indexes v1 , . . . , v j of j global names by
the indexes of a1 , . . . , a j respectively. Notice that since we are dealing with processes containing
neither first order variables nor higher order variables, by the time the on-the-fly interpretation

18

Y. FU

reaches υ(X), it has already been instantiated by a number. Thus v1 , . . . , v j can be safely calculated
from υ(X). The encoding of a higher order VPC process is given by ~P∅ , where ∅ is the nowheredefined function.
The translation of the higher order VPC into the first order VPC is notably different fromthe translation of the higher π into the first order π [San93]. For one thing the simulation of thehigher order communication in VPC is achieved by code transmission, whereas in the π scenario
the simulation is implemented via access control. An advantage of our encoding is that it allows
the ‘user’ to exert tight control over the executions. The user may wish to terminate the simulation
after a certain amount of time, bounded by a time complexity function. This can be implemented byincorporating into the encoding a timer that counts the number of simulation steps.
In practice higher order features are implemented in the same fashion. In real world what isreally passed over in a higher order communication is some code of a routine/process. The code is
not necessarily a number. But the receiver interprets the code in the same way a universal process of
VPC interprets a number. See Section 4.3 for more discussion.
4.2. Communication Security. The completeness of an interaction model means that any encryption/decryption algorithm can be implemented in it and an encrypted text can be passed from one
process to another. By exploiting that fact, a universal process can offer an effective way to enhance
the security of communications. Suppose party A intends to send a piece of programme to party B
through a public channel. There is no way to prevent anyone from eavesdropping on the communication channels. What party A can do is to encrypt the Gödel number of the programme before sending
it to party B. After receiving the number, party B decodes the number to recover the Gödel index. Itthen places the encoded programme in its private environment and puts it into action by invoking auniversal process. Far more complicated scenarios can be designed along this line of thinking.
The point is that the existence of a universal process allows one to implement the well known
security protocols in VPC to enhance communication security. This is a more traditional approachcompared to the one that introduces explicit operators to model security protocols in process calculi [AG99]. In security world one assumes that all channels are insecure. No matter what kindof operators are introduced in a calculus to enhance security of communication, they must be
implemented using cryptographic techniques. In one way or another one resorts to a universal
process.
4.3. Programming Paradigm. If VPC is seen as a machine model, what would be an implementation of a higher order programming language in VPC? If VPC is seen as a programming language,
what kind of programming paradigm does it support? The issue of constructing a higher orderprogramming language on top of a process model has been studied by several research groups, see
the references in [SWU10]. This is not the right place to overview the existing approaches and tools.
What we are going to do is to propose a new programming paradigm that makes essential use ofuniversal processes. To explain our idea we introduce a new process model referred to as PL. This isessentially the same as VPC. But instead of sending and receiving numbers, a PL process sends andreceives strings. The reason for a string-passing process calculus is that it provides the right level ofabstraction to study programming theory in process algebra. A piece of program is nothing but astring, which can be parsed, type checked and executed.
Let Σ be a finite set of symbols and Σ∗ be the set of finite strings over Σ. We will write % for astring variable and ` for a string term constructed from strings, string variables and string operations.
We write ψ for a boolean formula about strings. For simplicity we see a symbol as a string of lengthTHE UNIVERSAL PROCESS

19

one. We choose a set of basic string operations on Σ∗ and a set of basic logic operations on Σ∗ . We
obviously need the head, tail and length operations, as well as the binary prefix relation among others.
The particular choice of the operations is not our concern.
The set of the PL-terms is defined by the following BNF:
T:= 0 | a(%).T | a(`).T | T | T 0 | (c)T | if ψ then T | D(`1 , . . . , `k ).

The operational semantics of PL is obtained from the labeled transition system of VPC by substituting
strings for numbers. The model PL is easily seen to be complete. In fact there is clearly an effective
bijection between Σ∗ and N. Using this bijection it ought to be easy to construct two subbisimilarities
to support the claim that PL v VPC and VPC v PL. We assume that Σ contains the proper subset
ΣN = {0, succ, +, ×}, which makes the definition of the length function possible. The calculus PLN
defined in terms of the symbol set ΣN is as expressive as VPC. We may think of PLN as a machinemodel on which PL is implemented, by which we mean that there is an interpreter of PL in PLN .
Now the general framework has been set up, let’s explain how programming languages can be
implemented in our model. Suppose L is a concurrent, typed programming language, which could be
as sophisticated as a full-fledged programming language or as simple as the concurrent language
studied in [Mil89]. The definition of L is given by a parser {Pc }c∈N . Let Pr be an L program. Thenιc(Pr) | Pc −→ L
for some L. The process indicates acceptance if Pr is a well defined L program, it refuses if Pri, violates the L grammar. The implementation of L is given by an executor {Ec }i∈N, ∈N ∗ ,c< , which isfeasible by the technique developed in this paper. For a legitimate L program Pr of the right type one
must have thati,  ι
c(Pr) | Ec −→ I
for some I that implements Pr in PL. This oversimplified account should be enough to give thereader a taste of our methodology.
Different programming paradigms are supported by different process models. If one intends
to study the object oriented features, one uses the π-calculus. Since π is also complete [Fu16],
everything carried out in this paper can be repeated for π. It should not be difficult to internalize,
as it were, Walker’s meta translation of an object oriented language [Wal91, Wal95] in the fashion
advocated here. What we get is an implementation, rather than a translation, of the object oriented
language in π.
5. Recursion Theory in VPC
In this section we explain how to do recursion theory in VPC by taking a look at VPC version of the
S-m-n Theorem. The challenge here is actually how to formulate it correctly. We know from therecursion theory that S-m-n Theorem is about partial evaluation. There is an effective way to transfer
the index of a (k0 +k1 )-ary effective function f(x1 , . . . , xk0 , y1 , . . . , yk1 ) and the inputs i1 , . . . , ik0 to theindex of the k1 -ary effective function f(i1 , . . . , ik0 , y1 , . . . , yk1 ). If we are ever to have a recursion
theory of VPC processes, we must start by answering the question of what the right VPC counterpartof a recursive function is. It is not hard to see that the most natural generalization of a recursivefunction is a parametric definition of the formD(z1 , . . . , zk ) = T.

(5.1)

20

Y. FU

For numbers i1 , . . . , i j , where j ≤ k, we will write D(i1 , . . . , i j , z j+1 , . . . , zk ) for the (k− j)-ary parametric definition D0 (z j+1 , . . . , zk ) given by
D0 (z j+1 , . . . , zk ) = T {i1 /z1 , . . . , i j /z j }.
Suppose i is the number of local names of T and  is the list of the global names in T . We say thatthe D(z1 , . . . , zk ) defined in (5.1) is a k-ary parametric definition of type [i, ]. Two k-ary parametricdefinitions, say D0 (z1 , . . . , zk ) and D1 (z1 , . . . , zk ), are equal if for all numbers i1 , . . . , ik , one has
D0 (i1 , . . . , ik ) =VPC D1 (i1 , . . . , ik ).
By recycling the encoding in Section 3.1 we can Gödelize the set of the k-ary parametricdefinitions of type [i, ]. Our technique to derive a universal process, as developed in Section 3,[i, ][k]helps define a universal process Uz(z1 , . . . , zk ) for the set of the k-ary parametric definitions[i, ][k]of type [i, ]. Here the word ‘process’ is not very precise since Uz(z1 , . . . , zk ) is a parametric[i, ][k]definition rather than a process. The parameter z is made an index, suggesting that Uz(z1 , . . . , zk )should be thought of as the z-th k-ary parametric definition of type [i, ]. The defining property of[i, ][k]Uz(z1 , . . . , zk ) requires that for each number j, say the index of D(z1 , . . . , zk ), the equality[i, ][k]Uj(z1 , . . . , zk ) =VPC D(z1 , . . . , zk )holds. Now we can state the S-m-n Theorem.
Theorem 5.1. Suppose k0 , k1 are natural numbers. There is a total (k0 +1)-ary recursive function
skk01 (z, x1 , . . . , xk0 ) such that for all numbers j, i1 , . . . , ik0 the following equality holds:[i, ][k0 +k1 ]Uj[i, ][k1 ](i1 , . . . , ik0 , y1 , . . . , yk1 ) =VPC U k0

sk ( j,i1 ,...,ik0 )(y1 , . . . , yk1 ).

1

Proof. The proof follows the standard argument. Given the index of a (k0 +k1 )-ary parametricdefinition D00 (x1 , . . . , xk0 , y1 , . . . , yk1 ) of type [i, ], one can effectively construct the k1 -ary parametricdefinition D00 (i1 , . . . , ik0 , y1 , . . . , yk1 ) of the same type, from which we get its Gödel index effectively.
This defines a total recursive function.
The S-m-n Theorem helps import results in recursion theory to process theory. The famous Rice
Theorem [Rog87] is one such result.
Theorem 5.2. Suppose B is a set of k-ary parametric definitions that satisfies the following:(1) B is not empty;(2) there is some k-ary parametric definition that is not in B;(3) B is closed under the absolute equality.
[i, ][k]Then the set { j | U j(x1 , . . . , xk ) ∈ B for some [i, ]} is undecidable.

Proof. Without loss of generality, suppose Ω < B. By condition (1) the set B contains some k-ary
parametric definition D(x1 , . . . , xk ). Let W contain the number hi1 , . . . , ik i if the hi1 , . . . , ik i-th k-ary
recursive function is definable at i1 , . . . , ik . It is well known that W is recursive enumerable but notdecidable. Let the (k+1)-ary parametric definition D0 (z, x1 , . . . , xk ) be defined by
D0 (z, x1 , . . . , xk ) = if z ∈ W then D(x1 , . . . , xk ).
Suppose D0 (z, x1 , . . . , xk ) is of type [i, ]. Then some number j exists such that[i, ][k+1]Uj(z, x1 , . . . , xk ) =VPC D0 (z, x1 , . . . , xk ).

According to Theorem 5.1 some binary total recursive function s exists such that[i, ][k][i, ][k+1]Us( j,z) (x1 , . . . , xk ) =VPC U j(z, x1 , . . . , xk ).

THE UNIVERSAL PROCESS

21

Using (3) it is clear that k ∈ W if and only if D0 (k, x1 , . . . , xk ) =VPC D(x1 , . . . , xk ) if and only if[i, ][k]Us( j,k) (x1 , . . . , xk ) ∈ B. So B cannot be decidable.
There is nothing new about the above proof. But at least it demonstrates that the type constraint[i, ] of U [i, ][k] is not much of a restriction.
A simple consequence of the Rice Theorem is about the unobservable processes.
Corollary 5.3. The set of the unobservable processes is undecidable.

6. Future Work
The idea of designing universal processes was discussed in [AMS97] in the framework of CCS. Dueto the limitation of the model, a universal process for CCS is static in the sense that it must preload
the Gödel number of the CCS process to be simulated since it can never dynamically input any
number. In order to simulate the branching structure of a process, the universal process for CCS must
introduce divergence. A recent work is reported in [BLT11], where the authors studied universal
Reactive Turing Machines. A universal Reactive Turing Machine either introduces divergence, orplaces restriction on the maximum branching degree of the Reactive Turing Machine being simulated,both divergence and branching degree being of semantic nature. A universal machine for Reactive
Turing Machines is also static in the above sense since the transmission of the description of amachine, which is a string of symbols, to the universal machine should not be interrupted. The
advantage of our universal process is that it is dynamic and does not impose any semantic constraints
on any processes to be simulated.
We have chosen to study universal processes of VPC since natural numbers are familiar andthere is a handy decidable Presburger theory. The model introduced in Section 4.3 is built on anothervalue domain. To achieve completeness very little is required from value domain. Completeness has
more to do with the communication mechanism of a model than with the value domain of the model.
The constructions of the universal processes in other complete models might look quite different. In
π-calculus for example the numbers can be coded up using the following inductively defined nameindexed functions:~0a = a(c).c(b).c(e).ee,~i+1a = a(c).c(b).c(e).~ib .
It is more or less a formality to apply our approach to generate a universal process of π.
For a complete model the existence of universal process depends on the operators of the model.
Since interpretation is done on-the-fly, problem may arise if an operator is not congruent over theabsolute equality. The best counter example is given by the unguarded choice. Upon receiving theGödel number k for P0 + P00 , an interpreter I is expected to generate I(k0 ) + I(k00 ), where k0 codes
up P0 and k00 codes up P00 . But this would be disastrous because I(k0 ) would normally engage insome internal actions before the real simulation of P happens. In other words, it can preempt the
choice. Guarded choice would not have this problem.
Is there a reasonable (complete) model that does not have any universal process? How strong
is it to formulate a thesis postulating that all complete models have universal processes? This is an
important issue to be studied.
The idea of universal process can be further exploited. Two important directions are outlined
below.

22

Y. FU(1) At the theoretical level, it is interesting to see how recursion theory [Rog87, Soa87] defined
in VPC can help develop an interactability theory of the model. Interactability theory aims tostudy definability of interactive behaviours, rather than computational behaviours, in interactivemodels.
(2) At the programming level, it is worth the effort to study programming theory in a systematicway. More generally we can look at the class of process calculi with universal processes. These
are models well equipped to model programming features. The significance of these models toprogramming theory is yet to be investigated.
Is it possible for a universal process to be a single process rather than a family of processes? A
drastic approach to address the issue is to introduce a bijective naming function ν( ) : N → N that a
VPC process may make use of. The function ν( ) gives an enumeration ν0 , ν1 , . . . of the names. It canbe extended to a function from T to the set {νt | t ∈ T} of name expressions. Now the grammar of
VPCν can be defined by the following BNF:
T:= 0 | νt (x).T | νt (t).T | T | T | (νi )T | if ψ then T | D(t1 , . . . , tk ).

An example of a VPCν process isν0 (x).ν1 (y).if x = 2y then ν x (y).
It is clear from this example that VPCν admits mobile computing to a certain degree. Notice thatthe match operator [νt =νt0 ]T is definable in VPCν . The new model lacks the power, and the trouble
as well, introduced by relocating local names. The virtue of VPCν is that it has a single universal
process Uc that is capable of dealing with indices of all VPCν processes. This is rendered possibleby the naming function which produces a canonical indexing for all the names whatsoever. Further
study on VPCν is necessary before we can say more about its theoretical and practical relevance toprocess theory.
Acknowledgement
This work has been supported by NSFC (61472239, PACE 61261130589). Xiaojuan Cai’s idea about
the on-the-fly simulations has been very instructive to this work. Sandy Harris and Huan Long havehelped in improving the quality of this paper.
References[AG99]

M. Abadi and A. Gordon. A calculus for cryptographic protocols: The spi calculus. Informaiton and Computation, 148(1):1–70, 1999.
[AMS97] H. Andersen, S. Mørk, and M. Sørensen. A universal reactive machine. In Proc. CONCUR 1997, volume 1243
of Lecture Notes in Computer Science, pages 89–103, 1997.
[BGZ03] N. Busi, M. Gabbrielli, and G. Zavattaro. Replication vs recursive definitions in channel based calculi. In Proc.
ICALP’03, volume 2719 of Lecture Notes in Computer Science, pages 133–144, 2003.
[BGZ04] N. Busi, M. Gabbrielli, and G. Zavattaro. Comparing recursion, replication and iteration in process calculi. In
Proc. ICALP’04, volume 3142 of Lecture Notes in Computer Science, pages 307–319, 2004.
[BLT11] J. Baeten, B. Luttik, and P. Tilburg. Reactive turing machine. In Proc. FCT 2011, volume 6914 of Lecture Notes
in Computer Science, pages 348–359, 2011.
[End01] J. Enderton. A Mathematical Introduction to Logic. Harcourt/Academic Press, 2001.
[FL10]
Y. Fu and H. Lu. On the expressiveness of interaction. Theoretical Computer Science, 411:1387–1451, 2010.
[Fu13]
Y. Fu. The value-passing calculus. In Theories of Programming and Formal Methods, Lecture Notes in
Computer Science 8051, pages 166–195, 2013.
[Fu15]
Y. Fu. Nondeterministic structures of computation. Mathematical Structures in Computer Science, 25:1295–
1338, 2015.

THE UNIVERSAL PROCESS

23[Fu16][Gor08]Y. Fu. Theory of interaction. Theoretical Computer Science, 611:1–49, 2016.
D. Gorla. Towards a unified approach to encodability and separation results for process calculi. In CONCUR
2008, Lecture Notes in Computer Science 5201, pages 492–507, 2008.
[GSV04] P. Giambiagi, G. Schneider, and F. Valencia. On the expressiveness of infinite behavior and name scoping inprocess calculi. In FOSSACS 2004, Lecture Notes in Computer Science 2987, pages 226–240, 2004.
[HI93a] M. Hennessy and A. Ingólfsdóttir. Communicating processes with value-passing and assignment. Journal ofFormal Aspects of Computing, 5:432–466, 1993.
[HI93b] M. Hennessy and A. Ingólfsdóttir. A theory of communicating processes with value-passing. Information andComputation, 107:202–236, 1993.
[HL95]
M. Hennessy and H. Lin. Symbolic bisimulations. Theoretical Computer Science, 138:353–369, 1995.
[Hoa85] C. Hoare. Communicating Sequential Processes. Prentice Hall, 1985.
[Mil89] R. Milner. Communication and Concurrency. Prentice Hall, 1989.
[Mon76] J. Monk. Mathematical Logic. Springer-Verlag, New York, 1976.
[MP05] S. Maffeis and I. Phillips. On the computational strength of pure ambient calculi. Theoretical Computer Science,
330:501–551, 2005.
[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.
[MS92] R. Milner and D. Sangiorgi. Barbed bisimulation. In Proc. ICALP’92, volume 623 of Lecture Notes in Computer
Science, pages 685–695, 1992.
[Pal03]
C. Palamidessi. Comparing the expressive power of the synchronous and the asynchronous π-calculus. Mathematical Structures in Computer Science, 13:685–719, 2003.
D. Park. Concurrency and automata on infinite sequences. In Theoretical Computer Science, volume Lecture[Par81]
Notes in Computer Science 104, pages 167–183. Springer, 1981.
[Pos44] Post. Recursively enumerable sets of positive integers and their decision problems. Bulletin of the American
Mathematical Society, 50:284–316, 1944.
[Pre29]
M. Presburger. Über die vollständigkeit eines gewissen systems der arithmetik ganzer zahlen, in welchem die
addition als einzige operation hervortritt. In Warsaw Mathematics Congress, volume 395, pages 92–101, 1929.
[Pri78]L. Priese. On the concept of simulation in asynchronous, concurrent systems. Progress in Cybernatics andSystems Research, 7:85–92, 1978.
[Rog87] H. Rogers. Theory of Recursive Functions and Effective Computability. MIT Press, 1987.
[San92] D. Sangiorgi. Expressing Mobility in Process Algebras: First Order and Higher Order Paradigm. PhD thesis,
Department of Computer Science, University of Edinburgh, 1992.
[San93] D. Sangiorgi. From π-calculus to higher order π-calculus–and back. In Proc. TAPSOFT’93, volume 668 of
Lecture Notes in Computer Science, pages 151–166, 1993.
[Soa87] R. Soare. Recursively Enumerable Sets and Degrees, a study of computable functions and computably generated
sets. Springer, 1987.
[Sta84]
R. Stansifer. Presburger’s article on integer arithmetic: Remarks and translation. Technical report, Technicalreport, Computer Science Department, Cornell University, 1984.
[SWU10] P. Sewell, P. Wojciechowski, and A. Unyapoth. Nomadic pict: Programming languages, communication
infrastructure overlays, and semantics for mobile computation. ACM Tansactions on Programming Languages
and Systems, 32:1–63, 2010.
[Tho95] B. Thomsen. A theory of higher order communicating systems. Information and Computation, 116:38–57,
1995.
[vEB90] P. van Emde Boas. Machine models and simulations. In J. van Leeuwen, editor, Handbook of TheoreticalComputer Science: Algorithm and Complexity, volume A, pages 65–116. Elservier, 1990.
[vGLT09] R. van Glabbeek, B. Luttik, and N. Trčka. Branching bisimilarity with explicit divergence. Fundamenta
Informaticae, 93:371–392, 2009.
[vGW89] R. van Glabbeek and W. Weijland. Branching time and abstraction in bisimulation semantics. In Information
Processing’89, pages 613–618. North-Holland, 1989.
[Wal91] D. Walker. π-calculus semantics for object-oriented programming languages. In Proc. TACS ’91, volume 526
of Lecture Notes in Computer Science, pages 532–547, 1991.
[Wal95] D. Walker. Objects in the π-calculus. Information and Computation, 116:253–271, 1995.

This work is licensed under the Creative Commons Attribution-NoDerivs License. To view a copyof this license, visit http://creativecommons.org/licenses/by-nd/4.0/ or send a letter toCreative Commons, PO Box 1866, Mountain View, CA 9404, USA