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.

翻译：处理实数运算的算法在实践中通常实现为浮点计算，但浮点运算引入的舍入误差可能降低结果的精度。我们提出$\Lambda_{num}$，一种带有可表达舍入误差定量界限的类型系统的函数式编程语言。该类型系统将通过线性类型规范强制执行的敏感度分析与追踪舍入误差累积的新型分级单子相结合。通过将语言的指称语义与精确和浮点操作语义相关联，我们证明了类型系统的可靠性。为展示该系统，我们以数值分析文献中提出的误差度量实例化$\Lambda_{num}$，并展示如何整合忠实模拟IEEE 754浮点标准特性的舍入操作。为验证$\Lambda_{num}$可作为自动化误差分析的有用工具，我们开发了其原型实现，该实现推断的误差界限与现有工具相当，且运行速度通常显著更快。最后，我们考虑对分级单子进行语义扩展，以在更复杂的舍入行为（如非确定性和随机化舍入）下约束误差。