Document Open Access Logo

A Zoo of Continuity Properties in Constructive Type Theory

Authors Martin Baillon, Yannick Forster , Assia Mahboubi , Pierre-Marie Pédrot, Matthieu Piquerez

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2025.9.pdf
  • Filesize: 1.02 MB
  • 20 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Constructive mathematics
Keywords
  • type theory
  • constructive mathematics
  • continuity
  • Coq

Metrics

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

Abstract

Continuity principles stating that all functions are continuous play a central role in some schools of constructive mathematics. However, there are different ways to formalise the property of being continuous in constructive foundations. We analyse these continuity properties from the perspective of constructive reverse mathematics. We work in constructive type theory, which can be seen as a minimal foundation for constructive reverse mathematics. We treat continuity of functions F : (Q → A) → R, i.e. with question type Q, answer type A, and result type R. Concretely, we discuss continuity defined via moduli, making the relevant list L : LQ of questions explicit, dialogue trees, making the question-answer process explicit as inductive tree, and tree functions, making the question-answer process explicit as function. We prove equivalences where possible and isolate necessary and sufficient axioms for equivalence proofs. Many of the results we discuss are already present in the works of Hancock, Pattinson, Ghani, Kawai, Fujiwara, Brede, Herbelin, Escardó, and others. Our main contribution is their formulation over a uniform foundation, the observation that no choice axioms are necessary, the generalisation to arbitrary types from natural numbers where possible, and a mechanisation in the Coq/Rocq proof assistant.

Cite As Get BibTex

Martin Baillon, Yannick Forster, Assia Mahboubi, Pierre-Marie Pédrot, and Matthieu Piquerez. A Zoo of Continuity Properties in Constructive Type Theory. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 9:1-9:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.FSCD.2025.9

Author Details

Martin Baillon
  • Nantes Université, École Centrale Nantes, CNRS, Inria, LS2N, UMR 6004, F-44000 Nantes, France
Yannick Forster
  • Inria, Paris, France
Assia Mahboubi
  • Nantes Université, École Centrale Nantes, CNRS, Inria, LS2N, UMR 6004, F-44000 Nantes, France
  • Vrije Universiteit Amsterdam, The Netherlands
Pierre-Marie Pédrot
  • Nantes Université, École Centrale Nantes, CNRS, Inria, LS2N, UMR 6004, F-44000 Nantes, France
Matthieu Piquerez
  • Institut für Mathematik, Goethe-Universität Frankfurt, Germany

Funding

This work has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (grant agreement No.101001995).

Acknowledgements

The idea to investigate connections between different continuity properties was born during fruitful conversations with Yann Leray, Meven Lennon Bertrand and Loïc Pujet. The project then greatly benefited from discussions with Andrej Bauer, Bruno da Rocha Paiva, Martín Escardó, Dominik Kirst, Henri Lombardi and Vincent Rahli. Finally, we want to thank Olivier Bournez and all the attendees from the Continuity, Computability, Constructivity (CCC'2024) workshop for their interesting remarks and thoughts.

Supplementary Materials

References

  1. Martin Baillon, Assia Mahboubi, and Pierre-Marie Pédrot. Gardening with the Pythia A Model of Continuity in a Dependent Setting. In CSL, volume 216 of LIPIcs, pages 5:1-5:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPICS.CSL.2022.5.
  2. Andrej Bauer. An injection from the Baire space to natural numbers. Mathematical Structures in Computer Science, 25(7):1484-1489, 2015. URL: https://doi.org/10.1017/S0960129513000406.
  3. Andrej Bauer. Continuity principles and the KLST theorem. Personal blog post, 2023. URL: https://math.andrej.com/2023/07/19/continuity-principles-and-the-klst-theorem/.
  4. Michael J. Beeson. The nonderivability in intuitionistic formal systems of theorems on the continuity of effective operations. Journal of Symbolic Logic, 40(3):321-346, September 1975. URL: https://doi.org/10.2307/2272158.
  5. Nuria Brede and Hugo Herbelin. On the logical structure of choice and bar induction principles. In LICS, pages 1-13. IEEE, 2021. URL: https://doi.org/10.1109/LICS52264.2021.9470523.
  6. Luitzen E. J. Brouwer. On the domains of definition of functions. In From Frege to Gödel: A source book in mathematical logic, 1879-1931, volume 9, page 446. Harvard University Press, 1927. Google Scholar
  7. Luitzen E. J. Brouwer. Über Definitionsbereiche von-Funktionen. Mathematische Annalen, 97(1):60-75, 1927. URL: https://doi.org/10.1007/BF01447860.
  8. Grigori Samuilovitsch Ceitin. Algorithmic operators in constructive complete separable metric spaces. Doklady Akademii Nauk SSSR, 128:49-52, 1959. Google Scholar
  9. Liron Cohen, Bruno da Rocha Paiva, Vincent Rahli, and Ayberk Tosun. Inductive Continuity via Brouwer Trees. In MFCS, volume 272 of LIPIcs, pages 37:1-37:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPICS.MFCS.2023.37.
  10. Liron Cohen, Yannick Forster, Dominik Kirst, Bruno da Rocha Paiva, and Vincent Rahli. Separating Markov’s Principles. In LICS, pages 28:1-28:14. ACM, 2024. URL: https://doi.org/10.1145/3661814.3662104.
  11. Liron Cohen and Vincent Rahli. Realizing Continuity Using Stateful Computations. In CSL, volume 252 of LIPIcs, pages 15:1-15:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPICS.CSL.2023.15.
  12. Liron Cohen and Vincent Rahli. TT^◻_𝒞: a Family of Extensional Type Theories with Effectful Realizers of Continuity. Log. Methods Comput. Sci., 20(2), 2024. URL: https://doi.org/10.46298/LMCS-20(2:18)2024.
  13. The Coq Development Team. The Coq proof assistant, 2024. URL: https://doi.org/10.5281/ZENODO.11551307.
  14. Thierry Coquand. Metamathematical investigations of a calculus of constructions. Technical Report RR-1088, INRIA, 1989. URL: https://hal.inria.fr/inria-00075471.
  15. Thierry Coquand and Gérard P Huet. The calculus of constructions. Information and Computation, 76(2/3):95-120, 1988. URL: https://doi.org/10.1016/0890-5401(88)90005-3.
  16. Michel Coste, Henri Lombardi, and Marie-Françoise Roy. Dynamical method in algebra: effective Nullstellensätze. Annal of Pure and Applied Logic, 111(3):203-256, 2001. URL: https://doi.org/10.1016/S0168-0072(01)00026-4.
  17. Hannes Diener. Constructive reverse mathematics: Habilitationsschrift, 2018. Revised as https://arxiv.org/abs/1804.05495. URL: https://dspace.ub.uni-siegen.de/handle/ubsi/1306.
  18. Martín Hötzel Escardó. Continuity of Gödel’s System T Definable Functionals via Effectful Forcing. In MFPS, volume 298 of Electronic Notes in Theoretical Computer Science, pages 119-141. Elsevier, 2013. URL: https://doi.org/10.1016/j.entcs.2013.09.010.
  19. Martin Escardó and Paulo Oliva. Conversion of dialogue trees to Brouwer trees. https://www.cs.bham.ac.uk//~mhe/dialogue/dialogue-to-brouwer.agda, 2017.
  20. Yannick Forster, Dominik Kirst, and Niklas Mück. Oracle computability and turing reducibility in the calculus of inductive constructions. In APLAS, volume 14405 of Lecture Notes in Computer Science, pages 155-181. Springer, 2023. URL: https://doi.org/10.1007/978-981-99-8311-7_8.
  21. Yannick Forster, Dominik Kirst, and Niklas Mück. The kleene-post and post’s theorem in the calculus of inductive constructions. In CSL, volume 288 of LIPIcs, pages 29:1-29:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. URL: https://doi.org/10.4230/LIPIcs.CSL.2024.29.
  22. Makoto Fujiwara and Tatsuji Kawai. Equivalence of bar induction and bar recursion for continuous functions with continuous moduli. Annals of Pure and Applied Logic, 170(8):867-890, 2019. URL: https://doi.org/10.1016/j.apal.2019.04.001.
  23. Makoto Fujiwara and Tatsuji Kawai. Characterising Brouwer’s continuity by bar recursion on moduli of continuity. Archive for Mathematical Logic, 60(1-2):241-263, 2021. URL: https://doi.org/10.1007/S00153-020-00740-9.
  24. Neil Ghani, Peter Hancock, and Dirk Pattinson. Continuous Functions on Final Coalgebras. Electronic Notes in Theoretical Computer Science, 249:3-18, August 2009. URL: https://doi.org/10.1016/j.entcs.2009.07.081.
  25. Peter Hancock, Dirk Pattinson, and Neil Ghani. Representations of Stream Processors Using Nested Fixed Points. Logical Methods in Computer Science, Volume 5, Issue 3, September 2009. URL: https://doi.org/10.2168/LMCS-5(3:9)2009.
  26. Hajime Ishihara. Continuity properties in constructive mathematics. Journal of Symbolic Logic, 57(2):557-565, June 1992. URL: https://doi.org/10.2307/2275292.
  27. Hajime Ishihara. Reverse mathematics in Bishop’s constructive mathematics. Philosophia Scientae, (CS 6):43-59, September 2006. URL: https://doi.org/10.4000/philosophiascientiae.406.
  28. Tatsuji Kawai. Principles of bar induction and continuity on Baire space. Journal of Logic and Analysis, 2019. URL: https://doi.org/10.4115/jla.2019.11.ft3.
  29. Tatsuji Kawai. Representing definable functions of ha^ω by neighbourhood functions. Ann. Pure Appl. Log., 170(8):891-909, 2019. URL: https://doi.org/10.1016/J.APAL.2019.04.011.
  30. Stephen Cole Kleene. Countable functionals. 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 81-100. North-Holland, Amsterdam, 1959. Google Scholar
  31. Stephen Cole Kleene. Recursive Functionals and Quantifiers of Finite Types I. Transactions of the American Mathematical Society, 91(1):1, April 1959. URL: https://doi.org/10.2307/1993145.
  32. Georg Kreisel, Daniel Lacombe, and Joseph R. Shoenfield. Partial recursive functionals and effective operations. 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 290-297. North-Holland, Amsterdam, 1959. Google Scholar
  33. Daniel Misselbeck-Wessel and Peter Schuster. Radical theory of Scott-open filters. Theoretical Computer Science, 945:113677, February 2023. URL: https://doi.org/10.1016/j.tcs.2022.12.027.
  34. Christine Paulin-Mohring. Extraction de programmes dans le Calcul des Constructions. (Program Extraction in the Calculus of Constructions). PhD thesis, Paris Diderot University, France, 1989. URL: https://tel.archives-ouvertes.fr/tel-00431825.
  35. Christine Paulin-Mohring. Inductive definitions in the system Coq rules and properties. In International Conference on Typed Lambda Calculi and Applications, pages 328-345. Springer, 1993. URL: https://doi.org/10.1007/BFb0037116.
  36. Sam Sanders. On the computational properties of weak continuity notions. In Twenty Years of Theoretical and Practical Synergies - 20th Conference on Computability in Europe, CiE 2024, Amsterdam, The Netherlands, July 8-12, 2024, Proceedings, pages 113-125, 2024. URL: https://doi.org/10.1007/978-3-031-64309-5_10.
  37. Florian Steinberg, Laurent Thery, and Holger Thies. Computable analysis and notions of continuity in Coq. Logical Methods in Computer Science, Volume 17, Issue 2, May 2021. URL: https://doi.org/10.23638/LMCS-17(2:16)2021.
  38. Jonathan Sterling. Higher order functions and Brouwer’s thesis. Journal of Functional Programming, 31:e11, 2021. URL: https://doi.org/10.1017/s0956796821000095.
  39. Anne Sjerp Troelstra and Dirk van Dalen. Constructivism in mathematics. Vol. I. Studies in Logic and the Foundations of Mathematics, 26, 1988. Google Scholar
  40. Jaap van Oosten. Partial Combinatory Algebras of Functions. Notre Dame Journal of Formal Logic, 52(4):431-448, 2011. URL: https://doi.org/10.1215/00294527-1499381.
  41. Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, and Steve Zdancewic. Interaction trees: representing recursive and impure programs in Coq. Proc. ACM Program. Lang., 4(POPL):51:1-51:32, 2020. URL: https://doi.org/10.1145/3371119.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact