Type-Based Approaches to Rounding Error Analysis
Ariel Eileen Kellison
TL;DR
The work tackles the problem of providing sound, automated reasoning about rounding errors in numerical programs by melding numerical analysis with type theory. It introduces NumFuzz, a higher-order functional language with a linear type system and a graded neighborhood monad to statically bound forward rounding error, and Bean, a first-order language with a graded comonad and backward error lenses to track and bound backward error compositionally. The authors develop denotational and operational semantics that connect type-checked bounds to actual rounding behavior, demonstrate soundness, and implement prototypes that infer tight error bounds competitive with existing tools. By unifying forward and backward error analyses under a rigorous type-based framework, the work offers scalable, modular reasoning about numerical accuracy with potential applicability to verification and safe numerical software development.
Abstract
This dissertation explores the design and implementation of programming languages that represent rounding error analysis through typing. In the first part of this dissertation, we demonstrate that it is possible to design languages for forward error analysis with NumFuzz, a functional programming language whose type system expresses quantitative bounds on rounding error. This type system combines a sensitivity analysis, enforced through a linear typing discipline, with a novel graded monad to track the accumulation of rounding errors. We establish the soundness of the type system by relating the denotational semantics of the language to both an exact and floating-point operational semantics. To demonstrate the practical utility of NumFuzz as a tool for automated error analysis, we have developed a prototype implementation capable of automatically inferring error bounds. Our implementation produces bounds competitive with existing tools, while often achieving significantly faster analysis times. In the second part of this dissertation, we explore a type-based approach to backward error analysis with Bean, a first-order programming language with a linear type system that can express quantitative bounds on backward error. Bean's type system combines a graded coeffect system with strict linearity to soundly track the flow of backward error through programs. To illustrate Bean's potential as a practical tool for automated backward error analysis, we implement a variety of standard algorithms from numerical linear algebra in Bean, establishing fine-grained backward error bounds via typing in a compositional style. We also develop a prototype implementation of Bean that infers backward error bounds automatically. Our evaluation shows that these inferred bounds match worst-case theoretical relative backward error bounds from the literature.