×

Axiomatic reals and certified efficient exact real computation. (English) Zbl 07547745

Silva, Alexandra (ed.) et al., Logic, language, information, and computation. 27th international workshop, WoLLIC 2021, virtual event, October 5–8, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13038, 252-268 (2021).
Summary: 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.
For the entire collection see [Zbl 1489.03004].

MSC:

03B70 Logic in computer science
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Balluchi, A., Casagrande, A., Collins, P., Ferrari, A., Villa, T., Sangiovanni-Vincentelli, A.L.: Ariadne: a framework for reachability analysis of hybrid automata. In: Proceedings of the International Symposium on Mathematical Theory of Networks and Systems (2006)
[2] Boldo, S.; Filliâtre, J-C; Melquiond, G.; Carette, J.; Dixon, L.; Coen, CS; Watt, SM, Combining Coq and Gappa for certifying floating-point programs, Intelligent Computer Mathematics, 59-74 (2009), Heidelberg: Springer, Heidelberg · Zbl 1247.68232 · doi:10.1007/978-3-642-02614-0_10
[3] Boldo, S., Lelay, C., Melquiond, G.: Formalization of real analysis: a survey of proof assistants and libraries. Math. Struct. Comput. Sci. 26(7), 1196-1233 (2016). http://hal.inria.fr/hal-00806920 · Zbl 1364.68327
[4] Boldo, S., Melquiond, G.: Flocq: a unified library for proving floating-point algorithms in Coq. In: 2011 IEEE 20th Symposium on Computer Arithmetic, pp. 243-252. IEEE (2011)
[5] Brattka, V., Hertling, P.: Feasible real random access machines. J. Complex. 14(4), 490-526 (1998). doi:10.1006/jcom.1998.0488. https://www.sciencedirect.com/science/article/pii/S0885064X98904885 · Zbl 0913.68099
[6] Cruz-Filipe, L.; Geuvers, H.; Wiedijk, F.; Asperti, A.; Bancerek, G.; Trybulec, A., C-CoRN, the constructive Coq repository at Nijmegen, Mathematical Knowledge Management, 88-103 (2004), Heidelberg: Springer, Heidelberg · Zbl 1108.68586 · doi:10.1007/978-3-540-27818-4_7
[7] Hertling, P., A real number structure that is effectively categorical, Math. Log. Q., 45, 147-182 (1999) · Zbl 0946.03050 · doi:10.1002/malq.19990450202
[8] Hofmann, M.; Pacholski, L.; Tiuryn, J., On the interpretation of type theory in locally cartesian closed categories, Computer Science Logic, 427-441 (1995), Heidelberg: Springer, Heidelberg · Zbl 1044.03544 · doi:10.1007/BFb0022273
[9] Kawamura, A.; Steinberg, F.; Thies, H.; Moss, LS; de Queiroz, R.; Martinez, M., Parameterized complexity for uniform operators on multidimensional analytic functions and ODE solving, Logic, Language, Information, and Computation, 223-236 (2018), Heidelberg: Springer, Heidelberg · Zbl 1509.68110 · doi:10.1007/978-3-662-57669-4_13
[10] Konečný, M.: aern2-real: A Haskell library for exact real number computation (2021). https://hackage.haskell.org/package/aern2-real
[11] Konečný, M., Steinberg, F., Thies, H.: Computable analysis for verified exact real computation. In: 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Schloss Dagstuhl-Leibniz-Zentrum für Informatik (2020)
[12] Koswara, I.; Selivanova, S.; Ziegler, M.; van Bevern, R.; Kucherov, G., Computational complexity of real powering and improved solving linear differential equations, Computer Science - Theory and Applications, 215-227 (2019), Cham: Springer, Cham · Zbl 07121069 · doi:10.1007/978-3-030-19955-5_19
[13] Kreitz, C.; Weihrauch, K., Theory of representations, Theoret. Comput. Sci., 38, 35-53 (1985) · Zbl 0588.03031 · doi:10.1016/0304-3975(85)90208-7
[14] Luckhardt, H.: A fundamental effect in computations on real numbers. Theoret. Comput. Sci. 5(3), 321 - 324 (1977). doi:10.1016/0304-3975(77)90048-2. http://www.sciencedirect.com/science/article/pii/0304397577900482 · Zbl 0374.02018
[15] Melquiond, G.; Armando, A.; Baumgartner, P.; Dowek, G., Proving bounds on real-valued functions with computations, Automated Reasoning, 2-17 (2008), Heidelberg: Springer, Heidelberg · Zbl 1165.68464 · doi:10.1007/978-3-540-71070-7_2
[16] Müller, NT; Blanck, J.; Brattka, V.; Hertling, P., The iRRAM: exact arithmetic in C++, Computability and Complexity in Analysis, 222-252 (2001), Heidelberg: Springer, Heidelberg · Zbl 0985.65523 · doi:10.1007/3-540-45335-0_14
[17] Palmgren, E.: On universes in type theory. In: Twenty Five Years of Constructive Type Theory, pp. 191-204 (1998) · Zbl 0930.03090
[18] Park, S., et al.: Foundation of computer (algebra) analysis systems: semantics, logic, programming, verification. arXiv e-prints arXiv:1608.05787 (2016)
[19] Reus, B., Realizability models for type theories, Electron. Notes Theoret. Comput. Sci., 23, 1, 128-158 (1999) · Zbl 0958.68098 · doi:10.1016/S1571-0661(04)00108-2
[20] Schröder, M., Effectivity in spaces with admissible multirepresentations, Math. Logic Q., 48, S1, 78-90 (2002) · Zbl 1032.03039 · doi:10.1002/1521-3870(200210)48:1+<78::AID-MALQ78>3.0.CO;2-K
[21] Schwichtenberg, H.: Constructive analysis with witnesses. In: Proof Technology and Computation. Natio Science Series, pp. 323-354 (2006) · Zbl 1137.03327
[22] Seely, RAG, Locally cartesian closed categories and type theory, Math. Proc. Cambridge Philos. Soc., 95, 1, 33-48 (1984) · Zbl 0539.03048 · doi:10.1017/S0305004100061284
[23] Steinberg, F., Thery, L., Thies, H.: Computable analysis and notions of continuity in Coq. Log. Methods Comput. Sci. 17(2), May 2021. https://lmcs.episciences.org/7478 · Zbl 07350782
[24] Van Oosten, J.: Realizability: an introduction to its categorical side. Elsevier (2008) · Zbl 1225.03002
[25] Weihrauch, K., Computable Analysis (2000), Berlin: Springer, Berlin · Zbl 0956.68056 · doi:10.1007/978-3-642-56999-9
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.