Affine functions and series with co-inductive real numbers
Yves Bertot (INRIA Sophia Antipolis)

TL;DR
This paper extends co-inductive real number algorithms in Coq, demonstrating how to verify and construct functions for affine formulas and series, including the computation of Euler's number e, using co-recursion and recursion techniques.
Contribution
It introduces methods to combine co-recursion and recursion for defining functions on co-inductive real numbers, enabling effective verification of algorithms for series and affine formulas.
Findings
Verified digit streams relate to axiomatized real numbers.
Constructed correct-by-construction addition algorithms.
Defined functions for affine formulas and series, including Euler's number 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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Numerical Methods and Algorithms · Formal Methods in Verification
