nadezhin/verify-todec

Formal check of Raffaello Guilietti's paper "Rendering doubles in Java"

verify-todec's Issues

A question on the proof

Hi,

I'm the author of a variation of you and Rafaello's wonderful work, Schubfach algorithm. I'm writing this to ask you a question about Schubfach.

Honestly, I didn't fully read Schubfach paper when I was working on my algorithm, and just complemented the resulting missing stuffs by my own logic. As a result, I was not aware of what exactly Result 20 mentioned in the Schubfach paper was about. The corresponding mathematical result in my case is based on Ulf Adams' min-max Euclid algorithm. As you might already know, Ulf's algorithm as written in his paper does not always produce correct results, so I had to rethink about it and eventually came up with an improved, correct version of it, which is guaranteed to always produce the exact minimum and the maximum. You may refer to Theorem C.1 in my paper if you are interested.

The thing I'm curious about is this. So, even though the improved min-max Euclid algorithm gives us the exact minimum and maximum of modular products, in order to apply it into my algorithm, I still have to manually compute the required precision for every exponent (as shown in Figure 2 and Figure 3 in Ryu paper) which, practically, cannot be done by hand. I, just like Ulf, wrote a program for computing these to verify that 62-bits for float and 125-bits for double are indeed sufficient.

But it seems that your proof on Result 20 is not doing something similar, and just gives us the needed result at once. Is this correct? If that's the case, could you give me a pointer that I can look at to understand what's going on?

Thank you again, and sorry if the question were somewhat vague and/or hard to answer.