The Synthetic Plotkin Powerdomain

Wesley Phoa  Paul Taylor

1990

Abstract

Plotkin [1976] introduced a powerdomain construction on domains in order to give semantics to a non-deterministic binary choice constructor, and later [1979] characterised it as the free semilattice. Smyth [1983] and Winskel [1985] showed that it could be interpreted in terms of modal predicate transformers and Robinson [1986] recognised it as a special case of Johnstone’s [1982] Vietoris construction, which itself generalises the Hausdorff metric on the set of closed subsets of a metric space. The domain construction involves a curious order relation known as the Egli-Milner order.

In this paper we relate the powerdomain directly to the free semilattice, which in a topos is simply the finite powerset, i.e. the object of (Kuratowski-)finite subobjects of an object. We show that the Egli-Milner order coincides (up to “¬¬”) with the intrinsic order induced by a family of “observable predicates.”

This problem originally arose in the context of the Effective topos, in which the observable predicates are the recursively enumerable subsets. However we find that the results of this paper hold for any elementary topos, and so by considering a (pre)sheaf topos (which the Effective topos is not) we may compare them with the classical approach.

Important Note: Much of the credit for the work in this paper is due to Wesley Phoa and Martin Hyland, but I take the blame for its presentation. Comments on it are most welcome. When it is finished it will be submitted as a joint paper with Wesley Phoa, and an announcement will be made on types.

1 Introduction

1.1 The Plotkin powerdomain

Plotkin [1976] introduced his powerdomain construction in order to extend denotational semantics in the Scott style to languages involving a binary choice, or. The behaviour of a program in such a language may be that:

• it always diverges;

• it always terminates, and with the same output value;

• it always terminates, but there are several (but finitely many) possible output values;

• it sometimes converges and sometimes diverges;

and so to express its denotation we must consider the set of possible outputs. Divergence must be mentioned explicitly as a value if it occurs in order to distinguish the third and fourth cases. The set must be nonempty since there must be some behaviour — divergence if nothing else. Incidentally, by König’s lemma, if there are infinitely many possible output values, then divergence must also be possible.

By analogy with the powerset, Ω^{X}, one might suppose that the powerdomain would be of the form T^{X} for some “truthvalues” domain T. There are two objections to this: First, the class of admissible subobjects would then be closed under inverse images, so including “infinite” subobjects. Second, the subobjects themselves would be upwards-closed (on the reasonable assumption that the generic such set is a maximal element of T), but we want {⊥} to be admissible.

The central theme of denotational semantics is that each program constructor should correspond to an algebraic operation in the domain. In particular since or is a conjunction of nondeterministic behaviours, it must correspond to a binary operation ⋓ on the domain. In the natural understanding, this must be commutative, associative, idempotent and computable, so the nondeterministic domain must be a semilattice (A, ⋓) in the category of domains. Moreover since every deterministic program is nondeterministic in a trivial way, there is an inclusion of the deterministic domain X into the nondeterministic one. Indeed Hennessy and Plotkin [1979] argued that (A, ⋓) has to be the free semilattice on X.

There is another approach to semantics, which is axiomatic: we argue about the properties of programs. We have already informally said that a program may or must diverge: these are modalities on propositions concerning its actual behaviours in any particular run. Smyth [1983] showed how a program p (in particular a non-deterministic one) can be interpreted as a predicate transformer from post-conditions to the weakest corresponding pre-condition. Winskel [1985] characterised the powerdomain in terms of the properties it could express in a logic which includes these transformers [p] and ⟨p⟩ as unary operators. Robinson [1986] did something slightly different: he treated the modal predicates □ ϕ and ♢ ϕ as abstract symbols and showed that they generate the topology (i.e. the lattice of properties) on the powerdomain A as ϕ ranges over the open sets of the base domain X. In fact the point of Robinson’s paper was to show that the powerdomain is a special case of Johnstone’s [1982] Vietoris monad, which had already been generalised from a construction on metric spaces due originally to Hausdorff.

These axiomatic and topological approaches are very significant in the literature, but for two reasons we have not attempted to make use of them in this paper. First, Johnstone showed that the Vietoris construction and the free semilattice agree only in special cases (admittedly including all those of interest in classical domain theory), and our problem is likely to be as difficult as his. Secondly, the analogy with topology is not strict (in particular we do not assume all joins), so it is not yet clear what a “Σ-frame” should be.

1.2 Synthetic domain theory

(To be written)

1.3 The synthetic Plotkin powerdomain

Throughout we shall use the word “set” to mean an object of a given elementary topos, E. We suppose that we have a category C of predomains which is a full reflective subcategory of the category of sets. Then

• arbitrary limits of predomains exist (which is not true of most of the classical categories of domains) and are constructed “set-theoretically”

• we may perform some type construction with sets (for instance, in our case the Plotkin powerdomain is the free semilattice) and turn the result into a predomain.

Definition 1.1 A semilattice is a set A ∈ E together with a (global) element ⊚ ∈ A and a binary operation ⋓ : A × A → A which is

• idempotent: a ⋓ a = a,

• commutative: a ⋓ b = b ⋓ a,

• associative: a ⋓ (b ⋓ c) = (a ⋓ b) ⋓ c, and

• ⊚ is the unit: a ⋓ ⊚ = a = ⊚ ⋓ a.

We shall find that ⊚ is an inessential part of the structure, so we define a binary semilattice to be an algebra (A, ⋓) without the unit.

It is easy to see that

a ⋐ b ⟺^{def} a ⋓ b = b

defines a partial order (reflexive, transitive antisymmetric relation), and in fact ⋓ is the join for this. However it is important not to consider (A, ⋓) as specifically a join-semilattice (or as a meet-semilattice), because ⋐ is not what we shall mean by the intrinsic order on the set A (see section 2): it is intrinsic to the semilattice, not to the set.

The definition of a semilattice can be expressed in any category with finite products, so we write SL(−) for the category of semilattices in any such. Then we have forgetful functors

\begin{matrix}SL(C) & \overline{V} & C \\ SL(E) & \begin{aligned}U \\ & \end{aligned} & [figure: .; .; .; .; .; .; .; .; .; .; .; ^{K....................}; ⊥; V] & E & \begin{aligned}T & . . . . . . . . . . . . . . . . . \\ & ⊣ \begin{matrix}U \\ \end{matrix}∩ \end{aligned} \end{matrix}

two of which (we shall show) have left adjoints (indicated by dotted arrows). From K and T, it is a simple categorical argument to derive the other two adjoints.

Proposition 1.2 The left adjoint to SL(C) → SL(E) is given by the reflector T : E → C. Proof Explicitly, if (A, ⋓) is a (binary) semilattice, then the free C-semilattice on it is (T A, T ⋓). To make this meaningful we need

T A × T A ≅ T (A × A)

i.e. T preserves finite products: × itself is unambiguous because products in a reflective subcategory are always calculated as in the larger category. By functoriality this is a C-semilattice. If f : (A, ⋓) → (B, ⋓′) is a homomorphism into a C-semilattice then the underlying map has a lifting f̄: T A → B and this is a homomorphism because ⋓′ ∘ (f̄× f̄) and f̄∘ T ⋓ both serve as the unique lifting of ⋓′ ∘ (f × f) = f ∘ T ⋓, again using the fact that T preserves binary products. The argument for the unit, ⊚, is similar, using the terminal object. □

Theorem 1.3 The left adjoint to SL(C) → C is given by T ∘ K ∘ U. Proof Let X ∈ C and (A, ⋓) ∈ SL(C). We have to show a natural bijection between maps f : X → A and homomorphisms T (K(X), ∪) → (A, ⋓); it doesn’t matter whether we work in C or E because the former is a full subcategory of the latter. But T ∘ K ⊣ V ∘ U. □

So in order to construct the synthetic Plotkin powerdomain it suffices

• to define our categories of sets and domains, and show that the latter is a full reflective subcategory of the former and that the reflector preserves finite products,

• to show that the finite powerset affords the free semilattice in the category of sets.

These two topics will be the subject of sections 2 and 3 respectively.

This abstract nonsense, however, tells us little about the concrete structure of the powerdomain, and the main purpose of the paper is to show that the Egli-Milner order is (almost) the intrinsic order relation on it. In other words, the synthetic construction is the same as the concrete one. Section 4 shows one implication, and with the help of modal operators (section 5) we prove a weak form of the converse in section 6.

2 The intrinsic order

As usual, we use Ω to denote the object of truth values in E, and we shall also assume given a sublattice Σ ⊂ Ω whose elements we shall think of as “computable predicates.” In section 6 we shall need to assume that these predicates are ¬¬-closed, i.e. ¬¬ϕ ⇒ ϕ.

If we look at a parametric case it will become more reasonable to the intuition why Ω is a very complex object, much larger than the set 2 = {true, false} of decidable truthvalues or even than a typical choice of Σ. A map ϕ : ℕ → Ω is a predicate ϕ(n) on natural numbers, and as such it may perhaps be primitive recursive, recursively decidable, recursively enumerable, Π_{2}^{0} or worse. In fact the parameter is irrelevant and so using the Kleene bracket notation we can define

Σ = {ϕ ∈ Ω : ∃n.({n}(0)↓ ↔ ϕ)}

the object of recursively enumerable predicates.

Although this is the intended application, it is easier to grasp the intuition if you think of “open” instead of “computable” predicates. For this purpose the reader is invited to apply the following definitions to the topos Set^{C^{op}} where C is the category of countably based algebraic lattices and Scott-continuous maps and Σ is (the representable functor on) the two-point lattice. In this case a sieve (i.e. a subobject of a representable) is generated by the inclusion of an open set iff its characteristic function factors through Σ.

Given Σ, we can define the “intrinsic order:”

Definition 2.1 For any object X ∈ E and x, y ∈ X, write

x ⊑ y ⟺^{def} ∀ϕ ∈ Σ^{X}.ϕ(x) ⇒ ϕ(y)

This says that every computable property possessed by x is shared by y, so y is “more defined” than x. Clearly ⊑ is reflexive and transitive, but it need not be antisymmetric.

Examples 2.2 • if Σ = Ω then this order is discrete, i.e. x ⊑ y ⟺ x = y.

• if Σ = {⊤, ⊥} then the (pre)order is the finest decidable equivalence relation on X.

• in the topological example, (the externalisation of) ⊑ is exactly the specialisation order (on generalised points of representables).

• ⊥ ⊑ ⊤ in Σ [spell out]

Lemma 2.3 Every function is monotone with respect to this order. □

Unfortunately it is difficult to deduce very much about ⊑ on a power X^{I} from the order on X without additional assumptions, but we do have the expected result for binary product:

Lemma 2.4 For x_{1}, x_{2} ∈ X and y_{1}, y_{2} ∈ Y, we have ⟨x_{1}, y_{1}⟩ ⊑ ⟨x_{2}, y_{2}⟩ in X × Y iff x_{1} ⊑ x_{2} in X and y_{1} ⊑ y_{2} in Y. □

Traditional domain theory begins with posets — sets with an imposed order relation — and then considers extra conditions such as bottom and joins of chains. The idea here is to follow the same course, but starting from the intrinsic order relation on all sets, which is automatically preserved by all functions. Domains are then just special sets but with ordinary functions.

This point of view is analogous to the topological approach to domain theory, for which Vickers [1989] is an excellent introduction. A map X → Σ plays the rôle of an open set of X and ⊑ is antisymmetric iff X is T_{0} in this topology. The point ⊥ is characterised as being in no open set save the whole space, and sobriety is analogous to (but stronger than) directed-completeness. Note, however, that the class of Σ-subsets is in general not closed under arbitrary unions.

Definition 2.5 A Σ-space is an object X for which ⊑ is antisymmetric; it is focal^{1} if it has a least element ⊥ in this order.

Examples 2.6

• If Σ = Ω, every object is a Σ-space, but only the terminal object is focal.

• If Σ = {⊤, ⊥}, an object is a Σ-space iff (the equality predicate on) it is decidable, and again only the terminal object is a focal Σ-space.

• In a Scott topos, every representable object is a Σ-space, and is focal iff it has a bottom in the specialisation order.

• In the Effective topos, all Σ-spaces are modest sets (but not conversely) and hence definable by partial equivalence relations on ℕ.

It is not difficult to see that X is a Σ-space iff the map

ϵ_{X} : X → Σ^{Σ^{X}}  by  x ↦ λf.fx

is mono. This suggests forming the epi-mono factorisation of ϵ_{X}: we shall show that this does in fact give the reflection of X into the full subcategory of Σ-spaces.

Lemma 2.7 Let p : X → Y. Then • the induced map Σ^{p} : Σ^{Y} → Σ^{X} is split epi iff p factors into ϵ_{X}.

1For topological spaces, this term is due to Peter Freyd.

• if Σ^{p} is mono and X is focal then Y is focal and p preserves ⊥. □

Proposition 2.8 Let X →^{p_{X}} T X →^{e_{X}} Σ^{Σ^{X}} be the epi-mono factorisation of ϵ_{X}. Then T defines the reflection into the full subcategory of Σ-spaces, and also preserves the property of being focal. □

In order to be able to construct the powerdomain we need another property:

Proposition 2.9 T preserves finite products. □

So much for the synthetic analogue of posets; for (pre)domains we need some kind of either directed-completeness or sobriety. There are several different candidates for this, some of which are considered by the first author in [1990], but in this paper we prefer not to be drawn into this discussion. However in the proofs of the previous results the important property was being epi with respect to maps into Σ, and by isolating this we obtain easily a good notion, due to Martin Hyland, which suffices for our purposes (in fact we shall make no further use of it).

Definition 2.10 p : X → Y is called Σ-epi if it induces a mono Σ^{p} : Σ^{Y} → Σ^{X} and Σanodyne if this is an isomorphism. The object X is Σ-replete if the only Σ-anodyne maps p : X → Y are isomorphisms.

Proposition 2.11 Every object X has a Σ-replete reflection, SX, and S preserves finite products. □

In the topological example, a representable is Σ-replete iff it is sober, and in this case the specialisation order has directed joins.In the Effective Topos Σ-replete also implies that ωsequences have joins, although the proof makes crucial use of Markov’s Principle and Church’s Thesis.

3 The finite powerset

In order to construct free algebras it is in general necessary to assume that the topos E has a natural numbers object ℕ (since that is itself a free model). However the powerset Ω^{X} of a set X ∈ E is already the free internally-complete ⋃-semilattice on X, even when E itself fails to have infinitary colimits or a natural numbers object.

Since Ω^{X} has I-indexed joins for all I ∈ E, in particular it has nullary and binary ones, usually written ∅ and U ∪ V respectively, so it is a (finitary) ∪-semilattice.

Notation 3.1 Let K(X) ⊂ Ω^{X} denote the smallest subset which

• contains the empty set ∅ ∈ Ω^{X}

• contains the singletons {} : X ↪ Ω^{X} and

• is closed under binary unions ∪ : Ω^{X} × Ω^{X} → Ω^{X}.

So, to prove properties of K(X) we consider the class L ⊂ K(X) of sets which possess the property and show that it includes ∅ and singletons and is closed under binary unions.

If U ∈ K(X) for some X, we say U is Kuratowski-finite. On the assumption that the topos E has a natural numbers object ℕ, a set is Kuratowski-finite iff locally^{2} it has an enumeration

U = {x_{1}, …, x_{n}}

possibly including repetitions for some n ∈ ℕ, i.e. there is a surjection [n] ↠ U. Hence the class of Kuratowski-finite sets is closed under quotients, although not under subobjects. For an account of this characterisation, the reader is referred to Johnstone [1977]. Although it is useful intuition, we prefer not to make our proofs rely on it as it is more complicated to express categorically.

Proposition 3.2 K(X) is the free semilattice on X. Proof Let (A, ⋓, ⊚) be any semilattice; we are going to construct the structure map α : K(A) → A. Consider the set

C = {⟨U, a⟩ ∈ Ω^{A} × A : (∀u ∈ U.u ⋐ a) ∧ (∀b ∈ A.(∀u ∈ U.u ⋐ b) ⇒ a ⋐ b)}

and let

D = {U ∈ Ω^{A} : ∃a ∈ A.⟨U, a⟩ ∈ C}

Then by antisymmetry of ⋐, the projection π_{0} : C ↠ D is an isomorphism; also

• ⟨{} , id⟩ : A → Ω^{A} × A factors through C,

• ⟨∅, ⊚⟩ ∈ C and

• if ⟨U, a⟩, ⟨V, b⟩ ∈ C then ⟨U ∪ V, a ⋓ b⟩ ∈ C

Hence K(A) ⊂ D and the components of

α : K(A) ⊂ D ≅ C ⊂ Ω^{A} × A ⟶^{π_{1}} A

are semilattice homomorphisms. Moreover α ∘ {} = id because

α {a} = π_{1}⟨{a} , a⟩ = a

Hence if we are given any function f : X → A we may factor it through {} : X ↪ K(X) by the semilattice homomorphism

f̃ =^{def} α ∘ K(f)  where  K(f)(U) =^{def} {f(u) : u ∈ U}

(so essentially f̃(U) = ⋃ ∪{f(u) : u ∈ U}). This factorisation is unique, since given two such we may form their equaliser E ⊂ K(X), which is a sub-semilattice containing X and hence the whole. □

2The number n is not a constant, but is parametrised by v ∈ V, where V is some supported object (see next footnote). The indices i of the enumeration are similarly functions i : V → ℕ such that ∀v.1 ≤ i(v) ≤ n(v).

For example if E = Set^{G} for some group G, any finite set with a G-action is Kuratowski-finite, but (constant)

numerals [n] and their quotients carry the trivial action.

The following simple but important result is true of the free functor of any finitary algebraic theory:

Lemma 3.3 The functor K : E → E preserves surjectivity. Proof Let f : Y ↠ X in E, i.e.

∀x ∈ X.∃y ∈ Y.f(y) = x

Consider the set

L = {U ∈ K(X) : ∃V ∈ K(Y).K(f)(V) = U}

• It contains the singletons because for U = {x} we are given ∃y ∈ Y.f(y) = x, so put V = {y} and then K(f)(V) = {fy} = U.

• It contains the empty set because K(f)(∅) = ∅

• It is closed under unions because if U_{1} = K(f)(V_{1}) and U_{2} = K(f)(V_{2}) then U_{1} ∪ U_{2} = K(f)(V_{1}) ∪ K(f)(V_{2}) = K(f)(V_{1} ∪ V_{2}).

and so L = K(X), i.e. ∀U ∈ K(X).∃V ∈ K(Y).K(f)(V) = U. □

Corollary 3.4 (“Weak Axiom of Finite Choice”) Let U ⊂ X be finite (i.e. U ∈ K(X)) and let ϕ(x, f) be a predicate on X × F such that

∀u ∈ U.∃f ∈ F.ϕ(u, f)

Then there is a finite set of pairs V ⊂ U × F such that

∀u ∈ U.∃f ∈ F.⟨u, f⟩ ∈ V and ∀⟨u, f⟩ ∈ V.ϕ(u, f)

Proof Apply the Proposition to the projection

π_{0} : {⟨u, f⟩ ∈ U × F : ϕ(u, f)} ↠ U

and consider U ∈ K(U). □

Notation 3.5 Let K^{+}(X) ⊂ Ω^{X} be generated by the singletons and ∪ (not ∅). By a binary semilattice we mean an algebra (A, ⋓) with an idempotent, commutative and associative binary operation (but no unit).

Proposition 3.6

• K^{+}(X) is the free binary semilattice on X,

• any U ∈ K^{+}(X) is supported,^{3} i.e. ∃u ∈ U.⊤, and

• K(X) = K^{+}(X) + {∅} (the disjoint union).

3Being supported is the internal way of saying that a set has an element; diagrammatically, U ↠ 1. It need not be inhabited, i.e. have a global element 1 → U.

Proof The first part is exactly similar to what we did before. The subset L ⊂ K^{+}(X) of supported sets includes the singletons and is closed under ∪ so is all of it. Finally K^{+}(X)+{∅} carries a (⋓, ⊚)-semilattice structure, so there are mediators K(X) ⇆ K^{+}(X) + {∅}; the universal properties (coproduct and free semilattice) make these mutually inverse. □

So the finite powerset, like the Hausdorff and Vietoris constructions but unlike the full powerset Ω^{X}, falls into two parts. This means that, given a Kuratowski-finite set, there is a constructive procedure to determine whether it is empty or inhabited. The Plotkin construction only defined the larger part anyway because the empty set of process behaviours is not meaningful in denotational semantics.

4 The Egli-Milner order

Since the order on A × A is pointwise, we have

Lemma 4.1 If a_{1} ⊑ a_{2} and b_{1} ⊑ b_{2} in a semilattice (A, ⋓) then a_{1} ⋓ b_{1} ⊑ a_{2} ⋓ b_{2}. □

Here it is important to remember the distinction between the two order relations: the similar result for ⋐ is trivial.

Let S be a Kuratowski-finite set; informally, we can think of it as the word s_{1} ⋓s_{2} ⋓⋯⋓s_{n} for some n ∈ ℕ (where the s_{i} are not necessarily distinct). Now suppose that T is another finite set and the relation

(∀s ∈ S.∃t ∈ T.s ⊑ t) ∧ (∀t ∈ T.∃s ∈ S.s ⊑ t)

holds; this is called the Egli-Milner order, written S ⊑_{EM} T. Then for each i we have some t′_{i} ∈ T with s_{i} ⊑ t′_{i}. Similarly T is the word t_{1} ⋓ ⋯ ⋓ t_{m} and we have s′_{j} ⊑ t_{j} with s′_{j} ∈ S. Then

(s_{1} ⋓ ⋯ ⋓ s_{n}) = (s_{1} ⋓ ⋯ ⋓ s_{n}) ⋓ (s′_{1} ⋓ ⋯ ⋓ s′_{m}) ⊑ (t′_{1} ⋓ ⋯ ⋓ t′_{n}) ⋓ (t_{1} ⋓ ⋯ ⋓ t_{m}) = (t_{1} ⋓ ⋯ ⋓ t_{m})

using the semilattice equations for the equalities and ⊑-monotonicity of ⋓ for the inequality.

Now each of the authors who have discussed the Egli-Milner order have given motivations for it (from Computer Science), which one may or may not find convincing. However a little consideration of pure category theory shows how it is forced upon us. For each object X ∈ E we have

[⊑] =^{def} {⟨s, t⟩ ∈ X × X : s ⊑ t}

which internalises the order relation. We write p, q : [⊑] ⇉ X for the projections, and of course one is pointwise less than the other.

Now apply the functor K. What is this order^{4} K[⊑] ⇉ KX? An instance of it is a finite set V of pairs ⟨s, t⟩ with s ⊑ t; then let

S =^{def} K(p)(V) = {s ∈ X : ∃t ∈ X.⟨s, t⟩ ∈ V }

and

T =^{def} K(q)(V) = {t ∈ X : ∃s ∈ X.⟨s, t⟩ ∈ V }

4In fact K[⊑] → K(X) × K(X) is not mono, but this doesn’t matter; shortly we shall show that its image is [⊑_{EM}].

so we have S ⊑_{EM} T. We shall now give a purely categorical proof that it implies the Σorder. The first result (like preservation of surjectivity) is true of the free functor of any finitary algebraic theory.

Lemma 4.2 The functor K preserves the (pointwise) ⊑ relation. Proof We are given p, q : Y ⇉ X satisfying ∀y ∈ Y.p(y) ⊑ q(y). Consider the set

L = {V ∈ K(Y).K(p)(V) ⊑ K(q)(V)}

Then

• K(p)({y}) = {py} ⊑ {qy} = K(q)({y}) by monotonicity of {} : X → K(X),

• K(p)(∅) = ∅ = K(q)(∅) and

• if K(p)(V_{1}) ⊑ K(q)(V_{1}) and K(p)(V_{2}) ⊑ K(q)(V_{2}) then using the Corollary,

K(p)(V_{1} ∪ V_{2}) = K(p)(V_{1}) ∪ K(p)(V_{2}) ⊑ K(q)(V_{1}) ∪ K(q)(V_{2}) = K(q)(V_{1} ∪ V_{2})

so L = K(Y), i.e. ∀V ∈ K(Y).K(p)(V) ⊑ K(q)(V). □

Lemma 4.3 If S, T ∈ K(X) with S ⊑_{EM} T then there is some V ∈ K[⊑] with K(p)(V) = S and K(q)(V) = T. Proof We use the weak axiom of finite choice with the finite set S and the predicate s ⊑ t on S × T to find V_{1} ∈ K(S × T) with

∀s ∈ S.∃t ∈ T.⟨s, t⟩ ∈ V_{1}

and similarly V_{2} ∈ K(S × T) with

∀t ∈ T.∃s ∈ S.⟨s, t⟩ ∈ V_{2}

Then V_{1}, V_{2} ∈ K[⊑] with

K(p)(V_{2}) ⊂ K(p)(V_{1}) = S  and  K(q)(V_{1}) ⊂ K(q)(V_{2}) = T

Finally put V = V_{1} ∪ V_{2}. □

Proposition 4.4 For S, T ∈ K(X), if S ⊑_{EM} T then S ⊑ T in K(X). □

Corollary 4.5 ⊑ is not necessarily antisymmetric, but if X has a least element ⊥ in this order then K^{+}(X) has a least element {⊥}. Proof

• Let X = Σ × Σ and consider the finite sets

S =^{def} {⟨⊥, ⊥⟩, ⟨⊤, ⊥⟩, ⟨⊤, ⊤⟩}  and  T =^{def} {⟨⊥, ⊥⟩, ⟨⊥, ⊤⟩, ⟨⊤, ⊤⟩}

Then we have both S ⊑_{EM} T and T ⊑_{EM} S, so by the Proposition S ⊑ T and T ⊑ S in K(X). However neither is a subset of the other, so they’re certainly not equal.

• Any T ∈ K^{+}(X) is supported, i.e. ∃y ∈ T.⊥ ⊑ y, so {⊥} ⊑_{EM} T and hence {⊥} ⊑ T. □

5 Modalities

We want to derive a property of ⊑ on X (which is defined in terms of maps ϕ : X → Σ) from ⊑ on K(X) (which is defined in terms of ψ : K(X) → Σ). Therefore we need a way of generating computable properties of finite sets from those of elements.

Lemma 5.1 Let ϕ(x) be a Σ-predicate in x ∈ X. Then

♢ ϕ(U) =^{def} ∃u ∈ U.ϕ(u) and □ ϕ(U) =^{def} ∀u ∈ U.ϕ(u)

are Σ-predicates in U ∈ K(X). Proof Treating Σ as respectively an ∨- and an ∧-semilattice, these predicates are the mediators from K(X), the free semilattice, of the maps ϕ : X → Σ. □

□ ϕ concerns inevitable behaviour of a process (containment in Johnstone’s topological setting, where he writes “t(ϕ)”) and ♢ ϕ possible behaviour (non-empty intersection, “m(ϕ)”). In the rest of our discussion of the modal operators, the predicates to which they are applied are not necessarily computable, unless explicitly stated. In fact we shall simply find □_{S} a convenient abbreviation for ∀s ∈ S, and similarly ♢_{S}, □_{T} and ♢_{T}, but this notation already illustrates that when we use the modal operators for several variables, we more or less end up using quantifiers anyway.

Lemma 5.2 □ ⊤ = ⊤, □(ϕ ∧ ψ) = □ ϕ ∧ □ ψ and ♢ ⋁_{i∈I} ϕ_{i} = ⋁_{i∈I} ♢ ϕ_{i}. □

Definition 5.3 A family {ϕ_{i} : i ∈ I} of predicates is directed if

• ∃i ∈ I.⊤,

• ∀i, j ∈ I.∃k ∈ I.ϕ_{i} ⇒ ϕ_{k} ∧ ϕ_{j} ⇒ ϕ_{k}.

In this case we write ⋁ ; ϕ_{i} for their join^{5}. These two axioms are of course the nullary and binary forms of the more general

∀U ∈ K(I).∃j ∈ I.∀i ∈ U.ϕ_{i} ⇒ ϕ_{j}

which is shown to be equivalent by the same methods as before.

Lemma 5.4 □ is continuous, i.e. if {ϕ_{i} : i ∈ I} is a directed family of predicates then

□ ⋁ ; _{i∈I}ϕ_{i} = ⋁ ; _{i∈I}□ ϕ_{i}

Proof (⇐ follows from monotonicity of □.) For U ∈ K(X) we must show

∀u ∈ U.∃i ∈ I.ϕ_{i}(u) ⊢ ∃j ∈ I.∀u ∈ U.ϕ_{j}(u)

i.e. a “uniformity” result. For this we use the “weak axiom of finite choice” to obtain a finite set V ⊂ U × I such that

∀u ∈ U.∃i ∈ I.⟨u, i⟩ ∈ V  and  ∀⟨u, i⟩ ∈ V.ϕ_{i}(u)

5Not necessarily a Σ-predicate.

So by the general statement of directedness of I we have j ∈ I with

∀⟨u, i⟩ ∈ V.ϕ_{i} ⇒ ϕ_{j}

So ∃j ∈ I.∀u ∈ U.ϕ_{j}(u) as required. □

Remark 5.5 It seems that the dual result, cocontinuity of ♢, can only be proved by contradiction. This is a pity, because it is what we really want to use.

Finally there are two properties which relate the two modalities:

Lemma 5.6 □ ϕ ∧ ♢ ψ ⇒ ♢(ϕ ∧ ψ) and □(ϕ ∨ ψ) ⇒ □ ϕ ∨ ♢ ψ. Proof The first is obvious; for the second show that the set of finite sets satisfying it contains ∅ and the singletons and is closed under ∪. □

Johnstone defines the Vietoris locale V(A) of an arbitrary locale A as the free frame generated by symbols {□ a, ♢ a : a ∈ A} subject to these six relations. He shows that this is part of a monad defined on the category of locales, and that every algebra for this monad carries a (localic) semilattice structure. However the correspondence between the Vietoris and free semilattice constructions is only exact in special cases, so we do not expect it to hold in our setting.

Lemma 5.7 K^{+}(X) ⊂ K(X) is characterised by the imposition of either of the equivalent additional relations

□ ⊥ = ⊥ or ♢ ⊤ = ⊤

Proof The second is ∃x ∈ U.⊤, which is just the definition of being inhabited, whilst the first, ⊥ ⟺ ∀x ∈ U.⊥, is clearly equivalent. □

In the context of locales or Σ-predicates we do not consider negation, but of course it is defined for general predicates and we need to know how the modal operators relate to it. It is an easy exercise in natural deduction to show that ¬¬(ϕ ∧ ψ) ⟺ (¬¬ϕ) ∧ (¬¬ψ).

Lemma 5.8 ¬ ♢ ≡ □ ¬ and ¬¬ □ ≡ □ ¬¬. Proof The first follows immediately from the definitions as quantifiers, whilst the second holds because □ is really finite conjunction. Let L ⊂ K(X) be the class of finite sets U for which ¬¬ □ ϕ(U) ≡ □ ¬¬ϕ(U). Then L contains ∅, singletons and binary unions. □

6 Sigma implies not not Egli-Milner

As we said in section 2, we need an additional assumption:

every ϕ ∈ Σ is ¬¬-closed, i.e. ¬¬ϕ ⇒ ϕ

In the Effective Topos, where ϕ is of the form ∃n.f(n) = 1 for some f : ℕ → 2, this assumption is precisely Markov’s principle; intuitively, it says that if a process doesn’t diverge then eventually it converges. Although forcing all predicates ϕ ∈ Ω to be ¬¬-closed makes Ω Boolean, this condition does not even make Σ Boolean.^{6}

6The reader is invited to find a lattice Σ of regular (“pinhole-free”) open subsets of ℝ.

The converse argument is beset with negations, and the best way to understand them is by introducing a relation which says positively that not every property of s is shared by t:

x | ⊑ t ⟺^{def} ∃ϕ ∈ Σ^{X}.ϕ(s) ∧ ¬ϕ(t)

Clearly we have s | ⊑ t ⇒ ¬(s ⊑ t), but in fact

Lemma 6.1 s ⊑ t iff ¬(s | ⊑ t).

Proof It is convenient to introduce N(s) =^{def} {ϕ ∈ Σ^{X} : ϕ(s)}, the set of neighbourhoods or properties of s. Then the right hand side is

¬∃ϕ ∈ N(s).¬ϕ(t)

which, since ¬∃ ≡ ∀¬, is just

∀ϕ ∈ N(s).¬¬ϕ(t)

But ϕ(t) ∈ Σ and is by hypothesis ¬¬-closed, so this is just s ⊑ t. □

Corollary 6.2 ⊑ is ¬¬-closed, i.e. ¬¬(S ⊑ T) ⇒ S ⊑ T. □

Hence the best converse of section 4 we can expect is S ⊑ T ⇒ ¬¬(S ⊑_{EM} T). It is convenient to show this in the form ¬(S ⊑_{EM} T) ⇒ ¬(S ⊑ T): a classical “argument by contradiction.” Incidentally, all functions reflect | ⊑, but the best transitivity result we have is

x | ⊑ z ⇒ ∀y.¬¬(x | ⊑ y ∨ y | ⊑ z)

We introduce

S ⋢_{EM} T ⟺^{def} ∃s ∈ S.∀t ∈ T.s | ⊑ t ∨ ∃t ∈ T.∀s ∈ S.s | ⊑ t

Suppose informally that the first disjunct holds for a particular s ∈ S. Writing T = {t_{1}, …, t_{m}}, there are computable predicates ϕ_{j} ∈ Σ^{X} such that ϕ_{j}(s) but ¬ϕ_{j}(t_{j}). Then with ϕ = ϕ_{1} ∧ ⋯ ∧ ϕ_{m} we have ϕ(s) but ¬∃t ∈ T.ϕ(t). Then ψ = ♢ ϕ is satisfied by S but not by T. The other part is similar, with ϕ as the disjunction and □ ϕ. More formally,

Lemma 6.3 If S ⋢_{EM} T then S | ⊑ T. Proof The first predicate (fixing s) is

□_{T} ⋁ ; _{ϕ∈N(s)} ¬ϕ(T) ⟺ ⋁ ; _{ϕ∈N(s)} □_{T} ¬ϕ(T) ⟺ ⋁ ; _{ϕ∈N(s)} ¬ ♢_{T} ϕ(T)

by continuity of □ and then □ ¬ ≡ ¬ ♢. Recall that the former used the weak axiom of finite choice, and it is easy to check that N(s) is a filter. Then

∃ϕ ∈ Σ^{X}.∃s ∈ S.ϕ(s) ∧ ¬ ♢ ϕ(T)

whence the result follows by putting ψ = ♢ ϕ.

Using the ideal

M(t) =^{def} {ϕ ∈ Σ^{X}.¬ϕ(t)}

the second predicate (fixing t) is

□_{S} ⋁ ; _{ϕ∈M(t)} ϕ(S) ⟺ ⋁ ; _{ϕ∈M(t)} □_{S} ϕ(S)

Then

∃ϕ ∈ Σ^{X}.∃t ∈ T.¬ϕ(t) ∧ □_{S} ϕ(S)

from which we deduce ¬ □ ϕ(T) ∧ □ ϕ(S), so we put ψ = □ ϕ. □

A classical argument would now be complete, but we have to reason constructively, and negation is a delicate thing, so there is more work to be done and we must be careful. The negated Egli-Milner relations do not behave quite as well as | ⊑, but we do have

Lemma 6.4 ¬(S ⋢_{EM} T) iff ¬¬(S ⊑_{EM} T). Proof ¬(S ⋢_{EM} T) is of the form

¬ ♢_{S} □_{T} s | ⊑ t ∧ ¬ ♢_{T} □_{S} s | ⊑ t

whilst, by the first lemma, we have already expressed ¬¬(S ⊑_{EM} T) in the form

¬¬ □_{S} ♢_{T} ¬s | ⊑ t ∧ ¬¬ □_{T} ♢_{S} ¬s | ⊑ t

Then

¬ ♢ □ ≡ □ ¬ □ ≡ □ ¬¬¬ □ ≡ □ ¬ □ ¬¬ ≡ □ ¬¬ ♢ ¬ ≡ ¬¬ □ ♢ ¬

from the relationships between modal operators and negation.^{7} □

Theorem 6.5 S ⊑ T iff ¬¬(S ⊑_{EM} T). Proof We have shown that

S ⊑ T ⟺ ¬(S | ⊑ T) ⇒ ¬(S ⋢_{EM} T) ⟺ ¬¬(S ⊑_{EM} T) ⇒ ¬¬(S ⊑ T) ⟺ S ⊑ T

□

7 Bibliography

J.L. Bell Toposes and local set theories, Oxford logic guides 14, Oxford University Press, 1988.

M.P. Fourman, The Logic of Topoi, in: J. Barwise, ed., Handbook of Mathematical Logic, North-Holland, 1977, 1053–1090.

M. Hennessy and G.D. Plotkin, Full Abstraction for a Simple Parallel Programming Language, in J. Becvar, ed., Proc. MFCS, Lecture Notes in Computer Science 74, Springer, 1979, 108–120.

R. Hindley and J. Seldin, eds., To H.B. Curry: essays in combinatory logic, lambda calculus and formalisms, Academic Press, 1980

J.M.E. Hyland, The effective topos, in: A.S. Troelstra & D. van Dalen,, eds., Brouwer centenary symposium, North Holland, 1982.

7This formula, though terse and unorthodox, precisely captures the active part of the argument.

J.M.E. Hyland, P.T. Johnstone and A.M. Pitts, Tripos theory, Proc. Camb. Philos. Soc. 88 (1980) 205–232.

P.T. Johnstone, Topos Theory, Acedemic Press, 1977. P.T. Johnstone, Stone Spaces, Cambridge studies in advanced mathematics 3, Cambridge

University Press, 1983.

P.T. Johnstone, The Vietoris Monad on the Category of Locales, in: R.-E. Hoffmann, ed., Continuous Lattices and Related Topics, Universität Bremen Mathematik-Arbeitspapier 27 (1982) 162–179.

A. Kock, Synthetic differential geometry, LMS lecture notes, Cambridge University Press, 1981.

J. Lambek, From λ-calculus to cartesian closed categories, in: Hindley & Seldin. J. Lambek and P.J. Scott, Introduction to higher order categorical logic, Cambridge stud-

ies in advanced mathematics 7, Cambridge University Press, 1986.

M. Makkai and G. Reyes, First order categorical logic, Lecture notes in Mathematics 611, Springer, 1977.

W.K.-S. Phoa, Effective Domains and Intrinsic Structure, in: Logic in Computer Science (Philadelphia, 1990), to appear.

G.D. Plotkin, A Powerdomain Construction, SIAM J. Comp. 5 (1976) 452–487. G.D. Plotkin, Dijkstra’s predicate transformers and Smyth’s powerdomain, in: D. Bjørner,

ed., Abstract Software, Lecture Notes in Computer Science 86, Springer, 1979. E.P. Robinson, A Modal Language for Power-Domains, manuscript. E.P. Robinson, Powerdomains, Modalities and the Vietoris Monad, Cambridge University

Computer Laboratory Technical Report 98, 1986.

G. Rosolini, Continuity and effectiveness in topoi, Ph. D. thesis, Carnegie-Mellon University, 1986.

G. Rosolini, Categories and effective computation, in: D. Pitt, ed., Category Theory and Computer Science (Edinburgh, 1987), Lecture Notes In Computer Science 240, Springer, 1987.

D.S. Scott, Relating theories of the λ-calculus, in Hindley & Seldin. M.B. Smyth, Powerdomains and Predicate Transformers: a Topological view, in: J.

Diaz, ed., Automata, Languages and Programming, Lecture Notes in Computer Science 154, Springer, 1983, 662–675.

S.J. Vickers, Topology via Logic, Cambridge University Press, 1989. G. Winskel, Note on Powerdomains and Modality, Theor. Comp. Sci. 36 (1985) 127–137.