Document Open Access Logo

Internal Effectful Forcing in System T

Authors Martín H. Escardó , Bruno da Rocha Paiva , Vincent Rahli , Ayberk Tosun

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2025.19.pdf
  • Filesize: 1.21 MB
  • 17 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Constructive mathematics
  • Theory of computation → Type theory
Keywords
  • Effectful forcing
  • Continuity
  • System T
  • Constructive Mathematics

Metrics

Abstract

The effectful forcing technique allows one to show that the denotation of a closed System T term of type (ι ⇒ ι) ⇒ ι in the set-theoretical model is a continuous function (ℕ → ℕ) → ℕ. For this purpose, an alternative dialogue-tree semantics is defined and related to the set-theoretical semantics by a logical relation. In this paper, we apply effectful forcing to show that the dialogue tree of a System T term is itself System T-definable, using the Church encoding of trees.

Cite As Get BibTex

Martín H. Escardó, Bruno da Rocha Paiva, Vincent Rahli, and Ayberk Tosun. Internal Effectful Forcing in System T. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 19:1-19:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.FSCD.2025.19

Author Details

Martín H. Escardó
  • University of Birmingham, UK
Bruno da Rocha Paiva
  • University of Birmingham, UK
Vincent Rahli
  • University of Birmingham, UK
Ayberk Tosun
  • University of Birmingham, UK

References

  1. Jeremy Avigad and Solomon Feferman. Gödel’s functional ("dialectica") interpretation. In Handbook of Proof Theory, volume 137 of Studies in Logic and the Foundations of Mathematics, pages 337-405. Elsevier, 1998. URL: https://doi.org/10.1016/S0049-237X(98)80020-7.
  2. Martin Baillon. Continuity in Type Theory. (Continuité en théorie des types). PhD thesis, University of Nantes, France, 2023. URL: https://tel.archives-ouvertes.fr/tel-04617881.
  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. 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.
  5. Liron Cohen, Bruno da Rocha Paiva, Vincent Rahli, and Ayberk Tosun. Inductive continuity via brouwer trees. In Jérôme Leroux, Sylvain Lombardy, and David Peleg, editors, 48th International Symposium on Mathematical Foundations of Computer Science, MFCS 2023, August 28 to September 1, 2023, Bordeaux, France, 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.
  6. 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.
  7. 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.
  8. Michael A. E. Dummett. Elements of Intuitionism. Clarendon Press, second edition, 2000. Google Scholar
  9. Martín Escardó, Bruno da Rocha Paiva, Vincent Rahli, and Ayberk Tosun. Internal effectful forcing in Agda. Source code: https://github.com/martinescardo/TypeTopology/blob/master/source/EffectfulForcing/Internal/PaperIndex.lagda, and HTML rendering: URL: https://cs.bham.ac.uk/~mhe/InternalEffectfulForcing/EffectfulForcing.Internal.index.html.
  10. Martín H. Escardó and Paulo Oliva. Dialogue to Brouwer, 2017. URL: https://www.cs.bham.ac.uk/~mhe/TypeTopology/EffectfulForcing.MFPSAndVariations.Dialogue-to-Brouwer.html.
  11. Martín H. Escardó and Chuangjie Xu. The inconsistency of a Brouwerian continuity principle with the Curry-Howard interpretation. In TLCA, pages 153-164, 2015. URL: https://doi.org/10.4230/LIPIcs.TLCA.2015.153.
  12. Martín H. Escardó. Continuity of Gödel’s System T definable functionals via effectful forcing. In MFPS, volume 298, pages 119-141. Elsevier B.V, 2013. URL: https://doi.org/10.1016/j.entcs.2013.09.010.
  13. Neil Ghani, Peter G. Hancock, and Dirk Pattinson. Continuous functions on final coalgebras. In Neil Ghani and John Power, editors, CMCS, volume 164 of Electronic Notes in Theoretical Computer Science, pages 141-155. Elsevier, 2006. URL: https://doi.org/10.1016/j.entcs.2006.06.009.
  14. 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 Electronic Notes in Theoretical Computer Science, pages 3-18. Elsevier, 2009. URL: https://doi.org/10.1016/j.entcs.2009.07.081.
  15. 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.
  16. Tatsuji Kawai. Representing definable functions of HA^ω by neighbourhood functions. Annals of Pure and Applied Logic, 170(8):891-909, 2019. URL: https://doi.org/10.1016/j.apal.2019.04.011.
  17. S.C. Kleene. Recursive functionals and quantifiers of finite types revisited i. In J.E. Fenstad, R.O. Gandy, and G.E. Sacks, editors, 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.
  18. Georg Kreisel. On weak completeness of intuitionistic predicate logic. J. Symb. Log., 27(2):139-158, 1962. URL: https://doi.org/10.2307/2964110.
  19. John Longley. When is a functional program not a functional program? In ICFP, pages 1-7, 1999. URL: https://doi.org/10.1145/317636.317775.
  20. Pierre-Marie Pédrot and Nicolas Tabareau. An effectful way to eliminate addiction to dependence. In LICS, pages 1-12, 2017. URL: https://doi.org/10.1109/LICS.2017.8005113.
  21. Vincent Rahli and Mark Bickford. A nominal exploration of intuitionism. In CPP, pages 130-141, 2016. Extended version: http://www.nuprl.org/html/Nuprl2Coq/continuity-long.pdf. URL: https://doi.org/10.1145/2854065.2854077.
  22. Jonathan Sterling. Higher order functions and Brouwer’s thesis. J. Funct. Program., 31:e11, 2021. URL: https://doi.org/10.1017/S0956796821000095.
  23. 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
  24. A.S. Troelstra. Metamathematical Investigation of Intuitionistic Arithmetic and Analysis. New York, Springer, 1973. Google Scholar
  25. 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.
  26. Chuangjie Xu. A continuous computational interpretation of type theories. PhD thesis, University of Birmingham, UK, 2015. URL: http://etheses.bham.ac.uk/5967/.
  27. Chuangjie Xu. A Gentzen-Style Monadic Translation of Gödel’s System T. In Zena M. Ariola, editor, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020), volume 167 of Leibniz International Proceedings in Informatics (LIPIcs), pages 25:1-25:17, Dagstuhl, Germany, 2020. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.FSCD.2020.25.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact