Computably Based Locally Compact Spaces

Paul Taylor

June 29, 2004

Abstract Abstract Stone Duality is a re-axiomatisation of general topology in which the topology on a space is treated as an exponential object of the same category, with a λ-calculus, rather than as an infinitary lattice. In this paper, this is shown to be equivalent to a notion of computable basis for locally compact sober spaces or locales, involving a family of open subspaces and accompanying family of compact ones. This generalises Smyth’s effectively given domains and Jung’s Strong proximity lattices. Part of the data for a basis is the inclusion relation of compact subspaces within open ones, which is formulated in locale theory as the way-below relation ≪ on a continuous lattice. The finitary properties of this relation are characterised here, including the Wilker condition for the inclusion of a compact space in two open ones. The real line is used as a running example, being closely related to Scott’s domain of intervals. ASD does not use the category of sets, but the full subcategory of overt discrete objects plays this role; it is a pretopos with lists and general recursion. In particular it is the intermediary between the objects of the new category and computable bases for classical spaces.

1 Introduction

A locally compact space is one in which there is a good interaction of open and compact subspaces. The traditional definition was generalised from Hausdorff to sober spaces in [8, p. 211]:

Definition 1.1 Whenever a point is contained in an open subspace (x ∈ V), there is a compact subspace K and an open one U such that x ∈ U ⊂ K ⊂ V.

It is an easy exercise in the “finite open sub-cover” definition of compactness to replace the point x by another compact subspace:

Lemma 1.2 Let L ⊂ V ⊂ X be compact and open subspaces of a locally compact space. Then there are

L ⊂ U ⊂ K ⊂ V ⊂ X

with U open and K compact. □

We call this result the interpolation property. Alternating inclusions of open and compact subspaces like this will be very common.

Notation 1.3 We write U ≺ ≺ V and K ≺ ≺ L if there is such an interpolating compact or open subspace, respectively. The second version, in which K ⊃ L, follows the usage of [8, 15], cf. Theorem 3.17.

Now consider what we might mean by a computably defined locally compact space.

Suppose that you have some computational representation of a space. It can only encode some of the points and open and compact subspaces, since in classical topology there are uncountably many in any interesting case. Hence your “space” cannot be literally sober, or have arbitrary unions of open subspaces. We understand the intended space to be the corresponding sober one, in which arbitrary unions of opens have also been adjoined. Those open and compact subspaces that have codes are called basic.

Example 1.4 A computable definition of ℝ as a locally compact space might have

(a) as points, (encodings of) the rationals;

(b) as basic open subspaces, the (names of) open intervals (q ±ϵ) ≡ (q −ϵ, q +ϵ) ≡ {x | |x − q| < ϵ} with rational or infinite endpoints; and

(c) as basic compact subspaces, the closed intervals [q ± δ] ≡ [q − δ, q + δ] ≡ {x | |x − q| ≤ δ} with finite rational endpoints.

Notice that both open and closed intervals are used, though treatments of exact real arithmetic often just use one or the other, cf. Example 5.9. Also, by “rationals” we might actually mean all pairs \frac{p}{q} with integers p and q ≠ 0, or the dyadic rationals p/2^{n}, or continued fractions, or whatever our favourite countable dense set of reals may be. Unlike Dedekind cuts, this example readily generalises: for ℝ^{3} we use open and closed cuboids whose vertices have rational co-ordinates (or, better, a system based on close packing of spheres [2]).

In the Example, the intersection of two basic opens is again basic, but for technical reasons we shall need to extend the families to include finite unions of open (respectively, compact) intervals or cuboids. It’s an exercise that’s a little too complicated to be called algebra, but easy programming, to test inclusion and compute the representations of such unions and intersections.

Definition 1.5 A computably based locally compact space consists of a set of codes for “points”, basic “open” and “compact” subspaces, together with an interpretation of these codes in a locally compact sober space. We require of the space that every open subspace be a union of basic ones. We also want to be able to compute

(a) codes (that we shall just call 0 and 1) for the empty set and the entire space, considered as open and compact subspaces (if, that is, the entire space is in fact compact);

(b) codes for the union and intersection of two open subspaces, and for the union of two compact ones, given their codes (we write + and ⋆ instead of ∪ and ∩ for these binary operations, to emphasise that they act on codes, rather than on the subspaces that the codes name);

(c) whether a particular representable point belongs to a particular basic open subspace, given their codes; but we only need a positive answer to this question if it has one, as failure of the property is indicated by non-termination;

(d) more generally, whether an open subspace includes a compact one, given their codes;

(e) codes for U and K such that L ⊂ U ⊂ K ⊂ V, given codes for L ⊂ V as above.

(f) In fact, we shall require the basic compact and open subspaces to come in pairs, with U^{n} ⊂ K^{n}, where the superscript n names the pair, and we also need part (e) to yield such a pair as the interpolant.

Extensional equivalence of computable functions is not captured within the strength of the logic that we wish to study. So, for the “computations” above, we mean a particular program to be specified — at least up to provable equivalence, which means that we don’t have to nominate a programming language.

Definition 1.6 A computably continuous function between such spaces is a continuous function f : X → Y between the topological spaces themselves, for which the binary relation

fK^{m} ⊂ U^{n}

between the codes (n, m) for a compact subspace K^{m} ⊂ X and an open one U^{n} ⊂ Y is recursively enumerable, cf. part (c) of the previous definition.

In particular, computably equivalent bases for the same space are those for which the identities in both directions are computably continuous functions. This means that the relations K^{n} ⊂ U^{m} and K^{m} ⊂ U^{n} between n and m are recursively enumerable. For example, whilst there are several choices for the “rationals” and intervals in Example 1.4, all of the reasonable ones are computably equivalent.

Remark 1.7 It is out of place in the definition of something computable to specify a topological space: this was only included to guarantee topological consistency of the computations of union, intersection, containment and interpolation. In Section 8 we shall formulate this consistency in terms of finitary conditions on the transformations of encodings themselves.

Then in Section 10 we shall show that any such encoding (such as the one for ℝ above) that satisfies these consistency requirements defines a locally compact sober space, which is unique up to homeomorphism. Moreover this construction is done, not in traditional topology itself, which is not computable, but in a λ-calculus.

On the other hand, the practical situation is illustrated by Example 1.4: we have a classical definition of a topological space equipped with a conventional basis, which we want to use to obtain values in the space. So long as the above features of the basis are computable, the classical space guarantees the consistency conditions. In other words, the construction imports the classical data into the computational world (Section 12).

Remark 1.8 The operations ⋆ and + become ∩ and ∪ when we interpret them via the basic open subspaces that they encode. Amongst the abstract consistency requirements, therefore, we would expect (0, 1, +, ⋆) to define a distributive lattice.

However, we have only asked for the ability to test inclusion of a compact subspace in an open one, not inclusion or equality of two open or two compact subspaces, nor of an open subspace in a compact one. Even if these happen to be possible, it is computationally quite reasonable for different codes to denote the same subspace, but for this fact to be potentially undecidable.

On the other hand, as we want to stress the computable aspect of the names of basic subspaces, we shall often represent + and ⋆ as concatenations of lists. This clumsiness actually serves an expository purpose, keeping this “imposed” structure on codes separate in our minds from the “intrinsic” structure in the topology on X, which we shall regard as another space. If we used the notation and equations of a distributive lattice for the set N of codes, it would be all too easy to lapse into confusing it with the actual topology on the space. This would in fact make logical assumptions that amount to a solution of the Halting Problem (or worse).

The topological information is actually contained, not in the quasi-lattice structure (0, 1, +, ⋆) on N, but in the inclusion relation between compact and open subspaces. This satisfies some easily verified properties:

Lemma 1.9 ∅ ⊂ V,

{K ⊂ L ⊂ U ⊂ V \atop K ⊂ V}  {K ⊂ V  L ⊂ V \atop K ∪ L ⊂ V}  {K ⊂ U  K ⊂ V \atop K ⊂ U ∩ V}  □

Finally, there is a property similar to Lemma 1.2 that concerns binary unions. Easy enough to prove though this property may be — when you see it — it is not something whose significance one would identify in advance. Various forms of it were originally studied by Peter Wilker [24].

Lemma 1.10 Let K be a compact subspace covered by two open subspaces of a locally compact sober space X, that is, K ⊂ U ∪ V. Then there are compact subspaces L and M and open ones U′ and V′ such that

K ⊂ U′ ∪ V′ U′ ⊂ L ⊂ U and V′ ⊂ M ⊂ V.

Proof Classically, K \ V is a closed subspace of a compact space, and is therefore compact too, whilst K \ V ⊂ U, so by the interpolation property (Lemma 1.2) we have

K \ V ⊂ U′ ⊂ L ⊂ U ⊂ X

for some U′ open and L compact. Then K \ U′ ⊂ K \ (K \ V) ⊂ V so

K \ U′ ⊂ V′ ⊂ M ⊂ V ⊂ X

for some V′ open and M compact. Finally, K = (K ∩ U′) ∪ (K \ U′) ⊂ U′ ∪ V′. □

We didn’t mention the intersection of two compact subspaces in Definition 1.5, because there are spaces in which this need not be compact.

Definition 1.11 A locally compact sober space is called stably locally compact if the whole space is compact and the intersection of any two compact subspaces is again compact.

Examples 1.12

(a) Let x, y ∈ X in an overt discrete space. Then the intersection {x} ∩ {y} ⊂ X is open and so overt; by Corollary 8.15 it is also compact only if it is either empty or inhabited, i.e. x = y is decidable. So X is stably locally compact iff it is Hausdorff.

(b) A combinatory algebra has constants k and s and a binary operation · such that (k·x)·y = x and (((s · x) · y) · z) = (x · z) · (y · z). The free such algebra is overt discrete because terms can be proved equal using these rules, but proving inequality in A is like solving the Halting problem. So A is neither Hausdorff nor stably locally compact.

(c) Consider two copies of the real unit interval [0, 1] identified on their interiors (or, if you prefer, an interval with duplicated endpoints). Then the two copies of the interval are compact subspaces whose intersection is not compact [9, 11]. □

Points disappeared from the discussion right at the beginning, and we saw in Example 1.4 that it is easier to specify ℝ with the Euclidean topology using open and compact subspaces than using open subspaces and points. Arguably this would be the best way in which to formulate topology — just as lines and circles were entities in themselves in traditional geometry, rather than sets of points.

Locale theory reduces the description further, to one involving open subspaces alone. To do this for locally compact spaces, we must characterise the situation (U ≺ ≺ V) ≡ ∃K. (U ⊂ K ⊂ V).

Definition 1.13 Let L be a complete lattice.

(a) A family (ψ_{s}) ⊂ L is called directed^{1} if it is inhabited, and whenever ψ_{r} and ψ_{s} belong to the family, there is some ψ_{t} ≥ ψ_{r}, ψ_{s}. The join of the family is written ⋁ ; ψ_{s}.

(b) Now, for β, ϕ ∈ L, we write β ≪ ϕ (way-below) if, whenever ϕ ≤ ⋁ ; _{s} ψ_{s}, there is already some s for which β ≤ ψ_{s}. (So β ≪ ϕ implies β ≤ ϕ.)

(c) Then L is a continuous lattice [5] if, for all ϕ ∈ L, ϕ = ⋁ ; {β | β ≪ ϕ}.

Proposition 1.14 The topology of any locally compact space is a distributive continuous lattice, in which U ≺ ≺ V iff U ≪ V [8, p. 212]. Proof U ≺ ≺ V implies U ≪ V by compactness of K with U ⊂ K ⊂ V, and

V = ⋃ {W | W ≺ ≺ V }

by Definition 1.1. This union is directed by Lemma 1.9, so it may be used in the definition of U ≪ V, giving U ⊂ W ≺ ≺ V for some W, but then U ≺ ≺ V too. Hence U ≪ V iff U ≺ ≺ V, but notice that the proof does not supply the interpolating compact subspace U ⊂ K ⊂ V. □

Conversely, every distributive continuous lattice is the lattice of open subspaces of some locally compact sober space. However, this result relies on the axiom of choice, and is even then not a trivial matter to prove [7]..

Definition 1.5 for spaces has a simpler analogue for locales, since it’s all lattice theory.

Definition 1.15 A computable basis (N, 0, 1, +, ⋆, ≺ ≺) for a continuous distributive lattice L is a set N with constants 0, 1 ∈ N, computable binary operations +, ⋆ : N × N → N, a recursively enumerable binary relation ≺ ≺ and an interpretation β^{(−)} : N → L that takes (0, 1, +, ⋆) to the lattice structure in L, such that n ≺ ≺ m iff β^{n} ≪ β^{m} and

for all ϕ ∈ L, ϕ = ⋁ ; {β^{n} | β^{n} ≪ ϕ}.

If L_{1} and L_{2} have bases (β^{m}) and γ^{n} then H : L_{2} → L_{1} is a computable frame homomorphism if H preserves ⊤, ∧ and ⋁ and the relation (β^{m} ≪ Hγ^{n}) is recursively enumerable.

1The letter s stands for semilattice, but see Definition 2.21.

Bases were defined for continuous lattices in [5, Definition III 4.1], whilst this notion of effective or computational basis follows that of Michael Smyth in domain theory [19].

Once again we seek to remove the locale or continuous lattice from the definition, this time with the goal of eliminating the infinitary joins in favour of finitary properties of the way below relation. Of course, since ≪ was itself defined using directed joins, it will have to be replaced by an abstract relation ≺ ≺ satisfying axioms based on the following properties, which are the analogues of Lemmas 1.2, 1.9 and 1.10.

Lemma 1.16 If β′ ≤ β ≪ ϕ ≤ ϕ′ then β′ ≪ ϕ′. □

Lemma 1.17 The relation ≪ is transitive and interpolative: if α ≪ β ≪ γ then α ≪ γ, and conversely given α ≪ γ, there is some β with α ≪ β ≪ γ. □

Lemma 1.18 ⊥ ≪ ϕ, and if α ≪ ϕ and β ≪ ϕ then (α ∨ β) ≪ ϕ. Proof This uses the two clauses in the definition of the directed join ⋁ ; ψ_{s} in Definition 1.13(a).

□

The Wilker property in Lemma 1.10 used excluded middle, but its analogue for continuous lattices is both intuitionistic and very simple: it follows from the observation that binary joins distribute over joins of inhabited, and in particular directed, families.

Lemma 1.19 In any continuous lattice, if α ≪ β ∨ γ then α ≪ β′ ∨ γ′ for some β′ ≪ β and γ′ ≪ γ. Proof Since any directed set is inhabited,

β ∨ γ = ⋁ ; {β′ ∨ γ | β′ ≪ β} = ⋁ ; {β′ ∨ γ′ | β′ ≪ β, γ′ ≪ γ}.

Then if α ≪ β ∨ γ, we have α ≪ β′ ∨ γ′ for some term in this join. □ The relationship between ≪ and ∧ is more subtle.

Lemma 1.20 If α ≪ β ≪ ϕ and β ≪ ψ then α ≪ ϕ ∧ ψ. Proof Since β ≪ ϕ implies β ≤ ϕ, we have α ≪ β ≤ ϕ ∧ ψ, and so α ≪ ϕ ∧ ψ. □

Definition 1.21 A stably locally compact locale is one in which ⊤ ≪ ⊤, and if α ≪ ϕ and α ≪ ψ then α ≪ ϕ ∧ ψ.

Examples 1.12 can easily be adapted to yield locally compact locales that are not stably locally compact, and therefore only obey the weaker rule in the Lemma.

Remark 1.22 Stably locally compact sober spaces enjoy many superior properties, illustrating the duality between compact and open subspaces. Jung and Sünderhauf [15] set out “consistency conditions” for them that are similar to ours, except that they choose to make (0, 1, +, ⋆) a genuine (“strong proximity”) lattice.

However, not all of the locally compact spaces that we wish to consider are stably so, either in geometric topology or recursion theory. Most obviously for the former, in ℝ, the whole space (the trivial intersection) is not compact. In the latter, we also want to consider discrete spaces whose equality is not decidable such as Example 1.12(b).

Another reason why we consider the more general situation is that it corresponds to the monadic Axiom 2.3(c) that was the fundamental idea behind the research programme of which this paper is a part. This correspondence, which has no counterpart in [15], is the main technical goal of this paper.

We shall see at the end of Section 4 that the non-stable situation also highlights an interesting difference (separate from the usually mentioned ones of constructivity) between locales and sober spaces as ways of presenting topological information.

Applying G.H. Hardy’s test [6], we may wonder which of the stable and non-stable theories is “beautiful” and which is “ugly”. My suspicion is that stably locally compact spaces and the “relational” morphisms that they describe ([14] and Theorem 7.11) play another role in the bigger picture, whilst we are right to study “functional” morphisms in the non-stable case.

The logic that we use is a very weak computational one, but on closer examination, we see that a great deal of the work that has been done in domain theory, using many notions of “basis” or “information system” could actually be formulated in such a logic.

2 Axioms for abstract Stone duality

In this paper we develop a computable account of locally compact sober spaces and locales, but using a λ-calculus in place of the usual infinitary lattice theory, which conflicts with computable ideas. This calculus, called Abstract Stone Duality, exploits the fact that, for any such space X, its lattice of open subspaces provides the exponential Σ^{X} in the category. Here Σ is the Sierpiński space (which, classically, has one open and one closed point), and the lattice Σ^{X} is equipped with the Scott topology. Its relationship to the “consistency conditions” in the previous section and in [15] will be examined in Sections 8–11.

Remark 2.1 We are primarily interested in two particular models of the calculus:

(a) as a source of topological intuition, the classical ones, namely the categories of locally compact sober spaces (LKSp) and of locally compact locales (LKLoc);

(b) for computation, the term model.

The classical side has a wealth of concepts motivated by geometry and analysis, but its traditional foundations are logically very strong, being able to define many functions that are neither continuous nor computable, besides many other famous pathologies. Having created such a wild theory, we have to rein it back in again, with a double bridle. The topological bridle is constructed with infinitary lattice theory, whilst logically we are reduced to using Gödel numberings of manipulations of codes for basic elements [19]. Abstract Stone duality avoids all of this by only introducing computably continuous functions in the first place, although we pay a logical price in not being able to define objects and functions anything like so readily as in set theory.

On the other hand, logically motivated discussions read the foundational aspects more literally than their topological authors ever intended. They are so bound up in their own questions of what constitutes “constructivity” that they lose sight of the conceptual structure. To give an example in another discipline, the mathematician in hot pursuit of a proof typically postulates a least counterexample, in order to rule it out. It is impertinent of the logician to emphasise that this uses excluded middle, as proofs of this kind (once found) can very often be recast in terms of the induction scheme [21, Section 2.5]. As a result, foundational work often fails to reach “ground level” in the intended construction.

The lesson we draw from this is that logic and topology readily drift apart, if ever we let go of either of them. So we have to tell their stories in parallel. This means that we must often make do with rough-and-ready versions of parts of one, in order to make progress with the other. For example, we use concepts such as compactness to motivate our λ-calculus, which itself underlies the technical machinery that eventually justifies the correspondence with traditional topology and the use of its language. We shall make a point of explaining how each step (Definition, Lemma, etc.) of the new argument corresponds to some idea in traditional topology.

In this section we have to set up some logical structure that the topologically minded reader may prefer to skip at first. We catch up on some of the justifications in Section 7. In this section too we interleave the axioms and definitions of the λ-calculus with the technical issues that they are intended to handle.

Remark 2.2 Recall first the universal properties of the Sierpiński space, Σ. Any open subspace U ⊂ X is classified by a continuous function ϕ : X → Σ, in the sense that U = ϕ^{−1}(⊤), where ⊤ is the open point of Σ, and ϕ is unique with this property. This is summed up by the pullback diagram

[figure: U; 1; X; ∩; ϕ; Σ; ⊤]

In our calculus, we shall use the λ-term ϕ : Σ^{X} instead of the subset U ⊂ X. A similar diagram, using the closed point ⊥ ∈ Σ instead of ⊤, classifies (or, as we shall say, co-classifies) the closed subspace, that, classically, is complementary to U. We follow topology rather than logic in retaining the bijection between open and closed subspaces, even though they are not actually complementary in the sense of constructive set theory. This is because it is not sets but topological spaces that we wish to capture.

Unions and intersections of open and closed subspaces make the topology Σ^{X}, and in particular the object Σ, into distributive lattices — honest ones now, not consisting of codes as in Remark 1.8. We therefore have to axiomatise the exponential and the lattice structure.

Axiom 2.3 The category S of “spaces” has finite products and an object Σ of which all exponentials Σ^{X} exist. Then the adjunction Σ^{(−)} ⊣ Σ^{(−)} that relates S^{op} to S is to be monadic. This categorical statement has an associated symbolic form, consisting of

(a) the simply typed λ-calculus, except that we may only introduce types of the form Σ^{X×Y ×···} (or X → Y → ⋯ → Σ if you prefer), and therefore λ-abstractions whose bodies already have such types;

(b) an additional term-forming operation, focus, which may only be applied to a term P of type Σ^{Σ^{X}} that satisfies a certain primality equation capturing the situation P = λϕ. ϕa, and then focus P = a; the use of focus makes the space X sober [A];

(c) and an additional type-forming operation (with associated term calculus) that provides certain pullbacks and equalisers, namely those whose data satisfy another λ-equation, and these subspaces carry the subspace topology [B].

The equations required in parts (b) and (c) will be stated in Definitions 7.13 and 7.17, where we replace them by finitary lattice equations in the new calculus that are similar to the infinitary ones in traditional topology.

Axiom 2.4 (Σ, ⊤, ⊥, ∧, ∨) is an internal distributive lattice in S, which, moreover, satisfies the Phoa principle,

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

This equation (which is bracketable either way) is used to ensure that terms of type Σ^{X} yield data for the open or closed subspace of X, as required by the monadic axiom [C, Sections 2–3], and hence the pullback in Remark 2.2. It thereby enforces the bijective correspondences amongst open and closed subspaces and terms of type Σ^{X}. We shall assert an “infinitary” generalisation of the Phoa principle shortly.

Definition 2.5 The lattice structure on Σ and Σ^{X} defines an intrinsic order, ≤, where ϕ ≤ ψ ⟺ ϕ = ϕ ∧ ψ ⟺ ϕ ∨ ψ = ψ. This is inherited by other objects:

Γ ⊢ a ≤ b : X if Γ ⊢ (λϕ:Σ^{X} . ϕa) ≤ (λϕ. ϕb) : Σ^{Σ^{X}} .

There are other ways of defining an order, but sobriety and the Phoa principle make them equivalent, and also say that all maps are monotone [C, Section 5].

In LKLoc this order on hom-sets arises from the order on the objects, considered as lattices, whilst in LKSp it is the specialisation order,

x ≤ y ≡ (∀U ⊂ X open. x ∈ U ⇒ y ∈ U) ≡ x ∈ \overline{\{y\}},

where \overline{\{y\}} is the smallest closed subspace containing y.

Lemma 2.6 Let i : U ^{⊂} X and j : C ^{⊏} X be the open and closed subspaces (co)classified by ϕ : Σ^{X}. Then, with respect to the intrinsic orders on Σ and Σ^{X}, there are adjoints

∃_{i} ⊣ Σ^{i} and Σ^{j} ⊣ ∀_{j}

that behave like quantifiers [C, Section 3]. □

Remark 2.7 The order presents an important problem for the axiomatisation of the join in Definition 1.13(c),

ϕ = ⋁ ; {β | β ≪ ϕ}.

The predicate on the right of the “|” is monotone in ϕ (indeed, Remark 3.11 will use the fact that it is Scott-continuous), but contravariant with respect to β:

(β′ ≤ β) ⟹ ((β′ ≪ ϕ) ⇐ (β ≪ ϕ)).

We want to regard the topology Σ^{X} as another space, but the subset {β | β ≪ ϕ} is not a sober subspace (in the Scott topology), since it isn’t closed under ⋁ ; .

Remark 2.8 This means that we have, after all, to make a distinction between the exponential space Σ^{X} and the set (albeit structured) of open subspaces of X. We shall write |Σ^{X} | for the latter, since it is the set of points of the space Σ^{X}.

Although locale theory plays down the underlying set functor |−| : Loc → Set, since it is not faithful, this functor nevertheless exists. It may be characterised as the right adjoint to the inclusion Set → Loc that equips any set with its discrete topology, i.e. the powerset considered as a frame. In fact, this right adjoint is precisely what we have to add to the computably motivated axioms of abstract Stone duality given in this paper, in order to make them agree with the “official” theory of locally compact locales over an elementary topos [G] (which writes ΩX or UΣ^{X} for |Σ^{X} |). In other words, it distinguishes between the two leading models in Remark 2.1.

This adjunction says that there is a map ε : |Σ^{X} | → Σ^{X} that is couniversal amongst maps β : N → Σ^{X} from the objects N of a certain full subcategory, so β factors uniquely as N → |Σ^{X} | → Σ^{X}. However, the couniversal object |Σ^{X} | cannot exist in the computable theory: besides being uncountable, its equality test would solve the Halting Problem. So we have to develop alternatives to it. In traditional language, all we need is that any ϕ ∈ Σ^{X} be expressible as a directed join of β^{n}s, as in Definition 1.15.

Returning to the problem of Definition 1.13(c), we must use codes for (basic) open sets, since we cannot define ≪ in abstract Stone duality using the open set β : Σ^{X} itself. Thus Remark 4.12 will replace the formula β ≪ ϕ (with variables β and ϕ) by

n : N, ϕ : Σ^{X} ⊢ (β^{n} ≪ ϕ) : Σ,

where β^{n} is the basic open subspace with code n.

Objects like this N are playing the role taken by sets in traditional topology or locale theory, in particular to index infinitary joins and computable bases in Definitions 1.5 and 1.13(c). However, since we have no sets as such, we think of these objects as “discrete” spaces. In abstract Stone duality we take this particular word to mean that there is an internal notion of equality, but the logical structure that we need to express the join is existential quantification.

Definition 2.9 An object N ∈ obS is discrete if there is a pullback

[figure: N; 1; N × N; Δ; ∩; (=_{N}); Σ; ⊤]

i.e. the diagonal N ↪ N × N is open. We may express this symbolically by the rule

for Γ ⊢ n, m : N,  Γ ⊢ n = m : N ; = ; Γ ⊢ (n =_{N} m) = ⊤ : Σ

The (=) above the line denotes externally provable equality of terms of type N, whilst (=_{N}) below the line is the new internal structure. Categorically, (n, m) : Γ → N × N and ! : Γ → 1 provide a cone for the pullback iff (n =_{N} m) = ⊤, and in just this case (n, m) factors through Δ, i.e. n = m as morphisms.

We also write {n} for λm. (n =_{N} m) : Σ^{N}.

Beware that this notion of discreteness says that the diagonal and singletons are open, but not necessarily that all subspaces of N are open. For example, the Gödel numbers for non-terminating programs form a closed but not open subspace of ℕ [D, H], because the classically continuous map ℕ → Σ that classifies it is not computable (Definition 1.6).

Definition 2.10 Similarly, an object H is Hausdorff if H ^{⊏} H ×H is closed, i.e. co-classified by (≠_{H}) : H × H → Σ, so

for Γ ⊢ a, b : H,  Γ ⊢ a = b : H ; = ; Γ ⊢ (a ≠_{H} b) = ⊥ : Σ.

Notice that equality of the terms a, b : H corresponds to a sort of doubly negated internal equality, so this definition carries the scent of excluded middle. Like that of a closed subspace, it was chosen on the basis of topological rather than logical intuition. Beware again that discrete spaces need not be Hausdorff.

Definition 2.11 An object N ∈ obS is overt if Σ^{!_{N}} has a left adjoint, ∃_{N} : Σ^{N} → Σ, with respect to the intrinsic order (Definition 2.5). Then

for Γ ⊢ σ : Σ, ϕ : Σ^{N},  Γ, x : N ⊢ ϕx ≤ σ : Σ ; = ; Γ ⊢ ∃x. ϕx ≤ σ : Σ

where we write ∃x:N . ϕx or just ∃x. ϕx for ∃_{N}(λx:N . ϕx). The Frobenius law,

σ ∧ ∃x. ϕx = ∃x. σ ∧ ϕx

may be derived from the Phoa principle (Axiom 2.4), and Beck–Chevalley is also automatic [C, Section 8]. The lattice dual of this definition is the subject of the next section.

Axiom 2.12 S has a natural numbers object ℕ, i.e. a type that admits primitive recursion and equational induction [E] at all types, and so is discrete. Moreover we require ℕ to be overt.

Sobriety of ℕ provides general recursion, whilst terms can be translated into PROLOG programs [A, Section 11]. The free model of the calculus therefore satisfies the Church–Turing thesis, so we do not need to introduce Kleene-style notation with Gödel numbers in order to justify calling it a computable account of topology. In particular, the computations referred to in Definitions 1.5, 1.6 and 1.15 may be defined by terms of our calculus.

Remark 2.13 Since the object N over which the codes range is discrete, its intrinsic order ≤ is trivial [C, Lemma 6.2]. However, the structure (N, 0, 1, +, ⋆) of an abstract basis is, at least morally, that of a distributive lattice (Remark 1.8). But this is an “imposed” structure, i.e. one that is only defined by the explicit specification of (0, 1, +, ⋆), rather than by its relationship to the other objects in the category. We are completely at liberty to consider functions that preserve, reverse or disregard the associated imposed order relation ≼ that may be defined from + and ⋆ (Definition 9.10). Indeed, the need to make A_{n} contravariant in n was precisely the reason for distinguishing between N (or |Σ^{X} |) and Σ^{X} in Remark 2.7.

We typically use the letter N for an overt discrete object, as its topological properties are like those of the natural numbers (ℕ), though the foregoing remarks do not give it either arithmetical or recursive structure. So when we write (β^{n}) for the basis of open subspaces, we intend a family, not a sequence. The use of the letter N is merely a convention, like K for compact spaces; the letter I (for indexing set) is often used elsewhere in the situations where we use N below, but it has acquired another conventional use in abstract Stone duality (cf. Lemma 5.2).

Theorem 2.14 The full subcategory of overt discrete spaces is a pretopos, i.e. we may form products, equalisers and stable disjoint unions of them, as well as quotients by open equivalence relations [C, Section 11]. If the “underlying set” functor in Remark 2.8 exists, as in the classical models LKSp and LKLoc, then the overt discrete spaces form an elementary topos [G]. □

The combinatorial structures of most importance in this paper, however, are the following:

Theorem 2.15 Assuming a “linear fixed point” axiom (that any F : Σ^{U} → Σ^{V} preserves joins of ascending sequences), every overt discrete object N generates a free semilattice KN and a free monoid ListN in S, which satisfy primitive recursion and equational induction schemes, and are again overt discrete objects [E]. □

This result is easy to see in the two cases of primary interest, namely the classical and term models (Remark 2.1). In the classical ones (LKSp and LKLoc), overt discrete spaces are just sets with the discrete topology, and form a topos. In this case the general construction of List(−) and K(−) is well known — KN is often called the finite powerset. The notation and narrative may give the impression of countability, but bases may be indexed by any set, however large you please. Nevertheless, I make no apology for this impression, as I consider ℵ_{1} and the like to have no place in topology. I also suspect that occurrences of “sequences” and “countable sense subsets” in the subject betray the influence of objects whose significant property is overtness and not recursion.

Remark 2.16 In the term model, on the other hand, we shall find in Section 6 that ℕ itself is adequate to index the bases of all definable types. Moreover, any definable overt discrete space N is in fact the subquotient of ℕ by a some open partial equivalence relation (Corollary 7.2). This both allows us to construct List(N) and K(N), and also to extend any N-indexed basis to an ℕ-indexed one. There is, therefore, no loss of generality in taking all bases in this model to be indexed by ℕ, if only as a method of “bootstrapping” the theory.

To construct List(ℕ), we could use encodings of pairs, lists and finite sets of numbers as numbers. However, it is much neater to replace ℕ with the set 𝕋 of binary trees. Like ℕ, 𝕋 has one constant (0) and one operation, but the latter is binary (pairing) instead of unary (successor), and the primitive recursion scheme is modified accordingly. Hence 𝕋 ≅ {0} + 𝕋 × 𝕋 ≅ List(𝕋), whereas ℕ ≅ {0} + ℕ. The encoding of lists in 𝕋 has been well known to declarative programmers since Lisp: 0 denotes the empty list, and the “cons” h :: t is a pair.

Membership of a list is easily defined by list recursion, as are existential and universal quantification, i.e. finite disjunction and conjunction.

\begin{aligned}(λm. m ∈ 0)n & ≡ & ⊥ & (λm. m ∈ h :: t)n & ≡ & (h = n) ∨ (λm. m ∈ t)n \\ ∀m ∈ 0. ϕm & ≡ & ⊤ & ∀m ∈ h. ϕm & ≡ & ϕh ∧ ∀m ∈ t. ϕm \\ ∃m ∈ 0. ϕm & ≡ & ⊥ & ∃m ∈ h. ϕm & ≡ & ϕh ∨ ∃m ∈ t. ϕm \end{aligned}

Notation 2.17 The notation that we actually use in this paper conceals the preceding discussion. The letter N may just stand for 𝕋 in the term model, but may denote any overt discrete space. So in the classical models N is a set, or an object of the base topos, equipped with the discrete topology.

We use Fin(N) to mean K(N) or List(N) ambiguously. Since they are respectively the free monoids on N with and without the commutative and idempotent laws, this is legitimate so long as their interpretation also obeys these laws. But this is easy, as the interpretation is usually in Σ^{X}, with either ∧ or ∨ for the associative operation. In fact, these two interpretations in Σ^{Σ^{N}} are jointly faithful [E].

We are now ready to state the central assumption of this paper.

Axiom 2.18 The Scott principle: for any overt discrete object N,

F : Σ^{Σ^{N}} , ϕ : Σ^{N} ⊢ F ϕ = ∃ℓ:Fin(N). F (λn. n ∈ ℓ) ∧ ∀n ∈ ℓ. ϕn.

Notice that the Phoa principle (Axiom 2.4) is the special case with N = 1 and so K(N) = {0, 1}, whilst the “linear fixed point” axiom in Theorem 2.15 is equivalent to the case N = ℕ. More generally, the significance of this axiom is that it forces every object to have and every map to preserve directed joins (which we have to define), and so captures the important properties that are characteristic of topology and domain theory.

Remark 2.19 The lattice Σ^{X} has intrinsic M-indexed joins, for any overt discrete object M. These are given by λx. ∃m:M . ϕ^{m}x, and are preserved by any Σ^{f} [C, Corollary 8.4].

In speaking of such “infinitary” joins in Σ^{X}, we are making no additional assertion about lattice completeness: there are as many joins in each Σ^{X} as there are overt objects, no more, no fewer. In particular, there are not “enough” to justify impredicative definitions such as the interior of a subspace, or Heyting implication, though these can be made in the context of the “underlying set” assumption in Remark 2.8 [G]. Moreover, we use the symbol ∃ to emphasise that our joins are internal to our category S, whereas those in locale theory (written ⋁) are external to LKLoc, involving the topos (Set) over which it is defined. This distinction will, unfortunately, become a little blurred because of the need to compare the ideas of abstract Stone duality with those of traditional topology and locale theory. This happens in particular in the definition of compactness (Definition 3.1), the way-below relation (Definition 1.13(b) and Remark 4.13) and the characterisation of finite spaces (Theorem 7.10).

Remark 2.20 When we use M-indexed joins, we shall need M to be a dependent type, given, in traditional comprehension notation (not that of [B]), by

M ≡ {n : N | α_{n}} ⊂ N,

where α_{n} selects the subset of indices n for which ϕ^{n} : Σ^{X} is to contribute to the join. In practice, this subset is always open, so α_{n} : Σ. The sub- and super-script notation here (and in [G]) indicates that ϕ^{n} typically varies covariantly and α_{n} contravariantly with respect to an imposed order on N. Indeed there would be no point in using α_{n} to select which of the ϕs to include in the join if this had to be an upper subset, as the result would always be the greatest element, whilst it is harmless to close the subset downwards.

This means that, when using the existential quantifier, we can avoid introducing dependent types by defining

∃m:{n : N | α_{n}}. ϕ^{m} as ∃n:N . α_{n} ∧ ϕ^{n}.

In Section 4 we shall refer to terms like α_{n} of type Σ as scalars and those like ϕ^{n} of type Σ^{X} as vectors.

Definition 2.21 A pair of families

Γ, s : S ⊢ α_{s} : Σ, ϕ^{s} : Σ^{X}

indexed by an overt discrete object S is called a directed diagram, and the corresponding

∃s. α_{s} ∧ ϕ^{s}

is called a directed join (cf. Definition 1.13(a)), if

(a) α_{s} = ⊤ for some s : S that we call 0, and

(b) α_{s+t} = α_{s} ∧ α_{t} and ϕ^{s+t} ≥ ϕ^{t} ∨ ϕ^{s} for some binary operation + : S × S → S. In this, α_{s}∧α_{t} means that both ϕ^{s} and ϕ^{t} contribute to the join, so for directedness in the informal sense, we require some ϕ^{s+t} to be above them both (covariance), and also to count towards the join, for which α_{s+t} must be true.

Although the letter S stands for semilattice, in order to allow concatenation of lists to serve for + (and the empty list for 0), we do not require this operation to be commutative or idempotent (or even associative).

Remark 2.22 By the Scott principle, any Γ ⊢ F : Σ^{Σ^{X}} preserves directed joins, in the sense that

F (∃s. α_{s} ∧ ϕ^{s}) = ∃s. α_{s} ∧ F ϕ^{s}.

Notice that F is attached to the “vector” ϕ^{s} and not to the scalar α_{s}, since the join being considered is really that over the dependent subset M ≡ {s | α_{s}}.

This is proved in Theorem 7.6, so it is one of the points on which the logical proofs lag some way behind the topological intuitions. Of course, this result could have been used in place of Axiom 2.18, but I feel that I made an important point in [20] by showing how sobriety (actually the slightly weaker notion of repleteness) transmits Scott continuity from the single object Σ^{N} to the whole category.

Remark 2.23 After the separation of directed joins from finite ones (⊥, ∨), the behaviour of the latter corresponds much more closely to that of meets (⊤, ∧). So, although Scott continuity, strictly speaking, breaks the lattice duality that we enjoyed in [C, D], we shall still often be able to treat meets and joins at the same time. We sometimes use the symbol ⊙ for either of them, for example in Lemma 11.11. This means that we can try to transform arguments about open, discrete, overt, existential, ... things into their lattice duals about closed, Hausdorff, compact, universal, ... things. Such lattice dual results seem to be far more common that anyone brought up with intuitionistic logic or locale theory might expect, for example replacing ∃∧ with ∀∨ yields valid duals of the basis expansion and Scott continuity, but we must leave these to later work.

A simple example of lattice duality is the distributive or Frobenius law. In fact, this only requires that the diagram be inhabited, cf. Lemma 1.19.

Lemma 2.24 If ∃n. α_{n} = ⊤ (say, α_{0} = ⊤) then ϕ ∨ (∃n. α_{n} ∧ ψ^{n}) = ∃n. α_{n} ∧ (ϕ ∨ ψ^{n}). □

3 Compact subspaces

In the λ-calculus for abstract Stone duality that we introduced in the previous section, terms of type X and Σ^{X} denote points and open subspaces respectively of the space X. In this section, terms of type Σ^{Σ^{X}} will play the role of the compact subspaces in Section 1, although there is not a literal correspondence between them. In the following two sections we shall see how simple properties of the λ-calculus correspond to well known but more complicated constructions with locally compact spaces. What we mean to demonstrate by this discussion is that certain apparently novel formulae in our λ-calculus are really familiar idioms of topology and locale theory: the formal development within ASD really begins in Section 6.

Traditionally^{2}, a topological space K has been defined to be compact if every open cover, i.e. family {U_{s} | s ∈ S} of open subspaces such that K = ⋃_{s} U_{s}, has a finite subcover, F ⊂ S with K = ⋃_{s∈F} U_{s}. If the family is directed (Definition 1.13(a)) then F need only be a singleton, i.e. there is already some s ∈ S with K = U_{s}.

The Scott topology on the lattice |Σ^{K} | offers a simpler way of saying that K is compact. In this lattice, ⊤ denotes the whole of K, so compactness says that if we can get into the subset {⊤} ⊂ |Σ^{K} | by a directed join ⋃ ; _{s} U_{s} then some member U_{s} of the family was already there^{3}. In other words, {⊤} ⊂ Σ^{K} is an open subset in the Scott topology on the lattice.

Definition 3.1 In abstract Stone duality we say that a space K is compact if there is a pullback

[figure: 1; 1; Σ^{K}; ⊤; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; ∀_{K}; Σ; ⊤]

2In fact Bourbaki [1, I 9.3] relegated this formulation to Axiom C′′′, also calling it “the axiom of Borel–Lebesgue”.

The older intuitions from analysis involve the existence of cluster points of sequences or nets of points, or of filters of subsets.

3This is therefore an externally defined join, cf. Remark 2.19.

Using the fact that Σ classifies open subspaces (Remark 2.2), together with its finitary lattice structure (but not the Scott principle), [C, Proposition 7.10] shows that ∀_{K} exists with this property iff it is right adjoint to Σ^{!_{K}}. It is then demonstrated that this map does indeed behave like a universal quantifier in logic (the corresponding existential quantifier was given by Definition 2.11).

Lemma 3.2 If K and L are compact spaces then K + L is also compact, as is ∅.

[figure: Σ^{K+L} ≅ Σ^{K} × Σ^{L}; ∀_{K} × ∀_{K}; ⊤; \underline{Σ^{!_{K}} × Σ^{!_{L}}}; Σ × Σ; ∧; ⊤; \underline{Δ}; Σ]

Proof ∀_{K+L}(ϕ, ψ) = ∀_{K}ϕ ∧ ∀_{L}ψ and ∀_{∅} = ⊤ : Σ^{∅} ≅ 1 → Σ. □

The following result is the well known fact that the direct image of any compact subspace is compact (whereas inverse images of open subspaces are open).

Lemma 3.3 Let K be a compact space and p : K ↠ X be Σ-epi^{4}, i.e. a map for which Σ^{p} : Σ^{X} → Σ^{K} is mono. Then X is also compact, with quantifier ∀_{X} = ∀_{X} · Σ^{p}. Proof The given quantifier, Σ^{!_{K}} ⊣ ∀_{K}, satisfies the inequalities

id ≤ ∀_{K} · Σ^{p} · Σ^{!_{X}} = ∀_{K} · Σ^{!_{K}}
Σ^{p} · Σ^{!_{X}} · ∀_{K} · Σ^{p} = Σ^{!_{K}} · ∀_{K} · Σ^{p} ≤ Σ^{p},

from which we deduce Σ^{!_{X}} ⊣ ∀_{K} · Σ^{p}, since Σ^{p} is mono. □

What becomes of the quantifier ∀_{K} when K no longer stands alone but is a subspace of some other space X? We see that any compact subspace K ⊂ X defines a map A : Σ^{X} → Σ or A : Σ^{Σ^{X}} that preserves ⊤ and ∧. We shall call this a (□) modal operator, rather than a quantifier, since we have lost the ∀-elimination rule Aϕ ≤ ϕx.

Lemma 3.4 Let i : K → X be any map, with K compact. Then A = ∀_{K} · Σ^{i} : Σ^{X} → Σ preserves ⊤ and ∧. Moreover Aϕ ≡ ∀_{K}(Σ^{i}ϕ) = ⊤ iff Σ^{i}ϕ = ⊤_{K}. Proof Σ^{i} preserves the lattice operations and ∀_{K} is a right adjoint. □

Remark 3.5 In traditional language, for any open set U ⊂ X classified by ϕ : Σ^{X}, the predicate Aϕ says whether K ⊂ U. Just as ∀_{K} : Σ^{K} → Σ classifies {⊤} ⊂ Σ^{K}, the map A : Σ^{X} → Σ classifies a Scott-open family F of open subspaces of X, namely the family of neighbourhoods of K. Preservation of ∧ and ⊤ says that this family is a filter.

Notice that we have an example of the alternation K ⊂ U of compact and open subspaces that we saw in Lemma 1.2. Also, recall from Definition 1.5 that we wanted to test x ∈ U and K ⊂ U; these are expressed by the λ-applications ϕx and Aϕ respectively.

Lemma 3.6

(a) If K = ∅ then A = λϕ. ⊤, so in particular A⊥ = ⊤

(b) If K = {p} then A = λϕ. ϕp ≡ η_{X}(p), which is prime (Axiom 2.3(b)) and preserves all four lattice operations, in particular A⊥ = ⊥;

(c) If K ∪ L exists then A_{K∪L}ϕ = A_{K}ϕ ∧ A_{L}ϕ.

(d) If K ⊂ L then A_{K} ≥ A_{L}.

(e) Even when K ∩ L is compact, A_{K} ∨ A_{L} need not be its modal operator. Proof

(a) Σ^{K} = 1 and ∀_{K} = λx. ⊤, so A ≡ ∀_{K} · Σ^{i} = λx. ⊤.

4In our category, where every object is a subspace of some Σ^{Y} , Σ-epi is the same as epi. The name has been inherited from synthetic domain theory, a model of which is a topos, only some of whose objects (namely the predomains) may be so embedded.

(b) Σ^{K} = Σ, ∀_{K} = id and Σ^{i} = λϕ. ϕp.

(c) Since K +L [figure] K ∪L X, we have A_{K∪L} = A_{K+L} = A_{K} ∧A_{L} by Lemmas 3.2 and 3.3.

(d) This follows from the previous part, since K ∪ L = L.

(e) Classically, of course, K ∩ L ⊂ U does not imply (K ⊂ U ∨ L ⊂ U). For example, let K = {p} and L = {q}, where p, q ∈ X are incomparable points in the specialisation order (Definition 2.5), so K ∩ L = ∅. Then A_{K∩L}⊥ = ⊤ > ⊥ = A_{K}⊥ ∨ A_{L}⊥. □

Corollary 3.7 A_{K}⊥ = ⊤ if K is empty, ⊥ if it’s inhabited (sic). □

Remark 3.8 Classically, any compact (sub)space that satisfies A_{K}⊥ = ⊥ must contain a point, by excluded middle, but Choice is still needed to find it. In the localic formulation, it is a typical use of the maximality principle to find a prime filter containing F [9, Lemma III 1.9], so A ≤ P in our notation. □

The situation in which open and compact subspaces interact extremely well is that of a compact Hausdorff space (Definitions 2.10 and 3.1).

Lemma 3.9 Let X be a compact Hausdorff space and ϕ : Σ^{X}. Then

(x ≠ y) ∨ ϕx = (x ≠ y) ∨ ϕy
ϕx  = ∀y. (x ≠ y) ∨ ϕy
(x ≠ x)  = ⊥
(x ≠ y)  = (y ≠ x)
(x ≠ z)  ≤ (x ≠ y) ∨ (y ≠ z)

Proof These are the lattice duals of (x = y) ∧ ϕx = (x = y) ∧ ϕy, ϕx = ∃y. (x = y) ∧ ϕy, reflexivity, symmetry and transitivity in any overt discrete space, and the following proof is just the dual of that in [C, Lemma 6.7].

The closed subspace Δ : X ⊂ X × X is co-classified by (≠_{X}), so the corresponding nucleus, in the senses of both locale theory (j = Δ_{∗} · Δ^{∗}) and of abstract Stone duality (E = ∀_{Δ} · Σ^{Δ}, Lemma 2.6 and Definition 7.17) takes

ϕ : Σ^{X×X} to λxy. (x ≠ y) ∨ ϕy.

Consider in particular ψ ≡ Σ^{p_{0}}ϕ, or ψ(x, y) ≡ ϕx; then

∀_{Δ}ϕ = ∀_{Δ} · Σ^{Δ} · Σ^{p_{0}}ϕ = ∀_{Δ} · Σ^{Δ}ψ = (∀_{Δ}⊥) ∨ Σ^{p_{0}}ϕ.

The same thing in λ-calculus notation, and its analogue for p_{1}, are

(∀_{Δ}ϕ)(x, y) = (x ≠ y) ∨ ϕx = (x ≠ y) ∨ ϕy.

Now apply ∀_{p_{0}} ≡ ∀y, so ϕ = ∀_{p_{0}} · ∀_{Δ}ϕ = ∀_{p_{0}}(∀_{Δ}⊥ ∨ Σ^{p_{0}}ϕ), i.e. ϕx = ∀y. (x ≠ y) ∨ ϕy. Inequality is irreflexive by definition. We deduce symmetry by putting ϕ ≡ λu. y ≠ u and the dual of the transitive law with ϕ ≡ λu. u ≠ z. □

The idea of the following construction is that K ⊂ U iff U ∪ V = X, and conversely x ∈ V iff K ⊂ X \ {x}, where K is compact and V is its complementary open subspace, encoded by A and ψ respectively. The lattice dual of this result — that open and overt subspaces coincide in an overt discrete space — was proved for ℕ in [A, Section 10].

Proposition 3.10 In any compact Hausdorff space K, there is a retraction Σ^{K} ◁ Σ^{Σ^{K}} given by

ψ ↦ λϕ. ∀x. ψx ∨ ϕx
A ↦ λx. A(λy. x ≠ y),

where, if A is so defined from ψ then it preserves ⊤ and ∧. Later we shall show that closed and compact subspaces agree exactly. Proof ψ ↦ A ↦ λx. A(λy. ψy ∨ x ≠ y) = ψ, by the second part of the Lemma. Then A⊤ = ⊤ easily, whilst A(ϕ_{1} ∧ ϕ_{2}) = Aϕ_{1} ∧ Aϕ_{2} by distributivity.

On the other hand, A ↦ ψ ↦ λϕ. ∀x. A(λy. ϕy ∨ x ≠ y), whilst the first part of the Lemma says that A = λϕ. A(λy. ∀x. ϕy ∨ x ≠ y), so for the bijection between closed and compact spaces we need A to commute with ∀x. To show this, we need to know about the Tychonov product topology on X × X (Remark 6.3), and to use Scott continuity (Theorem 7.6). □

For our purposes, it will not in fact be a very important requirement on A that it preserve ⊤ and ∧. Consider the localic situation.

Lemma 3.11 For β ∈ L in a continuous lattice (Definition 1.13(c)), the subset

↑ ↑ β ≡ {ϕ | β ≪ ϕ} ⊂ L

is Scott-open, and therefore classified by some A : Σ^{L} (Remark 2.2). However, ↑ ↑ β need not be a filter (cf. Definition 1.21), so A need not preserve ⊤ or ∧. □

We obtain similar behaviour even in traditional topology. The following may seem a strange thing to do, but it will fall into place as we start to use the λ-calculus.

Notation 3.12 In [A] we found it useful to regard any map F : Σ^{X} → Σ^{Y} (not necessarily a homomorphism for the monad or of frames, but nevertheless Scott-continuous) as a “second class” map F̂ : Y −× X, and to write HS for the category composed of such maps. The work cited there explains how they interpret “control effects” such as jumps in programming languages. We shall in particular meet I : Σ^{X} → Σ^{Y} such that Σ^{i} · I = id, where i : X Y.

Remark 3.13 Just as in Lemma 3.4 we formed the modal operator corresponding to the direct image iK of K along i : K → X as the composite A = ∀_{K} · Σ^{i}, so we may form the direct image F̂A along a second class map F̂ : K −× X as ∀_{K} · F. Its open neighbourhoods are given, as in Remark 3.5, by

(F̂K ⊂ ϕ) = (∀_{K} · F)ϕ = A(F ϕ) = (K ⊂ F ϕ).

However, ∀_{K} · F need only a filter when F preserves ⊤ and ∧.

Even when A does preserve meets, and so classifies a Scott-open filter of open subspaces, it need not correspond to a compact subspace. (It does in a compact Hausdorff space, but even there we do not yet have to tools to prove it, cf. Proposition 3.10.) We make a brief excursion into classical topology to illustrate the duality of open and compact subspaces, and their alternating inclusions (Notation 1.3). Recall from Definition 1.1 that any open subspace is the union of the compact subspaces inside it: the first result answers the dual question of when a compact subspace is the intersection of the open subspaces that contain it.

Lemma 3.14 Using excluding middle in classical topology [8, p221 def 2.1],

{y ∈ X | ∃x ∈ K. x ≤ y} = ⋂ ; {U ⊂ X open | K ⊂ U},

where ≤ is the specialisation order (Definition 2.5). We call this the saturation of K. Hence compact subspaces of X can be recovered from their modal operators iff X is T_{1} (when ≤ is trivial). For a specific non-example, let X = Σ and K = {⊥}, so A = λϕ. ϕ⊥ and the saturation of K is Σ. □

What we might hope to recover from the modal operator A, therefore, is the saturation of K, as Karl Hofmann and Michael Mislove did for sober spaces [8, Theorem 2.16], and Peter Johnstone did for locales [11]. This result shows that we have identified enough of the properties of modal operators, at least in the classical model.

Proposition 3.15 Let F ⊂ |Σ^{X} | be a Scott-open filter of open subspaces of a sober (but not necessarily locally compact) space. Then, assuming the axiom of choice, K ≡ ⋂ ; F ⊂ X is a compact subspace, and F = {U | K ⊂ U}. □

Proposition 3.16 [8, p221 thm 2.16] Let K ≡ ⋂ ; _{s} K_{s} be a co-directed intersection of compact saturated subspaces of a sober space. Then K is also compact saturated, and A_{K} = ⋁ ; A_{K_{s}}. If all of the K_{s} are inhabited then so is K. □

Theorem 3.17 Compact saturated subspaces of a locally compact sober space form a continuous preframe under reverse inclusion. That is, for any compact saturated subspace K ⊂ X,

K = ⋂ ; {L compact saturated | L ≺ ≺ K}.

Here L ≺ ≺ K means that there is an open subspace U with K ⊂ U ⊂ L (sic — Notation 1.3), but this is equivalent to L ≪ K, the order-reversed analogue of Definition 1.13(b), i.e.

K ⊃ ⋂ ; _{s}M_{s} ⇒ ∃s. K ⊃ M_{s}.  □

Corollary 3.18 Using Choice in classical topology, stably locally compact spaces enjoy the dual Wilker property (cf. Lemma 1.10): if K ∩ L ⊂ U then there are open subspaces V and W and compact ones K′ and L′ such that K′ ∩ L′ ⊂ U, K ⊂ V ⊂ K′ and L ⊂ W ⊂ L′ [15, Theorem 23]. Proof Use Lemma 1.19 in the continuous lattice of compact saturated subspaces under reverse inclusion. It is significant in this that the abstract joins in the lattice be given by intersections of subspaces. □

Remark 3.19 There is still a problem. Even when X itself is locally compact, and we have a filter F that is Scott-open and therefore classified by a term A of type Σ^{Σ^{X}}, the compact subspace K that they define need not be locally compact, and therefore need not be expressible in abstract Stone duality, as the theory currently stands.

It is a desirable property of A that it be a filter, i.e. preserve ⊤ and ∧, because then we can fully exploit the intuitions of traditional topology. However, this property is by no means essential, and we shall usually manage without it, working with As rather than Ks.

4 Effective bases

This section introduces the central technical concept of the paper, and explores the ways in which it arises in traditional topology and locale theory.

We say that a system (U^{n}) of vectors in a vector space is a basis if any other vector V can be expressed as a sum of scalar multiples of basic vectors. Likewise, we say that a system (U^{n}) of open subspaces of a topological space is a basis if any other open set V can be expressed as a “sum” (union or disjunction) of basic opens.

How do we find out which basis elements contribute to the sum, and (in the case of vector spaces) by what scalar multiple? By applying the dual basis A_{n} to the given element V, giving A_{n} · V. Then

V = ∑_{n} A_{n} · V ∗ U^{n}

where

(a) ∑ denotes linear sum, union, disjunction or existential quantification;

(b) “scalars” in the case of topology range over the Sierpiński space;

(c) the dot denotes

• inner product of a dual vector with a vector to yield a scalar,

• that V is an element of the family classified by A_{n}, or

• λ-application; and (d) ‘∗’ denotes multiplication by a scalar of a vector, or conjunction. In abstract Stone duality, since the application of A_{n} to a predicate V : Σ^{X} yields a scalar, it must have type Σ^{Σ^{X}}. In the previous section we saw that such terms play the role of compact subspaces.

Definition 4.1 An effective basis for a space X is a pair of families

n : N ⊢ β^{n} : Σ^{X} n : N ⊢ A_{n} : Σ^{Σ^{X}} ,

where N is an overt discrete space (Section 2), such that every “vector” ϕ has a basis decomposition,

ϕ : Σ^{X} ⊢ ϕ = ∃n. A_{n}ϕ ∧ β^{n}.

This is a join ⋁ {β^{n} | α_{n}} over a subset, with α_{n} = A_{n}ϕ, in the sense of Remark 2.20. In more topological notation, this equation says that

for all V ⊂ X open, V = ⋃ {U^{n} | V ∈ F_{n}},

where β^{n}, ϕ and A_{n} classify U^{n}, V and F_{n} in the sense of Remark 2.2.

We call (β^{n}) the basis and (A_{n}) the dual basis. The reason for saying that the basis is “effective” is that it is accompanied by a dual basis, so that the coefficients are given effectively by the above formula — it is not the computational aspect that we mean to stress at this point. The sub- and superscripts indicate the co- and contravariant behaviour of compact and open subspaces respectively with respect to continuous maps.

The first observation that we make about this definition expresses the inclusion U^{n} ⊂ K^{n} (Definition 1.5(f)). After that we see some suggestion of the role of compact subspaces, although this result is too specific to be of much use, unless there is a basis of compact open subspaces, i.e. X is a coherent space [9, Section II 3].

Lemma 4.2 If Γ ⊢ ϕ : Σ^{X} satisfies Γ ⊢ A_{n}ϕ = ⊤ then Γ ⊢ β^{n} ≤ ϕ. Proof Since A_{n}ϕ = ⊤, the basis decomposition for ϕ includes β^{n} as a disjunct. □

Lemma 4.3 If ⊢ A_{n}β^{n} = ⊤ then β^{n} classifies a compact open subspace.

[figure: 1; 1; Σ^{K} = Σ^{X} ↓ β^{n}; β^{n}; Σ^{X}; A_{n}; Σ; ⊤]

Proof The equation A_{n}β^{n} = ⊤ says that the square commutes. Any test map ϕ : Γ → Σ^{X} ↓ β^{n} that (together with ! : Γ → 1) also makes a square commute must satisfy Γ ⊢ A_{n}ϕ = ⊤ and Γ ⊢ ϕ ≤ β^{n}, but then ϕ = β^{n} by the previous result. Hence the square is a pullback, whilst β^{n} = ⊤_{Σ^{K}}, so the lower composite is ∀_{K}, making K compact. □

The following jargon will be useful:

Definition 4.4 An effective basis (β^{n}, A_{n}) is called

(a) a directed or ∨-basis if there is some element (that we call 0 ∈ N) such that

β^{0} = λx. ⊥ and A_{0} = λϕ. ⊤

(though A_{0} = ⊤ ⇒ β^{0} = ⊥ by Lemma 4.2) and a binary operation + : N × N → N such that

β^{n+m} = β^{n} ∨ β^{m}  and  A_{n+m} = A_{n} ∧ A_{m};

this definition is designed to work with Definition 2.21; it is used first in Lemma 7.8 and then extensively in Sections 8–11; (b) an intersection or ∧-basis if β^{1} = λx. ⊤ for some element (that we call 1 ∈ N), and there

is a binary operation ⋆ such that

β^{n⋆m} = β^{n} ∧ β^{m} A_{n} ≤ A_{n⋆m} and A_{m} ≤ A_{n⋆m},

so the intersection of finitely many basic opens is basic; this is a positive way of saying that we do have a basis instead of what is traditionally known as a sub-basis;

(c) a lattice basis if it is both ∧ and ∨;

(d) a filter basis if each A_{n} preserves ∧ and ⊤, and so corresponds in classical topology to a compact saturated (though not necessarily locally compact) subspace K^{n}, by Proposition 3.15;

(e) a prime basis if each A_{n} of the form A_{n}ϕ = ϕp^{n} for some p^{n} : X (cf. Axiom 2.3(b)), the corresponding compact subspace being K^{n} = {p^{n}}.

Any effective basis can be “up-graded” to a lattice basis by formally adding unions and intersections (Lemma 6.4ff). Elsewhere we show that it can be made into a filter ∨-basis instead [F–]. Some of the other terminology is only applicable in special situations: if A_{1}⊤ = ⊤ then the space is compact, with ∀_{X} = A_{1}, whilst a topological space has a prime basis iff it is a continuous poset with the Scott topology (Theorem 8.19). Even when the intersection of two compact subspaces is compact, there is nothing to make A_{n⋆m} correspond to it, but we shall rectify this in Proposition 8.13.

Examples 4.5 Let N be an overt discrete space. Then

(a) N has an N-indexed prime basis given by

β^{n} ≡ {n} ≡ λx. (x =_{N} n) and A_{n} ≡ η_{N}(n) ≡ λϕ. ϕn,

because ∃n. ηnϕ ∧ {n}m = ∃n. ϕn ∧ (m = n) = ϕm.

(b) Σ^{N} has a Fin(N)-indexed prime ∧-basis given by

B^{ℓ} ≡ λϕ. ∀m ∈ ℓ. ϕm and A_{ℓ} ≡ λF. F (λm. m ∈ ℓ),

because F ϕ = ∃ℓ. F (λm. m ∈ ℓ) ∧ ∀m ∈ ℓ. ϕm by Axiom 2.18. (The convention that superscripts indicate covariance (Remarks 2.7 and 2.20) means that the imposed order on Fin(N) here is reverse inclusion of lists.)

We devote the remainder of this section to showing that every locally compact sober space or locale has an effective basis in our sense.

Proposition 4.6 Any locally compact sober space has a filter basis. Proof Definitions 1.1 and 1.5(f) provide families (K^{n}) and (U^{n}) of compact and open subspaces such that

for each open V ⊂ X, V = ⋃ {U^{n} | K^{n} ⊂ V };

As the subspace K^{n} is compact, Remark 3.5 defines A_{n} : Σ^{X} → Σ such that K^{n} ⊂ V iff A_{n}ϕ = ⊤, where β^{n} and ϕ : Σ^{X} classify U^{n} and V ⊂ X, so ϕ = ∃n. A_{n}ϕ ∧ β^{n}. □

Notice how the basis decomposition “short changes” us, for individual basis elements: we “pay” K^{n} ⊂ V but only receive U^{n} ⊂ K^{n} as a contribution to the union. Nevertheless, the interpolation property (Lemma 1.2) ensures that we get our money back in the end.

In many examples, U^{n} may be chosen to be interior of K^{n}, and K^{n} the closure of U^{n}. However, this may not be possible if we require an ∨-basis. For example, such a basis for ℝ would have as one of its members a pair of touching intervals, (0, 1) ∪ (1, 2), which is not the interior of [0, 1] ∪ [1, 2].

Remark 4.7 It is difficult to identify a substantive Theorem by way of a converse to this in traditional topology, since the λ-calculus can only by interpreted in a topological space if it is already locally compact, and therefore has an effective basis. Nevertheless, we can show that a filter basis (β^{n}, A_{n}) can only arise in the way that we have just described.

By Proposition 3.15, each A_{n} corresponds to some compact saturated subspace K^{n}, where

(K^{n} ⊂ V) ⟺ A_{n}ϕ ⟹ (U^{n} ⊂ V),

β^{n} and ϕ being the classifiers for U^{n} and V as usual. Since K^{n} = ⋂ ; {V | K^{n} ⊂ V }, we must have U^{n} ⊂ K^{n}. Then, given x ∈ V, so ϕx = ⊤, the basis decomposition ϕx = ∃n. A_{n}ϕ ∧ β^{n}x, means that x ∈ U^{n} ⊂ K^{n} ⊂ V, as in Definition 1.1. □

Remark 4.8 Martín Escardó proposes various candidates for “imaginary spaces” that would generalise the exponentials beyond locally compact spaces [4, §10]. By Corollary 5.5 below, such an imaginary space has an effective basis iff it is a locally compact “real” space. The existence of an effective basis on an object would therefore become the definition of local compactness in an extension of ASD, rather than a theorem for every definable object of the category.

Unfortunately, Escardó’s work cannot yet provide such an extension, as it is currently restricted to the the “classical” case in Remark 2.1, because his concrete examples are all modifications of textbook categories, whilst his abstract methods rely in other ways on an underlying topos.

Example 4.9 The closed real unit interval has a filter ∧-basis with

β^{q±ϵ} ≡ (q ± ϵ) ≡ λx. |x − r| < ϵ
A_{q±δ} ≡ [q ± δ] ≡ λϕ. ∀x. |x − r| ≤ δ ⇒ ϕx

where ϵ, δ > 0 and q are rational, and we re-deploy the interval notation of Example 1.4 in our λ-calculus. We also write ⟨r ± δ⟩ for a variable that ranges over the codes, as opposed to the open (r ± δ) and compact [r ± δ] intervals that it names. The imposed order is given by comparison of the radii ϵ or δ. Proof Let x ∈ U ⊂ [0, 1]; then, for some ϵ > 0, ∀y. |x − y| < ϵ ⇒ y ∈ U. So with δ = \frac{1}{2}ϵ, and r rational such that |x − r| < δ,

∀y. |y − r| ≤ δ ⇒ y ∈ U ∧ x ∈ {y | |y − r| < δ},

which is ∃⟨r ± δ⟩. A_{r±δ}ϕ ∧ β^{r±δ}x in our notation. □

Example 4.10 Recall that any compact Hausdorff space X has a stronger property called regularity: if C ⊂ X is closed with x ∉ C then there are x ∈ U ∩̸ V ⊃ C with U, V ⊂ X open and disjoint. Writing K = X \V and W = X \C for the complementary compact and open subspaces, this says that given x ∈ W, we can find x ∈ U ⊂ K ⊂ W, as in Definition 1.1. Let (β^{n}, γ_{n}) classify a sufficient computable family (U^{n} ∩̸ V_{n}) of disjoint open pairs, and put A_{n} ≡ λϕ. ∀x. ϕx ∨ γ_{n}x, which corresponds to the compact complement of V_{n} (Proposition 3.10). Then (β^{n}, A_{n}) is a filter basis for X. It is a lattice basis if the families (β^{n}) and (γ_{n}) are sublattices, with γ_{0} = ⊤, γ_{1} = ⊥, γ_{n+m} = γ_{n} ∧ γ_{m} and γ_{n⋆m} = γ_{n} ∨ γ_{m}. □

Remark 4.11 In these idioms of topology, where we say that there “exists” an open or compact subspace within certain bounds, that subspace may usually be chosen to be basic, and the existential quantifier in the assertion ranges over the overt discrete space N of indices for the basis, rather than over the topology Σ^{X} itself.

Proposition 4.12 Any locally compact locale has a lattice basis. Proof The localic definition is that the frame L be a distributive continuous lattice (Definition 1.13(c)), so

for all ϕ ∈ L, ϕ = ⋁ {β ∈ L | β ≪ ϕ},

and by Lemma 3.11, ↑ ↑ β ≡ {ϕ | β ≪ ϕ} is classified by some A : Σ^{L}.

This means that there is a basis decomposition

ϕ = ∃n. β^{n} ∧ A_{n}ϕ, where A_{n} ≡ λϕ. (β^{n} ≪ ϕ),

so (β^{n}, A_{n}) is an effective basis.

Recall, however, from Remark 2.7 that we must consider this basis to be indexed by the underlying set, |L|, of the frame L. Thus N ≡ |L|, whilst β^{(−)} : N → L is the couniversal map from an overt discrete object N to L.

In fact it is enough for the image of N to generate L under directed joins (Definition 1.15). There is no need for N to be the couniversal way of doing this, and so no need for the underlying set functor |−|. □

Remark 4.13 : The first part of the converse to this is Lemma 4.3, but with the relative notion ≪ in place of compactness itself: if A_{n}ϕ = ⊤ then β^{n} ≪ ϕ in the sense of Definition 1.13(b). For suppose that ϕ ≤ ⋁ ; _{s} θ_{s}, so ⊤ = A_{n}ϕ ≤ A_{n} ⋁ ; _{s} θ_{s} = ⋁ ; _{s} A_{n}θ_{s}. Then^{5} A_{n}θ_{s} = ⊤ for some s, so β^{n} ≤ θ_{s} by Lemma 4.2.

Now suppose that a locale carries an effective basis in our sense. Then

ϕ = ∃n. A_{n}ϕ ∧ β^{n} ≡ ⋁ {β^{n} | A_{n}ϕ} ≤ ⋁ ; {β^{n} | β^{n} ≪ ϕ} ≤ ϕ,

in which the second join is directed by Lemma 1.18. Hence the frame L is continuous. □

Remark 4.14 Notice that β^{m} ≤ β^{n} does not imply any relationship between n, m ∈ N, because β^{(−)} : N → L need not be injective. This is the reason why A_{n} need not be exactly λϕ. β^{n} ≪ ϕ, cf. Remark 1.8.

Proposition 4.15 A locale is stably locally compact iff it has a lattice filter basis. Proof [⇒] Let A_{n} = λϕ. β^{n} ≪ ϕ as before. [⇐] As we have an ∨-basis, the basis expansion is a directed join, to which we may apply the definition of β^{m} ≪ ϕ. In this case there is some n with β^{m} ≤ β^{n} and A_{n}ϕ = ⊤, so β^{m} ≪ ⊤. Also, if β^{m} ≪ ϕ and β^{m} ≪ ψ then, for some p, q,

β^{m} ≤ β^{p}, β^{m} ≤ β^{q}, A_{p}ϕ = ⊤ and A_{q}ψ = ⊤,

so β^{m} ≤ β^{p} ∧ β^{q} ≡ β^{p⋆q}. As we have a filter ∧-basis, A_{p⋆q}ϕ ∧ A_{p⋆q}ψ ≡ A_{p⋆q}(ϕ ∧ ψ) = ⊤. Hence, with n = p ⋆ q, β^{m} ≤ β^{n} and A_{n}(ϕ ∧ ψ) = ⊤, so β^{m} ≪ ϕ ∧ ψ. □

Remark 4.16 In summary, the dual basis A_{n}ϕ essentially says that there is a compact subspace K^{n} lying between β^{n} and ϕ, but K^{n} seems to play no actual role itself, and the localic definition in terms of ≪ makes it redundant. Nevertheless, each definition actually has its technical advantages:

(a) in the localic one, β ranges over a lattice, but ↑ ↑ β need not be a filter;

(b) in the spatial one we have filters, but the basis need only indexed by a semilattice. Effective bases in our sense can be made to behave in either fashion, though we shall only consider lattice bases (cf. the localic situation) in this paper. Stably locally compact objects have lattice filter bases, whose properties will be improved in Proposition 8.13 to take advantage of the intersections of compact subspaces.

5 Σ-split subspaces

A basis for a vector space is exactly (the data for) an isomorphism with ℝ^{N}, where N is the dimension of the space. It is not important for the analogy that the field of scalars be ℝ, or even that the dimension be finite. The significance of ℝ^{N} is that it carries a standard structure (in which the nth basis vector has a 1 in the nth co-ordinate and 0 elsewhere) which is transfered by the isomorphism to the chosen structure on the space under study. The standard object in our case is the space Σ^{N} (or the corresponding algebra Σ^{Σ^{N}}), for which Axiom 2.18 defined a basis.

5This involves the same confusion of internally and externally defined joins as in Definition 3.1, cf. Remark 2.19.

Bases for lattices are actually more like spanning sets than (linearly independent) bases for vector spaces, since we may add unions of members to the basis as we please, as we do in Lemma 6.4 below. Consequently, instead of isomorphisms with the standard structure, we have Σ-split embeddings X Σ^{N}. We shall see that these embeddings capture several well known constructions involving ℝ and locally compact spaces.

Definition 5.1 i : X Y is a Σ-split subspace if (it is the equaliser of some pair [B] and) there is a map I : Σ^{X} → Σ^{Y} such that Σ^{i} · I = id_{Σ^{X}}. Using Notation 3.12, we write

[figure: X; i; × \underline{Î}; Y; Σ^{X}; \underline{Σ^{i}}; I; Σ^{Y}]

The effect of this is that X carries the subspace topology inherited from Y, in a canonical way. The computational significance of Σ-split embeddings is that any observation (computation of type Σ) on the subspace extends canonically but not uniquely to the whole space; in particular I = ∃_{i} or ∀_{i} in the case of an open or closed subspace [B].

Lemma 5.2 Any object X that has an effective basis (β^{n}, A_{n}) indexed by N is a Σ-split subspace of Σ^{N}. Proof Using the basis (β^{n}, A_{n}), define

i : X → Σ^{N}  by x ↦ λn.β^{n}x
I : Σ^{X} → Σ^{Σ^{N}} by ϕ ↦ λψ.∃n. A_{n}ϕ ∧ ψn.

Then Σ^{i}(Iϕ) = λx. (Iϕ)(ix) = λx. ∃n. A_{n}ϕ ∧ β^{n}x = ϕ. □

Lemma 5.3 An embedding X Σ^{N} arises from a basis in this way iff each Iϕ preserves joins. It’s then a filter basis iff, for each n, λϕ. Iϕ{n} also preserves finite meets. Proof For any basis, ψ ↦ ∃n. A_{n}ϕ ∧ ψn preserves joins. Conversely, with

β^{n} ≡ λx. ixn and A_{n} ≡ λϕ. Iϕ{n}

we recover ϕx ≡ (Iϕ)(ix) = ∃n. Iϕ{n} ∧ ixn = ∃n. A_{n}ϕ ∧ β^{n}x so long as Iϕ preserves the join ix = ∃n. ixn ∧ {n}. □

Conversely, any Σ-split subspace inherits the basis of the ambient space, using the inverse images of the basic open subspaces along i : X Y. However, for the compact subspaces, we use their direct images along the “second class” map Î: Y × X, in the sense of Remark 3.13. Since I need not preserve meets, nor need the modal operator Σ^{I}A ≡ A · I. This is why we find bases in which A_{n} need not preserve ⊤ and ∧.

Lemma 5.4 Let (β^{n}, A_{n}) be an effective basis for Y and i : X Y a Σ-split subspace. Then (Σ^{i}β^{n}, Σ^{I}A_{n}) is an effective basis for X. If an ∨- or ∧-basis was given, the result is one too. If A_{n} is a filter and I preserves ⊤ and ∧ then Σ^{I}A_{n} is also a filter. Proof For ϕ : Σ^{X}, Iϕ : Σ^{Y} has basis decomposition

Iϕ = ∃n. A_{n}(Iϕ) ∧ β^{n} ≡ ∃n. (Σ^{I}A_{n})ϕ ∧ β^{n}.

Since Σ^{i} is a homomorphism, it preserves scalars, ∧ and ∃, so

ϕ = Σ^{i}(Iϕ) = Σ^{i}(∃n. A_{n}(Iϕ) ∧ β^{n}) = ∃n. A_{n}(Iϕ) ∧ Σ^{i}β^{n}.  □

Corollary 5.5 An object has an effective basis iff it is a Σ-split subspace of some Σ^{N}. Proof The Scott principle (Axiom 2.18) defined a basis on Σ^{N}. □

In the rest of this section we consider the classical interpretations of the Σ-split embedding that arises from an effective basis. Recall from [9, Theorem II 1.2] that the free frame on N is ΥKN (the lattice of upper subsets of KN), and that this is isomorphic to the lattice of Scott-open subsets of the powerset P(N).

Theorem 5.6 Let X be a locally compact sober space with N-indexed basis (U^{n}, K^{n}). Then X is a Σ-split subspace of P(N). Proof The embedding in Lemma 5.2 takes

x ∈ X to {n | x ∈ U^{n}} ∈ P(N)
V ⊂ X to {ℓ | ∃n ∈ ℓ. K^{n} ⊂ V } ∈ ΥKN.

The second map, I, is Scott-continuous because it takes ⋃ ; _{s} V_{s} to

{ℓ | ∃n ∈ ℓ. K^{n} ⊂ ⋃ ; _{s}V_{s}} = {ℓ | ∃n ∈ ℓ. ∃s. K^{n} ⊂ V_{s}} = ⋃ ; _{s}{ℓ | ∃n ∈ ℓ. K^{n} ⊂ V_{s}}.

The composite Σ^{i} · I takes V ⊂ X to ⋃ {⋂_{n∈ℓ} U^{n} | ∃n ∈ ℓ. K^{n} ⊂ V }. This contains V = {x | ∃n. x ∈ U^{n} ⊂ K^{n} ⊂ V } by Definition 1.1. Conversely, if x ∈ Σ^{i}(IV) then ∃ℓ. ∀n ∈ ℓ. x ∈ U^{n} ∧ ∃m ∈ ℓ. K^{n} ⊂ V, so ∃n. x ∈ U^{n} ⊂ K^{n} ⊂ V. □

Example 5.7 A compact Hausdorff space has a basis determined by a family of disjoint pairs (U^{n} ∩̸ V_{n}) of open subspaces. In this case, the embedding is

x ↦ {n | x ∈ U^{n}}
W ↦ {ℓ | ∃n ∈ ℓ. V_{n} ∪ W = X}  □

Consider in particular the embedding of ℝ in Σ^{N}, where N indexes a basis of open and closed intervals (Examples 1.4 and 4.9). This is closely related to one of the first examples that Dana Scott used to show how continuous lattices could be used as a model of computation [17].

Definition 5.8 The domain of intervals, Iℝ, of ℝ is the set of closed inhabited intervals [r ±δ], with r ∈ ℝ, 0 ≤ δ ≤ ∞, ordered by reverse inclusion, and given the Scott topology. The lattice of intervals, Iℝ^{⊤}, also includes the empty set, as the top element. We similarly define I[0, 1] from the closed unit interval.

Proposition 5.9 In LKSp, ℝ Iℝ ^{⊏} Iℝ^{⊤}[figure] Σ^{N}, where N is the set of pairs, written ⟨q ± ϵ⟩, with ϵ > 0 and q rational. Indeed, ℝ is identified with the maximal elements of Iℝ. Proof The embedding takes r ∈ ℝ to [r ± 0] and then to λ⟨q ± ϵ⟩. r ∈ (q ± ϵ), which is (the exponential transpose of) a continuous function. The retraction is defined by intersection:

[figure: Iℝ^{⊤}; Σ^{N}]
C  λ⟨q ± ϵ⟩. C ⊂ (q ± ϵ)
[r ± δ]  λ⟨q ± ϵ⟩. q − ϵ < r − δ ≤ r + δ < q + ϵ
∅  λ⟨q ± ϵ⟩. ⊤
ℝ  λ⟨q ± ϵ⟩. (ϵ = ∞)
⋂_{ϕ⟨q±ϵ⟩}[q ± ϵ] ϕ

Any compact interval of the T_{1} space ℝ is saturated in the sense of Lemma 3.14. It is therefore the intersection of its open neighbourhoods, amongst which open intervals suffice. Hence the composite is Iℝ^{⊤} → Σ^{N} → Iℝ^{⊤} is the identity.

The projection Iℝ^{⊤} [figure] Σ^{N} is Scott-continuous because it clearly takes directed unions of sets of codes to codirected intersections of compact subspaces. However, Proposition 3.16 showed that such intersections correspond to unions of neighbourhood filters, so the inclusion Iℝ^{⊤} Σ^{N} is also Scott-continuous.

The inverse image of ⊤ under Iℝ^{⊤} [figure] Σ^{N} is the open subspace classified by the inconsistency predicate

InCon(ϕ) ≡ ∃⟨q_{1} ± ϵ_{1}⟩⟨q_{2} ± ϵ_{2}⟩. q_{1} + ϵ_{1} < q_{2} − ϵ_{2}.

The complementary closed subspace of Σ^{N} is of course not classified, as it’s not open, but when we restrict attention to its (overt discrete collection of) finite elements we find that consistency is characterised by the decidable formula

Con(ℓ) ≡ ∃x:ℚ. ∀⟨q ± ϵ⟩ ∈ ℓ. x ∈ ⟨q ± ϵ⟩,

so InCon(λ⟨q ± ϵ⟩. ⟨q ± ϵ⟩ ∈ ℓ) = ¬Con(ℓ).  □

Remark 5.10 The idea behind the domain of intervals is not hard to generalise. Indeed, we may embed any locally compact sober space as a subspace of its continuous preframe of compact saturated subspaces (Theorem 3.17), each point being represented by its saturation in the sense of Lemma 3.14. That the image consists of the maximal points (excluding ∅) plainly depends on starting with a T_{1}-space, so can’t be an essential feature of the construction.

Some of the standard pathologies of real analysis can be represented by functions with values in Iℝ, the simplest example being a function ℝ → ℝ with a jump discontinuity such as the “sign” function [3, §3].

Another interesting aspect of the general construction is the decidable consistency predicate on finite elements. Scott developed these into what became a standard form of domain theory [18]. The consistent subspace of Σ^{N} is closed, but also overt [H].

Having identified this subspace, we then obtain Iℝ as a retract. This takes a collection of basic closed subspaces to its intersection C, and thence to the collection of all open neighbourhoods of C. I am not convinced of the importance of this step, as it seems to leave us in No Man’s Land between mathematical and computational ideas. The simple type Σ^{N} would appear to be the appropriate place in which to execute computations from which the mathematical meaning has been erased.

Now we give the localic version of Theorem 5.6.

Theorem 5.11 Let L be any N-based continuous distributive lattice. Then there is a frame homomorphism H and a Scott-continuous function I with H · I = id_{L}, as shown:

L[figure: \underline{H}; I] ΥKN

Conversely, any lattice L that admits such a pair of functions is continuous and distributive. Proof [⇒] Let (β^{n}) be a basis for the continuous lattice L and A_{n} = λϕ. (β^{n} ≪ ϕ). Let H : ΥKN → L be the unique frame homomorphism that extends β^{(−)} : N → L, so

for U ∈ ΥKN, HU = ⋁_{ℓ∈U} ⋀_{n∈ℓ} β^{n} ∈ L,

and define I : L → ΥKN by Iϕ = {ℓ | ∃n ∈ ℓ. β^{n} ≪ ϕ}. This is Scott-continuous by a similar argument to that in Theorem 5.6, with β^{n} ≺ ≺ ϕ_{s} instead of K^{n} ⊂ V_{s}. Then

β^{n} ≪ H(Iϕ) ⟺ ∃ℓ. β^{n} ≪ ⋀_{m∈ℓ} β^{m} ∧ ∃m ∈ ℓ. β^{m} ≪ ϕ
⟺ ∃m. β^{n} ≪ β^{m} ≪ ϕ ⟺ β^{n} ≪ ϕ,

from which we deduce H(Iϕ) = ϕ, because (β^{n}) is a basis.

[⇐] Conversely, if such a diagram exists then I · H is a Scott-continuous idempotent on a continuous lattice, so its splitting L is also continuous [9, Lemma VII 2.3]. As H preserves joins, it has a right adjoint, H ⊣ R, so id ≤ R · H ≡ j = j · j, and R preserves meets but not necessarily directed joins. Since H also preserves finite meets, so does j, and this is a nucleus in the sense of locale theory [9, Section II 2.2], so its splitting L is a frame. □

Any locally compact locale is therefore determined by a Scott-continuous idempotent E on ΥKN. It is not just an idempotent, however, since the surjective part of its splitting must be a frame homomorphism. Since the latter preserves ⊤ and ⊥ by monotonicity, and ⋁ ; as E is Scottcontinuous, it is enough to identify the condition on E the ensures preservation of the two binary lattice connectives, which we may treat exactly alike.

Lemma 5.12 Let I and H be monotone functions between two semilattices, with H · I = id. Then H preserves ∧ iff E ≡ I · H satisfies the equation E(ϕ ∧ ψ) = E(Eϕ ∧ Eψ). Proof If H preserves ∧ then

E(ϕ ∧ ψ) ≡ I(H(ϕ ∧ ψ))
= I(Hϕ ∧ Hψ)  hypothesis
= I(H · I · Hϕ ∧ H · I · Hψ)  H · I = id
= I · H(I · Hϕ ∧ I · Hψ)  hypothesis
≡ E(Eϕ ∧ Eψ)

For the converse, note first that we have H(ϕ ∧ ψ) ≤ Hϕ ∧ Hψ and I(ϕ′ ∧ ψ′) ≤ Iϕ′ ∧ Iψ′ by the definition of ∧. Then

I(Hϕ ∧ Hψ) = E(I(Hϕ ∧ Hψ))  I = I · H · I = E · I
≤ E(I · Hϕ ∧ I · Hψ)  above
= E(Eϕ ∧ Eψ)  E = I · H
= E(ϕ ∧ ψ)  hypothesis
= I · H(ϕ ∧ ψ)  E = I · H
Hϕ ∧ Hψ  ≤ H(ϕ ∧ ψ)  H · I = id

so H(ϕ ∧ ψ) ≤ Hϕ ∧ Hψ ≤ H(ϕ ∧ ψ). □

We now have to concentrate on the logical development within abstract Stone duality, and will only return to the connection with traditional topology in Section 12. The first task is to show that every definable space has an effective basis, and is therefore a Σ-split subspace of Σ^{N}. Such subspaces are determined by idempotents E on Σ^{Σ^{N}} satisfying the equation that we have just identified, along with its counterpart for ∨. However, even that characterisation depends on the use of bases (Lemma 7.18ff).

6 Every definable space has a basis

In Section 4, we justified the notion of effective basis in the classical models, i.e. for locally compact sober spaces and locales. This section considers the term model, showing by structural recursion that every definable type has an effective basis. We have already dealt with the base cases (Σ, ℕ, Σ^{ℕ}), and with Σ-split subspaces, so we consider binary products first (leaving the reader to define the 1-indexed basis for 1), then devote most of the section to the exponential Σ^{X}.

Lemma 6.1 If X and Y have effective bases then so does X × Y, given by Tychonov rectangles. Proof Given (β^{n}, A_{n}) and (γ^{m}, D_{m}) on X and Y, define

ϵ^{(n,m)} ≡ λxy. β^{n}x ∧ γ^{m}y
F_{(n,m)} ≡ λθ:Σ^{X×Y} . D_{m}(λy. A_{n}(λx. θ(x, y))),

on X × Y. Then

θ(x, y) = ∃n. A_{n}(λx′. θ(x′, y)) ∧ β^{n}x
= ∃nm. D_{m}(λy′. A_{n}(λx′. θ(x′, y′))) ∧ γ^{m}y ∧ β^{n}x
= ∃(n, m). F_{(n,m)}θ ∧ ϵ^{(n,m)}(x, y)  □

Notice that the formula for F_{(n,m)} is not symmetrical in X and Y, though we have learned to expect properties of binary products to be asymmetrical and problematic [A]. In fact, if A_{n} and D_{m} are filter bases, we have another example of the same problem that held us back in Proposition 3.10, along with the core of its solution.

Lemma 6.2 If A : Σ^{Σ^{X}} and D : Σ^{Σ^{Y}} both preserve either ⊤ and ∧ or ⊥ and ∨ then

A(λx. D(λy. θxy)) = D(λy. A(λx. θxy))

whenever θ : Σ^{X×Y} is a finite union of rectangles. Proof Applying the Phoa principle (Axiom 2.4) to a single rectangle,

A(λx. D(λy. ϕx ∧ ψy))
= A(λx. D⊥ ∨ ϕx ∧ Dψ)  Phoa for D wrt ϕx
= A(λx. ϕx ∧ Dψ) ∨ (D⊥ ∧ A⊤)  Phoa for A wrt D⊥
= A⊥ ∨ (Dψ ∧ Aϕ) ∨ (D⊥ ∧ A⊤)  Phoa for A wrt Dψ.

This would have the required symmetry if we had

A⊥ ∨ (D⊥ ∧ A⊤) = (A⊥ ∧ D⊤) ∨ D⊥.

If A⊤ = ⊤ = D⊤ then both sides are A⊥ ∨ D⊥, whilst if A⊥ = ⊥ = D⊥ then they are both ⊥. Under either hypothesis, the lattice dual argument shows the similar result

A(λx. D(λy. ϕx ∨ ψy)) = D(λy. A(λx. ϕx ∨ ψy))

for a cross. Now suppose, for illustration, that θ is a union of three rectangles,

θxy = (ϕ_{1}x ∧ ψ_{1}y) ∨ (ϕ_{2}x ∧ ψ_{2}y) ∨ (ϕ_{3}x ∧ ψ_{3}y).

If A and D preserve ⊥ and ∨ then ADθ is also a union of three terms, to each of which the first part applies.

We may also use distributivity of ∨ over ∧ to re-express the union θ as an intersection of eight crosses,

θxy = (ϕ_{1}x ∨ ϕ_{2}x ∨ ϕ_{3}x) ∧ (ϕ_{1}x ∨ ϕ_{2}x ∨ ψ_{3}y) ∧
(ϕ_{1}x ∨ ψ_{2}y ∨ ϕ_{3}x) ∧ (ϕ_{1}x ∨ ψ_{2}y ∨ ψ_{3}y) ∧
(ψ_{1}y ∨ ϕ_{2}x ∨ ϕ_{3}x) ∧ (ψ_{1}y ∨ ϕ_{2}x ∨ ψ_{3}y) ∧
(ψ_{1}y ∨ ψ_{2}y ∨ ϕ_{3}x) ∧ (ψ_{1}y ∨ ψ_{2}y ∨ ψ_{3}y).

So if A and D preserve ∧ then ADθ is a conjunction of eight factors, to each of which the second part applies, for example with ϕ = ϕ_{1} ∨ ϕ_{2} and ψ = ψ_{3}. In both cases, ADθ = DAθ as required. □

Remark 6.3 This still awaits Theorem 7.6 on Scott continuity to extend finite unions of rectangles to infinite ones, but once we have that we may draw the corollaries that

(a) if X and Y have filter bases then Lemma 6.1 provides a filter basis for X×Y, and is symmetrical in X and Y;

(b) Proposition 3.10 yields a bijection between closed and compact subspaces of a compact Hausdorff space. Moreover, despite the other problems discussed in Section 3, preserving finite meets is enough to characterise □ modal operators. □

We shall need to be able to turn any effective basis into a ∨-basis, which we do in the obvious way using finite unions of basic open subspaces. The corresponding unions of compact subspaces give rise to conjunctions of As by Lemma 3.6(c). Unfortunately, the result is topologically rather messy, both for products and for spaces such as ℝ that we want to construct directly. It could be that we should see this as an embedding into Σ^{Σ^{N}} rather than into Σ^{FinN}, cf. [E].

Lemma 6.4 If X has an effective basis indexed by N then it also has a ∨-basis indexed by Fin(N). If we were given a filter basis, the result is one too. Proof Given any basis (β^{n}, A_{n}), define

γ^{ℓ} ≡ λx. ∃n ∈ ℓ. β^{n}x D_{ℓ} ≡ λϕ. ∀n ∈ ℓ. A_{n}ϕ.

Then ϕ = ∃n. A_{n}ϕ ∧ β^{n} ≤ ∃ℓ. D_{ℓ}ϕ ∧ γ^{ℓ} using singleton lists. Conversely,

∃ℓ. D_{ℓ}ϕ ∧ γ^{ℓ} = ∃ℓ. (∀n ∈ ℓ. A_{n}ϕ) ∧ (∃m ∈ ℓ. β^{m})
= ∃ℓ. ∃m ∈ ℓ. (∀n ∈ ℓ. A_{n}ϕ) ∧ β^{m}
≤ ∃ℓ. ∃m ∈ ℓ. A_{m}ϕ ∧ β^{m} = ϕ.

Then (γ^{ℓ}, D_{ℓ}) is a ∨-basis using list concatenation for +. The imposed order ≼ on Fin(N) is list or subset inclusion,

(ℓ ≼ ℓ′) ≡ (ℓ ⊂ ℓ′) ≡ ∀n ∈ ℓ. n ∈ ℓ′.

Finally, if the A_{n} were filters then so are the D_{ℓ}, since ∀m ∈ ℓ preserves ∧ and ⊤. □

Lemma 6.5 If a ∧-basis was given, the previous result yields a lattice basis. Proof We are given β^{n} ∧ β^{m} = β^{n⋆m}.

Let ℓ ⋆ ℓ′ be the list (it doesn’t matter in what order) of n ⋆ m for n ∈ ℓ and m ∈ ℓ′. In functional programming notation, this is

ℓ ⋆ ℓ′ ≡ flatten (map ℓ (λn. map ℓ′(λm. n ⋆ m))),

where map applies a function to each member of a list, returning a list, and flatten turns a list of lists into a simple list. Categorically, map is the effect of the functor List(−) on morphisms, and flatten is the multiplication for the List monad. Using the corresponding notions for K(−), ⋆ can similarly be defined for finite subsets instead.

Now let

β^{ℓ⋆ℓ′} ≡ (∃n ∈ ℓ. ∃m ∈ ℓ′. β^{n⋆m}) = (γ^{ℓ} ∧ γ^{ℓ′})

by distributivity in Σ^{X}, whilst γ{ ; |1| ; } ≡ β^{1} and D{ ; |1| ; } ≡ A_{1} (where { ; |1| ; } is the singleton list) serve for γ^{1} and D_{1}. □

Remark 6.6 By switching the quantifiers we may similarly obtain ∧-bases, and turn a ∨-basis into a lattice basis. In fact, this construction featured in the proof of Theorems 5.6 and 5.11. This time the filter property is not preserved, since if A_{n}ϕ means K^{n} ⊂ U then A_{ℓ}ϕ means that ∃n ∈ ℓ. K^{n} ⊂ U, which is not the same a testing containment of a single compact subspace. Proposition 8.13 shows how to define an ∧-basis for a locally compact object in which A_{n⋆m} actually captures the intersection of the compact subspaces.

Proposition 6.7 N and Σ^{N} have effective bases as follows:

N prime  β^{n} ≡ {n} ≡ λm. (n = m) A_{n} ≡ η_{N}(n) ≡ λϕ. ϕn
N filter ∨ β^{ℓ} ≡ λm. m ∈ ℓ A_{ℓ} ≡ λϕ. ∀m ∈ ℓ. ϕm
N lattice  β^{L} ≡ λm. ∀ℓ ∈ L. m ∈ ℓ A_{L} ≡ λϕ. ∃ℓ ∈ L. ∀m ∈ ℓ. ϕm
Σ^{N} prime ∧ B^{ℓ} ≡ A_{ℓ} A_{ℓ} ≡ η_{Σ^{N}} β^{ℓ} ≡ λF. F (λm. m ∈ ℓ)
Σ^{N} filter lattice B^{L} ≡ A_{L}  A_{L} ≡ λF. ∀ℓ ∈ L. F (λm. m ∈ ℓ)

indexed by n : N, ℓ : Fin(N) or L : Fin(Fin(N)). The interchange of sub- and superscripts means that we’re reversing the imposed order on these indexing objects (Remark 2.20). □

The last of these also provides a basis for Σ^{Σ^{N}}, using Axiom 2.18 twice.

Lemma 6.8 Σ^{Σ^{N}} has a Fin(FinN)-indexed prime ∧-basis with

B^{L} ≡ A_{L} ≡ λF. ∀ℓ ∈ L. F β^{ℓ} and A_{L} ≡ η_{Σ^{2}N}A_{L} ≡ λF. FA_{L},

so, using Σ^{3}N as a shorthand for a tower of exponentials, ΣΣ^{Σ^{N}} ≡ (((N → Σ) → Σ) → Σ),

F : Σ^{3}N, F : Σ^{Σ^{N}} ⊢ FF = ∃L:Fin(FinN). FA_{L} ∧ ∀ℓ ∈ L. F β^{ℓ}.

Proof The prime ∧-basis on Σ^{N} makes Σ^{Σ^{N}} ◁ Σ^{Fin(N)} by

F ↦ λℓ. F β^{ℓ} and λϕ. ∃ℓ. Gℓ ∧ ∀n ∈ ℓ. ϕn ← G,

so Σ^{3}N ◁ Σ^{2}Fin(N) by

F ↦ λG. F(λϕ. ∃ℓ. Gℓ ∧ ∀n ∈ ℓ. ϕn) and λF. G(λℓ. F β^{ℓ}) ← G.

Using the prime ∧-basis on Σ^{Fin(N)}, for G : Σ^{Fin(N)},

GG = ∃L:FinFin(N). G(λℓ. ℓ ∈ L) ∧ ∀ℓ ∈ L. Gℓ
= ∃L. F(λϕ. ∃ℓ. (λℓ. ℓ ∈ L)ℓ ∧ ∀n ∈ ℓ. ϕn) ∧ ∀ℓ ∈ L. Gℓ
= ∃L. F(λϕ. ∃ℓ ∈ L. ∀n ∈ ℓ. ϕn) ∧ ∀ℓ ∈ L. Gℓ
= ∃L. FA_{L} ∧ ∀ℓ ∈ L. Gℓ

so F = λF. G(λℓ. F β^{ℓ}) = λF. ∃L. FA_{L} ∧ ∀ℓ ∈ L. F β^{ℓ}. □

Lemma 6.9 If X has an effective basis (β^{n}, A_{n}) then Σ^{X} has a lattice basis (D^{L}, λF. F γ_{L}) indexed by L : Fin(FinN), where

γ_{L} ≡ λx. ∃ℓ ∈ L. ∀n ∈ ℓ. β^{n}x and D^{L} ≡ λψ. ∀ℓ ∈ L. ∃n ∈ ℓ. A_{n}ψ.

Proof By Lemma 5.2, there is an embedding i : X Σ^{N} with Σ-splitting I by

ix ≡ λn. β^{n}x and Iψ ≡ λϕ. ∃n. A_{n}ψ ∧ ϕn.

So, for G : Σ^{Σ^{X}} and ψ : ΣX, define

F = Iψ,  ψ = λx. F (ix),  F = G · Σ^{i} and G = λϕ. F(Iϕ).

Then Gψ = (λϕ. F(Iϕ))(λx. F (ix))

= F(I(λx. F (ix)))
= ∃L. FA_{L} ∧ ∀ℓ ∈ L. I(λx. F (ix))β^{ℓ}  Lemma 6.8
= ∃L. G(Σ^{i}A_{L}) ∧ ∀ℓ ∈ L. Iψβ^{ℓ}
= ∃L. Gγ_{L} ∧ D^{L}ψ

since the given formulae are γ_{L} = Σ^{i}A_{L} and D^{L} = ∀ℓ ∈ L. Iψβ^{ℓ}. □

Theorem 6.10 Every definable space has a lattice basis indexed by Fin(Finℕ), and is a Σ-split subspace of Σ^{ℕ}. □

Remark 6.11 This is a “normal form” theorem, and, like all such theorems, it can be misinterpreted. It is a bridge over which we may pass in either direction between λ-calculus and a discrete encoding of topology, not an intention to give up the very pleasant synthetic results that we saw in [C]. In particular, we make no suggestion that either arguments in topology or their computational interpretations need go via the list or subset representation (though [13] seems to have this in mind). Indeed, subsets may instead be represented by λ-terms [E]. It is a simply a method of proof, and is exactly what we need to connect synthetic abstract Stone duality with the older lattice-theoretic approaches to topology, as we shall now show.

7 Basic corollaries

Making use of the availability of bases for all definable spaces, this section establishes the basic properties that justify the claim that abstract Stone duality is an account of domain theory and general topology, at least in so far as its morphisms are continuous functions. We first prove something that was claimed in Remark 2.16.

Proposition 7.1 Let M be an overt discrete space with effective basis (β^{n}, A_{n}) indexed by an overt discrete space N. Then M is the subquotient of N by an open partial equivalence relation. Proof Write n ⊩ x for n : N, x : M ⊢ A_{n}{x} ∧ β^{n}x (using discreteness of M) and N′ = {n | ∃x. n ⊩ x} ⊂ N, which is open, using overtness.

Then, using the basis expansion of open {x},

x : M ⊢ ⊤ = (x =_{M} x) = {x}(x) = ∃n. A_{n}{x} ∧ β^{n}x = ∃n. n ⊩ x,

so every point x : M has some code n : N′. The latter belongs only to x since

n ⊩ x ∧ n ⊩ y = A_{n}{x} ∧ β^{n}x ∧ A_{n}{y} ∧ β^{n}y
≤ A_{n}{x} ∧ β^{n}y
≤ (∃n. A_{n}{x} ∧ β^{n})y
= {x}y = (x =_{M} y).

Hence N′ → Σ^{M} by n ↦ λx. n ⊩ x factors through {} : M Σ^{M}, and M is N/∼ where m ∼ n iff ∃x. m ⊩ x ∧ n ⊩ x [C]. □

Corollary 7.2 Every definable overt discrete space is a subquotient of ℕ by an open partial equivalence relation. □

This does not restrict how “big” overt discrete objects can be in general models of ASD, for example ℵ_{1} still belongs to the classical model. It simply says that, having required certain base types to be overt discrete, as we did with ℕ, the additional overt discrete types that can be defined from them are no bigger. We leave it to the reader to define partial equivalence relations on List(N) whose quotients are List(M) and K(M).

Corollary 7.3 In the free model, if X has a basis indexed by any overt discrete space M then it has one indexed by ℕ. Proof Let n : ℕ, m : M ⊢ n ⊩ m be the relation defined in the Proposition and (β^{m}, A_{m}) the basis on X. Define

γ^{n} = λx. ∃m. n ⊩ m ∧ β^{m}x and D_{n} = λϕ. ∃m. n ⊩ m ∧ A_{m}ϕ

so γ^{n} = β^{m} and D_{n} = A_{m} if n ⊩ m, but γ^{n} = ⊥ and D_{n} = ⊥ if n ∉ N′. Then, using the properties of ⊩,

∃n. D_{n}ϕ ∧ γ^{n}x = ∃nmm′. n ⊩ m ∧ A_{m}ϕ ∧ n ⊩ m′ ∧ β^{m′}x
= ∃m. A_{m}ϕ ∧ β^{m}x = ϕx

so (γ^{n}, D_{n}) is an effective basis. □

The next goal is Scott continuity, i.e. preservation of directed joins. Recall from Definition 2.21 that these are defined in terms of a structure (S, 0, +) that indexes two families

s : S ⊢ α_{s} : Σ and ϕ^{s} : Σ^{X}.

Lemma 7.4 Γ, ℓ : Fin(M) ⊢ (∀m ∈ ℓ. ∃s:S. α_{s} ∧ ϕ^{s}m) = (∃s:S. α_{s} ∧ ∀m ∈ ℓ. ϕ^{s}m). Proof We have to show ≤, as ≥ is easy. For the base case, ℓ = 0, put s = 0. For the induction step, ℓ′ = m :: ℓ, suppose by the induction hypothesis^{6} that

α_{t} ∧ ϕ^{t}m ∧ α_{s} ∧ ∀m ∈ ℓ. ϕ^{s}m

6Since this equational hypothesis [E, §2] is of the form σ = ⊤, it can be eliminated in favour of an open subspace of the context.

Put u = s + t : S, so α_{u} = α_{s+t} = α_{s} ∧ α_{t} and ϕ^{s}, ϕ^{t} ≤ ϕ^{u}, so we have α_{u} ∧ ∀m ∈ m :: ℓ. ϕ^{u}m. □

Lemma 7.5 Any Γ ⊢ F : Σ^{3}N preserves the directed join Γ ⊢ ∃s. α_{s} ∧ F^{s} : Σ^{Σ^{N}}. Proof Using the previous lemma for X = Σ^{N} and M = FinN, and also the basis expansion of F (Lemma 6.8),

F(∃s. α_{s} ∧ F^{s}) = ∃L. FA_{L} ∧ ∀ℓ ∈ L. ∃s. α_{s} ∧ F^{s}β^{ℓ}
= ∃L. FA_{L} ∧ ∃s. α_{s} ∧ ∀ℓ ∈ L. F^{s}β^{ℓ}
= ∃s. α_{s} ∧ ∃L. FA_{L} ∧ ∀ℓ ∈ L. F^{s}β^{ℓ}
= ∃s. α_{s} ∧ FF^{s}  □

Theorem 7.6 Any Γ ⊢ G : Σ^{Σ^{X}} preserves the directed join ∃s. α_{s} ∧ ϕ^{s} : Σ^{X}. Proof Making the same substitutions as in Lemma 6.9,

G(∃s. α_{s} ∧ ϕ^{s}) = F · I(∃s. α_{s} ∧ Σ^{i}F^{s})
= (F · I · Σ^{i})(∃s. α_{s} ∧ F^{s})
= ∃s. α_{s} ∧ (F · I · Σ^{i})F^{s}
= ∃s. α_{s} ∧ Gϕ^{s}  □

Corollary 7.7 All F : Σ^{Y} → Σ^{X} preserve directed joins. □

We can now see the construction in Lemma 6.9 as a composite, of Lemma 6.4 twice and the following result. In order to apply F : Σ^{Σ^{X}} to the basis decomposition of ϕ : Σ^{X}, the decomposition must be a directed join.

Lemma 7.8 If X has a ∨-basis then Σ^{X} has a prime ∧-basis. Proof For F : Σ^{Σ^{X}} and ϕ : Σ^{X},

F ϕ = F (∃n. A_{n}ϕ ∧ β^{n}) = ∃n. A_{n}ϕ ∧ F β^{n}.

This is the decomposition of F with respect to the prime ∧-basis with

B^{n} ≡ A_{n} and A_{n} ≡ λF. F β^{n}.

Notice that it reverses the imposed order on the indexing object. □ We can also go up to the second exponential with just one level of lists.

Lemma 7.9 Let (β^{n}, A_{n}) be a ∨-basis for X. Then

B^{ℓ} ≡ λF. ∀n ∈ ℓ. F β^{n} and A_{ℓ} ≡ λF. F(λϕ. ∃n ∈ ℓ. A_{n}ϕ)

define an effective basis for Σ^{Σ^{X}}, i.e. we have a basis decomposition

F : Σ^{3}X ⊢ F = λF. ∃ℓ. F(λϕ. ∃n ∈ ℓ. A_{n}ϕ) ∧ ∀n ∈ ℓ. F β^{n}.

Proof (A_{n}, λF. F β^{n}) is a basis and (λϕ. ∃n ∈ ℓ. A_{n}ϕ, λF. ∀n ∈ ℓ. F β^{n}) an ∨-basis for Σ^{X} by Lemmas 7.8 and 6.4. Finally, Lemma 7.8 gives the prime ∧-basis for Σ^{Σ^{X}}. □

As a corollary, we have another result similar to Corollary 7.2, although this one does restrict the size of overt discrete compact objects. Such spaces are called Kuratowski finite [E].

Theorem 7.10 A space N is overt discrete compact iff it is listable, and therefore a quotient of a numeral by an open equivalence relation. Proof Expanding the quantifier ∀_{N} using the filter ∨-basis for N indexed by ListN,

∀_{N}ϕ = ∃ℓ. ∀n. n ∈ ℓ ∧ ∀m ∈ ℓ. ϕm,

so ⊤ = ∀_{N}⊤ = ∃ℓ. ∀n. n ∈ ℓ. The list is ℓ, though we require the Existence Property (cf. Remark 2.19) to pin down its order and so make it a quotient of a numeral. □

As another corollary, we can complete the business of Proposition 3.10 and Lemma 6.2.

Theorem 7.11 Let A : Σ^{Y} → Σ^{X} and B : Σ^{V} → Σ^{U}.

(a) If A and B both preserve ⊤ and ∧ then the squares

Σ^{X} ^{A} Σ^{Y}  X  \overline{Â ×} Y

Σ^{U} Σ^{X×U} ^{AU} Σ^{Y ×U}  X × U \overline{\begin{matrix}A × U \\ × \end{matrix}} Y × U  U

?  ?

[figure: Σ^{V}; B; Σ^{X×V}; B^{X}; A^{V}; Σ^{Y ×V}; B^{Y}; X × V; \begin{aligned}B × X \\ & × \end{aligned}; \overline{\begin{matrix}A × V \\ × \end{matrix}}; Y × V; \begin{matrix}B × Y \\ × \end{matrix}; V; B̂ ; ×]

commute. Hence × is a symmetric monoidal structure in the category whose objects are those of S and whose morphisms Â : X → Y are such A, cf. [A, Section 3]. In particular, these maps commute with ∀_{K}, for any compact K.

(b) If instead A and B both preserve ⊥ and ∨ then again the squares commute, so × is a symmetric monoidal structure in that category too, and these maps commute with ∃_{N}, for any overt N.

Proof Lemma 6.2 and Theorem 7.6. □

Corollary 7.12 Closed and compact subspaces coincide in any compact Hausdorff space, whilst open and overt ones agree in any overt discrete space. □

Next we consider homomorphisms of all four lattice connectives. As they also preserve directed joins, we might expect them to be frame homomorphisms, but we can only show that they preserve joins indexed by overt discrete objects, not “arbitrary” ones. On the other hand, spaces and inverse image maps are defined in Abstract Stone Duality as algebras and homomorphisms for the monad corresponding to Σ^{(−)} ⊣ Σ^{(−)}, rather than for an infinitary algebraic theory. We actually consider “Curried” homomorphisms.

Definition 7.13 The term Γ ⊢ P : Σ^{Σ^{X}} is prime [A, Definition 8.1] if

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

Axiom 2.3(b) says that we may then introduce a = focus P such that P = λϕ. ϕa.

We know that that frame homomorphisms (as defined externally using infinitary lattices) agree with Eilenberg–Moore homomorphisms in the case of the classical models [A, B]. Now we can use bases to prove a similar result for the internal finitary lattice structure in our category. This means that we can import at least some of the familiar lattice-theoretic arguments about topology into our category.

Theorem 7.14 If Γ ⊢ P : Σ^{Σ^{X}} is prime iff it preserves ⊤, ⊥, ∧ and ∨. Proof [⇒] Put F = λF. F ϕ ∧ F ψ, so FP = P ϕ ∧ P ψ, whilst

P (λx. F(λϕ. ϕx)) = P (λx. ϕx ∧ ψx) = P (ϕ ∧ ψ).

The other connectives are handled in the same way.

[⇐] First note that, using Axiom 2.4 for P and α,

P (α ∧ ϕ) = P ⊥ ∨ α ∧ P ϕ = α ∧ P ϕ.

Then FP = ∃ℓ. F(λϕ. ∃n ∈ ℓ. A_{n}ϕ) ∧ ∀n ∈ ℓ. P β^{n}  Lemma 7.9

= ∃ℓ. F(λϕ. ∃n ∈ ℓ. A_{n}ϕ) ∧ P (∀n ∈ ℓ. β^{n})  P preserves ∧, ⊤
= ∃ℓ. P (F(λϕ. ∃n ∈ ℓ. A_{n}ϕ) ∧ ∀n ∈ ℓ. β^{n})  above
= P (∃ℓ. F(λϕ. ∃n ∈ ℓ. A_{n}ϕ) ∧ ∀n ∈ ℓ. β^{n}) P preserves ⊥, ∨, ∃
= P (F(λϕ. ϕ)).  Lemma 7.9 □

Corollary 7.15 H : Σ^{X} → Σ^{Y} is an Eilenberg–Moore homomorphism iff it is a lattice homomorphism. In this case, it is of the form H = Σ^{f} for some unique f : Y → X. □

We have in particular a way of introducing points of a space by finitary lattice-theoretic arguments. By this method we can derive a familiar domain-theoretic result, but beware that, as the objects of our category denote locally compact spaces and not merely domains, such order-theoretic results by no means characterise the objects and morphisms.

Theorem 7.16 Every object has and every morphism preserves directed joins. Proof Let Γ, s : S ⊢ a_{s} : X be a directed family in X with respect to the intrinsic order (Definition 2.5), then

Γ, s : S ⊢ λϕ. ϕa_{s} : Σ^{Σ^{X}}

is a directed family of primes. But primes are characterised lattice-theoretically, and the property is preserved by directed joins (Theorem 7.6 for F), so

Γ ⊢ P ≡ λϕ. ∃s. ϕa_{s}

is also prime, and P = λϕ. ϕa for some unique a : X.

I claim that this is the join of the given family. By Definition 2.5, the order relation a_{s} ≤_{X} a means λϕ. ϕa_{s} ≤ λϕ. ϕa ≡ P, which we have by the definition of P, whilst similarly if Γ, s : S ⊢ a_{s} ≤ b then λϕ. ϕa_{s} ≤ λϕ. ϕb so P ≤ λϕ. ϕb as P is the join, and then a ≤ b.

By a similar argument, given f : X → Y, we have f(a_{s}) ≤_{Y} fa since ψ : Σ^{Y} provides ψ·f : Σ^{X}, and if f(a_{s}) ≤ b then f(a) ≤ b, so f preserves the join. □

Finally, we show that the equations in Lemma 5.12 that characterised the Scott-continuous functions E that are of the form I ·Σ^{i} for a Σ-split sublocale are also valid for subspaces in abstract Stone duality.

Definition 7.17 Recall from [B, Definition 4.3] that E : Σ^{X} → Σ^{X} is called a nucleus if

F : Σ^{3}X ⊢ E(λx. F(λϕ. Eϕx)) = E(λx. F(λϕ. ϕx)).

(This equation arises from Beck’s monadicity theorem, and is applicable without assuming any lattice structure on Σ.)

Lemma 7.18 If E is a nucleus then

ϕ, ψ : Σ^{X} ⊢ E(ϕ ∧ ψ) = E(Eϕ ∧ Eψ) and E(ϕ ∨ ψ) = E(Eϕ ∨ Eψ).

Proof Putting F ≡ λF. F ϕ ∧ F ψ,

E(λx. F(λϕ. ϕx)) = E(λx. ϕx ∧ ψx) = E(ϕ ∧ ψ)
E(λx. F(λϕ. Eϕx)) = E(λx. Eϕx ∧ Eψx) = E(Eϕ ∧ Eψ),

are equal. The argument for ∨ is the same. □

For the converse, first observe that the equations allow us to insert or remove Es as we please in any sub-term of a lattice expression, so long as E is applied to the whole expression. In particular, Eϕ = E(Eϕ) and E(ϕ ∨ ψ ∨ θ) = E(Eϕ ∨ Eψ ∨ θ) (sic).

Lemma 7.19 Although we needn’t have E⊤ = ⊤ or E⊥ = ⊥, we may extend the binary ∨-formula to finite (possibly empty) sets ℓ : Fin(N):

E(∃n ∈ ℓ. α_{n} ∧ ϕ^{n}) = E(∃n ∈ ℓ. α_{n} ∧ Eϕ^{n}),

where n : N ⊢ α_{n} : Σ and ϕ^{n} : Σ^{X}. Similarly but more simply, from the ∧-equation,

E(∀n ∈ ℓ. ϕ^{n}) = E(∀n ∈ ℓ. Eϕ^{n}).

Proof The base case of the induction, ℓ = 0, is E⊥ = E⊥. For the induction step^{7},

E(∃n ∈ m :: ℓ. α_{n} ∧ ϕ^{n})
= E((∃n ∈ ℓ. α_{n} ∧ ϕ^{n}) ∨ (α_{m} ∧ ϕ^{m}))
= E(E(∃n ∈ ℓ. α_{n} ∧ ϕ^{n}) ∨ E(α_{m} ∧ ϕ^{m}))  ∨-equation
= E(E(∃n ∈ ℓ. α_{n} ∧ Eϕ^{n}) ∨ E(α_{m} ∧ ϕ^{m}))  induction hypothesis
= E(E(∃n ∈ ℓ. α_{n} ∧ Eϕ^{n}) ∨ E⊥ ∨ (α_{m} ∧ Eϕ^{m}))  Phoa wrt α_{m}
= E((∃n ∈ ℓ. α_{n} ∧ Eϕ^{n}) ∨ ⊥ ∨ (α_{m} ∧ Eϕ^{m}))  above
= E(∃n ∈ m :: ℓ. α_{n} ∧ Eϕ^{n})  □

Lemma 7.20 The ∃ equation extends by Scott continuity (Proposition 7.6).

Proof E(∃n:N . α_{n} ∧ ϕ^{n}) = E(∃ℓ:FinN . ∃n ∈ ℓ. α_{n} ∧ ϕ^{n})

= ∃ℓ. E(∃n ∈ ℓ. α_{n} ∧ ϕ^{n})  Proposition 7.6
= ∃ℓ. E(∃n ∈ ℓ. α_{n} ∧ Eϕ^{n})  Lemma 7.19
= E(∃n:N . α_{n} ∧ Eϕ^{n})  similarly □

Theorem 7.21 E is a nucleus iff it satisfies

ϕ, ψ : Σ^{X} ⊢ E(ϕ ∧ ψ) = E(Eϕ ∧ Eψ) and E(ϕ ∨ ψ) = E(Eϕ ∨ Eψ).

Proof We expand F : Σ^{3}X in the defining equation for a nucleus

E(λx. F(λϕ. Eϕx)) = E(∃L. FA_{L} ∧ ∀ℓ ∈ L. Eβ^{ℓ})  Proposition 7.8
= E(∃L. FA_{L} ∧ E(∀ℓ ∈ L. Eβ^{ℓ}))  Lemma 7.20
= E(∃L. FA_{L} ∧ E(∀ℓ ∈ L. β^{ℓ}))  Lemma 7.19
= E(∃L. FA_{L} ∧ ∀ℓ ∈ L. β^{ℓ})  Lemma 7.20
= E(λx. F(λϕ. ϕx))  Proposition 7.8 □

Notice that a nucleus E in our sense with E ≥ id is the same thing as a nucleus in the sense of locale theory (usually called j) that is Scott-continuous.

8 The way-below relation

Recall from Definition 1.13(b) and the lemmas that followed it that any continuous distributive lattice carries a binary relation (written ≪ and called “way-below”) such that

⊥ ≪ γ  α ≪ γ β ≪ γ ; = ; α ∨ β ≪ γ  {α′ ≤ α ≪ β ≤ β′ \atop α′ ≪ β′}  α ≪ γ ; = ; ∃β. α ≪ β ≪ γ

{α ≪ β β ≪ ϕ β ≪ ψ \atop α ≪ (ϕ ∧ ψ)}  α ≪ β ∨ γ ; = ; ∃β′γ′. α ≪ β′ ∨ γ′ β′ ≪ β γ′ ≪ γ

In this section we introduce a new binary relation ≺ ≺ with analogous properties to these, but defined on the indexing set N of an ∨-basis (β^{n}, A_{n}) for X, not on Σ^{X}.

Notation 8.1 We write n ≺ ≺ m for n, m : N ⊢ A_{n}β^{m} : Σ. This is an open binary relation on the overt discrete space N of indices, not on the lattice Σ^{X}. It is an “imposed” structure on N in the sense of Remark 2.13.

Examples 8.2 (Not all of these are ∨-bases.)

7This use of equational hypotheses in the context [E, §2] is apparently unavoidable.

(a) Let β^{n} classify U^{n} ⊂ X, and A_{n} = λϕ. (K^{n} ⊂ ϕ) in a locally compact sober space. Then n ≺ ≺ m means that K^{n} ⊂ U^{m}. This is consistent with Notation 1.3 if we identify the basis element n with the pair (U^{n} ⊂ K^{n}).

(b) Let A_{n} = λϕ. (β^{n} ≪ ϕ) in a continuous lattice. Then n ≺ ≺ m means that β^{n} ≪ β^{m}, cf. Definition 1.15.

(c) In the interval basis on ℝ in Example 4.9, ⟨q, δ⟩ ≺ ≺ ⟨p, ϵ⟩ means that [q, δ] ⊂ (p, ϵ), i.e. p − ϵ < q − δ ≤ q + δ < p + ϵ.

(d) In the basis of disjoint pairs of opens, (U^{n} ∩̸ V_{n}), for a compact Hausdorff space in Example 4.10, n ≺ ≺ m means that V_{n} ∪ U^{m} = X.

(e) In the prime basis ({n}, ηn) for N (Example 4.5(a)), n ≺ ≺ m just when n = m.

(f) In the Fin(N)-indexed filter ∨-basis on N (Proposition 6.7), ℓ ≺ ≺ ℓ′ iff ℓ ⊂ ℓ′.

(g) In the prime ∧-basis on Σ^{N} (Example 4.5(b)), on the other hand, ℓ ≺ ≺ ℓ′ iff ℓ′ ⊂ ℓ.

(h) More generally, in the prime ∧-basis on Σ^{X} derived from an ∨-basis on X (Lemma 7.8), (n ≺ ≺_{Σ^{X}} m) iff (m ≺ ≺_{X} n).

(i) In the Fin(Fin(N))-indexed filter lattice basis on Σ^{N} (Proposition 6.7),

L ≺ ≺ R ≡ A_{L}B^{R} = R ⊂^{♯} L ≡ ∀ℓ ∈ L. ∃ℓ′ ∈ R. (ℓ′ ⊂ ℓ),

where R ⊂^{♯} L is known as the upper order on subsets induced by the relation ⊂ on elements.

(j) In the prime ∧-basis on Σ^{Σ^{N}} (Lemma 6.8), L ≺ ≺ R iff L ⊂^{♯} R.

(k) In the basis on Σ^{Σ^{X}} derived from an ∨-basis on X (Lemma 7.9), (ℓ ≺ ≺_{Σ^{2}X} ℓ′) iff (ℓ ≺ ≺^{♯}_{X} ℓ′).

(l) We shall see that any stably locally compact object X has a filter lattice basis (N, 0, 1, +, ⋆, ≺ ≺) such that the opposite (N, 1, 0, ⋆, +, ≻ ≻) is the basis of another such space, known as its Lawson dual.

Our first result just restates the assumption of an ∨-basis, cf. Lemmas 1.9 and 1.18:

Lemma 8.3 0 ≺ ≺ p, whilst if both n ≺ ≺ p and m ≺ ≺ p then n + m ≺ ≺ p. Proof A_{0} = λϕ. ⊤ and A_{n+m}β^{p} = A_{n}β^{p} ∧ A_{m}β^{p}. □

In a continuous lattice, α ≪ β implies α ≤ β, but we have no similar property relating ≺ ≺ to ≼. We shall see the reasons for this in the next section. But we do have two properties that carry most of the force of α ≪ β ⇒ α ≤ β. We call them roundedness. The second also incorporates many of the uses of directed joins and Scott continuity into a notation that will become increasingly more like discrete mathematics than it resembles the technology of traditional topology.

Lemma 8.4 β^{n} = ∃m. (m ≺ ≺ n) ∧ β^{m} and A_{m} = ∃n. A_{n} ∧ (m ≺ ≺ n). Proof The first is simply the basis expansion of β^{n}. For the second, we apply A_{m} to the basis expansion of ϕ, so

A_{m}ϕ = ∃n. A_{n}ϕ ∧ A_{m}β^{n} = (∃n. A_{n} ∧ A_{m}β^{n})ϕ,

since A_{n} preserves directed joins (Theorem 7.6). □

Corollary 8.5 If m ≺ ≺ n then β^{m} ≤ β^{n} and A_{m} ≥ A_{n}. □

Corollary 8.6 If m ≺ ≺ n, A_{m′} ≥ A_{m} and β^{n} ≤ β^{n′}, then m′ ≺ ≺ n′. Proof (m ≺ ≺ n) ≡ A_{m}β^{n} ≤ A_{m′}β^{n′} ≡ (m′ ≺ ≺ n′). □

Corollary 8.7 The relation ≺ ≺ satisfies transitivity and the interpolation lemma:

(m ≺ ≺ n) = (∃k. m ≺ ≺ k ≺ ≺ n).

Proof A_{m}β^{n} = (∃k. A_{k} ∧ k ≺ ≺ m)β^{n} = ∃k. A_{k}β^{n} ∧ k ≺ ≺ m. □

Now we consider the interaction between ≺ ≺ and the lattice structures (⊤, ⊥, ∧, ∨) and (1, 0, +, ⋆). Of course, to discuss ∧ and ⋆, we need a lattice basis.

Lemma 8.8 As directed joins,

ϕ ∧ ψ = ∃pq. β^{p⋆q} ∧ A_{p}ϕ ∧ A_{q}ψ and ϕ ∨ ψ = ∃pq. β^{p+q} ∧ A_{p}ϕ ∧ A_{q}ψ.

Proof The first is distributivity, since β^{p⋆q} = β^{p} ∧ β^{q}.

The second uses Lemma 2.24: we obtain the expression

ϕ ∨ ψ = ∃p. A_{p}ϕ ∧ (β^{p} ∨ ψ)

from the basis expansion ϕ = ∃p. A_{p}ϕ ∧ β^{p} by adding ψ to the 0th term (since A_{0}ϕ = ⊤ and β^{0} = ⊥) and, harmlessly, A_{p}ϕ ∧ ψ to the other terms. Similarly,

β^{p} ∨ ψ = ∃q. A_{q}ψ ∧ (β^{p} ∨ β^{q}) = ∃q. A_{q}ψ ∧ β^{p+q}.

The joins are directed because because A_{0}ϕ ∧ A_{0}ψ = ⊤ and

(A_{p_{1}}ϕ ∧ A_{q_{1}}ψ) ∧ (A_{p_{2}}ϕ ∧ A_{q_{2}}ψ) = (A_{p_{1}+p_{2}}ϕ ∧ A_{q_{1}+q_{2}}ψ).  □

Lemma 8.9 For a lattice basis, A_{n}⊤ = (n ≺ ≺ 1), A_{n}⊥ = (n ≺ ≺ 0) and

A_{n}(ϕ ∧ ψ) = ∃pq. (n ≺ ≺ p ⋆ q) ∧ A_{p}ϕ ∧ A_{q}ψ
A_{n}(ϕ ∨ ψ) = ∃pq. (n ≺ ≺ p + q) ∧ A_{p}ϕ ∧ A_{q}ψ

Proof The first two are A_{n}β^{1} and A_{n}β^{0}. The other two are ∃pq. A_{n}(β^{p⋆q}) ∧ A_{p}ϕ ∧ A_{q}ψ and ∃pq. A_{n}(β^{p+q}) ∧ A_{p}ϕ ∧ A_{q}ψ, which are A_{n} applied to the directed joins in Lemma 8.8. □

Lemma 8.10 The lattice basis (β^{n}, A_{n}) is a filter basis iff 1 ≺ ≺ 1 and

m ≺ ≺ p ⋆ q = m ≺ ≺ p m ≺ ≺ q

Proof (n ≺ ≺ 1) = A_{n}β^{1} = A_{n}⊤, but recall that n ≺ ≺ 1 for all n iff 1 ≺ ≺ 1.

The displayed rule is A_{m}β^{p} ∧ A_{m}β^{q} = A_{m}β^{p⋆q} ≡ A_{m}(β^{p} ∧ β^{q}). Given this, by distributivity and Lemma 8.9,

A_{m}ϕ ∧ A_{m}ψ = ∃pq. A_{p}ϕ ∧ A_{q}ψ ∧ A_{m}β^{p} ∧ A_{m}β^{q}
= ∃pq. A_{p}ϕ ∧ A_{q}ψ ∧ (m ≺ ≺ p) ∧ (m ≺ ≺ q)
= ∃pq. A_{p}ϕ ∧ A_{q}ψ ∧ (m ≺ ≺ p ⋆ q)
= A_{m}(ϕ ∧ ψ)  □

If we don’t have a filter basis, we have to let n “slip” by n ≺ ≺ m, cf. Lemma 1.20.

Lemma 8.11 For any lattice basis,

n ≺ ≺ p ⋆ q

=

n ≺ ≺ m  m ≺ ≺ p  m ≺ ≺ q

Proof Downwards, interpolate n ≺ ≺ m ≺ ≺ p⋆q ≼ p, q, then m ≺ ≺ p, q by monotonicity. Conversely, using Corollary 8.5, if A_{n}β^{m} = ⊤ and β^{m} ≤ β^{p⋆q} then A_{n}β^{p⋆q} = ⊤. □

The corresponding result for ∨ is our version of the Wilker property, cf. Proposition 1.10 and Lemma 1.19.

Lemma 8.12 n ≺ ≺ p + q

= ∃p′q′. (n ≺ ≺ p′ + q′) ∧ (p′ ≺ ≺ p) ∧ (q′ ≺ ≺ q)

Proof Lemma 8.9 with ϕ = β^{p} and ψ = β^{q}. □

We shall summarise these rules in Definition 10.1.

Jung and Sünderhauf [15, Section 5] used a very similar system of rules that they call a strong proximity lattice to characterise stably locally compact spaces. Their axioms are lattice dual, and in particular they prove the dual Wilker property (Corollary 3.18), albeit using Choice. If (N, 0, 1, +, ⋆, ≺ ≺) is an abstract basis satisfying these axioms then so too is (N, 1, 0, ⋆, +, ≻ ≻). The corresponding space, which is known as the Lawson dual, classically has the same points as the given one, but the opposite specialisation order, whilst the open subspaces of one correspond to the compact saturated subspaces of the other.

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

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

p ⋆ q ≺ ≺ n = ∃p′q′. (p′ ⋆ q′ ≺ ≺ n) ∧ (p ≺ ≺ p′) ∧ (q ≺ ≺ q′).

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

A_{p×q} ≡ ∃p′q′. A_{p′⋆q′} ∧ (p ≺ ≺ p′) ∧ (q ≺ ≺ q′).

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

A_{p×q}⊤  = ∃p′q′. A_{p′⋆q′}⊤ ∧ (p ≺ ≺ p′) ∧ (q ≺ ≺ q′)
≥ (p ≺ ≺ 1) ∧ (q ≺ ≺ 1) = ⊤
A_{p×q}ϕ ∧ A_{p×q}ψ = ∃p′q′p′′q′′. A_{p′⋆q′}ϕ ∧ A_{p′′⋆q′′}ψ
∧(p ≺ ≺ p′) ∧ (p ≺ ≺ p′′) ∧ (q ≺ ≺ q′) ∧ (q ≺ ≺ q′′)
≤ ∃p′′′q′′′. A_{p′′′⋆q′′′}ϕ ∧ A_{p′′′⋆q′′′}ψ
∧(p ≺ ≺ p′′′) ∧ (q ≺ ≺ q′′′)  p′′′ = p′ ⋆ p′′, q′′′ = q′ ⋆ q′′
= ∃p′q′. A_{p′⋆q′}(ϕ ∧ ψ) ∧ (p ≺ ≺ p′) ∧ (q ≺ ≺ q′)  filter basis
= A_{p×q}(ϕ ∧ ψ)
A_{p×q} = ∃p′′q′′. A_{p′′⋆q′′} ∧ (p ≺ ≺ p′′) ∧ (q ≺ ≺ q′′) interpolation
= ∃p′q′p′′q′′. A_{p′′⋆q′′} ∧ (p ≺ ≺ p′ ≺ ≺ p′′) ∧ (q ≺ ≺ q′ ≺ ≺ q′′)
= ∃p′q′. A_{p′×q′} ∧ (p ≺ ≺ p′) ∧ (q ≺ ≺ q′)

We deduce the dual Wilker property by applying the last equation to β^{n}. The new operation can be defined for longer lists in the same way, and we extend this to a new lattice basis as we did in Lemma 6.4ff. □

There are special results that we have in the cases of overt and compact spaces. We already know that 1 ≺ ≺ 1 iff the space is compact (cf. Lemma 4.3), but the lattice dual characterisation of overtness cannot be 0 ≺ ≺ 0, as that always happens.

Lemma 8.14 If X is overt then

(n ≺ ≺ m) ≤ (n ≺ ≺ 0) ∨ (∃y. β^{m}y) but (n ≺ ≺ 0) ∧ (∃x. β^{n}x) = ⊥.

Proof ϕx ≤ ∃y. ϕy so, using the Phoa principle (Axiom 2.4),

A_{n}ϕ ≤ A_{n}(λx. ∃y. ϕy) = A_{n}⊥ ∨ ∃y. ϕy ∧ A_{n}⊤ ≤ (n ≺ ≺ 0) ∨ ∃y. ϕy.

Putting ϕ = β^{m}, (n ≺ ≺ m) ≡ A_{n}β^{m} ≤ (n ≺ ≺ 0) ∨ ∃y. β^{m}y,

whilst ⊥ = ∃x. β^{0}x = (n ≺ ≺ 0) ∧ ∃x. β^{n}x  □

By a similar argument, we have Johnstone’s “Townsend–Thoresen Lemma” [10],

(n ≺ ≺ p + q) ≤ (n ≺ ≺ p) ∨ (∃y. β^{q}y).

Corollary 8.15 Given a compact overt space, it’s decidable whether it’s empty or inhabited, cf. Corollary 3.7. Proof (1 ≺ ≺ 1) ≤ (1 ≺ ≺ 0) ∨ (∃x. ⊤), but (1 ≺ ≺ 0) = A_{1}β^{0} = (∀x. ⊥). □

The following two sections are devoted to proving that the rules above for ≺ ≺ are complete, in the sense that from any abstract basis (N, 0, 1, +, ⋆, ≺ ≺) satisfying them we may recover an object of the category. This proof is very technical, so we first consider a special case, namely the characterisation of the objects that have prime bases in our sense, and are continuous dcpos in the classical model.

Definition 8.16 An filtered interpolative relation n, m : N ⊢ (n ◁ m) : Σ on an overt discrete object is an open relation that satisfies:

(a) transitivity and interpolation: n, m : N ⊢ (n ◁ m) = ∃k. (n ◁ k) ∧ (k ◁ m);

(b) extrapolation: n : N ⊢ ∃t. (n ◁ t);

(c) filteredness: n, r, s : N ⊢ (n ◁ r) ∧ (n ◁ s) = ∃t. (t ◁ r) ∧ (t ◁ s) ∧ (n ◁ t). A rounded filter for (N, ◁) is a predicate Γ ⊢ ψ : Σ^{N} that is

(a) rounded: Γ, m : N ⊢ ψm = ∃n. (n ◁ m) ∧ ψn;

(b) inhabited: Γ ⊢ ∃n. ψn = ⊤;

(c) filtered: Γ, r, s : N ⊢ ψr ∧ ψs ≤ ∃t. ψt ∧ (t ◁ r) ∧ (t ◁ s).

Lemma 8.17 If X has an N-indexed prime basis, so

ϕx = ∃n. ϕp_{n} ∧ β^{n}x,

then ≺ ≺ is a filtered interpolative relation and x : X ⊢ ψ ≡ λn. β^{n}x is a rounded filter. 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,

(a) the basis expansion of β^{n}p_{m} gives transitivity and interpolation, as in Corollary 8.7;

(b) that of (λx. ⊤)p_{m} gives extrapolation; whilst

(c) that of (β^{r} ∧ β^{s})p_{n} gives filteredness, as in Lemma 8.10. □

Beware that n ≺ ≺ m or n ◁ m means that β^{n} ≪ β^{m}, whereas A_{m} ≪ A_{n} and p_{m} ≪ p_{n}.

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

(a) Any open equivalence relation on an overt discrete object is filtered interpolative, and its rounded filters are the equivalence classes.

(b) Σ^{N} is the space of (ideals, i.e.) rounded filters for reverse inclusion in Fin(N).

(c) More generally, any reflexive transitive relation is filtered interpolative, and all filters are rounded. In this case the following result characterises algebraic dcpos. The idea of Lemma 4.3 may (perhaps) be adapted to identify the so-called finite or compact elements of the space, which form the image of a map N → X from an overt discrete space. However, N must be given alongside the algebraic dcpo X, for the same reasons as in Remark 2.7.

(d) If X has an N-indexed ∨-basis, Σ^{X} is the space of rounded filters for (N, ≻ ≻).

(e) A stronger notion of filteredness in which we require a meet r ⋆ s for any pair (r, s) with a lower bound n provides a class of spaces that includes the overt discrete ones and is closed under Σ^{(−)}, sums, products and retracts. □

Theorem 8.19 Any filtered interpolative relation (N, ◁) is the way-below relation for a prime basis on its space of rounded filters. Proof The space X will split the nucleus E on Σ^{N} defined by

F : Σ^{Σ^{N}} , ψ : Σ^{N} ⊢ EF ψ ≡ ∃n. F (↑ ↑ n) ∧ ψn,

where ↑ ↑ n ≡ λm. n ◁ m satisfies

(↑ ↑ n) = λm. ∃r. (n ◁ r ◁ m) = ∃r. (↑ ↑ r) ∧ (n ◁ r).

This union is directed^{8}, by the extrapolation and filterness conditions. By Theorem 7.6 we therefore have

F (↑ ↑ n) = ∃r. F (↑ ↑ r) ∧ (n ◁ r) ≡ EF (↑ ↑ n),

from which we deduce the equations for a nucleus in Theorem 7.21,

E(F ⊙ G)ψ ≡ ∃n. (F (↑ ↑ n) ⊙ G(↑ ↑ n)) ∧ ψn
≡ ∃n. (EF (↑ ↑ n) ⊙ EG(↑ ↑ n)) ∧ ψn
≡ E(EF ⊙ EG)ψ.

Remark 8.20 (Continuation of the proof). By [B, Section 8], we now have X ≡ {Σ^{N} | E} ^{i} Σ^{N}, into which ψ : Σ^{N} is admissible, i.e. of the form ix for some x ≡ admit ψ : X, if F : Σ^{Σ^{N}} ⊢ EF ψ = F ψ. Putting F ≡ λθ. θn, F ≡ λθ. ⊤ and F ≡ λθ. θr ∧ θs, we deduce that ψ is a rounded filter. Conversely, if ψ is a rounded filter then

F ψ ≡ ∃ℓ. F (λm. m ∈ ℓ) ∧ ∀m ∈ ℓ. ψm
= ∃n. ∃ℓ. ψn ∧ F (λm. m ∈ ℓ) ∧ ∀m ∈ ℓ. n ◁ m ≡ EF ψ,

where roundedness gives ≤ and filteredness gives ≥. Now I claim that

p_{n} ≡ admit(↑ ↑ n) and β^{n} ≡ λx. ixn ≡ Σ^{i}(λψ. ψn)

define a prime basis. First, ↑ ↑ n is admissible because ◁ is filtered interpolative. Since ψ = ix is admissible,

ϕx = Iϕ(ix) = E(Iϕ)(ix) = ∃n. Iϕ(↑ ↑ n) ∧ ixn
= ∃n. Iϕ(ip_{k}) ∧ β^{n}x
= ∃n. ϕp_{k} ∧ β^{n}x.

Finally, (n ≺ ≺ m) = A_{n}β^{m} = β^{m}p_{n} = i( admit(↑ ↑ n))m = (↑ ↑ n)m = (n ◁ m). □

General locally compact objects are a good deal more complicated than this. The proof relies heavily on the “lattice” structure (0, 1, +, ⋆), which we investigate next.

9 The lattice basis on Σ^{N}

In the next section we shall show that the properties of ≺ ≺ listed in the previous one are sufficient to reconstruct the space X and its basis. To do this, however, we need some more technical information about the lattice basis on Σ^{N}, and about the free distributive lattice on N.

Remark 9.1 When a space X has an an N-indexed basis (β^{n}, A_{n}) there is an embedding X Σ^{N}, given by Lemma 5.2. This structure may be summed up by the diagram,

[figure: Fin(FinN); B^{(−)}; Σ^{Σ^{N}}; E; Σ^{Σ^{N}}]

[figure: N; \begin{matrix}\{ \\ | & \begin{matrix}\{ \\ | & (−) & | \\ \} \end{matrix} & | \\ \} \end{matrix}; β^{(−)}; λϕ. ϕ(−); Σ^{X}; Σ^{i}; λn. A_{n}(−); I; Σ^{N}; J]

m ↦ ↓ ↓ m ≡ (λn. n ≺ ≺ m)

in which \begin{matrix}\{ \\ | & − & | \\ \} \end{matrix} means the singleton lists and the map J on the right is defined by

Jϕ ≡ λψ. ∃n. ϕn ∧ ψn

8It is directed in the existential sense of Definition 1.13(a), not in the canonical one of Definition 2.21 needed for Theorem 7.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 [F–].

and Jϕ preserves ∨, ⊥ and ∃. We shall construct E from ≺ ≺ using the lattice basis (B^{L}, A_{L}) on Σ^{N}.

Remark 9.2 These results may be seen as presentation of the algebra Σ^{X}. In this, N is the set of generators, and we have homomorphisms

[figure: Fin(FinN); B^{(−)}; Σ^{Σ^{N}}; Σ^{i}; Σ^{X}]

[figure: DL(N)]

as B^{(−)} takes the list operations + and ⋆ to the intrinsic structure ∨ and ∧ in Σ^{Σ^{N}}, whilst Σ^{i} preserves the latter in Σ^{X}. The relation ≺ ≺ encodes the system of “equations” that distinguishes the particular algebra Σ^{X} from the generic one Σ^{Σ^{N}} that is freely generated by N.

This explains why n ≺ ≺ m does not imply n ≼ m in our system, whereas α ≪ β implies α ≤ β in a continuous lattice. Topologically, we already saw the point in Remarks 1.8 and 4.14: many distinct codes may in principle represent the same open or compact subspace. To put this the other way round, since equality (or containment) of open subspaces is not computable, we cannot deduce equality (or comparison) of codes from semantic coincidence of subspaces.

Remark 9.3 The triangle

[figure: DL(N); B^{(−)}; Σ^{Σ^{N}}; N; λϕ. ϕ(−); \begin{matrix}\{ \\ | & \begin{matrix}\{ \\ | & − & | \\ \} \end{matrix} & | \\ \} \end{matrix}]

illustrates the comparison between the monad that captures the imposed (0, 1, +, ⋆) distributive lattice structure and the one in Axiom 2.3 based on Σ^{(−)} ⊣ Σ^{(−)}. The upward maps are the units of these monads. We leave the interested student to construct the multiplication map of the DL-monad as a list program, cf. flatten in Lemma 6.5.

We are not quite justified in saying that the Σ^{Σ^{(−)}} monad defines the intrinsic (⊥, ⊤, ∨, ∧) distributive lattice structure. Corollary 7.15 said that the homomorphisms are the same, but I have not been able to show that every object whose intrinsic order is that of a distributive lattice is an algebra for the monad, i.e. of the form Σ^{X} for some object X.

Notation 9.4 Recall from Proposition 6.7 that the basis on Σ^{N} is

B^{L}ϕ ≡ ∃ℓ ∈ L. ∀m ∈ ℓ. ϕm and A_{L}F = ∀ℓ ∈ L. F (λm. m ∈ ℓ),

from which we obtain the way-below relation

A_{L}B^{R} ≡ R ⊂^{♯} L ≡ ∀ℓ ∈ L. ∃ℓ′ ∈ R. (ℓ′ ⊂ ℓ).

The list of lists R+S is given by concatenation, whilst R⋆S and B^{R⋆S} were defined in Lemma 6.5.

Lemma 9.5 (B^{L}, A_{L}) is a lattice basis:

B^{1} = ⊤ B_{0} = ⊥ B^{R⋆S} = B^{R} ∧ B^{S} B^{R+S} = B^{R} ∨ B^{S}
A_{0}F = ⊤ A_{L}⊥ = (L = 0) A_{R+S} = A_{R} ∧ A_{S}.  □

Lemma 9.6 (B^{L}, A_{L}) is a filter basis: A⊤ = ⊤ and A_{L}(F ∧ G) = A_{L}F ∧ A_{L}G.

Proof A_{L}(F ∧ G) = ∀ℓ ∈ L. (F ∧ G)(λm. m ∈ ℓ)

= ∀ℓ ∈ L. F (λm. m ∈ ℓ) ∧ G(λm. m ∈ ℓ)
= (∀ℓ ∈ L. F (λm. m ∈ ℓ)) ∧ (∀ℓ ∈ L. G(λm. m ∈ ℓ))
= A_{L}F ∧ A_{L}G  □

The Wilker condition says that we can split the list into the two parts that satisfy the respective disjuncts.

Lemma 9.7 A_{L}(F ∨ G) = ∃L_{1}L_{2}. (L = L_{1} + L_{2}) ∧ A_{L_{1}}F ∧ A_{L_{2}}G. □

Proposition 9.8 We write L ≅ R if both R ⊂^{♯} L and L ⊂^{♯} R. This is an open congruence for the imposed structure on Fin(FinN), and the free imposed distributive lattice DL(N) is its quotient [C, Section 10]. □

Remark 9.9 So far we have not used any of the structure on N itself. Since we have a lattice basis for X, by definition

β^{(−)} : N → Σ^{X}

takes the imposed structure (0, 1, +, ⋆) on N to the intrinsic structure (⊥, ⊤, ∨, ∧) on Σ^{X}. Associated with this imposed structure is an imposed order relation ≼, which β^{(−)} takes to ≤, but with respect to which the dual basis A_{(−)} is contravariant.

Definition 9.10 We define ≼ from + and ⋆ as the least relation such that

0 ≼ n ≼ n ≼ 1 (k ⋆ n) + (k ⋆ m) ≼ k ∗ (n + m)
{n ≼ k ≼ m \atop n ≼ m}  k ≼ m k ≼ n ; = ; k ≼ m ⋆ n  n ≼ k m ≼ k ; = ; n + m ≼ k

and again we write n ≅ m when both n ≼ m and m ≼ n.

Proposition 9.11 The relation ≅ is an open congruence on N whose quotient is an imposed distributive lattice. □

Notation 9.12 Returning to Fin(FinN), L is regarded as a formal sum of products of elements of N (additive normal form). This may be “evaluated” by means of the operation

ev : Fin(FinN) → N.

This is defined for lists by a generalisation of Lemma 6.5. A similar construction works for K-finite subsets instead, except that then N has actually to satisfy the equations for a distributive lattice up to equality, and not just up to ≅ (cf. Notation 2.17). The map

DL(N) ≡ Fin(FinN)/(≅) ^{ev/(≅)} N/(≅)

is the structure map of the distributive lattice, regarded as an algebra for the DL-monad.

Proposition 9.13 The map ev : Fin(FinN) → N is a homomorphism in the sense that ev0 = 0 and ev1 = 1 by construction, whilst

ev(R + S) ≅ (evR) + (evS) and ev(R ⋆ S) ≅ (evR) ⋆ (evS).

Proof This is a standard piece of universal algebra, which again we leave as a student exercise. The + equation is proved by list induction, using associativity and commutativity of + up to ≅. The equation for ⋆ is more difficult, as we have to take apart the inner lists, and use distributivity.

□

Lemma 9.14 A_{L}B^{L} = ⊤ but

A_{L}B^{R} = (R ⊂^{♯} L) = ∀ℓ ∈ L. ∃ℓ′ ∈ R. (ℓ′ ⊂ ℓ) ≤ (evL ≼ evR)
A_{L}(λψ. ψn) = ∀ℓ ∈ L. n ∈ ℓ  ≤ (evL ≼ n)
A_{L}(λψ. ψn ∧ ψm) = ∀ℓ ∈ L. n ∈ ℓ ∧ m ∈ ℓ  ≤ (evL ≼ n ⋆ m)
A_{L}(λψ. ψn ∨ ψm) = ∀ℓ ∈ L. n ∈ ℓ ∨ m ∈ ℓ  ≤ (evL ≼ n + m)

with equality in the case L = \begin{matrix}\{ \\ | & \{ ; |k| ; \} & | \\ \} \end{matrix}. Proof In the expansion of A_{L}B^{R}, the products in L are of longer strings than those in R. The other three results follow by putting R = \begin{matrix}\{ \\ | & \{ ; |n| ; \} & | \\ \} \end{matrix}, \begin{matrix}\{ \\ | & \begin{matrix}\{ \\ | & n, m & | \\ \} \end{matrix} & | \\ \} \end{matrix} and \begin{matrix}\{ \\ | & \{ ; |n| ; \}, \{ ; |m| ; \} & | \\ \} \end{matrix}, □

Remark 9.15 The foregoing discussion of ≅ is the price that we pay for not requiring (N, 0, 1, +, ⋆) to satisfy the equations for a distributive lattice in Remark 1.8. If, like [15], we had done so, we would have instead paid the same price to construct the basis for Σ^{X}. This is indexed by the free distributive lattice on N^{op} quâ ⋆-semilattice, i.e. with new joins but using the old ones as meets.

The reason why we do not need to form the quotient of N or Fin(FinN) by the congruence ≅ is that we never deal with their elements up to equality. The things that matter are the rules

n ≅ n′  n ≺ ≺ k ; = ; n′ ≺ ≺ k  k ≺ ≺ n  n ≅ n′ ; = ; k ≺ ≺ n′

which are examples of Corollary 8.5. Indeed the relation ≼ itself is only needed to avoid the extra rules that relate + and ⋆ to ≺ ≺, which appear in [15, Lemma 7].

10 Constructing a space from an abstract basis

We are now able to show that any “abstract” basis satisfying the conditions of Section 8 actually arises from some definable space.

Definition 10.1 An abstract basis is an overt discrete object N with elements 0, 1 ∈ N, binary operations +, ⋆ : N × N → N and an open binary relation ≺ ≺ : N × N ⇉ Σ such that

0 ≺ ≺ 0  n ≺ ≺ p m ≺ ≺ p ; = ; n + m ≺ ≺ p  {m′ ≼ m m ≺ ≺ n n ≼ n′ \atop m′ ≺ ≺ n′}  n ≺ ≺ m ; = ; n ≺ ≺ k ≺ ≺ m

{n ≺ ≺ m m ≺ ≺ p m ≺ ≺ q \atop n ≺ ≺ p ⋆ q}  n ≺ ≺ p + q ; = ; n ≺ ≺ p′ + q′  p′ ≺ ≺ p  q′ ≺ ≺ q

where ≼ is defined from + and ⋆ by Definition 9.10.

Definition 10.2 Using the methods of [B, Section 8], X will be constructed as a Σ-split subspace of Σ^{N} determined by a “nucleus” E : Σ^{Σ^{N}} → Σ^{Σ^{N}}, where

E ≡ λF. λψ. J(λn. ∃L. (n ≺ ≺ evL) ∧ A_{L}F )ψ
≡ λF. λψ. ∃n. ∃L. ψn ∧ (n ≺ ≺ evL) ∧ A_{L}F.

The main task is to show that this satisfies the equations in Theorem 7.21,

F, G : Σ^{Σ^{N}} ⊢ E(F ∧ G) = E(EF ∧ EG) and E(F ∨ G) = E(EF ∨ EG),

for which we first have to evaluate the expression A_{L}(EB^{R}).

Lemma 10.3 EB^{R} = J(λn. n ≺ ≺ evR). Proof

EB^{R} = J(λn. ∃L. n ≺ ≺ evL ∧ A_{L}B^{R})  Definition 10.2
≤ J(λn. ∃L. n ≺ ≺ evL ≼ evR)  Lemma 9.14
= J(λn. n ≺ ≺ evR)  Definition 10.1

but the ≤ is an equality, as we may put L = R in the other direction. □

Lemma 10.4 If ≺ ≺ satisfies 0 ≺ ≺ k and (cf. Lemma 8.3)

n ≺ ≺ k  m ≺ ≺ k ; = ; n + m ≺ ≺ k  {n ≺ ≺ r \atop m ⋆ n ≺ ≺ r}

then A_{L}(EB^{R}) ≤ (evL ≺ ≺ evR), with equality in the case L = \begin{matrix}\{ \\ | & \{ ; |k| ; \} & | \\ \} \end{matrix}.

Proof The reason for the inequality is that, whereas B^{(−)} : Fin(FinN) → DL(N) → Σ^{Σ^{N}} sends + to ∨ and ⋆ to ∧, A_{(−)} only takes + to ∧.

A_{L}(EB^{R}) = ∀ℓ ∈ L. EB^{R}(λm. m ∈ ℓ)  def A_{L}
= ∀ℓ ∈ L. J(λn. n ≺ ≺ evR)(λm. m ∈ ℓ)  Lemma 10.3
= ∀ℓ ∈ L. ∃n ∈ ℓ. n ≺ ≺ evR  def. J
≤ ∀ℓ ∈ L. μℓ ≺ ≺ evR  ⋆ rule
= evL ≺ ≺ evR  0, + rules

where μℓ is the “product” of ℓ, in the sense of 1 and ⋆ (which functional programmers would write as fold ⋆ 1 ℓ), and evL is the sum of these products (Definition 9.10). Equality holds in the case

L = \begin{matrix}\{ \\ | & \{ ; |k| ; \} & | \\ \} \end{matrix} because ℓ = \{ ; |k| ; \} and evL = μℓ = k. □

Equipped with formulae for EB^{R} and A_{L}(EB^{R}), we can verify the two equations.

Lemma 10.5 In showing that E(EF ⊙ EG) = E(F ⊙ G), it suffices to consider F = B^{R} and G = B^{S}. Proof We use the lattice basis expansion F = ∃R. A_{R}F ∧ B^{R}. Note first that the combined expansion using distributivity (Lemma 8.8),

F ⊙ G = ∃RS. A_{R}F ∧ A_{S}G ∧ (B^{R} ⊙ B^{S}),

is directed in ⟨R, S⟩, so E preserves the join by Theorem 7.6 and EF = ∃R. A_{R}F ∧ EB^{R}. Using distributivity, directedness and Scott continuity again, we have

EF ⊙ EG  = ∃RS. A_{R}F ∧ A_{S}G ∧ (EB^{R} ⊙ EB^{S})  distributivity
E(EF ⊙ EG) = ∃RS. A_{R}F ∧ A_{S}G ∧ E(EB^{R} ⊙ EB^{S})  directedness
= ∃RS. A_{R}F ∧ A_{S}G ∧ E(B^{R} ⊙ B^{S})  hypothesis
= E(F ⊙ G)  □

The proofs of the two equations are almost the same, illustrating once again the lattice duality that we get by putting directed joins into the background. Unfortunately, they’re not quite close enough for us to use ⊙ and give just one proof. First, however, we give the similar but slightly simpler argument for idempotence, although it is easily seen to be implied by either of the other results.

Proposition 10.6 If ≺ ≺ satisfies the transitive and interpolation rules,

n ≺ ≺ r ; = ; n ≺ ≺ m ≺ ≺ r

cf. Corollary 8.7, then E is idempotent: E(EF) = EF. Proof By (a simpler version of) Lemma 10.5, it’s enough to consider F = B^{R},

E(EB^{R}) = J(λn. ∃L. (n ≺ ≺ evL) ∧ A_{L}(EB^{R}))  Definition 10.2
≤ J(λn. ∃m. (n ≺ ≺ m) ∧ (m ≺ ≺ evR))  Lemma 10.4
= J(λn. n ≺ ≺ evR)  hypothesis
= EB^{R}  Lemma 10.3

where m = evL, but the ≤ is an equality as we may use L = \begin{matrix}\{ \\ | & \{ ; |m| ; \} & | \\ \} \end{matrix} to prove ≥. □ Proposition 10.7 If ≺ ≺ obeys the rule linking it with ⋆,

n ≺ ≺ r ⋆ s = n ≺ ≺ m m ≺ ≺ r m ≺ ≺ s

cf. Lemma 8.11, then E satisfies the ∧-equation, E(F ∧ G) = E(EF ∧ EG). Proof By Lemma 10.5, it’s enough to consider F = B^{R} and G = B^{S}. With m = evL, r = evR and s = evS,

E(EB^{R} ∧ EB^{S}) = J(λn. ∃L. (n ≺ ≺ evL) ∧ A_{L}(EB^{R} ∧ EB^{S}))  Definition 10.2
= J(λn. ∃L. (n ≺ ≺ evL) ∧ A_{L}(EB^{R}) ∧ A_{L}(EB^{S})) Lemma 9.6
≤ J(λn. ∃m. (n ≺ ≺ m) ∧ (m ≺ ≺ r) ∧ (m ≺ ≺ s))  Lemma 10.4
= J(λn. n ≺ ≺ r ⋆ s)  hypothesis
= J(λn. n ≺ ≺ ev(R ⋆ S))  Lemma 9.13
= EB^{R⋆S} = E(B^{R} ∧ B^{S})  Lemma 10.3

but the ≤ is an equality as we may put L = \begin{matrix}\{ \\ | & \{ ; |m| ; \} & | \\ \} \end{matrix} the other way. □ Proposition 10.8 If ≺ ≺ satisfies the Wilker rule linking it with +,

n ≺ ≺ r + s = n ≺ ≺ p + q p ≺ ≺ r q ≺ ≺ s

cf. Lemma 8.12, then E satisfies the ∨-equation, E(F ∨ G) = E(EF ∨ EG). Proof With r = evR, s = evS, p = evL_{1} and q = evL_{2},

E(EB^{R} ∨ EB^{S}) = J(λn. ∃L. (n ≺ ≺ evL) ∧ A_{L}(EB^{R} ∨ EB^{S}))  Definition 10.2
= J(λn. ∃L_{1}L_{2}. (n ≺ ≺ evL_{1} + evL_{2}) ∧ A_{L_{1}}(EB^{R}) ∧ A_{L_{2}}(EB^{S}))  9.7
≤ J(λn. ∃pq. (n ≺ ≺ p + q) ∧ (p ≺ ≺ r) ∧ (q ≺ ≺ s))  Lemma 10.4
= J(λn. n ≺ ≺ r + s)  hypothesis
= J(λn. n ≺ ≺ ev(R + S))  Lemma 9.13
= EB^{R+S} = E(B^{R} ∨ B^{S})  Lemma 10.3

but again the ≤ becomes an equality with L_{1} = \begin{matrix}\{ \\ | & \{ ; |p| ; \} & | \\ \} \end{matrix}, L_{2} = \begin{matrix}\{ \\ | & \{ ; |q| ; \} & | \\ \} \end{matrix} and L = L_{1} + L_{2}. □ Corollary 10.9 E is a nucleus on Σ^{N} in the sense of [B, Section 8]. □

Now we can characterise the (parametric) points of the newly defined space, and construct a lattice basis on it in a similar way to Theorem 8.19. Notation 10.10 Let i : X ≡ {Σ^{N} | E} Σ^{N} with admit and I as in [B, §8]. Then Γ ⊢ ψ : Σ^{N} is admissible, i.e. of the form ψ = ix for some unique x : X, if

Γ, F : Σ^{Σ^{N}} ⊢ F ψ = EF ψ.

Lemma 10.11 If Γ ⊢ ψ : Σ^{N} is admissible then it is a rounded in the sense that

Γ, n : N ⊢ ψn = ∃m. ψm ∧ m ≺ ≺ n.

Proof Consider F ≡ λψ. ψn, so A_{L}F ≤ (evL ≼ n) by Lemma 9.14. Then

ψn = F ψ = EF ψ = ∃m. ∃L. ψm ∧ (m ≺ ≺ evL) ∧ A_{L}F  Definition 10.2
≤ ∃m. ∃L. ψm ∧ (m ≺ ≺ evL ≼ n)  above
≤ ∃m. ψm ∧ (m ≺ ≺ n)  monotonicity

where ≤ is actually equality, as we may put L = \begin{matrix}\{ \\ | & \{ ; |n| ; \} & | \\ \} \end{matrix} to obtain ≥. □

Lemma 10.12 If Γ ⊢ ψ : Σ^{N} is admissible then it is a lattice homomorphism in the sense that

ψ0 = ⊥  ψ1 = ⊤  ψ(n + m) = ψn ∨ ψm  ψ(n ⋆ m) = ψn ∧ ψm.

Proof Consider F ≡ λψ. ψn ⊙ ψm, so A_{L}F ≤ (evL ≼ n ⊙ m) by Lemma 9.14. Then

ψn ⊙ ψm = F ψ = EF ψ
= ∃k. ∃L. ψk ∧ (k ≺ ≺ evL) ∧ A_{L}F  Definition 10.2
≤ ∃k. ∃L. ψk ∧ (k ≺ ≺ evL ≼ n ⊙ m)  Lemma 9.14
≤ ψ(n ⊙ m)  monotonicity

with equality by L = \begin{matrix}\{ \\ | & \begin{matrix}\{ \\ | & n ⊙ m & | \\ \} \end{matrix} & | \\ \} \end{matrix} and roundedness. Similarly, for the constants, consider F ≡ λψ. ⊤, so A_{L}F = ⊤ = (evL ≼ 1), and F ≡ λψ. ⊥, so A_{L}F = ∀ℓ ∈ L. ⊥ = (L = 0). □

Notice that it is the fact that ψ is rounded (for ≺ ≺) rather than a homomorphism (for 0, 1, +, ⋆) that distinguishes the particular space X from the ambient Σ^{N} into which it is embedded.

Lemma 10.13 If Γ ⊢ ψ : Σ^{N} is a rounded lattice homomorphism then it is admissible.

Proof F ψ = ∃L. A_{L}F ∧ B^{L}ψ

= ∃L. A_{L}F ∧ ψ(evL)  homomorphism
= ∃L. ∃n. A_{L}F ∧ ψn ∧ (n ≺ ≺ evL)  rounded
= EF ψ  Definition 10.2

where we get equality by putting L = \begin{matrix}\{ \\ | & \{ ; |n| ; \} & | \\ \} \end{matrix}. □

Lemma 10.14 β^{n} ≡ λx. ixn and A_{n} ≡ λϕ. Iϕ{n} provide an effective basis for X. Proof First note that ψ ↦ Jϕψ preserves joins in ψ, and therefore so do ψ ↦ EF ψ and ψ ↦ Iϕψ, as required by Lemma 5.3, so we recover

ix = λn. β^{n}x and Iϕ = λψ. ∃n. A_{n}ϕ ∧ ψn.

For the basis expansion, let ϕ : Σ^{X} and x : X. Then ψ ≡ ix : Σ^{N} is admissible, and ϕ = Σ^{i}F, where F ≡ Iϕ : Σ^{Σ^{N}}.

∃n. A_{n}ϕ ∧ β^{n}x = ∃n. Iϕ{n} ∧ ixn  defs β^{n}, A_{n}
= ∃n. (I · Σ^{i})F {n} ∧ ψn  defs F, ψ
= ∃n. EF {n} ∧ ψn  defs i, I
= EF ψ  EF preserves ψ = ∃n. ψn ∧ {n}
= F ψ  ψ admissible
= (Iϕ)(ix)  defs F, ψ
= ϕx  {}η [B, Section 8]. □

Theorem 10.15 (β^{n}, A_{n}) is a lattice basis whose way-below relation is ≺ ≺. Proof β^{0} = λx. ⊥, β^{1} = λx. ⊤ and β^{n⊙m} = β^{n} ⊙ β^{m} since x : X ⊢ ψ ≡ ix ≡ λn. β^{n}x : Σ^{N} is admissible, and therefore a homomorphism by Lemma 10.12.

Next we check the equations on A_{n} for an ∨-basis. Let ϕ : Σ^{X} and F = Iϕ : Σ^{Σ^{N}}; then EF = I · Σ^{i} · Iϕ = Iϕ = F. So

A_{0}ϕ = Iϕ{0} = F {0} = EF {0}
= ∃L. (0 ≺ ≺ evL) ∧ A_{L}F  Definition 10.2
≥ (0 ≺ ≺ 0) ∧ A_{0}F = ⊤
A_{n}ϕ ∧ A_{m}ϕ  = EF {n} ∧ EF {m}
= ∃L_{1}L_{2}. (n ≺ ≺ evL_{1}) ∧ (m ≺ ≺ evL_{2}) ∧ A_{L_{1}}F ∧ A_{L_{2}}F Def. 10.2

≤ ∃L_{1}L_{2}. (n + m ≺ ≺ evL_{1} + evL_{2}) ∧ A_{L_{1}+L_{2}}F
≤ ∃L. (n + m ≺ ≺ evL) ∧ A_{L}F  Lemma 9.13
= EF {n + m} = A_{n+m}ϕ  Definition 10.2

using distributivity, L = L_{1} + L_{2} and Lemma 9.6. But A_{n+m}ϕ ≤ A_{n}ϕ, so we have equality. Finally,

A_{n}β^{m} = I(λx. ixm){n} = (I · Σ^{i})(λϕ. ϕm){n}  Lemma 10.14
= E(λϕ. ϕm){n}
= ∃L. (n ≺ ≺ evL) ∧ A_{L}(λϕ. ϕm)  Definition 10.2
≤ ∃L. (n ≺ ≺ evL ≼ m)  Lemma 9.14
≤ (n ≺ ≺ m)  monotonicity

where we also obtain ≥ by putting L = \begin{matrix}\{ \\ | & \{ ; |m| ; \} & | \\ \} \end{matrix}. □

Corollary 10.16 If the space X and its lattice basis (β^{n}, A_{n}) had been given, and ≺ ≺ and E derived from them, this construction would recover X and (β^{n}, A_{n}) up to unique isomorphism. In particular, if we had started with a filter basis, we would get one back. □

We have shown that the notion of “abstract basis” is a complete axiomatisation of the waybelow relation, and is therefore the formulation of the consistency requirements in Definitions 1.5 and 1.15, without using a classically defined topological space or locale as a reference. We have also characterised points of X as rounded lattice homomorphisms N → Σ. We shall generalise this to continuous functions Y → X in the next section, and then show how these calculations answer the questions in Section 1.

11 Morphisms as matrices

The analogy between bases for topology and bases for linear algebra in Section 4 can also be applied to morphisms. In this section we identify the abstract conditions satisfied by the relation

fK^{n} ⊂ U^{m} or K^{n} ⊂ f^{∗}U^{m}

that was used in Definition 1.6. Like ≺ ≺, this is a binary relation between the two overt discrete spaces of codes.

As this condition is an observable property of the function, it determines an open subspace of the set of functions X → Y, and such properties form a sub-basis of the compact–open topology. If X is locally compact then this space is the exponential Y^{X} in both traditional topology and locale theory, and the conditions below are those listed in [9, Lemma VII 4.11]. Unfortunately, there need not be a corresponding dual basis of compact subspaces to make Y^{X} locally compact. The general construction of Y^{X} in abstract Stone duality must therefore await the extension mentioned in Remark 3.19, but it will then be done in quite a different way.

In our notation, the condition is A_{n}(Σ^{f}β^{m}). Clearly this question can easily be generalised to A_{n}(Hβ^{m}), in which we replace f by the “second class” map Ĥ (Notation 3.12).

Notation 11.1 Let (β^{n}, A_{n}) and (γ^{m}, D_{m}) be ∨-bases for spaces X and Y respectively. Then any first or second class morphism Ĥ : X −× Y in HS (that is, H : Σ^{Y} → Σ^{X} in S) has a matrix,

Ĥ_{n}^{m} ≡ A_{n}(Hγ^{m}).

Lemma 11.2 H is recovered from Ĥ_{n}^{m} as Hψ = ∃mn. D_{m}ψ ∧ Ĥ_{n}^{m} ∧ β^{n}.

Proof Hψ = H(∃m. D_{m}ψ ∧ γ^{m})  (γ^{m}, D_{m}) basis for Y

= ∃m. D_{m}ψ ∧ Hγ^{m}  indeed ∨-basis
= ∃m. D_{m}ψ ∧ ∃n. A_{n}(Hγ^{m}) ∧ β^{n}  (β^{n}, A_{n}) basis for X
= ∃mn. D_{m}ψ ∧ Ĥ_{n}^{m} ∧ β^{n}  definition □

Lemma 11.3 The matrix is directed in n, cf. Lemma 8.3:

Ĥ_{0}^{m} = ⊤ and Ĥ_{n+p}^{m} = Ĥ_{n}^{m} ∧ Ĥ_{p}^{m}.

Proof These are A_{0}ϕ = ⊤ and A_{n+p}ϕ = A_{n}ϕ∧A_{p}ϕ with ϕ = Hγ^{m}. They hold because (β^{n}, A_{n}) is an ∨-basis (Definition 4.4(a)). □

Lemma 11.4 The matrix is monotone in m, cf. Lemma 8.6:

(n′ ≼_{X} n) ∧ Ĥ_{n}^{m} ∧ (m ≼_{Y} m′) ≤ Ĥ_{n′}^{m′}.

Proof A_{n} ≤ A_{n′} (though we already had this from directedness) and γ^{m} ≤ γ^{m′}. □

Lemma 11.5 The matrix is rounded, i.e. respects ≺ ≺, on both sides, cf. Lemma 8.7:

∃m′. (m′ ≺ ≺_{Y} m) ∧ Ĥ_{n}^{m′} = Ĥ_{n}^{m} = ∃n′. Ĥ_{n′}^{m} ∧ (n ≺ ≺_{X} n′).

Proof Ĥ_{n}^{m′} = A_{n}(Hγ^{m′})

= A_{n}(H(∃m. D_{m}γ^{m′} ∧ γ^{m}))  (γ^{m}, D_{m}) basis for Y
= ∃m. D_{m}γ^{m′} ∧ A_{n}(Hγ^{m})  indeed, ∨-basis
= ∃m. (m ≺ ≺ m′) ∧ Ĥ_{n}^{m}
Ĥ_{n′}^{m} = A_{n′}(Hγ^{m})
= A_{n′}(∃n. A_{n}(Hγ^{m}) ∧ β^{n})  (β^{n}, A_{n}) basis for X
= ∃n. A_{n}(Hγ^{m}) ∧ A_{n′}β^{n}  indeed, ∨-basis
= ∃n. Ĥ_{n}^{m} ∧ (n′ ≺ ≺ n)  □

Lemma 11.6 Suppose n, m : N ⊢ ρ(n, m) : Σ satisfies the foregoing properties, i.e.

ρ(0, k)  ρ(n, k) ρ(m, k) ; = ; ρ(n + m, k)  n ≺ ≺ n′ ρ(n′, m) ; = ; ρ(n, m)  ρ(n, m′) m′ ≺ ≺ m ; = ; ρ(n, m)

and let Hψ ≡ ∃mn. D_{m}ψ ∧ ρ(n, m) ∧ β^{n}. Then ρ(n, m) = A_{n}(Hγ^{m}). Proof Since ρ respects ≺ ≺ on the right,

Hγ^{m} = ∃m′n. D_{m′}γ^{m} ∧ ρ(n, m′) ∧ β^{n}
= ∃m′n. (m′ ≺ ≺ m) ∧ ρ(n, m′) ∧ β^{n}
= ∃n. ρ(n, m) ∧ β^{n}.

Then, since ρ also respects ≺ ≺ on the left and A_{n} preserves the join, which is directed because ρ respects 0 and +,

A_{n}(Hγ^{m}) = A_{n}(∃n′. ρ(n′, m) ∧ β^{n′})
= ∃n′. ρ(n′, m) ∧ A_{n}β^{n′}
= ∃n′. ρ(n′, m) ∧ n ≺ ≺ n′ = ρ(n, m).  □

Lemma 11.7 id_{n}^{m} = A_{n}(idβ^{m}) = (n ≺ ≺ m) = Ê_{n}^{m}. Proof The relationship with E follows from Lemma 10.4. The unit laws were given by Lemma 11.5, cf. the Karoubi completion, which splits idempotents in any category. □

Lemma 11.8 { \atop K · H}_{n}^{k} = ∃m. K̂_{m}^{k} ∧ Ĥ_{n}^{m}.

Proof { \atop K · H}_{n}^{k} = A_{n}(H(Kϵ^{k}))

= A_{n}(∃mn′. D_{m}(Kϵ^{k}) ∧ Ĥ_{n′}^{m} ∧ β^{n′})  Lemma 11.2
= ∃mn′. D_{m}(Kϵ^{k}) ∧ Ĥ_{n′}^{m} ∧ A_{n}β^{n′}  ∨-basis
= ∃mn′. D_{m}(Kϵ^{k}) ∧ Ĥ_{n′}^{m} ∧ (n ≺ ≺ n′)
= ∃m. D_{m}(Kϵ^{k}) ∧ Ĥ_{n}^{m}  Lemma 11.5
= ∃m. K̂_{m}^{k} ∧ Ĥ_{n}^{m}  def K. □

Theorem 11.9 HS (Notation 3.12) is equivalent to the category whose

(a) objects are abstract bases (N, 0, 1, +, ⋆, ≺ ≺) (Definition 10.1);

(b) morphisms are ρ(n, m) satisfying the conditions in Lemma 11.6;

(c) identity is ≺ ≺;

(d) composition is relational. □ The definition of HS in [A] was essentially taken from Hayo Thielecke’s work on “computational

effects”, which was in turn based on the Kleisli category for the monad, and was motivated by more syntactic considerations than ours. From a semantic point of view, however, it would have been more natural to have split the idempotents. In the classical models, the category would then be that of all continuous (but not necessarily distributive) lattices and Scott-continuous maps. In this result, we would drop the ≺ ≺ + and ≺ ≺ ⋆ rules from the definition of abstract basis.

In order to characterise first class maps, by Corollary 7.15 we have to consider preservation of the lattice connectives. For this, the target space Y must have a lattice basis.

Lemma 11.10 H⊤ = ⊤ iff Ĥ_{n}^{1} = (n ≺ ≺ 1), and H⊥ = ⊥ iff Ĥ_{n}^{0} = (n ≺ ≺ 0).

Proof If H⊤ = ⊤ then Ĥ_{n}^{1} ≡ A_{n}(Hγ^{1}) ≡ A_{n}(H⊤) = A_{n}⊤ ≡ A_{n}β^{1} ≡ (n ≺ ≺ 1) by Notation 11.1, Definition 4.4, and Notation 8.1.

Conversely, H⊤ ≡ Hγ^{1} ≡ ∃n. Ĥ_{n}^{1} ∧ β^{n} = ∃n. A_{n}⊤ ∧ β^{n} ≡ ⊤ by Definition 4.4, Lemma 11.5 and Definition 4.1.

We may substitute ⊥ and 0 for ⊤ and 1 in the same argument. □

Similarly we are able on this occasion to handle ∧ and ∨ simultaneously (Remark 2.23).

Lemma 11.11 H(ϕ ⊙ ψ) = Hϕ ⊙ Hψ iff Ĥ_{n}^{s⊙t} = ∃mp. Ĥ_{m}^{s} ∧ Ĥ_{p}^{t} ∧ (n ≺ ≺ m ⊙ p), both when ⊙ is ∧ or ⋆ and when it is ∨ or +. Proof If H(ϕ ⊙ ψ) = Hϕ ⊙ Hψ then

Ĥ_{n}^{s⊙t}  = A_{n}(Hβ^{s⊙t}) = A_{n}(H(β^{s} ⊙ β^{t}))
= A_{n}(Hβ^{s} ⊙ Hβ^{t})  hypothesis
= ∃mp. A_{m}(Hβ^{s}) ∧ A_{p}(Hβ^{t}) ∧ (n ≺ ≺ m ⊙ p)  Lemma 8.9
= ∃mp. Ĥ_{m}^{s} ∧ Ĥ_{p}^{t} ∧ (n ≺ ≺ m ⊙ p)

Conversely, using distributivity,

Hϕ ⊙ Hψ = (∃mu. D_{m}ϕ ∧ Ĥ_{u}^{m} ∧ β^{u}) ⊙ (∃pv. D_{p}ψ ∧ Ĥ_{v}^{p} ∧ β^{v})  Lemma 11.2
= ∃mpuv. D_{m}ϕ ∧ D_{p}ψ ∧ Ĥ_{u}^{m} ∧ Ĥ_{v}^{p} ∧ β^{u⊙v}  Lemma 2.24
= ∃kmpuv. D_{m}ϕ ∧ D_{p}ψ ∧ Ĥ_{u}^{m} ∧ Ĥ_{v}^{p} ∧ (k ≺ ≺ u ⊙ v) ∧ β^{k}  L. 8.4
= ∃kmp. D_{m}ϕ ∧ D_{p}ψ ∧ Ĥ_{k}^{m⊙p} ∧ β^{k}  hypothesis
= ∃nkmp. D_{m}ϕ ∧ D_{p}ψ ∧ (n ≺ ≺ m ⊙ p) ∧ Ĥ_{k}^{n} ∧ β^{k}  Lemma 11.5
= ∃nk. D_{n}(ϕ ⊙ ψ) ∧ Ĥ_{k}^{n} ∧ β^{k}  Lemma 8.9
= H(ϕ ⊙ ψ)  Lemma 11.2 □

Definition 11.12 An abstract matrix is a binary relation Ĥ_{n}^{m} such that

Ĥ_{0}^{m}  Ĥ_{n}^{m} Ĥ_{p}^{m} ; = ; Ĥ_{n+p}^{m}  n′ ≼_{X} n Ĥ_{n}^{m} m ≼_{Y} m′ ; Ĥ_{n′}^{m′}  Ĥ_{n′}^{m′} ; = ; n′ ≺ ≺_{X} n Ĥ_{n}^{m} m ≺ ≺_{Y} m′

n ≺ ≺ 0 ; = ; Ĥ_{n}^{0}  n ≺ ≺ 1 ; = ; Ĥ_{n}^{1}  Ĥ_{n}^{s⋆t} ; = ; Ĥ_{m}^{s} Ĥ_{p}^{t} n ≺ ≺ m ⋆ p  Ĥ_{n}^{s+t} ; = ; Ĥ_{m}^{s} Ĥ_{p}^{t} n ≺ ≺ m + p

Theorem 11.13 S is equivalent to the category

(a) whose objects are abstract lattice bases (N, 0, 1, +, ⋆, ≺ ≺);

(b) whose morphisms are abstract matrices;

(c) identity is ≺ ≺;

(d) composition is relational. □

Jung and Sünderhauf characterised continuous functions between stably locally compact spaces in a similar way [15].

12 Relating the classical and computable models

We promised to translate each step of the logical development into topological language, but we haven’t done this since the end of Section 5. We shall now show how the “coding” provides the link between the classical and computational models, and then how abstract matrices themselves describe exact computation for the reals and locally compact spaces in general.

Remark 12.1 On the one hand, we know from the classical proof for LKSp in [A, Theorem 5.12] and the intuitionistic one for LKLoc in [B, Theorem 3.11] that these categories are models of the calculus in Section 2, i.e. that there are interpretation functors [[−]] : S → LKSp and [[−]] : S → LKLoc. In the light of Theorem 6.10, that every object of S is a Σ-split subspace of Σ^{ℕ}, the converse part of Theorem 5.11 provides another proof in the localic setting.

In this paper we have sought the “inverse” of this functor. Since the classical models are of course richer, they have to be constrained in order to obtain something equivalent to the computational one. This constraint was in the form of a computational basis, as in Definitions 1.5 and 1.15. Nevertheless, as we saw in the case of ℝ, such bases may already be familiar to us from traditional considerations.

There is no need to verify the consistency conditions that we set out in Sections 8 and 10. They follow automatically from the existence of the classical space, which serves as a reference as in Remark 1.7. So long as ⋆, + and ≺ ≺ are defined by programs, which can be translated into our λ-calculus, we already have an abstract basis.

Examples 12.2 At this point let us recall the various ways in which a lattice basis can be defined on a locally compact sober space or locale.

(a) In a stably locally compact sober space (which is, in particular, compact in the global sense), we may choose a sublattice of compact subspaces K^{n} and corresponding sublattice of open ones U^{n}, such that U^{n} ⊂ K^{n} and the basis expansion is satisfied. Then the indexing set N, together with the operations + and ⋆ on codes corresponding to unions and intersections of open–compact pairs, and the relation n ≺ ≺ m given by K^{n} ⊂ U^{m}, define an abstract basis, so long as these operations are computable. In the corresponding lattice filter basis in the λ-calculus, β^{n} and A_{n} classify U^{n} and the Scott-open filter F_{n} ≡ {V | K^{n} ⊂ V }.

(b) In a compact Hausdorff space, the compact subspaces K^{n} are the complements of open subspaces V_{n}, which may be chosen from the same sublattice as the U^{n}, but with U^{n} ∩̸ V_{n}.

(c) In particular, finite unions of open and closed rational intervals provide this structure for the closed real unit interval [0, 1].

(d) ℝ is not globally compact, though binary intersections of compact subspaces are compact. The lattice basis may be defined in the same way as for [0, 1], with the single exception of A_{1} = λϕ. ⊥, which does not preserve ⊤.

(e) Let (N, ◁) be a recursively enumerable filtered interpolative relation (Definition 8.16). Then Theorem 8.19 defines an object in S, whose classical interpretation is the continuous dcpo of rounded ideals of (N, ◁); it is algebraic iff ◁ is reflexive.

(f) The reflexive order ≼ defined from any imposed distributive lattice (N, 0, 1, +, ⋆) by Definition 9.10 satisfies the conditions on ≺ ≺ for an abstract basis, and so defines an object of S whose classical interpretation is the coherent space whose compact open subspaces are indexed by N.

(g) Given a locally compact locale, we choose a sublattice N that provides a basis for the corresponding continuous distributive lattice L, so β^{(−)} : N → L. Then define (n ≺ ≺ m) ≡ (β^{n} ≪ β^{m}). This is a lattice basis, but only a filter basis in the stably locally compact case.

(h) Finally, in the case of a non-stably locally compact sober space, we only have a ∪-semilattice N of compact subspaces K^{n}, and therefore a (filter) ∨-basis (β^{n}, A_{n}). Remark 6.6 turned this into a lattice basis (β^{ℓ}, A_{ℓ}) indexed by Fin(N), by defining

β^{ℓ}x ≡ ∀n ∈ ℓ. x ∈ U^{n} and A_{ℓ}ϕ ≡ ∃n ∈ ℓ. K^{n} ⊂ V,

where ϕ classifies V as usual. Then β^{ℓ} simply classifies the intersection of the basic open subspaces as in the stably locally compact case, but A_{ℓ} is a logical disjunction, not a union of subspaces, cf. Lemma 3.6(e). Then

ℓ ≺ ≺ ℓ′ = ∃n ∈ ℓ. ∀m ∈ ℓ′. K^{n} ⊂ U^{m},

but this is not a filter basis.

Remark 12.3 Section 10 showed that the abstract basis is inter-definable with the nucleus E. These are interpreted both in the computational model S and in the classical ones LKSp and LKLoc. This means that the idempotent [[E]] on ΥKℕ is the one that defines the Σ-split embedding of the original space in P(ℕ), as in Theorems 5.6 and 5.11.

Hence any classically defined locally compact sober space or locale that has a computable basis may be “imported” into abstract Stone duality as a type, whose interpretation in the classical model is homeomorphic to the given space. Summing this up diagrammatically,

[figure: space; Def. 1.5; Thm. 5.6; embed in Pℕ; E on Pℕ]

[figure: abstract basis; Sec. 10; E on Σ^{ℕ}; [B]; subspace of Σ^{ℕ}]

[figure: locale; Def. 1.21; Thm 5.11; embed in ΥKℕ; E on ΥKℕ in LKLoc]

Remark 12.4 Having fixed computational bases for two classically defined spaces or locales, X and Y, we may look at continuous functions f : X → Y. By the basis property, any such map is determined by the relation

fK^{n} ⊂ K^{m}

as n and m range over the bases for X and Y respectively. If this relation is recursively enumerable (Definition 1.6) then the corresponding program may be translated into our λ-calculus. Just as we saw for abstract bases for the spaces, the resulting term satisfies Definition 11.12 for an abstract matrix because its interpretation agrees with a continuous function. Between the types whose denotations are X and Y there is therefore a term whose denotation is f.

In particular, computationally equivalent bases for the same space give rise to an isomorphism between the types. In the case of morphisms, extensionally equivalent terms give rise to the same (fK^{n} ⊂ K^{m})-relations, and therefore to the same continuous functions. However, programs may be extensionally equivalent for some deep mathematical reason, or as a result of the stronger logical principles in the classical situation, without being provably equivalent within our calculus. This is the reason why we required the computable aspects of the definitions in the Introduction to be accompanied by actual programs.

This completes the proof of our main result:

Theorem 12.5 Abstract Stone duality, i.e. the free model S of the axioms in Section 2, is equivalent to the category of computably based locally compact locales and computably continuous functions. □

Remark 12.6 An obvious lacuna in this result arises from the difference between sober spaces and locales: we are relying on the axiom of choice within the classical models to say that the two are the same. The fact that the bases are enumerated probably makes this Choice redundant within the classical setting, but it would be nice to have a corresponding result within the computational world of abstract Stone duality itself.

The first stage is to show that every object (which carries a lattice basis) has a filter ∨-basis. The idea, due to Jimmie Lawson [5, Section I 3.3], is to iterate the interpolation property [F–]. This can be shown with the aid of a weaker choice principle that merely extracts a total function from a non-deterministic one.

After that, we would like to show that every overt object X is recursively enumerable in the sense that there is a Σ-epi p : U → X (Lemma 3.3), where U ⊂ ℕ is open. I have not yet been able to prove this conjecture. A significant point seems to be the need to decide whether the intersection of two basic compact subspaces is inhabited, cf. the consistency predicate in Proposition 5.9.

Remark 12.7 Let us review what we have achieved by way of a type theory for general topology.

(a) The original idea of abstract Stone duality was that the non-computable unions could be eliminated from general topology by expressing the category of “frames” by a monadic adjunction over its opposite category of “spaces” rather than over sets.

(b) Beck’s theorem says that this is equivalent to the, perhaps less friendly, condition that the functor Σ^{(−)} reflect invertibility and “create Σ-split coequalisers”.

(c) In [B] we saw that the latter can be interpreted as (certain) subspaces, and that the data for such subspaces could be encapsulated in a single morphism E, called a “nucleus”.

(d) This was further developed, in Section 8 of that paper, into a λ-calculus similar to comprehension in set theory. However, the data defining a subspace remained arcane: terms satisfying the equation defining a nucleus could only be found with considerable expert ingenuity.

(e) Another axiom can be added, in type-theoretic form, to endow every space with an underlying set; this makes S equivalent to the category of locally compact locales over a topos [G].

(f) The notion of abstract basis in this paper puts the construction within the grasp of anyone who has a knowledge of open and compact subspaces in topology.

Remark 12.8 Let us consider the computational meaning of the matrix Ĥ_{n}^{m} when H = Σ^{f} for some continuous function f : ℝ → ℝ. In order to have a lattice basis, the indices n and m must range over (finite) unions of intervals, although by Lemma 11.3, n need only denote a single closed interval. The matrix therefore encodes the predicate

f[x_{0} ± δ] ⊂ ⋃_{j}(y_{j} ± ϵ_{j}),

the union being finite. Suppose that we have a real input value x that we know to lie in the interval [x_{0} ± δ], and we require f(x) to within ϵ.

We substitute the rational values x_{0}, δ and ϵ_{j} = ϵ in the predicate, leaving (y_{j}) indeterminate. Recall from [A, Remark 11.3] that any term, such as this, of type Σ may be translated into a PROLOG program. Such a program permits substitution of values for any subset of the free variables, and is executed by resolving unification problems, which result in values of (or at least constraints on) the remaining variables. In this case, we obtain (nondeterministically) some finite set (y_{j}).

In the language of real analysis, we are seeking to cover the compact interval f[x_{0} ± δ] with (finitely many) open intervals of size ϵ, centred on the y_{j}. The Wilker property (Lemma 11.11) then provides

[x_{0} ± δ] ⊂ ⋃_{j}(x_{j} ± δ′) with f[x_{j} ± δ′] ⊂ (y_{j} ± ϵ).

Responsibility now passes back to the supplier of the input value x to choose which of the x_{j} is nearest, and the corresponding y_{j} is the required approximation to the result f(x). □

Remark 12.9 This illustrates the way in which we would expect to use abstract Stone duality for computations with objects such as ℝ that we regard, from a mathematical point of view, as “base types” (though of course only 1, ℕ and Σ are actually base types of our λ-calculus). Where higher types, such as continuous or differentiable function-spaces, can be shown to be locally compact, they too have bases and matrices, but it would be an example of the mis-use of normalisation theorems (Remark 6.11) to insist on reducing everything to matrix form. We would expect to use higher-type λ-terms of our calculus to encode higher-order features of analysis, for example in the calculus of variations. Of course, much preliminary work with ℝ itself needs to be done before we see what can be done in such subjects.

Remark 12.10 The manipulations that we have done since introducing the abstract way-below relation have all required lattice bases. The naturally occurring basis on a space, on the other hand, is often just an ∧-basis. This didn’t matter in Section 10, as it was only concerned with the theoretical issue of the consistency of the abstract basis. We have just seen, however, that the “matrices” in Section 11 encapsulate actual computation, in which the base types are those of the indices of the bases. The lists used in Lemma 6.4 would therefore be a serious burden.

There is a technical issue here that is intrinsic to topology. In locale theory, which is based on an algebraic theory of finite meets distributing over arbitrary unions of “opens”, it is often necessary to specify when two such expressions are equal, which may be reduced to the question of when an intersection is contained in a union of intersections. This coverage relation is an important part of the technology of locale theory [9, Section II 2.12], whilst it was chosen as the focus of the axiomatisation of Formal Topology.

,

Remark 12.11 The question of whether, using abstract Stone duality, we can develop a technically more usable approach than these warrants separate investigation, led by the examples. Since, in a locally compact space, we may consider coverages of compact subspaces, the covering families of open subspaces need only be finite. Jung, Kegelmann and Moshier have exploited this idea to develop a Gentzen-style sequent calculus [13].

As this finiteness comes automatically, maybe we don’t need to force it by using lists. To put this another way, as the lists act disjunctively, we represent them by their membership predicates [E]. That is, we replace the matrix with the predicate

m : M, ψ : Σ^{N} ⊢ A_{m} · H(λy. ∃n. ψn ∧ β^{n}y) : Σ,

where N need no longer have +. In Remark 12.8 above, we could add the constraint that ψ only admits intervals of size < ϵ.

Remark 12.12 There are many more applications of matrices. For example, Theorem 7.11 gives us the means to study ∧-preserving maps. Classically, these are known as preframe homomorphisms; Vickers [23, 11.2.5] and later Jung, Kegelmann and Moshier related them semantically to the Smyth powerdomain [14] and syntactically to a Gentzen-style sequent calculus [13].

Similar investigations can be done for join-preserving maps and the Hoare powerdomain, and both versions should provide models of linear logic. This justifies the analogy that we have made with vector spaces, and which was exploited in locale theory in [12]. Interestingly, the composite of the two covariant powerdomains agrees with the contravariant functor Σ^{(−)} applied twice, cf. [16, 22].

Remark 12.13 Another striking feature of the matrix description is that it reduces the topological theory to an entirely discrete one. The latter may be expressed in an arithmetic universe, which is a category with finite limits, stable disjoint coproducts, stable effective quotients of equivalence relations and a List functor.

Once again, we need to see this normalisation theorem in reverse. It appears that any arithmetic universe with description may conversely be embedded as the full subcategory of overt discrete objects in a model of abstract Stone duality. This would enable topological, domain-theoretic and λ-calculus reasoning to be applied to problems in discrete algebra and logic. Topologically, it would strongly vindicate Marshall Stone’s dictum, always topologise, whilst computationally it would provide continuation-passing translations of discrete problems, and of type theories for inductive types.

References

[1] Nicolas Bourbaki. Topologie Générale. Hermann, 1966. English translation, “General Topology”, distrubuted by Springer-Verlag, 1989.

[2] John Horton Conway and Neil J A Sloane. Sphere Packings, Lattices and Groups. Number 290 in Grundlehren der Mathematischen Wissenschaften. Springer-Verlag, 1988.

[3] Abbas Edelat and Martín Hötzel Escardó. Integration in real PCF. 1996.

[4] Martín Escardó. Synthetic topology of data types and classical spaces. Electronic Notes in Theoretical Computer Science, 87, 2004.

[5] Gerhard Gierz, Karl Heinrich Hoffmann, Klaus Keimel, Jimmie Lawson, Michael Mislove, and Dana Scott. A Compendium of Continuous Lattices. Springer-Verlag, 1980. Second edition, Continuous Lattices and Domains, published by Cambridge University Press, 2003.

[6] G. H. Hardy. A Mathematician’s Apology. Cambridge University Press, 1940. Frequently reprinted.

[7] Karl Hofmann and Michael Lawson. Spectral theory of continuous lattices. Transactions of the American Mathematical Society, 246:285–310, 1978.

[8] Karl Hofmann and Michael Mislove. Local compactness and continuous lattices. In Bernhard Banaschewski and Rudolf-Eberhard Hoffmann, editors, Continuous Lattices, volume 871 of Springer Lecture Notes in Mathematics, pages 209–248, 1981.

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

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

[11] Peter Johnstone. Vietoris locales and localic semi-lattices. In R.-E. Hoffmann and K. H. Hoffmann, editors, Continuous Lattices and their Applications, number 101 in Pure and Applied Mathematics, pages 155–180. Marcel Dekker, 1985.

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

[13] Achim Jung, Mathias Kegelmann, and Andrew Moshier. Multi lingual sequent calculus and coherent spaces. Fundamenta Mathematicae, 20:1–42, 1999.

[14] Achim Jung, Mathias Kegelmann, and Andrew Moshier. Stably compact spaces and closed relations. Electronic Notes in Theoretical Computer Science, 45, 2001. MFPS 17.

[15] Achim Jung and Philipp Sünderhauf. On the duality of compact vs. open. In S. Andima, R.C. Flagg, G. Itzkowitz, P. Misra, Y. Kong, and R.D. Kopperman, editors, Papers on general topology and applications: Eleventh Summer Conference at University of Southern Maine, volume 806 of Annals of the New York Academy of Sciences, pages 214–230, 1996.

[16] Francisco Marmolejo, Robert Rosebrugh, and Richard Wood. A basic distributive law. Journal of Pure and Applied Algebra, 168:209–226, 2002.

[17] Dana Scott. Outline of a mathematical theory of computation. In 4th Annual Princeton Conference on Information Sciences and Systems, pages 169–176, 1970. Superseded by Oxford technical report PRG-2.

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

[19] Michael Smyth. Effectively given domains. Theoretical Computer Science, 5:257–274, 1977.

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

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

[22] Steven Vickers. The double powerlocale and exponentiation. Submitted to Theory and Applications of Categories, 2002.

[23] Steven J. Vickers. Topology Via Logic, volume 5 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1988.

[24] Peter Wilker. Adjoint product and hom functors in general topology. Pacific Journal of Mathematics, 34:269–283, 1970.

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, Inside every model of Abstract Stone Duality lies an Arithmetic Universe. Category Theory and Computer Science 10, Copenhagen, 2004.

[F–] Paul Taylor, Local compactness and the Baire category theorem in abstract Stone duality. Electronic Notes in Theoretical Computer Science 69, Elsevier, 2003.

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

[H] Paul Taylor, Scott domains in abstract Stone duality. March 2002.

This paper evolved from [F–], which included roughly Sections 3, 4, 5, 6 and 8 of the present version. It was presented at Category Theory and Computer Science 9, in Ottawa on 17 August 2002, and at Domains Workshop 6 in Birmingham a month later. The characterisation of locally compact spaces in terms of effective bases (Section 4) had been announced on categories on 30 January 2002.

The earlier version also showed that any object has a filter basis, and went on to prove Baire’s category theorem, that the intersection of any sequence of dense open subspaces (of any locally compact overt object) is dense. These arguments were adapted from the corresponding ones in the theory of continuous lattices [5, Sections I 3.3 and 3.43].

I would like to thank Martín Escardó, Peter Johnstone, Achim Jung, Jimmie Lawson, Graham White and the CTCS referees for their comments. Graham White has given continuing encouragement throughout the abstract Stone duality project, besides being an inexhaustible source of mathematical ideas.

This research is now supported by UK EPSRC project GR/S58522, but this funding was obtained in part on the basis of this paper. Apart from 3.18, 8.13 and 10.12, the work here was carried out during a period of unemployment, supported entirely from my own savings. However, I would have been unable to do this without the companionship and emotional support of my partner, Richard Symes.