Computable Analysis for Verified Exact Real Computation

Authors Michal Konečný , Florian Steinberg, Holger Thies



PDF
Thumbnail PDF

File

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

Document Identifiers

Author Details

Michal Konečný
  • School of Engineering and Applied Science, Aston University, UK
Florian Steinberg
  • Inria Saclay, France
Holger Thies
  • Department of Informatics, Kyushu University, Japan

Cite As Get BibTex

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
    PDF Downloads

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. Google Scholar
  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. Google Scholar
  4. Merrie Bergmann. An introduction to many-valued and fuzzy logic: semantics, algebras, and derivation systems. Cambridge University Press, 2008. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  13. Martín Hötzel Escardó. PCF extended with real numbers. Theoretical Computer Science, 162(1):79-115, 1996. Google Scholar
  14. Akitoshi Kawamura. Computational complexity in analysis and geometry. University of Toronto, 2011. Google Scholar
  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. Google Scholar
  17. Michal Konecny. AERN-Real: Arbitrary-precision interval arithmetic for approximating exact real numbers, 2008. Google Scholar
  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. Google Scholar
  20. Guillaume Melquiond. Proving bounds on real-valued functions with computations. In International Joint Conference on Automated Reasoning, pages 2-17. Springer, 2008. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  25. Klaus Weihrauch. Computable Analysis. Springer, Berlin/Heidelberg, 2000. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail