On Rigorous Numerical Computation as a Scala Library

Modern programming languages have adopted the floating point type as a way to describe computations with real numbers. Thanks to the hardware support, such computations are efficient on modern architectures. However, rigorous reasoning about the resulting programs remains difficult, because of a large gap between the finite floating point representation and the infinite-precision real-number semantics that serves as the mental model for the developers. Because programming languages do not provide support for estimating errors, some computations in practice are performed more and some less precisely than needed. We present a library solution for rigorous arithmetic computation. Our library seamlessly integrates into the Scala programming language, thanks to its extensibility mechanisms such as implicit conversions and the treatment of arithmetic operations as method calls. Our numerical data type library tracks a (double) floating point value, but also an upper bound on the error between this value and the ideal value that would be computed in the real-value semantics. The library supports 1) an interval-based representation of the error, and 2) an affine arithmetic representation, which is generally more precise and keeps track of the correlation between different numerical values in the program. The library tracks errors arising from the rounding in arithmetic operations and constants, as well as user-provided errors that can model method errors of numerical algorithms or measurement errors arising in cyber-physical system applications. Our library provides approximations for most of the standard mathematical operations, including trigonometric functions. The library supports automated demand-driven refinement of computed errors by lazily increasing the precision of iteratively computed values to meet the desired precision of the final expression. Furthermore, the library supports dynamic transformation of the evaluation order following a set of algebraic rules to reduce the estimated error in the computed value. The transformed expressions can be used to suggest static rewrites of the source code to the developer. We evaluate the library on a number of examples from numerical analysis and physical simulations. We found it to be a useful tool for gaining confidence in the correctness of the computation.