Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Numerical Fuzz: A Type System for Rounding Error Analysis

Ariel E. Kellison, Justin Hsu

TL;DR

This work proposes Λnum, a functional programming language with a type system that can express quantitative bounds on roundoff error and proves that the type system is sound by relating the denotational semantics of the language to the exact and floating-point operational semantics.

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 $Λ_{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 $Λ_{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 $Λ_{num}$ can be a useful tool for automated error analysis, we develop a prototype implementation for $Λ_{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.

Numerical Fuzz: A Type System for Rounding Error Analysis

TL;DR

This work proposes Λnum, a functional programming language with a type system that can express quantitative bounds on roundoff error and proves that the type system is sound by relating the denotational semantics of the language to the exact and floating-point operational semantics.

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 , 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 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 can be a useful tool for automated error analysis, we develop a prototype implementation for 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.
Paper Structure (43 sections, 19 theorems, 50 equations, 11 figures, 2 tables)

This paper contains 43 sections, 19 theorems, 50 equations, 11 figures, 2 tables.

Table of Contents

  1. Introduction
  2. A Tour of $\Lambda_\textbf{num}$
  3. Floating-Point Arithmetic
  4. Floating-Point Number Systems
  5. Rounding Operators
  6. The Standard Model
  7. Absolute and Relative Error
  8. Propagation of Rounding Errors
  9. Sensitivity Type Systems: An Overview
  10. Roundoff Error Analysis in $\Lambda_\textbf{num}$: A Motivating Example
  11. Composing Error Bounds
  12. Error Propagation
  13. The Language $\Lambda_\textbf{num}$
  14. Syntax
  15. Types
  16. ...and 28 more sections

Key Result

lemma 1

Let $\Gamma \vdash e : \tau$ be a well-typed term. Then for any typing environment $\Delta \sqsubseteq \Gamma$, there is a derivation of $\Delta \vdash e : \tau$.

Figures (11)

  • Figure 1: Types, values, and terms.
  • Figure 2: Typing rules for $\Lambda_\textbf{num}$, with $s,t,q,r \in \mathbb{R}^{\geq 0} \cup \{\infty\}$.
  • Figure 3: Evaluation rules for $\Lambda_\textbf{num}$.
  • Figure 4: Reducibility Predicate
  • Figure 5: Primitive operations in $\Lambda_\textbf{num}$, typed using the relative precision (RP) metric.
  • ...and 6 more figures

Theorems & Definitions (46)

  • definition 1
  • definition 2: The Relative Precision (RP) Metric
  • definition 3
  • definition 4: Subenvironment
  • lemma 1: Weakening
  • proof
  • lemma 2: Substitution
  • proof
  • theorem 1: Termination
  • definition 5
  • ...and 36 more