Formally Verified Argument Reduction with a Fused Multiply-Add
Formally Verified Argument Reduction with a Fused Multiply-Add
复制标题
使用融合乘法加法进行正式验证的参数缩减
DOI：
--
复制
发表时间：
2007
影响因子：
3.7
通讯作者：
Ren
中科院分区：
文献类型：
--
作者：
S. Boldo;M. Daumas;Ren
Cody和Waite参数减少技术对于相当大的参数非常有效，但是随着输入的增长，没有比特可以足够精确地近似常数。在温和的假设下，我们表明，与融合乘加计算的结果提供了一个完全准确的结果，为许多可能的值的输入与一个常数几乎准确的全部工作精度。我们还提出了一个算法，一个完全准确的第二个减少步骤，以达到完全双精度（两个数字的所有有效位是准确的），即使在最坏的情况下，参数减少。我们的工作回顾了常用算法并给出了正确性证明。所有的证明都使用Coq自动证明检查器进行了正式验证。
The Cody and Waite argument reduction technique works perfectly for reasonably large arguments, but as the input grows, there are no bits left to approximate the constant with enough accuracy. Under mild assumptions, we show that the result computed with a fused multiply-add provides a fully accurate result for many possible values of the input with a constant almost accurate to the full working precision. We also present an algorithm for a fully accurate second reduction step to reach full double accuracy (all the significand bits of two numbers are accurate) even in the worst cases of argument reduction. Our work recalls the common algorithms and presents proofs of correctness. All the proofs are formally verified using the Coq automatic proof checker.