Extracting efficient exact real number computation from proofs in constructive type theory
share
Exact real computation is an alternative to floating-point arithmetic where operations on real numbers are performed exactly, without the introduction of rounding errors. When proving the correctness of an implementation, one can focus solely on the mathematical properties of the problem without thinking about the subtleties of representing real numbers. We propose a new axiomatization of the real numbers in a dependent type theory with the goal of extracting certified exact real computation programs from constructive proofs. Our formalization differs from similar approaches, in that we formalize the reals in a conceptually similar way as some mature implementations of exact real computation. Primitive operations on reals can be extracted directly to the corresponding operations in such an implementation, producing more efficient programs. We particularly focus on the formalization of partial and nondeterministic computation, which is essential in exact real computation. We prove the soundness of our formalization with regards of the standard realizability interpretation from computable analysis and show how to relate our theory to a classical formalization of the reals. We demonstrate the feasibility of our theory by implementing it in the Coq proof assistant and present several natural examples. From the examples we have automatically extracted Haskell programs that use the exact real computation framework AERN for efficiently performing exact operations on real numbers. In experiments, the extracted programs behave similarly to native implementations in AERN in terms of running time and memory usage.
READ FULL TEXT