Powerdomains, Powerstructures and Fairness

Yiannis N. Moschovakis^{1} and Glen T. Whitney^{2}^{⋆}

1 Dept. of Math, UCLA, Los Angeles, CA 90024; ynm@math.ucla.edu 2 Dept. of Math, University of Michigan, Ann Arbor, MI 48109; gwhitney@umich.edu

Abstract. We introduce the framework of powerstructures for comparing models of non-determinism and concurrency, and we show that in this context the Plotkin powerdomain plot(D) [6] naturally occurs as a quotient of a refined and generalized player model ipf (D), following Moschovakis [2, 3]. On the other hand, Plotkin’s domains for countable non-determinism plot_{ω}(D) [7] are not comparable with these structures, as they cannot be realized concretely in the powerset of D.

If, as usual, we let the programs of a deterministic programming language L denote points in some directed-complete poset (dcpo) D, then programs in nondeterministic extensions of L should naturally correspond to non-empty subsets of D, members of the set of players^{3}

Π = Π(D) =df {x ⊆ D ||| x ≠ ∅}.  (1)

This idea immediately encounters a problem with non-deterministic recursive definitions. In the deterministic case, the open terms of L (its program transformations) denote (Scott) continuous functions on D. Their least fixed points (which exist precisely because D is a dcpo) provide a means of interpreting recursion. On Π(D), which does not carry a natural, complete partial ordering, how are we to interpret non-deterministic program transformations so that they still have “canonical” fixed points? No known semantics solves this basic problem in the modeling of non-determinism in an entirely satisfactory way.

For a concrete example, let Str be the dcpo of integer streams, where (following [5]) a stream is a finite or infinite sequence, or a finite sequence of the form a_{1}a_{2} … a_{n}t, where the terminator t is some fixed non-integer witnessing “termination.” Now Π(Str) is the set of non-deterministic integer streams, and many of the usual, non-deterministic constructs are naturally interpreted by functions on Π(Str) as follows:

x or y =df x ∪ y  (2)
merge(x, y) =df {μ[α, β] ||| α ∈ x, β ∈ y, μ: ℕ → {0, 1}}  (3)
fairmerge(x, y) =df {μ[α, β] ||| α ∈ x, β ∈ y, μ a fair merger}.  (4)

⋆ During the preparation of this paper, Moschovakis was partially supported by a NSF Grant and Whitney was supported by a Fellowship from the Fanny and John Hertz Foundation.

3 The term derives from the original construction in Moschovakis [2, 3] which was cast in game theoretic terms, for a specific domain D of partial strategies.

Here or stands for free, binary choice, μ[α, β] stands for “interleaving α and β by the merger μ” in the obvious way, and a (strict) fair merger (following Park [5]) is any sequence of 0’s and 1’s which is not ultimately constant. Note that as operations on players, these merges remain distinct. If D has further structure, then additional operations of this sort can be defined, such as state-dependent fair merges, see [3].

To model non-deterministic recursion within domain theory, we must embed Π(D) in some powerdomain D^{∗}, and not totally arbitrarily. For example, D is embedded in Π(D) by the natural map d ↦ {d}, and we would want to have “liftups” of the continuous functions in (D → D) to continuous functions in (D^{∗} → D^{∗}) which respect composition, yield the correct least fixed points, etc. Even such simple requirements seem to force undesirable consequences about D^{∗}, however. Consider the first and most interesting powerdomain construction plot(D) of Plotkin [6] (see also Smyth [8]) as an illustrative example. plot(D) does not faithfully model fairness because it identifies sets in Π(D) which are equivalent under^{4} the “observational Egli-Milner equivalence relation” ≃_{em}. This collapses the merge and fairmerge operations on Π(Str), e.g., fairmerge(a^{∞}, b^{∞}) ≃_{em} merge(a^{∞}, b^{∞}), where a^{∞} is the infinite string of ‘a’s. In addition, the equivalence relation ≃_{em} identifies certain unguarded recursions with similar, but intuitively distinct, guarded recursions, e.g., see Smyth [8].

To circumvent these imperfections of the powerdomain constructions, Moschovakis [2, 3] introduced (over some specific domains D) a model ipf (D) for non-determinism and concurrency in which programs are interpreted by arbitrary players, and program transformations are modeled by implemented player functions (ipfs) on Π(D). These ipfs encode more than their values on players: there exist distinct ipfs f and g such that f(x) = g(x) for all x ∈ Π(D). The extra, intensional information carried by an ipf makes it possible to assign “canonical solutions” to systems of recursive equations, so that the laws of recursion are obeyed; we will make this precise further on. The or, merge, and fairmerge operations introduced above are naturally modeled by certain ipfs (and incidentally “unnaturally” modeled by others, distinct from but extensionally equal to the natural ones.)

Our principal aim here is to show that (with modest hypotheses on D) the Plotkin powerdomain plot(D) can be recovered in a natural way from ipf (D), while the countable powerdomains plot_{ω}(D) appear to represent a fundamentally different modeling of fairness. For this, we will also introduce a refined construction of ipf (D) (for any D) and establish precise properties of ipf (D)

4 The terminology for various pre-orders on Π(D) is not entirely standardized. In this paper, we will use the lower preorder (x ⊑_{l} y if for all a ∈ x, there exists b ∈ y such that a ≤ b) and the upper preorder (x ⊑^{u} y if for all b ∈ y, there exists a ∈ x such that a ≤ b). The usual “Egli-Milner preorder” is the conjunction of these two. However, as outlined in Smyth [8], the easiest construction of the Plotkin powerdomain for countably algebraic D is in terms of the “observational Egli-Milner” preorder, defined as x ⊏ ∼ y if for all finite sets A of finite elements, A ⊑_{l} x implies A ⊑_{l} y and A ⊑^{u} x implies A ⊑^{u} y. Each preorder induces an equivalence relation, for example x ≃_{em} y if x ⊏ ∼ y and y ⊏ ∼ x.

which make it a suitable structure for modeling non-deterministic programs and program transformations. We will rely heavily on an axiomatization of the “standard” laws of recursive equations, and on a somewhat novel approach to the development of intensional semantics for formal languages, which has applications beyond its present use. These ideas are described in Section 1.

1 The main notions

For each vocabulary (signature) τ, i.e., set of function symbols with associated non-negative arities, the expressions of the language FLR_{0}(τ) are given by

E :≡ x | f(E_{1}, …, E_{n}) | E_{0} where {x_{1} = E_{1}, …, x_{n} = E_{n}} ,

where x is a variable (from some fixed, infinite set of variables) and f ∈ τ. Intuitively, FLR_{0} has notation just for function application and for solution of simultaneous recursion equations. The where operator binds the variables x_{1} through x_{n}; all other variable occurrences are free. A closed expression is one containing no free variables, e.g., f(g()) or x where {x = f(x)} if f is unary and g is nullary.

In the standard semantics for FLR_{0}, we have a dcpo D together with some continuous functions on D to interpret the function symbols, and with each FLR_{0} expression E and each assignment π : Variables → D, we associate a point value(E, π) ∈ D. If E is an open FLR_{0} expression and the list of variables x = x_{1}, …, x_{n} includes all the free variables of E, then

Λ(x)E = λ(y)value(E, {x_{1} := y_{1}, …, x_{n} := y_{n})})  (5)

is the n-ary function defined by E and x. The more general, intensional semantics for FLR_{0} needed here are defined directly in terms of a given interpretation Λ, making (5) a theorem rather than a definition in the standard case.

The universe of an interpretation Λ is a set Φ of objects with associated integer arities; Φ_{n} comprises the n-ary objects of Φ, and the nullary objects in Φ_{0} are its individuals. In a standard interpretation, Φ_{0} = D is a dcpo and Φ_{n} consists of all the continuous, n-ary functions on D. The interpretation Λ assigns to each expression E and list of variables x = x_{1}, …, x_{n} including all free variables of E an object Λ(x) E in Φ_{n}, so that the following basic conditions of compositionality hold:

(1) Λ(x) x_{i} depends only on the length of x and on i; in the standard case, this must be the usual projection function from D^{n} to D by the ith component.

(2) If Λ(x) M_{i} = Λ(y) M′_{i} for i = 1, …, n, then Λ(x) f(M_{1}, …, M_{n}) = Λ(y) f(M′_{1}, …, M′_{n}). In the standard case, these must be computed by ordinary function application of the interpretation of f on the given values.

(3) If Λ(y) E(y_{1}, …, y_{n}) = Λ(z) E′(z_{1}, …, z_{n}) and the substitutions E[M/y] and E′[M/z] are free, then Λ(x) E(M_{1}, …, M_{n}) = Λ(x) E′(M_{1}, …, M_{n}).

(4) If w = Λ(x) E_{0} where {y_{1} = E_{1}, …, y_{n} = E_{n}}, suppose first that no y_{i} occurs in x. Then w depends only on Λ(y, x) E_{i} for i from 0 to n. In general, let x′ be the same as x except that every variable from x occurring as one of the y_{i} has been replaced by a fresh variable. Then w depends only on Λ(y, x′) E_{i}, in the same sense as the last two requirements: if these values are equal to Λ(u, z′) M_{i}, respectively, then w = Λ(z) M_{0} where {u = M}. For a standard interpretation, w must be computed by taking the least fixed point of the system y_{i} = Λ(y, x′) E_{i} for i from 1 to n, and substituting the results (which are functions of the x′) into E_{0}.

An expression identity E = M is standard if it is valid for all standard interpretations, i.e., Λ(x)E = Λ(x)M for every list x which includes all the free variables of both E and M. The simplest example of a standard identity is

f( x where {x = f(x)}) = x where {x = f(x)}  (6)

which asserts that “the least fixed point of f is a fixed point of f”. Others include the Bekič-Scott rules which relate simultaneous and iterated recursion, the reduction of explicit definition to recursion, etc. It can be shown that the class of standard identities (on a recursive, countable vocabulary) is decidable, simply (and usefully) axiomatizable, and the same as the class of identities valid for all interpretations with individuals D_{0}, the set of all streams of ‘0’s.^{5} This robustness of the standard identities suggests that they truly codify the laws of recursive equations—the rules we use unthinkingly when we manipulate recursive definitions—and we look for modelings of non-determinacy and concurrency among FLR_{0} interpretations which satisfy them.

An (abstract, intensional) FLR_{0}-structure is a triple

A = (Φ_{0}, {Φ_{n}}_{n≥1} , Λ),

where Φ = ⋃ Φ_{n} is a universe and Λ is an interpretation of FLR_{0}(Φ) into Φ which satisfies the standard identities and also

Λ(x_{1}, …, x_{n}) f(x_{1}, …, x_{n}) = f for each f ∈ Φ_{n}.  (7)

Notice that here we view Φ as both a vocabulary and universe, each f ∈ Φ_{n} being an n-ary function symbol naming itself as enforced by (7). Each dcpo D gives rise to a standard FLR_{0}-structure, in which Φ_{0} = D, Φ_{n} consists of the n-ary continuous functions from D to D, and Λ is the standard interpretation as described above.

In an arbitrary FLR_{0}-structure, we think of the elements f of Φ as intensional functions on A = Φ_{0}, and every n-ary f determines an actual function \overline{f}: A^{n} → A via

\overline{f}(a_{1}, …, a_{n}) =df Λ() f(a_{1}, …, a_{n}).  (8)

We say that \overline{f} is the extension of f, or that f covers \overline{f}.

A homomorphism ρ : A → B from A (as above) to B = (Ψ_{0}, {Ψ_{n}}_{n≥1} , Λ′) is any arity-preserving map from Φ to Ψ = ⋃ Ψ_{n} which respects the interpretations,

5 These results will appear in a multi-authored paper The logic of recursive equations, now in preparation.

as follows: extend ρ (by substitution) so that it takes arbitrary expressions of FLR_{0}(Φ) to expressions of FLR_{0}(Ψ); then it must satisfy

ρ(Λ(x)E) = Λ′(x)(ρ(E)).

Thus, homomorphisms preserve all possible compositions and recursions.

A powerstructure over a dcpo D is an FLR_{0}-structure P = (P, Φ_{n≥1}, Λ) such that there is an injective FLR_{0}-homomorphism ρ from the standard FLR_{0}- structure over D to P satisfying the following two finite non-determinism conditions:

(1) The map {d} ↦ ρ(d) on the singletons of D extends to a surjective map π: S_{P} → → P, where S_{P} is a subset of Π(D) closed under continuous images and finite unions.

(2) Similarly, for each arity n, the map {F } ↦ ρ(F) on the singletons of continuous functions extends to a map π which takes each finite set J of n-ary continuous functions to some π(J) ∈ Φ_{n}, so that:

\overline{π(J)}(πx_{1}, …, πx_{n}) = π \{F (d_{1}, …, d_{n}) ||| F ∈ J, d_{i} ∈ x_{i}\} .  (9)

If for a particular powerstructure P both occurrences of “finite” in these conditions may be replaced by “countable” or “arbitrary”, then the powerstructure is called countably non-deterministic or fully non-deterministic, respectively. We also say that P is fine, if the map π on individuals is actually a bijection, so that P can be identified with a set of players.

The second condition applied to singletons {F } implies that each continuous F : D^{n} → D has a lift-up f, such that

\overline{f}(πx_{1}, …, πx_{n}) = π\{F (d_{1}, …, d_{n}) ||| d_{1} ∈ x_{1}, …, d_{n} ∈ x_{n}\}.

In addition, if U = {F_{1}, F_{2}} where F_{1}(d, e) = d, F_{2}(d, e) = e, then the corresponding intensional function π(U) covers the (“quotient” of the) binary union operation (2). If P is fine and fully non-deterministic over Str and M is the set of all functions of the form F_{μ}(α_{0}, α_{1}) = μ[α_{0}, α_{1}] with μ a fair merger, then π(M) covers fairmerge as defined above (4). Thus, fine, fully non-deterministic powerstructures can provide powerful and faithful models of “fair concurrency.”

Note that plot(D) together with the continuous functions on it is a powerstructure, but not a fine one: S_{P} is the collection of finitely generable subsets of D and π identifies Egli-Milner equivalent sets. Neither is plot(D) fully nondeterministic. The powerdomains plot_{ω}(D) enjoy the intermediate property of countable non-determinism which can be used to define fairmerge, although not in the direct way described above, for there are uncountably many fair mergers μ. It is not clear that countable non-determinism provides a rich enough model to handle the many extant notions of fairness; in particular, we do not expect to be able to define natural state-dependent fair merges or the fair merge of countably many streams using only countable non-determinism.

2 Main results

Theorem A. For each domain D, there is a fine, fully non-deterministic powerstructure ipf (D) = (Π(D), ipf (D), Λipf) over D.

In the construction of ipf (D), every intensional function essentially arises as f_{J} for some J, so every \overline{f} in ipf (D) ends up being set monotone, i.e.,

x ⊆ y ⇒ \overline{f}(x) ⊆ \overline{f}(y),  (10)

and this limits the functions on plot(D) we can represent inside ipf (D). Recall that (for countably algebraic D), plot(D) can be defined as the quotient of the finitely generable subsets of D (which we will denote by Π_{0}(D)), under the equivalence ≃_{em}. Therefore, each continuous function ϕ : plot(D) → plot(D) is induced by some continuous function ϕ_{∗} : Π_{0}(D) → Π_{0}(D) on the predomain Π_{0}(D), i.e.,

ϕ([x/ ≃_{em}]) = [ϕ_{∗}(x)/ ≃_{em}], (x ∈ Π_{0}(D)).  (11)

In particular, we say that ϕ is essentially monotone if it is induced by some set monotone ϕ_{∗}. The essentially monotone functions em(D) are closed under composition and recursion, and therefore together with plot(D) and the standard (least-fixed-point) interpretation comprise an FLR_{0}-structure Pl(D) = (plot(D), em(D), Λstd). This is a natural FLR_{0}-structure associated with the Plotkin powerdomain, and it includes all ∪-linear functions [1].

Theorem B. If D is strongly algebraic then there is an FLR_{0}-substructure ipf_{0}(D) = (Π_{0}(D), ipf_{0}(D), Λ_{0}) of ipf (D) with the following properties.

(a) Each player function \overline{f} in ipf_{0}(D) respects the Egli-Milner preorder on Π_{0}(D) and is Scott continuous, so that it induces a continuous function

ρ(f) = ϕ : plot(D) → plot(D)  (12)

on the Plotkin powerdomain by the equation ϕ([x/ ≃_{em}]) = [\overline{f}(x)/ ≃_{em}]. (By the observation (10), ϕ is necessarily essentially monotone.)

(b) If we extend the map ρ to Π_{0}(D) by ρ(x) = [x/ ≃_{em}], it becomes an FLR_{0}-homomorphism from ipf_{0}(D) to Pl(D).

(c) If ϕ : plot(D) → plot(D) is essentially monotone, then ϕ = ρ(f) for some player transformation f in ipf_{0}(D); that is, the image of the homomorphism ρ is exactly Pl(D).

No similar comparison is possible between ipf (D) and plot_{ω}(D), however. The obstacle is that except for extremely simple (e.g., flat) D, plot_{ω}(D) cannot be thought of as a structure on the subsets of D, or precisely:

Theorem C. For any domain D embedding (1_{⊥} × ℕ)_{⊥}, the free σ-semilattice over D is not the homomorphic image of (Π(D), ⊑, ⊆) with ordinary ⊆ and any partial order ⊑.

This means that plot_{ω}(D) is not technically a powerstructure in our sense, in that it does not represent non-deterministic “programs” (FLR_{0} expressions) by their set of possible “outcomes” (subset of D), but provides some altogether different, less concrete interpretation.

3 Details and proofs

To prove Theorem A, we need to define the class ipf (D) of implemented player functions on an arbitrary dcpo D, specify suitable operations of composition and recursion on this class, and then show that the resulting structure ipf (D) = (Π(D), ipf (D), Λipf) is a fully non-deterministic powerstructure. The complete construction is quite long, but not very different from that given in detail and with many motivating examples in [3], for a specific D. Here we confine ourselves to a brief sketch, highlighting the differences arising in the general case; [9] contains a full treatment.

A unary polyfunction on D is a monotone function F: D^{I} → D, where the index set I is an arbitrary set of integers and D^{I} is the dcpo of maps from I to D under the pointwise ordering. Each polyfunction induces a function on Π(D)

F̄(x) = {F (X) ||| X: I → x} ,

and we think of F as an “implementation” of F̄. However, some polyfunctions differ inessentially by the integer “tags” they use to name their arguments: we say that G: D^{J} → D reduces to F: D^{I} → D, written G ⪯ F, if there is an injection ι: I → J such that G(p) = F (p ∘ ι) for all p ∈ D^{J}. Let ≍ be the smallest equivalence relation extending ⪯, and call two polyfunctions F_{1} and F_{2} equivalent if F_{1} ≍ F_{2}. It is simple to verify that if F ≍ G, then F̄ = Ḡ. Finally, a (unary) implemented player function (ipf) is a nonempty set of polyfunctions closed under ≍. Each ipf f induces a function f̄: Π(D) → Π(D) (its extension) by

f̄(x) = ⋃_{F ∈f} F̄(x) = {F (X) ||| F ∈ f, X: I → x where F : D^{I} → D} . (13)

The members of f are called its implementations, and a set F of polyfunctions generates f, written f = ⟨F⟩, if f is the closure of F under ≍, i.e.,

G ∈ f ⟺ (∃F ∈ F) such that G ≍ F.

It is not difficult to see that a generating set of implementations suffices to determine the extension of f as per (13). For n-ary ipfs we use polyfunctions F: D^{I_{1}} × ⋯ × D^{I_{n}} → D and proceed similarly.

Polyfunctions generalize the infinitary behavior functions of [3], where, however, only one index set was allowed, I = ℕ. A more essential difference is the present choice of polyfunction equivalence, which is less coarse than that of [3] and produces more natural modelings in the specific examples.^{6} This choice of equivalence requires some extra care in the correct definition of ipf composition and ipf recursion, but these constructions are quite similar to those of [3] and we will skip them. We mention the one technical notion needed in the proofs below, to set notation.

6 The desirability of this refinement was discussed briefly in Footnote 8 of [3], but the methods of that paper were not strong enough to prove the main results with the present, more natural equivalence relation.

An implementation system for a single ipf equation of the form x = f(x) is a labeled infinite tree F, whose vertices are the set ℕ^{∗} of finite sequences of natural numbers. Each vertex is labeled with an implementation F_{τ} of f, and so F determines an infinite system of recursive equations over D,

X_{τ} = F_{τ} (λ(i ∈ ℕ)X_{τi}) (τ ∈ ℕ^{∗}),

where τi is the result of appending i to the end of τ. We let {X̂_{τ} ||| τ ∈ ℕ^{∗}} be the set of mutual fixed points of this system, and put

x̂ = {X̂_{∅} : X̂_{τ} are the simultaneous least fixed points of some F} .

This x̂ ∈ Π(D) is the “canonical” ipf fixpoint of the equation x = f(x), and it is not hard to verify that, indeed, it is a fixed point. The construction of canonical fixpoints for systems of equations with parameters is similar but more complicated, and still very close to [3].

The proof of Theorem A now essentially consists of showing that the standard identities hold in ipf (D). Armed with the axiomatization mentioned in Section 1, it suffices to verify a specific, short list of identities. This method improves on that of [3], both in content (as we can handle arbitrary D and the refined equivalence relation) and in simplicity.

3.1 Comparing ipf (D) and plot(D)

Turning to Theorem B, we first need to define ipf_{0}(D), which is most easily done topologically. So, place the usual Scott topology on all dcpos; note that for algebraic D, a base of this topology is given by the collection of sets N_{D}(e) = {d ∈ D ||| e ≤ d} for e finite. Let ℂ be the Cantor set (all infinite binary sequences) with its usual topology, and call a subset X of D compact-analytic if it is the continuous image of ℂ, i.e., if there is a (topologically) continuous function F: ℂ → D such that F [ℂ] = X. Since ℂ is homeomorphic to the direct product of countably many copies of itself, it is not hard to see that compact-analytic sets are closed under countable direct products and continuous images.

Now restrict attention for the remainder of this section to strongly algebraic D. These are the “SFP objects” of Plotkin [6]; we need just the following properties: If D is strongly algebraic, then there is an increasing sequence D_{0} ⊂ D_{1} ⊂ D_{2} ⋯ of finite sets of finite elements of D whose union is all finite elements of D. Furthermore, there is a family of projections p_{n}: D → D_{n} such that p_{n+1} ∘ p_{n} = p_{n+1} and for all d ∈ D, d = sup_{n} p_{n}(d).

It is not difficult to check that for strongly algebraic D, the compact-analytic subsets of D coincide with the finitely generable ones.^{7} Therefore, think of ipf_{0}(D) as a structure on the compact-analytic subsets of D. To provide the transformations ipf_{0}(D), call an ipf f compact-analytic^{8} if it is generated by a

7 This statement in fact holds for all algebraic D, but the proof requires considerably

more work; see [9]. 8 See also [4].

family of polyfunctions of the form {F_{α}: D^{ℕ} → D ||| α ∈ ℂ} where the function F: ℂ × D^{ℕ} → D via F (α, p) = F_{α}(p) is continuous. These ipfs have implementations continuously parametrized by the Cantor set, which one can think of as a space of “oracles” for the corresponding non-deterministic function. The closure properties of compact-analytic sets guarantee that such an f takes compactanalytic players to compact-analytic players, as f̄(x) = F [ℂ × x^{ℕ}].

It is a fact that the compact-analytic ipfs ipf_{0}(D) and players Π_{0}(D) are closed under composition and recursion, which means that Π_{0}(D), ipf_{0}(D), and the (restriction of) the usual ipf interpretation form an FLR_{0}-structure ipf_{0}(D). The proof of this fact is not difficult from the definitions, and is similar to the portions of Theorems 8.2 and 8.4 of [3] which state that ipf recursion preserves “type.”

Lemma. For x, y finitely generable, x ⊏ ∼ y is equivalent to the conjunction of x ⊑^{u} y and x ⊑′_{l} y, where x ⊑′_{l} y if for every c ∈ x and every finite a ∈ D such that a ≤ c, there exists d ∈ y such that a ≤ d.

Intuitively, x ⊑′_{l} y means that every finite approximation to x is also an approximation to y. This form of ⊏ ∼ will be most useful in the following proofs. Rephrasing Theorem B, part (a), we now wish to show

Claim. For any ipf f and players x and y, all compact-analytic, we have (1) If x ⊏ ∼ y, then f̄(x) ⊏ ∼ f̄(y). This condition means that f̄ takes ≃_{em}-equivalent players to ≃_{em}-equivalent

ones, so it induces a monotone function on the Plotkin powerdomain. (2) The induced function ρ(f) is continuous on the Plotkin powerdomain.

Proof of claim. Let A(d) denote the set of finite elements less than or equal to a given d ∈ D. Since D is algebraic, A(d) is directed and sup A(d) = d. Also let F: ℂ × D^{ℕ} → D be the continuous parametrization of f.

Suppose that a is a finite approximation to an element c ∈ f̄(x). By definition of ipf application, c = F_{α}(X) for some α ∈ ℂ and X: I → x. By continuity of F,

a ≤ c = sup {F_{α}(A) ||| ∀i, A(i) ∈ A(X(i))} .

But a is finite, so some individual term of the right-hand sup must already be beyond a. That is, for a particular sequence A ∈ D^{I} such that A(i) ∈ A(X(i)), we have a ≤ F_{α}(A). Each A(i) is finite below X(i) ∈ x, and hence there is some Y (i) ∈ y such that A(i) ≤ Y (i). Finally, by monotonicity of F_{α}, a ≤ F_{α}(Y) ∈ f̄(y). In other words, f̄(x) ⊑′_{l} f̄(y).

To finish the first part of the claim, show that f̄(x) ⊑^{u} f̄(y): if d = F_{α}(Y) ∈ f̄(y), choose a map X: I → x such that X(i) ≤ Y (i) for each i ∈ I. This is possible since x ⊑^{u} y. Then x ∋ c = F_{α}(X) ≤ F_{α}(Y) = d.

The second part of the claim asserting the continuity of ρ(f) is more delicate. Note it suffices to show that for each point z in the Plotkin powerdomain, there is a sequence of finite elements a_{n} with supremum z such that ρ(f)(z) is the supremum of ρ(f)(a_{n}). Let p_{n}: D → D_{n} be the sequence of projections witnessing that D is strongly algebraic. Choose the set-maximal representative Z^{∗} of z from Π_{0}(D), constructed in section 7 of Smyth [8]. Unsurprisingly, the players A_{n} = p_{n}[Z^{∗}] have ⊏ ∼-supremum Z^{∗}; we shall verify that the supremum of f̄(A_{n}) is f̄(Z^{∗}). The key property of the choice of representative Z^{∗} is that if {b_{i}}_{i∈ℕ} is any increasing sequence with b_{i} ∈ A_{i}, then the supremum of the b_{i} is in Z^{∗}.

Actually, Z^{∗} is a supremum of the A_{n} in the preorders ⊑′_{l} and ⊑^{u}, individually; so we can check that f̄(Z^{∗}) is the supremum of the A_{n} in these two preorders individually, as well. For ⊑′_{l}, the argument goes similarly to the monotonicity argument above, but using the stronger approximation

X = sup_{I′⊆I,|I′|<∞} sup {A ||| A(i) ∈ A(X(i)) and A(i) = ⊥ for i ∉ I′} ,

for a function X: I → Z^{∗}, which results from the pointwise ordering on D^{I}.

To show that f̄(Z^{∗}) is the ⊑^{u}- supremum of the f̄(A_{n}), let Y be any ⊑^{u}- upper bound of the f̄(A_{n}), and choose any member d of Y. Then for each n, there is some α_{n} and map B_{n}: ℕ → A_{n} such that f̄(A_{n}) ∋ F (α_{n}, B_{n}) ≤ d. Now, ℂ is a compact topological space, and every point has a countable neighborhood base, so ℂ is sequentially compact. Therefore we may safely assume that the α_{n} converge as n increases, to some α ∈ ℂ. Next notice that the projections p_{t} “push down” so that F (α_{n}, p_{t} ∘ B_{n}) ≤ d for any t and n as well. By similar compactness arguments (using Tychonoff’s theorem to see that D^{ℕ} is compact), one can choose a subsequence B_{n_{t}} so that for each k ∈ ℕ, the sequence of values p_{t}(B_{n_{t}}(k)) ∈ A_{t} is eventually monotone as t increases. Hence for each k, this sequence converges to Z(k) ∈ Z^{∗}, so that

F (α_{n_{t}}, p_{t} ∘ B_{n_{t}}) → F (α, Z) = c ∈ f̄(Z^{∗}) as t → ∞.

Since each element in the left hand sequence is ≤ d, the limit c ≤ d. Hence every element of Y has an element of f̄(Z^{∗}) below it, as desired. ⊓ ⊔

The previous claim together with the definition that ρ(x) = [x/ ≃_{em}] yields a map from the universe of ipf_{0}(D) to the standard structure over the Plotkin powerdomain of D. The next part of Theorem B states that this map ρ is an FLR_{0}-homomorphism. To see this, it suffices to show that ρ preserves function compositions and systems of recursive equations, since all FLR_{0} expressions are built up from these operations. The fact that ρ(f) ∘ ρ(g) = ρ(f ∘ g) is easy, because ρ(f) depends only on the extension f̄. For recursion, suppose that f(x) is a compact-analytic ipf with player fixed point x̂, and that X is the least fixed point in the Plotkin powerdomain of ρ(f). We wish to prove that X = ρ(x̂) = [x̂/ ≃_{em}]. (The following argument will directly generalize to systems of equations with parameters.)

First, ρ(f) fixes [x̂/ ≃_{em}], since by definition ρ(f)([x̂/ ≃_{em}]) = [f̄(x̂)/ ≃_{em}] and f̄ fixes x̂. Choose a compact-analytic representative x_{0} of X in the Plotkin powerdomain; since X is the least fixed point of ρ(f), this means that x_{0} ⊏ ∼ x̂. On the other hand, we know that f̄(x_{0}) ≃_{em} x_{0} since the ≃_{em}-equivalence class X of x_{0} is fixed by ρ(f). In particular, f̄(x_{0}) ⊏ ∼ x_{0}. To finish the proof, we show that for any compact-analytic player y, f̄(y) ⊏ ∼ y implies that x̂ ⊏ ∼ y:

Suppose f̄(y) ⊏ ∼ y. We shall show separately that x̂ ⊑′_{l} y and x̂ ⊑^{u} y. Let a ≤ ĉ_{∅} ∈ x̂ be a finite approximation to an element of x̂, where ĉ_{∅} is the toplevel fixed point for some implementation system F of f. By induction on k, each iterate c_{τ}^{(k)} of the corresponding fixed point equations satisfies that the singleton {c_{τ}^{(k)}} ⊑′_{l} y. Since a is a finite approximation to ĉ_{∅}, it must be less than or equal

to some top-level iterate c_{∅}^{(K)} of F, which is in turn less than some d ∈ y, as desired.

For x̂ ⊑^{u} y, let d be any element of y. Since f(y) ⊑^{u} y, choose some c ∈ f(y) such that c ≤ d. Now c must be of the form F (d_{1}, d_{2}, …) for some F ∈ f and d_{1}, d_{2}, … ∈ y. Proceeding by induction, once d_{τ} ∈ y is chosen, find some F_{τ} ∈ f and d_{τ ˆ 1}, d_{τ ˆ 2}, … ∈ y so that d_{τ} ≥ F_{τ} (d_{τ ˆ 1}, d_{τ ˆ 2}, …). In this way construct d_{τ} and F_{τ} for all finite sequences from ℕ.

The F_{τ} of course form an implementation system F for the ipf equation x = f(x). This system has least fixed points d̂_{τ} so that the top-level d̂_{∅} ∈ x. But since d_{τ} ≥ F_{τ} (d_{τ ˆ 1}, …), it must be that d_{τ} ≥ d̂_{τ} for all τ, by the general least-fixed-point properties of the d̂_{τ}. In particular, y ∋ d ≥ d̂_{∅} ∈ x as desired.

Only part (c) of Theorem B remains, which says that the homomorphism ρ produces every continuous, essentially monotone function on the Plotkin powerdomain. To prove this part, we must take an arbitrary essentially monotone g: plot(D) → plot(D) and construct a compact-analytic ipf f so that ρ(f) = g. Restated, the goal is to find a continuous function F: ℂ × D^{ℕ} → D such that F [ℂ × x^{ℕ}] ≃_{em} g([x/ ≃_{em}]) for any x ∈ Π_{0}(D). One reasonable approach is to arrange that if X: ℕ → x is surjective and so enumerates x, then F (α, p) will pick out all members of g([x])^{∗} as α varies over ℂ.

This approach calls for a “selection function” S which will take an α ∈ ℂ and some set R of the form R = Y^{∗} and return an element of R, so that

{S(α, R) ||| α ∈ ℂ} = R, for every R.  (14)

The following labeled tree σ which “generates” D will help to construct S. As before, let p_{n}: D → D_{n} be the projections which witness the fact that D is strongly algebraic. The root of σ is labeled with ⊥; if n − 1 levels have been constructed, then the new children of a current leaf σ_{u} should consist of a set of nodes labeled with each element of D_{n} greater than or equal to σ_{u}.

We may assume that σ is actually a perfect, infinite binary tree by replacing each node having k children by a small binary tree with k leaves. Therefore, identify the nodes of σ with finite binary sequences, and the set of branches of σ with the Cantor set. We denote by σ_{α} the supremum of the labels along the αth branch of σ. By construction, σ_{α} varies over all of D as α ranges over ℂ. Moreover, an analogue of this property holds at every node. For any node u, let N(u) denote the set of branches which extend u. Then as α varies over N(u), σ_{α} varies over all elements of D greater than or equal to σ_{u}, i.e., N_{D}(σ_{u}).

Let R = {Y^{∗} : Y ∈ Π_{0}} be the range of the ∗-operation. For the purposes of our proof, any selection function S: ℂ × R → D satisfying (15) will do:

S(α, R) = σ_{α} if σ_{α} ∈ R
∀u such that {σ_{u}} ⊑_{l} R, ∀α extending u, σ_{u} ≤ S(α, R).

(15)

The following construction provides one such S. Fixing an R for the moment, find all minimal u so that no element of R is greater than or equal to σ_{u}. For such a u, let t be its parent. Then R does contain some element greater than σ_{t}, which is exactly to say that {σ_{t}} ⊑_{l} R. Therefore, choose the “leftmost” branch extending t whose limit is in R, and call this limit m_{R,u}.

Now define S(α, R) = m_{R,u} if α ∈ N(u), and S(α, R) = σ_{α}, otherwise. There is at most one initial sequence u of α so that m_{R,u} is defined, and if there is none then σ_{α} ∈ R since R is closed under limits of approximations to itself; these observations ensure that S is well-defined and satisfies properties (14) and (15).

Finally define for X ∈ D^{ℕ}, α ∈ ℂ,

F (α, X) = S(α, g([X[ℕ]])^{∗}),

and let f be the ipf generated by the sections F_{α}. We must prove both that F is continuous and that ρ(f) = g. So, compute the inverse image of a generic neighborhood N_{D}(a) under F, as follows. Let U be the set of all minimal u so that σ_{u} ≥ a. By construction of S,

S^{−1}(N_{D}(a)) = ⋃_{u∈U} N(u) × {R ||| {σ_{u}} ⊑_{l} R} .

Since each N(u) is open in ℂ, we need only show that the collection of all X so that {σ_{u}} ⊑_{l} g([X[ℕ]])^{∗} is open in D^{ℕ}. Fix a u and let b = σ_{u} for convenience of notation. Note first that if {b} ⊑_{l} R, i.e., if ∃d ∈ R s.t. b ≤ d, then there is some finite set of finite elements A ∋ b so that A ⊏ ∼ R. That is, letting B = {[R] : {b} ⊑_{l} R}, then

B = ⋃_{{A finite \atop A∋b}} N_{plot(D)}(A),

and so B is open in plot(D). This means that g^{−1}(B) is also open in plot(D), and hence is of the form

g^{−1}(B) = ⋃_{A∈A′} N_{plot(D)}(A),  (16)

for some collection A′ of finite sets of finite elements of D.

Unfortunately, saying that the range X[ℕ] of a function from ℕ to D is bigger than a given finite set of finite elements A in the order ⊏ ∼ is not an open condition on X, because every value of X must then be greater than or equal to some element of A. The following argument which converts (16) into a collection of neighborhoods in the order ⊑_{l} is therefore the crux of the continuity proof.

Suppose y is given so that A ⊑_{l} y for some A ∈ A′. Clearly one can choose some subset z ⊆ y such that A ⊑^{u} z as well, so that in fact A ⊏ ∼ z. Then g([A]) ⊏ ∼ g([z]), so {b} ⊑_{l} g([A])^{∗} ⊑′_{l} g([z])^{∗}. But g is essentially monotone, so g([z])^{∗} ⊆ g([y])^{∗}, and hence {b} ⊑_{l} g([y])^{∗}, which is to say that g([y]) ∈ B.

Conversely, if there is no A ∈ A′ such that A ⊑_{l} y, then certainly no A ∈ A′ has A ⊏ ∼ y, and so g([y]) ∉ B. Thus equation (16) can be improved to

g^{−1}(B) = ⋃_{A∈A′} {[y] ||| A ⊑_{l} y} .

Finishing the proof of F ’s continuity therefore only requires showing that any set of the form X = {X ∈ D^{ℕ} ||| A ⊑_{l} X[ℕ]} for A a finite set of finite elements is open in D^{ℕ}. But A ⊑_{l} X[ℕ] just means there is some finite set of natural numbers whose images under X meet N_{D}(c) for each c ∈ A. Any candidate set of natural numbers of the appropriate size yields a finite condition on X, and so the entire set X is a union of basic neighborhoods in D^{ℕ}.

It remains to show that ρ(f) = g. If x ∈ Π_{0} and X: ℕ → x, then X[ℕ] ⊆ x. By the essential monotonicity of g, g([X[ℕ]])^{∗} ⊆ g([x])^{∗}. This inequality with

f(x) = ⋃_{X:ℕ→x} F [ℂ × {X}] = ⋃_{X:ℕ→x} g([X[ℕ]])^{∗}

shows that f(x) ⊆ g([x])^{∗}. Equality will be achieved if for some X, X[ℕ] ≃_{em} x. Collecting for each n and each element a of p_{n}[x] some element d_{a} ∈ x with a ≤ d_{a} produces a countable set which is ≃_{em}-equivalent to x. Then an X that enumerates {d_{a}} suffices.

This completes the proof of all three parts of Theorem B, providing a vivid picture of the Plotkin powerdomain as a powerstructure quotient of the player model.

3.2 Countable non-determinism

Since both the ipf structure ipf (D) and the powerdomains for countable nondeterminism plot_{ω}(D) seek to improve on the ability of earlier powerdomains to model fairness, it is natural to compare them. Is there a “countable nondeterminism” analogue of Theorem B? Unfortunately, the answer is “no,” for the simple reason that plot_{ω}(D) does not constitute a powerstructure. The points in plot_{ω}(D) cannot (all) be viewed as subsets of D. In other words, although it still may be true that “direct existence [of plot_{ω}(D)] along the lines of [6, 8] should be established,” as Plotkin [7] suggests, no construction which stays within the subsets of D can accomplish this goal.

Let W be the domain (1_{⊥} × ℕ)_{⊥}, which is just a tree with root ⊥ and countably many branches of length 2. Concretely, we take the elements of W to be ⊥ and all pairs of the form (0, n) or (1, n) for any n ∈ ℕ. The ordering on W is that ⊥ < (0, n) < (1, n) for any n, and these are the only relations. W is very close to being flat, having maximal chain length 3 as opposed to 2. Also, say that one dcpo D embeds another E if there is a projection from D onto a subdcpo D′ ⊆ D such that D′ and E are isomorphic.

Proof of Theorem C. We begin by showing that P = (Π(W)/ ≃_{em}, ⊏ ∼, ⊆) is a σ-semilattice, where ⊆ is the ordinary subset relation (modulo ≃_{em}). First note that since W has only finite elements, ⊏ ∼ is just the conjunction of ⊑^{u} and ⊑_{l} on W. Since every ⊏ ∼-chain in Π(W) has countable length, (Π(W), ⊏ ∼) is a dcpo exactly if it contains a least upper bound for each sequence. Let x_{0} ⊏ ∼ x_{1} ⊏ ∼ ⋯ be such a sequence, and check that its supremum is

x = {sup_{n} a_{n} ||| a_{n} ∈ x_{n}, a_{m} ≤ a_{n} for m ≤ n} .

Next, ⊆ must have least upper bounds of arbitrary countable sets from P. But ⋃_{n} x_{n} is the ordinary ⊆-least upper bound of {x_{n} ||| n ∈ ℕ}, so [⋃_{n} x_{n}/ ≃_{em}] is the least upper bound of {[x_{n}] ||| n ∈ ℕ} on P.

Finally, countable union (i.e., the operation of taking the ⊆-least upper bound of countably many arguments) must be ω_{1}-continuous and binary union must be continuous, with respect to ⊏ ∼. The former is trivial because there are no uncountable chains in P; the latter just requires that whenever x = sup x_{n}, then x ∪ y = sup x_{n} ∪ y, which is easy to check because W only has chains of finite length.

Thus, P is a σ-semilattice; however, it is not free over W. The singleton map would have to be the obvious {·}: w ↦ [{w}]. Now consider the map f from W into the σ-semilattice^{9} Q = (Π(ℕ_{⊥}), ⊏ ∼, ⊆) given by f(⊥) = f(0, n) = {⊥} and f(1, n) = {n}. f is certainly continuous, and so if P were free, f would have to factor through the singleton map. The values of F at singletons determine all its other values, since F must preserve countable unions and W is itself countable. Therefore, the only possibility for F turns out to be

F (A) = \{ \begin{matrix}\{n ||| (1, n) ∈ A\} & if A ∩ (\{⊥\} ∪ \{(0, n) ||| n ∈ ℕ\}) = ∅, \\ \{n ||| (1, n) ∈ A\} ∪ \{⊥\} & otherwise. \end{matrix}

But this map F is not continuous (on the “dcpo” part (Π(W), ⊏ ∼) of the semilattices), which is a contradiction. To see the non-continuity, consider the sets H_{k} = {(1, n) ||| n < k}∪{(0, n) ||| n ≥ k}. Clearly the H_{k} are increasing in ⊏ ∼, and have least upper bound H = {(1, n) ||| n ∈ ℕ}. But F (H_{k}) = {⊥, 0, 1, …, k − 1} so that sup_{k} F (H_{k}) = {⊥}∪ℕ, whereas F (H) = ℕ is strictly bigger than {⊥}∪ℕ in Q. (Intuitively, the true free σ-semilattice over W will have to include some “ideal” element, not corresponding to any set, to be the least upper bound of the sequence {H_{k}}_{k∈ℕ}.)

Assume by way of contradiction that the free σ-semilattice S over W is the homomorphic image of (Π(W), ⊏, ⊆) for some partial order ⊏. The homomorphism induces some equivalence relation ∼ on Π(W), so that S = (Π(W)/∼, ⊏ /∼, ⊆ /∼), with singleton map w ↦ {w} /∼. Since P is a σ-semilattice and the map w ↦ [{w}] ∈ P is continuous, there is a σ-semilattice map ϕ: S → P so

9 See Plotkin [7] for a proof that this is the free σ-semilattice over ℕ_{⊥}; the proof that it is simply a σ-semilattice is analogous to the proof for W.

that the following diagram commutes:

\begin{matrix}W \\ \{·\} ↓ & ↘ \{·\} \\ S & →^{ϕ} & P \end{matrix}

Now, w ↦ [{w}] ∈ P is an injective map, so the singleton map into S must be as well, i.e., ∼ cannot identify any singletons. Since the subset relation in S is ordinary subset (modulo ∼), the ⊂-lub of a countable set A of singletons in S is just {w ||| {w} ∈ A} /∼. Since W is countable, every element of S is produced in this way, and since ϕ must preserve ⊆, this means that the map ϕ is simply given by

ϕ(x/∼) = [x] ∈ P

for any x ∈ Π(W). Thus ϕ is clearly surjective. Suppose that ϕ(x/∼) = ϕ(y/∼), which means that x is equivalent to y under ⊏ ∼. Write x as {a_{0}, a_{1}, …} and y = {b_{0}, b_{1}, …} possibly with repetitions so that a_{i} ≤ b_{i}. Since the singleton map to S is monotone, and countable union in a σ-semilattice is monotone, this representation of x and y shows that x/∼ ⊏ y/∼. Symmetrically, y/∼ ⊏ x/∼, so that ϕ is injective as well. Hence ϕ is an isomorphism of σ-semilattices witnessing S ≅ P. But P is not free over W.

This argument proves the theorem for D = W. To extend to the case that D embeds W, just notice that any representation of the free σ-semilattice over D in the given form would yield such a representation of the free σ-semilattice over W by taking a quotient under the projection from D to W. ⊓ ⊔

References

1. M. Hennessy and G. D. Plotkin, “Full abstraction for a simple parallel programming language,” Proceedings of MFCS, Lecture Notes in Computer Science 74, ed. J. Becvar, Berlin: Springer-Verlag (1979) 108–120.

2. Y. N. Moschovakis, “A game-theoretic modeling of concurrency,” Extended abstract, Proceedings of the fourth annual symposium on Logic in Computer Science, IEEE Computer Society Press (1989) 154–163.

3. Y. N. Moschovakis, “A model of concurrency with fair merge and full recursion,” Information and Computation 93 (1991) 114–171.

4. Y. N. Moschovakis, “Computable, concurrent processes,” Theoretical Computer Science (to appear).

5. D. Park, “On the semantics of fair parallelism,” Proc. Copenhagen Winter School, Lecture Notes in Computer Science 104, Berlin: Springer-Verlag (1980) 504–526.

6. G. D. Plotkin, “A powerdomain construction,” SIAM J. of Comput. 5 (1976) 452– 487.

7. G.D. Plotkin, “A powerdomain for countable non-determinism,” Automata, Languages, and Programming 9th Colloquium, Lecture Notes in Computer Science 140, eds. M. Nielsen and E. Schmidt, Berlin: Springer-Verlag (1982) 418–428.

8. M. B. Smyth, “Power Domains,” J. Comput. System Sci. 16 (1978) 23–36.

9. G. T. Whitney, “Recursion Structures for Non-Determinism and Concurrency, ” Ph.D. Thesis, University of California, Los Angeles (1994).

This article was processed using the L^{A}TEX macro package with LLNCS style