ContrarianismPascal Cuoq - 14th May 2013
If I told you that when
n is a positive power of two and
d an arbitrary number, both represented as
double, the condition
(n - 1) * d + d == n * d in strictly-IEEE-754-implementing C is always true, would you start looking for a counter-example, or start looking for a convincing argument that this property may hold?
If you started looking for counter-examples, would you start with the vicious values? Trying to see if
+inf can be interpreted as “a positive power of two” or “an arbitrary number” represented “as
double”? A subnormal value for
d? A subnormal value such that
n*d is normal? A subnormal value such that
(n - 1) * d is subnormal and
n * d is normal?
Or would you try your luck with ordinary values such as
This post is based on a remark by Stephen Canon. Also, I have discovered a truly remarkable proof of the property which this quick post is too small to contain.