Primitive Floats in Coq
Primitive Floats in Coq
复制标题
Coq 中的原始浮点数
DOI：
10.4230/lipics.itp.2019.7
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
P. Roux
中科院分区：
文献类型：
--
作者：
Guillaume Bertholon;Érik Martin;P. Roux
一些数学证明涉及密集的计算，例如：四色定理，黑尔斯关于球面填充的定理（以前称为开普勒猜想）或区间算术。对于数值计算，尽管引入了舍入误差，但由于其效率，浮点运算得到了广泛的使用。基于IEEE 754标准的浮点算法可以获得形式保证，该标准精确地指定了浮点算法及其舍入模式，以及诸如Coq之类的证明助手，该助手具有高效的计算能力。Coq o编译器处理机器整数，但是仍然需要使用这些整数来模拟浮点运算。提出了一种改进的艾德版本的Coq，它可以使用机器的浮点运算符。这种实施的主要障碍和它的健全性进行了讨论。基准测试表明，潜在的性能增益的两个数量级。
Some mathematical proofs involve intensive computations, for instance: the four-color theorem, Hales’ theorem on sphere packing (formerly known as the Kepler conjecture) or interval arithmetic. For numerical computations, floating-point arithmetic enjoys widespread usage thanks to its efficiency, despite the introduction of rounding errors. Formal guarantees can be obtained on floating-point algorithms based on the IEEE 754 standard, which precisely specifies floating-point arithmetic and its rounding modes, and a proof assistant such as Coq, that enjoys efficient computation capabilities. Coq offers machine integers, however floating-point arithmetic still needed to be emulated using these integers. A modified version of Coq is presented that enables using the machine floating-point operators. The main obstacles to such an implementation and its soundness are discussed. Benchmarks show potential performance gains of two orders of magnitude.