Re: Dedekind versus Cauchy reals

[Andrej Bauer <andrej.bauer@andrej.com>]

On Sun, Feb 15, 2009 at 7:50 AM, Vaughan Pratt <pratt@cs.stanford.edu> wrote:
> If everything can be related to interval arithmetic in one way or
> another, why not take interval arithmetic itself as the gold standard
> for the constructive reals?  The Edalat-Escardo-Potter domain-theoretic
> analysis of interval arithmetic struck me as sufficiently canonical that
> I don't understand why all the alternatives aren't being evaluated
> relative to that one.  Are there alternatives that compensate for some
> shortcoming of interval arithmetic as understood through the lens of
> domain theory?

I essentially agree with you, namely that interval arithmetic
(actually, the interval domain) plays a fundamental role in the
construction of reals, as well as in practical computation (the
fastest implementations use interval arithmetic on top of
multiple-precision floating point).

A result of Vasco Brattka says that any two implementations of the
structure of reals (arithmetic, abs, semidecidable <, limit operator
for rapid sequences) are computably isomorphic. This can be
interpreted as saying that the domain-theoretic reals are as good as
any other version.

One reason why this is not the end of the story is that we do not
understand what happens at higher types. Vasco tells us that given two
versions of reals, R1 and R2, they are computably isomorphic. But how
about functions R1 -> R1, functionals (R1 -> R1) -> R1 and other
higher types?

For example, if R1 is the domain-theoretic reals (constructed as the
maximal elements of the interval domain) and R2 is the "Cauchy reals"
(represented as streams of digits, including negative digits), then we
know that the hierachies

R1,  R1 -> R1,  (R1 -> R1) -> R1, ...

and

R2,  R2 -> R2,  (R2 -> R2) -> R2, ...

agree in the first three terms, but do not know what happens after
that. This was established by Alex Simpson, Martin Escardo and myself.
Dag Normann has also investigated the two hierarchies.

For the familiar case of natural numbers John Longley has shown  that
"in nature" there are only three versions of the hierachy

N,  N -> N,  (N -> N) -> N, ...

These are the hereditarily effective operators, the Kleene-Kreisel
continuous functionals, and a "mixed" version (the computable
Kleene-Kreisel continuous functionals). We would like to have a result
like that for reals, but we're stuck with the continuous version of
the hierarchy at rank 3.

In terms of implementation, the question is the following: does it
matter whether the reals are implemented transparently (the programmer
has access to their internal representation) or opaquely (reals are
values of an abstract data type whose internal workings cannot be
inspected)? We know that up to types of rank 2 it does not matter.

Until such questions are answered, settling with a single construction
or theory of real number computation is premature.

By the way, can you give a single interesting _total_ functional of
type ((R -> R) -> R) -> R? (Please don't ask me to define
"interesting".)

Andrej