Formal Verification of Exact Computations Using Newton's Method
Formal Verification of Exact Computations Using Newton's Method
复制标题
使用牛顿法对精确计算进行形式验证
DOI：
--
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
I. Pasca
中科院分区：
文献类型：
--
作者：
Nicolas Julien;I. Pasca
我们对牛顿方法的验证很感兴趣。我们利用Coq的标准库的公理实数所做的方法的收敛和稳定性的形式化，以验证牛顿方法用基于余归纳流的精确实算术库所做的计算。这项工作的贡献是双重的。首先，在牛顿方法的基础上，我们设计并证明了一种在流上懒惰地计算实函数的求根的算法。其次，我们证明了牛顿方法中每一步的舍入仍然产生一个收敛的过程，该过程具有输入精度和结果精度之间的精确关系。事实证明，包含四舍五入的算法效率要高得多。
We are interested in the verification of Newton's method. We use a formalization of the convergence and stability of the method done with the axiomatic real numbers of Coq's Standard Library in order to validate the computation with Newton's method done with a library of exact real arithmetic based on co-inductive streams. The contribution of this work is twofold. Firstly, based on Newton's method, we design and prove correct an algorithm on streams for computing the root of a real function in a lazy manner. Secondly, we prove that rounding at each step in Newton's method still yields a convergent process with an accurate correlation between the precision of the input and that of the result. An algorithm including rounding turns out to be much more efficient.