Scott Domains in Abstract Stone Duality

Paul Taylor

August 5, 2003

Abstract Identifying the need for Scott domains to be overt (open) objects in intuitionistic locale theory, we re-work Scott’s informations systems construction from first principles, to obtain a cartesian closed full subcategory in abstract Stone duality. The necessary and sufficient condition for overtness is that the consistency predicate be decidable. We also construct the halting set: an open subspace of ℕ that is not closed.

1 Introduction

[[Dana Scott originally constructed topological models of the untyped λ-calculus using continuous and algebraic lattices [Sco76], in which ⊥ denotes non-terminating computation. Although ⊤ can be understood as an exception indicating observable inconsistency, it was considered undesirable by those using Scott’s results to give denotational semantics to programming languages. So he introduced (what came to be known as) Scott domains, encoded rather explicitly by information systems [Sco82]. We shall re-work this construction from first principles.]]

At first sight, a Scott domain [Sco82] is a closed subspace C of an algebraic lattice Y. However, when X is another domain, we want C^{X} to be a Scott domain too. The crucial point can be formulated in either the category of topological spaces or locales, cf. [Joh84]: [[Compare Lemma 3.1 and the Main Theorem of [Joh84]; if C is Hausdorff then so is C^{X}.]]

Proposition 1.1 Let X be locally compact. Then the functor (−)^{X} preserves closed inclusions C ^{⊏} Y iff there is a map ∃_{X} that makes the rightmost square a pullback:

[figure: C; 1; C^{X}; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; 1; 1; Y; ⊓; γ; Σ; ⊥; Y^{X}; \begin{matrix}⊓ \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \end{matrix}; γ^{X}; Σ^{X}; ⊥; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; ∃_{X}; Σ; ⊥]

Equivalently, there is a left adjoint, ∃_{X} ⊣ Σ^{!_{X}}. Proof C is closed iff there is a (unique) map γ making the leftmost square a pullback (we say that γ co-classifies C). In particular, {⊥} ⊂ Σ is the generic closed subset (of the Sierpiński space), and we are asking that {⊥} ⊂ Σ^{X} also be closed, which is what the rightmost pullback says. Using that, we may construct the rectangle as a pullback, and an easy comparison of universal properties shows that it is the exponential C^{X}. □

Definition 1.2 Locales with this property were called open by André Joyal and Myles Tierney [JT84, §V 3], but we shall call them overt. One reason for the new word is that we need to define a Scott domain as a closed subspace of an algebraic lattice that is also an overt space, but not an open subspace unless C = Y. Another is that overtness is the lattice dual of compactness [C, §7], and compact spaces have always been distinguished from closed subspaces.

Example 1.3 ℕ is overt because it admits existential quantification. Proposition 4.7 shows that its lift, ℕ_{⊥}, is a closed subspace of its topology, Σ^{ℕ}, co-classified by γ = λϕ. ∃yz. ϕ[y]∧ϕ[z]∧y ≠ z.

[figure: ℕ_{⊥}; 1; (ℕ_{⊥})^{ℕ}; 1; 1; Σ^{ℕ}; ⊓; γ; Σ; ⊥; Σ^{ℕ×ℕ}; ⊓; γ^{ℕ}; Σ^{ℕ}; ⊥; ∃_{ℕ}; Σ; ⊥]

Then (ℕ_{⊥})^{ℕ} is co-classified by δ = ∃_{ℕ} · γ^{ℕ} = λϕ. ∃xyz. ϕ[x, y] ∧ ϕ[x, z] ∧ y ≠ z, which we recognise as the statement that ϕ is not a functional relation. □

Remark 1.4 Overtness is not familiar in classical topology, where {⊥} is trivially a Scott-closed subset of the lattice Σ^{X} of open subsets of X. We shall see in the final section that things are very different in recursion theory; indeed, recursive enumerability implies overtness (and, I conjecture, conversely). [[Termination predicate (⊥ is closed).]]

Another role of an overt space I is that I-indexed joins exist in any lattice of open sets and are preserved by inverse image maps [C, Corollary 8.4]. Once again, this is axiomatic classically in topology and locale theory, but fails for recursion, where we only want recursive joins.

This is where abstract Stone duality comes in: by defining algebras of open subsets over the category of spaces itself (instead of over Set), the infinitary structure that is needed is provided in the background (to the extent that a lot can be done without actually stating it at all [C, D]), and we are at liberty to decree that selected objects such as ℕ be overt.

Remark 1.5 To do topology, we still need the finitary lattice operations ⊥, ⊤, ∧ and ∨, and state as an axiom that Σ is an internal distributive lattice. The exponential Σ^{X} must exist for each X, and provides the topology on X. Also, the Phoa principle,

F : Σ^{Σ}, σ : Σ ⊢ F σ = F ⊥ ∨ σ ∧ F ⊤,

is needed to capture the way in which ⊥, ⊤ ∈ Σ classify open and closed subspaces respectively [C, Section 5].

[[Phoa = Euclid + co-Euclid + monotone. Intrinsic order: write Γ ⊢ a ≤ b : X for Γ, ϕ : Σ^{X} ⊢ ϕa ≤ ϕb : Σ.]]

Remark 1.6 In order to construct these open and closed pre-images (as pullback squares) we need more types in the category than those generated from 1, Σ and ℕ by Σ^{(−)}. Such subspaces and others (but not all pullbacks) are provided by requiring that the adjunction Σ^{(−)} ⊣ Σ^{(−)} be monadic, and the type system may be extended in a corresponding way by a comprehension-like calculus [B].

In particular, all objects are to be sober [A], i.e. η_{X} : X → Σ^{2}X is the equaliser of Σ^{2}η_{X} and η_{Σ^{2}X}. This has the effect that when Γ ⊢ P : Σ^{Σ^{X}} is prime, i.e.

Γ, F : Σ^{3}X ⊢ FP = P (λx. F(λϕ. ϕx)),

we may introduce a new term Γ ⊢ focus P : X such that Γ, ϕ : Σ^{X} ⊢ ϕ(focus P) = P ϕ. [[−× notation.]]

Remark 1.7 In order to make the new (Eilenberg–Moore) notion of homomorphism agree with the lattice-theoretic one in topology, we need an infinitary axiom, which is invoked for the first time in the abstract Stone duality programme in this paper. The axiom has many forms and many roles, the most famous of which is that it provides fixed points. For us, its main purpose is to approximate any predicate or open subset ϕ : Σ^{ℕ} by its finite subsets, with the idea that meta-observation F : Σ^{Σ^{ℕ}} of ϕ can only test ϕ at finitely many values:

F : Σ^{Σ^{ℕ}} ⊢ F ⊤ = ∃ℓ:List(ℕ). F (λn. n ∈ ℓ).

We call this the Scott principle. [[F ϕ for F ⊤?]] Remark 1.8 The sobriety assumption is similar to (though in fact stronger than) repleteness [Hyl91, Tay91]. This provides a unique diagonal mediator in any commutative square in which s is Σ-epi (i.e. Σ^{s} is mono), as the map shown is, assuming the Scott principle.

ℓ  λn. n ∈ ℓ
List(ℕ)  [figure: s] Σ^{ℕ}  ψ

[figure: X; a_{(−)}; η_{X}; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; Σ^{Σ^{X}}; λϕ. ∃ℓ. ϕ(a_{ℓ}) ∧ ∀n ∈ ℓ. ψ[n]]
x  λϕ. ϕx

If a_{(−)} is monotone with respect to list inclusion then the square commutes because λϕ. ϕ[a_{ℓ}] = λϕ. ∃ℓ′. ϕ(a_{ℓ}) ∧ ∀n ∈ ℓ′. n ∈ ℓ. The mediator extends a_{(−)} from lists to all open subsets.

[[Interpretation in LKSp and LKLoc.]]

[[ There is a classical model, in which in particular Σ^{ℕ} is interpreted as the Pℕ, ∃ as union and ⊤ and ⊥ as the entire and empty subsets. It follows that the free model has the existence property:

if the term n : ℕ ⊢ ϕ[n] : Σ satisfies ⊢ ∃n. ϕ[n] = ⊤ (i.e. this is provable from the axioms) then there is a numeral (closed term ⊢ a : ℕ) such that ⊢ ϕ[a] = ⊤. □ ]] [[Justification of the definition of compactness.]]

2 Encoding predicates on ℕ

The greater part of this paper consists of heavy manipulation of (hereditarily) finite sets. For this, it is much more natural to use lists than be encumbered at every point by an isomorphism List(ℕ) ≅ ℕ. In fact we shall encode lists as binary trees, as functional programmers have done since Lisp. Trees provide a versatile data structure, with which we can give more or less explicit formulae throughout. [[lists versus tokens]]

Definition 2.1 The axioms for 𝕋 are the same as Peano’s for ℕ, merely replacing the unary operation-symbol (successor) with a binary one (pairing), together with a corresponding modification to the recursion scheme. Thus 𝕋 is the free algebra with

𝕋 ≅ 1 + 𝕋 × 𝕋,

in which the constant is called 0 here (but [ ] or nil elsewhere) and the binary operation is written ⟨−, −⟩ : 𝕋 × 𝕋 → 𝕋.

Proposition 2.2 𝕋 ≅ List(𝕋), in which the list [a, b, c] is encoded as ⟨a, ⟨b, ⟨c, 0⟩⟩⟩. The empty list is 0, and the value k is prepended (“cons-ed”) to the front of the list ℓ to form k :: ℓ ≡ ⟨k, ℓ⟩. We use the notation k :: ℓ when we’re thinking of this as a list, but we use the pair ⟨k, ℓ⟩ more frequently, and never actually need the [a, b, c] notation. [[Also, I have a habit of writing ϕ[a] for predicates.]] □

Notation 2.3 Lists encode finite sets, over which we may quantify:

\begin{aligned}(n ∈ 0) & ≡ & ⊥ & (n ∈ k :: ℓ) & ≡ & (n = k) ∨ (n ∈ ℓ) \\ ∀n ∈ 0. ϕ[n] & ≡ & ⊤ & ∀n ∈ k. ϕ[n] & ≡ & ϕ[k] ∧ ∀n ∈ ℓ. ϕ[n] \\ ∃n ∈ 0. ϕ[n] & ≡ & ⊥ & ∃n ∈ k. ϕ[n] & ≡ & ϕ[k] ∨ ∃n ∈ ℓ. ϕ[n] \\ ∃ℓ′ ⊂ 0. ϕ[ℓ′] & ≡ & ϕ[0] & ∃ℓ′ ⊂ k. ϕ[ℓ′] & ≡ & ∃ℓ′ ⊂ ℓ. ϕ[ℓ′] ∨ ϕ[k :: ℓ′]. \end{aligned}

Notice that we write ∀n ∈ ℓ. ϕ[n], and not ∀n:𝕋. n ∈ ℓ ⇒ ϕ[n], since neither ∀_{𝕋} nor ⇒ is defined on Σ. Also, these formulae are decidable (complemented) if ϕ is.

In particular, we write ℓ′ ⊂ ℓ for ∀n ∈ ℓ′. n ∈ ℓ, even though this is a preorder: it allows repetition and re-ordering. Also, it is only consistent with the formulae for ∃ℓ′ ⊂ ℓ. ϕ[ℓ′] if ϕ[ℓ′] is invariant under repetition and re-ordering of the list ℓ′.

Finite sets define predicates: ∅ = λk. ⊥, {n} = λk. (k = n), {m, n} = λk. (k = n ∨ k = m), etc., although we cannot generalise this to {ℓ} as it is ambiguous whether ℓ means an element or a list. Nevertheless, we do use the function ℓ ↦ λn. n ∈ ℓ, which we call s : 𝕋 → Σ^{𝕋}.

Finally, ℕ and 2 ≡ {no, yes} are retracts of 𝕋 by

\overline{0} = 0  \overline{1 + n} = ⟨0, \overline{n}⟩  |0| = 0  |k :: ℓ| = 1 + |ℓ|
\overline{no} = 0  \overline{yes} = ⟨0, 0⟩  ∥0∥ = no  ∥⟨p, q⟩∥ = yes

where |ℓ| is the length of the list ℓ.

We begin with the symbolic form of Remark 1.8.

Lemma 2.4 Let Γ, ℓ : 𝕋 ⊢ a_{ℓ} : X be monotone in the sense that

Γ, ℓ, ℓ′ : 𝕋, ϕ : Σ^{X} ⊢ ϕ(a_{ℓ′}) ∧ (ℓ′ ⊂ ℓ) ≤ ϕ(a_{ℓ}) : Σ.

Then Γ ⊢ P ≡ λϕ. ∃ℓ. ϕ[a_{ℓ}] is prime and Γ ⊢ ⋁ ; _{ℓ} a_{n} ≡ focus (λϕ. ∃ℓ. ϕ[a_{ℓ}]) is the least upper bound.

Proof Put Γ, F : Σ^{3}X ⊢ F ≡ λψ. F(λϕ. ∃ℓ. ϕ(a_{ℓ}) ∧ ∀n ∈ ℓ. ψ[n]) : Σ^{Σ^{𝕋}}. Then

P (λx. F(λϕ. ϕx)) = ∃ℓ. (λx. F(λϕ. ϕx))a_{ℓ} = ∃ℓ. F(λϕ. ϕa_{ℓ}).

By monotonicity, this is ∃ℓ. F(λϕ. ∃ℓ′. ϕa_{ℓ′} ∧ ∀n ∈ ℓ′. n ∈ ℓ) = ∃ℓ. F (λn. n ∈ ℓ) = F ⊤ = FP, using the Scott principle. In the case of a constant family, b_{ℓ} = b_{0}, ⋁ ; b_{ℓ} = b_{0}. On the other hand, if Γ, ℓ : 𝕋 ⊢ a_{ℓ} ≤ b_{ℓ} then Γ ⊢ ⋁ ; a_{ℓ} ≤ ⋁ ; b_{ℓ}. So the construction yields the least upper bound. □

Proposition 2.5 All objects have and all maps preserve ⋁ ; . Proof Let f : X → Y. Then

f( ⋁ ; a_{ℓ}) = focus_{Y} (λψ. ψ · f(focus_{X} λϕ. ∃ℓ. ϕa_{ℓ})) = focus_{Y} (λψ. ∃ℓ. ψ(fa_{ℓ})) = ⋁ ; _{ℓ} fa_{ℓ}.

Alternatively, the result follows from naturality of η in Remark 1.8. □ [[Beware that we mean internal joins!]]

Lemma 2.6 If Γ ⊢ F : Σ^{Σ^{X}} preserves ⊥ and ∨ (in the sense that F (ϕ_{1} ∨ ϕ_{2}) = F ϕ_{1} ∨ F ϕ_{2}) then it also preserves ∃. Proof Let Γ, n : ℕ ⊢ ϕ_{n} : Σ^{X}. Put Γ, ℓ : Listℕ ⊢ θ_{ℓ} ≡ ∃n ∈ ℓ. ϕ_{n} : Σ^{X}, so ∃n. ϕ_{n} = ⋁ ; _{ℓ} θ_{ℓ}. Then F (∃n. ϕ_{n}) = ⋁ ; _{ℓ} F θ_{ℓ} by Proposition 2.5, but F θ_{ℓ} = ∃n ∈ ℓ. F (ϕ_{n}) since the bounded quantifier is defined from ⊥ and ∨, which are preserved by F. Finally, ⋁ ; _{ℓ} ∃n ∈ ℓ. F ϕ_{n} ≡ ∃n. F ϕ_{n}. □

[[Directed join of a family qualified by an open subset, used in Remark ??.]]

Now we generalise the Phoa principle (Remark 1.5) from a single value σ to a list, and then to an open set of values. In this we write ϕ_{ℓ} = λn. n ∈ ℓ ∧ ϕ[n] for any ϕ : Σ^{𝕋} and ℓ : 𝕋.

Lemma 2.7 F : Σ^{Σ^{𝕋}}, ϕ : Σ^{𝕋} ⊢ F ϕ_{ℓ} = ∃ℓ′ ⊂ ℓ. F (λn. n ∈ ℓ) ∧ ∀n ∈ ℓ′. ϕ[n]. Proof The base case, ℓ = 0, is easy. In the induction step we prepend an element k to the list ℓ. By the Phoa principle with respect to σ = ϕ[k], the left hand side is

F ϕ_{k::ℓ} = F (λn. (n ∈ ℓ ∨ n = k) ∧ ϕ[n]) = F (ϕ_{ℓ} ∨ (σ ∧ {k})) = F ϕ_{ℓ} ∨ σ ∧ F (ϕ_{ℓ} ∨ {k}),

where {k} ≡ (λn. n = k). The right hand side is a disjunction over ℓ′′ ⊂ k :: ℓ. This breaks into two cases, the first, with k ∉ ℓ′′, being handled by the induction hypothesis. The other is k ∈ ℓ′′ = k :: ℓ′ with ℓ′ ⊂ ℓ.

RHS = ∃ℓ′ ⊂ ℓ. F (λn. n ∈ ℓ′) ∧ ∀n ∈ ℓ′. ϕ[n]
∨ ∃ℓ′ ⊂ ℓ. F (λn. n ∈ k :: ℓ′) ∧ ∀n ∈ k. ϕ[n]
= F ϕ_{ℓ} ∨ ∃ℓ′ ⊂ ℓ. F′(λn. n ∈ ℓ′) ∧ (∀n ∈ ℓ′. ϕ[n]) ∧ σ
= F ϕ_{ℓ} ∨ σ ∧ F′ϕ_{ℓ} = F ϕ_{ℓ} ∨ σ ∧ F (ϕ_{ℓ} ∨ {k})

using the induction hypothesis for F′ ≡ λψ. F (λn. ψ[n] ∨ n = k). □

Theorem 2.8 F : Σ^{Σ^{𝕋}}, ϕ : Σ^{𝕋} ⊢ F ϕ = ∃ℓ. F (λn. n ∈ ℓ) ∧ ∀n ∈ ℓ. ϕ[n]. Proof By the Scott principle and the Lemma,

F ϕ = ∃ℓ. F ϕ_{ℓ} = ∃ℓ. ∃ℓ′ ⊂ ℓ. F (λn. n ∈ ℓ′) ∧ ∀n ∈ ℓ′. ϕ[n] = ∃ℓ′. F (λn. n ∈ ℓ′) ∧ ∀n ∈ ℓ′. ϕ[n]. □

Recall from [A, Section 10] that if Γ ⊢ P : Σ^{2}ℕ preserves ⊤, ∧ and ∃_{𝕋} then it’s prime; this did not depend on the Scott principle, but the same result at higher types does.

Lemma 2.9 If Γ ⊢ P : Σ^{3}𝕋 preserves ⊤, ∧ and ∃_{𝕋} then it’s prime. Proof By Phoa, P(λϕ. σ) = P(⊥) ∨ σ ∧ P(⊤) = σ, so

PF = P(λϕ. ∃ℓ. F (λn. n ∈ ℓ) ∧ ∀n ∈ ℓ. ϕ[n])  Theorem 2.8
= ∃ℓ. P(F (λn. n ∈ ℓ) ∧ λϕ. ∀n ∈ ℓ. ϕ[n])  P preserves ∃
= ∃ℓ. F (λn. n ∈ ℓ) ∧ ∀n ∈ ℓ. P(λϕ. ϕ[n])  P preserves ⊤, ∧
= F (λn. P(λϕ. ϕ[n]))  Theorem 2.8 □

Corollary 2.10 By Lemmas 2.6 and 2.9, in order to show that H : Σ^{Σ^{𝕋}} → Σ^{U} is an Eilenberg– Moore homomorphism, it suffices to verify that it preserves ⊥, ⊤, ∧ and ∨. □

We complete the circle back to the categorical argument in Remark 1.8 by showing that s : 𝕋 ↠ Σ^{𝕋} is Σ-epi.

Lemma 2.11 S ⊣ Σ^{s} with S · Σ^{s} = id, where

s : 𝕋 ≅ List(𝕋) → Σ^{𝕋}  by s : ℓ ↦ λn. (n ∈ ℓ)
S : Σ^{𝕋} → Σ^{Σ^{List(𝕋)}} ≅ Σ^{Σ^{𝕋}} by S : ϕ ↦ λψ. ∃ℓ. [ϕ(ℓ) ∧ ∀n ∈ ℓ. ψ(n)].

Proof Using Theorem 2.8,

S(Σ^{s}F)ψ = ∃ℓ. Σ^{s}F ℓ ∧ ∀n ∈ ℓ. ψ[n] = ∃ℓ. F (λn. n ∈ ℓ) ∧ ∀n ∈ ℓ. ψ[n] = F ψ.
Σ^{s}(Sϕ)ℓ = (Sϕ)(sℓ) = ∃ℓ′. ϕℓ′ ∧ ∀n ∈ ℓ′. n ∈ ℓ = ∃ℓ′ ⊂ ℓ. ϕℓ′ ≥ ϕℓ.  □

In the next section we generalise this to embed all types in Σ^{𝕋}, and afterwards to deduce that all lattice homomorphisms are Eilenberg–Moore homomorphisms.

3 Algebraic lattices

Lemma 3.1 Let C : Σ^{𝕋} → Σ^{𝕋} [[M/C]] and write ℓ ⊩ n for C(λm. m ∈ ℓ)n. Then by Theorem 2.8,

Cϕn = ∃ℓ. ℓ ⊩ n ∧ ∀m ∈ ℓ. ϕ[m].  □

Lemma 3.2

(a) If ℓ′ ⊃ ℓ ⊩ n then ℓ′ ⊩ n.

(b) id : Σ^{𝕋} → Σ^{𝕋} corresponds to (ℓ ⊩ n) ≡ (n ∈ ℓ).

(c) id ≤ C : Σ^{𝕋} → Σ^{𝕋} iff ∀ℓn. n ∈ ℓ ⇒ ℓ ⊩ n.

(d) C = C · C : Σ^{𝕋} → Σ^{𝕋} iff (∃ℓ′. ℓ′ ⊩ n ∧ ∀m ∈ ℓ′. ℓ ⊩ m) ⟺ ℓ ⊩ n.

Proof In (d), the left hand side is C(C(λm. m ∈ ℓ))n. □

Definition 3.3 A binary predicate ℓ, n : 𝕋 ⊢ (ℓ ⊩ n) : Σ that satisfies (a,c,d) is called a saturated closure condition. The image X of the associated closure operator C = C · C ≥ id is called the algebraic lattice encoded by ⊩ [[although we don’t have space to justify the name]]. We also define an “imposed” order on 𝕋 by

ℓ′ ≤_{X} ℓ  if  ∀n ∈ ℓ′. ℓ ⊩ n.

[[Warning about imposed and intrinsic orders.]]

Examples 3.4 The following types are encoded by decidable saturated closure conditions.

(a) 1 is encoded by the relation ⊩ for which ℓ ⊩ n for all n, ℓ, so ℓ′ ≤_{1} ℓ always.

(b) Σ by ℓ ⊩ n for all n, ℓ ≠ 0, so ℓ′ ≤_{Σ} ℓ unless ℓ′ = 0, but only ⊥, ⊤ ∈ Σ are represented.

(c) ϖ (the ascending natural numbers with ⊤) is encoded by ℓ ⊩_{ϖ} n if ∃m ∈ ℓ. |m| ≤ |n|.

(d) Σ^{Σ^{𝕋}} is encoded by L ⊩ N iff ∃U ∈ L. U ⊂ N. Proof

(a) Cϕn = (∃ℓ. ∀m ∈ ℓ. ϕ[m]) = ⊤ [[with ℓ = 0]].

(b) Cϕn = (∃ℓ. ℓ ≠ 0 ∧ ∀m ∈ ℓ. ϕ[m]) = ∃m. ϕ[m] [[with ℓ = [m], i.e. the singleton list, ⟨m, 0⟩]].

(d) By Lemma 2.11, Σ^{Σ^{𝕋}} is the image of the closure operator C = Σ^{s} · S, and C(λm. m ∈ L)N = ∃U ∈ L. ∀u ∈ U. u ∈ N.

Proposition 3.5 Any saturated closure condition ⊩_{X} gives rise to adjunctions

[figure: 𝕋; s_{X}; X; \underline{c_{X}}; ⊥; i_{X}; Σ^{𝕋}; Σ^{𝕋}; S_{X}; ⊥; Σ^{s_{X}}; Σ^{X}; \underline{Σ^{i_{X}}}; ⊥; I_{X}; Σ^{Σ^{𝕋}}]

in which C_{X}(λm. m ∈ ℓ)n ≡ i_{X}(c_{X}(λm. m ∈ ℓ))n ≡ i_{X}(s_{X}ℓ)n ≡ ℓ ⊩_{X} n with s_{X}0 = ⊥_{X},

C_{X} = i_{X} · c_{X},  s_{X} = c_{X} · s,  S_{X} = Σ^{i_{X}} · S
I_{X} = Σ^{c_{X}} = S · Σ^{s_{X}}  and  I_{X} · Σ^{i_{X}} = S · Σ^{i_{X}·s_{X}}

where S ≡ S_{Σ^{𝕋}} : ϕ ↦ λψ. ∃ℓ. (ϕℓ ∧ ∀n ∈ ℓ. ψ[n]). Also, s_{X}ℓ ≤ s_{X}ℓ′ in X iff ℓ ≤_{X} ℓ′. Proof The closure operator C_{X} is defined from ⊩ by Lemma 3.1; we split this idempotent as C_{X} = i_{X} · c_{X} with c_{X} ⊣ i_{X} via the object X. In the notation of [B], X = {Σ^{𝕋} | Σ^{C_{X}} } and

s_{X}ℓ = c_{X}(sℓ) = admit (C_{X}(sℓ)) = admit(λn. ℓ ⊩ n).

Then c_{X} · i_{X} = id_{X} and id ≤ Σ^{C_{X}}, so, by Lemma 2.11,

S_{X} · Σ^{s_{X}} = Σ^{i_{X}} · S · Σ^{s} · Σ^{c_{X}} = Σ^{i_{X}} · Σ^{c_{X}} = id_{Σ^{X}}
Σ^{s_{X}} · S_{X} = Σ^{s} · Σ^{c_{X}} · Σ^{i_{X}} · S = Σ^{s} · Σ^{C_{X}} · S ≥ Σ^{s} · S ≥ id_{Σ^{𝕋}}
I_{X} · Σ^{i_{X}} = S · Σ^{s} · Σ^{c_{X}} · Σ^{i_{X}} = Σ^{C_{X}} ≥ id_{Σ^{2}𝕋}
Σ^{i_{X}} · I_{X} = Σ^{i_{X}} · S · Σ^{s} · Σ^{c_{X}} = Σ^{i_{X}} · Σ^{c_{X}} = id_{Σ^{X}} .

Finally, s_{X}ℓ ≡ c_{X}(sℓ) ≤ a : X for any a : X iff sℓ ≤ i_{X}a : Σ^{𝕋} iff ∀n ∈ ℓ. i_{X}an : Σ. □

Corollary 3.6 L ⊩_{Σ^{X}} N iff ∃U ∈ L. ∀u ∈ U. N ⊩_{X} u, that is, ∃U ∈ L. U ≤_{X} N, and so L′ ≤_{Σ^{X}} L iff ∀U′ ∈ L′. ∃U ∈ L. U ≤_{X} U′. If ⊩_{X} is decidable then so is ⊩_{Σ^{X}}. Proof This is the closure condition corresponding to the way in which we have just expressed Σ^{X} as the image of a closure operation on Σ^{𝕋}. Notice the contravariance in the last part, and also that N and U are treated here as lists, and L as a list of lists. □

Proposition 3.7 Any Γ, ℓ : 𝕋 ⊢ ϕ[ℓ] : Σ that sends the “imposed” order ≤_{X} on 𝕋 to the intrinsic order on Σ extends uniquely to θ : X → Σ such that θ · s_{X} = ϕ.

[figure: 𝕋; s_{X}; X; Σ; θ; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; ϕ]

Proof Define Γ, x : X ⊢ θx ≡ ∃ℓ. ϕ[ℓ] ∧ ∀n ∈ ℓ. i_{X}xn, so, by monotonicity,

θ(s_{X}ℓ) = ∃ℓ′. ϕ[ℓ′] ∧ ∀n ∈ ℓ′. i_{X}(s_{X}ℓ)n = ∃ℓ′. ϕ[ℓ′] ∧ ℓ′ ≤_{X} ℓ = ϕ[ℓ].

In fact this holds for any sober object Y as target in place of Σ, cf. Remark 1.8 and Lemma 2.4. □

Corollary 3.8 [[explain]] Σ^{C_{X}} F ϕ = ∃L. F (λN. N ∈ L) ∧ ∀N ∈ L. ∃U. ϕ[U] ∧ U ≤_{X} N, which “forces ϕ to be monotone with respect to ≤_{X}”. □

There are other situations in which the exponential transpose, ℓ ↦ λn. ℓRn, of a binary relation R factorises as i · s via some object X, with S · Σ^{s} = id_{X} = Σ^{i} · I. Of course, the formulae above for I and S are only valid when R is a saturated closure condition.

Proposition 3.9 Let R be an open equivalence relation on 𝕋. Then

(a) q : 𝕋 ↠ 𝕋/R is its quotient, q being an open surjection, with Q = ∃_{q} ⊣ Σ^{q} [[conflict in use of q and Q]];

(b) 𝕋/R admits equality, and, if R is decidable, inequality too;

(c) Σ^{𝕋/R} is an algebraic lattice, encoded by the closure condition (ℓ ⊩ n) ≡ ∃m ∈ ℓ. nRm; this is decidable if R is;

(d) the inclusion i : 𝕋/R Σ^{𝕋} by x ↦ λn. (qn=_{X}x) is the unique map for which i(qℓ) = λn. nRℓ;

(e) it is Σ-split by I : ϕ ↦ λψ. ∃n. ϕ(qn) ∧ ψ[n], but Σ^{i_{X}} ⊣ I_{X} only when R is (=_{𝕋}). [[Use idempotents, then may restrict to canonical values ⊂ 𝕋.]] Proof By the penultimate paragraph of [C, Lemma 10.8], the closure operation is Σ^{q} ·Q = Σ^{q} · ∃_{q} = λϕ. λx. ∃y. xRy∧ϕ[y], which yields the stated closure condition when we put ϕ = λm. m ∈ ℓ.

□

Examples 3.10

(a) ℕ ≅ 𝕋/R_{|·|}, where ℓ_{1}R_{|·|}ℓ_{2} ≡ |ℓ_{1}| = |ℓ_{2}|, i.e. these lists have the same length.

(b) 2 ≅ 𝕋/R_{∥·∥}, where R_{∥·∥} identifies any two pairs, ⟨p, q⟩ and ⟨p′, q′⟩, treating them as the value yes, but distinguishes them from 0 ≡ no.

(c) 𝕋 × 𝕋 ≅ 𝕋/R_{×} where R_{×} disposes of the constant 0 by identifying it with ⟨0, 0⟩.

(d) 𝕋 + 𝕋 ≅ 2 × 𝕋 ≅ 𝕋/R_{+}, where R_{+} identifies 0 with ⟨0, 0⟩, and ⟨⟨p, q⟩, n⟩ with ⟨⟨p′, q′⟩, n⟩. □

The applications of these examples stretch our list notation. However, whilst any functional programmer could code up our “filtering” operations on lists quite easily, for the sake of familiarity we (ab)use set-theoretic notation instead.

Lemma 3.11 If Y is an algebraic lattice then so is Y^{𝕋}, and L ⊩_{Y^{𝕋}} ⟨n, m⟩ ≡ {v | ⟨n, v⟩ ∈ L} ⊩_{Y} m, which is decidable if ⊩_{Y} is. Proof L ⊩_{Σ^{𝕋×𝕋}} n is n ∈ L ∨ (n = ⟨0, 0⟩ ∧ 0 ∈ L) ∨ (n = 0 ∧ ⟨0, 0⟩ ∈ L) by Example (c). Thus L is considered as a list of pairs, but if we find 0 in the list (or as the value of n), we treat it as ⟨0, 0⟩. Then we obtain C_{Y}^{𝕋} = i_{Y}^{𝕋} · c_{Y}^{𝕋} and ⊩_{X×Y} as the clockwise composite from 𝕋 to Σ^{𝕋} in the diagram

[figure: 𝕋; s; Σ^{𝕋}; ⊥; Σ^{𝕋×𝕋}; c_{Y}^{𝕋}; ⊥; i_{Y}^{𝕋}; Y^{𝕋}]

As we intend to evaluate C_{Y}^{𝕋} (sL) at ⟨n, m⟩, we restrict the set sL to those pairs that have n as their first component, since this is unaffected by C_{Y}^{𝕋}. This “filtered list” is defined as

{v | ⟨n, v⟩ ∈ 0}  = 0
{v | ⟨n, v⟩ ∈ p :: L} = v :: {v | ⟨n, v⟩ ∈ L}  if ⟨n, v⟩ = p or n = v = p = 0
= {v | ⟨n, v⟩ ∈ L}  otherwise. □

[[In ML: fold append (map (fn (u, v) ⇒ if u = n then [v] else [ ] )L).]]

Lemma 3.12 If X and Y are algebraic lattices then so is X × Y, and if ⊩_{X} and ⊩_{Y} are decidable then so is ⊩_{X×Y}. Proof Example (d) encodes Σ^{𝕋} × Σ^{𝕋} ≅ Σ^{𝕋} + Σ^{𝕋} in a similar way to Σ^{𝕋×𝕋}, using lists whose elements are either ν_{0}(n) = ⟨no, n⟩ or ν_{1}(n) = ⟨yes, n⟩.

[figure: 𝕋; s; Σ^{𝕋}; ⊥; Σ^{𝕋} × Σ^{𝕋}; c_{X} × c_{Y}; ⊥; i_{X} × i_{Y}; X × Y]

Then ℓ ⊩_{X×Y} ⟨0, n⟩ ≡ ℓ_{0} ⊩_{X} n and ℓ ⊩_{X×Y} ⟨⟨p, q⟩, n⟩ ≡ ℓ_{1} ⊩_{Y} n, where ℓ_{0} = {n | ⟨0, n⟩ ∈ ℓ} and ℓ_{1} = {n | ∃pq. ⟨⟨p, q⟩, n⟩ ∈ ℓ} are filtered lists (in the latter, ∃pq involves pattern-matching and not a search). □

Theorem 3.13

(a) All logical types in the restricted λ-calculus are distributive algebraic lattices that are encoded by decidable saturated closure conditions.

(b) All types in the monadic λ-calculus are Σ-split subspaces of Σ^{𝕋} (or of Σ^{ℕ}). Proof Recall that the restricted λ-calculus is generated from 1 and ℕ by products and Σ^{(−)} [A, Section 2], and that in the monadic λ-calculus we may also form Σ-split subspaces [B]. A logical type is one of the form Σ^{X}, which is distributive. We have shown in this section that the classes of algebraic lattices and subspaces of Σ^{𝕋} are closed under these constructions. □

In fact, we have already done enough to show that the full subcategory of algebraic lattices is cartesian closed, but we shall construct Y^{X} explicitly in Lemma 6.1.

4 Total and partial functions

We shall refer to Σ-split subspaces of Σ^{𝕋} (that is, to all of the objects definable in the monadic λ-calculus including the Scott principle) as locally compact spaces. This usage will be justified in future work, but we can now generalise Corollary 2.10 to obtain an analogue of [A, Theorem 5.7] entirely within Abstract Stone Duality.

Theorem 4.1 Let Y be a locally compact sober space and H : Σ^{Y} → Σ^{X}. Then the following are equivalent:

(a) H = Σ^{f} for some unique f : X → Y;

(b) H preserves ⊥, ⊤, ∧ and ∨ (it is a lattice homomorphism);

(c) it preserves ⊤, ∧ and ∃ (it is a σ-frame homomorphism);

(d) it is an Eilenberg–Moore homomorphism.

Proof Let i : Y  Σ^{𝕋} with Σ-splitting I : Σ^{Y}  Σ^{Σ^{𝕋}}. If H is a lattice homomorphism then

so is H ·Σ^{i} : Σ^{Σ^{𝕋}} → Σ^{X}, which is therefore an Eilenberg–Moore homomorphism by Corollary 2.10, i.e. the rectangle commutes.

[figure: Σ^{4}ℕ; Σ^{3}i; Σ^{2}I; Σ^{3}Y; Σ^{2}H; Σ^{3}X]

?

[figure: Σ^{2}ℕ; Σ^{2}ηΣℕ; Σ^{i}; Σ^{Y}; ΣηΣY; H; Σ^{X}; ΣηΣX]
Σ^{ℕ} [figure: i] Y ×  Ĥ  X

Then, since Σ^{3}i is split epi, the right-hand square also commutes, i.e. H is an Eilenberg–Moore homomorphism too. Then H = Σ^{f} since Y is sober [A, Theorem 4.10]. □

Remark 4.2 Here is the symbolic version of the same proof. If Γ ⊢ P : Σ^{2}X is a lattice homomorphism (in the sense that P (ϕ_{1} ∧ ϕ_{2}) = P ϕ_{1} ∧ P ϕ_{2} etc.) then so is Γ ⊢ Σ^{2}iP ≡ λF. P (λx. F (ix)):

P (λx. (F_{1} ∧ F_{2})(ix)) = P ((λx. F_{1}(ix)) ∧ (λx. F_{2}(ix))) = P (λx. F_{1}(ix)) ∧ P (λx. F_{2}(ix)).

Hence Σ^{2}iP is prime by Lemma 2.9, so P is also prime because

FP = (Σ^{2}IF)(Σ^{2}iP) = (Σ^{2}iP)(λψ. (Σ^{2}IF)(λF. F ψ))
= P (λx. (Σ^{2}IF)(λF. F (ix))) = P (λx. F(λϕ. (Iϕ)(ix))) = P (λx. F(λϕ. ϕx)),

where (Iϕ)(ix) = ϕx is the η-rule saying that Σ^{i} · I = id [B, Remark 2.5]. □

This lattice-theoretic characterisation of (the inverse images of) total maps easily extends to one of partial maps with open support. The construction of the partial map classifier is nevertheless valid without the characterisation, but the proof is rather more difficult [D].

Lemma 4.3 The topology on an open subspace i : U ^{⊂} X classified by ϕ ∈ Σ^{X} is the slice or lower set Σ^{X} ↓ ϕ, the inclusion being ∃_{i}. Also, ∃_{i} ⊣ Σ^{i} with ∃_{i} · Σ^{i} = (−) ∧ ϕ [C, Section 3]. □

Lemma 4.4 Σ ↓ Σ^{Y} ≡ {(σ, ψ) | y : Y ⊢ σ ≤ ψ(y)} is an algebra, which we call Σ^{Y_{⊥}}. The projections Σ Σ ↓ Σ^{Y} Σ^{Y} are homomorphisms, corresponding to maps that we call 1 ^{⊥} Y_{⊥} ^{i} _{⊃} Y, where i is an open inclusion with ∃_{i} : ϕ ↦ (⊥, ϕ). Proof Σ ↓ Σ^{Y} ◁ Σ × Σ^{Y} by (σ, ψ) ↦ (σ, λy. σ ∨ ψy). Then there is a pullback,

Σ × Σ^{Y} \overline{\begin{matrix}Σ^{!} × id \\  \end{matrix}}Σ^{Y} × Σ^{Y}

Σ ↓ Σ^{Y} \begin{matrix}[figure] & . . . . . . . . . . . . \\ ⊣  \end{matrix}  \overline{}Σ^{Σ×Y} [figure]

in which the top and right maps are homomorphisms, so Σ ↓ Σ^{Y} is a subalgebra of Σ × Σ^{Y}. The projections are homomorphisms because those from the product are, and the open subspace Y ^{⊂} Y_{⊥} is classified by (⊥, ⊤). □

Proposition 4.5 Let X and Y be locally compact sober spaces. There are bijective correspondence (up to isomorphism of U) amongst

(a) partial maps X ⇀ Y with open support, i.e. X ^{i} _{⊃} U ^{f} Y;

(b) F : Σ^{Y} → Σ^{X} preserving ⊥, ∧, ∨ and ∃;

(c) homomorphisms \overline{F} : Σ ↓ Σ^{Y} → Σ^{X} and

(d) \overline{f} : X → Y_{⊥}.

Hence Y_{⊥} is the partial map classifier: for any partial map f : X ⇀ Y with open support as in (a), there is a unique total map as in (d) that makes the left hand square a pullback.

\begin{matrix}U & \overline{f} & Y & Σ^{U} = Σ^{X} ↓ F ⊤ & [figure: F′] & Σ^{Y} \\ X & ^{\begin{aligned}i \\ & \end{aligned}∩} & ............................^{\overline{f}} & Y_{⊥} & ^{\begin{matrix}∩ \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \\ . \end{matrix}} & Σ^{X} & \begin{matrix}\begin{aligned}∃_{i} \\ & \end{aligned} & \\ ⊣ (−) ∧ F ⊤ [figure] \end{matrix} & ^{\overline{F}} & F ; \underline{} & Σ ↓ Σ^{Y} = Σ^{Y_{⊥}} & \begin{matrix}\begin{aligned}(⊥, (−)) \\ & \end{aligned} & \\ ⊣ π_{1} [figure] \end{matrix} \end{matrix}

Proof [a⇒b] ∃_{i}, being a left adjoint, preserves ∃, and it also preserves ∧ by the Frobenius law [C, Lemma 3.7], so F = ∃_{i}·Σ^{f} : Σ^{Y} → Σ^{X} preserves ⊥, ∧, ∨ and ∃. [b⇒a] Let i : U ^{⊂} X be the open subset classified by F ⊤ ∈ Σ^{X}. Then ∃_{i} : Σ^{X} ↓ F ⊤ Σ^{X} is the inclusion and F = ∃_{i} · F′ where F′ also preserves ⊤, so F′ = Σ^{f} by Theorem 4.1. [b⇒c] Let \overline{F} : (σ, ψ) ↦ σ ∨ F ψ, which may be verified to preserve the lattice operations. [c⇒b] F : ψ ↦ \overline{F} (⊥, ψ) preserves ⊥, ∧, ∨ and ∃. [c⇔d] \overline{F} = Σ\overline{f} since it is a homomorphism. The square is a pullback because \overline{F} (⊥, ⊤) = F ⊤ [C, Proposition 3.11(b)]. [[uniqueness?]] □

Lemma 4.6 The inclusion i : Y ^{⊂} Y_{⊥} is split iff Y has a least element. In this case, b ⊣ i and ∃_{i} ⊣ Σ^{i} ⊣ Σ^{b}. Proof Any splitting of the homomorphism Σ^{i} ≡ π_{1} : Σ ↓ Σ^{Y} ↠ Σ^{Y} must be of the form ψ ↦ (P ψ, ψ). If the splitting is a homomorphism then P is prime, with P ψ = ψp for some p : 1 → Y. This is the least element since ψp = P ψ ≤ ψy by the defining property of Σ ↓ Σ^{Y}. Conversely, ψ ↦ (ψp, ψ) is a splitting homomorphism (as it preserves the lattice operations), so it is Σ^{b} with b · i = id_{Y}, and indeed the adjunctions hold. □

Proposition 4.7 ℕ_{⊥} → Σ^{ℕ} is the closed subset co-classified by γ : ψ ↦ ∃mn. ϕ[n]∧ϕ[m]∧n ≠ m.

Proof The dotted map is defined from ℕ_{⊥} _{⊃} ℕ ^{{}} Σ^{ℕ} using Proposition 4.5.

[figure: ℕ; {}; Σ^{ℕ}; Σ^{ℕ}; Σ^{Σ^{ℕ}}]

ℕ_{⊥}^{∩} ........................ (Σ^{ℕ})_{⊥}^{⊣ ∩}  Σ ↓ Σ^{ℕ}^{⊣ } \underline{}Σ ↓ Σ^{Σ^{ℕ}}^{⊣ ⊣ }

As Σ^{ℕ} has a least element, its inclusion into (Σ^{ℕ})_{⊥} is split, and we put c : ℕ → Σ^{ℕ} for the composite, so Σ^{c} : F ↦ (F ∅, λn. F {n}). Also, define ∀_{c} : Σ^{ℕ_{⊥}} ≡ Σ ↓ Σ^{ℕ} → Σ^{Σ^{ℕ}} by

∀_{c}(σ, ϕ)ψ = σ ∨ (∃n. ϕ[n] ∧ ψ[n]) ∨ (∃nm. ψ[n] ∧ ψ[m] ∧ n ≠ m).

Then Σ^{c}(∀_{c}(σ, ϕ)) = (σ, λn. σ ∨ ϕn) = (σ, ϕ) since σ ≤ ϕ[n], and

∀_{c}(Σ^{c}F)ψ = F ⊥ ∨ (∃n. F {n} ∧ ψ[n]) ∨ (∃mn. ψ[m] ∧ ψ[n] ∧ m ≠ n)
= (∃ℓ. F (λn. n ∈ ℓ) ∧ ∀n ∈ ℓ. ψ[n]) ∨ (∃mn. ψ[m] ∧ ψ[n] ∧ m ≠ n)
= F ψ ∨ γψ

by Theorem 2.8 [[which uses 𝕋]], where the cases for lists with two or more distinct elements are absorbed into the term γψ. □

[[Of course, we also have]]

Proposition 4.8 If Y has ⊥ then every f : Y → Y has a least fixed point. Proof The fixed point is ⋁ ; _{n} f^{n}(⊥) by a familiar argument. Alternatively, the object ϖ (Example 3.4(c)) may be shown to be both the initial algebra and the final coalgebra for the functor (−)_{⊥}, and then the sequence λn. f^{n}(⊥) arises from the unique (−)_{⊥}-homomorphism ϖ → Y, whose value at ⊤ is the fixed point. □

[[Least fixed point in terms of ⋁ ; _{n} rec(n, ⊥, f).]]

5 Scott domains

We are now ready to resolve the problem of overt closed subspaces raised in Proposition 1.1 and so identify a cartesian closed full subcategory of locally compact spaces that includes 2_{⊥} and ℕ_{⊥} as objects.

Lemma 5.1 Let Y be an algebraic lattice encoded by ⊩_{Y}, and let C ^{⊏} Y be a closed subspace co-classified by γ : Y → Σ. Then α = γ·s_{Y} : 𝕋 → Σ satisfies ℓ ≤_{Y} ℓ′ ⇒ (αℓ ≤ αℓ′) and co-classifies a closed subspace A of 𝕋 such that the squares are pullbacks and p : A ↠ C is Σ-split epi.

[figure: A; p; C; 1; 𝕋; j; ⊓; s; Σ^{𝕋}; c_{Y}; ⊥; i_{Y}; Y; i; ⊓; γ; Σ; ⊥; \overline{α}; \overline{β}]  \begin{matrix}Σ^{A} & [figure: Σ^{p}; ⊤; .; .; .; .; .; .; .; .; .; .; .; .; .; P; .; .; .; .; .; .; .; .; .; .; .] & C \\ Σ^{𝕋} & [figure: Σ^{j}]⊣ \begin{matrix}∀_{j} \\  \end{matrix} & [figure: Σ^{s_{Y}}; ⊤; S_{Y}] & Σ^{Y} & [figure: Σ^{i}]⊣ \begin{matrix}∀_{i} \\  \end{matrix} \end{matrix}

Conversely, if α is monotone with respect to ≤_{Y} then γ = S_{Y} (α), and this is a bijective correspondence. We also put β = γ · c_{Y}, so γ = β · i_{Y}, α = β · s and β = λϕ. ∃ℓ. α[ℓ] ∧ ∀n ∈ ℓ. ϕ[n].

[[Use β in Lemma 6.3. Σ^{C} is an algebraic lattice. Combine with Lemma 5.5.]] Proof Proposition 3.7 gives the correspondence between α and γ, the adjunction S_{Y} ⊣ Σ^{s_{Y}} that between β and γ and Lemma 3.1 that between α and β.

The pullbacks are inverse images. Put P = Σ^{i} · S_{Y} · ∀_{j}. Then by the Beck–Chevalley equation [C, Proposition 3.11(b)] and the splittings,

P · Σ^{p} = Σ^{i} · S_{Y} · ∀_{j} · Σ^{p} = Σ^{i} · S_{Y} · Σ^{s_{Y}} · ∀_{i} = Σ^{i} · ∀_{i} = id,

whilst since i · p = s_{Y} · j and S_{Y} ⊣ Σ^{s_{Y}},

Σ^{p} · P = Σ^{p} · Σ^{i} · S_{Y} · ∀_{j} = Σ^{j} · Σ^{s_{Y}} · S_{Y} · ∀_{j} ≤ Σ^{j} · id · ∀_{j} = id.  □

Lemma 5.2 The object C is a overt iff the predicate α ∈ Σ^{𝕋} is decidable. Proof If α is decidable then the closed inclusion j : A → 𝕋 is also open, so A is overt (as is 𝕋 as an axiom) and so is C since p is Σ-epi [C, Section 7]. Explicitly, ∃_{C} = ∃_{𝕋} · ∃_{j} · Σ^{p} because we have three pullback squares as shown:

[figure: C; p; A; ⊂; j; 𝕋]
[figure: 1; 1; 1; 1]

[figure: Σ^{C}; ⊥; Σ^{p}; Σ^{A}; ⊥; ∃_{j}; Σ^{𝕋}; ⊥; ∃_{𝕋}; Σ; ⊥]

Conversely, if C is overt then we may use ∃_{C} to define a map 𝕋 → Σ:

[figure: 𝕋; s_{X}; X; i ^{⊐}; C; !; 1; 𝕋; {}; Σ^{𝕋}; S_{X}; ⊥; Σ^{s_{X}}; Σ^{X}; Σ^{i}; ⊥; ∀_{i}; Σ^{C}; ∃_{C}; ⊥; Σ^{!}; Σ.]

Then, by the adjunctions, ∃_{C} · Σ^{i} · S_{X} · {n} = ⊥ iff {n} ≤ Σ^{s_{X}} · ∀_{i}⊥, which is α[n] since ∀_{i}⊥ = γ (notice that we use {n} ≡ λm. m = n here and not sℓ ≡ λm. m ∈ ℓ). Therefore

¬α[n] = ∃_{C} · Σ^{i} · S_{X}{n}.  □
[[Even though 𝕋 is a discrete space ({ℓ} ^{⊂}  𝕋 and 𝕋 ^{⊂}  𝕋 × 𝕋 are open), we shall see in

the final section that it can have a closed subspace C that’s not open.]]

[[For locales, do we just need ¬α, which exists automatically? Ask Steve Vickers or Peter Johnstone.]]

Definition 5.3 As α must be decidable, we prefer to use Con_{X} ≡ ¬α to refer positively to the closed subspace, and say that ℓ ∈ 𝕋 is consistent if Con_{X}[ℓ]. We shall also write Con_{X}[ℓ] ⇒ ϕ for ϕ ∨ ¬Con_{X}[ℓ].

An information system (⊩_{X}, Con_{X}) consists of a saturated closure condition ⊩_{X} (Section 3) and a decidable predicate Con_{X} ∈ Σ^{𝕋} such that

Con_{X}[0]  {ℓ′ ≤_{X} ℓ  Con_{X}[ℓ] \atop Con_{X}[ℓ′]}

Then ⊩_{X} alone encodes an algebraic lattice \overline{X}, of which Con_{X} defines a closed subspace X ^{⊏} \overline{X} as above. This space X is called a Scott domain. The requirement that 0 be consistent excludes the empty set from being a domain, and ensures that X has ⊥ and so the fixed point property; Dana Scott achieved the same end by means of a special token Δ_{X}.

[[Dense injectives. Boundedly complete. Fixed point property. Lift of Scott domain.]]

Example 5.4 From Example 1.3, 𝕋_{⊥} is the Scott domain encoded by the information system (⊩, Con) in which (ℓ ⊩ n) ≡ (n ∈ ℓ) and Con[ℓ] ≡ ∀n ∈ ℓ. ∀m ∈ ℓ. n = m, so \overline{𝕋_{⊥}} = Σ^{𝕋}. We obtain ℕ_{⊥} and 2_{⊥} by restricting Con to the encodings of the numerals and booleans, cf. Examples 3.10.

Lemma 5.5 If X is a Scott domain encoded by (⊩_{X}, Con_{X}) then Σ^{X} is an algebraic lattice encoded by

L ⊩_{Σ^{X}} N  if  Con_{X}[N] ⇒ ∃U ∈ L. U ≤_{X} N.

If ⊩_{X} is decidable then so is ⊩_{Σ^{X}}.

Proof Without Con_{X} this is Corollary 3.6. Let γ co-classify X ^{⊏} ^{i} \overline{X}.

[figure: 𝕋; s; Σ^{𝕋}; c\overline{X}; ⊥; i\overline{X}; Σ\overline{X}; Σ^{i}; ⊥; ∀_{i}; Σ^{X}]

Σ^{X} ◁ Σ\overline{X} is the image of the closure operator ∀_{i} · Σ^{i} ≡ (−) ∨ γ, and γ[s_{X}ℓ] = α[ℓ] = ¬Con_{X}[ℓ]. □

Corollary 5.6 In the notation of [B], X = {Σ^{𝕋} | E_{X}}, where, for F : Σ^{Σ^{𝕋}} and ϕ : Σ^{𝕋},

E_{X}F ϕ = ∃L. F (λN. N ∈ L) ∧ ∀N ∈ L. Con_{X}[N] ⇒ ∃U. ϕ[U] ∧ U ≤_{X} N.  □

Lemma 5.7 If X and Y are Scott domains then so is X × Y. In the notation of Lemma 3.12, Con_{X×Y} [ℓ] ≡ Con_{X}[ℓ_{0}]∧Con_{Y} [ℓ_{1}]. [[Product of closed subspaces; state the formula in the notation of [B].]] □

6 Function spaces of Scott domains

Before we can construct the function-space of two Scott domains, we need a little more information about algebraic lattices and closure conditions. In the following, the letters X, U, u and N are associated with the input and Y, V, v and m with the output.

Lemma 6.1 If Σ^{X} and Y are algebraic lattices then so is Y^{X}. If Y is distributive, so is Y^{X}. Proof C_{Y^{X}} is the endo-map of Σ^{𝕋×𝕋} given by the diagram

[figure: 𝕋; s_{Σ^{𝕋×𝕋}}; Σ^{𝕋×𝕋}; S_{X}^{𝕋}; ⊥; Σ^{𝕋×s_{X}}; Σ^{𝕋×X}; c_{Y}^{X}; ⊥; i_{Y}^{X}; Y^{X}]

so C_{Y^{X}} = Σ^{𝕋×s_{X}} · i_{Y}^{X} · c_{Y}^{X} · S_{X}^{𝕋} = (i_{Y} · c_{Y})^{𝕋} · Σ^{𝕋×s_{X}} · S_{X}^{𝕋} = C_{Y}^{𝕋} · C_{Σ^{X}}^{𝕋} since Σ^{s_{X}} central. Then by Lemmas 3.1 and 3.11,

L ⊩_{Y^{X}} ⟨N, m⟩ = C_{Y^{X}} (sL)⟨N, m⟩ = C_{Y}^{𝕋} (C_{Σ^{X}}^{𝕋} (sL))⟨N, m⟩
= ∃L′. C_{Y}^{𝕋} (sL′)⟨N, m⟩ ∧ ∀⟨N′, v⟩ ∈ L′. C_{Σ^{X}}^{𝕋} (sL)⟨N′, v⟩
= ∃L′. {v | ⟨N, v⟩ ∈ L′} ⊩_{Y} m ∧ ∀⟨N′, v⟩ ∈ L′. {U | ⟨U, v⟩ ∈ L} ⊩_{Σ^{X}} N′
= ∃L′′. L′′ ⊩_{Y} m ∧ ∀v ∈ L′′. {U | ⟨U, v⟩ ∈ L} ⊩_{Σ^{X}} N
= C_{Y} (λv. {U | ⟨U, v⟩ ∈ L} ⊩_{Σ^{X}} N)[m],

in which {v | ⟨N, v⟩ ∈ L′} and {U | ⟨U, v⟩ ∈ L} are filtered lists. □

Corollary 6.2 If X is a Scott domain encoded by (⊩_{X}, Con_{X}) and Y an algebraic lattice encoded by ⊩_{Y} then Y^{X} is an algebraic lattice encoded by

L ⊩_{Y^{X}} ⟨N, m⟩ ≡ C_{Y} (λv. Con_{X}(N) ⇒ ∃U. ⟨U, v⟩ ∈ L ∧ U ≤_{X} N)[m]
≡ Con_{X}[N] ⇒ {v | ∃U. ⟨U, v⟩ ∈ L ∧ U ≤_{X} N} ⊩_{Y} m.

The second form applies when ⊩_{X} is decidable, and then {v | ⋯} is a filtered list. If ⊩_{Y} is also decidable then so is ⊩_{Y^{X}}. □

Lemma 6.3 If X and C are Scott domains then the exponential C^{X} exists.

[figure: D; C^{X}; 1; 1; 𝕋; ⊓; s_{Y^{X}}; Y^{X}; ⊓; γ^{X}; Σ^{X}; ⊥; ∃_{X}; Σ; ⊥]

Proof We know this from Proposition 1.1. The point is to find a formula for δ = ∃_{X} · γ^{X} · s_{Y^{X}}. [[Invert the diagram to make composites clockwise.]]

[figure: 1; !; 𝕋; i  _{⊃}; U; p; X]
\overline{∃_{X}}
[figure: Σ; \underline{∃_{𝕋}}; ⊥; Σ^{!}; Σ^{𝕋}; ∃_{i}; ⊥; Σ^{i}; Σ^{U}; Σ^{p}; ⊥; P; Σ^{X}]

[figure: 𝕋; s_{Σ^{𝕋×𝕋}}; Σ^{𝕋×𝕋}; β^{𝕋}; ∃_{i}^{𝕋}; ⊥; Σ^{𝕋×i}; Σ^{𝕋×U}; β^{U}; Σ^{𝕋×p}; ⊥; P^{𝕋}; Σ^{𝕋×X}; β^{X}; i_{Y}^{X}; ⊥; c_{Y}^{X}; Y^{X}; γ^{X}]
\overline{s_{Y^{X}}}

By Lemma 5.1, β = γ · c_{Y} = λϕ. ∃ℓ. ¬Con_{Y} [ℓ] ∧ ∀n ∈ ℓ. ϕ[n] : Σ^{𝕋} → Σ since α = ¬Con_{Y}. Also,

∃_{i} · Σ^{p} · β^{X} · P^{𝕋} · Σ^{𝕋×i} = (∃_{i} · Σ^{i}) · β^{𝕋} · (∃_{i} · Σ^{i} · P · Σ^{i})^{𝕋}
= λθN. Con_{X}[N] ∧ β(λv. C_{Σ^{X}}^{𝕋} θ⟨N, v⟩)

by naturality of β^{(−)} with respect to p and i, and since Σ^{i} · ∃_{i} = id_{Σ^{U}} and ∃_{i} · Σ^{i} = λN. Con_{X}[N] ∧ ϕ[N]. where i : U ^{⊂} 𝕋 is classified by Con_{X}.

C_{Σ^{X}}^{𝕋} (sL)⟨N, v⟩ = {U | ⟨U, v⟩ ∈ L} ⊩_{Σ^{X}} N  Lemma 3.11
= Con_{X}[N] ⇒ ∃U. ⟨U, v⟩ ∈ L ∧ U ≤_{X} N  Lemma 5.5

Hence δ[L] = ∃NV . Con_{X}[N] ∧ (∀v ∈ V . ∃U. ⟨U, v⟩ ∈ L ∧ U ≤_{X} N) ∧ ¬Con_{Y} [V]. □

Lemma 6.4 If X and C are Scott domains then so is C^{X}. Proof It remains to show that δ[L] is decidable, and δ[0] = ⊥. It is in fact not necessary for ⊩_{X} to be decidable, but we do have to bound the quantifiers ∃NV. Applying the “axiom of choice” for lists to ∀v.∃U,

δ[L] ⟺ ∃L′ ⊂ L. (∀⟨U_{1}, v⟩ ∈ L′. ∀⟨U_{2}, v⟩ ∈ L′. U_{1} = U_{2}) ∧ δ[L′],

so without loss of generality the quantifier ∃U is unique, whence it selects every U in the list L′ for some v.

Suppose δ[L′] holds for some particular N and V. I claim that they may as well be U_{L′} and V_{L′} respectively, these being the filtered lists

U_{L′} ≡ ⋃ {U | ∃v. ⟨U, v⟩ ∈ L′}  and  V_{L′} ≡ {v | ∃U. ⟨U, v⟩ ∈ L′}.

Indeed, V ⊂ V_{L′}, because of the middle term in δ[L′], and then ¬Con_{Y} [V_{L′}] by monotonicity of Con_{Y}. Also, each U in the list satisfies U ≤_{X} N ≡ ∀u ∈ U. N ⊩_{X} u, so U_{L′} ≤_{X} N too, but then Con_{X}[U_{L′}] by monotonicity of Con_{X}. The middle term is still satisfied since U ⊂ U_{L′}, so U ≤_{X} U_{L′}; in fact this term is now redundant, being ∀v ∈ V_{L′}. ∃U. ⟨U, v⟩ ∈ L′ ∧ U ≤_{X} U_{L′}.

Thus, in order to determine δ[L], we need to consider, for each L′ ⊂ L with the uniqueness condition (of which there is a filtered list),

δ[L′] = Con_{X}[U_{L′}] ∧ ¬Con_{Y} [V_{L′}],

which is decidable. In particular, δ[0] = Con_{X}[0] ∧ ¬Con_{Y} [0] = ⊥, so Con_{C^{X}} [0] = ⊤. □

Remark 6.5 We may read consistency of a list L of function-tokens,

Con_{Y^{X}} [L] ≡ ¬δ[L] ≡ ∀NV . Con_{X}[N] ∧ (∀v ∈ V . ∃U. ⟨U, v⟩ ∈ L ∧ U ≤_{X} N) ⇒ Con_{Y} [V]
≡ ∀L′ ⊂ L. (∀⟨U_{1}, v⟩ ∈ L′. ∀⟨U_{2}, v⟩ ∈ L′. U_{1} = U_{2}) ∧ Con_{X}[U_{L′}] ⇒ Con_{Y} [V_{L′}]

as follows. For any consistent finite set N of input tokens, the finite set V of output tokens must be consistent whenever each v ∈ V comes from some function-token ⟨U, v⟩ ∈ L that matches the input in the sense that U ≤_{X} N. A list L (or, more generally, an RE set) with this property is called an approximable mapping from (⊩_{X}, Con_{X}) to (⊩_{Y} , Con_{Y}). □

[[Spell out the correspondence with morphisms. Also, how to obtain the least fixed point.]]

Remark 6.6 In his own construction of the function-space [Sco82, Definition 7.1], Scott chose for the function-tokens pairs ⟨U, V ⟩ with Con_{X}[U] and Con_{Y} [V], using a consistent finite set V instead of a single output token v. Then

L ⊩_{Y^{X}} ⟨N, M⟩ ≡ ∀m ∈ M. L ⊩_{Y^{X}} ⟨N, m⟩ ≡ ⋃ {V | ∃U. ⟨U, V ⟩ ∈ L ∧ U ≤_{X} N} ≥_{Y} M,

in which Con_{X}[N] is redundant. Scott actually wrote out L = [⟨u_{0}, v_{0}⟩, ⟨u_{1}, v_{1}⟩, …, ⟨u_{k_{1}}, v_{k−1}⟩], with ⟨u_{i}, v_{i}⟩ for our ⟨U, V ⟩ and ⟨u, v⟩ for our ⟨N, M⟩. He also used ⊢ for both our ⊩ and ≥, so for our Corollary 6.2 he defined

L ⊩_{Y^{X}} ⟨u′, v′⟩ ≡ ⋃ {v_{i} | u′ ⊢_{X} u_{i}} ⊢_{Y} v′.  □

[[Scott’s Con_{Y^{X}} doesn’t have the uniqueness term, as it can be shown to be redundant. Computational complexity.]] Theorem 6.7 The full subcategory consisting of Scott domains is cartesian closed, as are the full subcategories of domains that are distributive, or for which ⊩ is decidable. □

One reason for wading into this morass of symbols was, of course, to show that the simple categorical idea for C^{X} does indeed yield Scott’s information systems. We may still wonder whether C^{X} can be shown to be overt by more conceptual methods, or whether the connection between overtness and recursive enumerability really demands that we find a way of coding the compact elements of the function space. Indeed, Joyal and Tierney [JT84, §V 3] and Phoa [Pho90, §6.5], considering locales and the effective topos respectively, also used such an explicit enumeration to show that the partial-function space (X_{⊥})^{ℕ} ≡ [ℕ ⇀ X] is overt when X is. (Phoa also showed that ℕ^{ℕ} is not overt.)

7 Untyped λ-calculus and recursive enumeration

In [Sco76], Dana Scott showed that Pℕ (or, as he called it, Pω) is a model of the untyped λcalculus that satisfies the β-rule but not the η-rule. Here we shall show that Σ^{𝕋}, which is our analogue of Pℕ, is also such a model in the same way.

However, Pω, being the full powerset, is uncountable, and therefore has many elements that are not the denotations of untyped λ-terms. Our Σ^{𝕋}, on the other hand, is itself defined by means of a λ-calculus, so there is a function ξ : 𝕋 ↠ Σ^{𝕋} that is surjective (not merely Σ-epi as s was in Lemma 2.11). This provides the basis for doing recursion theory in abstract Stone duality, instead of using partial recursive functions on numbers alone. We shall be content with showing that ℕ has open subsets that are not closed, even though it is discrete as far as its individual points are concerned.

From Section 3, Λ^{Λ} is a retract of (indeed, the image of a closure operator on) Λ ≡ Σ^{𝕋}, where

Λ^{Λ} ≅ Σ^{𝕋×Σ^{𝕋}}

lambda ≡ Σ^{s}
⊤

{ \atop apply} ≡ S_{𝕋×Σ^{𝕋}}

Λ ≡ Σ^{𝕋}

arise from s_{𝕋×Σ^{𝕋}} : 𝕋 ↠ 𝕋 × Σ^{𝕋}.

Any one-variable expression x : Λ ⊢ p(x) : Λ is encoded as an element of Λ by lambda(λx. p(x)), and its meaning is recovered by the equation

[a/x]^{∗}p(x) = (λx. p(x))a = apply(lambda(λx. p(x)), a).

By a well known translation, λ may be eliminated in favour of application, free variables and the combinators K and S. Recall that the constants of our own λ-calculus are

⊤, ⊥ : Σ  ∧, ∨ : Σ × Σ → Σ  ∃ : Σ^{𝕋} → Σ
0 : 𝕋  ⟨−, −⟩ : 𝕋 × 𝕋 → 𝕋  rec : Σ^{𝕋} × Σ^{𝕋×𝕋×Σ^{𝕋}×Σ^{𝕋}} × 𝕋 → Σ^{𝕋}.

Recursion at other types is provided by [B, Lemma 8.8] since every other object in the category may be expressed as a subtype of Λ. Moreover, since Λ is injective, all of the morphisms (in particular these constants) are tracked by endo-maps of this type, and therefore by elements of Λ:

[figure: Λ; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; Λ; X; f; Y]

We are therefore left with the binary apply operation on Λ and a handful of constants. This is called an applicative algebra. The expressions in this algebra may be represented as binary trees, i.e. as elements of 𝕋. Confusing the closed term ⊢ ϕ : Λ^{𝕋} with its syntax, we write ⊢ ⌜ϕ⌝ : 𝕋 for the tree representation. It is known as the Turing number of ϕ [[cite him]].

Lemma 7.1 There is an interpretation function ξ : 𝕋 → Λ, with the property that for any closed term ⊢ ϕ : Λ^{𝕋},

n : 𝕋 ⊢ ξ⟨⌜ϕ⌝, n⟩ = ϕ[n] : Λ.

Moreover, ξ : 𝕋 → Λ is universal in the (weak) sense that for any C-map f : 𝕋 → Λ there is some (not unique) tracking function g : 𝕋 → 𝕋 such that f = ξ · g.

\begin{aligned}& 𝕋 \\ 𝕋 & \overline{f} & \begin{matrix}g \\ . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & . & \end{matrix} & Λ & [figure: ξ] \end{aligned}

Proof In fact, g : n ↦ ⟨⌜λm. fm⌝, n⟩. Notice that this is primitive recursive, because it merely “loads the program into the interpreter”: it is ξ that executes the program. □

[[Justify Σ^{ℕ} as the set of recursively enumerable subsets of ℕ: ϕ ∈ Σ^{ℕ} is encoded by some program ⌜ϕ⌝, then ϕ\overline{n} ≡ ξ⟨⌜ϕ⌝, \overline{n}⟩ terminates iff n ∈ [[ϕ]] ⊂ ℕ.]]

Theorem 7.2 There is an open subset U ⊂ 𝕋 that’s not closed. Proof Let U be classified by n : 𝕋 ⊢ ξ⟨n, n⟩ : Σ, and suppose that ⊢ ϕ : Σ^{𝕋} satisfies

n : 𝕋 ⊢ ϕ[n] = ¬ξ⟨n, n⟩.

By the Lemma,

n : 𝕋 ⊢ ξ⟨⌜ϕ⌝, n⟩ = ϕ[n]

for some Turing number ⌜ϕ⌝. But, putting n = ⌜ϕ⌝, we then have the contradiction,

⊢ ξ⟨⌜ϕ⌝, ⌜ϕ⌝⟩ = ϕ(⌜ϕ⌝) = ¬ξ⟨⌜ϕ⌝, ⌜ϕ⌝⟩.  □

U ⊂ 𝕋 is known as “the” halting set, although it’s not unique.

[[ξ may be used in place of s_{Λ} to develop the domain theory that we have done. If ξ : 𝕋 → Λ a recursive enumeration then it is also a topological enumeration. Let g : 𝕋 → 𝕋 be such that s_{Λ} = g ; ξ, and put Ξ = Σ^{g} ; S_{Λ}. Then Σ^{ξ} ; Ξ = id, but there’s no reason why we should have id ≤ Ξ ; Σ^{ξ}.]]

[[The fixed point combinator Y. Read Data Types as Lattices.]]

[[In fact, if we restrict attention to those objects that are algebraic lattices, the objects themselves may be encoded as closure operations on Λ, and these also form a domain that is encoded as a closure operation, which may be regarded as a “type of (names of) types”.]]

References

[Hyl91] Martin Hyland. First steps in synthetic domain theory. In Aurelio Carboni, Maria-Cristina Pedicchio, and Giuseppe Rosolini, editors, Proceedings of the 1990 Como Category Conference, volume 1488 of Lecture Notes in Mathematics, pages 131–156. Springer-Verlag, 1991.

[Joh82] Peter Johnstone. Stone Spaces. Number 3 in Cambridge Studies in Advanced Mathematics. Cambridge University Press, 1982.

[Joh84] Peter Johnstone. Open locales and exponentiation. Contemporary Mathematics, 30:84–116, 1984.

[JT84] André Joyal and Myles Tierney. An Extension of the Galois Theory of Grothendieck, volume 309 of Memoirs. American Mathematical Society, 1984.

[Pho90] Wesley Phoa. Domain Theory in Realizability Toposes. PhD thesis, Cambridge, 1990. http://www.lfcs.informatics.ed.ac.uk/reports/91/ECS-LFCS-91-171.

[Sco76] Dana Scott. Data types as lattices. SIAM Journal on Computing, 5:522–587, 1976.

[Sco82] Dana Scott. Domains for denotational semantics. In M. Nielson and E. M. Schmidt, editors, Automata, Languages and Programming: Proceedings 1982. Springer-Verlag, Berlin, 1982. Lecture Notes in Computer Science 140.

[Tay91] Paul Taylor. The fixed point property in synthetic domain theory. In Gilles Kahn, editor, Logic in Computer Science 6, pages 152–160. IEEE, 1991.

[Tay99] Paul Taylor. Practical Foundations of Mathematics. Number 59 in Cambridge Studies in Advanced Mathematics. Cambridge University Press, 1999.

[Thi97] Hayo Thielecke. Categorical Structure of Continuation Passing Style. PhD thesis, University of Edinburgh, 1997. Also available as technical report ECS-LFCS-97-376.

The papers on abstract Stone duality may be obtained from

                                 www.cs.man.ac.uk/∼pt/ASD

[A] Paul Taylor, Sober spaces and continuations. Theory and Applications of Categories, 10(12):248–299, 2002.

[B] Paul Taylor, Subspaces in abstract Stone duality. Theory and Applications of Categories, 10(13):300– 366, 2002.

[C] Paul Taylor, Geometric and higher order logic using abstract Stone duality. Theory and Applications of Categories, 7(15):284–338, 2000.

[D] Paul Taylor, Non-Artin gluing in recursion theory and lifting in abstract Stone duality. 2000. [E–] Paul Taylor, Local compactness and the Baire category theorem in abstract Stone duality. Category

Theory and Computer Science, Ottawa, 2002. ENTCS 69.

[E] Paul Taylor, Computably based locally compact spaces. May 2003.

[G] Paul Taylor, An elementary theory of the category of locally compact locales. March 2003.

[[Where does one find the expanded version of [Sco82]?]]

This appendix is not intended to be included in the conference paper: it is put here for the interest of the referee for [A]. The journal version will also show how the denotational semantics of PCF in (our) Scott domains provides two continuation-passing translations.

A Partial, discardable and copyable maps

The lattice-theoretic characterisation of maps between locally compact sober spaces in Theorem 4.1 may be extended from first class maps to other maps of interest in topology and computer science. In particular, many “ordinary” programs X −× Y exhibit a trichotomous behaviour:

• they abort with some error message,

• terminate normally with an output value, or

• fail to terminate ever, but this behaviour is reproducible.

Remark A.1 Programs that may fail to terminate, but whose results are valid and reproducible if they come, correspond to maps that are well defined on some open subspace i : U ^{⊂} X. Such subspaces are classified by elements of Σ^{X}. The inverse image Σ^{i} has a left adjoint, which is called ∃_{i} since it enjoys the properties of an existential quantifier, including the Frobenius law

∃_{i}(ϕ ∧ Σ^{i}ψ) = (∃_{i}ϕ) ∧ ψ.

Topologically, open subsets of U are already open in X, so we regard ∃_{i} : Σ^{U} Σ^{X} as an inclusion. See [C, Section 3] for open subsets in abstract Stone duality.

Remark A.2 Dually, a program X −× Y that always terminates, but possibly by aborting its calling program, is a partial map with closed support i : C ^{⊏} X. Its predicate transformer F : Σ^{Y} → Σ^{X} preserves ∧, ∨ and ⊤. [[Explain using force: x ↦ ψ(force λψ. F ψx) = F ψx.]]

The open subspace U ^{⊂} X classified by F ⊥ is where abortion occurs — it is open because this is a computationally observable or affirmative phenomenon. The complementary closed subspace C is where this doesn’t happen, and instead the program behaves “normally”.

The inverse image map Σ^{c} of a closed subspace has a right adjoint, called ∀_{c} because it enjoys the properties of a universal quantifier, but also the dual Frobenius law

∀_{c}(ϕ ∨ Σ^{c}ψ) = (∀_{c}ϕ) ∨ ψ.

Topologically, an open subset of C is extended to one of X by its union with U, so ∀_{c} : Σ^{C} Σ^{X} is represented as (−) ∨ F ⊥. See [C, Corollary 5.6] for closed subspaces in abstract Stone duality.

Remark A.3 When both kinds of undesirable behaviour are possible, F preserves neither ⊥ nor ⊤. Then there is an open subspace (classified by F ⊥) on which the program aborts, and a closed one (co-classified by F ⊤) on which it fails to terminate, behaviour on the remainder being normal. This is the intersection of an open subspace (termination) with a closed one (non-abortion), and is called locally closed.

Instead of using a denotational semantics based on lattices, Hayo Thielecke formulated “reproducibility” of programs in terms of the extent to which they respect the extension of the categorical product from C to HC [Thi97, Definition 4.2.4].

Definition A.4

(a) An HC-map F̂ : X −× Y is called discardable if it respects the naturality of the terminal (or product) projection (!), i.e. Σ^{!_{Y}} ; F = Σ^{!_{X}}. Equivalently, H : Σ^{Y} → Σ^{X} is a homomorphism with respect to all constants σ ∈ Σ, i.e.

σ : Σ ⊢ F (λy. σ) = λx. σ.

(b) Similarly, F̂ : X −× Y is copyable if it respects the naturality of the diagonal (Δ). We shall show that this is equivalent to preserving ∧ and ∨.

Thielecke gave examples of programs that are discardable in this sense but nevertheless have computational effects, specifically by making use of their continuations twice. His intuition is that a computational object that is both discardable and copyable is effect-free [[and is therefore a first class value? Josh Berdine is working on linearly used continuations.]]

Examples A.5

(a) ˆ∃_{f} is discardable for any open surjection f : X ↠ Y.

(b) ˆ∃_{i} is copyable for any open inclusion i : U ^{⊂} X. Proof See [C, Definition 10.4] for open surjections, for which ∃_{f} preserves ⊤, ⊥ and ∨ but not necessarily ∧.

Σ^{U}[figure: ∃_{i}] Σ^{X}

[figure: Σ^{U×U}; Σ^{Δ_{U}}; ∃_{i}^{U}; Σ^{U×U}; ∃_{i}^{X}; Σ^{X×X}; Σ^{Δ_{X}}]

We regard Γ ⊢ θ : Σ^{U×U} as θ ∈ Σ^{X×X} with Γ, x, y : X ⊢ θ(x, y) ≤ ϕ(x) ∧ ϕ(y). Clockwise, this is taken to λu. θ(u, u) and then to λx. θ(x, x), whilst the anticlockwise route results in the same thing. In topological notation, W ⊂ U × U ⊂ X × X is taken clockwise to W ∩ Δ_{U} ≅ {u | (u, u) ∈ W } ⊂ U ⊂ X, which is the same as W ∩ Δ_{X}. Compare Lemma A.10 below. □

Remark A.6 Similarly, a program that may return its input in some reproducible cases U ^{⊂} ℕ, but otherwise fails to terminate, is like ˆ∃_{i}, being copyable but partial with open support. On the other hand, an oracle for a surjection f : ℕ ↠ ℕ is a non-deterministic program for f^{−1}, being discardable but not copyable.

In the topological interpretation, discardability and copyability suffice.

Lemma A.7 If F̂ : X −× Y is a discardable and copyable HC-map then F preserves ⊤ and ∧.

[figure: Σ^{Y} × Σ^{Y}; ∧; Σ^{Y ×Y}; Σ^{Δ}; Σ^{Y}]

[figure: Σ^{X} × Σ^{Y}; F × id; ∧; Σ^{X×Y}; F^{Y}]

[figure: Σ^{X} × Σ^{X}; id × F; ∧; Σ^{X×X}; F^{X}; Σ^{Δ}; Σ^{X}; F]

Proof The map (∧) : Σ^{Y} × Σ^{Y} → Σ^{Y ×Y} is defined by (ϕ, ψ) ↦ λy_{1}y_{2}. ϕ(y_{1}) ∧ ψ(y_{2}). As F̂ is copyable, the rectangle on the right commutes, and as it is discardable, F (λy. σ∧ϕy) ≤ F (λy. σ) = λx. σ. Hence

F (λy. σ ∧ ϕy)x = σ ∧ F (λy. σ ∧ ϕy)x = σ ∧ F (λy. ϕy)x

by the Euclidean principle for G : σ ↦ F (λy. σ ∧ ϕy)x. Hence, putting σ = ψ(y_{2}),

F^{Y} (λy_{1}y_{2}. ϕy_{1} ∧ ψy_{2}) = λy_{2}. F ϕ ∧ ψy_{2},

so the two squares on the left commute. The whole diagram says that F preserves ∧. □

This adds another condition to Theorem 4.1:

Theorem A.8 F̂ : X −× Y is a discardable and copyable map between locally compact spaces iff F = Σ^{f} for some continuous map f : X → Y. Proof We have shown that if F̂ is discardable and copyable then F preserves ⊤, ⊥ and ∧. The argument for ∨ is similar, using the lattice dual of the Euclidean principle [C, Corollary 5.5],

σ ∨ G(σ) = σ ∨ G(⊥).

Then F = Σ^{f} by Theorem 4.1. Conversely, f ≡ Σ̂^{f} is discardable and copyable. □

In order to show that copyability alone is equivalent to preserving the binary connectives, we have to “repair” the failure of a given map F̂ : X −× Y to preserve the constants.

Lemma A.9 If Ĝ : X −× Y is copyable then so are f ; Ĝ : W −× Y and Ĝ; h : X −× Z, where f : W → X and h : Y → Z.

X  \overline{Ĝ  ×} Y  \overline{Ĥ  ×} Z

[figure: X × X; Δ_{X}; \overline{X × Ĝ×}; X × Y; \overline{Ĝ × Y ×}; Y × Y; Δ_{Y}]

X × Z \begin{aligned}X × Ĥ \\ & × \end{aligned}  \overline{Ĝ × Z ×} Y × Z \begin{matrix}Y × Ĥ \\ × \end{matrix} \overline{Ĥ × Z ×} Z × Z \begin{matrix}Δ_{Z} \\  \end{matrix}

Proof If G and H are copyable then the two rectangles commute, whilst so does the square if either G = Σ^{g} or H = Σ^{h}. □

Lemma A.10 Let X′ = U \ V ⊂ X be a locally closed subspace and

I = ∀_{c} · ∃_{i} : Σ^{X′} = V ↓ Σ^{X} ↓ U Σ^{X}.

Then Î: X −× X′ is copyable, cf. Lemma A.5 above. Proof Let W ∈ Σ^{X′×X′}, as indicated by the quarter-circle in the Venn diagram [[The pious reader may wish to reformulate this argument in a purely symbolic way. However, to do so would say just the same things, but less clearly.]] of subsets of X × X below. Hence Σ^{Δ_{X′}} (W) is the part of the diagonal within the quarter-circle, and then I : Σ^{X′} Σ^{X} adds the top right part of the diagonal, Δ_{V}.

[figure: V; X′; U; V; X′; U]

On the other hand, consider the effect of

[figure: Σ^{X′×X′}; Σ^{X×X′}; Σ^{X×X}.]

This first expands the open subset W ⊂ X′ × X′ in the horizontal direction, adding the single rectangle V × X′ on the right. Then it expands vertically, adding the three-part rectangle X × V at the top.

Notice that this treats the components asymmetrically, as we have come to expect from the product in HC. Indeed there are two more representations of X′ × X′ as a locally closed subspace of X × X:

• considering it as the intersection of U × U with (X \ V) × (X \ V), the expansion of W would also add the bottom right square;

• taking it to be the intersection of U × U with (X × X) \ (V × V), the expansion would instead omit the top left square.

Nevertheless, whichever representation of X′ × X′ we choose, the restriction to the diagonal is the same, namely Σ^{Δ_{X′}} (W) ∪ Δ_{V}. □

Theorem A.11 F̂ : X −× Y is copyable iff F preserves ∧ and ∨.

\begin{matrix}Σ^{Y} & \overline{F} & Σ^{X} \\ F ⊥ ↓ Σ^{X} ↓ F ⊤ & ^{\begin{aligned}F′ \\ & \end{aligned}. . . . . . . . . . . . . . . .} & [figure: ∀_{c}; ⊤; \underline{Σ^{c}}] & Σ^{X} ↓ F ⊤ & \begin{matrix}\begin{aligned}∃_{i} \\ & \end{aligned} & \\ ⊣ [figure: Σ^{i}] \end{matrix} \end{matrix}

Proof Let i : U ^{⊂}  X be the open subset classified by F ⊤ and c : X′ ^{⊏}  U the closed

subset co-classified by F ⊥. Then let F′ : Σ^{Y} → Σ^{X′} such that F = ∃_{i} · ∀_{c} · F′, so F′ = Σ^{c} · Σ^{i} · F.

If F is copyable then so is F′, by Lemma A.9, as Σ^{c} · Σ^{i} is a homomorphism. But F′ preserves ⊤ and ⊥, so it is also discardable, and therefore F′ = Σ^{f′} for some unique f′ : X′ → Y by Theorem A.8. Hence F = ∃_{i} · ∀_{c} · Σ^{f′} preserves ∧ and ∨ by composition.

Conversely, if F preserves ∧ and ∨ then so does F′ by composition. But it also preserves ⊤ and ⊥, so it is a homomorphism by Theorem 4.1. Then its composite with ∃_{i} · ∀_{c}, which is copyable by Lemma A.10, is also copyable, by Lemma A.9. □

Corollary A.12 Copyable maps between locally compact spaces compose. □

Example A.13 The subspace 2 ≅ {(⊤, ⊥), (⊥, ⊤)} ^{i} Σ × Σ is locally closed, and the Σsplitting

Σ^{2} ≅ Σ × Σ ^{I} Σ^{Σ×Σ}

defined by the quantifiers in Lemma A.10 is

(a, b) ↦ λcd. (a ∧ c) ∨ (b ∧ d) ∨ (c ∧ d).

The four (definable) points of Σ × Σ are taken by I to the black points in the “copyable” diagram:

\begin{aligned}& • \\ & ∘ \\ • & & • \\ & ∘ \\ & • \end{aligned}  \begin{aligned}& ∘ \\ & • \\ • & & • \\ & ∘ \\ & • \end{aligned}  \begin{aligned}& ∘ \\ & • \\ • & & • \\ & • \\ & ∘ \end{aligned}  \begin{aligned}& • \\ & ∘ \\ • & & • \\ & • \\ & ∘ \end{aligned}

ab ∨ ac ∨ bd  ac ∨ bd  ac ∨ bd ∨ cd ab ∨ ac ∨ bd ∨ cd[[ = (a ∨ d)(b ∨ c)]]
preserves ⊥⊤  ⊥∨  ∧∨  ∧⊤
discardable  angelic  copyable  demonic

The other diagrams illustrate different splittings, in which Î is discardable or non-deterministic. (Recall from [A, Introduction] that terms of type Σ are programs that may or may not terminate, amongst which ∨ and ∧ are defined by waiting for one or both of the pair.) In the “angelic” and “demonic” splittings, I is respectively left and right adjoint to Σ^{i}. □

B Interpretation of PCF

Do fixed points and Y here.

Set out the rules of Plotkin’s calculus. Parallel or Plotkin’s “Existential quantifier” some : (Num → Bool) → Bool

some C = \{ \begin{matrix}yes & if ∃n. (Cn = yes) \\ no & if C⊥ = no \\ ⊥ & otherwise \end{matrix}

Interpretation in ASD by continuation-passing. Adequacy and definability.

Remark B.1 Let N : Num; C, D : Bool; x, P, Q : U; M : V; F : U → V (or F : Num → Bool in the last case). Then

[[Num]]  = ℕ_{⊥} ^{⊏} Σ^{ℕ}
[[Bool]]  = 2_{⊥} ^{⊏} Σ × Σ
[[U → V]]  = [[V]]^{[[U]]} ^{⊏} Y^{X} where X = [[U]], [[V]] = C ^{⊏} Y
[[yes]]  = admit(⊤, ⊥) : 2_{⊥}
[[no]]  = admit(⊥, ⊤)
[[0]]  = admit(λn. n = 0) : 𝕋_{⊥}
[[succ N]]  = admit(λn. ∃m. i[[N]]m ∧ n = m + 1)
[[pred N]]  = admit(λn. i[[N]](n + 1))
[[isz N]]  = admit(let ϕ = i[[N]] in ⟨ϕ[0], ∃n. ϕ[n + 1]⟩) : 2_{⊥}
[[if C then P else Q]] = admit(let ⟨ϕ, ψ⟩ = i[[C]] in ϕ ∧ i[[P]] ∨ ψ ∧ i[[Q]]) : [[U]]
[[x]]  = x
[[λx. M]]  = admit(λx. i[[M]]) : [[U → V]]
[[F P]]  = admit(i[[F]](i[[P]])) : [[V]]
[[μx. P]]  = admit(∃n. rec(n, ⊥, λxm. i[[P]])) : [[U]]
[[C por D]]  = admit(let (ϕ, ψ) = i[[C]], (θ, χ) = i[[D]] in ϕ ∨ θ, ψ ∧ χ)
[[some F]]  = admit (∃n. let (ϕ, ψ) = i[[F]]n in ϕ,
let (ϕ, ψ) = i[[F]]⊥ in ψ)

Definability of all elements of Σ^{Σ^{𝕋}} and hence of all morphisms of C.

Remark B.2 Alternative translation based on

[figure: [[Bool]] = 2_{⊥}; ⊏; Σ^{2}; \underline{Σ^{i}}; Σ^{Σ×Σ}]

2[figure: i] Σ × Σ

[figure: [[Num]] = ℕ_{⊥}; ⊏; Σ^{ℕ}; \underline{Σ^{\{\}}}; Σ^{Σ^{ℕ}}]

ℕ[figure: {}] Σ^{ℕ}

C ^{⊏} Σ^{Y} ◁ Σ^{Y′}

C^{X} ^{⊏} Σ^{X×Y} ◁ Σ^{X×Y′}

Pure PCF is done without disjunction.

[[0]]  = admit(λϕ. ϕ[0])
[[yes]]  = admit(λϕψ. ϕ)
[[no]]  = admit(λϕψ. ψ)
[[succ N]]  = admit(λϕ. i[[N]])(λn. rec(n, ϕ[0], λxm. ϕ[m])
[[isz N]]  = admit(λϕψ. i[[N]](λn. rec(n, ϕ, λxm. ψ)))
[[if C then P else Q]] = admit(i[[C]](i[[P]])(i[[Q]]))

Remark B.3 New operational semantics by translation of ASD into PROLOG. Global element of 𝕋 in ASD translates into a terminating PROLOG program that returns this value, hence adequacy of denotational semantics for PCF.

Remark B.4 Abramsky’s lazy λ-calculus.

C The fixed point property

Topologically, ℕ is a discrete space, but we also understand it to carry an “imposed” order relation in which 0 < 1 < 2 < · · ·. We begin by constructing an object N for which this is the intrinsic (Σ-)order. There is another object, called ϖ, in which these finite ascending numerals have a join, \overline{∞}. One way of expressing the fixed point or continuity axiom is to postulate that these two objects be isomorphic.

Lemma C.1 Let U ⊂ Σ^{ℕ} consist of functions that are ascending, in the sense that n : ℕ ⊢ ϕ[n] ≤ ϕ[n + 1] with respect to the semilattice order ≤ on Σ. Then U is well defined as an object of \overline{C}, and uniquely carries the structure of an Eilenberg–Moore subalgebra of Σ^{ℕ}, the inclusion being split by a function. Proof U ◁ Σ^{ℕ} splits the idempotent ϕ ↦ ϕ^{↑} defined using primitive recursion by

ϕ^{↑}(0) = ϕ(0) ϕ^{↑}(n + 1) = ϕ(n + 1) ∨ ϕ^{↑}(n).

Then there is a pullback in \overline{C},

Σ^{ℕ}[figure: ⟨id, Σ^{succ}⟩] Σ^{ℕ} × Σ^{ℕ}  2

[figure: U; Σ^{Σ×ℕ}; Σ^{p×ℕ}; Σ; p]

in which the maps on the top and right are Eilenberg–Moore homomorphisms, whence so is that on the left. [[U is the inserter of id and Σ^{succ}.]] □

Corollary C.2 The inclusion U Σ^{ℕ} is the inverse image of some morphism ℕ ↠ N in C that’s Σ-split epi. [[Pick up pts(A, α) in [B, Examples]: this is N = {Σ^{Σ^{ℕ}} | Σ^{(−)^{↑}}}.]] This defines ascending numerals

\overline{n} = admit(λϕ. ϕ^{↑}[n]) = admit(λϕ. ∃m. m ≤ n ∧ ϕ[m]).  □

Now here is the sense in which N carries the arithmetic order intrinsically.

Lemma C.3 Every function ℕ → Σ that is monotone in the sense that it takes the arithmetic order to the logical one extends uniquely to N → Σ. [[Formula for lifting: as in Proposition C.6.]] Hence ℕ → N is Σ-split epi.

ℕ  \overline{}N

[figure: Σ; ∃!; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; monotone]

Proof Monotone f : Γ × ℕ → Σ^{Δ} correspond to monotone Γ × Δ → Σ^{ℕ} that factor through Γ × Δ → U = Σ^{N}, which correspond to \overline{f} : Γ × N → Σ^{Δ}. Γ, ν : N ⊢ · · ·. □

Remark C.4 Similarly, the object D ◁ Σ^{ℕ} of descending functions is the topology on a domain N of “descending integers”. However, ϖ ≡ D itself is another domain of ascending integers, this time with a greatest element:

\overline{n} = admit(λk. k < n) \overline{∞} = admit(λk. ⊤),

in particular \overline{0} = (λk. ⊥).

Lemma C.5 The homomorphism H : Σ^{D} → U corresponding to the lifting N → ϖ of

n ↦ admit(λk. k < n) is F ↦ λn. admit(iF (λk. k < n)).
ℕ  \overline{}N

ϖ = D = Σ^{N} ∃! ; ..........................^{monotone  \overline{}}

F \overline{n} = HF n.

Moreover,

J : U → Σ^{D}  by  ϕ ↦ admit(λν. iϕ[0] ∨ ∃n. iϕ[n + 1] ∨ iν[n])

satisfies H · J = id_{U} (so N → ϖ is Σ-split mono) and takes (λk. m ≤ k) to {k | m ≤ k}.

Also, for Γ ⊢ ϕ : U, we have Jϕ\overline{n} = iϕ[n] and Jϕ\overline{∞} = ∃n. iϕ[n]. Proof earlier parts?

Jϕ\overline{n} = iϕ[0] ∨ ∃k. iϕ[k + 1] ∧ i\overline{n}k
= iϕ[0] ∨ ∃k. iϕ[k + 1] ∧ k < n
= iϕ[n]  ϕ monotone
Jϕ\overline{∞} = iϕ[0] ∨ ∃k. iϕ[k + 1] ∧ i\overline{∞}k
= iϕ[0] ∨ ∃k. iϕ[k + 1] ∧ ⊤
= ∃n. iϕ[n] = ∃n. J(iϕ)\overline{n}  □

Proposition C.6 Suppose that N ≅ ϖ, so that also H · J = id_{U}. Then every (sober) object has and every morphism preserves joins of ℕ-indexed ascending sequences. Proof Let Γ, n : ℕ ⊢ x_{n} : X with Γ, n : ℕ, ϕ : Σ^{X} ⊢ ϕ[x_{n}] ≤ ϕ[x_{n+1}]. Then Γ, ϕ : Σ^{X} ⊢ λn. ϕ[x_{n}] : U ◁ Σ^{ℕ} and so Γ, ϕ : Σ^{X} ⊢ J(λn. ϕ[x_{n}]) : Σ^{D}.

Since H · J = id_{U},

λϕ. ϕx_{n} = η_{X}(x_{n}) = λϕ. (λn. ϕx_{n})n
= λϕ. H(J(λn. ϕx_{n}))n
= λϕ. J(λn. ϕx_{n})(λk. k < n)

so the upper square commutes:

n  admit(λk. k < n)

Γ × ℕ  [figure] Γ × N ≅ Γ × ϖ ν

[figure: X; x_{(−)}; η_{X}; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; Σ^{Σ^{X}}; λϕ. J(λn. ϕx_{n})ν]

[figure: Y; f; η_{Y}; Σ^{Σ^{Y}}; Σ^{Σ^{f}}]

Now, the assumption J · H = id says that ℕ → ϖ is Σ-epi, so there is a unique diagonal mediator as shown, which means that

Γ, ν : ϖ ⊢ focus(λϕ. J(λn. ϕ[x_{n}])ν) : X

is well formed, i.e. that λϕ. J(λn. ϕ[x_{n}])ν is prime [[maybe a direct proof of this?]]. Putting ν = \overline{∞}, we may define

Γ ⊢ ⋁ ; _{n}x_{n} ≡ focus(λϕ. ∃n. ϕ[x_{n}]) : X.

This construction of ⋁ ; _{n} x_{n} is monotone: if Γ, n : ℕ ⊢ x_{n} ≤ y_{n} then ⋁ ; x_{n} ≤ ⋁ ; y_{n}. Also, if y_{n} takes the same value y_{0} independently of n then ⋁ ; _{n} y_{n} = y_{0}. It follows that ⋁ ; _{n} x_{n} really is the least upper bound of the sequence (x_{n}).

Now let f : X → Y, so Γ, n : ℕ ⊢ fx_{n} ≤ fx_{n+1}. Then

f(⋁ ; _{n}x_{n}) = f(focus(λϕ. ∃n. ϕ(x_{n})))
= focus(Σ^{2}f(λϕ. ∃n. ϕ(x_{n})))
= focus(λψ. ∃n. ψ(fx_{n})))
= ⋁ ; _{n}fx_{n},

which we may alternatively deduce from naturality of the diagram above with respect to f. □

Lemma C.7 Let Γ, n : ℕ ⊢ x_{n} : X be an increasing sequence, i.e.

Γ, n : ℕ, ϕ : Σ^{X} ⊢ ϕ[x_{n}] ≤ ϕ[x_{n+1}] : Σ.

Then Γ ⊢ P ≡ λϕ. ∃n. ϕ[x_{n}] is prime and

Γ ⊢ ⋁ ; _{n}x_{n} ≡ focus(λϕ. ∃n. ϕ[x_{n}])

is the least upper bound of the sequence. Proof Put Γ, F : Σ^{3}X ⊢ F = λψ. F(λϕ. ∃n. ϕ[x_{n}] ∧ ψ[n]) : Σ^{Σ^{ℕ}}. Then

P (λx. F(λϕ. ϕ[x])) = ∃m. (λx. F(λϕ. ϕ[x]))x_{m}
= ∃m. F(λϕ. ϕ[x_{m}])
= ∃m. F(λϕ. ∃n. ϕ[x_{n}] ∧ n ≤ m)  (x_{n}) increasing
= ∃m. F (λn. n ≤ m)
= F ⊤  Scott principle
= F(λϕ. ∃n. ϕ[x_{n}]) = FP

In the case of a constant sequence, y_{n} = y_{0}, ⋁ ; y_{n} = y_{0}. On the other hand, if Γ, n : ℕ ⊢ x_{n} ≤ y_{n} then Γ ⊢ ⋁ ; x_{n} ≤ ⋁ ; y_{n}. So the construction yields the least upper bound. □

Corollary C.8 If (N ≅ ϖ and) X has ⊥ then every f : X → X has a least fixed point. Proof Put x_{n} = f^{n}⊥ = rec(n, ⊥, λnx. fx); this is monotone by induction on n, so long as ⊥ ≤ fx. Then ⋁ ; x_{n} is the least fixed point of f by a familiar argument. □

These results can be presented in terms of algebras and coalgebras for the lift functor, although the following results will not be used in the rest of the paper. Proposition 4.5 below uses the fixed point property to show that Σ^{X_{⊥}} = Σ ↓ Σ^{X}, where X_{⊥} is the partial map classifier. [D] studies the lift without using the fixed point property.

Lemma C.9 Σ^{ℕ} is the final coalgebra for Σ × (−) : C → C. Proof Σ^{ℕ} is the collection of streams of type Σ; its algebra structure adjoins a new value on the front of the stream, and the coalgebra structure detaches it: ϕ ↦ (ϕ[0], λk. ϕ[k + 1]).

Σ × A^{......... \begin{matrix}(id, ϕ) \\  \end{matrix}}Σ × Σ^{ℕ}

[figure: A; (h, t); .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; ϕ; Σ^{ℕ}; ≅; cons]

Given any other coalgebra as shown, commutativity of the square requires

ϕ(a) = ha :: ϕ(ta) = (ha, hta, ht^{2}a, ...) = λn. h(rec(n, a, t)).  □

Given a map κ : Σ → A (which, by the Phoa principle, is determined by κ⊥ ≤ κ⊤ ∈ A [[working in Σ ↓ C?]]),

Σ ↓ A = {(σ, a) | κσ ≤ a},

which is well defined as an object of C because it’s a retract of Σ × A.

Lemma C.10 If A is an algebra then so are Σ ↓ A and A ↓ Σ. Proof [[Copy from [D].]] □

Indeed it is an algebra if A is, by an argument similar to Lemma C.1.

Lemma C.11 U and D are the final coalgebras in Σ ↓ C for Σ × (−), Σ ↓ (−) and (−) ↓ Σ respectively. Proof (h, t) : A → Σ ↓ A is well defined so long as ∀a. κ(ha) ≤ ta [[then ∀a. ha ≤ hta?]], and the same formula for ϕ : A → U is valid. □

Definition C.12 Focal property, equivalent to being an algebra for the lift monad:

Σ^{X}[figure] Σ ↓ Σ^{X}.

Also, an algebra for the lift functor consists of b ∈ X, f : X → X such that ∀x. b ≤ fx.

Proof X [figure: ⊂; (b,id)] X_{⊥} where b ≤ id, which means ∀x. b ≤ x. □

For a pointed object p : 1 → X, Σ^{X} is a coalgebra for Σ × (−).

Proposition C.13 N is the initial lift algebra.

\begin{matrix}X_{⊥} & ................ & N_{⊥} \\ X & \begin{aligned}(b, f) \\ & \end{aligned} & .................... & N & \end{matrix}

Proof In Lemma C.11, \overline{n} ↦ f^{n}(b) ∈ X; ascending since ∀x. b ≤ fx. Lifts λn. f^{n}b. If (h, t) : A → Σ ↓ A is a homomorphism then so is ϕ [[why?]] □

Lemma C.14 Σ^{Σ↓A} ≅ Σ^{A} ↓ Σ. Proof Let κ : Σ → A be the unique map that preserves ⊥ and ⊤. Then Σ ↓ A = {(σ, a) | κσ ≤ a} and Σ^{A} ↓ Σ = {(ϕ, τ) | ϕ ≤ λa. τ}.

Define Σ^{Σ↓A} → Σ^{A} ↓ Σ by ψ ↦ (ϕ, τ) where ϕ = λa. ψ(⊥, a) and τ = ψ(⊤, ⊤).

Conversely, define Σ^{A} ↓ Σ → Σ^{Σ↓A} by (ϕ, τ) ↦ ψ where ψ = λ(σ, a). ψ[a] ∨ (σ ∧ τ).

Then

ψ ↦ λ(σ, a). ψ(⊥, a) ∨ σ ∧ ψ(⊤, ⊤) = ψ

by Phoa. Conversely,

(ϕ, τ) ↦ (λa. ϕa ∨ (⊥ ∧ τ), ϕ⊤ ∨ τ) = (ϕ, τ)

since ϕ⊤ ≤ τ. □

Proposition C.15 ϖ is the final lift coalgebra. Proof By Lemma C.11, D is the final coalgebra for the functor (−) ↓ Σ (so N is the initial drop algebra on C). But by Lemma C.14, Σ^{D} ≅ Σ^{D↓Σ} ≅ Σ ↓ Σ^{D}. [[Formula for corecursion.]] □

Remark C.16 Discuss Crole–Pitts, Scott, Freyd and Plotkin axioms.

Theorem C.17 The following are equivalent:

(a) N ≅ ϖ;

(b) every object has and every map preserves ⋁ ; ;

(c) F : Σ^{Σ^{𝕋}}, ϕ : Σ^{𝕋} ⊢ F ϕ = ∃ℓ. F ϕ_{ℓ};

(d) F : Σ^{Σ^{𝕋}}, ϕ : Σ^{𝕋} ⊢ F ϕ = ∃ℓ. F (λn. n ∈ ℓ) ∧ ∀n ∈ ℓ. ϕ[n]. Proof [a⇒b] Proposition C.6. [b⇒c] F : Σ^{X} → Σ preserves ϕ = ⋁ ; _{ℓ} ϕ_{ℓ}; [c⇒d] By the Lemma,

F ϕ = ∃ℓ. F ϕ_{ℓ} = ∃ℓ. ∃ℓ′ ⊂ ℓ. F (λn. n ∈ ℓ′)∧∀n ∈ ℓ′. ϕ[n] = ∃ℓ′. F (λn. n ∈ ℓ′)∧∀n ∈ ℓ′. ϕ[n].

[d⇒a] For F : Σ^{D} ◁ Σ^{Σ^{𝕋}} and ν : D ◁ Σ^{𝕋},

J(HF)ν = F (λk. k < 0) ∨ ∃n. F (λk. k < n + 1) ∨ ν[n] = F ν

since ν is monotone, where n corresponds to the list ℓ = [0, 1, …, n − 1]. □

D Algebraic types

Lemma C.1 constructed objects N and ϖ whose intrinsic order is that of the imposed arithmetical order on ℕ, although ϖ has an additional element \overline{∞}. Similarly, the elements of 𝕋 are considered as lists, and therefore as finite sets, together with an imposed inclusion order, whilst the elements of Σ^{𝕋} are (infinite but recursively enumerable) sets in which the inclusion order is the intrinsic one.

Develop more complicated closure conditions, working towards Scott domains.

Remark D.1 This is a closure operation: it closes a collection of lists under sublists (extension?), permutations and repetitions. This is a unary closure, but there is no right adjoint, as ∀_{𝕋} would be derivable from it.

Definition D.2 An object X is algebraic if there are maps

Σ^{X}  X  X

Σ^{𝕋} [figure: S_{X}]⊣ \begin{matrix}Σ^{s_{X}} \\  \end{matrix}𝕋[figure: s_{X}] [figure: i_{X}]

S_{X} = Σ^{i_{X}} · S_{Σ^{𝕋}} and I_{X} = S_{Σ^{𝕋}} · Σ^{s_{X}}. Lemma D.3 Σ^{𝕋} is algebraic.

Σ^{Σ^{𝕋}} Σ^{𝕋} Σ^{𝕋}

Σ^{𝕋} [figure: S]⊣ \begin{matrix}Σ^{s} \\  \end{matrix}𝕋[figure: s] Σ^{𝕋} \begin{matrix}i_{Σ^{𝕋}} = id \\  \end{matrix}

where

s : 𝕋 ≅ List(𝕋) → Σ^{𝕋}  by s_{L} : ℓ ↦ λn. (n ∈ ℓ)
S : Σ^{𝕋} → Σ^{Σ^{List(𝕋)}} ≅ Σ^{Σ^{𝕋}} by S : ϕ ↦ λψ. ∃ℓ. [ϕ(ℓ) ∧ ∀n ∈ ℓ. ψ(n)].

Also,

ϕ : Σ^{𝕋} ⊢ ϕ ≤ Σ^{s}(Sϕ) and ℓ : List𝕋 ⊢ S(λm. m = ℓ)(sℓ) = ⊤.

So S ⊣ Σ^{s}, but S doesn’t preserve ⊤ or ∧, so s isn’t an open or proper surjection, nor is Ŝ copyable. Proof

S(Σ^{s}F)ψ  = ∃ℓ. Σ^{s}F ℓ ∧ ∀n ∈ ℓ. ψ[n]
= ∃ℓ. F (λn. n ∈ ℓ) ∧ ∀n ∈ ℓ. ψ[n]
= F ψ  Theorem 2.8
Cϕℓ = Σ^{s}(Sϕ)ℓ = (Sϕ)(sℓ)
= ∃ℓ′. ϕℓ′ ∧ ∀n ∈ ℓ′. n ∈ ℓ
= ∃ℓ′ ⊂ ℓ. ϕℓ′
≥ ϕℓ  □

Lemma D.4 If X is algebraic then so is Σ^{X}. Proof i_{Σ^{X}} = Σ^{s_{X}}, whilst s_{Σ^{X}} and S_{Σ^{X}} are defined by

[figure: Σ^{Σ^{X}}; Σ^{X}]

Σ^{Σ^{𝕋}} [figure: Σ^{Σ^{s_{X}}}]⊣ \begin{matrix}Σ^{S_{X}} \\  \end{matrix}Σ^{𝕋} [figure: S_{X}]

S_{Σ^{X}}  Σ^{𝕋} [figure: S_{𝕋}]⊣ \begin{matrix}Σ^{s_{𝕋}} \\  \end{matrix}𝕋[figure: s_{𝕋}]  s_{Σ^{X}}

where s_{𝕋} was given in Corollary D.3. □

Remark D.5 In particular, s_{Σ} = ∃_{𝕋} · s_{Σ^{𝕋}} and S_{Σ} = Σ^{2}!_{𝕋} · S_{Σ^{𝕋}}, but this might as well be

\begin{matrix}(σ, σ ∨ τ) & Σ^{Σ} & Σ \\ (σ, τ) & & Σ^{2} & ^{[figure]⊣ } & 2 & [figure] \end{matrix}

Lemma D.6 The types 1, 𝕋 and 𝕋 × 𝕋 are algebraic. Proof

\begin{matrix}s_{1} =!_{𝕋} & S_{1} = ∃_{𝕋} & i_{1} = ⊤ \\ s_{𝕋} = id_{𝕋} & S_{𝕋} = id_{Σ^{𝕋}} & i_{𝕋} = \{\} \end{matrix}

s_{𝕋×𝕋} : 𝕋 → 𝕋 × 𝕋 by 0 ↦ ⟨0, 0⟩ and [n, m] ↦ ⟨n, m⟩.

i_{𝕋×𝕋} : 𝕋 × 𝕋 → Σ^{𝕋} by ⟨n, m⟩ ↦ {[n, m]}. S_{𝕋×𝕋} : Σ^{𝕋×𝕋} → Σ^{𝕋} by

S_{𝕋×𝕋}ϕ⟨n, m⟩ = \{ \begin{matrix}ϕ[0, 0] ∨ ϕ0 & if n = m = 0 \\ ϕ[n, m] & otherwise \end{matrix}

Then S_{𝕋×𝕋}ϕ ≤ θ ⟺ ∀n, m. ϕ[n, m] ≤ θ⟨n, m⟩ & ϕ0 ≤ θ⟨0, 0⟩ ⟺ ϕ ≤ Σ^{s_{𝕋×𝕋}}θ. □ Lemma D.7 ⊩_{𝕋×𝕋}.

\begin{matrix}(ϕ, ψ) & Σ^{𝕋} × Σ^{𝕋} & 𝕋 + 𝕋 & ν_{0}0 & ν_{0}n & ν_{1}n \\ θ & Σ^{𝕋} & ^{[figure]⊣ } & 𝕋 & [figure] & 0 & & [0, n] & & [[p, q], n] & \end{matrix}

An essentially arbitrary covering of the disjoint union 𝕋 + 𝕋.

θ0  = ϕ0
θ[0, n]  = ϕn
θ[[p, q], n]  = ψn
ϕn  = θ[0, n] ∨ (n = 0 ∧ θ0)
ψn  = ∃pq. θ[[p, q], n]
Cθ0  = θ[0, 0] ∨ θ0
Cθ[0, n]  = θ[0, n] ∨ θ0
Cθ[[p, q], n] = ∃p′q′. θ[[p′, q′], n]
ℓ ⊩ 0  = [0, 0] ∈ ℓ ∨ 0 ∈ ℓ
ℓ ⊩ [0, n]  = [0, n] ∈ ℓ ∨ 0 ∈ ℓ
ℓ ⊩ [[p, q], n] = ∃p′q′. [[p′, q′], n] ∈ ℓ  □

Lemma D.8 If X and Y are algebraic then so is X × Y. Proof s_{X×Y} : 𝕋 → X × Y and S_{X×Y} : Σ^{𝕋} → Σ^{X×Y} are given by the diagonal composites from bottom to top right in the diagrams

[figure: Σ^{X×𝕋}; S_{Y}^{X}; ⊥; Σ^{X×s_{Y}}; Σ^{X×Y}; X × 𝕋; X × s_{Y}; X × Y]

Σ^{𝕋×𝕋} [figure: S_{X}^{𝕋}]⊣ \begin{matrix}Σ^{s_{X}×𝕋} \\  \end{matrix}[figure: S_{Y}^{𝕋}; ⊥; Σ^{𝕋×s_{Y}}] Σ^{𝕋×Y} [figure: S_{X}^{Y}]⊣ \begin{matrix}Σ^{s_{X}×Y} \\  \end{matrix}𝕋 × 𝕋 [figure: s_{X} × 𝕋]  [figure: 𝕋 × s_{Y}] 𝕋 × Y [figure: s_{X} × Y]

Σ^{𝕋} [figure: S_{𝕋×𝕋}]⊣ \begin{matrix}Σ^{s_{𝕋×𝕋}} \\  \end{matrix}𝕋[figure: s_{𝕋×𝕋}]

where the square of left adjoints commutes because that of right adjoints does.

Also, i_{X×Y} = i_{Σ^{𝕋}×Σ^{𝕋}} · (i_{X} × i_{Y}). □

Proposition D.9 For every object (context or product of types) X that is definable in the restricted λ-calculus. □

Remark D.10 ℓ ⊢_{X} n if s_{X}(n :: ℓ) = s_{X}ℓ. i_{X}(s_{X}ℓ) = λℓ′. ∀n ∈ ℓ′. ℓ ⊢_{X} n.

If X is logical then ℓ′ ⊂ ℓ ⇒ s_{X}ℓ′ ≤ s_{X}ℓ (including permutation and repetition).

[figure: 𝕋; s_{X}; X; Σ; ϕ; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; f]

If ℓ ⊢_{X} n ⇒ f(n :: ℓ) ≤ fℓ then there is a unique map ϕ. □

Theorem D.11 The subcategory of locally compact spaces is the minimal model. Proof Every definable object is a Σ-split subspace of Σ^{𝕋} and there is a diagram

[figure: 𝕋; s; ×; Σ^{𝕋}; i; \overline{\overline{×}}; X]

Remark D.12 For any such s, S, S(λm. m = ℓ)(sℓ) = C(λm. m = ℓ)ℓ ≥ (λm. m = ℓ)ℓ = ⊤. Construct N and N again as examples.

E Lattices

Move to a new paper on powerdomains and relational algebra.

Definition E.1 A σ-semilattice is an object A equipped with a join operator

{Γ, n : ℕ ⊢ f[n] : A \atop Γ ⊢ ⋁_{n} f[n] : A}

that agrees with the intrinsic order on A.

Lemma E.2 Any semilattice is a σ-semilattice, likewise maps.

Γ × ℕ

[figure: Γ × Listℕ; g; A; f; B]

[figure: Γ × Σ^{ℕ}; .; .; .; .; .; .; .; .; .; .; .; h; k; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; Σ^{2}A; η_{A}; Σ^{2}B; η_{B}]
gℓ  = ⋁_{n∈ℓ} fn
hϕ  = λψ. ∃ℓ. ψ[⋁_{n∈ℓ} fn] ∧ ∀n ∈ ℓ. ϕ[n]
h(λn. n ∈ ℓ) = λψ. ∃ℓ′. (ℓ′ ⊂ ℓ) ∧ ψ[ ⋁_{n∈ℓ′} fn]
= λψ. ψ[⋁_{n∈ℓ} fn]
= η_{A}[gℓ]
kϕ  = focus[λψ. ∃ℓ. ψ[⋁_{n∈ℓ} fn] ∧ ∀n ∈ ℓ. ϕ[n]]
⋁ f  = focus[λψ. ∃ℓ. ψ[⋁_{n∈ℓ} fn]]

If Γ ⊢ P : Σ^{3}𝕋 preserves ⊥ and ∨ then it also preserves ∃_{𝕋}. □ Definition E.3 A σ-frame is a σ-semilattice A that is also equipped with ⊤ : 1 → A and ∧ : A × A → A. agreeing with the intrinsic order on A and satisfying the frame axioms, in particular distributivity of ∧ over ⋁. Lemma E.4 Σ is the initial σ-frame. Proof Let κ : Σ → A be the unique map that preserves ⊥ and ⊤. Then it preserves ∧ and ⋁ too. □ Lemma E.5 Σ^{Σ^{ℕ}} is the free σ-frame on ℕ. Proof Let f : ℕ → A. For F : Σ^{Σ^{ℕ}}, put

pF = ⋁_{ℓ:Listℕ} κ[F (λn. n ∈ ℓ)] ∧ ⋀_{n∈ℓ} f[n].

Then

p(η_{ℕ}m)  = p(λϕ. ϕ[m])
= ⋁_{ℓ:Listℕ} κ[(λϕ. ϕ[n])(λn. n ∈ ℓ)] ∧ ⋀_{n∈ℓ} f[n]
= ⋁_{ℓ:Listℕ} κ[m ∈ ℓ] ∧ ⋀_{n∈ℓ} f[n]
= f[m]  putting ℓ = [m]
p(⊤)  = ⋁_{ℓ:Listℕ} κ[(λϕ. ⊤)(λn. n ∈ ℓ)] ∧ ⋀_{n∈ℓ} f[n]

= ⋁_{ℓ:Listℕ} κ[⊤] ∧ ⋀_{n∈ℓ} f[n]
= ⊤  putting ℓ = ∅
p(F_{1} ∧ F_{2}) = ⋁_{ℓ:Listℕ} κ[(F_{1} ∧ F_{2})(λn. n ∈ ℓ)] ∧ ⋀_{n∈ℓ} f[n]
= ⋁_{ℓ:Listℕ} κ[F_{1}(λn. n ∈ ℓ)] ∧ κ[F_{2}(λn. n ∈ ℓ)] ∧ ⋀_{n∈ℓ} f[n]
= ⋁_{ℓ_{1}:Listℕ} ⋁_{ℓ_{2}:Listℕ} κ[F_{1}(λn. n ∈ ℓ_{1})] ∧ κ[F_{2}(λn. n ∈ ℓ_{2})] ∧ ⋀_{n∈ℓ_{1}} f[n] ∧ ⋀_{n∈ℓ_{2}} f[n]
= ⋁_{ℓ_{1}:Listℕ} κ[F_{1}(λn. n ∈ ℓ_{1})] ∧ ⋀_{n∈ℓ_{1}} f[n]
∧ ⋁_{ℓ_{2}:Listℕ} κ[F_{2}(λn. n ∈ ℓ_{2})] ∧ ⋀_{n∈ℓ_{2}} f[n]  distributivity
= pF_{1} ∧ pF_{2}
p(∃k. F_{k}) = ⋁_{ℓ:Listℕ} κ[(∃k. F_{k})(λn. n ∈ ℓ)] ∧ ⋀_{n∈ℓ} f[n]
= ⋁_{ℓ:Listℕ} ⋁_{k} κ[F_{k}(λn. n ∈ ℓ)] ∧ ⋀_{n∈ℓ} f[n]
= ⋁_{k} pF_{k}  □

Lemma E.6 Let A be a σ-frame together with s : ℕ → A, S : Σ^{ℕ} → Σ^{A} such that S ; Σ^{s} = id_{Σ^{ℕ}} and S(λn. m = n)(sm) = ⊤. Then A is an Eilenberg–Moore algebra.

[figure: Σ^{2}ℕ; Σ^{2}π; Σ^{4}ℕ; Σ^{4}s; Σ^{4}A]

[figure: ℕ; η_{ℕ}; π; Σ^{2}ℕ; Σ^{η_{Σ^{ℕ}}}; Σ^{2}s; Σ^{S}; Σ^{2}A; Σ^{2}α; Σ^{η_{Σ^{A}}}; Σ^{2}p]

[figure: ℕ; η_{ℕ}; s; A; α; η_{A}; p]

Proof Let p : Σ^{2}ℕ → A be the lifting of s : ℕ → A to a σ-frame homomorphism. We shall show that α = Σ^{S} ; p : Σ^{2}A → A is an Eilenberg–Moore structure map.

The composite s; η_{A} ; Σ^{S} ; p takes

m to ⋁_{ℓ} κ[(λϕ. (Sϕ)(sm)))(λn. n ∈ ℓ)] ∧ ⋀_{n∈ℓ} s[n]
= ⋁_{ℓ} κ[S(λn. n ∈ ℓ)(sm)] ∧ ⋀_{n∈ℓ} s[n]
= s[m]  ℓ = [m]

since S(λn. m = n)(sm) = ⊤ and S⊥(sm) = ⊥. Hence η_{A} ; α = η_{A} ; Σ^{S} ; p = id since s is Σ-epi. Now

η_{ℕ} ; Σ^{2}π ; Σ^{4}s; Σ^{2}α; α = π ; Σ^{2}s; α; η_{A} ; α
= π ; Σ^{2}s; α

= π ; Σ^{2}s; η_{Σ^{2}α} ; Σ^{η_{Σ^{A}}} ; α
= η_{ℕ} ; Σ^{2}π Σ^{4}s; Σ^{η_{Σ^{A}}} ; α

so Σ^{2}π; Σ^{4}s; Σ^{2}α; α = Σ^{2}π Σ^{4}s; Σ^{η_{Σ^{A}}} ; α as these are σ-frame homomorphisms Σ^{2}ℕ → A. Then Σ^{2}α; α = Σ^{η_{Σ^{A}}} ; α since Σ^{2}π ; Σ^{4}s is Σ-epi. □

Corollary E.7 If A is an algebra then its structure is unique. □

Remark E.8 If A is a distributive lattice in the intrinsic order, then A is an algebra. Need powerdomain ideas to do this.

F Functional relations on ℕ

In this section we shall prove and exploit the fact that the inclusion {} : ℕ Σ^{ℕ} is locally closed. Thus, we may regard ϕ : Σ^{ℕ} as a copyable program whose “normal” behaviour is to return the n. ϕ[n], terminating if ∃n. ϕ[n], but it aborts if

Dψ ≡ ∃mn. ϕ[n] ∧ ϕ[m] ∧ n ≠ m.

[[Generalise to N/ℕ, overt discrete compact Hausdorff locally compact.]]

Remark F.1 Recall from [D] that c : ℕ_{⊥} → Σ^{ℕ} is defined by lifting {} : ℕ → Σ^{ℕ}.

[figure: ℕ; {}; Σ^{ℕ}; Σ^{ℕ}; Σ^{Σ^{ℕ}}]

ℕ_{⊥}^{∩} .............. (Σ^{ℕ})_{⊥}^{⊣ ∩}  Σ ↓ Σ^{ℕ}^{⊣ } \underline{}Σ ↓ Σ^{Σ^{ℕ}}^{⊣ ⊣ }

Then Σ^{c} : F ↦ (F ∅, λn. F {n}).

Proposition F.2 c : ℕ_{⊥} → Σ^{ℕ} is the closed subset that is classified by D = ⊥.

[figure: ℕ_{⊥}; 1; Σ^{ℕ}; c; ⊓; D; Σ; ⊥]

Proof Consider ∀_{c} : Σ^{ℕ_{⊥}} ≡ Σ ↓ Σ^{ℕ} → Σ^{Σ^{ℕ}} defined by

∀_{c}(σ, ϕ)ψ = σ ∨ (∃n. ϕn ∧ ψn) ∨ (∃nm. ψn ∧ ψm ∧ n ≠ m).

Then

Σ^{c}(∀_{c}(σ, ϕ)) = (σ, λn. σ ∨ ϕn)
= (σ, ϕ)  σ ≤ ϕ[n]
∀_{c}(Σ^{c}F)ψ = F ⊥ ∨ (∃n. F {n} ∧ ψ[n]) ∨ (∃mn. ψ[m] ∧ ψ[n] ∧ m ≠ n)
= (∃ℓ. F (λn. n ∈ ℓ) ∧ ∀n ∈ ℓ. ψ[n]) ∨ (∃mn. ψ[m] ∧ ψ[n] ∧ m ≠ n)
= F ψ ∨ Dψ

by Theorem 2.8 [[which uses 𝕋]], where the cases for lists with two or more distinct elements are absorbed into the term Dψ. □

Remark F.3

[figure: ℕ; ⊂; i; ℕ_{⊥}; ⊏; c; Σ^{ℕ}; Σ^{ℕ}; ∃_{i}; ⊥; \underline{Σ^{i}}; Σ^{ℕ_{⊥}}; ∀_{c}; ⊤; \underline{Σ^{c}}; Σ^{Σ^{ℕ}}]

Σ^{{}} ⊣ A, where Aϕψ = (∃n. ϕn ∧ ψn) ∨ (∃mn. ψn ∧ ψm ∧ n ≠ m).

Remark F.4

[figure: (ℕ_{⊥})^{ℕ}; 1; 1; Σ^{ℕ×ℕ}; ⊓; D^{ℕ}; Σ^{ℕ}; ⊥; ∃; Σ; ⊥]

where D^{ℕ}ϕ = λx. ∃yz. ϕ[y] ∧ ϕ[z] ∧ y ≠ z.

Remark F.5 {} : ℕ → Σ^{ℕ} is the locally closed subset classified by (D, ∃_{ℕ}) = (⊥, ⊤).

[figure: ℕ; 1; ℕ^{ℕ}; 1; ℕ_{⊥}; ∩; ∃; Σ; ⊤; (ℕ_{⊥})^{ℕ}; Σ^{ℕ}; ⊤]

(−)^{ℕ} preserves pullbacks, i.e. if the pullback exists then it’s the exponential, and vice versa. The map ℕ^{ℕ} → (ℕ_{⊥})^{ℕ} is a regular mono, but is not Σ-split.

Remark F.6 Lazy NNO with and without ⊤. ℕ_{⊥} ◁ lazy N ^{⊏}  2_{⊥}^{ℕ} ^{⊏}  Σ^{2×ℕ} — by general

recursion.

Also Moggi’s example: one-point compactification ℕ_{∞} as a non-Σ-split subspace of lazy N.

Theorem F.7 Let X be overt, discrete, Hausdorff and locally compact. Then X ≅ U ^{⊂} ℕ. It’s also compact iff it’s finite. Proof {} : X Σ^{X} is locally closed and X_{⊥}^{⊤} ◁ Σ^{X} ◁ Σ^{ℕ} ↞ ℕ. What’s the inverse image of ⊥ ∈ X_{⊥}^{⊤}, as a closed subspace of ℕ? {n | 0 ⊩_{X} n}, which is both open and closed.

[figure: 𝕋; q; 𝕋/R; \{\}; Σ^{𝕋/R}; Σ^{q}; ⊤; \underline{∃_{q}}; Σ^{𝕋}]

[figure: Σ^{𝕋}; Σ^{q}; ⊤; ∃_{q}; Σ^{𝕋/R}; \underline{Σ^{\{\}}}; ⊤; I; Σ^{2}𝕋/R; Σ^{∃_{q}}; ⊤; \underline{Σ^{2}q}; Σ^{Σ^{𝕋}}]

I ⊣ Σ^{{}}, where I : ϕ ↦ λψ. ϕ[n] ∧ ψ[n].

G For later work

Dual fixed point axiom:

\begin{aligned}ℕ & \overline{} & N & \overline{} & U \\ & & X & \overline{} & ............................... \end{aligned}

Objects that think that ℕ is compact, i.e. admit N-meets.

All objects as locales or PERs. Open discrete objects form an arithmetic universe. Representation theorems: for free model, as PERs; minimal models with all objects open, as

countably based locally compact locales.

One-point compactification of ℕ as open subset of lazy natural numbers, or as patch topology on ℕ_{⊥}. Moggi’s counterexample; why it is not Σ-split. Cauchy sequence ≈ function from lazy ℕ; Euclidean topology on ℚ (≅ ℝ).

Zariski and p-adic topologies on ℕ (Vickers?) Lift as free “local space”. Lift as a co-KZ-monad. Denotational semantics and domain equations. ℕ-indexed limits of compact Hausdorff spaces and ℕ-indexed colimits of open discrete spaces,

by the limit-colimit coincidence.

Exponentials of the form X^{Y} where X is compact Hausdorff and Y is open discrete. The embedding. Suppose C has stable unions of open subsets, so we may define its open cover

(Grothendieck) topology and the topos E. The Yoneda embedding C → E preserves any limits which exist, and unions of opens.

Show that the representable Σ is complete in the internal logic of E. Let I be a sheaf (diagram shape). Calculate the sheaf Σ^{I}. At X it is the set of natural transformations I(−) → C(−×X, Σ). Form the join pointwise (using unions of opens in C); show that it’s natural.

Now we have Alg ↪ Frm(E). Why does the embedding preserve Σ^{(−)}? It preserves exponentials, so we have to show that

the sheaf Σ^{A} is the Scott topology on A, i.e. it consists of upper sets and all functions are Scottcontinuous. For the first part use the Phoa principle.

Then by following the earlier constructions, the embedding also preserves ⊗ and other things.

Remark G.1 Domain theory agenda (from undated red handwritten notes).

• Various natural numbers objects.

• Fixed point property: Freyd, Plotkin, Scott, ... axioms.

• Topological enumerability.

• Untyped λ-calculus.

• Type of types.

• Solving domain equations.

• Cartesian closed subcategories.

• Powerdomains.

• Interpretation of PCF and while, using the ASD compiler. Read Abramsky’s Domain Theory in Logical Form.

Remark G.2 Computational interpretation (from undated red handwritten notes). • Any definable global element of an open discrete space in \overline{C} translates into a terminating PROLOG program that outputs a number that represents the term.

• Every morphism ℕ → ℕ_{⊥} defines a partial recursive function.

• Also PROLOG to ASD.

• Any ℕ → ℕ in C is primitive recursive, by separation of variables.

Remark G.3 Domain theory using Abstract Stone Duality (from notes in pencil dated 18 June 1999).

1. Domain-theoretic calculations using primitive recursion and openness of ℕ (∃_{ℕ}) but not a Scott–Freyd axiom. Construct lazy and rising ℕ with and without ⊤, show that these are initial algebras or final coalgebras. Also ℕ_{⊥}, (2_{⊥})^{ℕ}, (ℕ_{⊥})^{ℕ} with general recursion. Isolate the Scott–Freyd axiom.

2. Gluing to Set to show that the global sections of the free such model are exactly general recursive functions on ℕ.

3. Gluing (or other inductive argument) to Dcpo (?) to show that the Scott–Freyd axiom is true in the free model (Rice–Shapiro–Myhill–Shepherdson).

4. Topological enumeration (ℕ → Σ^{ℕ} Σ-epi) from the Scott–Freyd axiom. All objects in minimal model have Σ-split monos to Σ^{ℕ} (Scott).

5. Initial algebras and final coalgebras for functors, defined internally using the “universal” object Σ^{ℕ}. Freyd axiom.

6. Free algebras for finitary generalised algebraic theories using open discrete objects (maybe don’t need Scott–Freyd).

7. Free internal model inside the free (external) model. Glue the internal and external. Universal Turing–Kleene machine. Recursive enumeration.

8. Characterise using PERs? Do 4–6 using synthetic domain theory.

8

[figure]

7

[figure]

6

5

2  3  4
[figure]

1