Document Open Access Logo

Continuous and Monotone Machines

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

PDF
Thumbnail PDF

File

LIPIcs.MFCS.2020.56.pdf
  • Filesize: 0.57 MB
  • 16 pages

Document Identifiers

Author Details

Michal Konečný
  • School of Engineering and Applied Science, Aston University, Birmingham, UK
Florian Steinberg
  • INRIA Saclay Île-de-France, Palaiseau, France
Holger Thies
  • Department of Informatics, Kyushu University, Japan

Funding

  • Konečný, Michal: This project has received funding from the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie grant agreement No 731143.
  • Thies, Holger: Supported by JSPS KAKENHI Grant Numbers JP18J10407 and JP20K19744 and by the Japan Society for the Promotion of Science (JSPS), Core-to-Core Program (A. Advanced Research Networks).

Cite As Get BibTex

Michal Konečný, Florian Steinberg, and Holger Thies. Continuous and Monotone Machines. In 45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 170, pp. 56:1-56:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020) https://doi.org/10.4230/LIPIcs.MFCS.2020.56

Abstract

We investigate a variant of the fuel-based approach to modeling diverging computation in type theories and use it to abstractly capture the essence of oracle Turing machines. The resulting objects we call continuous machines. We prove that it is possible to translate back and forth between such machines and names in the standard function encoding used in computable analysis. Put differently, among the operators on Baire space, exactly the partial continuous ones are implementable by continuous machines and the data that such a machine provides is a description of the operator as a sequentially realizable functional. Continuous machines are naturally formulated in type theories and we have formalized our findings in Coq as part of Incone, a Coq library for computable analysis.
The correctness proofs use a classical meta-theory with countable choice. Along the way we formally prove some known results such as the existence of a self-modulating modulus of continuity for partial continuous operators on Baire space. To illustrate their versatility we use continuous machines to specify some algorithms that operate on objects that cannot be fully described by finite means, such as real numbers and functions. We present particularly simple algorithms for finding the multiplicative inverse of a real number and for composition of partial continuous operators on Baire space. Some of the simplicity is achieved by utilizing the fact that continuous machines are compatible with multivalued semantics.

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
    0
    Metadata Views

Related Versions

Supplementary Materials

References

  1. Ana Bove, Alexander Krauss, and Matthieu Sozeau. Partiality and recursion in interactive theorem provers-an overview. Mathematical Structures in Computer Science, 26(1):38-88, 2016. Google Scholar
  2. Vasco Brattka and Guido Gherardi. Completion of choice. arXiv preprint arXiv:1910.13186, 2019. Google Scholar
  3. Vasco Brattka, Guido Gherardi, and Arno Pauly. Weihrauch complexity in computable analysis. arXiv preprint arXiv:1707.03202, 2017. Google Scholar
  4. Cyril Cohen, Maxime Dénès, and Anders Mörtberg. Refinements for free! In International Conference on Certified Programs and Proofs, pages 147-162. Springer, 2013. Google Scholar
  5. Robert L Constable. Type two computational complexity. In Proceedings of the fifth annual ACM symposium on Theory of computing, pages 108-121. ACM, 1973. Google Scholar
  6. 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
  7. Damir D. Dzhafarov. Joins in the strong Weihrauch degrees. Math. Res. Lett., 26(3):749-767, 2019. URL: https://doi.org/10.4310/MRL.2019.v26.n3.a5.
  8. Yannick Forster, Dominik Kirst, and Florian Steinberg. Towards Extraction of Continuity Moduli in Coq. EUTYPES-TYPES 2020, 2020. Google Scholar
  9. Andrzej Grzegorczyk. On the definitions of computable real continuous functions. Fund. Math., 44:61-71, 1957. Google Scholar
  10. Martín Hötzel Escardó and Chuangjie Xu. The inconsistency of a brouwerian continuity principle with the curry-howard interpretation. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2015. Google Scholar
  11. Akitoshi Kawamura. Computational complexity in analysis and geometry. University of Toronto, 2011. Google Scholar
  12. Stephen Cole Kleene. Countable functionals. Constructivity in Mathematics: proceedings of the colloquium held at Amsterdam, 1959. Google Scholar
  13. Ker-I Ko. Complexity theory of real functions. Progress in Theoretical Computer Science. Birkhäuser Boston Inc., Boston, MA, 1991. Google Scholar
  14. Michal Konecnỳ, Florian Steinberg, and Holger Thies. Continuous and monotone machines. CoRR, abs/2005.01624, 2020. URL: http://arxiv.org/abs/2005.01624.
  15. Georg Kreisel. Interpretation of analysis by means of constructive functionals of finite types. In Constructivity in mathematics: Proceedings of the colloquium held at Amsterdam, 1957 (edited by A. Heyting), Studies in Logic and the Foundations of Mathematics, pages 101-128. North-Holland Publishing Co., Amsterdam, 1959. Google Scholar
  16. Christoph Kreitz and Klaus Weihrauch. Theory of representations. Theoretical computer science, 38:35-53, 1985. Google Scholar
  17. 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
  18. Branimir Lambov. The basic feasible functionals in computable analysis. Journal of Complexity, 22(6):909-917, 2006. Google Scholar
  19. Peter Lammich. Automatic data refinement. In International Conference on Interactive Theorem Proving, pages 84-99. Springer, 2013. Google Scholar
  20. John Longley. The sequentially realizable functionals. Annals of Pure and Applied Logic, 117(1-3):1-93, 2002. Google Scholar
  21. John Longley and Dag Normann. Higher-order computability, volume 100. Springer, 2015. Google Scholar
  22. Dag Normann. Computability over the partial continuous functionals. The Journal of Symbolic Logic, 65(3):1133-1142, 2000. Google Scholar
  23. Arno Pauly and Martin Ziegler. Relative computability and uniform continuity of relations. J. Logic & Analysis, 5, 2013. Google Scholar
  24. Matthias Schröeder. Admissible Representations for Continuous Computations. PhD thesis, FernUniversität Hagen, 2002. Google Scholar
  25. Matthieu Sozeau, Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster, Fabian Kunze, Gregory Malecha, Nicolas Tabareau, and Théo Winterhalter. The MetaCoq Project. working paper or preprint, June 2019. URL: https://hal.inria.fr/hal-02167423.
  26. Florian Steinberg, Laurent Thery, and Holger Thies. Quantitative continuity and computable analysis in coq. arXiv preprint arXiv:1904.13203, 2019. Google Scholar
  27. Alan Mathison 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.
  28. Jaap Van Oosten et al. Partial combinatory algebras of functions. Notre Dame Journal of formal logic, 52(4):431-448, 2011. Google Scholar
  29. Klaus Weihrauch. Computable Analysis. Springer, Berlin/Heidelberg, 2000. Google Scholar
  30. Chuangjie Xu and Martín Escardó. A constructive model of uniform continuity. In International Conference on Typed Lambda Calculi and Applications, pages 236-249. Springer, 2013. 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
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact