The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

> 2012/6/23 Vladimir Voevodsky 
> <vladimir AT ias.edu>:
>> I wonder if someone tried to build a constructive model of real numbers 
>> starting with the floating point representations of increasing precision?
>>
>> Vladimir.

I wonder if anybody's done a development based on a real number being
an almost-homomorphism from Z -> Z, i.e. a function f such that for
some C, |f(m+n) - f(m) - f(n)| <= C.  (Where, of course, we think of
f(n) as a series of approximations to alpha*n for some real number
alpha -- and then addition is pointwise addition, multiplication is
composition, f==g if |f(n)-g(n)| is bounded, etc.)  If you keep C in
the type domain, that should make it possible to do (theoretically)
effective computations with such real numbers.  And in fact, by
replacing f with fun n => round (f(C*n) / C), it should be possible to
reduce C to 1 or 2, which could be important for some completeness
computations.

Of course, ahead of time it might be hard to tell whether this
actually gives an effective computation method, or whether in practice
C would explode to the point that it's virtually useless.
-- 
Daniel Schepler