When double rounding is odd
Ecole Normale, Supérieure De Lyon, Guillaume Melquiond, Ecole Normale, Supérieure De Lyon, Sylvie Boldo, Guillaume Melquiond · 2004
Abstract- Many general purpose processors (including Intel's) may not always produce the correctly rounded result of a oating-point opera-tion due to double rounding. Instead of rounding the value to the working precision, the value is rst rounded in an intermediate extended precision and then rounded in the working precision; this often means a loss of accuracy. We suggest the use of rounding to odd as the rst rounding in order to regain this accuracy: we prove that the double rounding then gives the correct rounding to the nearest value. To increase the trust on this result, as this rounding is unusual and this property is surprising, we formally proved this property using the Coq automatic proof checker. Keywords|Floating-point, double rounding, formal proof, Coq. I.