Verifying the Accuracy of Polynomial Approximations in HOL
Verifying the Accuracy of Polynomial Approximations in HOL
复制标题
验证 HOL 中多项式逼近的准确性
DOI：
10.1007/bfb0028391
复制
发表时间：
1997
期刊：
影响因子：
--
通讯作者：
J. Harrison
中科院分区：
文献类型：
--
作者：
J. Harrison
许多现代的超越函数算法依赖于一个大的预计算值表格以及一个低阶多项式来在它们之间进行内插。在验证这样的算法时，人们面临着在这种多项式逼近中误差的界的问题。最直接的方法是基于数值近似的，并且表面上不能归结为正式的HOL证明。我们讨论了一种在HOL中形式化证明这些结果的技术，通过形式化多项式理论中的一些结果，例如无平方分解和Sturm定理，并使用计算机代数系统来计算结果，然后在HOL中检验这些结果。我们通过处理文献中的一个例子来演示我们的方法。
Many modern algorithms for the transcendental functions rely on a large table of precomputed values together with a low-order polynomial to interpolate between them. In verifying such an algorithm, one is faced with the problem of bounding the error in this polynomial approximation. The most straightforward methods are based on numerical approximations, and are not prima facie reducible to a formal HOL proof. We discuss a technique for proving such results formally in HOL, via the formalization of a number of results in polynomial theory, e.g. squarefree decomposition and Sturm's theorem, and the use of a computer algebra system to compute results that are then checked in HOL. We demonstrate our method by tackling an example from the literature.