Document Open Access Logo

Inductive Continuity via Brouwer Trees

Authors Liron Cohen , Bruno da Rocha Paiva , Vincent Rahli , Ayberk Tosun

PDF
Thumbnail PDF

File

LIPIcs.MFCS.2023.37.pdf
  • Filesize: 1.07 MB
  • 16 pages

Document Identifiers

Author Details

Liron Cohen
  • Ben-Gurion University, Beer-Sheva, Israel
Bruno da Rocha Paiva
  • University of Birmingham, UK
Vincent Rahli
  • University of Birmingham, UK
Ayberk Tosun
  • University of Birmingham, UK

Funding

  • Cohen, Liron: This research was partially supported by Grant No. 2020145 from the United States-Israel Binational Science Foundation (BSF).

Acknowledgements

We would like to thank Martin Escardo, Martin Baillon, and Yannick Forster for useful discussions about continuity and dialogue trees.

Cite AsGet BibTex

Liron Cohen, Bruno da Rocha Paiva, Vincent Rahli, and Ayberk Tosun. Inductive Continuity via Brouwer Trees. In 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 272, pp. 37:1-37:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.MFCS.2023.37

Abstract

Continuity is a key principle of intuitionistic logic that is generally accepted by constructivists but is inconsistent with classical logic. Most commonly, continuity states that a function from the Baire space to numbers, only needs approximations of the points in the Baire space to compute. More recently, another formulation of the continuity principle was put forward. It states that for any function F from the Baire space to numbers, there exists a (dialogue) tree that contains the values of F at its leaves and such that the modulus of F at each point of the Baire space is given by the length of the corresponding branch in the tree. In this paper we provide the first internalization of this "inductive" continuity principle within a computational setting. Concretely, we present a class of intuitionistic theories that validate this formulation of continuity thanks to computations that construct such dialogue trees internally to the theories using effectful computations. We further demonstrate that this inductive continuity principle implies other forms of continuity principles.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Theory of computation → Constructive mathematics
Keywords
  • Continuity
  • Dialogue trees
  • Stateful computations
  • Intuitionistic Logic
  • Extensional Type Theory
  • Constructive Type Theory
  • Realizability
  • Theorem proving
  • Agda

Metrics

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

Supplementary Materials

References

  1. Michael Gordon Abbott. Categories of containers. PhD thesis, University of Leicester, England, UK, 2003. URL: https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.401007.
  2. Agda wiki. URL: http://wiki.portal.chalmers.se/agda/pmwiki.php.
  3. 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.
  4. Michael J. Beeson. Foundations of Constructive Mathematics. Springer, 1985. Google Scholar
  5. Stefano Berardi, Marc Bezem, and Thierry Coquand. On the computational content of the axiom of choice. J. Symb. Log., 63(2):600-622, 1998. URL: https://doi.org/10.2307/2586854.
  6. Nuria Brede and Hugo Herbelin. On the logical structure of choice and bar induction principles. In LICS, pages 1-13, 2021. URL: https://doi.org/10.1109/LICS52264.2021.9470523.
  7. Douglas Bridges and Fred Richman. Varieties of Constructive Mathematics. London Mathematical Society Lecture Notes Series. Cambridge University Press, 1987. Google Scholar
  8. L.E.J. Brouwer. From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931, chapter On the Domains of Definition of Functions, pages 1923b, 1954, and 1954a. Harvard University Press, 1927. Google Scholar
  9. Venanzio Capretta and Tarmo Uustalu. A coalgebraic view of bar recursion and bar induction. In Bart Jacobs and Christof Löding, editors, FOSSACS, volume 9634 of LNCS, pages 91-106. Springer, 2016. URL: https://doi.org/10.1007/978-3-662-49630-5_6.
  10. Liron Cohen and Vincent Rahli. Constructing unprejudiced extensional type theories with choices via modalities. In FSCD, volume 228 of LIPIcs, pages 10:1-10:23. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.FSCD.2022.10.
  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. Thierry Coquand and Guilhem Jaber. A note on forcing and type theory. Fundam. Inform., 100(1-4):43-52, 2010. URL: https://doi.org/10.3233/FI-2010-262.
  13. Thierry Coquand and Guilhem Jaber. A computational interpretation of forcing in type theory. In Epistemology versus Ontology, volume 27 of Logic, Epistemology, and the Unity of Science, pages 203-213. Springer, 2012. URL: https://doi.org/10.1007/978-94-007-4435-6_10.
  14. M. J. Cresswell and G. E. Hughes. A New Introduction to Modal Logic. Routledge, 1996. Google Scholar
  15. Michael A. E. Dummett. Elements of Intuitionism. Clarendon Press, second edition, 2000. Google Scholar
  16. Peter Dybjer and Anton Setzer. A finite axiomatization of inductive-recursive definitions. In TLCA, volume 1581 of LNCS, pages 129-146. Springer, 1999. URL: https://doi.org/10.1007/3-540-48959-2_11.
  17. Martín Escardó and Paulo Oliva. Dialogue to brouwer, 2017. URL: https://www.cs.bham.ac.uk/~mhe/dialogue/dialogue-to-brouwer.html.
  18. Martín H. Escardó and Chuangjie Xu. The inconsistency of a Brouwerian continuity principle with the Curry-Howard interpretation. In TLCA, volume 38 of LIPIcs, pages 153-164. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015. URL: https://doi.org/10.4230/LIPIcs.TLCA.2015.153.
  19. Martín Hötzel Escardó. Continuity of Gödel’s system T definable functionals via effectful forcing. Electr. Notes Theor. Comput. Sci., 298:119-141, 2013. URL: https://doi.org/10.1016/j.entcs.2013.09.010.
  20. Neil Ghani, Peter G. Hancock, and Dirk Pattinson. Continuous functions on final coalgebras. In CMCS, volume 164 of ENTCS, pages 141-155. Elsevier, 2006. URL: https://doi.org/10.1016/j.entcs.2006.06.009.
  21. Neil Ghani, Peter G. Hancock, and Dirk Pattinson. Continuous functions on final coalgebras. In Samson Abramsky, Michael W. Mislove, and Catuscia Palamidessi, editors, MFPS, volume 249 of ENTCS, pages 3-18. Elsevier, 2009. URL: https://doi.org/10.1016/j.entcs.2009.07.081.
  22. Neil Ghani, Peter G. Hancock, and Dirk Pattinson. Representations of stream processors using nested fixed points. Log. Methods Comput. Sci., 5(3), 2009. URL: http://arxiv.org/abs/0905.4813.
  23. S.C. Kleene. Recursive functionals and quantifiers of finite types revisited i. In Generalized Recursion Theory II, volume 94 of Studies in Logic and the Foundations of Mathematics, pages 185-222. Elsevier, 1978. URL: https://doi.org/10.1016/S0049-237X(08)70933-9.
  24. Stephen C. Kleene and Richard E. Vesley. The Foundations of Intuitionistic Mathematics, especially in relation to recursive functions. North-Holland Publishing Company, 1965. Google Scholar
  25. Georg Kreisel. On weak completeness of intuitionistic predicate logic. J. Symb. Log., 27(2):139-158, 1962. URL: https://doi.org/10.2307/2964110.
  26. Saul A. Kripke. Semantical analysis of modal logic i. normal propositional calculi. Zeitschrift fur mathematische Logik und Grundlagen der Mathematik, 9(5-6):67-96, 1963. URL: https://doi.org/10.1002/malq.19630090502.
  27. Saul A. Kripke. Semantical analysis of intuitionistic logic i. In Formal Systems and Recursive Functions, volume 40 of Studies in Logic and the Foundations of Mathematics, pages 92-130. Elsevier, 1965. URL: https://doi.org/10.1016/S0049-237X(08)71685-9.
  28. John Longley. When is a functional program not a functional program? In ICFP, pages 1-7. ACM, 1999. URL: https://doi.org/10.1145/317636.317775.
  29. Pierre-Marie Pédrot and Nicolas Tabareau. An effectful way to eliminate addiction to dependence. In LICS, pages 1-12. IEEE Computer Society, 2017. URL: https://doi.org/10.1109/LICS.2017.8005113.
  30. Andrew M Pitts. Nominal sets: Names and symmetry in computer science, volume 57 of cambridge tracts in theoretical computer science, 2013. Google Scholar
  31. Vincent Rahli. Exercising nuprl’s open-endedness. In ICMS, volume 9725 of LNCS, pages 18-27. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-42432-3_3.
  32. Vincent Rahli and Mark Bickford. A nominal exploration of intuitionism. In Jeremy Avigad and Adam Chlipala, editors, CPP, pages 130-141. ACM, 2016. URL: https://doi.org/10.1145/2854065.2854077.
  33. Vincent Rahli and Mark Bickford. Validating brouwer’s continuity principle for numbers using named exceptions. MSCS, pages 1-49, 2017. URL: https://doi.org/10.1017/S0960129517000172.
  34. Vincent Rahli, Mark Bickford, Liron Cohen, and Robert L. Constable. Bar induction is compatible with constructive type theory. J. ACM, 66(2):13:1-13:35, 2019. URL: https://doi.org/10.1145/3305261.
  35. Jonathan Sterling. Higher order functions and brouwer’s thesis. J. Funct. Program., 31:e11, 2021. URL: https://doi.org/10.1017/S0956796821000095.
  36. Anne S. Troelstra and Dirk van Dalen. Constructivism in Mathematics An Introduction, volume 121 of Studies in Logic and the Foundations of Mathematics. Elsevier, 1988. Google Scholar
  37. A.S. Troelstra. Metamathematical Investigation of Intuitionistic Arithmetic and Analysis. New York, Springer, 1973. Google Scholar
  38. A.S. Troelstra. A note on non-extensional operations in connection with continuity and recursiveness. Indagationes Mathematicae, 39(5):455-462, 1977. URL: https://doi.org/10.1016/1385-7258(77)90060-9.
  39. Wim Veldman. Understanding and using Brouwer’s continuity principle. In Reuniting the Antipodes — Constructive and Nonstandard Views of the Continuum, volume 306 of Synthese Library, pages 285-302. Springer Netherlands, 2001. URL: https://doi.org/10.1007/978-94-015-9757-9_24.
  40. Chuangjie Xu. A continuous computational interpretation of type theories. PhD thesis, University of Birmingham, UK, 2015. URL: http://etheses.bham.ac.uk/5967/.
  41. Chuangjie Xu and Martín Hötzel Escardó. A constructive model of uniform continuity. In TLCA, volume 7941 of LNCS, pages 236-249. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-38946-7_18.
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 Imprint Privacy Contact