arXiv · 2510.13414
Mechanizing Olver's Error Arithmetic
Abstract
We mechanize the fundamental properties of a rounding error model for floating-point arithmetic based on relative precision, a measure of error proposed as a substitute for relative error in rounding error analysis. A key property of relative precision is that it forms a true metric, providing a well-defined measure of distance between exact results and their floating-point approximations while offering a structured approach to propagating error bounds through sequences of computations. Our mechanization formalizes this property, establishes rules for converting between relative precision and relative error, and shows that the rounding error model based on relative precision slightly overapproximates the standard rounding error model. Finally, we demonstrate, with a simple example of the inner product of two vectors, that this alternative model facilitates a tractable approach to developing certified rounding error bounds.
Explore related subjects
Keep this discovery
Max Fan, Ariel E. Kellison, Samuel D. Pollard. 2025-10-15. Mechanizing Olver's Error Arithmetic. https://doi.org/10.4204/eptcs.432.6
Cite the original work for its findings. Save a collection to share your selection of sources.