We provide a computer-verified exact monadic functional implementation of the Riemann integral in type theory. Together with previous work by O'Connor, this may be seen as the beginning of the realization of Bishop's vision to use constructive mathematics as a programming language for exact analysis.
There is some potential to increase efficiency by using a non-uniform'' definition of uniform continuity. That is to say, using a definition of uniform continuity that allows different segments of the domain to have local moduli associated with them. Ulrich Berger uses such a definition of uniform continuity to define integration @cite_12 . Simpson also defines an integration algorithm that uses a local modulus for a function that is computed directly from the definition of the function @cite_10 . However, implementing his algorithm directly in Coq is not possible because it relies on bar induction, which is not available in Coq unless one adds an axiom such as bar induction to it or one treats the real numbers as a formal space @cite_36 @cite_16 .
@cite_36 @cite_16 @cite_10 @cite_12
1486536800 2111094344 1515039666 2108845204
The notion of formal space was introduced by Fourman and Grayson [FG] only a few years ago, but it is only a recent though important step of a long story whose roots involve such names as Brouwer and Stone and whose development is due to mathematicians from different fields, mainly algebraic geometry, category theory and logic. Cauchy’s construction of reals as sequences of rational approximations is the theoretical basis for a number of implementations of exact real numbers, while Dedekind’s construction of reals as cuts has inspired fewer useful computational ideas. Nevertheless, we can see the computational content of Dedekind reals by constructing them within Abstract Stone Duality (ASD), a computationally meaningful calculus for topology. This provides the theoretical background for a novel way of computing with real numbers in the style of logic programming. Real numbers are dened in terms of (lower and upper) Dedekind cuts, while programs are expressed as statements about real numbers in the language of ASD. By adapting Newton’s method to interval arithmetic we can make the computations as ecient as those based on Cauchy reals. The results reported in this talk are joint work with Paul Taylor. We show how functional languages can be used to write programs for real-valued functionals in exact real arithmetic. We concentrate on two useful functionals: definite integration, and the functional returning the maximum value of a continuous function over a closed interval. The algorithms are a practical application of a method, due to Berger, for computing quantifiers over streams. Correctness proofs for the algorithms make essential use of domain theory. We give a coinductive characterization of the set of continuous functions defined on a compact real interval, and extract certified programs that 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. This is a pilot study in using proof-theoretic methods for certified algorithms in exact real arithmetic.