17  Relating the classical and term 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 7. We shall now show how the “coding” provides the link between the classical and computational models (Remark 3.1), and then how abstract matrices themselves describe exact computation for the reals and locally compact objects in general.

Remark 17.1 On the one hand, we know from the classical proof for LKSp in Theorem A 5.12 and the intuitionistic one for LKLoc in Theorem B 3.11 that these categories are models of the calculus in Sections 3–4, i.e. that there are interpretation functors ⟦−⟧:S→LKSp and ⟦−⟧:S→LKLoc. In the light of Theorem 8.11, that every object of S is a Σ-split subobject of Σ^ℕ, the converse part of Theorem 7.14 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 (Remark 3.1). This constraint was in the form of a computable basis, as in Definitions 1.5 and 2.3. Nevertheless, as we saw in the case of ℝ (Example 1.4), 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 11 and 14. 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 17.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.

1. 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ⁿ and corresponding sublattice of open ones Uⁿ, such that Uⁿ⊂ Kⁿ 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ⁿ⊂ U^m, define an abstract basis, so long as these operations are computable. In the corresponding lattice filter basis in the λ-calculus, βⁿ and A_n classify Uⁿ and the Scott-open filter F_n≡{V ∣ Kⁿ⊂ V}.
2. In a compact Hausdorff space, the compact subspaces Kⁿ are the complements of open subspaces V_n, which may be chosen from the same sublattice as the Uⁿ, but with Uⁿ⋔ V_n.
3. In particular, finite unions of open or of closed rational intervals provide this structure for the closed real unit interval [0,1].
4. ℝ 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₁≡λφ.⊥, which does not preserve ⊤.
5. Let (N,◁) be a recursively enumerable directed interpolative relation (Definition 12.1). Then Theorem 12.11 defines an object in S, whose classical interpretation is the continuous dcpo of rounded ideals of (N,◁); it is algebraic iff ◁ is reflexive.
6. The reflexive order ≼ defined from any imposed distributive lattice (N,0,1,+,⋆) by Definition 13.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 byN.
7. Given a locally compact locale, we choose a sublattice N that provides a basis for the corresponding continuous distributive lattice L, with inclusion β⁽⁻⁾:N→ L. Then define (n≺≺ m)≡(βⁿ≪β^m). This is a lattice basis, but only a filter basis in the stably locally compact case.
8. Finally, in the case of a non-stably locally compact sober space, we only have a ∪-semilattice N of compact subspaces Kⁿ, and therefore a (filter) ∨-basis (βⁿ,A_n). Remark 8.7 turned this into a lattice basis (β^ℓ,A_ℓ) indexed by Fin(N), by defining

   βℓx  ≡  ∀ n∈ℓ.x ∈ Un   and   Aℓφ  ≡  ∃ n∈ℓ.Kn⊂ 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 5. Then

   ℓ≺≺ ℓ′  ⇔  ∃ n∈ℓ.∀ m∈ℓ′.Kn⊂ Um,

   but this is not a filter basis.

Remark 17.3 Section 14 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 ℘(ℕ), as in Theorems 7.8 and 7.14.

Hence any classically defined locally compact sober space or locale that has a computable basis may be “imported” into abstract Stone duality as an object, whose interpretation in the classical model is homeomorphic to the given space. Summing this up diagrammatically,

Remark 17.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

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, the resulting term satisfies Definition 16.12 for an abstract matrix, because its interpretation agrees with a continuous function. Between the objects 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 objects of S. In the case of morphisms, extensionally equivalent terms give rise to the same (f Kⁿ⊂ V^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 17.5 Abstract Stone duality, i.e. the free model S of the axioms in Sections 3 and 4, is equivalent to the category of computably based locally compact locales and computably continuous functions.         ▫

Remark 17.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. Recall [Joh82, Theorem VII 4.3] that, using excluded middle, the crucial requirement is to find, for any φ≰ψ:L in a distributive continuous lattice,

1. some (Scott open) filter A:Σ^L for which Aφ⇔⊤ but Aψ⇔⊥, and then
2. using Zorn’s lemma, enlarge A to a maximal such filter P, which is prime.

For stage (a), we would like to show, more generally, that every object (which we know carries a lattice basis) also has a filter ∨-basis. The idea, due to Jimmie Lawson [GHK++80, §I 3.3], is to iterate the interpolation property [G–]. This can be shown with the aid of a weaker choice principle that merely extracts a total function from a non-deterministic one.

For stage (b), since any space has a ℕ-indexed lattice basis, we only need to consider Σ^ℕ, and not general distributive continuous lattices. The filter A provides a rounded filter (semilattice homomorphism) ξ₀:Σ^ℕ such that Iφξ⇔⊤ but Iψξ⇔⊥, which we enlarge to a rounded lattice homomorphism ξ (Lemmas 15.2ff) with the same values on φ and ψ. To do this, we may replace Zorn’s Lemma by an argument that uses excluded middle but not Choice: we build up ξ from ξ₀ by adding each number 0, 1, 2, ... in turn if it generates a proper filter.         ▫

Remark 17.7 Let’s review what we’ve achieved by way of a type theory for topology.

1. 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.
2. Beck’s theorem says that this is equivalent to the, perhaps less friendly, condition that the functor Σ⁽⁻⁾ reflect invertibility and “create Σ-split coequalisers”.
3. In [B] we saw that the latter can be interpreted as (certain) subobjects, and that the data for such subobjects could be encapsulated in a single morphism E, called a “nucleus”.
4. This was further developed, in Section 8 of that paper, into a λ-calculus similar to comprehension in set theory. However, the data defining a subobject remained arcane: terms satisfying the equation defining a nucleus could only be found with considerable expert ingenuity.
5. In Theorem 10.10 of this paper we reformulated the λ-equation in a much simpler way using the lattice connectives.
6. 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 17.8 Let us consider the computational meaning of the matrix H_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 16.3, n need only denote a single closed interval. The matrix therefore encodes the predicate

as an ASD term of type Σ, the union being finite. Suppose that we have a real input value x that we know to lie in the interval [x₀±δ], and we require f(x) to within є.

We substitute the rational values x₀, δ and є_j≡є in the predicate, leaving (y_j) indeterminate. Recall from Remark 3.5 and Section t ha t any such term 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₀±δ] with (finitely many) open intervals of size є, centred on the y_j. The Wilker property (Lemma 16.11) then provides

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). This discussion is taken up again in [I, J].         ▫

Remark 17.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 8.12) 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 [I, J].

Remark 17.10 The manipulations that we have done since introducing the abstract way-below relation have all required lattice bases. The naturally occurring basis on an object such as ℝ, on the other hand, is often just an ∧-basis. This didn’t matter in Sections 14–16, as they were only concerned with the theoretical issue of the consistency of the abstract basis. We have just seen, however, that the “matrices” in Section 16 encapsulate actual computation, in which the base types are those of the indices of the bases. The lists used in Lemma 8.4 would then 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 [Joh82, Section II 2.12], whilst it was chosen as the focus of the axiomatisation of Formal Topology.

Remark 17.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 object, we may consider coverages of compact subobjects, the covering families of open subobjects need only be finite. Jung, Kegelmann and Moshier have exploited this idea to develop a Gentzen-style sequent calculus [JKM99].

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 (Remark 8.5). That is, we replace the matrix H_mⁿ with the predicate

where N need no longer have +. In Remark 17.8 above, we could add the constraint that ξ only admits intervals of size <є.

Remark 17.12 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 [E].

Once again, we need to see this normalisation theorem in reverse. It appears that any arithmetic universe may conversely be embedded as the full subcategory of overt discrete objects in a model of abstract Stone duality. Example 4 shows that we can do this by modelling a much simpler structure than that of abstract bases and matrices for general locally compact spaces. The differences in logical strength amongst models of ASD are therefore measured by the overt discrete objects that they contain.

Such a construction 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.