The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

I was actually thinking about a type-theoretical model of real numbers which 
would use both a number of meaningful digits *and* the exponent. Neither of 
the standard models seems to use exponent as a part of the description.

Vladimir.





On Jun 23, 2012, at 1:05 PM, Andrej Bauer wrote:

>> 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