Document Open Access Logo

Realizing Continuity Using Stateful Computations

Authors Liron Cohen , Vincent Rahli

PDF
Thumbnail PDF

File

LIPIcs.CSL.2023.15.pdf
  • Filesize: 1.06 MB
  • 18 pages

Document Identifiers

Author Details

Liron Cohen
  • Ben-Gurion University of the Negev, Beer-Sheva, Israel
Vincent Rahli
  • 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).

Cite AsGet BibTex

Liron Cohen and Vincent Rahli. Realizing Continuity Using Stateful Computations. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 15:1-15:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.CSL.2023.15

Abstract

The principle of continuity is a seminal property that holds for a number of intuitionistic theories such as System T. Roughly speaking, it states that functions on real numbers only need approximations of these numbers to compute. Generally, continuity principles have been justified using semantical arguments, but it is known that the modulus of continuity of functions can be computed using effectful computations such as exceptions or reference cells. This paper presents a class of intuitionistic theories that features stateful computations, such as reference cells, and shows that these theories can be extended with continuity axioms. The modulus of continuity of the functionals on the Baire space is directly computed using the stateful computations enabled in the theory.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Theory of computation → Constructive mathematics
Keywords
  • Continuity
  • Stateful computations
  • Intuitionism
  • 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. Agda wiki. URL: http://wiki.portal.chalmers.se/agda/pmwiki.php.
  2. Stuart F. Allen, Mark Bickford, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo, and Evan Moran. Innovations in computational type theory using Nuprl. J. Applied Logic, 4(4):428-469, 2006. URL: https://doi.org/10.1016/j.jal.2005.10.005.
  3. Martin Baillon, Assia Mahboubi, and Pierre-Marie Pédrot. Gardening with the pythia A model of continuity in a dependent setting. In Florin Manea and Alex Simpson, editors, 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. Douglas Bridges and Fred Richman. Varieties of Constructive Mathematics. London Mathematical Society Lecture Notes Series. Cambridge University Press, 1987. URL: https://doi.org/10.1017/CBO9780511565663.
  6. Liron Cohen and Vincent Rahli. Constructing unprejudiced extensional type theories with choices via modalities. In Amy P. Felty, editor, 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.
  7. Robert L. Constable, Stuart F. Allen, Mark Bromley, Rance Cleaveland, J. F. Cremer, Robert W. Harper, Douglas J. Howe, Todd B. Knoblock, Nax P. Mendler, Prakash Panangaden, James T. Sasaki, and Scott F. Smith. Implementing mathematics with the Nuprl proof development system. Prentice-Hall, Inc., Upper Saddle River, NJ, USA, 1986. Google Scholar
  8. 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.
  9. 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.
  10. M. J. Cresswell and G. E. Hughes. A New Introduction to Modal Logic. Routledge, 1996. Google Scholar
  11. Michael A. E. Dummett. Elements of Intuitionism. Clarendon Press, second edition, 2000. Google Scholar
  12. Martín H. Escardó and Chuangjie Xu. The inconsistency of a Brouwerian continuity principle with the Curry-Howard interpretation. In TLCA 2015, volume 38 of LIPIcs, pages 153-164. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015. URL: https://doi.org/10.4230/LIPIcs.TLCA.2015.153.
  13. 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.
  14. Jean-Yves Girard, Paul Taylor, and Yves Lafont. Proofs and Types. Cambridge University Press, 1989. Google Scholar
  15. 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
  16. Georg Kreisel. On weak completeness of intuitionistic predicate logic. J. Symb. Log., 27(2):139-158, 1962. URL: https://doi.org/10.2307/2964110.
  17. Georg Kreisel and Anne S. Troelstra. Formal systems for some branches of intuitionistic analysis. Annals of Mathematical Logic, 1(3):229-387, 1970. URL: https://doi.org/10.1016/0003-4843(70)90001-X.
  18. 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.
  19. Saul A. Kripke. Semantical analysis of intuitionistic logic i. In J.N. Crossley and M.A.E. Dummett, editors, 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.
  20. John Longley. When is a functional program not a functional program? In ICFP'99, pages 1-7. ACM, 1999. URL: https://doi.org/10.1145/317636.317775.
  21. Joan R. Moschovakis. An intuitionistic theory of lawlike, choice and lawless sequences. In Logic Colloquium'90: ASL Summer Meeting in Helsinki, pages 191-209. Association for Symbolic Logic, 1993. Google Scholar
  22. Pierre-Marie Pédrot and Nicolas Tabareau. An effectful way to eliminate addiction to dependence. In LICS 2017, pages 1-12. IEEE Computer Society, 2017. URL: https://doi.org/10.1109/LICS.2017.8005113.
  23. Andrew M Pitts. Nominal sets: Names and symmetry in computer science, volume 57 of cambridge tracts in theoretical computer science, 2013. Google Scholar
  24. Vincent Rahli and Mark Bickford. A nominal exploration of intuitionism. In Jeremy Avigad and Adam Chlipala, editors, CPP 2016, pages 130-141. ACM, 2016. Extended version: http://www.nuprl.org/html/Nuprl2Coq/continuity-long.pdf. URL: https://doi.org/10.1145/2854065.2854077.
  25. Vincent Rahli and Mark Bickford. Validating brouwer’s continuity principle for numbers using named exceptions. Mathematical Structures in Computer Science, pages 1-49, 2017. URL: https://doi.org/10.1017/S0960129517000172.
  26. Anne S. Troelstra. Choice sequences: a chapter of intuitionistic mathematics. Clarendon Press Oxford, 1977. Google Scholar
  27. Anne S. Troelstra. Choice sequences and informal rigour. Synthese, 62(2):217-227, 1985. Google Scholar
  28. 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
  29. A.S. Troelstra. Metamathematical Investigation of Intuitionistic Arithmetic and Analysis. New York, Springer, 1973. Google Scholar
  30. 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.
  31. Mark van Atten and Dirk van Dalen. Arguments for the continuity principle. Bulletin of Symbolic Logic, 8(3):329-347, 2002. URL: http://www.math.ucla.edu/~asl/bsl/0803/0803-001.ps, URL: https://doi.org/10.2178/bsl/1182353892.
  32. 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.
  33. Chuangjie Xu. A continuous computational interpretation of type theories. PhD thesis, University of Birmingham, UK, 2015. URL: http://etheses.bham.ac.uk/5967/.
  34. Chuangjie Xu and Martín Hötzel Escardó. A constructive model of uniform continuity. In TLCA 2013, 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