## 1  Locally compact sober spaces

Definition 1.1 The traditional definition of local compactness was generalised from Hausdorff to sober spaces in [HM81, p. 211]: Whenever a point is contained in an open subspace (xV), there is a compact subspace K and an open one U such that xUKV.

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 LVX be compact and open subspaces of a locally compact space. Then there are LUKVX 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 in this paper, and compact subspaces will be more important than points.

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 KL, follows the usage of [HM81, JS96], cf. our Theorem 5.18.

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 of them 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 points, open and compact subspaces that have codes are called basic.

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

1. as basic points, (encodings of) the rationals;
2. as basic open subspaces, the (names of) open intervals (q±є)≡(q−є,q+є)≡ {x ∣ |xq|<є} with rational or infinite endpoints; and
3. as basic compact subspaces, the closed intervals [q±δ]≡[q−δ,q+δ]≡ {x ∣ |xq|≤δ} with finite rational endpoints.

Notice that both open and closed intervals are used, although treatments of exact real arithmetic often just use one or the other, cf. Example 7.12. Also, by “rationals” we might actually mean all pairs p/q with integers p and q≠ 0, or the dyadic rationals p/2n, 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 [CS88]).

In the Example, the intersection of two basic opens is again basic, but for technical reasons we shall also 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 basic “points”, “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

1. 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);
2. 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);
3. 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 there is one, as failure of the property is indicated by non-termination;
4. more generally, whether an open subspace includes a compact one, given their codes;
5. codes for U and K such that LUKV, given codes for LV as above.
6. In fact, we shall require the basic compact and open subspaces to come in pairs, with UnKn as in [JS96], 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:XY between the topological spaces themselves, for which the binary relation

 f Km  ⊂  Un

(between the codes (n,m) for a compact subspace KmX and an open one UnY) 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 KnUm and KmUn 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. This is also the reason why the codes for basic points played no actual role in Definition 1.5 — there needn’t be any of them. Since we said that the spaces are sober, continuous functions are determined entirely by their effect on basic open and compact subspaces, as they are in locale theory. Neither the (optional) basic points, nor the computable ones that we recover in Section 15, nor the uncountably many points of the classical theory, are actually needed to specify continuous functions, or prove topological properties such as compactness.

At the technical level, therefore, what we call a computably based locally compact “space” is really just a system of codes and programs acting on them, for which there exists a topological space in which these codes may be interpreted as compact and open subspaces. Likewise, a computably “continuous function” is just an equivalence class of programs, for which there exists a continuous function that agrees with the program in the way that we have said.

The particular way in which computations are set up is of course a matter for discussion: I still have to convince you of the merits of my way, in comparison to the many other ways that have been used to calculate in ℝn over the millennia, and of course any theoretical picture is subject to technical optimisation. However, these other ways share the same pattern, in that they have a technical definition that is (a) used for applied computation but (b) justified by the existence of an interpretation in some “pure” theory of (Euclidean) space. The pure theory is not the computation, at any rate if it is based on twentieth century topology. So the practical situation is illustrated by Example 1.4: we have a classical definition of a topological space, equipped with a basis that is defined in some conventional way, and 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 Section 11 we shall formulate this consistency in terms of finitary conditions on the transformations of encodings themselves, eliminating the topological space, i.e. we prove necessity of the abstract conditions. Then in Section 14 we prove sufficiency, i.e. that any such encoding (such as the one for ℝ above) satisfying these consistency requirements does define a locally compact sober space, and this is unique up to homeomorphism.

This construction is done, not in traditional topology itself, which is not computable, but in a λ-calculus. Therefore, the construction imports the classical data into the computational world (Section 17). But again there is a distinction between the technical and philosophical meaning: whilst our theory (ASD) starts from (and is reducible back to) computational foundations, it adapts these to give a new account of the mathematical theory that is ultimately intended to be usable by pure mathematicians in place of the old one.

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 (the inclusion UnKn is given, not tested). 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. (We shall regard this topology 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,

 ▫

Finally, there is a property similar to Lemma 1.2 that concerns binary unions. Easy enough though this property may be to prove — 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 [Wil70].

Lemma 1.10 Let K be a compact subspace covered by two open subspaces of a locally compact sober space X, that is, KUV. 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, KV is a closed subspace of a compact space, and is therefore compact too, whilst KVU, so by the interpolation property (Lemma 1.2) we have

 K∖ V ⊂ U′ ⊂ L ⊂ U ⊂ X

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

 K∖ U′ ⊂ V′ ⊂ M ⊂ V ⊂ X

for some V′ open and M compact. Finally, K = (KU′) ∪ (KU′) ⊂ 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

1. 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, but their intersection is not [Kel55, Problem 5 B(a)].
2. A combinatory algebra has constants k and s and a (non-associative) binary operation · such that (k· xy=x and (((s· xyz) = (x· z)·(y· z). In the free such algebra A, terms can be enumerated, and proved equal, using these rules. But, since this structure can be used to encode computation [Bar81], proving inequality in A is like solving the Halting problem. (Similar unsolvable word problems can also be set up in other algebraic theories, such as groups.)
Hence A is discrete but not Hausdorff.
Since it is discrete, its compact subspaces are the Kuratowski-finite ones, i.e. those that can be listed, possibly with repetition. In particular, singletons {x} are open and compact, but not closed. However, the intersection {x}∩{y} is compact (Kuratowski-finite, listable) iff it is either empty (xy) or a singleton (x=y), i.e. iff equality is decidable, which it isn’t.         ▫