Document Open Access Logo

Quantitative Continuity and Computable Analysis in Coq

Authors Florian Steinberg, Laurent Théry, Holger Thies

PDF
Thumbnail PDF

File

LIPIcs.ITP.2019.28.pdf
  • Filesize: 0.59 MB
  • 21 pages

Document Identifiers

Author Details

Florian Steinberg
  • INRIA Saclay, France
Laurent Théry
  • INRIA Sophia-Antipolis, France
Holger Thies
  • Kyushu University, Japan

Funding

  • Steinberg, Florian: Supported by the ANR project FastRelax (ANR-14-CE25-0018-01) of the French National Agency for Research and by EU-MSCA-RISE project 731143 "Computing with Infinite Data" (CID).
  • Théry, Laurent: Supported by the ANR project FastRelax (ANR-14-CE25-0018-01) of the French National Agency for Research.
  • Thies, Holger: Supported by JSPS KAKENHI Grant Number JP18J10407 and by the Japan Society for the Promotion of Science (JSPS), Core-to-Core Program (A. Advanced Research Networks).

Acknowledgements

The first and last authors would like to thank Hugo Férée, Akitoshi Kawamura and Matthias Schröder for discussion on the topics of this paper.

Cite AsGet BibTex

Florian Steinberg, Laurent Théry, and Holger Thies. Quantitative Continuity and Computable Analysis in Coq. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 28:1-28:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.ITP.2019.28

Abstract

We give a number of formal proofs of theorems from the field of computable analysis. Many of our results specify executable algorithms that work on infinite inputs by means of operating on finite approximations and are proven correct in the sense of computable analysis. The development is done in the proof assistant Coq and heavily relies on the Incone library for information theoretic continuity. This library is developed by one of the authors and the results of this paper extend the library. While full executability in a formal development of mathematical statements about real numbers and the like is not a feature that is unique to the Incone library, its original contribution is to adhere to the conventions of computable analysis to provide a general purpose interface for algorithmic reasoning on continuous structures. The paper includes a brief description of the most important concepts of Incone and its sub libraries mf and Metric. The results that provide complete computational content include that the algebraic operations and the efficient limit operator on the reals are computable, that the countably infinite product of a space with itself is isomorphic to a space of functions, compatibility of the enumeration representation of subsets of natural numbers with the abstract definition of the space of open subsets of the natural numbers, and that continuous realizability implies sequential continuity. We also describe many non-computational results that support the correctness of definitions from the library. These include that the information theoretic notion of continuity used in the library is equivalent to the metric notion of continuity on Baire space, a complete comparison of the different concepts of continuity that arise from metric and represented space structures and the discontinuity of the unrestricted limit operator on the real numbers and the task of selecting an element of a closed subset of the natural numbers.

Subject Classification

ACM Subject Classification
  • Mathematics of computing → Continuous functions
  • Theory of computation → Models of computation
  • Software and its engineering → Formal methods
Keywords
  • computable analysis
  • Coq
  • contionuous functionals
  • discontinuity
  • closed choice on the naturals

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

Supplementary Materials

References

  1. Klaus Ambos-Spies, Ulrike Brandt, and Martin Ziegler. Real Benefit of Promises and Advice. In Paola Bonizzoni, Vasco Brattka, and Benedikt Löwe, editors, The Nature of Computation. Logic, Algorithms, Applications, pages 1-11, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. Google Scholar
  2. Jeremy Avigad and Vasco Brattka. Computability and analysis: the legacy of Alan Turing, page 1–47. Lecture Notes in Logic. Cambridge University Press, 2014. URL: https://doi.org/10.1017/CBO9781107338579.002.
  3. Andrej Bauer. The Realizability Approach to Computable Analysis and Topology. PhD thesis, Carnegie Mellon University, Pittsburgh, PA, USA, 2000. AAI3002721. Google Scholar
  4. Andrej Bauer and C.A. Stone. RZ: A tool for bringing constructive and computable mathematics closer to programming practice. Computation and Logic in the Real World. CiE 2007. Lecture Notes in Computer Science, vol 4497., 2007. Google Scholar
  5. Yves Bertot, Laurence Rideau, and Laurent Théry. Distant decimals of π. Journal of Automated Reasoning, pages 1-45, 2017. URL: https://hal.inria.fr/hal-01582524.
  6. Errett Bishop and Douglas Bridges. Constructive analysis, volume 279. Springer Science & Business Media, 2012. Google Scholar
  7. Jens Blanck. Exact real arithmetic systems: Results of competition. In Computability and complexity in analysis. 4th international workshop, CCA 2000. Swansea, GB, September 17-19, 2000. Selected papers, pages 389-393. Berlin: Springer, 2001. Google Scholar
  8. Lenore Blum, Mike Shub, and Steve Smale. On a theory of computation and complexity over the real numbers: NP-completeness, recursive functions and universal machines. Bulletin of the American Mathematical Society, 21(1):1-46, 1989. Google Scholar
  9. Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, and Pierre Weis. Wave Equation Numerical Resolution: a Comprehensive Mechanized Proof of a C Program. Journal of Automated Reasoning, 50(4):423-456, April 2013. URL: https://doi.org/10.1007/s10817-012-9255-4.
  10. Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, and Micaela Mayero. A Coq Formal Proof of the Lax-Milgram theorem. In Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, pages 79-89, Paris, France, January 2017. ACM. URL: https://doi.org/10.1145/3018610.3018625.
  11. Sylvie Boldo and Guillaume Melquiond. Computer Arithmetic and Formal Proofs. ISTE Press - Elsevier, December 2017. URL: https://hal.inria.fr/hal-01632617.
  12. Vasco Brattka and Atsushi Yoshikawa. Towards computability of elliptic boundary value problems in variational formulation. Journal of Complexity, 22(6):858-880, 2006. Computability and Complexity in Analysis. URL: https://doi.org/10.1016/j.jco.2006.04.007.
  13. Cyril Cohen. Construction of real algebraic numbers in Coq. In Lennart Beringer and Amy Felty, editors, ITP - 3rd International Conference on Interactive Theorem Proving - 2012, Princeton, United States, August 2012. Springer. Google Scholar
  14. 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
  15. K. Deimling. Multivalued Differential Equations. De Gruyter series in nonlinear analysis and applications. W. de Gruyter, 1992. Google Scholar
  16. Ali Enayat. δ as a continuous function of x and ε. The American Mathematical Monthly, 107(2):151-155, 2000. Google Scholar
  17. Martín Escardó and Chuangjie Xu. A constructive manifestation of the Kleene–Kreisel continuous functionals. Annals of Pure and Applied Logic, 167(9):770-793, 2016. Fourth Workshop on Formal Topology (4WFTop). URL: https://doi.org/10.1016/j.apal.2016.04.011.
  18. Hugo Feree. Game Semantics Approach to Higher-order Complexity. J. Comput. Syst. Sci., 87(C):1-15, August 2017. URL: https://doi.org/10.1016/j.jcss.2017.02.003.
  19. Hugo Férée, Samuel Hym, Micaela Mayero, Jean-Yves Moyen, and David Nowak. Formal proof of polynomial-time complexity with quasi-interpretations. In Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, pages 146-157. ACM, 2018. Google Scholar
  20. Yannick Forster and Gert Smolka. Call-by-Value Lambda Calculus as a Model of Computation in Coq. Journal of Automated Reasoning, 2018. Google Scholar
  21. A. Grzegorczyk. On the definitions of computable real continuous functions. Fund. Math., 44:61-71, 1957. Google Scholar
  22. Fabian Immler and Johannes Hölzl. Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL. In ITP, volume 7406 of LNCS, pages 377-392, 2012. Google Scholar
  23. Bruce M. Kapron and Stephen A. Cook. A New Characterization of Type-2 Feasibility. SIAM J. Comput., 25:117-132, 1996. Google Scholar
  24. Bruce M. Kapron and Florian Steinberg. Type-two polynomial-time and restricted lookahead. In LICS, 2018. Google Scholar
  25. Akitoshi Kawamura and Stephen Cook. Complexity theory for operators in analysis. ACM Transactions in Computation Theory, 4(2):Article 5, 2012. Google Scholar
  26. 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
  27. Akitoshi Kawamura, Florian Steinberg, and Holger Thies. Second-order linear-time computability with applications in computable analysis. 15th Annual Conference on Theory and Applications of Models of Computation, 2019. extended abstract accepted for presentation at TAMC 2019. Google Scholar
  28. S.C. Kleene. Countable functionals. Constructivity in Mathematics: proceedings of the colloquium held at Amsterdam, 1959. Google Scholar
  29. Ker-I Ko. Complexity theory of real functions. Progress in Theoretical Computer Science. Birkhäuser Boston Inc., Boston, MA, 1991. Google Scholar
  30. Michal Konecný and Eike Neumann. Representations and evaluation strategies for feasibly approximable functions. CoRR, abs/1710.03702, 2017. URL: http://arxiv.org/abs/1710.03702.
  31. Georg Kreisel. Interpretation of analysis by means of constructive functionals of finite type, Constructivity in Mathematics, 1959. Google Scholar
  32. Christoph Kreitz and Klaus Weihrauch. Theory of representations. Theoretical computer science, 38:35-53, 1985. Google Scholar
  33. Daniel Lacombe. Sur les possibilités d'extension de la notion de fonction récursive aux fonctions d'une ou plusieurs variables réelles. In Le raisonnement en mathématiques et en sciences expérimentales, Colloques Internationaux du Centre National de la Recherche Scientifique, LXX, pages 67-75. Editions du Centre National de la Recherche Scientifique, Paris, 1958. Google Scholar
  34. John Longley and Dag Normann. Higher-order computability, volume 100. Springer, 2015. Google Scholar
  35. Robert S. Lubarsky and Michael Rathjen. On the constructive Dedekind reals. Logic and Analysis, 1(2):131-152, May 2008. URL: https://doi.org/10.1007/s11813-007-0005-6.
  36. Marco Maggesi. A Formalization of Metric Spaces in HOL Light. J. Autom. Reasoning, 60(2):237-254, 2018. Google Scholar
  37. Evgeny Makarov and Bas Spitters. The Picard Algorithm for Ordinary Differential Equations in Coq. In ITP, volume 7998 of Lecture Notes in Computer Science, pages 463-468. Springer, 2013. Google Scholar
  38. The Mathematical Components library. . URL: https://math-comp.github.io/math-comp/.
  39. Kurt Mehlhorn. Polynomial and abstract subrecursive classes. Journal of Computer and System Sciences, 12(2):147-178, 1976. URL: https://doi.org/10.1016/S0022-0000(76)80035-9.
  40. 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
  41. Norbert Th. Müller, Sewon Park, Norbert Preining, and Martin Ziegler. On Formal Verification in Imperative Multivalued Programming over Continuous Data Types. CoRR, abs/1608.05787, 2016. URL: http://arxiv.org/abs/1608.05787.
  42. Eike Neumann and Florian Steinberg. Parametrised second-order complexity theory with applications to the study of interval computation. CoRR, abs/1711.10530, 2017. submitted for publication. URL: http://arxiv.org/abs/1711.10530.
  43. Russell O'Connor. Essential Incompleteness of Arithmetic Verified by Coq. In Joe Hurd and Tom Melham, editors, Theorem Proving in Higher Order Logics, pages 245-260, Berlin, Heidelberg, 2005. Springer Berlin Heidelberg. Google Scholar
  44. Russell O'Connor. Incompleteness & Completeness: Formalizing Logic and Analysis in Type Theory. PhD thesis, Radboud Universiteit Nijmegen, 2009. Google Scholar
  45. Arno Pauly. Multi-valued functions in computability theory. In Conference on Computability in Europe, pages 571-580. Springer, 2012. Google Scholar
  46. Arno Pauly. On the topological aspects of the theory of represented spaces. Computability, 5(2):159-180, 2016. Google Scholar
  47. Arno Pauly and Martin Ziegler. Relative computability and uniform continuity of relations. J. Logic & Analysis, 5, 2013. Google Scholar
  48. Marian B. Pour-El and J. Ian Richards. Computability in Analysis and Physics, volume Volume 1 of Perspectives in Mathematical Logic. Springer-Verlag, Berlin, 1989. Google Scholar
  49. Marian Boykan Pour-El and Jerome Caldwell. On a simple definition of computable function of a real variable-with applications to functions of a complex variable. Mathematical Logic Quarterly, 21(1):1-19, 1975. Google Scholar
  50. Matthias Schröder. Extended admissibility. Theoretical computer science, 284(2):519-538, 2002. Google Scholar
  51. Matthias Schröder and Florian Steinberg. Bounded time computation on metric spaces and Banach spaces. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017, pages 1-12. IEEE Computer Society, 2017. URL: https://doi.org/10.1109/LICS.2017.8005139.
  52. Matthias Schröeder. Admissible Representations for Continuous Computations. PhD thesis, FernUniversität Hagen, 2002. Google Scholar
  53. Matthias Schröder. Spaces allowing Type-2 Complexity Theory revisited. Math. Log. Q., 50:443-459, September 2004. URL: https://doi.org/10.1002/malq.200310111.
  54. Svetlana Selivanova and Victor Selivanov. Computing Solutions of Symmetric Hyperbolic Systems of PDE’s. Electron. Notes Theor. Comput. Sci., 221:243-255, December 2008. URL: https://doi.org/10.1016/j.entcs.2008.12.021.
  55. Robert I Soare. Recursively enumerable sets and degrees. Bulletin of the American Mathematical Society, 84(6):1149-1181, 1978. Google Scholar
  56. Florian Steinberg. The Incone library. https://github.com/FlorianSteinberg/incone, 2019. release v1.0.
  57. Florian Steinberg. The Metric library. , 2019. release v1.0. URL: https://github.com/FlorianSteinberg/metric.
  58. Florian Steinberg. The Mf library. , 2019. release v1.0. URL: https://github.com/FlorianSteinberg/mf.
  59. Florian Steinberg. The Rlzrs library. , 2019. release v1.0. URL: https://github.com/FlorianSteinberg/rlzrs.
  60. Florian Steinberg, Laurent Thery, and Holger Thies. Quantitative continuity and computable analysis in Coq. working paper or preprint, April 2019. URL: https://hal.inria.fr/hal-02088293.
  61. A. S. Troelstra and D. van Dalen. Constructivism in mathematics. Vol. II, volume 123 of Studies in Logic and the Foundations of Mathematics. North-Holland Publishing Co., Amsterdam, 1988. Google Scholar
  62. A. M. Turing. On computable numbers, with an application to the Entscheidungsproblem. Proceedings of the London Mathematical Society, 2(1):230-265, 1936. URL: https://doi.org/10.1112/plms/s2-42.1.230.
  63. Alan Mathison Turing. On computable numbers, with an application to the Entscheidungsproblem. A correction. Proceedings of the London Mathematical Society, 2(1):544-546, 1938. Google Scholar
  64. Klaus Weihrauch. Computability on computable metric spaces. Theoretical Computer Science, 113(2):191-210, 1993. Google Scholar
  65. Klaus Weihrauch. Computable Analysis. Springer, Berlin/Heidelberg, 2000. Google Scholar
  66. Maximilian Wuttke. Verified Programming of Turing Machines in Coq. Master’s thesis, Saarland University, 2018. Google Scholar
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact