From coinductive proofs to exact real arithmetic: theory and applications

TL;DR

This paper introduces a coinductive framework for exact real arithmetic, enabling the extraction of certified algorithms for real number computations from constructive proofs, with applications to polynomials and integrals.

Contribution

It presents a novel coinductive characterization of continuous functions that allows extracting certified real arithmetic algorithms from constructive proofs.

Findings

Extracted programs for degree two polynomials

Algorithms for definite integrals of continuous functions

Framework ensures correctness of real number computations

Abstract

Based on a new coinductive characterization of continuous functions we extract certified programs for exact real number computation from constructive proofs. The extracted programs construct and combine exact real number algorithms with respect to the binary signed digit representation of real numbers. The data type corresponding to the coinductive definition of continuous functions consists of finitely branching non-wellfounded trees describing when the algorithm writes and reads digits. We discuss several examples including the extraction of programs for polynomials up to degree two and the definite integral of continuous maps.