coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Daniel Schepler <dschepler AT gmail.com>
- To: Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] real numbers
- Date: Mon, 25 Jun 2012 07:27:03 -0700
> 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
- [Coq-Club] real numbers, Vladimir Voevodsky, 06/23/2012
- Re: [Coq-Club] real numbers, Jonas Oberhauser, 06/23/2012
- Re: [Coq-Club] real numbers, Daniel Schepler, 06/25/2012
- Re: [Coq-Club] real numbers, Guillaume Melquiond, 06/25/2012
- Re: [Coq-Club] real numbers, Yves Bertot, 06/26/2012
- Re: [Coq-Club] real numbers, Guillaume Melquiond, 06/25/2012
- Re: [Coq-Club] real numbers, Daniel Schepler, 06/25/2012
- Re: [Coq-Club] real numbers, Andrej Bauer, 06/23/2012
- Re: [Coq-Club] real numbers, Freek Wiedijk, 06/23/2012
- Re: [Coq-Club] real numbers, Andrej Bauer, 06/23/2012
- Re: [Coq-Club] real numbers, Freek Wiedijk, 06/23/2012
- Re: [Coq-Club] real numbers, Andrej Bauer, 06/23/2012
- Re: [Coq-Club] real numbers, Freek Wiedijk, 06/23/2012
- Re: [Coq-Club] real numbers, Andrej Bauer, 06/23/2012
- Re: [Coq-Club] real numbers, Vladimir Voevodsky, 06/24/2012
- Re: [Coq-Club] real numbers, Andrej Bauer, 06/24/2012
- Re: [Coq-Club] real numbers, Freek Wiedijk, 06/24/2012
- Re: [Coq-Club] real numbers, Andrej Bauer, 06/24/2012
- Re: [Coq-Club] real numbers, Freek Wiedijk, 06/23/2012
- Re: [Coq-Club] real numbers, Jonas Oberhauser, 06/23/2012
Archive powered by MHonArc 2.6.18.