2 ms·
Floating point numbers do not form a field
- jepler 9y agoAnother simple proof of the non-field-ness of floating point numbers. in this case for the IEEE "double precision" type, that associativity doesn't hold: >>> a, b, c = 2 ** -53, 2 ** -53, 1 >>> (a+b)+c == a+(b+c) # definition of associativity False
- jepler 9y agoAnd here is a C program annotated for the C Bounded Model Checker to find a counterexample of associativity for floats: #include <math.h> extern float nondet_float(); // works equally well (quick) for double int main() { float a = nondet_float(), b = nondet_float(), c = 1; __CPROVER_assume(isfinite(a) && isfinite(b) && isfinite(c)); float s1 = (a+b)+c, s2 = a+(b+c); __CPROVER_assume(isfinite(s1) && isfinite(s2)); __CPROVER_assert(s1 == s2, "associativity holds for floats"); } http://www.cprover.org/cbmc/ http://www.cprover.org/cbmc/