Under consideration for publication in Math. Struct. in Comp. Science

Nondeterministic Structure of Computation
Yuxi Fu†

BASICS, Department of Computer Science
Shanghai Jiaotong University, Shanghai 200240
MOE-MS Key Laboratory for Intelligent Computing and Intelligent Systems
Received 8 June 2012; Revised 22 December 2013

Divergence and nondeterminism play a fundamental role in the theory of computation.
Their combined effect on computational equality deserves further study. By looking at
the issue from the point of view of both computation and interaction, one is led to a
canonical equality for nondeterministic computation, revealing its rich algebraic
structure. The structure is studied in three ways. Firstly a complete equational system
for finite state nondeterministic computation is constructed. The challenge with such asystem is to find an equational alternative to the fixpoint induction à la Milner. A
negative result, the non-existence of a finite equational system for the canonical equalityof nondeterministic computation, is established to support our approach. Secondly
infinite state nondeterministic computation is investigated in the light of definability. It
is shown that every recursively enumerable set is generated by an unobservable process.
Thirdly it is proved that, as far as computation is concerned, the effect produced jointly
by divergence and nondeterminism is model independent for a large class of processmodels. In all the studies C-graphs, which are themselves interesting, are used as
abstract representations of the computational objects.

1. Introduction
Our conception of computation is independent of individual mental power since theconcept is supported by physical realizability. A Turing machine, or its physical implementation, with an input written on its storage tape, constitutes a computational object.
An execution of the computational object, driven by physical laws, either terminates ina final computational object, which is the machine with the result value placed on its
storage tape, or does not terminate. In a more abstract model, say the λ-calculus (Barendregt 1984), there is no distinction between machine and datum. Computational objects
can take many different shapes and forms. The essence of a computational object is thatit can be physically implemented and can be executed by resorting to physical laws. The† fu-yx@cs.sjtu.edu.cn

Nondeterministic Structure of Computation

2

two kinds of computational objects we have just mentioned are dramatically different.
From the point of a user, a terminating computation, or execution, provides a result,whereas a divergent, or nonterminating, computation can never do him/her any good. In
the physical world, a divergent computation is bound to go bankrupt, at least theoretically, before it exhausts all the energy of the universe. A model theoretical treatment tocomputation must distinguish these two kinds of computational objects from the outset.
Modern computing environments feature interactions. What comes with interaction
is nondeterminism. In such an environment a computational object may be capable ofproducing a result, and at the same time it also has the potential to diverge. The choice
between the two actions is nondeterministic. This computational object differs from aterminating computational object and a divergent computational object in both thehuman world and the physical world. In fact the situation is far more complicated.
Nondeterminism and divergence can be combined in a very complex way. It is not at all
clear if anything can be said about these computational objects.
This paper sets out to study the nondeterministic computational objects. Our objective
is to answer the following questions:— What is the right notion of equality for the nondeterministic computational objects? A
reasonable answer to the question is the starting point for subsequent investigations.
— What are the structures of the nondeterministic computational objects? More specifically are there any characterizations of the equivalence classes of these objects?
— What are the nondeterministic computational objects defined in a computation orinteraction model? Do they differ from one model to another?
We document in this paper the results we have obtained by looking into these problems.
Our contributions are summarized as follows:— We will present a coherent account of the following interrelated concepts: ChurchTuring thesis, bisimulation, computation, interaction, divergence, nondeterminism,computational equality, observational equivalence, Turing completeness. The equality
for the nondeterministic computational objects will emerge from the uniform account.
— We will construct a complete equational system for the equality we introduced on
finite state computational objects. The system contains a few axiom schemata. We
will prove a negative result saying that there does not exist any finite axiom system
for the finite state computational objects.
— We will study infinite state computations from the point of view of definability. A
general definability result will be established.
— We will show that the nondeterministic structure of computation is model independent for a general class of models.
The rest of the paper is organized as follows. Section 2 discusses equality properties
for deterministic computation. Section 3 extends these properties to take into account ofinteraction. Section 4 characterizes finite state computational objects. Section 5 investigates infinite state computational objects. Section 6 establishes the model independence
property of the nondeterministic computational objects. Section 7 points out some further research issues.

Mathematical Structures in Computer Science3

2. Church-Turing Thesis and Bisimulation
Our understanding of effective calculability was greatly enhanced in the 1930’s by thestudy of computation models (Kleene 1981). Church’s simple and elegant model, the wellknown λ-calculus (Church 1936; Cardone and Hindley 2009), turned out to be extremely
expressive from the programming point of view. Gödel’s recursive functions (Gödel 1931;
Davis 1965), known as primitive recursive functions after (Kleene 1936a), evolved to
Herbrand-Gödel’s general recursive functions (see Gödel’s 1934 lecture notes reprinted
in (Davis 1965)), although at the time Gödel himself wasn’t very sure that general recursion captures all possible effective calculability. The year 1936 was when the foundationof computation theory began to take shape. Kleene (Kleene 1936a) provided a characterization of general recursive functions in terms of primitive recursive functions andthe least number operator (the µ-operator). Church (Church 1936) and Kleene (Kleene
1936b) showed that the general recursive functions are in fact the same as the λ-definable
functions. Turing, having worked independently on his machine model (Turing 1936;
Turing 1937b) and having learnt about the work on λ-definability and general recursion,
gave a proof of the equivalence between Turing computability and λ-definability (Turing
1937a). These equivalence results led researchers, in particular Gödel, to believe in the
Church-Turing Thesis (called Church Thesis in (Kleene 1952)). Later it was pointed out
by Kleene (Kleene 1938) that the thesis also covers the situation of partially definedrecursion. Turing remarked in (Turing 1937a) that the λ-calculus is more convenient.
What he couldn’t say at the time is that, owing to this simplicity, the λ-calculus plays afoundational role among (functional) programming languages (Abramsky 1988). Gödelwas reported as saying that Turing machines offer the most convincing formalization of
mechanical procedures (Davis 1965). It came as no surprise that the physical feasibilityof Turing machines is exploited in the influential von Neumann architecture. After the
discoveries of the 1930’s, models of computation with different emphases were proposed
and proved equivalent to the earlier models of Gödel, Church, Kleene and Turing. Post
Systems (Post 1943) and Markov Algorithms (Markov 1960) can be seen as language
models, while counter machines (like Minsky Machines (Minsky 1967) and the Unlimited Register Machines of Shepherdson and Sturgis (Shepherdson and Sturgis 1965)) andRandom Access Machines (Cook and Reckhow 1973) are members of the class of registermachines.
Our understanding of effective calculability can be further enhanced by revealing thehidden depth of the Church-Turing Thesis. The thesis was originally formulated in termsof computable functions. It is normally stated as follows:
CTT-I. The set of functions definable in a model of computation is precisely the set of computable functions.

According to the thesis, the computable functions are precisely those definable by thepartial recursive functions (Rogers 1987). The equivalence proofs since the 1930’s that
support the Church-Turing Thesis reveal a lot more than CTT-I. In all cases there isactually an effective translation from one computation model to another that preserves
and reflects computations. To describe the general phenomenon in a model independent
way, we need to be a bit more formal about computation models and translations be-Nondeterministic Structure of Computation

4

tween them. We assume that every model is a pair hCA , →A i, where CA is the set ofcomputational objects, or configurations, and →A , whose subscript will be omitted, isthe one step computation relation. Let C be the class of all computation models, ranged
over by A, B. The reflexive and transitive closure of → will be denoted by →∗ . Now
suppose T is a translation from A to B and M → M 0 is a one step computation in A.
The preservation property of T requires that T (M ) → N1 → N2 → . . . → Nk , for somecomputational objects N1 , . . . , Nk of B, such that the sequence of transitions from T (M )simulates M → M 0 . One difficulty in proving the correctness of T is in showing that
Nk is essentially the same as T (M 0 ). This requires the introduction of an equivalenceon the computational objects of B, which would complicate the issue from the outset.
An elegant way to bypass this problem is to think of T as a recursive relation rather
than as a recursive function. To make the following account simpler, we abuse notation
by identifying CA with the set of the Gödel indices of the computational objects of A.
A translation from A to B can then be regarded as a binary relation on the set N ofnatural numbers. For every computational object M of A, the interpreter should be able
to generate effectively the interpretations of M . Suppose N is one interpretation of M
and N → N 0 . The correctness of the interpreter also requires that it should be capableof effectively finding a computational object M 0 in A such that M →∗ M 0 and N 0 is
an interpretation of M 0 . This is usually called reflection property. These remarks leadto Definition 1 introduced below. Henceforth the set N is ranged over by i, j, k. Suppose S is a binary relation. The infix notation xSy stands for the membership predicate(x, y) ∈ S, and S −1 denotes the reverse relation {(y, x) | xSy}. The domain d(S) of
S is {x | ∃y.xSy} and the range r(S) of S is {y | ∃x.xSy}. The relation S is total if∀x.∃y.xSy.
Definition 1. A relation S ⊆ N × N is recursive if the following are valid:
1 Both d(S) and r(S) are recursive.
2 There are (partial) recursive functions s+ , s− : N → N, called encoding and decoding
functions respectively, such that d(s+ ) = d(S) and d(s− ) = r(S).
3 ∀x ∈ d(S).s− (s+ (x)) = x.
By definition the composition of two recursive relations is a recursive relation. To appreciate the above definition, notice that the condition (3) of the above definition rules out
nonsensical translations like the one translating every divergent Turing machine configuration to (λx.xx)(λx.xx) and every terminating Turing machine configuration to λx.x.
Studies in complexity theory and programming activities in the real world have led us tobelieve that the translation overheads, as well as the simulation costs, between computation models are actually polynomially bounded (van Emde Boas 1990; Wegener 2005).
In this paper we ignore this quantitative aspect of the Church-Turing Thesis.
We are now in a position to define in a model independent manner translations from one
computation model to another, formalizing a number of proposals summarized in (vanEmde Boas 1990).
Definition 2. Suppose A, B are computation models. A relation T from CA to CB is aneffective reduction of A to B if the following statements are valid:Mathematical Structures in Computer Science5

T is total.
T is recursive.
If M T N , then ∃M 0 .M →∗ M 0 T N 0 whenever N → N 0 , and ∃N 0 .N →∗ N 0 T −1 M 0
whenever M → M 0 .
4 If M T N , then there is an infinite sequence of computation starting from M if andonly if there is an infinite sequence of computation starting from N .

1
2
3

We write A ≤e B if there is an effective reduction from A to B.
As we have alluded to in the above, Definition 2 makes little sense without condition 2.
Condition (3) is the weak bisimulation property (Park 1981; Milner 1989a) well-known inlogic and process theory (Sangiorgi 2009). We will come back to this point later. Conditions (2) and (3) are the fundamental qualitative properties of T . Condition (4), usuallyreferred to as the termination preservation condition, says that a computational objectof A is undefined if and only if its interpretation in B is undefined. There are other ways
to deal with undefinedness. But the identification of undefinedness with nontermination,or divergence as it is normally called, is the simplest model independent treatment for
undefinedness. It is important to realize that if Definition 2 is strengthened by adding thequantitative condition saying that the length of a simulating sequence is polynomial on
the length of the computation sequence being simulated, then condition (4) is a corollaryof condition (3) if both A and B are deterministic. In a quantitative approach terminating computations must be interpreted by terminating computations, and consequently
divergent computations must be interpreted by divergent computations. Termination
preservation is subordinate to condition (3) in a quantitative framework.
The equivalence proofs that substantiate CTT-I suggest that every one of the wellknown (deterministic) computation models can be regarded as an initial model. From thepoint of view of this paper it is most convenient to take a Counter Machine Model as theinitial model R. A CM consists of a finite number of registers r1 , . . . , rk0 and a program, thelatter being a finite sequence of instructions L1 , . . . , Lk with the line numbers 1, 2, . . . , krespectively. An instruction is in one of three forms: Succ(rj ) increments the number in
rj by one before moving to the next instruction; DecJump(rj , s) decreases the number
in rj by one if it is not zero, or it jumps to the s-th instruction; and End stops theexecution of the program. Without loss of generality we assume that an instruction ofa program is End if and only if it is the last instruction of the program. The set CRof the computational objects of R is a CM configuration hn1 , . . . , nk0 ; ii, where nj , forj ∈ {1, . . . , k 0 }, is the current number stored in the j-th register and i is the locationof the current instruction. The one step computation hn1 , . . . , nk0 ; ii → hn01 , . . . , n0k0 ; i0 i
indicates the change of configuration after the execution of the current instruction.
We can now reformulate CTT-I in terms of the effective reduction.
CTT-II. ∀A∈C. R ≤e A.

Conditions (3,4) of Definition 2 are formulated for deterministic computation. This is
not really a restriction for CTT-II since R is deterministic. We shall see in the next
section how ≤e can be strengthened so that it applies to every pair of deterministic/nondeterministic computation models.

Nondeterministic Structure of Computation

6

3. Church-Turing Thesis and Process Equality
Let’s now turn to nondeterministic computations. In a semantic setting, nondeterminism
is about state change. Suppose M is a configuration of a nondeterministic Turing machine
and that M may in one step evolve nondeterministically to two distinct configurations
M 0 , M 00 . If M 0 and M 00 always lead to final configurations with the same numbers in the
output tapes, one may think of these two configurations as semantically equivalent. In
this case the nondeterminism is fake. True nondeterminism comes into the picture when
M 0 , M 00 are not semantically equivalent. This is the situation in which it is possible for
M 0 for instance to reach a final configuration with a number on the output tape whereas
M 00 can never reach a final configuration with the same output number.
Nondeterminism is not a concept about effectiveness. One can never argue in favourof it from the point of view of effective calculability. Nondeterminism is inevitable if
computations are defined in an interactive framework. In the broader picture of modern
computing (distributed and mobile computing), everything is about interaction (Milner
1993) and computation is a special form of interaction (Milner 1992; Cai and Fu 2011).
Milner pioneered the study of interaction models with his work on the well-known process
calculus CCS (Milner 1989a). A major contribution of the study of process calculi isthe theory of observational equivalence. Before explaining the relationship between theobservational theory and the Church-Turing Thesis, we need to introduce the CCS model.
Crucial to the definition of CCS is the notion of (channel) name. We summarize therelevant terminology concerning names and name variables below.
— The countable set N of names is ranged over by a, b, c, d, e, f, g, h.
— The set N of co-names is {a | a ∈ N }.
— The set of actions A = N ∪N ∪{τ } is ranged over by λ and its decorated versions. The
notation τ stands for an internal action. It is different from any name and co-name.
— The set Nv of name variables is ranged over by u, v, w, x, y, z.
— The union N ∪ Nv is ranged over by l, m, n, o, p, q.
— The set L = A ∪ Nv ∪ {x | x ∈ Nv } is ranged over by `.
A finite sequence of names c1 , . . . , ck for example is sometimes abbreviated to ec.
The set of CCS terms is generated by the following grammar:
T:= S | T | T 0 | (c)T | D(n1 , . . . , nk ),S:= 0 | `.T | S + S 0 .

In `.T we say that ` is a prefix of T . The term `1 .T1 +`2 .T2 +. . .+`n .Tn will be called a ΣPterm or a choice term. We will write 1≤i≤n `i .Ti for `1 .T1 + `2 .T2 + . . . + `n .Tn . We haveomitted the brackets in `1 .T1 + `2 .T2 + . . . + `n .Tn since the operator ‘+’ is commutativePand associative. The notation i∈I `i .Ti will also be used, where the indexing set I isP
finite. If the indexing set I is empty, i∈I `i .Ti is understood as 0. A trailing 0 will often
be omitted. The operator ‘|’ composes two terms into one, allowing the components
to interact. In the localization term (c)T the name c is bound. For simplicity we will
abbreviate (c1 ) . . . (ck )T to (c1 . . . ck )T . We avail ourselves of the α-conversion, whichsays that a local name in a term can be renamed to a fresh name without changing
the syntax of the term. The α-conversion is used whenever it is necessary to preventMathematical Structures in Computer Science7

name capture. The term D(n1 , . . . , nk ) is the instantiation of a parametric definition
D(x1 , . . . , xk ) at n1 , . . . , nk . A k-ary parametric definition D(x1 , . . . , xk ) is given by anequationD(x1 , . . . , xk ) = T(1)such that the set of the name variables appearing in T is a subset of {x1 , . . . , xk }.
The instantiation of D(x1 , . . . , xk ) at n1 , . . . , nk is T {n1 /x1 , . . . , nk /xk }. We will write
A, B, C, D for processes defined by parametric definition. In (1) the parameters x1 , . . . , xk
are bound. A name variable is free if it is not bound. A CCS process is a CCS termthat does not contain any free variables. The set of processes will be ranged over by
L, M, N, O, P, Q.
The labeled transition semantics of CCS is generated by the following rules.
ActionλλS1 −→ S10λS2 −→ S20λλ

S1 + S2 −→ S10

λ.T −→ T

S1 + S2 −→ S20

Composition
λa

T0 −→ T00a

T0 −→ T00

T1 −→ T10
τ

T0 | T1 −→ T00 | T10

λT0 | T1 −→ T00 | T1λa

T1 −→ T10a

T0 −→ T00

T1 −→ T10
τ

T0 | T1 −→ T00 | T10

λT0 | T1 −→ T0 | T10
Localization
λT −→ T 0

c does not appear in λ.

λ(c)T −→ (c)T 0
Recursion
λT {n1 /x1 , . . . , nk /xk } −→ T 0
λD(n1 , . . . , nk ) −→ T 0

D(x1 , . . . , xk ) = T.

In the recursion rule T {n1 /x1 , . . . , nk /xk } is the term obtained from T by substituting
n1 , . . . , nk for x1 , . . . , xk simultaneously.
a
If T −→ T1 , meaning that T can evolve into T1 by performing the external actionaa, and T 0 −→ T10 , meaning that T 0 can turn into T10 by performing the external coaction a, then T and T 0 may interact at the channel a, resulting in an internal actionττ
T 0 | T −→ T10 | T1 . The relation −→ is in fact the one-step computation relation. Forττ
example τ.a −→ a is a deterministic computation step, whereas τ.a + τ.b −→ a is aτnondeterministic computation step. The reflexive and transitive closure of −→ is denotedλλby =⇒. The composition =⇒−→=⇒ is abbreviated to =⇒.
Among the several variants of CCS used by Milner (Milner 1989a), the one with the
fixpoint operator is relevant to the present work. The grammar of this model is given byT:= X | S | T | T 0 | (c)T | µX.T,

S:= 0 | λ.T | S + S 0 .

Nondeterministic Structure of Computation

8

In the fixpoint term µX.T the free term variable X in T gets bound in µX.T . Noticethat in this variant, henceforth denoted by CCSµ , there is no need for name variables.
The semantics of the fixpoint term is defined by the following ruleλT {µX.T /X} −→ T 0
λµX.T −→ T 0
In CCS the fixpoint term µX.T can be simply defined by D = T {D/X}. So we can use
the fixpoint notation in CCS. In (Fu and Lu 2010) it is shown that CCSµ is strictly lessexpressive than CCS. In fact CCS is Turing complete (Busi, Gabbrielli and Zavattaro
2003; Busi, Gabbrielli and Zavattaro 2004) whereas CCSµ is not even Turing complete (Fuand Lu 2010). Milner in his book (Milner 1989a) used another variant, the one withdynamic binding, that is equivalent to CCS (Giambiagi, Schneider and Valencia2004).
We shall use CCSµ to characterize the finite state computation, and use CCS to study
the infinite state computation. A more restricted recursion is given by the replication
operator. A replication term is of the form !λ.T , whose semantics is given by the ruleλ!λ.T −→ T | !λ.T
Clearly !λ.T can be defined by µX.λ.(T | X).
Had the development of process theory paralleled that of computation theory, one
would have seen the introduction of ‘reduction’ between process calculi at an early stage.
This is not what happened in reality. The truth is that the equivalence relation, a relatively simple concept in computation theory, becomes the most intriguing issue in process
theory (Milner 1980). And it has remained one of the major concerns throughout thedevelopment of process theory (Milner 1989a; Hennessy 1988; Baeten and Weijland 1990;
Sangiorgi and Walker 2001). This is understandable since one would not know how todefine a reduction between two process calculi if one did not know how to define an equivalence on one process calculus. After all an equivalence can be seen as a reduction fromone process calculus to itself (Fu 2012). For a long time Milner’s weak bisimilarity (Milner
1989a) was the main tool to identify the interactive behaviors of processes (Milner 1993).
The relation was originally defined in terms of both internal and external actions. Milner
and Sangiorgi (Milner and Sangiorgi 1992) pointed out later that the bisimulation property for the external actions is a derivable property. In other words, bisimulation is about
computation. To guarantee that a bisimulation equivalence is observational, it should atleast be closed under interactive environment and preserve the ability to interact. Hencethe next two definitions.
Definition 3. A relation R on processes is extensional if the following statements arevalid: (c)P R (c)Q if P RQ; and (P | P 0 ) R (Q | Q0 ) if P RQ and P 0 RQ0 .
λDefinition 4. A process P is observable, notation P ⇓, if P =⇒−→ for some λ 6= τ . A
process P is unobservable, notation P 6⇓, if ¬(P ⇓). A relation R on processes is equipollent
if (P ⇓) ⇔ (Q⇓) whenever P RQ.
The equipollence is the barbed condition of Milner and Sangiorgi (Milner and Sangiorgi

Mathematical Structures in Computer Science91992). We now define Milner’s weak bisimilarity (Milner 1989a) in the style of barbed
bisimulation.
Definition 5. The Milner equality ≈ is the largest relation R that validates the following
statements:
1
2
3

R is reflexive.
R is extensional and equipollent.
R is a weak bisimulation. In other words the following statements are valid:τ— If M RN −→ N 0 then M =⇒ M 0 RN 0 for some M 0 .
τ— If N R−1 M −→ M 0 then N =⇒ N 0 R−1 M 0 for some N 0 .
The equivalence ≈↓ is the largest reflexive, extensional, equipollent weak bisimulationthat satisfies the termination preservation property:
4

If M RN , then there is an infinite sequence of τ actions starting from M if and only
if there is an infinite sequence of τ actions starting from N .

The resemblance between Definition 2 and Definition 5 deserves comment. The totality
condition of the former turns into the reflexivity condition of the latter. This is because
the former is a relation on two models, while the latter is a relation on one model.
Condition (2) of Definition 2, which is an intensional requirement, becomes condition(2) of Definition 5, which is an observational requirement. The analogy brings out thefollowing criticisms to ≈:1

2

As we have said, weak bisimulation is essentially a property about deterministic computation. It does not really fit in a definition that is supposed to take good care of
the nondeterminism caused by interaction.
The condition (4) of Definition 2 is completely ignored by ≈. This is a deficiency ifprocess calculi are seen to subsume computation models.

One may cast similar doubts on the equivalence ≈↓ .
3

The condition (4) of Definition 2 is formulated for the deterministic computations.
Does it still make sense in the presence of nondeterminism?
A well known example that showcases the problem of ≈ is given by the equality
τ.(a + τ.b) + c ≈ τ.(a + τ.b) + τ.b + c.

The one-step nondeterministic computationττ.(a + τ.b) + τ.b + c −→ b(2)

is simulated by the two-step nondeterministic computationττ

τ.(a + τ.b) + c −→ a + τ.b −→ b.

(3)

The intermediate state a + τ.b is bisimilar to neither τ.(a + τ.b) + c nor b. At state a + τ.b
the environment may well intervene to disrupt the simulation. It is debatable if (3) canreally be seen as a simulation of (2). In computation theory the distinction between deterministic computations and nondeterministic computations is of fundamental importance.
The issue raised by this example should be properly addressed.

Nondeterministic Structure of Computation

10

van Glabbeek and Weijland (van Glabbeek and Weijland 1989) proposed a more discriminating approach to nondeterminism. The branching bisimulations they discovered isbased on the following Computation Lemma (Fu and Lu 2010), called Stuttering Lemmain (van Glabbeek and Weijland 1989).
Lemma 1. Let P be either the weak bisimilarity or the absolute equality to be definedτττlater. If P1 −→ P2 −→ . . . −→ Pn P P1 , then P1 P P2 P . . . P Pn .
τ

τ

τ

τ

The lemma implies that if P1 −→ P2 −→ . . . −→ Pk −→ Pk+1 such that Pk+1 is not
equivalent to Pk , then Pk+1 is not equivalent to Pi for any i < k. The philosophy ofthe branching bisimulation of van Glabbeek and Weijland (van Glabbeek and Weijland1989) is that a state-change internal action (nondeterministic computation step) is so
dramatic that it has to be bisimulated in a one-to-one fashion, and that a state-preserving
internal action (deterministic computation step) has so little consequence that it can becompletely ignored. In the following definition we leave out the adjective ‘branching’.
Definition 6. R is a bisimulation if the following statements are valid:τ— If P RQ −→ Q0 then one of the following statements is valid:– P =⇒ P 0 for some P 0 such that P 0 RQ and P 0 RQ0 .
τ– P =⇒ P 00 RQ for some P 00 such that ∃P 0 .P 00 −→ P 0 RQ0 .
τ

— If QR−1 P −→ P 0 then one of the following statements is valid:– Q =⇒ Q0 for some Q0 such that Q0 R−1 P and Q0 R−1 P 0 .
τ

– Q =⇒ Q00 R−1 P for some Q00 such that ∃Q0 .Q00 −→ Q0 R−1 P 0 .
Let’s now turn to the second criticism. The equivalence ≈ does not differentiatedefΩ = µX.τ.X(4)

from 0. One way to strengthen the weak bisimulation is to impose the termination preservation property (Walker 1990; Aceto and Hennessy 1992), as we have done to ≈↓ . While
this condition distinguishes between Ω and 0, it identifies the following processes.
µX.(τ.(X | d) + τ.X + τ ),

D1

=

D2

= µX.(τ.(X | d) + τ ).

(5)
(6)

The equivalence ≈↓ allows an infinite sequence of deterministic computations
τ

τ

τ

τ

D1 −→ D1 −→ . . . −→ D1 −→ . . .
to be simulated by an infinite sequence of nondeterministic computations
τ

τ

τ

τ

D2 −→ D2 | d −→ . . . −→ D2 | d | d −→ . . . ,which cannot be justified since the former produces nothing, whereas the latter keepoffering the environment the possibility to interact at channel d.
It is not difficult to see how to modify the termination preservation condition to takenondeterminism into account. Suppose P0 ≈ Q0 and
τ

τ

τ

τ

P0 −→ P1 −→ . . . −→ Pi −→ . . .

(7)

Mathematical Structures in Computer Science11

is an infinite computation sequence. If (7) contains an infinite number of nondeterministic computation steps, the bisimulation property guarantees that (7) is bisimulated byan infinite computation. However bisimulation fails to achieve that if (7) contains only
a finite number of nondeterministic computation steps. The additional requirement is
captured by the condition introduced next.
Definition 7. A relation R is codivergent if the following statements are valid:
τ

τ

τ

τ

— If P0 RQ0 −→ Q1 . . . −→ Qn −→ . . ., then ∃P1 .∃j > 0.P0 =⇒ P1 RQj .
ττττ— If P0 R−1 Q0 −→ Q1 . . . −→ Qn −→ . . ., then ∃P1 .∃j > 0.P0 =⇒ P1 R−1 Qj .
The property described in Definition 7 was introduced by Priese (Priese 1978). It has
been rediscovered in different contexts (van Glabbeek, Luttik and Trčka 2009; Fu andLu 2010).
At last we reach the model independent definition of process equality. We assume thatall process models have both the concurrent composition operator and the restriction
operator.
Definition 8. The absolute equality =M of a process model M is the largest binary
relation on M processes that validates the following statements:
1
2
3

The relation is reflexive.
The relation is extensional and equipollent.
The relation is a codivergent bisimulation.

The definition of the absolute equality is uniform for all models. We shall often omit thesubscript in =M . For more motivation for absolute equality the reader may consult (Fu2012). Let’s see an interesting equality about unobservable processes.
Lemma 2. P | Ω = Ω for every unobservable process P .
Proof. Let R be {(P0 , P1 ) | ∀i∈{0, 1}.Pi ≡ Ω ∨ (P | Ω =⇒ Pi and P is unobservable)}and let R◦ be the least relation satisfying the following: (i) R ⊆ R◦ ; (ii) R◦ is reflexive;(iii) if P R◦ Q then (P | O)R◦ (Q | O) and (O | P )R◦ (O | Q) for every process O; (iv) if
P R◦ Q then (c)P R◦ (c)Q for every name c. The relation R◦ is a reflexive, extensional,
equipollent, codivergent bisimulation.
We can now formally define the terminology we have informally used so far.
τ

— T → T 0 if T −→ T 0 = T . We say that T → T 0 is a deterministic computation stepsince T and T 0 must have the same input/output capacities.
ιτι— T −→ T 0 if T −→ T 0 6= T . We say that T −→ T 0 is a nondeterministic computation
0
step for the reason that either T and T have different input/output behaviors or they
have different divergent behaviors.
In the presence of the bisimulation condition, the codivergence condition is equivalent to
the termination preserving condition for deterministic computations. So the two conditions are equivalent when we deal with deterministic computation models.
Let’s come back to the examples (5) and (6). One has D1 ≈↓ D2 . However D1 6= D2

Nondeterministic Structure of Computation

12

since D1 can perform an infinite sequence of deterministic computation steps whereas
D2 cannot. It is the codivergence condition that tells them apart.
After Definition 8 we can now define effective translations between computation models
that admit nondeterminism.
Definition 9. A relation R from a model A to a model B is an effective subbisimilarity
if the following statements are valid:
1
2
3

R is total.
R is recursive.
R is a codivergent bisimulation.

We write A ve B if there is an effective subbisimilarity from A to B.
The terminology “subbisimilarity” is introduced for the fact that, if A ve B then there
is a bisimulation from A to B that reveals a submodel relationship between A and B.
The relation ve applies to a more general situation than ≤e . Obviously R ve A implies
R ≤e A. So CTT-II can be strengthened in terms of the more informative relation ve .
CTT-III. ∀A∈C. R ve A.

CTT-III applies to both computation models and interaction models. We say that amodel A is Turing complete if R ve A. The transitivity of ve allows one to conclude that
B is Turing complete after showing R ve A ve B.
The following particular instance of CTT-III is relevant to the present work. Apartfrom the argument for the recursiveness the proof is from (Busi, Gabbrielli and Zavattaro2003).
Proposition 1. R ve CCS.
Proof. The j-th register rj with the initial value 0 is interpreted by Zj defined byZj=

zeroj .Zj + incj .(c)(Sj (c) | c.Zj ),(8)

Sj (x)=

decj .x + incj .(c)(Sj (c) | c.Sj (x)).

(9)

The value of the register can be increased and decreased by interacting at channel
incj and decj respectively. The standard form of the interpretation of rj with value iis the process (ci−1 . . . c0 )(Sj (ci−1 ) | ci−1 .Sj (ci−2 ) | . . . | c2 .Sj (c1 ) | c1 .Sj (c0 ) | c0 .Zj ). Suppose L1 , L2 , . . . , Lk is the program of a CM. For each i ∈ {1, . . . , k − 1} the instruction
Li is interpreted by
incj .Ii+1
if Li = Succ(rj ),
(10)
Ii =
decj .Ii+1 + zeroj .Is
if Li = DecJump(rj , s).
The last instruction, which is End, is simply interpreted as 0. To achieve recursiveness we
use a fixed countable set of names {c0 , c1 , c2 , . . .}. We also need the following commutative
and associative rewriting system:
0|T(ci )(T | T 0 )(ci )T(ci )(ci | ci .T | T 0 )

7→ T,
7
→
T | (ci )T 0 ,
7
→
T,
7
→
(ci )(T | T 0 ),if ci does not appear in T ;if ci does not appear in T ;if ci does not appear in T 0 .

Mathematical Structures in Computer Science13

The reflexive and transitive closure of 7→ is denoted by 7→∗ . Suppose CM is a CM. The
canonical interpretation of CM is the tuple
hN1 , . . . , Nk0 , Ij , D(L1 ), . . . , D(Lk )i,where L1 , . . . , Lk is the program of CM, D(L1 ), . . . , D(Lk ) are the parametric definitions interpreting the instructions, Ij is the interpretation of the current instruction, andN1 , . . . , Nk0 are the normal forms interpreting the values of the registers of CM. Let R
be the set of the pairs of the form hCM, hN10 , . . . , Nk0 0 , Ij , D(L1 ), . . . , D(Lk )ii such that
N10 7→∗ N1 , . . . , Nk0 0 7→∗ Nk0 , where hN1 , . . . , Nk0 , Ij , D(L1 ), . . . , D(Lk )i is the canonicalinterpretation of CM. Busi, Gabbrielli and Zavattaro’s proof can be strengthened to showthat R is total, codivergent and bisimilar. The recursiveness is due to the following facts:
1 It is decidable if a CCS process is the interpretation of a CM configuration.
2 Given a CCS interpretation of a CM configuration, it is algorithmically feasible torecover the CM configuration.
Both (1) and (2) make use of the rewriting system.
Just as CTT-I allows one to use a recursive function without worrying about how
it is defined, CTT-III asserts that in a Turing complete model a process with certain
behavior must exist and we may refer to it without explicitly defining it. Let’s illustrate
this point by an example. Suppose f(x) is a unary computable function and A is a CCS
process A. Then there exists a parametric definition, notation Cf (x, u, y, v, z, w).A, suchdefthat F = Cf (in, end, out, stop, dec, zero).A behaves as follows: If f(k) is undefined, then
in

in

end

F |→∗ −→ .{z. . →∗ −→} −→ = Ω;
k

∗ in

in

end

out

out

stop

if f(k) is defined, then F →. . →∗ −→} −→ |→∗ −→ .{z. . →∗ −→} −→ = A | JkKzero
dec ,| −→ .{zkf(k)where JkKzero· · .dec}.zero. For those who have not built up strong confidence indec ≡ dec.
| ·{zk

the interactive version of Turing completeness, we point out that formally the parametricdefinition Cf (x, u, y, v, z, w).A is given by(ab)(ak0 )(ak1 )(zr)(ic)(dc)(ic1 )(R | Z0 | JfKzr,ic,dc| a.b.ak1 .A | b.Cp(dc, zr, y, v) | R1 ),
a
where
R
S(z)
Z0
S0 (x)R1
S1 (x)Cp (dc, zr, y, v)
Sc (z)= u.ak0 + x.(c)(S(c) | c.R),= u.ic.ic1 .z.u + x.(c)(S(c) | c.S(z)),= ak0 .zr + ic.(c)(S0 (c) | c.Z0 ),= ak0 .dc.x.ak0 + ic.(c)(S0 (c) | c.S0 (z))),= ak1 .w + ic1 .(c)(S1 (c) | c.R1 ),= ak1 .z.x.ak1 + ic1 .(c)(S1 (c) | c.S1 (z))),= zr.v + dc.(c)(Sc (c) | c.R),= zr.y.z.zr + dc.(c)(Sc (c) | c.Sc (z)),

Nondeterministic Structure of Computation

14

and JfKzr,ic,dc
is the process that calculates f with the input number stored in the registerawith access channels zr, ic, dc. The process indicates the termination of the calculation
by performing the action a, which can be achieved by interpreting the End instruction
by a. In summary the process F inputs the number k at channels in, end, and thencalculates f(k); if f(k) is undefined, then it loops forever; otherwise it outputs the number
f(k) at channels out, stop and copy the number k at channel dec, zero before it starts A.
The number k is kept because later calculation may well need it. It is easily seen how
to generalize from Cf (x, u, y, v, z, w).A to Cf (ex, ue, y, v, ze, w).Ae
for a k-ary computablefunction.
We are now in a position to define reductions between process calculi. Suppose R is aneffective reduction from M to N and that P RP 0 and QRQ0 . If P and Q are codivergent
bisimilar, then P 0 and Q0 are codivergent bisimilar by the definition of R. In other words
equal computational objects are translated to equal computational objects by R. We
need to promote this soundness condition from the level of computation to the level ofinteraction.
Definition 10. A relation from the set of M-processes to the set of N-processes is soundif P RP 0 , QRQ0 and P =M Q implies P 0 =N Q0 .
The next definition should be compared to Definition 2 and Definition 8.
Definition 11. A relation from the set of M-processes to the set of N-processes is asubbisimilarity if it validates the following statements:
1
2
3

It is total and sound.
It is extensional and equipollent.
It is a codivergent bisimulation.

We write M v N if there is a subbisimilarity from M to N.
Intuitively M v N means that N is at least as expressive as M. In this paper there
are only a few simple references to v. So we shall not elaborate on the relation. See (Fu2012) for a full exposition of the expressiveness relation.
We now fix the class M of interaction models we are concerned with in this paper. The
running theme of this paper is that an interaction model is a computation model if theinteractive capacity of the model is ignored. Thus M ⊆ C. When thinking of a processmodel M as a computational model the following assumptions on M are general enoughto cover all models of our interest.
— There is an effective bijection between N and the set of the M-processes. In otherwords the M-processes are Gödel enumerable.
— All computations in M are finite branching.
— There is an algorithm that, given an M-process P , calculates all the one-step compuτ
tations of the form P −→ P 0 .
These effective conditions have been used to study structural operational semantics, giving rise to effective operational semantics (Vaandrager 1993). Variants of these conditions
are proposed in a number of papers (Baeten, Bergstra and Klop 1987; de Simone 1985;
Darondeau 1990; Bloom, Istrail and Meyer 1995).

Mathematical Structures in Computer Science15

Our interaction models are expressive enough so that (i) they are Turing complete and(ii) they are at least as expressive as CCS. By Proposition 1, (i) is subsumed by (ii).
Hence the next definition.
Definition 12. An interaction model M rendering true the above three statements iscalled a Turing-Milner model if CCS v M.
In a Turing-Milner model the execution tree of an unobservable process can be algorithmically generated. The finite branching versions of the well-known complete process calculi are Turing-Milner models. These include the π-calculus (Milner, Parrow andWalker 1992; Sangiorgi and Walker 2001) and the value-passing calculus (Hennessy andIngólfsdóttir 1993; Hennessy and Lin 1995; Fu 2013). Proving that a model is not a
Turing-Milner model is generally a tricky issue. We know however that CCSµ is not a
Turing-Milner model since it is not even complete (Fu 2012).
From now on M denotes the class of Turing-Milner models. For a model M in M, wewrite P ∈ M to indicate that P is an M-process.
What we have done so far is a condensed account of the journey starting from theoriginal formulation of the Church-Turing Thesis, via Milner and Park’s notion of weakbisimulation and van Glabbeek and Weijland’s discovery of the branching bisimulation,
reaching to a technical formalization of the thesis. Our journey was led by the fact that it
is in the theory of interaction that the full picture of the nondeterministic computations
can be unveiled. It is against this background that Definition 8 emerges as a canonicalequality for both interactive objects and computational objects. The purpose of this paper
is to start investigating the rich structures of nondeterministic computations revealed bythis equality.
4. Finite State Computation
In this section we shall use a variant of CCSµ that admits only τ actions. The finite state
terms are generated from the following grammar:
T:= X | S | ∆(T ) | µX.T,

S:= 0 | τ.T | S + S.

The ∆ operator is introduced by Hennessy and Milner (Hennessy 1981), where it is calleda delay operator and is denoted by δ. It plays an important role in the algebraic theory of
SCCS (Milner 1983). The term ∆(T ) either behaves as T or evolves to itself. A finite statecomputational object is a finite state term that does not contain any free term variables.
The semantics of the ∆-operator is defined by the following two rules:ττ∆(T ) −→ ∆(T )τ

T −→ T 0
τ∆(T ) −→ T 0

We call the transition ∆(T ) −→ ∆(T ) a self-loop. We write T
T 0 if T → T 0 , that isττ00
T −→ T = T , and the transition T −→ T is not caused by a self-loop. If there does
not exist any T 0 such that T → T 0 then we write T 9. The notation T 6 is definedsimilarly.

Nondeterministic Structure of Computation

16

The simplest terminating computational object is of course 0, and the simplest divergent computational object is Ω defined in (4). All the other finite state computational
objects have potential both to terminate and to diverge. The execution of ∆(τ ) can be
described by the following labeled tree:
•

−→

ι

◦

−→

ι

◦

ι

◦

↓
◦
↓
◦ −→
..
.

where the node indicated by ‘•’ is the root of the tree. The object τ + τ.Ω is an internal
choice between 0 and Ω. Its execution tree is
···

◦

←

ι

•

−→

ι

◦

•
↓
ι
←− ◦
↓
ι
←− ◦
..
.

−→

ι

◦

−→

ι

◦

ι

◦

◦

←

◦

←−

←−

The execution tree of ∆(τ + τ.Ω) is
···

◦

←

◦

←

◦

···

◦

←

◦

←

◦

···

◦

←

◦

←

◦

ι

−→

Using the codivergence condition it is easy to see that the above five computational
objects are pairwise unequal.
The finite state computational objects would not be very interesting if there are only
finitely many of them. We now construct an infinite sequence of finite state computational
objects that are pairwise unequal. The first three in the sequence are defined as follows:
Υ0

= 0,

Υ1

=

Υ2

= τ.0 + τ.Ω.

∆(τ.0),Starting from Υ3 the sequence is defined recursively by (11) and (12), where i > 0:
Υ2i+1

=

∆(τ.0 + τ.Υ2i ),

(11)

Υ2i+2

=

τ.0 + τ.Ω + τ.Υ2i+1 .

(12)

The next theorem says that the processes Υ0 , Υ1 , Υ2 , . . . are pairwise unequal.
Theorem 1. ∀i > 0.∀j < i. Υj 6= Υi .
Proof. The natural induction is as follows:— It is clear that Υ0 , Υ1 , Υ2 are pairwise unequal and none of them is equal to any Υkfor every k ≥ 3.

Mathematical Structures in Computer Science17— Suppose k ≤ 2i. By the induction hypothesis the self loop Υ2i+1 → Υ2i+1 cannot beτbisimulated by Υk if k is even. If k is odd Υ2i+1 −→ Υ2i cannot be bisimulated byΥk according to the induction hypothesis. So the process Υ2i+1 is not equal to any
Υk with k ≤ 2i.
ι— Suppose k ≤ 2i + 1. The action Υ2i+2 −→ Ω cannot be matched up by any actionτof Υk whenever k is odd. If k is even, Υ2i+2 −→ Υ2i+1 cannot be bisimulated by Υkaccording to the induction hypothesis. So the process Υ2i+2 is not equal to any Υkwith k ≤ 2i + 1.
We are done.

4.1. Algebraic Properties
Since a computational object never interacts, the absolute equality over the computational objects is simply the largest codivergent bisimulation on these objects. We will
also use the so called strong bisimilarity (Milner 1980; Park 1981).
Definition 13. The Milner-Park equality ∼ is the largest relation R that validates thefollowing strong bisimulation property:ττ— If P RQ −→ Q0 , then P −→ P 0 RQ0 for some P 0 .
ττ— If QR−1 P −→ P 0 , then Q −→ Q0 R−1 P 0 for some Q0 .
Obviously ∼ ( = ( ≈.
An equality on processes can be extended to an equality on terms in the standard
manner. For instance T = T 0 if T {P1 /X1 , . . . , Pn /Xn } = T 0 {P1 /X1 , . . . , Pn /Xn } for allprocesses P1 , . . . , Pn .
Let’s now take a look at the algebraic properties of the fixpoint terms modulo theequalities ∼, =, ≈. The following equality is the defining property of the fixpoint µX.T :µX.T ∼ T {µX.T /X}.

(13)

The term T {µX.T /X} is said to be the unfolding of µX.T . The following beautiful
axioms of Bloom and Ésik (Bloom and Esik 1994) are also valid with respect to theMilner-Park equality.
µX.T {T 0 /X}µX.µY.T∼ T {µX.T 0 {T /X}/X},(14)∼ µY.T {Y /X}.

(15)

Thinking of µX.T {T 0 /X} as a tree, it is an infinite alternation of the part defined by T
and the part defined by T 0 , which explains (14). It should be clear that (13) is a special
case of (14). If we admit the unguarded choice terms of the form T + T 0 , we have thefollowing equalities:µX.(X+T ) ∼µX.T,µX.(τ.X+T ) ≈µX.τ.T,

0µX.(τ.(X+T )+T )

=

(16)
(17)
0

µX.(τ.X+T +T ).

(18)

Nondeterministic Structure of Computation

18

The equalities (16), (17) and (18) are the famous axioms of Milner (Milner 1989b) for
the finite states. They help to remove the unguarded occurrences of a bound variable sothat the following fixpoint induction rule can be applied.
T 0 = T {T 0 /X}
T 0 = µX.T

(19)

X is guarded in T.

By ‘X is guarded in T ’ we mean that every occurrence of X in T is guarded by at least
one non-τ prefix.
The equalities (13) through (18) have all been used as axioms in equational systems
for the finite state behaviours. If we intend to construct an equational proof system forthe absolute equality = on the finite state computational objects, none of (16), (17) and(18) would be useful. This is because (16) and (18) make essential use of the unguarded
choice operator and (17) is not even valid for the termination preservation bisimilarity.
Needless to say the fixpoint induction rule (19) is also irrelevant in the present context
since we have ignored all non-τ actions.
Let’s now turn to the algebraic properties of divergence. Milner’s approach to obtaining
complete axiom systems for finite state behaviours heavily relies on the fixpoint induction
rule. If we try to apply it to tackle the divergent problem of the finite state processes,
we would face the following dilemma:— All divergence is essentially caused by the unguarded occurrences of bound variables.
— The side condition of (19) rules out any possibility to reason about divergence using
fixpoint induction.
An ingenious solution that bypasses this dilemma is given by Lohrey, D’Argenio andHermanns (Lohrey, D’Argenio and Hermanns 2002; Lohrey, D’Argenio and Hermanns
2005). Their key observation is that for finite state behaviours all forms of divergence arecaused by τ -loops, and that all τ -loops can be reduced to self-loops. An induced operator
that helps rewrite all τ -loops to self-loops is therefore important. Using the unguarded
choice operator it can be defined by
def

∆(T )

=

µX.(τ.X+T ),(20)

where the variable X does not appear in T . Some useful equalities about the ∆-operator
follow immediately from definition (20). For example∆(T ) ∼ τ.∆(T ) + T ∼ ∆(T ) + T ∼ τ.∆(T ) + ∆(T ).
In this paper we cannot use (20) to define ∆ because we do not use the general choice
operator. This is why we have introduced ∆ as a primitive operator. The equalities
studied in (Lohrey, D’Argenio and Hermanns 2002; Lohrey, D’Argenio and Hermanns
2005) are all weaker than the absolute equality. But some of their laws are valid for =.
Here are two examples.
µX.(∆(X+T ) + T 0 )0µX.(τ.(X+T ) + T )= µX.∆(T +T 0 ),

(21)
0

0

= µX.(τ.∆(T +T ) + T ).

Again these laws make use of the unguarded choice.

(22)

Mathematical Structures in Computer Science19

Let’s summarize the issues we must resolve in order to produce an equational system. First of all most laws concerning the µ-operator and the ∆-operator are no longer
available. We need to come up with some alternatives. Secondly we need to find an
equational replacement for the fixpoint induction. The fixpoint induction allows one toprove the equality between a short term and a very long term. An example is µX.a.X =µX.a. . a} .X where k > 0. It is proved in (Sewell 1994; Sewell 1997) that no pure equa| .{zk timestional system is strong enough to derive this equality for all k > 0. We will give a similar
non-existence result in Section 4.3. Our solution is to use axiom schemata. For that
purpose one needs to use C-contexts.
Definition 14. A C-context is either [ ], or τ.C[ ]+S, or S+τ.C[ ], or ∆(C[ ]), or µX.C[ ]whenever C[ ] is a C-context.
The next lemma states three useful schemata with the help of C-contexts.
Lemma 3. The following equalities are valid:1
2
3µX.C[τ.(τ.X+S1 )+S2 ] = µX.C[τ.X+S1 +S2 ];µX.C[∆(X)] = µX.C[τ.X];µX.C[∆(τ.X+S)] = µX.C[τ.X+S].
Proof. All the three equalities can be established using Computation Lemma.

4.2. Axioms for Finite State Computation
To simplify the description of the computational objects, we have introduced the prefixedversion of the binary choice operator and the ∆-operator. The tradeoff is that the absoluteequality is no longer a congruence. It is well known that the binary choice operator does
not preserve =. One has that 0 = τ , yet 0 + τ.Ω 6= τ + τ.Ω. The ∆-operator does notpreserve = either. The processes τ and 0 are equal. But clearly ∆(τ ) 6= ∆(0). The largest
congruence contained in the absolute equality can be defined in the standard manner.
Definition 15. P and Q are congruent, notation P  Q, if the following are valid:ττ

1 If P −→ P 0 then Q −→ Q0 = P 0 for some Q0 .
ττ
2 If Q −→ Q0 then P −→ P 0 = Q0 for some P 0 .
PPSuppose P ≡ i∈I τ.Ti and Q ≡ j∈J τ.Tj with ≡ being the syntactic equality, andιneither P nor Q contains any occurrences of the µ-operator. If Q = P −→ P 0 and Q0 6= P 0
τfor all Q0 such that Q −→ Q0 , then it is easily seen that P + τ.Υk 6= Q + τ.Υk for somelarge enough k. This explains why clause (1) of the above definition cannot be replacedττ
by “If P −→ P 0 then Q →∗ −→ Q0 = P 0 for some Q0 ”. The proof of the next proposition
is standard.
Proposition 2. The equivalence  is the largest congruence contained in =.
The proof system AC for finite state computational objects consists of the axioms
defined in Fig. 1. We write AC ` T = T 0 to indicate the fact that the equality T = T 0

Nondeterministic Structure of Computation

20

S1
S2
S3
S4

0+S
S1 + S2(S1 + S2 ) + S3
S+S

=
=
=
=

S
S2 + S1
S1 + (S2 + S3 )
S

F1
F2
F3
F4
F5
F6

µX.T
µX.X
µX.(τ.X+S)µX.C[τ.(τ.X+S1 )+S2 ]µX.C[∆(X)]µX.C[∆(τ.X+S)]

=
=
=
=
=
=

T {µX.T /X}
0∆(µX.S)µX.C[τ.X+S1 +S2 ]µX.C[τ.X]µX.C[τ.X+S]

D1
D2∆(∆(T ))
∆(S)

=
=

∆(T )
S + τ.∆(S)

T
C

τ.T
τ.(S+S 0 )

=
=

τ.τ.T
τ.(S+τ.(S+S 0 ))Fig. 1. Axioms for Computation
can be derived by repetitive use of the equivalence laws, the congruence laws and thelaws of AC.
The axiom C is related to the B law of van Glabbeek and Weijland (van Glabbeek and
Weijland 1989) by restricting to τ -prefix. The T law is a special case of Milner’s first tau
law. A special case of C isτ.S=

τ.(S + τ.S).

(23)

F2 deals with bound variables that are not prefixed. F3 and F4 can be applied to get
rid of a prefixed bound variable. F5 and F6 help to remove a ∆-operator outside abound variable. These axioms and axiom schemata should be compared to the laws (21)and (22) of Lohrey, D’Argenio and Hermanns (Lohrey, D’Argenio and Hermanns 2002;
Lohrey, D’Argenio and Hermanns 2005). For the above system the fixpoint unfolding law
F1 can be simplified toµX.T = Twith the side condition that X does not appear in T . The axiom D1, appeared in Hennessy’s work more than 30 years ago (Hennessy 1981), is weaker than the following axiomof Lohrey, D’Argenio and Hermanns:∆(∆(T ) + T 0 ) = τ.(∆(T ) + T 0 ).

(24)

The equality (24) fails the codivergence condition.
Proposition 3. If AC ` T = T 0 then T  T 0 .
Proof. F3 is obviously valid if X does not appear in S. If X occurs in S then µX.(τ.X +S)  µX.S. So clearly F3 also holds in this case. F4, F5 and F6 are valid by Lemma 3.
D1 and D2 are actually true of the Milner-Park equality.

Mathematical Structures in Computer Science ◦ - ◦

6


•


21
◦

-◦

6
•


Fig. 2. Two D-Graphs
The following equality follows from F3, F1, S1 and S2.
∆(0) = µX.τ.X.

(25)µX.∆(X) = µX.τ.X.

(26)

An instance of F5 is
The law D2 is as it were a divergent counterpart of the C law. It implies the equality∆(0) = τ.∆(0).

(27)

4.2.1. D-Normal Form The finite state computational objects can be visualized as graphs.
Conversely finite graphs of a certain type can be coded up by the finite state computational objects. It is trivial to generalize the finite graphs that represent the finite statecomputational objects to infinite graphs.
Definition 16. A directed graph is a D-graph if the following hold:
1
2

There is a special node called the root of the D-graph.
There is at most one edge from one node to another node. A self-loop is an edge froma node to itself.
3 Every node is reachable from the root.
The two diagrams in Fig. 2 are D-graphs. A root is indicated by a ‘•’. If the root selfloops, a ‘’ is placed right below the ‘•’. If a node is not a root, it is indicated by a ‘◦’;and if it self-loops, it is simply indicated by a ‘’.
Definition 17. A D-graph is definable in a process model if there is an unobservable
process P of that model that is codivergent bisimilar to the root of the D-graph. In thiscase we say that the D-graph represents the process. We write d(P ) for the D-graphgenerated by P .
Every finite D-graph is definable by a finite state computational object. We start byintroducing a variable for each node of a given finite D-graph. If the D-graph has nnodes, we define a set of n equations of the form:
X0 = T0 , . . . , Xn−1 = Tn−1 .
The first is the head equation corresponding to the root. If the i-th node has no outgoing edges then we have Xi = 0, and if the node has a self-loop then we introduce
the equation Xi = ∆(0). If the i-th node has k children Xm1 , . . . , Xmk , then the i-th
equation is Xi = τ.Xm1 +. . .+τ.Xmk . If in addition the i-th node has a self-loop, the i-th
equation is Xi = ∆(τ.Xm1 + . . . + τ.Xmk ). Using the standard method (Milner 1984) we
can easily construct solutions to the equation system. The solution to X0 is represented
by the D-graph.

Nondeterministic Structure of Computation

22

We now describe a procedure that converts a finite computational object to one that
corresponds to a D-graph. For that purpose we introduce D-normal forms.
Definition 18. A term T is a D-normal form, or D-nf, if it satisfies the following:
1
2

T is a variable;P
If T is a Σ-term, say i∈I τ.Ti , then Ti must be a D-nf for every i ∈ I; in particular
0 is a D-nf;
3 If T is a ∆-term then it must be either of the form ∆(X) or of the form ∆(S) suchthat S is a D-nf;
4 If T is a µ-term then it must be of the form µX.S such that S is a D-nf and X appearsin S;
5 T contains no subterm of the form ∆(X) for any bound variable X.
The finite state µX.µY.(τ.X +τ.Y ) for example is equal to µX.(∆(µY.τ.X)) by F3, whichis in turn converted to µX.(∆(τ.X)) by F1, which can be further reduced to µX.τ.X by
F6. We conclude that AC ` µX.µY.(τ.X + τ.Y ) = µX.τ.X = ∆(µX.X) = ∆(0) by F2,
F3, S1 and S2.
A D-nf is a CCS process notation for a finite D-graph. The process 0 is the trivial onenode D-graph, and Ω is the D-graph with only one node and the self-loop. The Σ-processP1≤i≤n τ.Ti defines the D-graph whose root has n out-going edges pointing to the rootsof the D-graphs defining T1 , . . . , Tn respectively. The ∆-process ∆(S) corresponds to theD-graph whose root has a self-loop. The µ-process µX.S is obtained from the D-graphof S{0/X} by adding the obvious edges pointing to the root.
Lemma 4. For each term T , there is a D-nf T 0 such that AC ` T = T 0 .
Proof. According to the structural definition of D-nf, a subterm of a D-nf is a D-nf
and if T, T 0 are in D-nf then T {T 0 /X} is a D-nf. The proof of the lemma is given by thefollowing structural induction.
— T ≡ 0 or T ≡ X. There is nothing to prove.
— T ≡ τ.T 0 . We apply the induction hypothesis to T 0 .
P— T ≡ i∈I τ.Ti . We apply the induction hypothesis to each Ti . Notice that we canapply S1 to remove redundant 0 from a Σ-term.
— T ≡ ∆(T 0 ). By the induction hypothesis some D-nf T 00 exists such that AC ` T 0 = T 00 .
If T 00 is a ∆-term, we apply D1 to remove the extra ∆-operator. If T 00 is a µ-term,
we apply F1 to unfold it.
— T ≡ µX.T 0 . By the induction hypothesis, AC ` T 0 = T 00 for some D-nf T 00 . If X does
not occur in T 00 , we get rid of the µ-operator by applying F1. If T 00 is X, we apply
F2 to get 0. If T 00 is ∆(X), we apply (26) to get Ω. If T 00 is a µ-term, we apply F1to unfold it. If T 00 is of the form ∆(S), then we apply F6 to remove the ∆-operator.
Finally use F5 to remove the ∆-operator in all occurrences of ∆(X).
We are done.
4.2.2. C-Normal Form Two nodes in a D-graph are said to be equal if they are codivergent in the sense of Definition 7 and bisimilar in the sense of Definition 6. The left

Mathematical Structures in Computer Science

23

◦ -◦

◦ -◦

◦ -◦

◦ -◦



I
@
?@

@
I
?
@

@ 6
I
?@

@ 6
I
?
@

@ 6
I
?@



•




•




•




•


◦


•





@ 6
I
?@

◦

•






@ 6
I
@
?


◦

•





@ 6
I
@
?


◦

•


Fig. 3. C-Graphs with Four Nodes
D-graph in Fig. 2 has two pairs of equal nodes; the right D-graph has one pair of equal
nodes. The structure of computations is given by the D-graphs containing no equal nodes.
Definition 19. A C-graph is a D-graph in which no two nodes are equal.
The eight D-graphs in Fig. 3 are C-graphs with four nodes.
It follows from definition that a C-graph does not contain any loops larger than aself-loop. In particular the root of a C-graph does not have any incoming edges apartfrom a possible self-loop.
Let G be the set of C-graphs, ranged over by f, g, h, i. The letter f will stand for a finite
C-graph and i an infinite one. For each k > 0 let Fk be the set of the finite C-graphs withk-nodes. The C-graph representing Υk has precisely k + 1 nodes. So Fk is a nonempty
finite set for each k > 0.
Lemma 5. The roots of two C-graphs are equal if and only if the C-graphs are isomorphic.
Proof. Suppose g0 , g1 are C-graphs. If they are isomorphic, then one can construct a
codivergent bisimulation by paring all the corresponding nodes. Conversely suppose theroots of the graphs are equal. Given any node N in g0 , a unique path from the root to N
exists. Using the bisimulation property one can construct a unique corresponding pathin g1 . The end node of this path corresponds to N . This gives rise to a function fromthe set of nodes of g0 to the set of nodes of g1 . By induction one easily sees that it is an
isomorphic map.
According to Lemma 5, the C-graph representation of an unobservable process P is
unique. Consequently we can talk about equality between C-graphs. We write c(P ) for
this unique C-graph.
We are now going to single out the set of finite state computational objects that
correspond to finite C-graphs. The correspondence is not as close as that between the Dnf’s and the finite D-graphs. In the process algebraic notation there is no way to remove
all the repetitive occurrences of a subterm.
Definition 20. A D-nf T is a C-normal form, or C-nf, if the following are valid:1
2

T does not contain any occurrences of the µ-operator;
One of the following statements is true:(a) T ≡ X or T ≡ ∆(X) for some term variable X;
P(b) T ≡ i∈I τ.Ti such that, for each i ∈ I, the term Ti is a C-normal form; moreover∀j, k ∈ I.j 6= k ⇒ Tj 6= Tk and ∀i ∈ I.Ti 6= T ;PP(c) T ≡ ∆( i∈I τ.Ti ) such that i∈I τ.Ti is a C-nf and ∀i ∈ I.Ti 6= T .

Nondeterministic Structure of Computation

24

Conditions (2a,2b) make sure that T 6 , meaning that T contains no loops other thanself-loops. If T1 , T2 are C-normal forms then T1  T2 is almost the same as T1 ∼ T2 . Thissuggests that the C-nf’s should play an important role in the completeness proof. The
next proposition states a pre-completeness result.
Proposition 4. Suppose T1 , T2 are C-nf’s and T1 = T2 . The following are valid:
1 If both T1 and T2 are Σ-terms, then AC ` τ.T1 = τ.T2 .
2 If both T1 and T2 are ∆-terms, then AC ` T1 = T2 .
Proof. The proof is carried out by simultaneous structural induction. Since a ∆-termloops while a Σ-term that is also a C-nf does not loop, T1 , T2 must be both Σ-terms orboth ∆-terms.
PPτ— T1 ≡ i∈I τ.T1i and T2 ≡ j∈J τ.T2j with I 6= ∅ 6= J. The action T1 −→ T1i must beτmatched by T2 −→ T2j = T1i for some T2j , according to the definition of C-nf. By the
induction hypothesis AC ` τ.T1i = τ.T2j . It follows that AC ` T2 + τ.T1i = T2 + τ.T2j =T2 . We conclude by induction and symmetry that AC ` T1 = T1 + T2 = T2 .
P
PPP
— T1 ≡ ∆( i∈I τ.T1i ) and T2 ≡ ∆( j∈J τ.T2j ). Since both i∈I τ.T1i and j∈J τ.T2j
P
P
are C-nf’s, it follows easily by a bisimulation argument that i∈I τ.T1i = j∈J τ.T2j .
P
PSo AC ` i∈I τ.T1i = j∈J τ.T2j by the induction hypothesis. Hence AC ` T1 = T2 .
We are done.
We will reach our goal if we can prove a normalization result, stating that every termis provably equal to a C-nf. This is indeed the case to a large extent.
Proposition 5. The following statements are valid:
1 For every Σ-term T there is some C-nf T 0 such that AC ` τ.T = τ.T 0 .
2 For every ∆-term T there is some C-nf T 0 such that AC ` T = T 0 .
Proof. Observe that we may remove all occurrences of µ-operator in a term by using
the F-laws. The following is an algorithm that removes the fixpoint operator in µX.T .
— If X does not appear in T , apply F1 and exit.
— If T ≡ X, apply F2 and exit.
— Suppose X appears in T and T 6≡ X.
– Replace every occurrence of ∆(X) by τ.X using F5.
– Now every occurrence of X must appear in some subterm τ.X of T . We can remove
all occurrences of X in the following manner:•

Apply F4 and F6 to remove all τ -prefixes and ∆’s in front of the subterm.

•

If the subterm τ.X is not guarded by any τ and ∆, apply F3.

Notice that the transformation does not create any new occurrence of X.
It follows from the observation and the proof of Lemma 4 that we may assume that T isa D-normal form containing no occurrences of the µ-operator. The following argument
is by structural induction.
— T ≡ 0 or T ≡ X. There is nothing to prove.

Mathematical Structures in Computer Science
—T ≡
that

25

0
i∈I τ.Ti . For each i ∈ I there is by the induction hypothesis a C-nf Ti suchPAC ` τ.Ti = τ.Ti0 .

(28)

If Ti0 = Tj0 for some j 6= i then AC ` τ.Ti0 = τ.Tj0 according to Proposition 4. So wemay remove one of them using S4. Without loss of generality, we assume that for alli, i0 ∈ I, Ti0 6= Ti00 whenever i 6= i0 . Now supposeX
τ.Ti0 = Tk0
(29)
i∈I

for some k ∈ I. If I is a singleton set, thenAC ` τ.T = τ.τ.Tk0 = τ.Tk0
by the T-law. Now suppose the size of I is greater than 1. There are two subcases.
τ– Tk0 is a Σ-term. For every j ∈ I \ {k} there is some D-nf Tkj such that Tk0 −→ Tkj =Tj0 . So we haveAC ` τ.Tkj = τ.Tj0(30)

by Proposition 4. It follows from (28), (30), S4 and C thatXAC ` τ.T = τ. τ.Tk0 +τ.Tj0 j∈I\{k} X= τ. τ. Tk0 +τ.Tkj  +τ.Tkj j∈I\{k}j∈I\{k}




X


X

= τ. Tk0 +τ.Tkj j∈I\{k}τ.Tk0 .

=

– Tk0 is ∆(Sk ) for some C-nf Sk . Using a similar argument one can show thatX
AC `
τ.Tj0 = Sk .
(31)
j∈I\{k}It follows from (31) thatAC ` T= τ.Tk0 +

X

τ.Tj0

j∈I\{k}= τ.∆(Sk ) + Sk=∆(Sk )= Tk0 ,
where the second last equality is due to D2. Hence AC ` τ.T = τ.Tk0 .
PPP— T ≡ ∆( i∈I τ.Ti ) where i∈I τ.Ti is a C-nf. Suppose ∆( i∈I τ.Ti ) = Tk for somek ∈ I. Since Tk is a C-nf, it must be a ∆-term. Let Tk be ∆(Sk ). Using the above

Nondeterministic Structure of Computation

26

argument we can show thatAC ` Sk

=

X

Sk +

τ.Tj

j∈I\{k}X=

τ.Tj .

j∈I\{k}ThereforeAC ` T=∆ τ.∆(Sk ) +X

τ.Tj 

j∈I\{k}=∆ (τ.∆(Sk ) + Sk )=∆(∆(Sk ))=∆(Sk ),

where the third equality holds by D2 and the fourth equality holds by D1.
This completes the proof.
4.2.3. Completeness We are now in a position to prove the completeness result.
Theorem 2. T 0  T 00 if and only if AC ` T 0 = T 00 .
Proof. Suppose T 0 , T 00 are C-nf’s and T 0  T 00 . The proof is a structural induction.
— If T 0 is 0 then T 00 must be 0. Similarly if T 0 is X then T 00 must be X.
— If T 0 , T 00 are ∆-terms, then AC ` T 0 = T 00 by Proposition 4 and Proposition 5.
P
00— Suppose T 0 ≡i∈I τ.Ti  ∆(S) ≡ T . By Proposition 5 and the C law we may
assume that ∆(S) and all Ti ’s are C-nf’s. By definition there is some k ∈ I such that
Tk = ∆(S). Therefore Tk  ∆(S) since both Tk and ∆(S) are C-nf. If I \ {k} isPnonempty, then it is easy to see that i∈I\{k} τ.Ti  S. So
XAC `τ.Ti = Si∈I\{k}by induction. Hence
X
X
AC `τ.Ti = τ.∆(S) +τ.Ti = τ.∆(S) + S = ∆(S),i∈I

i∈I\{k}where the last equality is due to D2. Suppose I \ {k} is empty. Then τ.Tk  ∆(S).
By codivergence Tk = ∆(S). Since both Tk and ∆(S) are C-nf, one must have Tk ∆(S). If S ≡ 0 then we can use (27) to finish the proof. If S is not 0, it must be aproper choice term. By a bisimulation argument and induction one easily sees thatAC ` Tk = τ.∆(S) + S = ∆(S).
— If both T 0 , T 00 are Σ-terms, then AC ` T 0 = T 00 follows from Proposition 4, Proposition 5 and the C law.
The proof is complete.

Mathematical Structures in Computer Science27

It can be easily verified that µX.∆(T )  ∆(µX.T {∆(X)/X}). So Theorem 2 implies
AC ` µX.∆(T ) = ∆(µX.T {∆(X)/X}). Using this equality we can push all occurrencesof ∆ up to the root and down to the leaves.

4.3. Nonaxiomatisability
One may feel a little unhappy about the C-contexts which appear in the axiomatic systemdefined in Fig. 1. The fact is, however, that the use of such contexts is unavoidable. The
situation reminds one of Sewell’s remarkable result (Sewell 1994; Sewell 1997) on thenonexistence of a finite purely equational system for finite state processes. We shallestablish a nonexistence result concerning finite pure axiom systems. In our setting apure axiom system is a recursive set of equations between the finite state computational
objects. The equations in a pure axiom system are pure as it were since schematic axioms
like F4, F5 and F6 are banned.
The proof of Sewell’s negative result is highly nontrivial. Fortunately we have a simple
proof of a nonexistence result in the present case. The intuition is that for every finite
pure axiom system there is a large enough number k such thatµX.(τ.(τ.(. . . τ.(τ.X + τ.Υ1 ) + . . .) + τ.Υk−1 ) + τ.Υk ) = ∆(τ.Υ1 + . . . + τ.Υk )(32)

is not provable in the system.
Theorem 3. There does not exist any sound and complete finite pure axiom system for on the finite state terms.
Proof. For the purpose of this proof, let’s define the size of a term as the maximum
number of nested τ prefixes that guard a variable. Given any finite pure axiom system
ACp there is a number k such that the size of the term on the left/right hand side of any
axiom of ACp is less than k. Now supposeµX.(τ.(τ.(. . . τ.(τ.X + τ.Υ1 ) + . . .) + τ.Υk−1 ) + τ.Υk ) = T 0 .

(33)

We prove by induction on derivation that T 0 must be a µ-term whose size is at leastk. If (33) is derived by the transitive rule, we apply the induction hypothesis. If (33) isderived by an application of an axiom in ACp then, since the size of the axiom is lessthan k, the term T 0 must be of the form µX.Tc for some Tc and we must have
ACp ` τ.(τ.(. . . τ.(τ.X + τ.Υ1 ) + . . .) + τ.Υk−1 ) + τ.Υk = Tc .
The variable X must appear in Tc for otherwise we could instantiate the X on the left
hand side by a term with sufficiently many nested τ prefixes such that a computation
sequence from the left hand side cannot be matched up by any computational sequencesfrom the right hand side. We claim that every occurrence of X in Tc is prefixed by τ atleast k times. If not then
τ

τ

Tc −→
. . −→} X| .{zj times(34)

Nondeterministic Structure of Computation
..
.
◦

..
.

-◦

28
..

Q .
Q
6
?C
Q
s
Q
C
◦


3

C
B 
6
?B C
-◦
◦
C
AB C
6
B
-  A BC◦@A BCBNCW
I
@
RAU
@
@
•
◦
Fig. 4. An Infinite C-Graphfor some j < k. Assume that (34) was bisimulated byττ

τ.(τ.(. . . τ.(τ.X + τ.Υ1 ) + . . .) + τ.Υk−1 ) + τ.Υk |−→ .{z. . −→} Td
j 0 times

for some Td and some j 0 ≤ j such that
Td = X.

(35)

It is apparent that (35) is a contradiction. Either Td does not contain any occurrence of
X or every occurrence of X in Td is prefixed by at least one τ . In either case Td cannot
be equal to X. We conclude that if (33) is derivable from ACp then T 0 must be of theform µX.Tc such that the size of Tc is at least k. It follows from induction that (32) is
not provable in ACp .
Theorem 3 adds considerable weight to the system defined in Fig. 1. For further study
one could carry out an investigation of the system using the approach of Mendler andLüttgen (Mendler and Lüttgen2010).

5. Infinite State Computation
We take a look at infinite C-graphs in this section. Our first infinite C-graph is given in
Fig. 4. The reader might have noticed that this example is motivated by the sequenceΥ0 , Υ1 , Υ2 , . . .. Starting from the root, the computation can travel as high as it is necessary. Once it takes a horizontal move, it reaches a node whose number of descendants isfinite. Two distinct nodes on the left vertical chain are unequal since the one nearer tothe root can make a move to the right, which cannot be bisimulated by the other. The
nodes on the right vertical chain are pairwise distinct because they represent essentiallythe sequence Υ0 , Υ1 , Υ2 , . . .. A node on the left chain is unequal to a node on the rightchain for the reason that the former can engage in an infinite computation composedof nondeterministic steps whereas the latter cannot do that. As this example shows thenodes in an infinite C-graph can be classified into two categories, those that admit an
infinite sequence of nondeterministic computations and those that do not.

Mathematical Structures in Computer Science

29

f0

f1

f2

f3

f4

6

6

6

6

6

•

-◦

-◦

-◦

-◦

...

-

Fig. 5. Construction of a General Infinite C-Graph
Definition 21. A node in a C-graph is finite if the number of the nodes it can reachτ
is finite. The rank of a finite node N is the size of {N 0 | N =⇒ N 0 }. An infinite node
is a node that is not finite. A finite node is extremal if there is an arrow going from an
infinite node to the finite node.
The rank of a finite C-graph is the rank of its root. For example the rank of Υk is k foreach k ≥ 0.
Suppose i is an infinite C-graph. Let iω denote the subgraph of i consisting of all theinfinite nodes of i. The following lemma follows immediately from definition.
Lemma 6. Suppose i is an infinite C-graph. If none of the nodes of i has an infinite
number of outgoing edges pointing to extremal nodes, then every finite path in iω can beextended.
Proof. The assumption of the lemma simply says that iω is nonempty. The conclusionof the lemma follows from the fact that every infinite node has at least one child and allof its children in iω are infinite.
Obviously a finite branching infinite C-graph satisfies the property described in the abovelemma.
Can an infinite C-graph contain only a finite number of finite nodes? Before answering
the question we explain a general construction of an infinite C-graph demonstrated inFig. 5. Suppose f0 , f1 , f2 , . . . is an infinite sequence of finite C-graphs such that there isan infinite number of pairwise unequal finite C-graphs, each occurring only finitely often
in the sequence. Imagine that the k-th vertical arrow points to the root of fk . As it
stands, the diagram of Fig. 5 is an infinite D-graph. If we coerce all the equal nodes inthe D-graph we get an infinite C-graph. We need to argue that the nodes in the infinite
computation • → ◦ → ◦ → . . . do not shrink to finite nodes. For that purpose let’s namethese nodes N0 , N1 , N2 , N3 , . . .. For each i ≥ 0 the node Ni can reach some root of fj
that occurs a finite number of times in f0 , f1 , f2 , . . .. Let k be large enough such that fj
no longer appears in fk , fk+1 , fk+2 , . . .. Clearly Ni is not equal to Nk . If f0 , f1 , f2 , . . . are
pairwise distinct, then they are pairwise unequal according to Lemma 5. In this case thenodes in • → ◦ → ◦ → . . . are pairwise unequal. Once we know that • → ◦ → ◦ → . . .
does not shrink to a finite sequence, we immediately know that for each k ≥ 0 the node
Nk is not equal to any nodes in any of f0 , f1 , f2 , . . . since the former admits an infinite
nondeterministic computation whereas the latter does not.
Theorem 4. An infinite C-graph has an infinite number of extremal nodes.
Proof. Suppose towards a contradiction there is an infinite C-graph i containing a finite
number of extremal nodes. Then none of the nodes of i has an infinite number of outgoingNondeterministic Structure of Computation

30

edges pointing to the extremal nodes. It follows from Lemma 6 that every path of iω canbe extended to an infinitely long path from the root. Suppose the finite C-graphs rooted
by these extremal nodes are f1 , f2 , . . . , fk . Let’s say that fi , where 1 ≤ i ≤ k, belongs toιι
a node N of iω if there is a path N −→ . . . −→ N 0 in iω such that N 0 has an outgoingωωω
edge pointing to the root of fi . Now define the subgraphs iω
0 , i1 , . . . , ik of i successively
by the following induction:
ω— Let iω0 be i ;— For i ∈ {1, . . . , k}, if there is some node Ni in iω
i−1 to which fi does not belong, thenωω
ω
let ii be the subgraph of ii−1 rooted by Ni ; otherwise let iω
i be ii−1 .

By assumption iω
k is infinite. It is easy to see that the relation consisting of all the pairsωof the nodes of iω
k is a codivergent bisimulation. In other words all the nodes of ik are infact equal. This is a contradiction.
5.1. Definability
Let’s now turn to the issue of definability. Is the behavior of the infinite C-graph inFig. 4 definable in CCS? The answer is positive. Consider the process Centipeda defined
as follows:
Centipeda =(inc)(dec)(odd)(even)(Cp | Cnt | even.E | odd.O),

where
Cp = τ.Υ0 + τ.(τ.Υ1 + τ.(even | !even.inc.odd | !odd.inc.even)),
Cnt = inc.(d)(A(d) | d),(36)= dec.x + inc.(d)(A(d) | d.A(x)),

(37)

O

= µX.(τ.X + τ + dec.E),

(38)

E

= τ + τ.Ω + dec.O.

(39)

A(x)

The component Cp is the main process of Centipeda. It admits an infinite computation.
At each point of the infinite computation it may branch into a computational object equalto Υk for some k > 0. The part odd | !odd.inc.even | !even.inc.odd either increments thevalue of the one-time counter Cnt, or fires O or E depending on the parity of the current
value of Cnt. Once O (or E) has started, the counter can only decrements. The local
name dec is used to control the depth of the recursive calls of E and O. The recursive
definition given by (38) and (39) makes clear the relationship to (11) and (12).
Conceivably a C-graph of a computational nature is definable. In what follows wesubstantiate this intuition.
Definition 22. The number set n(g) of a C-graph g is defined as follows: A natural
number k is in n(g) if and only if there is an extremal node of g that is of rank k. A setof natural number is generated by an unobservable CCS process P , denoted by n(P ), if
it is the set n(c(P )).
The number sets of C-graphs do not really capture any nondeterminism. Nonethelessthey can be used to indicate the richness of the nondeterministic structures of C-graphs.

Mathematical Structures in Computer Science
f0

f1

f2

f3

31
f4

...

6
6
6
6
6
-◦ -◦ -◦ -◦ •
Fig. 6. Construction of a General Infinite Branching C-Graph
Theorem 5. Every recursively enumerable set containing zero is generated by an unobservable CCS process represented by a finitely branching C-graph.
Proof. Suppose R is a recursively enumerable set containing zero and χ is the partial
characteristic function of R. By definition x ∈ R if and only if χ(x) is defined and isequal to 1. Let G be the process given by the following parametric definitions.
G =(in)(end)(dec)(odd)(even)(f )(Reo | F | even.E | odd.O),Reo =(e)(o)(in.in.e | !e.in.o | !o.in.e | e.end.f.even | o.end.f.odd),

F=(out)(stop)(zero)Cχ (in, end, out, stop, dec, zero).f ,where E and O are defined in (38) and (39) respectively, and F is defined in terms ofthe general construction described on page 13. The role of Reo is to randomly generate anumber greater than one and record the parity of the number. The process F simulates
the calculation of the function χ. When the simulation terminates, it invokes either O
or E. Finally let Gr be either τ.Ω + τ.(τ.Υ1 + τ.G) or τ.Ω + τ.G, depending on whether
1 ∈ R or not. Clearly the process Gr generates the set R.
5.2. Infinite Branching C-GraphIf we coerce all the equal nodes of a finite branching infinite D-graph, we may get an
infinite branching C-graph. That is why a D-graph is not required to be finite branching.
A typical construction of a finite branching D-graph equivalent to an infinite branching
C-graph is described in Fig. 6. By the Computation Lemma all the nodes in •  ◦ 
◦  . . . are equal.
Theorem 6. There are infinite branching C-graphs definable in CCS.
Proof. Suppose {k0 , k1 , k2 , . . .} is a recursively enumerable set. Then there is a unary
total recursive function f such that the range of f is {k0 , k1 , k2 , . . .} and that for each j ≥ 0
there are infinite number of i’s such that f(i) = kj . Let F be (a)(b)Cf (in, end, out, zr, a, b),
where Cf (x, u, y, v, z, w) is the parametric definition introduced on page 13. Let Qng be(c)(c | !c.in.c | c.end). The process Qng is a quasi number generator since it may neverstop. Let Cq be the process
zr.Υ0 + out.(zr.Υ1 + out.(e)(o)(e | !e.dec.(zr.even+out.o) | !o.dec.(zr.odd+out.o))).
Finally the process F r is defined by(odd)(even)(dec)(out)(zr)(in)(end)(Qng | F | Cq | even.E | odd.O),
where O and E are defined in (38) and (39) respectively. The process F r does not reachany finite node before F performs any action. After F has done an action, the system

Nondeterministic Structure of Computation

32

turns into a state equal to Υki for some ki . Clearly F r generates the set {k0 , k1 , k2 , . . .}.
Let T r be the infinite path caused by Qng starting from the root of the D-graph of F r.
It follows from the assumption on f that for every i ≥ 0 and every node in T r there isa path from the node to the root of Υki consisting solely of deterministic computation
steps. Using the proof technique of Theorem 4, one can easily prove that all the nodes
in T r are equal. This says that the root of c(F r) points to the root of every graph inΥk0 , Υk1 , Υk2 , . . .. We conclude that the root of c(F r) is infinite branching.
The proof of the above theorem also implies the following result.
Theorem 7. Each recursively enumerable set is generated by an unobservable CCS
process.
6. Church-Turing Thesis and Nondeterminism
Do the unobservable processes defined in one model differ from those definable in anothermodel? More specifically is there a C-graph definable in the π-calculus (Milner, Parrow
and Walker 1992) that is not definable in CCS? It is tempting to start one’s investigation
by trying to answer the second question. It turns out however that the technique allowing one to answer the specific question also help answer the general question to one’s
satisfaction. The following theorem tells us that the unobservable processes definable in
one Turing-Milner model are definable in another Turing-Milner model.
Theorem 8. ∀M∈M.∀P ∈M.(P 6⇓ ⇒ ∃Q∈CCS.(Q6⇓ ∧ Q = P )).
Proof. Suppose M ∈ M. The relation CCS v M immediately implies that for each
unobservable CCS process P there is some unobservable M-process Q that is codivergent
bisimilar to P . We have the computable functions and the corresponding CCS processes
described below:— Let n be the unary computable function that, given the Gödel index of an unobservableτ
M-process P , outputs the number of the one-step computations of the form P −→ P 0 .
n
Let C (x, u, b, e, c, f ).A be obtained from the general construction defined on page 13.
— Let p be the binary function that, given a number i and the Gödel index of anunobservable M-process P , produces the Gödel index of the M-process P 0 such thatτP −→ P 0 is the i-th one-step computation of P . Let the CCS process
Cp (h1 , h2 , c, f, a, d, b+ , e+ , c, f ).A
be obtained from the general construction defined on page 13, where the pair h1 , h2
and the pair c, f are used to access the input numbers, a, d are used to deliver the
result, and b+ , e+ , c, f keep the input numbers.
— Let C0 (b+ , e+ ) be the CCS process whose sole function is to output the number ‘0’
at channels b+ , e+ .
— Let C+1 (b+ , e+ , b, e, h1 , h2 , b, e).g2 be the CCS process that increments the number
at channels b+ , e+ by one if the number stored at b+ , e+ is less than the number
stored at channels b, e, and then puts the result at channels h1 , h2 before firing A.
The number at channels b, e is kept unchanged.

Mathematical Structures in Computer Science33

Now the parametric definition S(x, u) is given by
S(x, u)=(becf )Cn (x, u, b, e, c, f ).(g)(g1 g2 )(h1 h2 )(b+ e+ )(g | g1 | C0 (b+ , e+ )| !g1 .C+1 (b+ , e+ , b, e, h1 , h2 , b, e).g2| !g2 .(ad)Cp (h1 , h2 , c, f, a, d, b+ , e+ , c, f ).g1 .g.S(a, d)).

Suppose k is the Gödel index of an M-process P . Let JkKzero
dec be the CCS encoding of thenumber k. The process S(dec, zero) in(dec)(zero)(JkKzero
dec | S(dec, zero))(40)

reads the number k at channels dec, zero, and then calculates the number i of P 0 suchτthat P −→ P 0 is a distinct transition. If i = 0 then the process halts. If i > 0 thenthe process executes the while-command defined by the two replication processes. In thej-th loop of the execution, where 0 < j ≤ i, the Gödel index kj of the j-th child of P iscalculated and stored at the local names a, d. By the end of the execution the following
situation occurs:(41)(g) g | (ad)(Jk1 Kda | g.S(a, d)) | . . . | (ad)(Jki Kda | g.S(a, d)) .
The computation from the process in (40) to the process in (41) is mainly arithmetical.
The two processes are equal. Clearly the CCS process in (41) has i transitions, simulating
all the one-step computations of the M-process P .
Theorem 8 should be interpreted as saying that, from the perspective of the ChurchTuring Thesis, the nondeterministic structure of computation is model independent. This
result tells us a number of things. Firstly if we want to study nondeterminism of computation, we may choose any Turing-Milner model without losing any generality. Secondly aTuring-Milner model differs from another Turing-Milner model in that they have different
sets of external actions. A model is more expressive than another if the external actionsof the former are more expressive than those of the latter. Finally the approach to define
the universal equality = and the universal expressiveness relation v in terms of internal
actions (computations) is justified. Theorem 8 can be seen as a formal justification ofDefinition 8 and Definition 11.
Our careful choice of the equality has paid off. The nondeterministic structures ofcomputations revealed by the absolute equality are rich, and at the same time remain
invariant in a general class of models. Such a theory is impossible had we used the weakbisimilarity or termination preserving weak bisimilarity. Weak bisimilarity identifies allcomputational objects. The termination preserving weak bisimilarity tells apart the threecomputational objects 0, Ω and τ.0 + τ.Ω, but identifies any other computational object
to one of the three.
Before ending this section we mention that investigations similar to those in Section 5
and this section have been carried out for effective operational semantics (de Simone
1984; de Simone 1985; Vaandrager 1993). Further studies are necessary to see if there isany connection between their work and the present work.

Nondeterministic Structure of Computation

34

7. RemarkOur understanding of the nondeterminism for both finite-state and infinite-state computations has been improved. There is an algorithm to check if a finite D-graph is a
C-graph, based on which one can design a brute force algorithm to enumerate all theelements of Fk for every k > 0. However we do not know any closed formula to calculate
the size of Fk at the moment. Although this is a problem belonging to enumerative combinatorics, trying to solve the problem will definitely improve our understanding of thefinite state computations. The problem of checking the equivalence of two unobservable
CCS processes is likely beyond the arithmetical hierarchy (Srba 2004a). Checking theequality between an unobservable CCS process and a finite C-graph poses a much lesshard challenge (Srba 2004b). A related problem is the regularity problem, which asks if
an unobservable CCS process is equal to some finite C-graph. Further study is necessary
to clear up these equivalence checking issues. A problem that deserves further investigation is a complete characterization of the C-graphs definable in Turing-Milner models.
In the light of Theorem 8, it is worth the effort to work out the answer to the question.
Acknowledgments
We thank Chaodong He for raising our interest in the unobservable processes. We also
thank the members of BASICS for their interest. We owe the two anonymous referees agreat deal. Their constructive criticisms and suggestions have helped improve the qualityof the paper considerably. The support from the National Natural Science Foundation ofChina (60873034, 61033002, 91318301) is gratefully acknowledged.

References
Abramsky, S. (1988) The Lazy Lambda Calculus. In D. Turner, editor, Declarative Programming,
Addison-Wesley, 65–116.
Aceto, L. and Hennessy, M. (1992) Termination, Deadlock, and Divergence. Journal of ACM,
39:147–187.
Baeten, J., Bergstra, J. and Klop, J. (1987) On the Consistency of Koomen’s Fair Abstraction
Rule. Theoretical Computer Science, 51:129–176.
Baeten, J. and Weijland, W. (1990) Process Algebra, Cambridge Tracts in Theoretical Computer
Science 18. CUP.
Barendregt, H. (1994) The Lambda Calculus: Its Syntax and Semantics. North-Holland.
Bloom, S. and Ésik, Z. (1994) Iteration Algebras of Finite State Process Behaviors.
Bloom, B., Istrail, S. and Meyer, A. (1995) Bisimulation Can’t be Traced. Journal of ACM,
42:232–268.
Busi, N., Gabbrielli, M. and Zavattaro, G. (2003) Replication vs Rcursive Definitions in Channel
Based Calculi. In Proc. ICALP’03, Lecture Notes in Computer Science 2719, 133–144.
Busi, N., Gabbrielli, M. and Zavattaro, G. (2004) Comparing Recursion, Replication and Iteration in Process Calculi. In Proc. ICALP’04, Lecture Notes in Computer Science 3142,
307–319.
Cai, X. and Fu, Y. (2011) The λ-Calculus in the π-Calculus. Mathematical Structure in Computer
Science, 21:943–996.

Mathematical Structures in Computer Science

35

Cardone, F. and Hindley, J. (2009) Lambda Calculus and Combinators in 20th Century. In
D. Gabbay and J. Woods, editors, Handbook of the History of Logic, Volume 5: Logic from
Russel to Church, Elsevier, 723–817.
Church, A. (1936) An Unsolvable Problem of Elementary Number Theory. American Journalof Mathematics, 58:345–363.
Cook, S. and Reckhow, R. (1973) Time Bounded Random Access Machines. Journal of Computerand System Science, 7:354–375.
Darondeau, P. (1990) Concurrency and Computability. In Semantics of Systems of Concurrent
Processes, Proceedings LITP Spring School on Theoretical Computer Science, Lecture Notes
in Computer Science 469, 223–238.
Davis, M. (1965) The Undecidable: Basic Papers on Undecidable Propositions, Unsolvable Problems and Computable Functions. Raven Press.
van Emde Boas, P. (1990) Machine Models and Simulations. In J. van Leeuwen, editor, Handbookof Theoretical Computer Science: Algorithm and Complexity, volume A, Elservier, 65–116.
Fu, Y. and Lu, H. (2010) On the Expressiveness of Interaction. Theoretical Computer Science,
411:1387–1451.
Fu, Y. (2012) Theory of Interaction.
Fu, Y. (2013) The Value-Passing Calculus. In Theories of Programming and Formal Methods,
Lecture Notes in Computer Science 8051, 166–195.
Giambiagi, P., Schneider, G. and Valencia, F. (2004) On the Expressiveness of Infinite Behavior
and Name Scoping in Process Calculi. In FOSSACS 2004, Lecture Notes in Computer Science
2987, 226–240.
van Glabbeek, R, Luttik, B. and Trčka, N. (2009) Branching Bisimilarity with Explicit Divergence. Fundamenta Informaticae, 93:371–392.
van Glabbeek, R. and Weijland, W. (1989) Branching Time and Abstraction in Bisimulation
Semantics. In Information Processing’89, North-Holland, 613–618.
Gödel, K. Über Formal Unentscheidbare Sätze der Principia Mathematica und Verwandter
Systeme. Monatshefte für Mathematik und Verwandter Systeme I, 38:173–198.
Hennessy, M. (1981) A Term Model for Synchronous Processes. Computation and Control,
51:58–75.
Hennessy, M. (1988) An Algebraic Theory of Processes. MIT Press, Cambridge, MA.
Hennessy, M. and Ingólfsdóttir, A. (1993) A Theory of Communicating Processes with ValuePassing. Information and Computation, 107:202–236.
Hennessy, M. and Lin, H. (1995) Symbolic Bisimulations. Theoretical Computer Science,
138:353–369.
Kleene, S. (1936) General Recursive Functions of Natural Numbers. Mathematicsche Annalen,
112:727–742.
Kleene, S. (1936) λ-Definablity and Recursiveness. Duke Mathematical Journal, 2:340–353.
Kleene, S. (1938) On Notation for Ordinal Numbers. Journal of Symbolic Logic, 3:150–155.
Kleene, S. (1952) Introduction to Metamathematics. Van Nostrand.
Kleene, S. (1981) Origin of Recursive Function Theory. Annals of the History of Computing,
3:52–67.
Lohrey, M., D’Argenio, P. and Hermanns, H. (2002) Axiomatising Divergence. In Proc. ICALP
2002, Lecture Notes in Computer Science 2380, 585–596.
Lohrey, M., D’Argenio, P. and Hermanns, H. (2005) Axiomatising Divergence. Information andComputatio, 203:115–144.
Markov, A. (1960) The Theory of Algorithms. American Mathematical Society Translations,series 2, 15:1–14.

Nondeterministic Structure of Computation

36

Mendler, M. and Lüttgen, G. (2010) Is Observational Congruence on µ-Expressions Axiomatisable in Equational Horn Logic? Informaiton and Computation, 208:634–651.
Milner, R. (1980) A Calculus of Communicating Systems. Lecture Notes in Computer Science,
92.
Milner, R. (1983) Calculi for Synchrony and Asynchrony. Theoretical Computer Science, 25:267–
310.
Milner, R. (1984) A Complete Inference System for a Class of Regular Behaviours. Journal ofComputer and System Science, 28:439–466.
Milner, R. (1989) Communication and Concurrency. Prentice Hall.
Milner, R. (1989) A Complete Axiomatization System for Observational Congruence of Finite
State Behaviours. Information and Computation, 81:227–247.
Milner, R. (1992) Functions as Processes. Mathematical Structures in Computer Science, 2:119–
146.
Milner, R. (1993) Elements of Interaction. Communication of ACM, 36:78–89.
Milner, R., Parrow, J. and Walker, D. (1992) A Calculus of Mobile Processes. Information andComputation, 100:1–40 (Part I), 41–77 (Part II), 1992.
Milner, R and Sangiorgi, D. (1992) Barbed Bisimulation. In Proc. ICALP’92, Lecture Notes in
Computer Science 623, 685–695.
Minsky, M. (1967) Computation: Finite and Infinite Machines. Prentice-Hall.
Park, D. (1981) Concurrency and Automata on Infinite Sequences. In Theoretical Computer
Science, Lecture Notes in Computer Science, 104:167–183.
Post, E. (1943) Formal Reduction of the General Combinatorial Decision Problem. American
Jounal of Mathematics, 65:197–215.
Priese, L. (1978) On the Concept of Simulation in Asynchronous, Concurrent Systems. Progress
in Cybernatics and Systems Research, 7:85–92.
Rogers, H. (1987) Theory of Recursive Functions and Effective Computability. MIT Press.
Sangiorgi, D. (2009) On the Origin of Bisimulation and Coinduction. Transactions on Programming Languages and Systems, 31(4).
Sangiorgi, D. and Walker, D. (2001) The π Calculus: A Theory of Mobile Processes. Cambridge
University Press.
Sewell, P. (1994) Bisimulation is not Finitely (First Order) Equationally Axiomatisable. In
Proc. LICS’94, IEEE, 62–70.
Sewell, P. Nonaxiomatisability of Equivalence Over Finite State Processes. Annals of Pure andApplied Logic, 90:163–191.
Shepherdson, J. and Sturgis, H. (1965) Computability and Recursive Functions. Journal of
Symbolic Logic, 32:1–63.
de Simone, R. (1984) On Meije and SCCS: Infinite Sum Operators vs. Non-Guarded Definitions.
Theoretical Computer Science, 30:133–138.
de Simone, R. (1985) Higher-Level Synchronising Devices in Meije-SCCS. Theoretical Computer
Science, 37:245–267.
Srba, J. (2004) Completeness Results for Undecidable Bisimilarity Problems. Electronic Notes
in Theoretical Computer Science, 98:5–19.
Srba, J. (2004) Roadmap of Infinite Results. In Formal Models and Semantics, II. World
Scientific Publishing Co..
Turing, A. (1936) On Computable Numbers, with an Application to the Entsheidungsproblem.
Proceedings of the London Mathematical Society, 42:230–265.
Turing, A. (1937) Computability and λ-Definability. Journal of Symbolic Logic, 2:153–163.

Mathematical Structures in Computer Science

37

Turing, A. (1937) On Computable Numbers, with an Application to the Entsheidungsproblem:
A Correction. Proceedings of the London Mathematical Society, 43:544–546.
Vaandrager, F. (1993) Expressiveness Results for Process Algebras. In Proceedings REX Workshop on Semantics: Foundations and Applications, Lecture Notes in Computer Science 666,
609–638.
Walker, D. (1990) Bisimulation and Divergence. Information and Computation, 85:202–241.
Wegener, I. (2005) Complexity Theory. Springer-Verlag.