一句话：提出带线性灵敏度与分级单子的类型系统 Λ_num，静态推导浮点舍入误差的定量界并证明其语义可靠性。
浮点实现会引入舍入误差，影响实数算法结果的精度。论文提出函数式语言 Λ_num，其类型系统结合线性类型约束的灵敏度分析与新型 graded monad 来跟踪舍入误差累积，可表达舍入误差的定量上界。作者通过将指称语义关联到精确与浮点操作语义，证明类型系统可靠；并以数值分析文献中的误差度量实例化，支持忠实建模 IEEE 754 的舍入操作。原型实现能自动推断误差界，结果与现有工具相当且通常显著更快。最后把 graded monad 语义扩展到非确定性与随机舍入等复杂行为。
Algorithms operating on real numbers are implemented as floating-point computations in practice, but floatingpoint 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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{KellisonH24,
title = {Numerical Fuzz: A Type System for Rounding Error Analysis},
author = {Ariel E. Kellison and Justin Hsu},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {PLDI},
year = {2024},
doi = {10.1145/3656456}
}