Previous Up Next

11  Scott continuity

Although it is remarkable how much the theory already looks like traditional general topology without invoking it, we come to the point where we actually have to say that all functions are Scott continuous as an axiom.

Since this axiom completes the theory of locally compact spaces, we are moving into the territory of a user-oriented account (cf. §3.8), but certain foundational issues remain. One of these is the question of which statement of the Scott continuity axiom we should adopt, since there are several candidates that arise from some of the applications of this idea.


11.1.   Denotational semantics generalises the notion of recursion from minimalisation (µ, §9.12) to fixed points of operators of higher types. Applying the operator F repeatedly to ⊥ gives an increasing sequence φ nFn⊥. Then F fixes the join of such a sequence if we assume the rule

In this case, every space has and every map preserves joins of definable ascending chains with respect to the ⊑ order (§8.2). Also, on any object that has ⊥, every endomorphism has a least fixed point [Tay91].


11.2.   Turning to real analysis, a common use of the Heine–Borel theorem (§1.8) is to derive a uniform value that is valid throughout a compact space K from local values at each point. For example, b:ℝ is an upper bound on a function f:K→ℝ at x if θ(x,b)≡(f x< b)⇔⊤. Then θ is monotone in the sense of taking the imposed arithmetical order ≤ on ℝ to the intrinsic one ⇒ on Σ:

…,  b≤ b′  ⊢    θ(x,b) =⇒ θ(x,b′). 

The δ> 0 that is used in the ε–δ definitions of continuity, differentiability, etc. , is similar, but the defining property reverses the arithmetical order:

…,  0<δ≤ δ′  ⊢    θ(x,δ) ⇐= θ(x,δ′). 

In either case, by compactness, the quantifier ∀K satisfies

∀ k.∃ b.θ(k,b)  =⇒  ∃ b.∀ k.θ(kb). 

In Section J 910 this is used to prove that any expression Γ,x:ℝ⊢ a:ℝ is continuous in the ε–δ-sense, and uniformly so on any compact domain.

This principle, in which the second argument of θ ranges over ℝ, is equivalent to its analogue with ℚ instead. The latter is preferable foundationally (cf. §3.8), as we would like to work with overt discrete spaces (§9).


11.3.   The indexing objects ℕ and ℚ in these two properties have max operations, whilst we may form binary unions of finite open subcovers, so the common pattern is a directed join. In practice, we have a set (overt discrete space) N of indices, equipped with an imposed semilattice operation (+). Then we select an open subsemilattice of N classified by α:ΣN. As in §5.8, we use sub- and super-scripts to indicate co- and contra-variance with respect to this imposed order on N. Then a directed join, written

{n:N ∣ αn} φn  ≡  ∃ n:Nn∧φn

involves a pair of families (αnn) such that

⊤⇔∃ nn,     αn∧αm⇔αn+m     and     φn∨φm⊑φn+m

Then we say that F preserves this join if F(∃ nn∧φn)  =  ∃ nnFφn.

To do this, + does not actually need to satisfy the equations for a semilattice, so the leading examples of (N,+) are (ℕ,max), (ℚ,max), (ℚ,min), (K(M),∪) and (List (M),+) for any overt discrete M.


11.4.   In the first instance we shall be content with N≡ℕ, although it is equivalent but more useful to take NT instead, since List (T)≅T9.6). For either of these Ns, we assert the Scott continuity axiom in the form

FΣN,  φ:ΣN  ⊢     Fφ  ⇔ ∃ℓ:List  N.F(λ n.n∈ℓ) ∧ ∀ n∈ℓ. φ n.

Consider in particular φ≡λ x.σ and F≡λψ.G(ψ 0), for any given σ:Σ and GΣ. Since it’s decidable whether a list is empty or inhabited, ∃ℓ reduces to the disjunction of these two cases, so

Gσ  ≡  Fφ  ⇔ G⊥ ∨ σ∧ G⊤. 

Hence the Phoa principle follows from that of Scott.


11.5.   The Scott axiom for N says that ΣN has a basis as a locally compact space, in the sense of §§5.8f, with

β ≡ λ n.n∈ℓ     and     A ≡ λφ.∀ n∈ℓ.φ n.

This corresponds to the classical description of the Scott topology on ℘(N), whose open sets are U≡{U⊂ℕ ∣ ℓ⊂ U} for all finite ℓ⊂ℕ.

Another way of putting this is that ΣΣN is a retract of ΣN, and it is not difficult to extend this to all objects that are definable using × and Σ(−). Hence any object that is definable in the monadic framework (§6) is a Σ-split subspace of ΣN [Section C 8].

[G] goes on to show how any computably based locally compact Bourbaki space or locale X may be “imported” into ASD. That is, suppose that X has a basis (Kn,Vn) indexed by N, such that the relation (n≺≺ m)≡(KnVm) is recursively enumerable. Then this relation is a term n,m:N⊢(n≺≺ m):Σ satisfying certain properties [Section G 11], from which we may define a nucleus on ΣN [Section G 14], and so a type whose interpretation is X [Section G 17].


11.6.   It is in this representation that we can show that the λ-calculus definitions of primes and nuclei (§§6.36.6) are equivalent to more familiar lattice-theoretic ones [Section G 10].

We can also characterise certain classes of definable objects [Section G 9]:

  1. any overt discrete space is the subquotient of ℕ by some open partial equivalence relation;
  2. any compact overt discrete space is Kuratowski-finite (§9.7); and
  3. any compact Hausdorff overt discrete space is finite, i.e. of the form {mm< n}.


From (a) we may derive definition by description (§9.11), the free monoid (List (N), §9.7) and the Scott principle (§11.4) for all overt discrete N.

Beware, however, that all of these results apply just to objects that are definable in the monadic framework as we gave it in §6. They will need to be proved again, or may cease to be valid, in a more general setting (§12).


11.7.   Even without assuming that N is definable, we may use the intuitions gained from these results to construct List (N) for any overt discrete N. The key idea is to encode any Kuratowski-finite ℓ⊂ N by the pair of modal operators (§8.8) that say that ℓ is overt and compact. Then List (N) is a Σ-split subspace of ΣΣN×ΣΣN. It is obtained using a nucleus that is itself defined as a fixed point, using the basic Scott continuity axiom (§11.1) and a tour de force of techniques in ASD and domain theory [E].

We deduce that the overt discrete objects form an arithmetic universe (§9.7).


11.8.   The general Scott continuity axiom in §11.4 is only meaningful for general overt discrete N that have List (N) or K(N). But we may obtain the latter from either

  1. the underlying set axiom (§10), in which case ℘(N)≡Ω N exists, and K(N)⊂Ω N is the semilattice generated by N [Mik76, Appx 2]; or
  2. fixed points defined by joins of chains (§11.1).

Armed with these, we are in a position to assert the Scott continuity axiom (§11.4) for general overt discrete N.

In the setting of classical topology, the weaker axiom would only provide countable unions of open sets, whereas arbitrary cardinalities are required for the usual theory.

Similarly, in the context of our underlying set axiom, Scott continuity for general general overt discrete objects is exactly what is required to make the monad in §10.5 agree with the one that defines the category of frames over E4.4). The full subcategory of spaces with enough points and enough opens then agrees with the category of sober Bourbaki spaces over E.


11.9.  Turning to the applications of general topology in elementary real analysis, this axiomatic setting (in fact, with just §11.1) is enough to construct the Dedekind reals using the nucleus that we mentioned in §5.12 [I].

We may use this as an experimental test of the prototype axioms (cf. §3.2). The claim is that ASD is a theory of computable topology, and in particular that its terms x:ℝ⊢ a:ℝ exactly capture the computably continuous functions f:ℝ→ℝ. We already know that the interpretation of such a term in the model using locally compact locales (§5.10) is continuous, whilst [K] gives some ideas of how to compute with our calculus.

So, is every classically continuous function f:ℝ→ℝ that can be computed by a program representable in ASD? First we need to agree on some notion of computability, but whatever yours is, I would hope that it could be adapted to provide a program π(q,e,t) that takes three rational arguments and terminates iff e< f(q)< t. Using the denotational semantics of your programming language, interpreted in the domain theory of ASD, π is a term of type Σ3. From this we may derive a morphism g:ℝ→ℝ in ASD whose classical interpretation is the given function f.


11.10.   In foundational studies it has been long been customary to regard ℝ as something constructed from ℕ (cf. §2), and indeed that is what we too have done [I]. However, the importance of ℝ throughout mathematics and science surely justifies introducing it as a base type, especially if we can formulate convincing axioms for it.

For these, we propose that

  1. it is an overt space, with ∃8.10);
  2. it is Hausdorff, with an inequality or apartness relation, ≠ (§8.6);
  3. the closed interval [0,1] is compact (§§1.8, 5.7, 5.12, 8.7, 11.2);
  4. ℝ has a total order < with (xy)⇔ (x< y)∨(y< x);
  5. it is Dedekind complete, in a sense in which the two halves of a cut are open;
  6. it is a field, where x−1 is defined iff x≠ 0;
  7. and Archimedean, i.e. , for x,y:ℝ,
    y> 0  ⇒ ∃ n:ℤ. y(n−1) < xy(n+1).


11.11.   Dedekind completeness plays the same role for ℝ that definition by description (§9.11) does for ℕ, namely to recover numbers from the computation that we do in the arena of logic. Cuts and primes are inter-definable by

(δ,υ)   ≡   (λ d.P(λ x.dx), λ u.P(λ x.xu)) 

and

P  ≡  λφ.∃ du.δ d∧υ u∧∀ x:[d,u].φ x

showing that Dedekind completeness cannot really be separated from the Heine–Borel theorem (Section I 14).

Once again, there is a system of logical rules, in which the definition of a Dedekind cut is the premise of the introduction rule for cut (δ,υ), and the elimination rule represents any a:ℝ by the cut

δ  ≡  λ d.da      υ  ≡  λ u.au.

Like focus and descriptions, Dedekind cut operations may be eliminated everywhere except on the outside of a term. Any cut sub-term has a smallest enclosing sub-term [cut /x]*σ of type Σ (typically <, ≠ or >), and then

[cut (δ,υ)/x]*σ   ⇔   (λ x.σ)cut (δ,υ)  ⇔   ∃ du:ℚ.δ d∧υ u∧∀ x:[d,u].σ.


11.12.  The applications of this construction to elementary real analysis are begun in [J]. The principal objective of this paper is to solve equations defined by continuous functions f:ℝ→ℝ, which makes novel use of overt subspaces. By way of an experimental test of our axioms for ℝ (cf. §3.2), it also proves the traditional characterisation of open subspaces of ℝ as countable unions of disjoint open intervals, although the words “countable” and “interval” need some qualification. This result fails in real analysis without the Heine–Borel theorem, in particular in Bishop’s theory [BB85].

From here there should be no difficulty in developing a theory of differential and integral calculus on ℝn. However, since the version of ASD that we have developed so far only gives an account of locally compact spaces, we cannot study Banach spaces and functional analysis until we have a much more general framework than the one in §6.


Previous Up Next