We extend the work of A. Ciaffaglione and P. di Gianantonio on the mechanical verification of algorithms for exact computation on real numbers, using infinite streams of digits implemented as a co-inductive type. Four aspects are studied. The first concerns the proof that digit streams correspond to axiomatised real numbers when they are already present in the proof system. The second re-visits the definition of an addition function, looking at techniques to let the proof search engine perform the effective construction of an algorithm that is correct by construction. The third concerns the definition of a function to compute affine formulas with positive rational coefficients. This is an example where we need to combine co-recursion and recursion. Finally, the fourth aspect concerns the definition of a function to compute series, with an application on the series that is used to compute Euler's number e. All these experiments should be reproducible in any proof system that supports co-inductive types, co-recursion and general forms of terminating recursion; we used the Coq system (Dowek et al. 1993; Bertot and Casteran 2004; Gimenez 1994).
展开▼
机译：我们扩展了A. Ciaffaglione和P. di Gianantonio的工作，即使用实现为归纳类型的无限数字流，对用于对实数进行精确计算的算法进行机械验证。研究了四个方面。首先涉及证明，证明数字流与证明系统中已经存在的公理实数相对应。第二部分重新讨论了加法函数的定义，着眼于使证明搜索引擎能够有效构造通过构造正确的算法的技术。第三个问题涉及计算具有正有理系数的仿射公式的函数的定义。这是我们需要结合使用联合递归和递归的例子。最后，第四个方面涉及用于计算序列的函数的定义，该序列的一个应用程序用于计算欧拉数e。所有这些实验在支持共归纳类型，共递归和终止递归的一般形式的任何证明系统中都应可重现；我们使用了Coq系统（Dowek等，1993； Bertot和Casteran，2004； Gimenez，1994）。
展开▼
