The Coq mailing list

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

> I wonder if someone tried to build a constructive model of real numbers 
> starting with the floating point representations of increasing precision?

There is a minor industry devoted to arbitrary-precision computation
with real numbers. But instead of "increasing precision floating
point" we usually speak of "dyadic rationals" (which is exactly the
same thing).

The most relevant for this list is probably Robbert Krebbers and Bas
Spitters' formalization in Coq, see
http://arxiv.org/pdf/1105.2751.pdf, which I think builds on an earlier
implementation by Russell O'Connor, see
http://arxiv.org/pdf/0805.2438.pdf

There is work by Iztok Kavkler and myself. We took a constructive
theory of domains (in real number computation one is very quickly lead
to consider spaces of intervals, which are domains in the sense of
domain theory) and implemented reals by interpreting the constructive
theory in a realizability model based on Ocaml. (So this one is not
formalized, but it is a constructive model.) See
http://math.andrej.com/2008/01/31/a-constructive-theory-of-domains-suitable-for-implementation/

Another approach is that of Paul Taylor and myself. It is a
constructive theory of reals as (two-sided) Dedekind cuts. The theory
is very weak, essentially a restricted form of lambda calculus with
some extra stuff (a space of semidecidable truth values). We developed
a programming language based on the theory, called Marshall, see
https://github.com/andrejbauer/marshall . The etc/haskell subdirectory
contains yet another implementation of exact reals in Haskell, where a
real is represented as a nested sequence of intervals -- here again we
take care to follow an underlying constructive theory. The theory is
described in http://www.monad.me.uk/ASD/analysis.php#dedras ans see
also "A Lambda Calculus for Real Analysis" on the same page.

Of course, there are much older constructive treatments of reals, but
those are typically not interested in actual computation.

Moving on from constructive to computable treatments, one should
definitely mention Norbert Mueller's iRRAM, http://irram.uni-trier.de/
. It is a venerable C++ implementation, and quite likely the fastest
one around, but the underlying theory follows more closely ideas of
computable analysis (http://cca-net.de/publications/books.html).

There are other implementations, but all that I am aware of don't
really measure up to Norbert's iRRAM, execpt for Branimir Lambov's
RealLib (I would be delighted to hear of other efficient
implementations with a clear theoretical model).

With kind regards,

Andrej