The Coq mailing list

[roconnor AT theorem.ca]

On Mon, 2 Jul 2007, Guillaume Melquiond wrote:

> I'm interested in Ziv's strategy for evaluating correctly rounded
> floating-point approximations of real numbers. The idea is quite simple,
> you repeat your computations with increasing precision until you know
> you have got the correct result (it is just a matter of looking at the
> last digits of the approximation).
>
> Images of non-trivial floating-point numbers by elementary functions are
> transcendental numbers, so the functions do terminate because the digit
> pattern is guaranteed to become acceptable. The proof is trivial, since
> approximations cannot get closer than a certain threshold to a given
> rational number, by definition of transcendental numbers.

So the correctness of this function is based on a theorem that the image 
of a rational point under an elementary function is almost always 
irrational.  isIrrational would be defined something like:

Definition isIrrational x :=
forall (q:Q), exists (e:Q), 0 < e /\ (q < approximate x e - e \/
                                      approximate x e + e < q)

where approximate x e is a returns a rational approximation of x within e.

This statement is a Pi_2 statement, so it is almost certainly provable 
without classical logic.  Then one can proceed with Ziv's algorithm. 
There is only one rational number that an approximation could be too close 
to know how to round correctly.  By apply the above theorem one can 
construct some e that would be a sufficent approximation.  Then one can 
compute from this e an upper bound on the number of iterations needed.

I'm not suggesting you not use classical logic, rather I conjecture that 
one never needs classical logic when proving properties of algorithms and 
I wanted to make sure that my conjecture still holds.

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''