Document

# Computable Analysis for Verified Exact Real Computation

## File

LIPIcs.FSTTCS.2020.50.pdf
• Filesize: 0.56 MB
• 18 pages

## Cite As

Michal Konečný, Florian Steinberg, and Holger Thies. Computable Analysis for Verified Exact Real Computation. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 50:1-50:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.FSTTCS.2020.50

## Abstract

We use ideas from computable analysis to formalize exact real number computation in the Coq proof assistant. Our formalization is built on top of the Incone library, a Coq library for computable analysis. We use the theoretical framework that computable analysis provides to systematically generate target specifications for real number algorithms. First we give very simple algorithms that fulfill these specifications based on rational approximations. To provide more efficient algorithms, we develop alternate representations that utilize an existing formalization of floating-point algorithms and interval arithmetic in combination with methods used by software packages for exact real arithmetic that focus on execution speed. We also define a general framework to define real number algorithms independently of their concrete encoding and to prove them correct. Algorithms verified in our framework can be extracted to Haskell programs for efficient computation. The performance of the extracted code is comparable to programs produced using non-verified software packages. This is without the need to optimize the extracted code by hand. As an example, we formalize an algorithm for the square root function based on the Heron method. The algorithm is parametric in the implementation of the real number datatype, not referring to any details of its implementation. Thus the same verified algorithm can be used with different real number representations. Since Boolean valued comparisons of real numbers are not decidable, our algorithms use basic operations that take values in the Kleeneans and Sierpinski space. We develop some of the theory of these spaces. To capture the semantics of non-sequential operations, such as the "parallel or", we use multivalued functions.

## Subject Classification

##### ACM Subject Classification
• Theory of computation → Logic and verification
• Mathematics of computing → Continuous mathematics
##### Keywords
• Computable Analysis
• exact real computation
• formal proofs
• proof assistant
• Coq

## Metrics

• Access Statistics
• Total Accesses (updated on a weekly basis)
0

## References

1. S. Abramsky and A. Jung. Domain theory. In S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, volume 3, pages 1-168. Clarendon Press, Oxford, 1994.
2. Reynald Affeldt, Cyril Cohen, and Damien Rouhling. Formalization techniques for asymptotic reasoning in classical analysis. Journal of Formalized Reasoning, 11(1):43-76, 2018. URL: https://doi.org/10.6092/issn.1972-5787/8124.
3. Andrea Balluchi, Alberto Casagrande, Pieter Collins, Alberto Ferrari, Tiziano Villa, and Alberto L Sangiovanni-Vincentelli. Ariadne: a framework for reachability analysis of hybrid automata. In In: Proceedings of the International Syposium on Mathematical Theory of Networks and Systems., 2006.
4. Merrie Bergmann. An introduction to many-valued and fuzzy logic: semantics, algebras, and derivation systems. Cambridge University Press, 2008.
5. Sylvie Boldo, Catherine Lelay, and Guillaume Melquiond. Coquelicot: A user-friendly library of real analysis for Coq. Mathematics in Computer Science, 9(1):41-62, 2015.
6. Sylvie Boldo, Catherine Lelay, and Guillaume Melquiond. Formalization of real analysis: A survey of proof assistants and libraries. Mathematical Structures in Computer Science, 26(7):1196-1233, 2016. URL: http://hal.inria.fr/hal-00806920.
7. Sylvie Boldo and Guillaume Melquiond. Flocq: A unified library for proving floating-point algorithms in coq. In 2011 IEEE 20th Symposium on Computer Arithmetic, pages 243-252. IEEE, 2011.
8. Vasco Brattka and Peter Hertling. Feasible real random access machines. J. Complexity, 14(4):490-526, 1998. URL: https://doi.org/10.1006/jcom.1998.0488.
9. Vasco Brattka, Peter Hertling, and Klaus Weihrauch. A Tutorial on Computable Analysis. In S. Barry Cooper, Benedikt Löwe, and Andrea Sorbi, editors, New Computational Paradigms: Changing Conceptions of What is Computable, pages 425-491. Springer, 2008.
10. Franz Brauße, Pieter Collins, Johannes Kanig, SunYoung Kim, Michal Konečny, Gyesik Lee, Norbert Müller, Eike Neumann, Sewon Park, Norbert Preining, et al. Semantics, logic, and verification of" exact real computation". arXiv preprint arXiv:1608.05787, 2016.
11. Alberto Ciaffaglione and Pietro Di Gianantonio. A certified, corecursive implementation of exact real numbers. Theoretical Computer Science, 351(1):39-51, 2006. Real Numbers and Computers. URL: https://doi.org/10.1016/j.tcs.2005.09.061.
12. Luís Cruz-Filipe, Herman Geuvers, and Freek Wiedijk. C-CoRN, the constructive Coq repository at Nijmegen. In International Conference on Mathematical Knowledge Management, pages 88-103. Springer, 2004.
13. Martín Hötzel Escardó. PCF extended with real numbers. Theoretical Computer Science, 162(1):79-115, 1996.
14. Akitoshi Kawamura. Computational complexity in analysis and geometry. University of Toronto, 2011.
15. Akitoshi Kawamura, Norbert Th. Müller, Carsten Rösnick, and Martin Ziegler. Computational Benefit of Smoothness. Journal of Complexity, 2015. URL: https://doi.org/10.1016/j.jco.2015.05.001.
16. Akitoshi Kawamura, Florian Steinberg, and Holger Thies. Parameterized complexity for uniform operators on multidimensional analytic functions and ODE solving. In International Workshop on Logic, Language, Information, and Computation, pages 223-236. Springer, 2018.
17. Michal Konecny. AERN-Real: Arbitrary-precision interval arithmetic for approximating exact real numbers, 2008.
18. Michal Konečný, Florian Steinberg, and Holger Thies. Continuous and Monotone Machines. In Javier Esparza and Daniel Kráľ, editors, 45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020), volume 170 of Leibniz International Proceedings in Informatics (LIPIcs), pages 56:1-56:16, Dagstuhl, Germany, 2020. Schloss Dagstuhl-Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.MFCS.2020.56.
19. Christoph Kreitz and Klaus Weihrauch. Theory of representations. Theoretical computer science, 38:35-53, 1985.
20. Guillaume Melquiond. Proving bounds on real-valued functions with computations. In International Joint Conference on Automated Reasoning, pages 2-17. Springer, 2008.
21. R.E. Moore, R.B. Kearfott, and M.J. Cloud. Introduction to Interval Analysis. SIAM e-books. Society for Industrial and Applied Mathematics (SIAM, 3600 Market Street, Floor 6, Philadelphia, PA 19104), 2009.
22. Norbert Th. Müller. The iRRAM: Exact arithmetic in C++. In Computability and complexity in analysis. 4th international workshop, CCA 2000. Swansea, GB, September 17-19, 2000. Selected papers, pages 222-252. Berlin: Springer, 2001.
23. Florian Steinberg. The Incone library. https://github.com/FlorianSteinberg/incone, 2019. release v1.0.
24. Florian Steinberg, Laurent Thery, and Holger Thies. Computable analysis and notions of continuity in coq. arXiv preprint arXiv:1904.13203, 2019.
25. Klaus Weihrauch. Computable Analysis. Springer, Berlin/Heidelberg, 2000.