The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT ens-lyon.fr>]

Le lundi 02 juillet 2007 à 09:28 -0400, 
roconnor AT theorem.ca
 a écrit :

> BTW, could you point me to some introductory material showing easy 
> classical proofs of termination that are hard to prove constructively? 
> I'd be interested to know more about them.

There are probably some introductory material, but I can't remember
where to find it right now. So here are a few details.

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.

But if you want to know an upper bound on the number of iterations, you
need to explicitly know how close you will actually get from this given
rational number. Note that this is more or less what the function
computes, hence the difficulty. So you have to invoke some theorems like
the ones from Nesterenko and Waldschmidt, which happen to give huge
theoretical bounds that are plain useless for practical use.

* Ziv, "Fast evaluation of elementary functions with correctly rounded
last bit."

* Nesterenko and Waldschmidt, "On the approximations of the values of
the exponential function and logarithm by algebraic numbers."

Best regards,

Guillaume