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