Sie befinden Sich nicht im Netzwerk der Universität Paderborn. Der Zugriff auf elektronische Ressourcen ist gegebenenfalls nur via VPN oder Shibboleth (DFN-AAI) möglich. mehr Informationen...
Axiomatic Reals and Certified Efficient Exact Real Computation
Ist Teil von
Logic, Language, Information, and Computation, 2021, Vol.13038, p.252-268
Ort / Verlag
Switzerland: Springer International Publishing AG
Erscheinungsjahr
2021
Link zum Volltext
Quelle
Alma/SFX Local Collection
Beschreibungen/Notizen
We introduce a new axiomatization of the constructive real numbers in a dependent type theory. Our main motivation is to provide a sound and simple to use backend for verifying algorithms for exact real number computation and the extraction of efficient certified programs from our proofs. We prove the soundness of our formalization with regards to the standard realizability interpretation from computable analysis. We further show how to relate our theory to a classical formalization of the reals to allow certain non-computational parts of correctness proofs to be non-constructive. We demonstrate the feasibility of our theory by implementing it in the Coq proof assistant and present several natural examples. From the examples we can automatically extract 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 hand-written implementations in AERN in terms of running time.