Medina 逼近反正切函数多项式序列的形式验证
计算机科学中的逻辑
2014-06-09 v1 数学软件
摘要
许多计算超越函数算法的验证基于对这些函数的多项式逼近，通常是泰勒级数逼近。然而，计算和验证反正切函数的逼近是非常具有挑战性的问题，很大程度上是因为泰勒级数收敛到反正切函数的速度非常慢——要获得 arctan(0.95) 的三位小数精度需要一个 57 次多项式。Medina 提出了一系列多项式来逼近反正切函数，其收敛速度快得多——仅需一个 7 次多项式即可获得 arctan(0.95) 的三位小数精度。我们在本文中提出了在 ACL2(r) 中对该多项式序列的正确性和收敛率的证明。该证明尤为优美，因为它使用了实分析中的许多结果。其中一些必要的结果已在先前的工作中得到证明，而另一些则是作为本次工作的一部分被证明的。
引用
@article{arxiv.1406.1561,
title = {Formal Verification of Medina's Sequence of Polynomials for Approximating Arctangent},
author = {Ruben Gamboa and John Cowles},
journal= {arXiv preprint arXiv:1406.1561},
year = {2014}
}
备注
In Proceedings ACL2 2014, arXiv:1406.1238