The Coq mailing list

[roconnor AT theorem.ca]

On Mon, 2 Jul 2007, Guillaume Melquiond wrote:

> 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.

Theoretical bounds may not be useless for practical use because one does 
not need to fully compute the upperbound.  One can lazily compute only 
what is needed.  So one may feel free to use the most impractical 
upperbounds available.

--
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.''