Medina多项式序列逼近反正切的形式化验证
Formal Verification of Medina's Sequence of Polynomials for Approximating Arctangent
摘要：
计算超越函数的许多算法的验证是基于这些函数的多项式近似，通常是泰勒级数近似。然而，计算和验证反正切函数的近似值是非常具有挑战性的问题，这在很大程度上是因为泰勒级数收敛到反正切非常慢-需要57次多项式才能获得反正切（0.95）的三位小数。Medina提出了一系列的多项式，以更快的收敛速度近似反正切-一个7次多项式是所有需要得到三个小数位的arctan（0.95）。本文给出了这一多项式序列的正确性和收敛速度在ACL 2（r）中的证明。这个证明特别漂亮，因为它使用了许多来自真实分析的结果。其中一些必要的结果在以前的工作中得到了证明，但也有一些是作为这项工作的一部分得到证明的。
英文摘要：
The verification of many algorithms for calculating transcendental functions is based on polynomial approximations to these functions, often Taylor series approximations. However, computing and verifying approximations to the arctangent function are very challenging problems, in large part because the Taylor series converges very slowly to arctangent-a 57th-degree polynomial is needed to get three decimal places for arctan(0.95). Medina proposed a series of polynomials that approximate arctangent with far faster convergence-a 7th-degree polynomial is all that is needed to get three decimal places for arctan(0.95). We present in this paper a proof in ACL2(r) of the correctness and convergence rate of this sequence of polynomials. The proof is particularly beautiful, in that it uses many results from real analysis. Some of these necessary results were proven in prior work, but some were proven as part of this effort.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
