Mechanizing Olver's Error Arithmetic
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866914094210088960 |
|---|---|
| author | Fan, Max Kellison, Ariel E. Pollard, Samuel D. |
| author_facet | Fan, Max Kellison, Ariel E. Pollard, Samuel D. |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2510_13414 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Mechanizing Olver's Error Arithmetic Fan, Max Kellison, Ariel E. Pollard, Samuel D. Numerical Analysis D.2.4; G.1.0 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. |
| title | Mechanizing Olver's Error Arithmetic |
| topic | Numerical Analysis D.2.4; G.1.0 |
| url | https://arxiv.org/abs/2510.13414 |