The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

Le lundi 25 juin 2012 à 07:27 -0700, Daniel Schepler a écrit :
> > 2012/6/23 Vladimir Voevodsky:
> >> 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 I remember correctly, that's the way John Harrison defined positive
real numbers in HOL (except that f : N -> N) and C was equal to 1.
Effective computation was possible, though it was not the main point of
the development.

Depending on your point of view, Nicolas Julien's PhD thesis about real
numbers as coinductive digit sequences in Coq may fit into this category
too. That time, effective computation was one of the goals.

Best regards,

Guillaume