Document Open Access Logo

A Linear-Logical Reconstruction of Intuitionistic Modal Logic S4

Authors Yosuke Fukuda, Akira Yoshimizu

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2019.20.pdf
  • Filesize: 1.16 MB
  • 24 pages

Document Identifiers

Author Details

Yosuke Fukuda
  • Graduate School of Informatics, Kyoto University, Japan
Akira Yoshimizu
  • French Institute for Research in Computer Science and Automation (INRIA), France

Acknowledgements

The authors thank Kazushige Terui for his helpful comments on our work and pointing out related work on multicolored linear logic, and Atsushi Igarashi for his helpful comments on earlier drafts. Special thanks are also due to anonymous reviewers for their fruitful comments. This work was supported by the Research Institute for Mathematical Sciences, an International Joint Usage/Research Center located in Kyoto University.

Cite AsGet BibTex

Yosuke Fukuda and Akira Yoshimizu. A Linear-Logical Reconstruction of Intuitionistic Modal Logic S4. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 20:1-20:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.FSCD.2019.20

Abstract

We propose a modal linear logic to reformulate intuitionistic modal logic S4 (IS4) in terms of linear logic, establishing an S4-version of Girard translation from IS4 to it. While the Girard translation from intuitionistic logic to linear logic is well-known, its extension to modal logic is non-trivial since a naive combination of the S4 modality and the exponential modality causes an undesirable interaction between the two modalities. To solve the problem, we introduce an extension of intuitionistic multiplicative exponential linear logic with a modality combining the S4 modality and the exponential modality, and show that it admits a sound translation from IS4. Through the Curry-Howard correspondence we further obtain a Geometry of Interaction Machine semantics of the modal lambda-calculus by Pfenning and Davies for staged computation.

Subject Classification

ACM Subject Classification
  • Theory of computation → Linear logic
  • Theory of computation → Modal and temporal logics
  • Theory of computation → Proof theory
  • Theory of computation → Type theory
Keywords
  • linear logic
  • modal logic
  • Girard translation
  • Curry-Howard correspondence
  • geometry of interaction
  • staged computation

Metrics

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

References

  1. Samson Abramsky, Esfandiar Haghverdi, and Philip Scott. Geometry of Interaction and Linear Combinatory Algebras. Mathematical Structures in Computer Science, 12(5):625-665, 2002. URL: http://dx.doi.org/10.1017/S0960129502003730.
  2. Andrew Barber. Dual intuitionistic linear logic, 1996. Technical report LFCS-96-347. URL: http://www.lfcs.inf.ed.ac.uk/reports/96/ECS-LFCS-96-347.
  3. Cristiano Calcagno, Eugenio Moggi, and Walid Taha. ML-like inference for classifiers. In Proceedings of ESOP 2004, pages 79-93, 2004. URL: http://dx.doi.org/10.1007/978-3-540-24725-8_7.
  4. Vincent Danos, Jean-Baptiste Joinet, and Harold Schellinx. The Structure of Exponentials: Uncovering the Dynamics of Linear Logic Proofs. In G. Gottlob, A. Leitsch, and D. Mundici, editors, Computational Logic and Proof Theory, pages 159-171. Springer-Verlag, 1993. URL: http://dx.doi.org/10.1007/BFb0022564.
  5. Rowan Davies and Frank Pfenning. A Modal Analysis of Staged Computation. Journal of the ACM, 48(3):555-604, 2001. URL: http://dx.doi.org/10.1145/382780.382785.
  6. Yosuke Fukuda and Akira Yoshimizu. A Higher-arity Sequent Calculus for Modal Linear Logic. In RIMS Kôkyûroku 2083: Symposium on Proof Theory and Proving, pages 76-87, 2018. URL: http://www.kurims.kyoto-u.ac.jp/~kyodo/kokyuroku/contents/pdf/2083-07.pdf.
  7. Jean-Yves Girard. Linear Logic. Theoretical Compututer Science, 50(1):1-102, 1987. URL: http://dx.doi.org/10.1016/0304-3975(87)90045-4.
  8. G. A. Kavvos. Dual-Context Calculi for Modal Logic. In Proceedings of LICS 2017, pages 1-12, 2017. URL: http://dx.doi.org/10.1109/LICS.2017.8005089.
  9. Patrick Lincoln, John Mitchell, Andre Scedrov, and Natarajan Shankar. Decision problems for propositional linear logic. Annals of Pure and Applied Logic, 56(1):239-311, 1992. URL: http://dx.doi.org/10.1016/0168-0072(92)90075-B.
  10. Ian Mackie. The Geometry of Implementation. PhD thesis, University of London, 1994. Google Scholar
  11. Ian Mackie. The Geometry of Interaction Machine. In Proceedings of POPL 1995, pages 198-208, 1995. URL: http://dx.doi.org/10.1145/199448.199483.
  12. John Maraist, Martin Odersky, David N. Turner, and Philip Wadler. Call-by-name, call-by-value, call-by-need and the linear lambda lalculus. Theoretical Computer Science, 228(1-2):175-210, 1999. URL: http://dx.doi.org/10.1016/S0304-3975(98)00358-2.
  13. Simone Martini and Andrea Masini. A Modal View of Linear Logic. Journal of Symbolic Logic, 59(3):888-899, 1994. URL: http://dx.doi.org/10.2307/2275915.
  14. Vivek Nigam and Dale Miller. Algorithmic Specifications in Linear Logic with Subexponentials. In Proceedings of PPDP 2009, pages 129-140, 2009. URL: http://dx.doi.org/10.1145/1599410.1599427.
  15. Vivek Nigam, Elaine Pimentel, and Giselle Reis. An extended framework for specifying and reasoning about proof systems. Journal of Logic and Computation, 26(2):539-576, 2016. URL: http://dx.doi.org/10.1093/logcom/exu029.
  16. Yo Ohta and Masahito Hasegawa. A Terminating and Confluent Linear Lambda Calculus. In Proceedings of RTA 2006, pages 166-180, 2006. URL: http://dx.doi.org/10.1007/11805618_13.
  17. Frank Pfenning. Lecture Notes on Combinatory Modal Logic, 2010. Lecture note. URL: http://www.cs.cmu.edu/~fp/courses/15816-s10/lectures/09-combinators.pdf.
  18. Frank Pfenning and Rowan Davies. A judgmental reconstruction of modal logic. Mathematical Structures in Computer Science, 11(4):511-540, 2001. URL: http://dx.doi.org/10.1017/S0960129501003322.
  19. Klaas Pruiksma, William Chargin, Frank Pfenning, and Jason Reed. Adjoint Logic, 2018. Manuscript. URL: http://www.cs.cmu.edu/~fp/papers/adjoint18b.pdf.
  20. Harold Schellinx. A Linear Approach to Modal Proof Theory. In Proof Theory of Modal Logic, pages 33-43. Springer, 1996. URL: http://dx.doi.org/10.1007/978-94-017-2798-3_3.
  21. Walid Taha and Michael Florentin Nielsen. Environment Classifiers. In Proceedings of POPL 2003, pages 26-37, 2003. URL: http://dx.doi.org/10.1145/640128.604134.
  22. Walid Taha and Tim Sheard. MetaML and multi-stage programming with explicit annotations. Theoretical Computer Science, 248(1-2):211-242, 2000. URL: http://dx.doi.org/10.1016/S0304-3975(00)00053-0.
  23. A. S. Troelstra and H. Schwichtenberg. Basic Proof Theory. Cambridge University Press, 1996. Google Scholar
  24. Takeshi Tsukada and Atsushi Igarashi. A Logical Foundation for Environment Classifiers. Logical Methods in Computer Science, 6(4:8):1-43, 2010. URL: http://dx.doi.org/10.2168/LMCS-6(4:8)2010.
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