Document Open Access Logo

A Gentzen-Style Monadic Translation of Gödel’s System T

Author Chuangjie Xu

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2020.25.pdf
  • Filesize: 0.49 MB
  • 17 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Program analysis
  • Theory of computation → Type theory
  • Theory of computation → Proof theory
Keywords
  • monadic translation
  • Gödel’s System T
  • logical relation
  • negative translation
  • majorizability
  • continuity
  • bar recursion
  • Agda

Metrics

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

Abstract

We introduce a syntactic translation of Gödel’s System 𝖳 parametrized by a weak notion of a monad, and prove a corresponding fundamental theorem of logical relation. Our translation structurally corresponds to Gentzen’s negative translation of classical logic. By instantiating the monad and the logical relation, we reveal the well-known properties and structures of 𝖳-definable functionals including majorizability, continuity and bar recursion. Our development has been formalized in the Agda proof assistant.

Cite As Get BibTex

Chuangjie Xu. A Gentzen-Style Monadic Translation of Gödel’s System T. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 25:1-25:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020) https://doi.org/10.4230/LIPIcs.FSCD.2020.25

Author Details

Chuangjie Xu
  • Ludwig-Maximilians-Universität München, Germany

Funding

  • Xu, Chuangjie: Alexander von Humboldt Foundation and LMUexcellent initiative.

Acknowledgements

The author is grateful to Martín Escardó, Hajime Ishihara, Nils Köpp, Paulo Oliva, Thomas Powell, Benno van den Berg, Helmut Schwichtenberg for many fruitful discussions and the anonymous reviewers for their valuable suggestions and comments.

Supplementary Materials

References

  1. Peter Aczel. The Russell-Prawitz modality. Mathematical Structures in Computer Science, 11(4):541-554, 2001. URL: https://doi.org/10.1017/S0960129501003309.
  2. Agda community. The Agda Wiki. URL: https://wiki.portal.chalmers.se/agda/pmwiki.php.
  3. Rob Arthan and Paulo Oliva. On affine logic and łukasiewicz logic, 2014. https://arxiv.org/abs/1404.0570 [cs.LO]. URL: https://arxiv.org/abs/1404.0570.
  4. Gilles Barthe and Tarmo Uustalu. CPS translating inductive and coinductive types. In 2002 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation (PEPM'02), volume 37 of SIGPLAN Notices, pages 131-142. ACM Press, New York, 2002. URL: https://doi.org/10.1145/503032.503043.
  5. Michael J. Beeson. Foundations of Constructive Mathematics. Springer, 1985. URL: https://doi.org/10.1007/978-3-642-68952-9.
  6. Thierry Coquand and Guilhem Jaber. A note on forcing and type theory. Fundamenta Informaticae, 100(1-4):43-52, 2010. URL: https://doi.org/10.3233/FI-2010-262.
  7. Martín H. Escardó. Continuity of Gödel’s system T functionals via effectful forcing. In Proceedings of the Twenty-ninth Conference on the Mathematical Foundations of Programming Semantics (MFPS'2013), 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.
  8. Martín H. Escardó and Paulo Oliva. The Peirce translation. Annals of Pure and Applied Logic, 163(6):681-692, 2012. URL: https://doi.org/10.1016/j.apal.2011.11.002.
  9. Martín H. Escardó and Chuangjie Xu. A constructive manifestation of the Kleene-Kreisel continuous functionals. Annals of Pure and Applied Logic, 167(9):770-793, 2016. Fourth Workshop on Formal Topology (4WFTop). URL: https://doi.org/10.1016/j.apal.2016.04.011.
  10. Michael P. Fourman. Notions of choice sequence. In The L. E. J. Brouwer Centenary Symposium, volume 110 of Studies in Logic and the Foundations of Mathematics, pages 91-105. Elsevier, 1982. URL: https://doi.org/10.1016/S0049-237X(09)70125-9.
  11. William A. Howard. Hereditarily majorizable functionals of finite type. In Metamathematical investigation of intuitionistic Arithmetic and Analysis, volume 344 of Lecture Notes in Mathematics, pages 454-461. Springer, Berlin, Heidelberg, 1973. URL: https://doi.org/10.1007/BFb0066739.
  12. Hajime Ishihara. A note on the Gödel-Gentzen translation. Mathematical Logic Quarterly, 46(1):135-137, 2000. URL: https://doi.org/10.1002/(SICI)1521-3870(200001)46:1<135::AID-MALQ135>3.0.CO;2-R.
  13. Ulrich Kohlenbach. Pointwise hereditary majorization and some applications. Archive for Mathematical Logic, 31(4):227-241, 1992. URL: https://doi.org/10.1007/BF01794980.
  14. Ulrich Kohlenbach. Applied Proof Theory: Proof Interpretations and their Use in Mathematics. Springer Monographs in Mathematics. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-77533-1.
  15. Paulo Oliva. Unifying functional interpretations. Notre Dame Journal of Formal Logic, 47(2):263-290, 2006. URL: https://doi.org/10.1305/ndjfl/1153858651.
  16. Paulo Oliva and Gilda Ferreira. On the relation between various negative translations. In Logic, Construction, Computation, volume 3 of Mathematical Logic Series, pages 227-258. Ontos-Verlag, 2012. URL: https://doi.org/10.1515/9783110324921.
  17. Paulo Oliva and Silvia Steila. A direct proof of Schwichtenberg’s bar recursion closure theorem. The Journal of Symbolic Logic, 83(1):70-83, 2018. URL: https://doi.org/10.1017/jsl.2017.33.
  18. Thomas Powell. A functional interpretation with state. In Proceedings of the Thirty third Annual IEEE Symposium on Logic in Computer Science (LICS 2018), pages 839-848. IEEE Computer Society Press, July 2018. URL: https://doi.org/10.1145/3209108.3209134.
  19. Thomas Powell. A unifying framework for continuity and complexity in higher types, 2019. https://arxiv.org/abs/1906.10719 [cs.LO]. URL: https://arxiv.org/abs/1906.10719.
  20. Helmut Schwichtenberg. On bar recursion of types 0 and 1. The Journal of Symbolic Logic, 44(3):325-329, 1979. URL: https://doi.org/10.2307/2273126.
  21. Richard Statman. Logical relations and the typed lambda-calculus. Information and Control, 65(2/3):85-97, 1985. URL: https://doi.org/10.1016/S0019-9958(85)80001-2.
  22. Anne Sjerp Troelstra and Helmut Schwichtenberg. Basic Proof Theory, volume 43 of Cambridge tracts in theoretical computer science. Cambridge University Press, 2nd edition, 2000. Google Scholar
  23. Anne Sjerp Troelstra and Dirk van Dalen. Constructivism in mathematics, Vol. II, volume 123 of Studies in Logic and the Foundations of Mathematics. North-Holland Publishing Co., Amsterdam, 1988. Google Scholar
  24. Tarmo Uustalu. Monad translating inductive and coinductive types. In Types for Proofs and Programs (TYPES 2002), volume 2646 of Lecture Notes in Computer Science, pages 299-315. Springer, 2002. URL: https://doi.org/10.1007/3-540-39185-1_17.
  25. Benno van den Berg. A Kuroda-style j-translation. Archive for Mathematical Logic, 58(5-6):627-634, 2019. URL: https://doi.org/10.1007/s00153-018-0656-x.
  26. Gerrit van der Hoeven and Ieke Moerdijk. Sheaf models for choice sequences. Annals of Pure and Applied Logic, 27(1):63-107, 1984. URL: https://doi.org/10.1016/0168-0072(84)90035-6.
  27. Chuangjie Xu. A syntactic approach to continuity of T-definable functionals. Logical Methods in Computer Science, 16(1):22:1-22:11, 2020. URL: https://lmcs.episciences.org/6130.
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