Document Open Access Logo

Realising Intensional S4 and GL Modalities

Authors Liang-Ting Chen , Hsiang-Shang Ko

PDF
Thumbnail PDF

File

LIPIcs.CSL.2022.14.pdf
  • Filesize: 0.85 MB
  • 17 pages

Document Identifiers

Author Details

Liang-Ting Chen
  • Institute of Information Science, Academia Sinica, Taipei, Taiwan
Hsiang-Shang Ko
  • Institute of Information Science, Academia Sinica, Taipei, Taiwan

Funding

This work was partially supported by EPSRC grant number EP/N028139/1 and supported by the Ministry of Science and Technology of Taiwan under grant MOST 109-2222-E-001-002-MY3.

Acknowledgements

We are grateful to Alex Kavvos and Tsung-Ju Chiang for insightful discussions. We would also like to thank Jacques Carette, Martín Escardó, Tom de Jong, Churn-Jung Liau, Rasmus Ejlers Møgelberg, Chad Nester, Anton Setzer, Andrea Vezzosi, Ren-June Wang, and Zhixuan Yang for useful exchanges. Finally, we thank the anonymous reviewers for their thoughtful comments.

Cite AsGet BibTex

Liang-Ting Chen and Hsiang-Shang Ko. Realising Intensional S4 and GL Modalities. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 14:1-14:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.CSL.2022.14

Abstract

There have been investigations into type-theoretic foundations for metaprogramming, notably Davies and Pfenning’s (2001) treatment in S4 modal logic, where code evaluating to values of type A is given the modal type Code A (□A in the original paper). Recently Kavvos (2017) extended PCF with Code A and intensional recursion, understood as the deductive form of the GL (Gödel-Löb) axiom in provability logic, but the resulting type system is logically inconsistent. Inspired by staged computation, we observe that a term of type Code A is, in general, code to be evaluated in a next stage, whereas S4 modal type theory is a special case where code can be evaluated in the current stage, and the two types of code should be discriminated. Consequently, we use two separate modalities ⊠ and □ to model S4 and GL respectively in a unified categorical framework while retaining logical consistency. Following Kavvos’ (2017) novel approach to the semantics of intensionality, we interpret the two modalities in the P-category of assemblies and trackable maps. For the GL modality □ in particular, we use guarded type theory to articulate what it means by a “next” stage and to model intensional recursion by guarded recursion together with Kleene’s second recursion theorem. Besides validating the S4 and GL axioms, our model better captures the essence of intensionality by refuting congruence (so that two extensionally equal terms may not be intensionally equal) and internal quoting (both A → □A and A → ⊠A). Our results are developed in (guarded) homotopy type theory and formalised in Agda.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
Keywords
  • provability
  • guarded recursion
  • realisability
  • modal types
  • metaprogramming

Metrics

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

Supplementary Materials

References

  1. Sergei N. Artemov. Explicit provability and constructive semantics. Bulletin of Symbolic Logic, 7(1):1-36, 2001. URL: https://doi.org/10.2307/2687821.
  2. Sergei N. Artemov and Lev D. Beklemishev. Provability logic. In D.M. Gabbay and F. Guenthner, editors, Handbook of Philosophical Logic, 2nd Edition, volume 13 of Handbook of Philosophical Logic, pages 189-360. Springer, Dordrecht, 2005. URL: https://doi.org/10.1007/1-4020-3521-7_3.
  3. Robert Atkey and Conor McBride. Productive coprogramming with guarded recursion. In Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming (ICFP), page 197, New York, New York, USA, 2013. ACM Press. URL: https://doi.org/10.1145/2500365.2500597.
  4. Henk Barendregt. The Lambda Calculus: Its Syntax and Semantics, volume 103 of Studies in Logic. North Holland, 1984. Google Scholar
  5. George S. Boolos. The Logic of Provability. Cambridge University Press, 1994. URL: https://doi.org/10.1017/cbo9780511625183.
  6. J.R.B. Cockett and Pieter J.W. Hofstra. Categorical simulations. Journal of Pure and Applied Algebra, 214(10):1835-1853, 2010. URL: https://doi.org/10.1016/j.jpaa.2009.12.028.
  7. Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. Cubical type theory: A constructive interpretation of the univalence axiom. In Tarmo Uustalu, editor, 21st International Conference on Types for Proofs and Programs (TYPES), volume 69 of Leibniz International Proceedings in Informatics (LIPIcs), pages 5:1-34, Dagstuhl, Germany, 2015. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.TYPES.2015.5.
  8. Djordje Čubrić, Peter Dybjer, and Philip J. Scott. Normalization and the Yoneda embedding. Mathematical Structures in Computer Science, 8(2):153-192, 1998. URL: https://doi.org/10.1017/S0960129597002508.
  9. Rowan Davies. A temporal logic approach to binding-time analysis. Journal of the ACM, 64(1):1-45, 2017. URL: https://doi.org/10.1145/3011069.
  10. Rowan Davies and Frank Pfenning. A modal analysis of staged computation. Journal of the ACM, 48(3):555-604, 2001. URL: https://doi.org/10.1145/382780.382785.
  11. Agda development team. Agda 2.6.2 documentation. Accessed: 2021-06-20. URL: https://agda.readthedocs.io/en/v2.6.2/.
  12. Murdoch J. Gabbay and Aleksandar Nanevski. Denotation of contextual modal type theory (CMTT): Syntax and meta-programming. Journal of Applied Logic, 11(1):1-29, 2013. URL: https://doi.org/10.1016/j.jal.2012.07.002.
  13. Evan Goris. A modal provability logic of explicit and implicit proofs. Annals of Pure and Applied Logic, 161(3):388-403, 2009. URL: https://doi.org/10.1016/j.apal.2009.07.020.
  14. Pieter Hofstra and Jaap van Oosten. Ordered partial combinatory algebras. Mathematical Proceedings of the Cambridge Philosophical Society, 134(3):445-463, 2003. URL: https://doi.org/10.1017/S0305004102006424.
  15. G. A. Kavvos. On the semantics of intensionality. In Javier Esparza and Andrzej S. Murawski, editors, Proceedings of the 20th International Conference the Foundations of Software Science and Computation Structures (FoSSaCS), volume 10203 of Lecture Notes in Computer Science, pages 550-566. Springer, Berlin, Heidelberg, 2017. URL: https://doi.org/10.1007/978-3-662-54458-7_32.
  16. G. A. Kavvos. Intensionality, intensional recursion, and the Gödel-Löb axiom. Journal of Applied Logics - The IfCoLog Journal of Logics and their Applications, 8(8):2287-2311, 2021. Special Issue: Intuitionistic Modal Logic and Applications. URL: http://collegepublications.co.uk/ifcolog/?00050.
  17. Oleg Kiselyov. The design and implementation of BER MetaOCaml. In Michael Codish and Eijiro Sumii, editors, Proceedings of the 12th International Symposium on Functional and Logic Programming (FLOPS), volume 8475 of Lecture Notes in Computer Science, pages 86-102. Springer, Cham, 2014. URL: https://doi.org/10.1007/978-3-319-07151-0_6.
  18. Magnus Baunsgaard Kristensen, Rasmus Ejlers Møgelberg, and Andrea Vezzosi. Greatest HITs: Higher inductive types in coinductives via induction under clocks. ArXiv preprint, 2021. URL: http://arxiv.org/abs/2102.01969.
  19. Jean-Louis Krivine. A program for the full axiom of choice. Logical Methods in Computer Science, 17(3):21:1-22, 2021. URL: https://doi.org/10.46298/lmcs-17(3:21)2021.
  20. Rasmus Ejlers Møgelberg and Niccolò Veltri. Bisimulation as path type for guarded recursive types. Proceedings of the ACM on Programming Languages, 3(POPL):4:1-29, 2019. URL: https://doi.org/10.1145/3290317.
  21. Hiroshi Nakano. A modality for recursion. In Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science (LICS). IEEE Computer Society, 2000. URL: https://doi.org/10.1109/LICS.2000.855774.
  22. Aleksandar Nanevski, Frank Pfenning, and Brigitte Pientka. Contextual modal type theory. ACM Transactions on Computational Logic, 9(3):1-49, 2008. URL: https://doi.org/10.1145/1352582.1352591.
  23. Frank Pfenning. Intensionality, extensionality, and proof irrelevance in modal type theory. In Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science (LICS), pages 221-230. IEEE Computer Society, 2002. URL: https://doi.org/10.1109/LICS.2001.932499.
  24. Andrew Polonsky. Axiomatizing the quote. In Marc Bezem, editor, Computer Science Logic (CSL) - 25th International Workshop/20th Annual Conference of the EACSL, volume 12 of Leibniz International Proceedings in Informatics (LIPIcs), pages 458-469, Dagstuhl, Germany, 2011. Schloss Dagstuhl-Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CSL.2011.458.
  25. Daniyar S. Shamkanov. Circular proofs for the Gödel-Löb provability logic. Mathematical Notes, 96(3-4):575-585, 2014. URL: https://doi.org/10.1134/S0001434614090326.
  26. Daniyar S. Shamkanov. A realization theorem for the Gödel-Löb provability logic. Sbornik: Mathematics, 207(9):1344-1360, 2016. URL: https://doi.org/10.1070/SM8667.
  27. Tim Sheard and Simon Peyton Jones. Template meta-programming for Haskell. In Proceedings of the 2002 ACM SIGPLAN Workshop on Haskell, pages 1-16, New York, New York, USA, 2002. ACM Press. URL: https://doi.org/10.1145/581690.581691.
  28. Walid Taha and Tim Sheard. MetaML and multi-stage programming with explicit annotations. Theoretical Computer Science, 248(1-2):211-242, 2000. URL: https://doi.org/10.1016/S0304-3975(00)00053-0.
  29. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
  30. Jaap van Oosten. Realizability: An Introduction to its Categorical Side. Studies in Logic and the Foundations of Mathematics. Elsevier, 2008. URL: https://doi.org/10.1016/S0049-237X(08)80001-8.
  31. Niccolò Veltri and Andrea Vezzosi. Formalizing π-calculus in guarded cubical Agda. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP), pages 270-283, New York, NY, USA, 2020. ACM. URL: https://doi.org/10.1145/3372885.3373814.
  32. Andrea Vezzosi, Anders Mörtberg, and Andreas Abel. Cubical Agda: A dependently typed programming language with univalence and higher inductive types. Journal of Functional Programming, 31:e8:1-47, 2021. URL: https://doi.org/10.1017/s0956796821000034.
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