COMPUTABLE CONCURRENT PROCESSES

YIANNIS N. MOSCHOVAKIS

Abstract. We study relative computability for processes and process transformations, in general, and in particular the non-deterministic and concurrent processes which can be specified in terms of various fair merge constructs. The main result is a normal form theorem for these (relatively) computable process functions which implies that although they can be very complex when viewed as classical set-functions, they are all “loosely implementable” in the sense of Park [17]. The precise results are about the player model of concurrency introduced in [13], which supports both fairness constructs and full recursion.

Consider the non-deterministic process^{1} C defined recursively by the equation

C = (0 or 1) ; C, (1)

where 0 and 1 stand for the acts of printing the corresponding digits, “ ; ” denotes sequential execution and “or” stands for unrestricted (random, autonomous) choice. Intuitively, an execution of C prints a 0 or a 1, at random, and then calls itself to repeat this, so “in the end” the trace of C produced by this sequence of random choices is (essentially) some infinite, binary sequence. We would like to call C a computable process, since it is defined by such an elementary recursion from the simple or construct, but this brings up a question: the traces of C are arbitrary binary sequences, most of them not individually computable.

Revised version, April 14, 1994. A preliminary version of these results was announced in the 1990 POPL meeting, [11].

The POPL announcement contained some additional material on the semantics of concurrent languages, whose proofs have been written up in [13].

During the preparation of this paper the author was partially supported by an NSF Grant.

1Terms like “process,” “execution,” “trace,” “fairness” etc. are used intuitively and vaguely in these introductory remarks. One of the main aims of “concurrency theory” is to supply rigorous definitions of these notions within a specific model, and we will review how this is done for our model in Section 1.

The same question arises more dramatically when we combine non-determinacy with interaction, as in the following classical example of Park [17]: set

P = X := 0 ; Y := 0 ; while(X = 0){X := 1 || Y := Y + 1}, (2)

where the parallel construct || is meant to be understood fairly, so that both of its process arguments will get as many chances to execute as they need. In fact, the simple assignment X := 1 needs only one chance, which must be given to it “at some point,” after which there is nothing more to be done and the process terminates. Thus—Park argues—the traces of P are all finite sequences of acts of the form

<X := 0, Y := 0, \underbrace{Y := Y + 1, …, Y := Y + 1}_{n−1}, X := 1>,

and any satisfactory semantics for such concurrent processes should entail this basic fact about P. Using Park’s fair-merge construct, we can also set

M = (\overline{0} || \overline{1}), (3)

where \overline{0} = <0, 0, … > and \overline{1} = <1, 1, … > are the constant infinite sequences. The traces of M are exactly the “fair” binary sequences, those with infinitely many 0s and infinitely many 1s, most of them, again, not individually computable. Still, we are tempted to say that M is a computable process, relative to the fair merge construct.

Park [17] was responding to Dijkstra [5], who advocated banning definitions like (2) and (3) from programming because they involve unbounded non-determinism— which “cannot be implemented”—and he argued that in discussing implementability issues we should understand non-deterministic and concurrent definitions of this type loosely:

No-one requires of a correct implementation for parallelism that there be an appropriate sense in which all scheduling algorithms be possible in it, only that there be one such scheduling algorithm, and if fairness be required that the scheduler be fair.

So we can claim that C and M are implementable since the computable, alternating sequence of 0s and 1s is a trace of both of them. Now the existence of implementations is obviously important, but it will hardly do as a sole criterion for computability: no-one would call an arbitrary set of infinite binary sequences computable simply because it may happen to have a computable member. If there is a natural concept of computable process, then it must involve more than the mere existence of a computable trace.

At the same time, we cannot profitably interpret the definitions of C or M so that they only have computable traces, we truly need all their traces, if we are to gain anything from allowing unrestricted choice or fair merging among our primitive programming constructs. When we call M from within some program E, we are simply specifying that a fair, binary sequence should be produced; and in proving properties of E, all we can assume is that the sequence produced will be fair, not that it is also computable, as it may well be that some piece of hardware is doing the merging, non-computably. In fact, we tend to call non-deterministic processes like C, P and M “computable” primarily because they are defined in terms of simple and intuitive programming constructs. The fact that they have computable traces should be a formal consequence of such definitions (however trivial for these examples) and not the basic reason for thinking them computable.

The main aim of this paper is to define rigorously and establish some basic facts about computable processes and computable process functions, in the context of the game-theoretic modeling of concurrent, asynchronous systems introduced in [13]. We will characterize these objects in the cases where we take as given unrestricted choice, the full (unfair) merge, the fair merge in the sense of Park (as above) and the richer state-dependent fair merge which is most natural in the context of our concurrency theory. The main result is that the processes which are computable relative to these constructs are all “loosely implementable” in the sense of Park, although their sets of traces can be extremely complex; it is a corollary of a Normal Form Theorem for computable processes and process functions, which also implies that these notions are very robust and provides some considerable justification for our choice of definitions.

There are two important notions in the player model of concurrency introduced in [13], the players which model concurrent processes and the implemented player functions (ipfs) which represent process transformations. After a brief review of these notions in Section 1 and a briefer comparison of the player model with other modelings of concurrency, we will define process computability and state rigorously our results in Section 2. These sections can be read with only a fair acquaintance of Sections 1-4 and 6 of [13], but the proofs, in the remaining two sections, depend heavily on the technical machinery developed in [13].

1. The player and other models of concurrency

A useful tool for defining the player model and comparing it with other modelings of concurrency is the following, simple formal language.^{2}

1.1. The expressions (terms) of FLR_{0}(τ) are defined inductively by

E ::≡ x | f(E_{1}, …, E_{n}) | rec(x_{1}, …, x_{n})[E_{0}, …, E_{n}],

2This was called L in [13]. FLR_{0} is the equational (or “propositional”) part of FLR, the Formal Language of Recursion introduced in [12]. There is also an intermediate language FLR_{1}, which comes from FLR by dropping the conditional but retaining value passing and functional recursion, and which plays for recursion the role that the first order predicate calculus plays for explicit definability.

where x is any variable (from a fixed, infinite set), f is any function symbol (from a fixed vocabulary τ of function symbols, each with an assigned, non-negative arity) and a more familiar notation for the mutual recursion construct is

E_{0} where {x_{1} = E_{1}, …, E_{n}}.

FLR_{0} is an abstract version of several languages which have been used to study concurrency, including Hoare’s Communicating Sequential Processes (CSP) [7], Milner’s Calculus of Communicating Systems (CCS) [9], the metric approach of de Bakker-Zucker [4] and the reactive processes of Manna-Pnueli [8]. The idea is that a particular model can be made precise and compared to other models by giving rigorous semantics for FLR_{0}(τ), with some specific vocabulary τ. Most of these languages include some or all of the following function symbols, in common, infix notation and with their intended, intuitive meaning:

skip  Skip, or idle.
a  Act execution.
ax  Act prefixing.
x; y  Sequential execution.
if R then x else y Conditional execution.
x or y  Autonomous choice.
x || y  Merge.

The act symbols are from some fixed set A (sometimes endowed with additional structure) and the conditionals are often described by an auxiliary language of “conditions” (on some assumed “state”). When included, the merge operation is sometimes interpreted by the full (unfair) rather than the fair merge. In addition, most theories include special functions to model the interaction (or synchronization) of processes, which is the heart of the problem of modeling concurrency. There is no single, special construct for interaction in the player model, the ability to interact is, in some sense, built into the very definition of “process,” and it is controlled by a typing mechanism for interaction.

In [13] we defined three kinds of FLR_{0}(τ) semantics, for structures of the form

(4) 𝔄 = (S, I) = (States, ι, Acts, skip, exec, I),

where S = (States, ι, Acts, skip, exec) is the state structure of 𝔄 and I is a set of “functions” which distinguishes the semantics. About S we assume the following: States is an arbitrary set of states containing the initial state ι; Acts is an arbitrary set of atomic acts containing the “delay” act skip; every act a induces a function s ↦ sa = exec(s, a) on the states, such that s skip = s; and every state s is accessible by a sequence of acts a_{1}, …, a_{n} from ι, i.e. s = a_{1}a_{2} ⋯ a_{n}ι. A state structure S is trivial if its only member is ι, in which case we can identify it with the set of its acts. We summarize briefly and comment on each of these interpretations.

I  s_{0}  s_{1}  s_{2}  ⋯  s_{n}
II (a_{0}, ∂) (a_{1}, ∂) (a_{2}, ∂) ⋯ (a_{n}, t)
State: ι s_{0}a_{0}  s_{1}a_{1}  s_{2}a_{2} ⋯ n_{3}a_{n}

Figure 1. The interaction game; a terminating run.

1.2. Input-dependent, deterministic processes. A procedure (or input dependent stream, [13, 2.4-2.8]) on S is a function α : States → Streams(Acts) which assigns to each state a stream of acts. These are the natural denotations of programs which read the state just once (presumably to get input) and then execute a stream of acts in total isolation from the environment. The set Π = Π(S) of procedures over S is a directed, complete poset (dcpo) and in a procedure structure (S, I) for FLR_{0}(τ), I assigns to each n-ary function symbol f of the vocabulary τ a continuous, n-ary function I(f) : Π^{n} → Π. To interpret FLR_{0}(τ) on (S, I), we let the variables range over procedures and we use composition and least-fixed-point recursion to associate with each expression E and each sequence x⃗ of variables (which includes all the free variables of E) an n-ary procedure function

procedure(𝔄, x⃗)E = ϕ_{E} : Π^{n} → Π.

Two expressions E and M are procedure equivalent if for all procedure structures, ϕ_{E} = ϕ_{M}. There are obvious, procedure interpretations of act execution, act prefixing and sequential and conditional execution, [13, 2.7]

In a trivial state structure, procedures stand for totally isolated programs which cannot interact at all with one another. If the state is non-trivial, then the sequential execution α; β affords some minimal communication at the entry and exit stages, because if α(s) terminates after executing the acts a_{1}, …, a_{n}, then (after these acts) (α; β)(s) executes the stream β(a_{1}a_{2} ⋯ a_{n}s) which may depend on a_{1}, …, a_{n}.

1.3. Interactive, deterministic processes. A behavior (or state dependent stream of acts) is a partial strategy for II in the interaction game pictured in Figure 1, formally a partial function

(5) σ : States^{⋆} ⇀ Acts × {∂, t}

on non-empty sequences of states, except that we identify behaviors which agree on all partial runs of the game, [13, Section 3]. Player II represents in this game the denotation of some deterministic, interactive program, which responds (if defined) to each state s_{n} played by I with an act a_{n} and either the indicator ∂, meaning that more moves are needed, or t, signifying successful termination; player I represents “the rest of the world,” the collective action of all the other agents operating in the same environment. The set B = B(S) of behaviors is a dcpo. An n-ary behavior function is any continuous F : B^{n} → B, and a behavior structure 𝔄 = (S, I) is one where I assigns behavior functions (of the appropriate arity) to the function symbols. The behavior semantics of such a structure interpret recursion by the taking of least fixed points, and they associate with each expression E and each list of variables x⃗ which includes all the free variables of E, a behavior function

behavior(𝔄, x⃗)E = F_{E} : B^{n} → B,

the behavior denotation of E. Two expressions E and M are behavior equivalent if F_{E} = F_{M} on every behavior structure.

Behaviors are the natural denotations of deterministic, interactive programs and several examples of them are worked out in [13, Section 3], including act execution and prefixing, sequential and conditional execution and the handling of interrupts. It is also claimed in [13, Theorem 3.7] that procedure equivalence coincides with behavior equivalence for FLR_{0} expressions; the proof of this is quite simple.

1.4. Interaction through the state vs. message passing. Among actual, interactive systems, there is an important difference between those with a common, central memory which can be accessed by all the processes, and those in which communication can only take place by the passing of messages through private channels. Our notion of behavior might suggest that the player model can only handle efficiently central-memory interaction, but this is not true. Suppose, for example, that the process x can only execute acts in some set K ⊊ Acts, the process y can only “see” changes in the state which are produced by the execution of acts in K, and no other process can either execute acts in K or discern changes in the state produced by the execution of acts in K; we might then reasonably call K a private, one way channel of communication from x to y. There is a natural notion of behavior type for processes which provides a flexible mechanism for introducing and keeping track of such restrictions and by which we can easily represent in the player model a local state interaction through message-passing, [13, 4.3-4.7,8.2]. See also [13, 3.6] for some remarks on the representation of concurrent systems by the game of interaction.

1.5. Traces of behaviors. If ω is a (total) strategy for player I and σ ∈ B, then

ω ∗ σ = a_{0}, a_{1}, … (6)

is the stream of acts “executed” (by player II) in the run of the game where I plays by ω and II responds by σ—terminated with t if II ever plays (a_{n}, t). The trace of σ is the set of all these streams,

(7) trace(σ) = {ω ∗ σ ||| ω is a strategy for I}.

If, for example

σ(<s_{0}>) = (a, ∂),
σ(<s_{0}, s_{1}>) = if R(s_{1}) then (b, t) else (c, t),

(8) then trace(σ) = {<a, b, t>, <a, c, t>} is a doubleton and an “observer” who is simply recording the acts executed by σ (in repeated experiments) without knowing the state structure or the relation R may well consider σ a non-deterministic process.

1.6. Concurrent processes. A player on a state structure S is any non-empty set of behaviors, and we set

P(S) = P = {x ||| ∅ ≠ x ⊆ B(S)}; (9)

this is the set by which we model the non-deterministic, interactive processes on S. Intuitively, a player x can “play” (interact with the world, be implemented by) any of its “behaviors,” i.e. any σ ∈ x. A player x is deterministic if it is a singleton x = {σ} and total if every σ ∈ x is a totally defined strategy. For example, for each act a

a^{ȷ} = {λ(<s_{0}, …, s_{n}>)(a, t)} (10)

is the total, deterministic player who (confronted by any state) executes a and quits. The trace of a player is the union of the traces of its behaviors,

trace(x) = ⋃{trace(σ) ||| σ ∈ x}
= {ω ∗ σ ||| σ ∈ x, ω is a strategy for I}.

(11)

Now P is not a dcpo in any natural way, so it is not immediate how to model process transformations by functions which have fixed points. Before dealing with this, notice that each behavior function F : B^{n} → B induces naturally a (set) function F^{ȷ} : P^{n} → P by “distribution,”

F^{ȷ}(x_{1}, …, x_{n}) = {F (σ_{1}, …, σ_{n}) ||| σ_{1} ∈ x_{1}, …, σ_{n} ∈ x_{n}}; (12)

for example (and skipping the ^{ȷ}),

x; y = {σ; τ ||| σ ∈ x, τ ∈ y},
if R then x else y = {if R then σ else τ ||| σ ∈ x, τ ∈ y}
= {F_{R}(σ, τ) ||| σ ∈ x, τ ∈ y},

where for each σ and τ,

F_{R}(σ, τ) = λ(<s_{0}, …, s_{n}>)if R(s_{0}) then σ(<s_{0}, …, s_{n}>) else τ(<s_{0}, …, s_{n}>).

These liftups are deterministic player functions, in the sense that when applied to deterministic arguments (singletons) they yield deterministic values. Typical non-deterministic functions on P include

(13)  x or y = x ∪ y,
(14)  x + y = {if R then σ else τ ||| σ ∈ x, τ ∈ y, R ⊆ States},

which represent two distinct ways of modeling choice. Notice here that for all players x, y, easily,

trace(x + y) = trace(x or y) = trace(x) ∪ trace(y), but in general, (x or y) ≠ (x + y), in fact

a^{ȷ} or b^{ȷ} ≠ a^{ȷ} + b^{ȷ}

if a and b are distinct acts and the state structure is non-trivial: because if R(s) is true for some state and false for some other, then the state-dependent strategy

σ(s_{0}) = if R(s_{0}) then (a, t) else (b, t)

is a behavior of a^{ȷ} + b^{ȷ} but not of a^{ȷ} or b^{ȷ}. For the same reason,

a^{ȷ}; (b^{ȷ} + c^{ȷ}) ≠ a^{ȷ}; b^{ȷ} + a^{ȷ}; c^{ȷ} (15)

for distinct acts in a non-trivial state structure, although these two players have the same traces. Thus, a non-deterministic player is not determined by its trace.

1.7. Modeling process transformations. One of the basic premises of [13] is that a function f : P → P models a process transformation if it is determined by its “implementations,” and one is tempted (at first) to consider only the linear implementations of f, i.e. the continuous F : B → B such that

σ ∈ x ⟹ F (σ) ∈ f(x).

But if the recursive definition (with a parameter)

y = x; y, (16)

makes sense (as it should), we would expect it to define the process transformation

y(x) = {σ_{0} ; σ_{1} ; ⋯ ||| σ_{0}, σ_{1}, … ∈ x}

and the most natural implementation of y(x) is the “infinitary” continuous operation

Y (σ_{0}, σ_{1}, σ_{2}, …) = σ_{0} ; σ_{1} ; σ_{2} · · · .

In general, an (infinitary) behavior function (of n arguments) is any continuous operation

F : (N → B)^{n} → B, (N = {0, 1, … }),

and we call F an abstract implementation of a function

f : P^{n} → P

if for every n-tuple of players x⃗ = x_{1}, …, x_{n} and sequences of behaviors p⃗ = p_{1}, …, p_{n},

p_{1} : N → x_{1}, …, p_{n} : N → x_{n} ⟹ F (p⃗) ∈ f(x⃗).

A function f : P^{n} → P is implementable if there exists some set I of abstract implementations which determines its values, i.e.

f(x⃗) = {F (p⃗) ||| p_{1} : N → x_{1}, …, p_{n} : N → x_{n}, F ∈ I}. (17)

The second basic premise of [13] is that the correct way to model process transformations is to forget the extensional “implementable” and use the intensional

I  s_{0}  s_{1}  s_{2}  s_{3}  s_{4}
μ :  1  0  1  1  0
μ[σ_{0}, σ_{1}] : II σ_{1}(s_{0}) σ_{0}(s_{1}) σ_{1}(s_{0}, s_{2}) σ_{1}(s_{0}, s_{2}, s_{3}) σ_{0}(s_{1}, s_{4})

Figure 2. Action of binary merger.

“implemented”, [13, Section 7]: an n-ary implemented player function (ipf) is^{3} any set f of n-ary abstract implementations which is closed under a suitable reducibility relation, [13, 7.2-7.4]; and the (player) value of f is given by

f(x⃗) = {F (p⃗) ||| p_{1} : N → x_{1}, …, p_{n} : N → x_{n}, F ∈ f}.

A set I ⊆ f generates an ipf f, if

(18) f = [I] = {F ||| F is reducible to some G ∈ I},

i.e. if f is the closure of I under reducibility. It can be verified that every set I which generates f determines the values of f by (17), [13, 7.3]. Most often we define ipfs by specifying a simple generating set for them. For example, for each behavior function F : B^{n} → B, we let

F^{ȷ} = [F^{∗}], with F^{∗}(p_{1}, …, p_{n}) = F (p_{1}(0), …, p_{n}(0)), (19)

the notation chosen because this F^{ȷ} indeed satisfies (12). Similarly,

or = [F_{l}, F_{r}], with F_{l}(p, q) = p(0), F_{r}(p, q) = q(0), (20)

is the ipf version of autonomous choice, easily satisfying

x or y = {F_{l}(p, q) ||| p : N → x, q : N → y} ∪ {F_{r}(p, q) ||| p : N → x, q : N → y}

A similar modeling can be given for x + y as an ipf, but now we need an infinite generating set, all the conditionals. An ipf is deterministic if it is generated by a single behavior function F_{0}, as each F^{ȷ} is but or is not.

1.8. Merge operations. A merger on a process structure 𝔄 is any (total) function μ : States^{⋆} → {0, 1} on non-empty sequences of states to {0, 1}. Given behaviors σ_{0}, σ_{1} in 𝔄, μ[σ_{0}, σ_{1}] is the (conjunctive) merged behavior of σ_{0}, σ_{1}, defined (roughly) by decreeing that in a certain stage of the game it calls σ_{0} or σ_{1} accordingly as μ gives the value 0 or 1. Rather than give the formal definition which is somewhat technical, we indicate in Figure 2 the first few moves of the play by μ[σ_{0}, σ_{1}] for given values of μ; see also [13, 3.3]. (The picture does not indicate that if some σ_{i} first plays some (a_{n}, t) when it is called, then from that stage on μ[σ_{0}, σ_{1}] calls the other behavior σ_{1−i} independently of the value of μ.) A merger μ is state independent if its values depend only on the stage of the game and not what has been played, i.e. for some ν : N → {0, 1} and all sequences of states,

3An ipf “is” a set of abstract implementations in the same sense that a function “is” a set of ordered pairs—i.e. this is the way by which we represent these objects within set theory.

μ(<s_{0}, …, s_{n}>) = ν(n);

a merger μ is fair if for every σ_{0}, σ_{1} and every infinite run of the game by μ[σ_{0}, σ_{1}], each σ_{i} either plays some (a_{n}, t) at some stage when it is called, or is called infinitely often.

We define the (full, unfair) merge, the parkmerge and the fairmerge operations by the equations

merge(x, y) = {μ[p(0), q(0)] ||| p : N → x, q : N → y,

μ any merger},

parkmerge(x, y) = {μ[p(0), q(0)] ||| p : N → x, q : N → y,

μ any fair, state-independent merger},

fairmerge(x, y) = {μ[p(0), q(0)] ||| p : N → x, q : N → y,

μ any fair merger}.

Of course, we read these equations as definitions of ipfs (sets of abstract implementations), so that (for example) merge is the ipf generated by all

F_{μ}(p, q) = μ[p(0), q(0)], (μ any merger),

and its abstract implementations are precisely all functions of the form

F_{μ,k,l}(p, q) = μ[p(k), q(l)], (k, l ∈ N, μ any merger).

We use the name parkmerge for Park’s fairmerge, his terminology being more appropriate in our context for the full, state dependent fair merge operation.

In concrete modelings of concurrency closer to applications, the state structure is taken to be quite specific (typically determined by variables, stacks and buffers), and it is possible to define a large variety of “fair merge operations,” see Francez [6] and Manna-Pnueli [8]. It should be clear from this discussion that these operations can all be “represented faithfully” by ipfs: this is what we mean when we say that the player model supports fairness.

1.9. The player model. We represent processes over a state structure S by players and process functions by ipfs, and to keep the language less stilted we will use the more familiar terms from now on,

process = player, process transformation = ipf,

except where we need to emphasize the special properties of the player model. A process structure for FLR_{0}(τ) is a pair 𝔄 = (S, I), where the interpretation I assigns ipfs to the function symbols in τ.

The most substantial contribution of [13, Section 8] is a method for solving recursion equations of the form (a) x = f(x)

(b) y = g(x, y), where f and g are given process functions; the solution of (a) is a process, that of (b) a process function, and the method also solves similar systems of mutual recursion. Using this ipf recursion to interpret the rec construct and a a natural notion of ipf composition, we assign to each FLR_{0}(τ) expression E and each list of n variables x⃗ which includes all the free variables of E, a process function f_{E}; closed expressions are assigned processes. We call E and M process equivalent if f_{E} = f_{M} on every process structure.

The main result of [13, Sections 8-10] is that for FLR_{0} expressions, process equivalence coincides with behavior equivalence, and hence also with procedure equivalence. In effect, with this modeling of interaction and concurrency, the logic of concurrent recursion is the same as the logic of deterministic, interactive recursion, or even deterministic, non-interactive recursion^{4}: this is what we mean when we say that the player model supports full recursion.

1.10. Other modelings. The main—and characteristic—feature of the player model is that it supports both fairness and full recursion. Modelings like Hoare’s CSP and Milner’s CCS, whose primary semantics are operational do not support fairness, and the same is true of axiomatic and algebraic approaches; where fairness is included, on the other hand, as in Manna-Pnueli [8], full recursion is weakened to iteration (“while” looping), and Park [17] already gives a simple model which supports both fairness and iteration. Many models have also been proposed which do not support either fairness or full recursion, e.g. the “metric space” models of de Backer-Zucker [4].^{5}

In the joint paper [14] with Glen Whitney, we generalize the construction of [13] to define a player model ipf(D) over an arbitrary dcpo D, we define an abstract notion of powerstructure which covers many models of concurrency and makes it possible to compare them, and we show that if D is a profinite dcpo, then the Plotkin [19] powerdomain over D together with the set-monotone continuous functions on it is a quotient of a substructure of ipf(D). Whitney has obtained similar “embedding” results for the Hoare and Smyth powerdomains, [21].

4In fact the FLR_{0}-identities which are valid in process structures are exactly those which are valid in all domain structures (D, I), where D is a dcpo, I interprets the function symbols by continuous functions on D and the recursion construct is interpreted by the taking of least-fixed-points. This is a joint result with Tonny Hurkens, based on a simple axiomatization of the logic of recursive equations, which also proves the decidability and substantial robustness of this class of identities and relates this work to earlier results on recursive program schemes, trees and networks, see [3].

5“Guarded” recursion in the de Bakker-Zucker model obeys the laws of least-fixed-point recursion, [15], but this is apparently not true for unguarded (continuous) recursion. The suggestion in [4, 3.5] that (in effect) every recursion be made guarded “by definition” is not serious: in our notation, it assigns to x = a; x the solution <skip, a, skip, a ⋯ >, which does not satisfy the equation it is supposed to solve!

1.11. Intensionality in the player model. The fact that a player is not determined by its traces in 1.6 exhibits some intensionality in our modeling of processes. This is quite common in many modelings of concurrency, e.g. both the strong and the weak bisimulation models of Milner’s CCS [9] yield a notion of process (agent) which is not determined by its traces. What may be peculiar to the player model, is that process transformations are also modeled by intensional functions which are not completely determined by their values. It appears that this is necessary,^{6} but it also adds some unexpected “expressibility” to the model. The following example may help illustrate some of the subtleties involved.

Suppose that the structure 𝔄 = (S, I) has a countable number of states which we identify with the integers, and consider the following two (infinitary) behavior functions F and G on 𝔄:

F (p)(<s_{0}, …, s_{n}>) ≃ \{ \begin{matrix}(skip, ∂), if n = 0, \\ p(0)(<s_{1}, …, s_{n}>), otherwise, \end{matrix}
G(p)(<s_{0}, …, s_{n}>) ≃ \{ \begin{matrix}(skip, ∂), if n = 0, \\ p(s_{0})(<s_{1}, …, s_{n}>), otherwise. \end{matrix}

Let f = [F] and g = [G] be the process functions generated by F and G. It is quite obvious that these are extensionally equal, in fact for all processes x,

g(x) = f(x) = skip ; x.

Viewed intensionally as sets of implementations, however, f ⊂ g but f ≠ g, because G(p)(<s_{0}, s_{1}>) depends on s_{0} while F (p) does not, and it is easy to see that “reducibility preserves state independence.” Now what is the difference between the (intuitively understood) “process transformations” modeled by these two distinct mathematical objects? It appears that the best we can describe them is as follows:

f(x): Given x, call some behavior σ ∈ x and then: to the first state s_{0} respond by skip and after that follow σ.

g(x): Given x: to the first state s_{0} respond by skip, then call some behavior σ ∈ x and after that follow σ.

We have used “infinitary” behavior functions to capture the fact that implementations may “get access” to distinct behaviors on different “calls” to non-deterministic arguments, and we have imposed closure under reducibility to insure that process functions treat their arguments as sets rather than sequences of behaviors. The example makes it clear, however, that the modeling forces the incorporation of some aspects of the “timing” of “calls” (and their consequent, possible dependence on the state) into the modeling. It is not clear now just what role this distinction f ≠ g plays in the modeling, but we will see in Section 3 that it is quite important.

6In his Ph.D. Thesis [22], Glen Whitney has answered Question [13, 9.7] by constructing an example of two extensionally equal, unary ipfs with distinct ipf fixed points; he has constructed an extensional model which supports fairness and satisfies the “minimum conditions” for a model of concurrency listed in of [13, 6.1]—and quite a bit more; and he has shown that there is no extensional model which further satisfies some simple, natural properties of the player model.

2. Definitions and results

Definition 2.1. A process function f on a structure 𝔄 is computable, if it is definable on 𝔄 by some expression E of FLR_{0}, i.e. f = f_{E} in the sense of the process semantics of 𝔄 to which we alluded above.

Since we are interested in characterizing the computability of “true” (non-deter-ministic) process functions like the fair merge, we will factor out the mundanely computable behavior functions by means of the following definition.

Definition 2.2. A behavior structure 𝔄 as in (4) is manageable, complete if there exist fixed, non-repetitive enumerations of its (countably) infinite set of states and (possibly finite) set of acts

States = {S_{0}, S_{1}, … }, Acts = {A_{0}, A_{1}, … },

so that the following conditions hold:

(1) There is a fixed recursive partial function exec : N × N ⇀ N such that exec(i, j) is defined when A_{j} is an act and

S_{i}A_{j} ≃ Sexec(i, j).

(2) For each state s, there are infinitely many distinct states which are accessible from s.

(3) Every (classical) recursive behavior function is computable in 𝔄.

The first two of these hypotheses certainly hold in the standard example where the state is a finite (or effectively enumerable) store of variables, stacks and buffers and the acts include assignments to integer variables. They allow us to “identify” (code) states and acts with integers, but also (using standard recursive codings) to identify finite sequences of states with integers, behaviors with (special) partial functions on N to N, etc. Thus we can talk about recursive behavior functions in the third hypothesis, meaning recursive functionals which take partial functions as arguments and values, and these certainly include act execution, sequential execution, conditionals based on recursive conditions on the state, etc. Precise definitions will be given in Section 3.^{7}

We will characterize computability in expanded structures of the form (𝔄, F^{∗}), obtained by adding to a manageable, complete behavior structure 𝔄 some set F^{∗} of process functions, e.g. the various merges. Formally we should write (𝔄^{ȷ}, F^{∗}), where 𝔄^{ȷ} is the process structure obtained by replacing each behavior function F in 𝔄 by its liftup F^{ȷ} defined in (19), but [13, Theorem 8.9] implies that the distinction is only notational.

If F is a monotone, continuous operation of the type

F : (N → B)^{n} × (N → N) → B, (21)

then for each δ ∈ (N → N), the δ-section F_{δ} : (N → B)^{n} → B of F is the infinitary behavior function of n arguments defined by fixing δ in F,

F_{δ}(p_{1}, …, p_{n}) = F (p_{1}, …, p_{n}, δ). (22)

Definition 2.3. A process function f is defined recursively from a set O of total, number-theoretic functions, if there exists a recursive function F as in (21) such that f is generated by the δ-sections of F with δ ∈ O, i.e. f = [{F_{δ} ||| δ ∈ O}].

Notice that if f is defined recursively from O via the recursive function F, then its values are given by

f(x⃗) = {F (p⃗, δ) ||| p_{1} : N → x_{1}, …, p_{n} : N → x_{n}, δ ∈ O},

i.e. intuitively, we can compute a value of f(x⃗) if we are “given” arbitrary calls to behaviors in the process arguments and an “oracle” δ ∈ O. The definition makes sense for functions with 0 arguments, i.e. processes: a process x is defined recursively from the set of oracles O if there is a recursive F : (N → N) → B such that

x = {F (δ) ||| δ ∈ O}. (23)

Theorem 2.4. Main Result. Fix a manageable, complete behavior structure 𝔄.

(1) The computable process functions of (𝔄, merge) are the same as the computable process functions of (𝔄, or); they are the same as the computable process functions of (𝔄, +); and they are precisely the process functions defined recursively from the Cantor set C = (N → {0, 1}).

7We want to avoid technical issues of abstract recursion and language design here. It is quite routine to turn the third hypothesis into a theorem, by enriching the language with a few simple, natural constructs.

(2) A process function f is computable in the expansion (𝔄, parkmerge) if and only if f is defined recursively from the full Baire space N = (N → N).

(3) A process function f is computable in the expansion (𝔄, fairmerge) if and only if it is defined recursively from the set of (codes of) wellfounded trees

WF = \{δ ∈ C ||| (∀α : N → N)(∃n)[δ(\overline{α}(n)) = 1]\}, (24)

where \overline{α}(n) is the integer code of the finite sequence (α(0), …, α(n − 1)).

(4) In each of these cases the set of computable process functions does not change if we further expand the structure by functions which are defined recursively from the specified set of oracles.

(5) For each of the structures in (1)–(3), every computable process function has a recursive abstract implementation and every computable process contains a recursive behavior. ⊣

It is easiest to read off some of the consequences of this theorem for the case of total processes, which may be identified with subsets of the Baire space N since all their members are totally defined behaviors. Recall the logical classification of analytical subsets of Baire space by how many and what kind of quantifiers we need to define them beginning with a recursive relation R, cf. [16, 10]. In this summary table of definitions, i varies over N and Greek letters vary over the Baire space N:

\begin{aligned}Π_{1}^{0} & δ ∈ x & ⟺ & (∀i)R(δ, i) \\ Σ_{1}^{1} & δ ∈ x & ⟺ & (∃α)(∀i)R(δ, α, i) \\ Σ_{2}^{1} & δ ∈ x & ⟺ & (∃α)(∀β)(∃i)R(δ, α, β, i) \end{aligned}

The dual classes to these are defined by taking the negations of these forms and they are denoted by interchanging Σ and Π, e.g. the class of complements of Π_{1}^{0} sets is Σ_{1}^{0}. It is known that each of these classes is proper, i.e. none of them is included in its dual.

We will characterize the total processes computable in the full (unfair) merge in terms of a natural notion of “observables” of processes.

Definition 2.5. A direct observable of a behavior σ is a finite sequence

obs = s_{0}, σ(<s_{0}>), s_{1}, σ(<s_{0}, s_{1}>), …, s_{n}, σ(<s_{0}, …, s_{n}>) (25)

which is a legal initial part of the game of interaction, i.e. all the terms of the sequence are defined and I’s partial play <s_{0}, …, s_{n}> satisfies the condition of accessibility. An ideal observable of σ is any finite set of its direct observables.

The direct and ideal observables of a process x are the direct and ideal observables of the behaviors of x.

2.6. Observability and initial non-determinism. The direct observables of a player x are the “finite” facts about x that we can learn by direct “experimentation” or “testing”, assuming that we have full control of the state: we adopt the role of player I in the interaction game, start with some s_{0}, x (perhaps) responds with some (a_{0}, ∂), we choose some s_{1}, etc. If the game goes on for n + 1 turns, we have at the end an observable of x as in (25), where σ is the behavior followed by x in this run; this is because by our understanding of “initial non-determinism,” x “chose” a fixed behavior σ at the start of this run and he will follow it until the game ends (σ(<s_{0}, …, s_{n}>) = (a_{n}, t)) or hangs ((σ(<s_{0}, …, s_{n}>) = ⊥). The ideal observables may also be viewed as facts about x which can be learned by testing, but we must be allowed some questionable “backtracking” (or “undoing”) moves in the game, where (playing as I) we can “change our mind,” take back a state s_{i} and replace it by s′_{i} after recording x’s response to s_{i}—while x is not allowed to switch behaviors. We will not analyze here any further the various notions of observational equivalence between players and their relation to the extensive literature on this notion in process theory.

Each ideal observable of a behavior σ is (essentially) the restriction σ ↾ Δ of σ to a finite set Δ of sequences of states which is closed under initial segments (a tree) and such that σ is defined on every member of Δ. For each process x and finite tree of state sequences Δ, we let

(26) idobs_{x}(Δ) = {σ ↾ Δ ||| σ ∈ x, (∀<s_{0}, …, s_{n}> ∈ Δ)σ(<s_{0}, …, s_{n}>) ↓}

be the set of ideal observables of x on Δ.

Definition 2.7. A process x is effectively dense in itself if from (a canonical listing of) each ideal observable Θ = σ ↾ Δ of x, we can effectively find a recursive behavior σ′ ∈ x which realizes Θ in the sense that Θ = σ′ ↾ Δ.

Park (adapted to the present context) would call a process x implementable if it has a recursive behavior, so we can think of effective self-density as a very strong form of implementability.

Theorem 2.8. Let 𝔄 be a fixed, manageable, complete behavior structure. A total process x is computable in (𝔄, merge) if and only if it is closed as a subset of Baire space and for each finite tree of state sequences Δ, the set of ideal observables idobs_{x}(Δ) is a finite set which we can effectively list from a canonical listing of Δ.

As a subset of Baire space, each total process x computable in (𝔄, merge) is Π_{1}^{0}, compact and effectively dense in itself.

2.9. Initial vs. persistent non-determinism. A plausible modeling of a (total) process x̃ is that it is a function

(27)  x̃ : States^{⋆} → power(Acts × {∂, t}) \ {∅}

on non-empty sequences of states to non-empty sets of acts (paired with indicators), which acts as a multiple valued strategy in the interaction game: to I’s move s_{0}, x̃ responds by choosing some (a_{0}, w_{0}) ∈ x̃(<s_{0}>), to I’s next move s_{1}, x̃ responds by choosing some (a_{1}, w_{1}) ∈ x̃(<s_{0}, s_{1}>), etc. For each world strategy ω, the responses of x̃ form a closed set

ω ∗ x̃ = {a_{0}, a_{1}, …, ||| (∀n)(∃w_{n})[(a_{n}, w_{n}) ∈ x̃(<s_{0}, …, s_{n}>)]}, (28)

the appropriate analog od ω ∗ σ defined for a single-valued σ in (6). The (stream) members of this ω∗x̃ are the (observable) responses of x̃ to ω. This is the “persistent” variety of non-determinism, and versions of it occur in several models of concurrency, sometimes with the added restriction that x̃(<s_{0}, …, s_{n}>) is always a finite set; it is different from Park’s “initial non-determinism” we have adopted, by which a player x chooses at the beginning of the game a single (deterministic) strategy among those available to him, and then sticks with it no matter what. The persistent non-determinism picture of a process is quite attractive, but it cannot accomodate fairness, because if x = fairmerge(\overline{0}, \overline{1}) (for example), then the set ω ∗ x is not closed. For structures with only the full (unfair) merge to which Theorem 2.8 applies, however, if a player x is computable, then the set

ω ∗ x = {ω ∗ σ ||| σ ∈ x} (29)

is closed, in fact compact. Second, each computable player x determines a computable, multiple valued strategy

x̃(<s_{0}, …, s_{n}>) = {(a_{n}, w_{n}) ||| (∃u)[u ∗ <(a_{n}, w_{n})> ∈ idobs_{x}(Δ)},

where Δ = {<s_{0}>, <s_{0}, s_{1}>, …, <s_{0}, …, s_{n}>} is the tree of sequence states determined by <s_{0}, …, s_{n}>. Finally,

ω ∗ x̃ = ω ∗ x,

in fact x̃ determines x completely. Thus, in the absence of fairness, our picture of initial non-determinism is reconciled with the persistent non-determinism picture, at least for the computable players in which we are ultimately interested.

We do not have a complete characterization of the total, computable processes for the more complex merges, in terms of classical notions, but we can say something about them.

Theorem 2.10. Let 𝔄 be a fixed manageable, complete behavior structure.

(1) If a total process x is computable in the expansion (𝔄, parkmerge), then x is effectively dense in itself and for each finite tree of states Δ, the set of ideal observables idobs_{x}(Δ) is recursively enumerable; as a subset of Baire space, x is Σ_{1}^{1}, possibly in Σ_{1}^{1} \ Π_{1}^{1}.

(2) If a total process x is computable in the expansion (𝔄, fairmerge), then x is effectively dense in itself and for each finite tree of states Δ the set of its ideal observables idobs_{x}(Δ) is recursively enumerable; as a subset of Baire space x is Σ_{2}^{1}, possibly in Σ_{2}^{1} \ Π_{2}^{1}. ⊣

The upshot of these results is that total processes which are computable in either of the fair merges are very effective in the “loose” sense of Park; at the same time, they can be terribly complex when we view them “extensionally” (as subsets of Baire space), even proper Σ_{2}^{1} sets in the case of the full, state-dependent fairmerge.

3. Proof of the Main Result

Let

PF = (N ⇀ N), N = (N → N)

be the sets of all partial and total functions on N to N respectively. We will assume as given the notion of a (partial) recursive functional with partial function and integer arguments,

F : PF^{n} × N^{k} ⇀ N,

and the basic properties satisfied by that notion.^{8} A functional F : X → PF with values in PF is recursive if there is a recursive (partial) functional F^{∗} : X × N ⇀ N such that

F (x) = λ(n)F^{∗}(x, n).

It is sometimes important that a recursive functional takes total (number-theoretic) functions to total functions; we will abbreviate this by writing

F : N^{n} × N^{k} → N.

In general, the notation F : X → W means that F (which may have been defined as a partial function on some superset of X) is in fact totally defined on X and takes values in W.

Fixing some natural recursive isomorphism of the set of infinite sequences of partial functions (N → PF) with PF, we will also apply recursive functionals to arguments in (N → PF). We also use the correspondences i ↦ S_{i} and j ↦ A_{j}

F (α, β) ≃ if (α(0) ↓ or β(0) ↓) then 1 else ⊥

8Actually there are at least three competing notions in the literature, so that (for example) the partial functional is recursive by one of them but not the others. We will only use properties of recursive functionals which are true for all three notions, but for definiteness we adopt the most natural definition via Turing machines with oracle calls. A partial functional F : PF^{n}×N^{l} ⇀ N is recursive, if there is a deterministic Turing machine M equipped with an extra oracle tape and special states O_{i}, for i = 1, …, n, which computes F (α_{1}, …, α_{n}, j_{1}, …, j_{l}) for all unary partial function arguments α_{1}, …, α_{n} in the usual way, as if it were a partial function of its integer arguments only, but with the following rule for the computation in the oracle state: if M is in state O_{i} and the oracle tape has the number k on it (however we code numbers, unary or binary), then the computation stops if α_{i}(k) is undefined or proceeds with k replaced by α_{i}(k) on the oracle tape if α_{i}(k) is defined.

supplied with a manageable, complete structure 𝔄 to identify the set of states with N and the set of acts with the either N or a finite initial segment of N. From that, the set States^{⋆} of non-empty sequences of states is also identified with N, by some canonical, recursive coding of sequences. If we further identify the indices ∂ and t with 0 and 1 respectively and then N × {0, 1} with N using another recursive bijection, we can code the behaviors of 𝔄 with (suitably restricted) partial functions σ : N ⇀ N, i.e.

B ⊆ PF.

Finally, infinite sequences of behaviors will also be viewed as partial functions on N to N,

(N → B) ⊆ PF.

We will also use in the proofs several convenient notational conventions from [13], including

\overline{s}(n) = <s_{0}, …, s_{n}>.

Finite sequences of integers will often be confused with their codes, and then concatenation is understood appropriately. We will sometimes indicate whether an object or one of its various codes is used, but in most cases it is clear from the context what is meant and the introduction of explicit, coding functions would add little.

Suppose now that O ⊆ N is a set of total, number-theoretic functions which we take as the “oracles” and suppose f is a binary (for example) process function which is defined recursively from O via a recursive functional F as in 2.3. In our intensional approach we identify f with the collection of all its abstract implementations, which (by closure under reducibility) are exactly all behavior functions of the form

F_{π,ρ,δ}(p, q) = F (p^{π}, q^{ρ}, δ), (30)

with π, ρ : N → N and δ ∈ O. We will abbreviate this situation by writing

f(x, y) = {F (p^{π}, q^{ρ}, δ) ||| π, ρ : N → N, δ ∈ O}. (31)

The Main Result of the paper characterizes the process functions computable in various expansions (𝔄^{ȷ}, F^{∗}) of a manageable, complete structure 𝔄 as precisely the process functions which are representable by (31) with a suitably chosen O.

We will need a Lemma about the peculiar behavior function G already discussed in Section 1.

Lemma 3.1. If 𝔄 is manageable, complete and g is the process function generated by the recursive behavior function

(32) G(p) = λ(s_{0}, …, s_{n}) \{ \begin{matrix}(skip, ∂), if n = 0, \\ p(s_{0})(<s_{1}, …, s_{n}>), otherwise, \end{matrix}

then g is computable in 𝔄^{ȷ}.

Proof. Here, of course, the expression p(s_{0}) makes sense because we are identifying the states of the structure with the integers. Notice that we cannot get a trivial proof by showing that g is the lift-up G_{1}^{ȷ} of some recursive behavior function on 𝔄, among the givens of 𝔄^{ȷ} by the hypothesis that 𝔄 is manageable, complete. This is because every abstract implementation of such a G_{1}^{ȷ} satisfies

G′(p) = G_{1}(p(i_{0}))

with a fixed i_{0}, easily, so G cannot be reducible to such a G′. It is also not hard to check that g is not a composition of process functions which are lift-ups of behavior functions, which means that we must use process recursion in the proof.

Consider first the behavior function

H(σ, τ) = λ(<s_{0}, …, s_{n}>) \{ \begin{matrix}(skip, ∂), if n = 0, \\ σ(<s_{0} − 1, s_{1}, …, s_{n}>) if n > 0 & s_{0} > 0, \\ τ(<s_{1}, …, s_{n}>), if n > 0 & s_{0} = 0. \end{matrix}

This is recursive, hence computable in 𝔄, so let h = H^{ȷ} be the process function which is the lift-up of H in 𝔄^{ȷ} and let y(x) be defined by the ipf recursion

y(x) = h(y(x), x).

We will show that y is precisely the process function g generated by G in (32). The argument is basically a direct computation, but we include it primarily as an example of how these computations go.

Notice first that the typical abstract implementation of h is of the form

H′(q, p) = H(q(i_{0}), p(j_{0})) (33)

with arbitrary i_{0}, j_{0}. By the definition of recursion, each abstract implementation of y is defined by a system {H_{u} ||| u ∈ N^{∗}} of such abstract implementations of h, specifically by setting

Y (p) = σ_{∅}, (34)

where (keeping p fixed) the system {σ_{u} ||| u ∈ N^{∗}} of behaviors is defined by the simultaneous recursion

σ_{u} = H_{u}(λ(i)σ_{u∗<i>}, p).

Fix the particular system of representations of h

H_{u}(q, p) = H(q(0), p(lh(u))),

where lh(u) is the length of the sequence u. Now the behaviors

σ_{u} = σ^{lh(u)}

depend only on the length of u and they are determined by the recursion

σ^{n} = H(σ^{n+1}, p(n)),

from which it follows quite easily that

σ^{0}(<s_{0}, …, s_{n}>) ≃ \{ \begin{matrix}(skip, ∂), if n = 0, \\ p(s_{0})(<s_{1}, …, s_{n}>), if n > 0, \end{matrix}

i.e. Y (p) = σ^{0} = G(p). This proves that the process function g generated by G is a sub-process function of y.

To prove the converse inclusion, consider an arbitrary implementation system for h which must be of the form

H_{u}(q, p) = H(q(π(u)), p(ρ(u))),

for suitable π, ρ : N^{∗} → N. The behaviors assigned to this system (for each fixed p) are determined by the recursion

σ_{u} = H_{u}(λ(i)σ_{u∗<i>}, p) = H(σ_{u∗<π(u)>}, p(ρ(u))), (35)

and the abstract implementation of y determined by the system is given by (34) with these σ_{u}. It follows immediately from (35) and the definition of H that

σ_{∅}(<s_{0}>) ≃ (skip, ∂) ≃ G(p′)(<s_{0}>)

with any p′. For sequences of length greater than 1, check again from (35) and the definition of H that

σ_{u}(<0> ∗ \overline{s}(n)) ≃ p(ρ(u))(\overline{s}(n)),
σ_{u}(<i + 1> ∗ \overline{s}(n)) ≃ σ_{u∗<π(u)>}(<i> ∗ \overline{s}(n))),

so that by a simple induction on i, for each i and each u there is some number ρ^{∗}(i, u) such that

σ_{u}(<i> ∗ \overline{s}(n)) ≃ p(ρ^{∗}(i, u))(\overline{s}(n));

setting u = ∅ in this, we get the required reduction of Y (p) to G(p) via λ(i)ρ^{∗}(i, ∅). ⊣

The Main Result follows from the next two simple Lemmas, one for each direction of the claimed equivalence.

Lemma 3.2. If 𝔄^{ȷ} is the lift-up of a manageable, complete behavior structure 𝔄, F : (N → B)^{n} → B is a recursive behavior function and f is the n-ary process function generated by F, then f is computable in 𝔄^{ȷ}.

Proof. We will prove the result for n = 1, the general case being similar, so fix a recursive functional F : (N → B) → B and let f be the unary process function generated by it. The abstract implementations of f are all functions of the form

F^{π}(p) = F (p^{π}) = F (λ(i)p(π(i))), (36)

where π : N → N is arbitrary. Set

F^{∗}(σ) = F (λ(i)λ(\overline{s}(n))σ(<i> ∗ \overline{s}(n))),

so that F^{∗} is a recursive behavior function, and it is quite easy to check (by a direct computation) that we can recover F from F^{∗} using the G of Lemma 3.1,

F (p) = F^{∗}(G(p)). (37)

Since F^{∗} is recursive, it is computable in 𝔄, so let

f^{∗} = F^{∗ȷ}

be its lift-up to the process structure 𝔄^{ȷ}; we will finish off the proof by verifying that the process function f generated by F is the composition of g and f^{∗}, i.e.

f(x) =_{proc} f^{∗}(g(x)). (38)

Notice here that we are required to prove the intensional identity (38), i.e. we must show that as process functions of x, the two sides of (38) have exactly the same abstract implementations, [13, 7.6]. Now f^{∗} is generated by the single abstract implementation

F_{1}^{∗}(q) = F^{∗}(q(0)),

and by (37), F (p) = F_{1}^{∗}(λ(i)G(p)), so F is an abstract implementation of λ(x)f^{∗}(g(x)), hence f ⊆ λ(x)f^{∗}(g(x)), since F generates f. For the other direction, the typical abstract implementation of the composition on the right-hand-side of (38) is of the form

λ(p)F_{1}^{∗}((λ(i)G^{π_{i}}(p))^{ρ}) = λ(p)F^{∗}(G(p^{π_{ρ(0)}}))
= λ(p)F (p^{π}), with π = π_{ρ(0)},

i.e. it is reducible to F, which completes the proof. ⊣

This lemma will be used to show that the lift-up 𝔄^{ȷ} of a manageable, complete structure and its expansions have a rich collection of computable process functions. To show that they do not have too many, we will use the next result, which assumes a minimal regularity property of sets of oracles.

Definition 3.3. An infinite sequence coding for a set of oracles O ⊆ N is any recursive functional

proj : N × N → N

such that

(1) μ ∈ O ⟹ (∀i)[proj(μ, i) ∈ O],

(2) (∀i)[δ_{i} ∈ O] ⟹ (∃μ ∈ O)[(∀i)proj(μ, i) = δ_{i}].

For example, if O is the full Baire space N or the Cantor set C = (N → {0, 1}), we can take

proj(μ, i) = λ(n)μ(<i, n>).

If O is the set WF of wellfounded trees, we can take

proj(μ, i) = λ(u)μ(<i> ∗ u),

where ∗ here stands for concatenation of sequence codes, since a tree is wellfounded precisely when all the subtrees starting from the nodes of length 1 are wellfounded. It will be convenient to use the same classical, Kleene notation for all sequence codings,

(μ)_{i} =_{def} proj(μ, i).

Lemma 3.4. If ∅ ⊊ O ⊆ N is a set of oracles which admits an infinite sequence coding, 𝔄 is a process structure, and every given process function of 𝔄 is defined recursively from O, then every 𝔄-computable process function is also defined recursively from O.

Proof. . We use induction on the expression which defines the given process function, beginning with the obvious case of the projection function

f(x_{1}, …, x_{n}) = x_{i}

on the variable x_{i}. This is defined recursively by the functional

F (p⃗, δ) = p_{i}(0)

which makes no use of the argument in O. It is clearly enough to show that the class of process functions defined recursively from O is closed under composition and process recursion.

Composition. Suppose for simplicity that

f(x) = g(h(x))

with g, h defined recursively from O via the recursive functionals G, H, the general case being similar. A typical abstract implementation of f is given by

F_{1}(p) = G′(H_{0}(p), H_{1}(p), …,)  (G′ ∈ g, H_{i} ∈ h)
= G′(H(p^{π_{0}}, δ_{0}), H(p^{π_{1}}, δ_{1}), …, ) (δ_{i} ∈ O)
= G((λ(i)H(p^{π_{i}}, δ_{i}))^{ρ}, ϵ)  (ϵ ∈ O)
= G(λ(i)H(p^{π_{ρ(i)}}, δ_{ρ(i)}), ϵ).

If we choose μ ∈ O (depending on the given parameters) so that

(μ)_{0} = ϵ, (μ)_{i+1} = (δ)_{ρ(i)},

we then see that the typical abstract implementation of f satisfies

F_{1}(p) = G(λ(i)H(p^{π_{ρ(i)}}, (μ)_{i+1}), (μ)_{0}) (39)

with some μ ∈ O and some ρ, π_{i} : N → N.

Define now the following recursive functional F, where we think of μ as a variable over Baire space:

F (p, μ) = G(λ(i)H(λ(j)p(<i, j>), (μ)_{i+1}), (μ)_{0}).

For each μ ∈ O, F_{μ} = λ(p)F (p, μ) is certainly an abstract implementation of f, since it is a special case of (39) with ρ(i) = i and π_{i}(j) = <i, j>. To verify that all abstract implementations of f are of this form, it is enough to show that with μ ∈ O so that (39) holds and some σ : N → N we have

F_{1}(p) = F (p^{σ}, μ);

so take any σ which satisfies

σ(<i, j>) = π_{ρ(i)}(j),

i.e. without caring what the values of σ are on non-codes of pairs, and compute:

F (p^{σ}, μ) = G(λ(i)H(λ(j)p^{σ}(<i, j>), (μ)_{i+1}), (μ)_{0})
= G(λ(i)H(λ(j)p(π_{ρ(i)}(j)), (μ)_{i+1}), (μ)_{0})
= F_{1}(p).

Recursion. To keep the notation simple again, we will consider only the case of a single fixed point process \overline{x}, defined by the equation

x = f(x),

where f is assumed defined recursively from O. By the basic representation lemma 8.2 of [13], every behavior of \overline{x} is given by

σ = rec(i, p)[p(0), F_{1}(i, p)]

where F_{1} is an arbitrary representation of f. The hypothesis is that

F_{1}(i, p) = F (p^{π_{i}}, δ_{i})

holds, with a fixed recursive functional F and suitable π_{i} : N → N and δ_{i} ∈ O. Thus the typical behavior in \overline{x} is given by

σ = \overline{p}(0),

where \overline{p} is the least-fixed-point of the fixpoint equation

p(i) = F (λ(j)p(π_{i}(j)), δ_{i}). (40)

If we put together all the π_{i} into one,

π(<i, j>) = π_{i}(j),

then equation (40) which we must solve becomes

p(i) = F (λ(j)p(π(<i, j>)), δ_{i}). (41)

Next define a function ρ(w) on sequence codes of integers to integers by recursion on the length of the sequence (coded by) w,

ρ(<a>) = a,
ρ(u ∗ <a>) = π(<ρ(u), a>),

COMPUTABLE CONCURRENT PROCESSES 25

and using this ρ, define the behavior \overline{q} from \overline{p} by \overline{q}(w) = \overline{p}(ρ(w)). (42) We compute the equation satisfied by \overline{q}:

\overline{q}(w) = \overline{p}(ρ(w))
= F (λ(j)\overline{p}(π(<ρ(w), j>)), δ_{ρ(w)}) by (41)
= F (λ(j)\overline{p}(ρ(w ∗ <j>), δ_{ρ(w)})  by def. of ρ
= F (λ(j)\overline{q}(w ∗ <j>), δ_{ρ(w)})  by def. of \overline{q}.

Thus \overline{q} is a solution of the equation q(w) = F (λ(j)q(w ∗ <j>), δ_{ρ(w)}), (43) and if q̃ is the least solution of this equation we have q̃ ≤ \overline{q}. (44) We also need to show that \overline{q} ≤ q̃ and to do this we will check by induction on n that

\overline{q}^{(n)} ≤ q̃,

where

\overline{q}^{(n)}(w) = \overline{p}^{(n)}(ρ(w))

and \overline{p}^{(n)} is the n’th stage in the recursion which define \overline{p}. The basis case is similar to the induction step, so we compute for this:

\overline{q}^{(n+1)}(w) = \overline{p}^{(n+1)}(ρ(w))
= F (λ(j)\overline{p}^{(n)}(π(<ρ(w), j>)), δ_{ρ(w)}) by def.
= F (λ(j)\overline{p}^{(n)}(ρ(w ∗ <j>)), δ_{ρ(w)}) by def. of ρ
= F (λ(j)\overline{q}^{(n)}(w ∗ <j>), δ_{ρ(w)})  by def. of \overline{q}^{(n)}
≤ F (λ(j)q̃(w ∗ <j>), δ_{ρ(w)})  by ind. hyp.
= q̃(w).

Here the monotonicity of the functional F is used in the application of the induction hypothesis and the last step uses the fact that q̃ satisfies the fixed-point equation which defined it. Thus we now have that

(45) \overline{q} is the least-fixed-point of (43). Since each δ_{ρ(w)} ∈ O, we can find a single μ ∈ O such that for all w (μ)_{w} = δ_{ρ(w)}, (46) and with this μ, \overline{q} is the least-fixed-point of q(w) = F (λ(j)q(w ∗ <j>), (μ)_{w}). (47) If we now consider μ as a variable and let

H(w, μ) = \overline{q}(w) relative to μ
= the least-fixed-point of (47),

then this functional H is recursive, since it is the least-fixed-point of a recursive equation;^{9} the proof will be completed if we can show that

\overline{x} = \{H(<0>, μ) ||| μ ∈ O\}.

We have already verified that the typical behavior of \overline{x} is given by

σ = \overline{p}(0) = \overline{p}(ρ(<0>))  (ρ(<0>) = 0)
= \overline{q}(<0>)
= H(<0>, μ),

with the μ chosen above. On the other hand, we can show that for arbitrary μ ∈ O, H(<0>, μ) defines a behavior in \overline{x} by choosing π(<i, j>) = π_{i}(j) = j, so ρ(u ∗ <a>) = a and then tracing the definitions:

H(<0>, μ) = \overline{p}(ρ(<0>)) = \overline{p}(0) ∈ \overline{x}. ⊣

To prove the Main Result using lemmas 3.2 and 3.4, we will appeal repeatedly to the trivial fact that the “merging functional”

(μ, σ, τ) ↦ μ[σ, τ] (μ : States^{⋆} → {0, 1}, σ, τ ∈ B)

is recursive. Here we identify (States^{∗} → {0, 1}) with the Cantor set C = (N → {0, 1}) by the obvious recursive isomorphism, i.e. we think of the set of all mergers as identical with C. We check parts (1) – (5) in turn.

Proof of (1). Directly from the definitions, merge, or and + are defined recursively from the Cantor set C, so that by 3.4 all the computable functions in the expansions of 𝔄 by merge or or are also defined recursively from C. To check the converse, identify some two distinct acts with the numbers 0 and 1, let

\overline{0} = rec(x)[x, 0 ; x], \overline{1} = rec(x)[x, 1 ; x]

be the (deterministic) processes with sole behaviors the indefinite iterations of 0 or 1, and let

c = merge(\overline{0}, \overline{1}) = rec(x)[x, (0 or 1) ; x]

be the (non-deterministic, state-independent) process whose behaviors are all binary sequences, so that (with our identifications, as a set), c = C. The definition exhibits that c is computable in both expansions of 𝔄 by merge or or, so it is enough to check that every process function which is defined recursively from C is computable in the simpler expansion (𝔄^{ȷ}, c). For example, if

f(x, y) = {F (p, q, δ) ||| p : N → x, q : N → y, δ ∈ C}

with F recursive, let g be the process function defined by

g(x, y, z) = {F (p, q, r(0)) ||| p : N → x, q : N → y, r : N → z}

and check immediately that f(x, y) =_{proc} g(x, y, c). The argument for + is similar.

9We are appealing here to the fundamental First Recursion Theorem of Kleene, which holds of all, natural notions of “recursive functional.” See e.g. [16, XII].

Proof of (2). There is a well known recursive correspondence between the fair binary sequences and N which goes as follows. If α(0) = 2n is even, we associate with α the binary sequence π(α) which gives n + 1 consecutive 0s, then α(1) + 1 consecutive 1s, then α(2) + 1 consecutive 0s, etc. If α(0) = 2n + 1 is odd, we define π(α) similarly, but starting this time with n + 1 consecutive 1s. The inverse of π is also recursive, easily. From this correspondence, it is immediate that parkmerge is defined recursively from the Baire space N, so that by 3.4, every process function in (𝔄^{ȷ}, parkmerge) is defined recursively from N. The converse is proved as above, taking this time the constant

p = fairmerge(\overline{0}, \overline{1})

which is computable in (𝔄^{ȷ}, fairmerge) and checking using π, π^{−1} that every process function defined recursively from N can be obtained by the substitution of p in a process function which is generated by a recursive functional.

Proof of (3). To check first that fairmerge is defined recursively from the set WF of wellfounded trees, consider the following map which assigns to each sequence of wellfounded trees

T⃗ = T (0), T (1), …,

a fair merger μT⃗. We will use T (0) only to decide whether the merger should start giving 0s or 1s: say “give 0s” if (0, 0) ∈ T (0), else “give 1s”. For this definition, let <s_{0}, …, s_{n}> be the integer code of the sequence \overline{s}(n) = (s_{0}, …, s_{n}) (which is never 0), the states being identified with integers again, suppose T (0) told us to start with 0, and to I’s play of s_{0}, s_{1}, … have the merger give 0 until the finite sequence \overline{s}(n) ∉ T (<∅>); next start using the tree T (<\overline{s}(n)>) and to I’s play s_{n+1}, s_{n+2}, … have the merger give 1 until the sequence (s_{n+1}, s_{n+2}, …, s_{m}) ∉ T (<s_{0}, …, s_{n}>); and so on, using for the next stage the tree T (<s_{n+1}, …, s_{m}>). It is quite easy to verify that we get all fair (state dependent) mergers in this way. Moreover, with each wellfounded tree T we can associate such a sequence by the obvious map

T_{i} = {u ||| (i) ∗ u ∈ T },

and combining these two operations we have a map from the set of wellfounded trees onto the set of all fair mergers. Moreover, the map is represented by a recursive functional (say) F on the subset WF of Baire space which codes the wellfounded trees, so that we get the representation

fairmerge(x, y) = {F (δ)(p(0), q(0)) ||| p : N → x, q : N → y, δ ∈ WF}

which shows that fairmerge is recursively defined from WF. By 3.4 then, every process function computable in (𝔄^{ȷ}, fairmerge) is recursively defined from WF.

The converse is verified exactly as above replacing c and p by

f_{0} = fairmerge(\overline{0}, 1).

This is a process whose behaviors are precisely all binary functions on (N → States) (the plays of I) which take at least once the value 1, i.e. precisely the set of (codes of) wellfounded trees.

The proof of the Main Result is now completed by noticing that (4) is an immediate consequence of 3.4 and (5) follows trivially from the fact that each of the oracle sets C, N and WF has a recursive member.

4. Total computable processes

Let us assume throughout this section that 𝔄 is a fixed, manageable, complete behavior structure. The proofs of 2.8 and 2.10 will follow from some simple lemmas, which combine the Main Result with a few elementary computations and applications of König’s Lemma. We restate here for easy reference the definition of the ideal observables of a total process x on a finite tree of state sequences Δ,

idobs_{x}(Δ) = {σ ↾ Δ ||| σ ∈ x},

where

σ ↾ Δ = \{<\overline{s}(n), σ(\overline{s}(n))> ||| \overline{s}(n) ∈ Δ\}.

Notice that each σ ↾ Δ is a finite object which can be represented by an integer, via some canonical coding.

Lemma 4.1. If x is a total process, recursively defined from the Cantor set C, then x is compact (as a subset of Baire space) and for each finite tree of state sequences Δ, the set idobs_{x}(Δ) is finite and can be effectively listed from a listing of Δ.

Proof. By definition, we know that there exists a recursive (hence continuous) function F : C → B such that

x = F [C] = {F (δ) ||| δ ∈ C} ⊆ N, (48)

so x is certainly compact. For each finite tree of state sequences Δ, set

G_{Δ}(δ) = F (δ) ↾ Δ

and notice that G_{Δ} is a continuous function, total on the Cantor set C and with discrete values (essentially) in N. By König’s lemma there is a fixed integer m such that G_{Δ}(δ) depends only on the first m values of δ. It follows that the image G_{Δ}[C] = idobs_{x}(Δ) is finite, we can find one such bound m by a dumb search and we then use it to give a listing of idobs_{x}(Δ). ⊣ Lemma 4.2. If x is a total process, closed as a subset of Baire space and such that for each finite tree of state sequences Δ, the set idobs_{x}(Δ) is finite and can be effectively listed from a listing of Δ, then x is recursively defined from the Cantor set C.

Proof. Recall that we have identified the states with integers and for each i, let Δ_{i} be the finite tree of all state sequences which have length at most i and involve only the first i + 1 states. Notice that

Δ_{0} ⊆ Δ_{1} ⊆ ⋯,

so for any behavior σ,

σ ↾ Δ_{0} ⊆ σ ↾ Δ_{1} ⊆ · · · .

Consider now the tree T of all finite sequences of the form

(Θ_{0}, Θ_{1}, …, Θ_{n}) (49)

so that the following conditions hold.

(1) For each i ≤ n, there is some σ ∈ x such that

Θ_{i} = σ ↾ Δ_{i},

i.e. Θ_{i} is an ideal observable of x on Δ_{i}.

(2) Θ_{0} ⊆ Θ_{1} ⊆ ⋯ ⊆ Θ_{n}.

We can think of a coded version of T as a tree on integers, since its nodes are finite objects which can be listed, and as such, quite obviously from the hypothesis on x, T is a recursive, finitely branching tree. Moreover, every sequence in T has a proper extension in T , because its last term is an ideal observable of some behavior of x, which is total and therefore has a “fuller” observable on the next, larger tree of state sequences. Each Θ_{i} which occurs in a sequence of T determines some partial behavior σ(Θ_{i}) defined on the sequences in Δ_{i}, such that

Θ_{i} = σ(Θ_{i}) ↾ Δ_{i}

and σ(Θ_{i}) has a total extension in x. Moreover, for every sequence in T as in (49), we have

σ(Θ_{0}) ⊆ σ(Θ_{1}) ⊆ ⋯ ⊆ σ(Θ_{n}),

so that we can map each infinite branch

Θ⃗ = (Θ_{0} ⊆ Θ_{1} ⊆ ⋯)

of T onto a behavior

σ(Θ⃗) = lim_{n} σ(Θ_{n}).

The hypothesis that x is closed implies that σ(Θ⃗) ∈ x, so the construction gives an effective map from T onto x. The proof is completed by composing this map with some canonical, recursive surjection of the Cantor set onto the infinite branches in T , which exists because T is a finitely branching, recursive tree. ⊣ Lemma 4.3. Every total process computable from C is Π_{1}^{0}, as a subset of N.

Proof. The player x = F [C] is the continuous image of a compact set, hence compact, hence closed, and every closed subset of N is “Π_{1}^{0} in some parameter,” so we are almost there—but we need to check that the parameter is not needed, i.e. give a direct Π_{1}^{0} definition of x. By the basic representation (48) for x we have

σ ∉ x ⟺ (∀δ ∈ C) \underbrace{[F (δ) ≠ σ]};

for a fixed σ, the condition on δ above the brace is open and by another simple application of König’s Lemma and the recursiveness of F we have a semi-effective procedure for verifying that it is true of all δ ∈ C. This proves that the complement of x is Σ_{1}^{0}, so x is Π_{1}^{0}, as required. ⊣

Lemma 4.4. Every total process, recursively defined from C, N or WF is effectively dense in itself.

Proof. Suppose that x = F [O] with F recursive and the relevant O and let Θ be an ideal observable of x, so that for some δ ∈ O, we have

(∃Δ)[F (δ) ↾ Δ = Θ]. (50)

This is an open condition on δ, so if satisfiable it holds for all δ (in O or outside O) which extend some finite sequence of values w, and we can certainly find such a w by a dumb search. The (trivial) key fact is that every w has recursive extensions δ ∈ O for the Os in which we are interested, and any such δ satisfies (50). ⊣

With the Main Result, these lemmas imply immediately 2.8 and some of 2.10. The remaining claims of 2.10 are trivial consequences of the Main Result and known properties of the analytical classes of relations.

References

1. M. Abadi, L. Lamport and P. Wolper, Realizable and unrealizable specifications of reactive systems, Proceedings of the 1989 ICALP, to appear.

2. M. Broy, A theory for nondeterminism, parallelism, communication, and concurrency, Th. Computer Science 45 (1986), 1-61.

3. B. Courcelle, Recursive applicative program schemes, Handbook of Theoretical Computer Science, ed. J. van Leeuwen, Elsevier (1990), pp. 461-492.

4. J. W. de Bakker and J. I. Zucker, Proccesses and the denotational semantics of concurrency, reprinted in Ten years of concurrency semantics, World Scientific Publishing Co., 1992.

5. E. W. Dijkstra, A discipline of programming, Prentice-Hall, 1976.

6. N. Francez, Fairness, Springer-Verlag, 1986.

7. C. A. R Hoare, Communicating sequential processes, Prentice Hall, 1985.

8. Zohar Manna and Amir Pnueli, The temporal logic of reactive and concurrent systems, Springer-Verlag, 1992.

9. Robin Milner, Communication and concurrency, Prentice Hall, 1989.

10. Y. N. Moschovakis, Descriptive set theory, Studies in Logic, North Holland, 1980.

11. Y. N. Moschovakis, Computable processes, Proceedings of the 1990 POPL meeting in San Francisco.

12. Y. N. Moschovakis, The formal language of recursion, J. Symbolic Logic, 54 (1989), pp. 1216-1252.

13. Y. N. Moschovakis, A model of concurrency with fair merge and full recursion, Information and Computation, 93, 1991, pp. 114-171.

14. Y. N. Moschovakis and Glen T. Whitney, Powerdomains, powerstructures and fairness, in preparation.

15. Viggo Stoltenberg-Hansen and J. V. Tucker, Algebraic and fixed point equations over inverse limits of algebras, Theoretical Computer Science, 267 (1991), pp. 1-24.

16. H. Rogers, Jr., Theory of recursive functions and effective computability, McGraw-Hill, NY, 1967.

17. D. Park, On the semantics of fair parallelism, Proc. Copenhagen Winter School, Springer LNCS 104 (1980), 504-526.

18. D. Park, The “fairness” problem and nondeterministic computing networks, Foundations of Comp. Sc. IV, 33-162, Mathematisch Centrum, Amsterdam 1983.

19. G. D. Plotkin, A powerdomain construction, SIAM J. of Comput. 5, 1976, pp 452-487.

20. A. Pnueli and R. Rosner, On the synthesis of a reactive module, Proceedings of the 1989 ICALP, to appear.

21. M. B. Smyth, Modeling concurrency with partial orders, J. Comput. System Sci. 16, 1978, pp. 23-36.

22. Glen T. Whitney, Recursion structures for non-determinism and concurrency, Ph.D. Thesis, in preparation.

Department of Mathematics, University of California, Los Angeles, LA CA 90024

E-mail address: ynm@math.ucla.edu