仿射函数与具有共归实数的级数
摘要：用共识类型实现的无限数字流扩展了A. Ciaffaglione和P. Di Gianantonio关于对实数精确计算算法的机械验证的工作。研究了四个方面：第一个方面涉及证明数字流可以与在证明系统中已经公理化的实数相关联（已公理化，但没有固定表示）。第二个方面重新审视了加法函数的定义，探讨让证明搜索机制执行通过构造正确的算法的有效构建的技术。第三个方面涉及定义一个计算带有正有理系数的仿射公式的函数。这应该被理解为描述一种通过合作递归和递归来获得一个算法模型的技术的测试床，这个算法模型乍一看似乎超出了证明系统允许的表达能力。第四个方面涉及定义一个计算级数的函数，并将其应用于计算欧拉数e的级数。所有这些实验都可以在支持共识类型、合作递归和一般形式的终止递归的任何证明系统中重现，但我们使用的是Coq系统[12, 3, 14]。
作者：Yves Bertot (INRIA Sophia Antipolis)
论文ID：cs/0603117
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2007-05-23