Re: Dedekind versus Cauchy reals

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

This is a reply to Thomas's post about "Dedekind vs. Cauchy". I am too
young to know why Cauchy reals were preferred by the early
constructivists, so I will reply only to remarks that regard
real-number computation, of which I have more experience.

Thomas gives pragmatic reasons for preferring Cauchy sequences,
actually the rapid ones, with rate of convergence 2^-n. Given a rapid
Cauchy sequence we can easily get an approximation to any desired
degree. On the other hand, Thomas says, a Dedekind real is implemented
as a semidecision procedure, which forces us to _guess_ approximations
to the real. And he says this must be done in parallel, which just
makes things worse.

Firstly, I think arguments which are based too heavily on efficiency
are on a shaky ground. C is faster than Haskell, therefore everyone
should use C. Perhaps nobody has rally tried to implement efficient
Dedekind reals so how can we tell? In fact, as far as I know, nobody
has until last year. By the way, Cauchy sequences with a fixed rate of
convergence are a bad idea if you worry about efficiency. As Norbert
Mueller has demonstrated over the years, it is better to allow Cauchy
sequences (actually sequences of eventually shrinking intervals)
_without_ a priori conditions on the rate of convergence. Somewhat
paradoxically, by allowing arbitrarily slow rate of convergence we are
able to write _faster_ real arithmetic. This is a non-obvious fact
which the practitioners have been trying to get across, but it's not
sticking with the theorists for some reason. Thomas's argument about
AC_N being of only moderate help is true, but in a twisted way: in
practice AC_N is just never used explicitly, and moduli of continuity,
even fixed ones like 2^-n, are avoided at all cost.

Secondly, there are other criteria by which we should judge an
implementation. One of them is expressivity and the level of
abstraction. With the Dedekind reals certain concepts are more easily
expressed. For example, if one wants to talk constructively about
compactness of the closed interval, Cauchy reals will not be of much
help (unless you essentially declare [0,1] to be compact), whereas
locale-theoretic constructions in the style of Dedekind will work
better.

Lastly, since my computer believes in number choice, there really is
no dilemma. The Cauchy and Dedekind reals _must_ be equivalent to the
computer. Paul Taylor and I have devised algorithms for efficient,
sequential computation with Dedekind reals which use the equivalence
with Cauchy reals under the hood (at least I think that's what is
going on, but I do not fully understand the whole thing yet). There is
no need to think of a Dedekind real as a clumsy semidecision
procedure. Instead, the left and the right cut may be seen as
instructions for calculating better approximations from existing ones.
This can be done quite efficiently with Newton's method (the variant
for interval arithmetic). The computation that comes out then behaves
very much like an iterative procedure for computing a Cauchy sequence.

Best regards,

Andrej