Affine functions and series with co-inductive real numbers

Yves Bertot 1
1 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : We extend the work of A. Ciaffaglione and P. Di Gianantonio on mechanical verification of algorithms for exact computation on real numbers, using infinite streams of digits implemented as co-inductive types. Four aspects are studied: the first aspect concerns the proof that digit streams can be related to the axiomatized real numbers that are already axiomatized in the proof system (axiomatized, but with no fixed representation). The second aspect re-visits the definition of an addition function, looking at techniques to let the proof search mechanism perform the effective construction of an algorithm that is correct by construction. The third aspect concerns the definition of a function to compute affine formulas with positive rational coefficients. This should be understood as a testbed to describe a technique to combine co-recursion and recursion to obtain a model for an algorithm that appears at first sight to be outside the expressive power allowed by the proof system. 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, but we performed with the Coq system [12, 3, 14].
Document type :
Journal articles
Liste complète des métadonnées

Cited literature [39 references]  Display  Hide  Download
Contributor : Yves Bertot <>
Submitted on : Monday, May 1, 2006 - 9:01:06 AM
Last modification on : Wednesday, September 12, 2018 - 1:16:57 AM
Document(s) archivé(s) le : Monday, September 20, 2010 - 2:32:14 PM




Yves Bertot. Affine functions and series with co-inductive real numbers. Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2006, 17 (1), pp.37-63. ⟨10.1017/S0960129506005809⟩. ⟨inria-00001171v2⟩



Record views


Files downloads