12  Domain theory in ASD

In this section we provide the basic tools for implementing domain theory within ASD. Denotational semantics can then be developed in the usual way using this, allowing programming languages such as Gordon Plotkin’s PCF [Plo77] to be interpreted in ASD, and with them the programs required in Definitions 1.5, 1.6 and 2.3 for computable bases and functions. The difference is that classical domain theory leads to the dead end of set theory, whilst ASD can be translated back into programming languages.

However, the denotational semantics of programming languages will have to wait for a separate investigation. In this section we merely provide a few results that connect ASD with the topological aspects of domain theory such as [JKM99, JKM01, JS96] that rely on manipulation of bases (in the sense of that subject).

We first characterise the objects that have prime bases in our sense, and are continuous dcpos in the classical setting. The following results are essentially those of [Smy77, §2], where ◁ is called an R-structure. However, whereas Michael Smyth imposed a separate theory of recursion on the existing set-based theory of continuous dcpos, recursion is intrinsic to ASD. We also form the domain of rounded ideals using our own technology, which was developed in [B].

Definition 12.1 A directed interpolative relation n,m:N⊢(n◁ m):Σ on an overt discrete object N is an open relation that satisfies:

1. transitivity and interpolation: n,m:N ⊢ (n◁ m)  ⇔  ∃ k.(n◁ k)∧(k◁ m);
2. extrapolation downwards: n:N ⊢ ∃ k.(k◁ n)⇔⊤;
3. directedness: n,r,s:N ⊢ (r◁ n)∧(s◁ n)  ⇔  ∃ k.(r◁ k)∧(s◁ k)∧(k◁ n).

A rounded ideal for (N,◁) is a predicate Γ⊢ξ:Σ^N that is

1. rounded: Γ,  n:N ⊢ ξ n  ⇔  ∃ k.(n◁ k)∧ξ k;
2. inhabited: Γ ⊢ ∃ k.ξ k  ⇔  ⊤;
3. an ideal: Γ,  r,s:N ⊢ ξ r∧ξ s  ⇒  ∃ k.(r◁ k) ∧ (s◁ k)∧ξ k.

Lemma 12.2 For each n:N,  ↓ n ≡ λ k.k◁ n  is a rounded ideal.         ▫

We shall see that the ↓ n provide the “basic points” p_n (cf. Definition 1.5) of continuous and algebraic dcpos. In fact, the situation is summed up by the next result, whose converse we shall prove in Theorem 12.11.

Proposition 12.3 If X has an N-indexed prime basis, so

then ≻≻ is a directed interpolative relation, and x:X⊢ξ≡λ n.βⁿ x is a rounded ideal, with

Beware that ≺≺ and ◁ have opposite senses, following the conventions for continuous lattices, cf. the use of ≪ for compact and open subspaces in Notation 1.3: we think of ◁ as relating points. Thus m≻≻ n and m◁ n mean that A_m≪ A_n and p_m≪ p_n, but βⁿ≪β^m.

Proof    We have already proved these properties when ≺≺ arises from a filter ∨-basis. An ∨-basis was needed in order to use Scott continuity for A_n, but in this case A_n≡λφ.φ p_n preserves finite joins too, so directedness is redundant. Briefly,

1. the basis expansion of (n≺≺ m)≡β^m p_n gives transitivity and interpolation, as in Corollary 11.7;
2. that of (λ x.⊤)p_n gives extrapolation; whilst
3. that of (β^r∧β^s)p_n gives directedness, as in Proposition 11.10.

The directed join is focus(λφ.−) applied to the basis expansion, as in Theorem 10.4.         ▫

Examples 12.4 Here again are the prime bases that we have encountered.

1. Equality or any open equivalence relation on an overt discrete object is a directed interpolative relation, whose rounded ideals are the equivalence classes.
2. Σ^N is the object of (rounded) ideals for list or subset inclusion in Fin(N).
3. If X has an N-indexed ∨-basis, ≺≺_X is a directed interpolative relation on N, and Σ^X is the object of rounded ideals for this (recall from Lemma 9.8 that ≺≺_Σ^X is ≻≻_X).
4. In the case of an N-indexed filter lattice basis (so X is stably locally compact), the opposite relation (≻≻_X) is also directed interpolative, because

   ∃ k.Anβk  ⇔  Anβ1  ⇔  An⊤  ⇔ ⊤      Anβr∧ Anβs  ⇔  An(βr∧βs)  ⇔  An(βr+s).

5. Classically, the rounded ideals for ≻≻ are in order-reversing bijection with the compact saturated subspaces of X (Theorem 5.18).         ▫

Lemma 12.5 Any reflexive transitive relation is directed interpolative, and then all ideals are rounded.         ▫

Examples 12.6

1. If the way-below relation ≺≺ of the space X in Proposition 12.3 is reflexive then X is called an algebraic dcpo, and the p_n are its so-called finite or compact elements.
2. The space X is a continuous lattice iff it has a basis (N,◁) that’s a semilattice, i.e. the extrapolative and directed conditions are strengthened to a least element and binary joins respectively, instead of the extra/interpolant k.
3. In a Scott domain, the join is conditional: the join r+s exists in N whenever there is some upper bound n. Any Scott domain is a closed subspace of a continuous lattice, but if they are to form a cartesian closed category, they must also be overt [F]. Indeed, the basis N is overt in the formulation of this section. Instead of a conditional join, we may add a formal top element to N, or, equivalently, specify what part of an enlarged basis is to define the required domain by means of a decidable consistency predicate, cf. Proposition 7.12 [Sco82].
4. With pushouts (joins of pairs that are bounded below) but not necessarily a least element, we have a class of objects that includes the overt discrete ones and is closed under Σ⁽⁻⁾, sums and products. The structure of this subcategory is simple enough to be axiomatised directly in terms of overt discrete objects, i.e. from an arithmetic universe [E]. On the other hand, the whole category S may be recovered from it by the monadic construction in [B].
5. In an L-domain, the conditional joins in (c) are replaced by joins within the lower subset ↓ n.
6. If you are familiar with the characterisation of SFP or bifinite domains, and their continuous generalisations, you will be able to see how to encode them and their bases in ASD. Maybe this could provide a way of making the results about them more constructive, and identifying the largest cartesian closed category of locally compact objects [Jun90].         ▫

In the classical theory, a domain is recovered from its basis as the (continuous or algebraic) dcpo of (rounded) ideals, with the Scott topology. We can prove the corresponding result within ASD.

Lemma 12.7 For any directed interpolative relation (N,◁),

is a nucleus on Σ^N.

Proof    We have a directed⁶ union

by the extrapolation and directedness conditions, so by Theorem 9.6 and the definition of E,

Hence we deduce the equations for a nucleus in Theorem 10.10,

Definition 12.8 We have defined E from entirely abstract data (a directed interpolative relation) but have shown (via Theorem 10.10) that it satisfies the characteristic property of the composite Σⁱ· I that arises from a Σ-split subobject.

Now, it was exactly the purpose of the monadic calculus (Section B 8) that, in this situation, we do have an object, called X≡{Σ^N ∣ E} there, that has such a Σ-split inclusion. That is, the calculus provides i:{Σ^N ∣ E}↣Σ^N and I formally. Then Γ⊢ξ:Σ^N is admissible, i.e. an element of the new subobject, if

The idea of this is that E “normalises” open subobjects Φ of Σ^N by restricting and re-expanding them, and it is only the elements of the subobject being defined whose membership of all such Φ remains unchanged in this process.

In this case, the calculus allows us to introduce x≡admitξ:X such that ξ=i x.

Lemma 12.9 ξ:Σ^N is admissible iff it is a rounded ideal.

Proof    Putting Φ≡λθ.θ n, Φ≡λθ.⊤ and Φ≡λθ.θ r∧θ s, we deduce that ξ is a rounded ideal. Conversely, if ξ is a rounded ideal then

by equational induction on ℓ. Then, using the prime ∧-basis on Σ^N,

Corollary 12.10 ↓ n is admissible, because it is a rounded ideal.         ▫

Theorem 12.11 Any directed interpolative relation (N,◁) is the opposite of the way-below relation for a prime basis on its object of rounded ideals.

Proof    Let X≡{Σ^N ∣ E}↣ⁱΣ^N in the notation of Section B 8. Now I claim that

define a prime basis. Since ξ≡ i x is admissible, we have the basis expansion,

Finally, (n≺≺ m)  ⇔  A_n β^m  ⇔  β^m p_n  ⇔  i(admit(↓ n)) m  ⇔  (↓ n)m  ⇔  (m◁ n).         ▫

We leave domain theory aside there and return to topology.

Remark 12.12 Jung and Sünderhauf characterise stably locally compact spaces using a system of rules that they call a strong proximity lattice [JS96, Section 5]. These axioms are very similar to those in Section 11, except that theirs are lattice dual, whereas ours are not. In particular, they prove the dual Wilker property (Corollary 5.19), albeit using Choice. If (N,0,1,+,⋆,≺≺) is an abstract basis satisfying these axioms then so too is (N,1,0,⋆,+,≻≻). The corresponding object, which is known as the Lawson dual, classically has the same points as the given one, but the opposite specialisation order, whilst the open subobjects of one correspond to the compact saturated subobjects of the other.

Example 12.13 Let ≺≺ be the way-below relation for a filter lattice basis on a stably locally compact space X. The object ℘^♯X of rounded ideals for ≻≻ (Example 4) is called the Smyth or upper powerdomain of X and is Lawson dual to the topology Σ^X.         ▫

Lawson duality goes way beyond the purposes of this paper, but we can achieve the dual Wilker property by defining a new basis.

Proposition 12.14 Any stably locally compact object, i.e. one that has a filter ∧-basis (N,0,1,+,⋆,≺≺), has another such basis indexed by Fin(N) that also satisfies the dual Wilker property,

This can be extended to a new filter lattice basis with the same property by Lemma 8.4ff.

Proof    We define a new version of ⋆, called ×, by

This construction, unlike Remark 8.7, preserves the filter property, and is also idempotent.

We deduce the dual Wilker property by applying the last equation to βⁿ. Now, as the A_n preserve ∧,

For the converse, we put p‴≡ p′⋆ p″ and q‴≡ q′⋆ q″ and need

which we have from contravariance of A_p and the fact that we had an ∧-basis. The new operation × can be defined for more factors in the same way, using recursion and equational induction.         ▫

General locally compact objects are a good deal more complicated than domains. The extension of the earlier results of this section rely heavily on the “lattice” structure (0,1,+,⋆), which we investigate next.

6

It is directed in the existential sense of Definition 1, not in the canonical one of Definition 4.13 needed for Theorem 9.6. An ℕ–ℕ choice principle is needed for open (recursively enumerable) relations that amounts to sequentialising non-deterministic programs. This will be justified and applied to other questions arising from this paper in future work [G–].