Whether the closed interval is, or ought to be, compact in computable and constructive mathematics is a question that never ceases to be interesting. This is partly because compactness is such an important property for a topological space to have, and partly because there are several schools of constructive and computable mathematics that disagree about the answer, each of which sets up its own framework, differing slightly from all the others. The matter is made all the more confusing by the number of different definitions of compactness that have been given, even classically [Bou66, §I 9]. In this section we make a few observations about compactness of the closed interval in ASD and how it relates to various other schools of computability.
Most urgently, we hear alarm bells ringing in the minds of recursive analysts. On the one hand, we saw in Remark 3.4 that there is a model of ASD in which maps are precisely the computable maps between computably based locally compact spaces. On the other, Section 10 proved that the closed interval is compact. If all functions are computable, then surely we should be able to use some enumeration of the definable points of the closed interval to show that it is not compact?
Remark 15.1
In Recursive Analysis, the closed interval [0,1] can be
shown not to be compact by means of a singular cover,
i.e. a countable cover by open intervals with rational endpoints
whose total length is bounded above by ½.
It can be shown that no finite sub-cover of a singular cover is a cover
of [0,1],
see [TvD88, §6.4.3] or [BR87, §3.4].
Such covers exist in Recursive Analysis [TvD88, §6.4.2]
because of the formal Church’s Thesis CT0
[TvD88, §3.3.2],
which states that every function ℕ → ℕ has a Gödel code.
(With hindsight,
it would have been more natural to enumerate ℕ → ℕ⊥,
but this is the way in which CT0 is usually stated.)
It follows that every real number has a Gödel code, too.
In classical recursion theory, a singular cover is described as a
computable enumeration of open intervals with rational endpoints of
bounded total length which effectively covers all computable reals.
Example 15.2
The closed interval may also fail to be compact
for reasons that have nothing to do with computability.
The construction of the “Dedekind reals” R
as the equaliser in Remark 6.9
can be done in any category with finite limits, certain exponentials
and some mild assumptions on Σℕ, as in Section 4.
An example is the category Dcpo of posets with
directed joins and Scott-continuous functions.
Here the equaliser carries the discrete (“specialisation”) order,
but in this category the order determines the topology.
The object R therefore also carries the discrete topology,
so ΣR is the powerset ℘(R) with the Scott topology,
and the only compact subsets of R are the finite ones.
Hence the predicate [d,u]⊂ U is not continuous in U.
The formula in Proposition 2.15 gives an element of ΣΣℚ×Σℚ
for each U⊂ R,
but the function I is not Scott-continuous,
so it does not yield a sound interpretation of the ASD calculus
(Warning 5.17).
Remark 15.3
One resolution of the abnormalities of Recursive Analysis
that has been adopted by several schools
is that of relative computability,
in which the maps are computable,
but the spaces are the classical topological ones,
i.e. they have “all” points instead of just the computable ones.
Each space is also equipped with a “computability” structure,
such as an enumeration of basic open sets,
that is used to specify which continuous maps are computable.
Examples are
(one variant of) Type Two Effectivity [Wei00],
and computable equilogical spaces [Bau00].
Another is Martín Escardó’s synthetic topology of data types
[Esc04], but beware that,
whilst this is very similar to the calculus in Section 4,
it lacks the crucial monadic property of ASD (Section 5).
In all of these three settings, the closed interval is compact,
the proof being the well known classical one.
In particular, Escardó stresses the need for “all” points,
as compactness would fail in a purely recursive version of his theory.
Remark 15.4
The sceptical pupil from the Russian School will not be so easily convinced,
but will press us on the structure of the syntactic term model of ASD,
in which the objects are types and the morphisms are the definable maps.
Since everything is enumerable in such a model,
one might expect to obtain a singular cover,
and so non-compactness of the closed interval.
Indeed, by following the usual construction,
we could define a sequence of intervals with rational endpoints, (an, bn),
whose total length is bounded by ½,
and prove the meta-theorem that
| “if ⊢ t : [0,1] then ⊢ ∃ n:ℕ . an < t < bn ”. |
However, it does not follow that (an, bn) covers [0,1], by which we mean
| x : [0,1] ⊢ ∃ n:ℕ. an < x < bn, |
because that would be to confuse a family of theorems about all definable closed terms t with a single theorem containing a free variable x. In category theory, the calculus is said to be not well pointed. Even though its morphisms are recursively enumerable, there are not enough of them 1→ R to cover the equaliser.
Example 15.5
As a final attempt to break compactness of the closed interval in ASD,
we might try to interpret it in a setting,
such as Markov’s Recursive Mathematics,
in which the formal Church’s Thesis CT0 holds.
A useful formulation of this is the category PER
of partial equivalence relations over Stephen Kleene’s first algebra
[Kle45],
or Martin Hyland’s larger effective topos, Eff [Hyl82].
We try to interpret ASD in PER or Eff in the natural way, using the universal properties of ℕ, products, equalisers and exponentials. For Σ we take the object of semidecidable propositions. This yields a valid interpretation of the language and construction of Sections 4 and 6, so that the equaliser R in Remark 6.9 is perhaps a reasonable candidate for the “real line” in these worlds.
However, we do not have a sound interpretation of Σ-split subspaces, because the map I that Remark 5.17 requires need not exist. In particular, the object ΣR does not have the properties of the “Euclidean” topology, and the closed interval is not compact.
In PER, the formula in Proposition 2.15 does not define a morphism I because [d,u] ⊂ U is not a completely r.e. predicate (in d, u and U). In the internal language of Eff, the sub-expression ∀ x:[d,u].x∈ U is a term of type Ω but not Σ. Consequently, the formula defines a morphism I from ΣR to ΩΣℚ×Σℚ and not to ΣΣℚ×Σℚ.
This situation is better documented for Cantor space:
Example 15.6
Richard Friedberg [Fri58]
defined an effective operation on the set of total recursive functions
ℕ→ℕ that is not the restriction of a recursive functional.
See [Rog92, §15.3.XXXI]
for another account of this construction,
which also works for the total recursive binary sequences ℕ→2.
In the effective topos we can reformulate Friedberg’s example by saying that the topology of 2ℕ (i.e. the object Σ2ℕ) is not the subspace topology induced by the inclusion 2ℕ⊂ 2⊥ℕ. In this topos, 2ℕ is actually homeomorphic to ℕℕ, so neither of these spaces can be locally compact, and their topology is not the subspace topology of 2⊥ℕ.
In the construction of 2ℕ in ASD [L], on the other hand, the space 2⊥ℕ of partial functions from ℕ to 2 plays a role similar to that of IR in Sections 7–8, being a closed subspace of Σℕ×Σℕ. Then 2ℕ⊂2⊥ℕ is defined by a nucleus that satisfies both the ASD and localic definitions. The quantifier ∀ that says that 2ℕ is compact is obtained from this nucleus in a similar way to that for [d,u].
Escardó [Esc04] has shown how ∀ for 2ℕ may be implemented as a program in Haskell. He proved its correctness using relative computability (Remark 15.3), but this may also be done using the monadic principle in ASD.
Remark 15.7 You may be left thinking that models of ASD are complicated,
mysterious and hard to find. In fact, the calculus has interpretations
in many kinds of classical or constructive set, type or topos theory.
It is more accurate to say that these interpretations can be
based on other foundational systems, because we obtain a model
of our calculus by doing a construction on top of a system with
weaker properties.
In other words, whilst the direct interpretation in PER and Eff
in Example 15.5 does not work,
a slightly more involved one does.
Theorem 15.8 Let (C,Σ) be a model of the axioms
in Section 4,
in particular with products and powers ΣX.
Suppose also that idempotents split in C.
Then Aop is a model of ASD,
where A is the category of Eilenberg–Moore algebras for the monad
arising from Σ(−)⊣Σ(−) [B]. ▫
Remark 15.9 Any category that results from this construction contains
(the sober objects of) the original one (and more),
and the embedding preserves Σ(−).
However, many other constructions are not preserved,
important examples being, of course, Cantor space and the Dedekind reals
as we have defined them.
Whilst these objects may have had undesirable properties in the original structure, their analogues in the new one turn out to behave as the mainstream mathematician would expect. The new objects are by definition the exponentials, equalisers, etc. for the same data in the new category, whilst (the images of) the old objects are relieved of their former duties.
This construction can be carried out for all of the well known models of computable mathematics, including Recursive Mathematics, domain-theoretic PER models and Type Two Effectivity. For example, when we apply it to the category CL of continuous lattices and Scott-continuous functions, we obtain the category LKLoc of locally compact locales. It would be interesting and fruitful to do this in detail for the other cases, and, in particular, to compare their collections of overt objects.
On the other hand, these models have other significant properties besides those given in Section 4, which it may not be easy to reproduce in the new category. For example, CL is cartesian closed, but LKLoc is not.
Theorem 15.10 Over the effective topos Eff there is a sheaf topos EffA
that has a model Aop of ASD as a reflective subcategory.4
Proof There is an internal category C∈Eff of PERs that is weakly equivalent to a reflective subcategory C⊂Eff of Ω¬¬-discrete objects [HR90]. (This situation is a peculiarity of realisability toposes, and the weakness of the equivalence is essential: Peter Freyd observed in the 1960s that, classically, any small complete category is a lattice [Tay99, Example 7.3.2(k)], and this extends to Grothendieck toposes.)
Now let A be the internal Eilenberg–Moore category for the monad over C within Eff, and A the external one over C (or equivalently over Eff). Then by Theorem 15.8, both Aop and Aop are models of ASD.
Since Aop is an internal category, i.e. a small one in classical language, we may form the sheaf topos EffA. But Aop and Aop are weakly equivalent to each other, and therefore to a full subcategory of EffA, by the Yoneda embedding. On the other hand, Aop is also totally cocomplete (see [Kel86, Corollary 6.5] in particular, but the theory was developed in [SW78, Str80, Tho80, Woo82]), so this full subcategory is reflective in EffA. ▫
Remark 15.11 Altogether, it is often very interesting (and not just for
gladiatorial reasons) to investigate the conflicts between one view
of the mathematical world and another,
because the resolution of such conflicts often leads to powerful applications.
It is therefore perhaps a little disappointing that we have not managed
to bring ASD into confrontation, let alone conflict, with singular covers
and similar recursive phenomena.
The explanation is simply that, as we have shown, the quantifier ∀ that encodes compactness of the closed interval is inter-definable with the map I that we introduced classically in Proposition 2.15. The systems in which the Heine–Borel theorem is true are exactly those in which I is definable. In any particular system, there may be some difficult proof of the existence of ∀ and I, but in ASD, the latter is given, essentially axiomatically, by the monadic principle.