Скачать или смотреть [PLDI24] Numerical Fuzz: A Type System for Rounding Error Analysis

Numerical Fuzz: A Type System for Rounding Error Analysis (Video, PLDI 2024)
Ariel E. Kellison and Justin Hsu
(Cornell University, USA; Cornell University, USA)

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.

Article: https://doi.org/10.1145/3656456

Supplementary archive: https://doi.org/10.5281/zenodo.10802849 (Badges: Artifacts Available, Artifacts Evaluated — Reusable)

ORCID: https://orcid.org/0000-0003-3177-7958, https://orcid.org/0000-0002-8953-7060

Video Tags: Floating point, Roundoff error, Linear type systems, pldi24main-p666-p, doi:10.1145/3656456, doi:10.5281/zenodo.10802849, orcid:0000-0003-3177-7958, orcid:0000-0002-8953-7060, Artifacts Available, Artifacts Evaluated — Reusable

Presentation at the PLDI 2024 conference, June 24–28, 2024, https://pldi24.sigplan.org/
Sponsored by ACM SIGPLAN,