The Dedekind Reals in Abstract Stone Duality

The Dedekind Reals in Abstract Stone Duality

[Paul Taylor]

	The Dedekind Reals in Abstract Stone Duality
		www.PaulTaylor.EU/ASD

Andrej Bauer is a co-author of this paper, but not of this posting
about it.

We construct something that was supposed to be impossible: a model of
(topology containing) the real line that satisfies the Heine--Borel
theorem (the closed interval is compact in the "finite open sub-cover"
sense) but in which all terms are computable.

This fails in the "obvious" model of recursive analysis, ie the subset
of real numbers that are representable by programs, roughly because we
can enumerate them, and cover them with intervals of length m.2^-k for
any chosen m (say 1/4). Then recursive [0,1] is covered by total length
2m (=1/2), but no finite subcover is enough.   The clearest account of
this counterexample that I have seen is in Bridges & Richman,
"Varieties of Constructive Mathematics", LMS Lecture Notes 97,
CUP, 1987, Section 3.4.

The reason why the Heine--Borel theorem holds in ASD is that, like
locale theory and formal topology, it is an account of topology based
on open subspaces and not points.   But, unlike them, ASD is presented
as a lambda calculus that makes it LOOK like a point-based theory, and
therefore shows up exactly what the difference is.

This paper appeared in the proceedings of "Computability and
Complexity in Analysis" (Kyoto, August 2005), but since then it has
been completely rewritten, and almost every lemma has been re-thought
-- so it's worth re-reading.  It now provides the best available
introduction to the construction of topology in ASD, and also compares
the construction and properties of the real line in ASD with those in
locale theory, formal topology and constructive analysis.

SS 11-13 of the paper also consider real arithmetic and the relationship
between Dedekind completeness and the Archimedean axiom.

It has just been submitted to a journal, so we would still welcome
comments.

Below I shall explain the category theoretic idea behind this
construction.  For further discussion of constructive analysis in ASD,
you should see SS 1 & 15 of the paper itself, and "A Lambda
Calculus for Real Analysis", which was also presented at CCA 2005,
and has been revised a lot, but is not yet ready to go to a journal.

---

Before I describe this work, I feel that the time has come to make a
disclaimer:
      ABSTRACT STONE DUALITY IS *NOT* ESCARDO'S SYNTHETIC TOPOLOGY

Martin Escardo's paper "Synthetic topology of data types and classical
spaces" (ENTCS 87 (2004) 21--156 or www.cs.bham.ac.uk/~mhe) is a very
interesting collection of material drawn from the literature on the
boundaries of topology and recursion theory.  If it had been written
by somebody ten years earlier, as it could and perhaps should have been,
it would have provided a very useful background to my work on ASD.

However, the main use to which I would have put an earlier version of
that paper would have been to say WHAT ASD IS NOT.  In particular,
Martin describes the failure of compactness of Cantor space and of the
closed real interval in recursive analysis.  The theory that he then
discusses is a form of "relative computability", which bolts recursion
theory on to classical topology.  The best developed form of this
approach is Klaus Weihrauch's "Type Two Effectivity", on which Vasco
Brattka (www.cca-net.de/vasco) is the most productive researcher.

In ASD, Cantor space and [0,1] are compact, but this is not achieved
by bolting recursion theory on to classical topology.  ASD is a direct
axiomatisation of the ideas of general topology, not based on set
theory or recursion theory.

The features that are common to Martin's work and mine are that
  - the topology on a space X is seen as the exponential Sigma^X,
    where Sigma is the Sierpinski space; I would attribute this to
    Dana Scott's "Continuous Lattices" (LNM 274 (1972) 97-136); and

  - compactness of a space K is captured by a "universal quantifier"
    all_K : Sigma^K -> Sigma;  I picked up this idea from 1970s locale
    theory and categorical logic.

I took these ideas for granted a long time ago, they appeared in the
first ASD paper in 2000, and I have since developed them into a
complete axiomatisation of computably based locally compact spaces.

If Martin had developed his own calculus for topology based on similar
ideas, it would have been possible to write (the paper and) this
posting as an ordinary comparison of scientific theories, just as we
do with locale theory, etc: "the Heine--Borel theorem holds in ASD but
not in Escardo's calculus because of such-and-such".

Unfortunately, there is no "Escardo's calculus".  Indeed, I recently
put it to him that he could eliminate the friction between us either
by working with me on ASD, or by proposing some other axiom system,
but he declined.  He doesn't want to take a view on whether
Heine--Borel is true or false.  Therefore no scientific comparison
is possible, and I have to make this disclaimer instead.

However, the reason why I consider it necessary to make such a
statement is not actually because of Martin himself. His research is
not my business, and this is not an issue of priority or plagiarism.
My complaint is against those who go around saying that Martin presents
MY work better than I do myself, whereas in fact the fundamental
ideas of ASD (see below) get no mention in his account.

I encourage Martin to clarify (on "categories") both which specific
results he claims as HIS OWN, and more generally what the message of
"Synthetic Topology" is, as distinct from ASD.  On the other hand,
I would ask other people to read my papers properly.

----

THE MONADIC PRINCIPLE

As a research programme, ASD is an example of a maxim due to Paul
Dirac that Ronnie Brown quoted on "categories" on 8 June 2007:

 >>  One should allow oneself to be led in the direction which the
 >>  mathematics suggests... one must follow up a mathematical idea
 >>  and see what its consequences are, even though one gets led to
 >>  a domain which is completely foreign to what one started
 >>  with.... Mathematics can lead us in a direction we would not
 >>  take if we only followed up physical ideas by themselves.

The mathematical idea that I followed in this way was a standard
categorical one, and the following account is intended for
categorists.  It explains how the application of this idea led
"directly" to important fundamental principles in real analysis.

The idea (in 1993) was that, not only is the topology on X given by
the exponential Sigma^X as above, but also

    the self-adjunction   Sigma^(-)  -|   Sigma^(-)  is monadic.

I still don't know where I picked up the idea that adjunctions "ought"
to be monadic.  Maybe it was just that lots of interesting categories
turn up that way.  The main inspiration was Bob Pare's "Colimits in
Topoi" (Bull AMS 80 (1974) 556), where he shows that any elementary
topos has this property, with Sigma=Omega.

A famous theorem of Jon Beck characterises monadic adjunctions
F -| U  by two clauses:
- U reflects invertibility, and
- U preserves U-split coequalisers.

----

SOBRIETY

In the context of ASD, the first clause is equivalent to saying that
every object X is SOBER, ie it is the equaliser of the diagram

                            eta_Sigma^2 X         Sigma^ Sigma^X
         eta_X      Sigma^X ------------>     Sigma
     X  >-----> Sigma       ------------> Sigma
                            Sigma^2 eta_X

When we apply this principle to the two most important ground types of
mathematics (in the context of suitable extra structure), we find that

- sobriety for N is equivalent to definition by description
   (Sober Spaces and Continuations, SS 9-10)

- sobriety for R is equivalent to Dedekind completeness
   (Dedekind Reals in ASD, S 14).

Sobriety is slightly stronger than the property of repleteness that
Martin Hyland introduced in synthetic domain theory in 1991.

Essentially, all of these ideas say HOW LOGIC IMPACTS ON NUMERICAL
COMPUTATION.  They can be formulated as "introduction rules" in a
type-theoretic style in which the elimination rules are given by
equality, arithmetic order or lambda-application.  To put this another
way, sobriety completes the square of types of operations:

         results:  numerical              logical
   arguments:
     numerical:    arithmetic (+ - x /)   relations (= < > !=)

       logical:    sobriety (cut descr)   logic (and or exists all)

There are normalisation theorems that say that any numerical term
built from these four sets of operations is equivalent to a purely
logical one, with numerical variables and constants on the inside and
a single sobriety operator on the outside.  Computation is then by
logic programming. (See "Interval analysis without intervals".)

-----

MONADICITY

Turning to the more difficult half of Beck's theorem, this yields
the Heine--Borel theorem, and also compactness of Cantor space, 2^N.

In fact it was already known that (Dedekind completeness and) the
Heine--Borel theorem are consequences of the view that the algebra
of open sets is fundamental in topology, and not the set of points.
Fourman & Hyland showed this for locales (LNM 753 (1979) 280-301)
and Negri for formal topology (LNCS 1158 (1996)).  Because of the
monadic principle, ASD is also an "open sets" account of topology.

We say that a subspace   i : X >---> Y  is  SIGMA-SPLIT  if there's
a map   I : Sigma^X >---> Sigma^Y  such that  Sigma^i . I = id.
Monadicity provides for the existence of Sigma-split subspaces.

The representation of reals as Dedekind cuts defines a subspace
     i : R >--->  Sigma^Q x Sigma^Q

The crucial observation (in S 2 of "Dedekind reals in ASD") is that
this subspace is Sigma-split, classically, using the fact that [0,1]
is compact.  (This result is already significant in interval analysis:
it says that interval computations can be made arbitarily accurate by
making the interval arguments narrow enough.)

The idempotent composite E = I . Sigma^i can be expressed entirely in
terms of the rationals, not the reals.  This is the key idea of the
construction of R in ASD (S 8), and the same formula E turns up again
in the definitions of the quantifiers that make [0,1] compact and R
overt (SS 9-10):
     all  x:[d,u].phi x   =   I phi (lambda x.x<d, lambda x.u<x)
     some x:[d,u].phi x   =   I phi (lambda x.x<u, lambda x.d<x)
S 14 reproduces the classical argument in ASD to show that R is unique.

Altogether, the Sigma-splitting I and the universal quantifier
all_[0,1] are inter-definable.  In the models of recursive analysis
where Heine--Borel fails, the map I also does not exist (or if it
does, it's not Scott continuous).  If, as Martin Escardo does, you
believe that compactness is defined by a quantifier Sigma^K -> Sigma,
ie a term of one higher type, surely you should be willing to accept
an inter-definable term of another higher type (I:Sigma^X >---> Sigma^Y)
as the categorical explanation of the Heine--Borel theorem. This term
also exists in the "relative computability" models: what ASD does is
to abstract the computable, topological ideas away from proofs that
rely on non-topological, non-computable set-theoretic hypotheses.

Sigma-split subspaces also provide a simple categorical
characterisation of local compactness: X is locally compact iff it can
be expressed as a Sigma-split subspace of Sigma^N.  ("Computably
based locally compact spaces".)

----

THE MONADIC LAMBDA CALCULUS

What sets ASD apart from locale theory and formal topology is that it
LOOKS as if it's based on "points", whereas locale theory looks like
lattice theory, and formal topology works with basic open sets and
coverage relations.

How does ASD manage this?

We now have 40 years experience of the interpretation of lambda
calculi (predicate calculus, type theories, etc) in categories.
We know, in particular, that the introduction, elimination, beta
and eta rules for a logical connective correspond to various
features of an adjunction between functors (see S 7.2 of my book).

Now that we have seen this correspondence for numerous logical
operations, we can turn it around: given an adjunction between
functors, we might be able to design a formal calculus that
corresponds to it.

That is what "Subspaces in ASD" does with the monadic property.

It allows one to work in a natural way with the given structure of the
category (in particular N and the lattice Sigma), but then to introduce
Sigma-split subspaces given certain "subspace data" called a NUCLEUS.
This word was appropriated from locale theory because nuclei serve the
same essential purpose in both cases, but the definitions are slightly
different.

It is important to understand that the "subspaces" in this calculus
are not subsets.  Putting this back in categorical language, SS 4--6
of that paper constructs the monadic category by formally adjoining
NEW Sigma-split equalisers.

----

THE EUCLIDEAN & PHOA PRINCIPLES

I want to stick to one categorical idea in this posting, but I should
also point out that the thing that made monadicity look like topology
rather than just category theory or lambda calculus was the Phoa
principle.  The "Frobenius laws" for open and proper maps follow from
this.  (These things are not in "Synthetic Topology" either.)

This says that open and closed subspaces of X are in bijection, not
because of set-theoretic complementation, but because they each
correspond bijectively to maps  X --> Sigma.  Whereas locale theory
has infinite joins but finite meets, and there are double negations
all over the place in intuitionistic analysis,  ASD has a very
strong duality between open and closed ideas.   This is applied
to connectedness and (approximate forms of) the intermediate value
theorem in "Lambda calculus for real analysis".

The "miracle" that led to my working full time on ASD was the
relationship between the Euclidean principle and dominances,
and the fact that overt discrete spaces form a pretopos
(See "Geometric and higher order logic").

---

DIFFICULTIES WITH THE ASD PROGRAMME

I want to cross-examine the charge that I cannot present my own work.

It has turned out that the nucleus that we use to construct R is the
simplest non-trivial example, and the one that is best motivated by
other considerations.  It is a pity that I did not know this ten years
ago, and that I was so reluctant to do real analysis.  Instead, I
spent a lot of time developing more general locally compact spaces,
and also overt discrete ones.  However, the construction of the
Dedekind reals involves topological and combinatorial arguments
that we can now present with confidence ONLY BECAUSE I had previously
done a thorough study of them.

Working with ASD nuclei is extremely difficult.  For each one,
several sections of a paper are needed simply to show that some
bizarre formula satisfies another bizarre equation.  The proofs
are long and intricate because the axioms are very weak and the
techniques are novel.

The reason for this difficulty is that I am working with monads and
Beck's theorem.  Let me point out some history.  Although this result
appears in many textbooks (including mine), Jon Beck never wrote it up
himself.  He might have taught us about non-Abelian cohomology, and
what "exactness" means for general algebras, except that his thesis
advisers told him that homological algebra had to be done with Abelian
groups.  In that subject, there is a black art of finding contraction
maps.  Beautiful though monadic adjunctions are, they don't compose.
Altogether, Beck's theorem was a very awkward beast long before
I had even heard of category theory.

I feel that, with the monadic lambda calculus, I have begun to tame
this beast.  (Moggi's calculus did so too, but that worked with the
Kleisli category, not the Eilenberg--Moore one that is crucial to
Heine--Borel.)  Whereas locale theory, formal topology, topos theory
and algebraic geometry stuck to the abstract algebra, ASD turns it
into topological notation. Constructing new spaces with nuclei may
still be a black art, for the reasons that I have mentioned, but the
continuous functions between them are handled very naturally.

----

BEYOND LOCAL COMPACTNESS

The awkwardness of working with (the monad and) nuclei is directly
related to the difficulty in generalising them beyond locally compact
spaces.  The point is that we want general equalisers and function
spaces
without sacrificing the principle of using the algebra of open
subspaces.

Actually, I have plenty of proposals for more general AXIOMS, and for
theorems that we might prove with them.

The problem with Beck's theorem lies in the restricted form of the
second clause.  There are several interesting cases of monads where
the forgetful functor   U : A=Algebras --> C=Carriers  PRESERVES
ALL REFLEXIVE COEQUALISERS.
  - Pare's theorem, for any topos C;
  - Richard Wood's A=CCD, C=CCC^op;
  - A=Frm, C=Dcpo;
  - C=Set, A= algebras for any single-sorted finitary algebraic theory.

Unfortunately, I have no idea how to construct such a category for
topology in the ASD formulation.  There are plenty of cartesian closed
supercategories of topological spaces, but they are point-based.
Reinhold Heckmann constructed a CCC in which the category of locales
is reflective (MSCS 16 (2006) 231--253), but this relies on the Axiom
of Collection, and I don't think that it yields what I want either.

Another possibility is a sheaf topos over the effective topos, which
provides a model of ASD that has all exponentials and finite limits.
However, whilst it satisfies the Heine--Borel theorem, there will
be higher-type analogues of the failure in recursive analysis.

Maybe we should look for models that just satisfy specific instances
of this property. The underlying principle seems to be this:

    given a parallel pair (u,v) of homomorphisms of algebras
    and a function f with f.u = f.v,

    under what circumstances does f factor through a homomorphism w
    with w.u = w.v?

Heine--Borel, monadicity, injectivity of Sigma, and the Beck--Chevalley
condition for open and proper maps seem to be examples of this
principle.

Can we find models based on traditional topology, locale theory,
formal topology or recursion theory that satisfy it in more cases?

----

CONCLUSION

Synthetic Topology interprets ideas of general topology in cartesian
closed categories and lambda calculus.  Abstract Stone Duality shows
that, in order to make the topology work PROPERLY (with the
Heine--Borel theorem etc), we need to postulate additional higher
type lambda terms associated with subspaces.

I have just stated what I think the challenge is regarding the
construction of more general models.  Separate from this are other
challenges in real analysis and computation.

I have taken the intellectual and personal risks and done much of the
groundwork to demonstrate the viability of ASD as an approach to
constructive topology and analysis.  It seems to me that these
challenges are worthy of the attention of the best categorical minds.
However, it will only be possible to achieve these things if my
colleagues are willing to make a professional study and assessment of
what has already been done in ASD.

Paul Taylor
pt07 @ PaulTaylor.EU
www.PaulTaylor.EU/ASD