Numerical Fuzz: A Type System for Rounding Error Analysis

TL;DR

This paper introduces a type system for a functional language, $ ext{Lambda}_{num}$, that can express and analyze quantitative bounds on roundoff errors in floating-point computations, ensuring soundness and efficiency.

Contribution

It presents a novel type system combining sensitivity analysis with a graded monad to track roundoff errors, along with a prototype implementation for automated error bounds.

Findings

Type system is sound and relates denotational and operational semantics.

Prototype infers competitive error bounds faster than existing tools.

Incorporates IEEE 754 rounding behaviors and extends to complex rounding scenarios.

Abstract

Algorithms operating on real numbers are implemented as floating-point computations in practice, but floating-point operations introduce roundoff errors that can degrade the accuracy of the result. We propose $\Lambda_{num}$, a functional programming language with a type system that can express quantitative bounds on roundoff error. Our type system combines a sensitivity analysis, enforced through a linear typing discipline, with a novel graded monad to track the accumulation of roundoff errors. We prove that our type system is sound by relating the denotational semantics of our language to the exact and floating-point operational semantics. To demonstrate our system, we instantiate $\Lambda_{num}$ with error metrics proposed in the numerical analysis literature and we show how to incorporate rounding operations that faithfully model aspects of the IEEE 754 floating-point standard. To show that $\Lambda_{num}$ can be a useful tool for automated error analysis, we develop a prototype implementation for $\Lambda_{num}$ that infers error bounds that are competitive with existing tools, while often running significantly faster. Finally, we consider semantic extensions of our graded monad to bound error under more complex rounding behaviors, such as non-deterministic and randomized rounding.