Affine functions and series with co-inductive real numbers

Details Affine functions and series with co-inductive real numbers Affine functions and series with co-inductive real numbers

2006-03-29

arxiv.org/abs/cs/0603117v2

Mathematical Structures in Computer Science 17, 1 (2006)

Computer Science

Logic in Computer Science

Scientific paper

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].

Affiliated with

Also associated with

No associations

Rating

Affine functions and series with co-inductive real numbers does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Affine functions and series with co-inductive real numbers, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Affine functions and series with co-inductive real numbers will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-585847