Hostname: page-component-586b7cd67f-2brh9 Total loading time: 0 Render date: 2024-11-20T07:31:33.353Z Has data issue: false hasContentIssue false
  • English
  • Français

Monadic translation of classical sequent calculus

Published online by Cambridge University Press:  18 January 2013

JOSÉ ESPÍRITO SANTO ,
RALPH MATTHES ,
KOJI NAKAZAWA  and
LUÍS PINTO
JOSÉ ESPÍRITO SANTO
Affiliation:
Centro de Matemática, Universidade do Minho, Portugal Email: [email protected], [email protected]
RALPH MATTHES
Affiliation:
I.R.I.T. (C.N.R.S. and University of Toulouse), France Email: [email protected]
KOJI NAKAZAWA
Affiliation:
Graduate School of Informatics, Kyoto University, Japan Email: [email protected]
LUÍS PINTO
Affiliation:
Centro de Matemática, Universidade do Minho, Portugal Email: [email protected], [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

We study monadic translations of the call-by-name (cbn) and call-by-value (cbv) fragments of the classical sequent calculus ${\overline{\lambda}\mu\tilde{\mu}}$ due to Curien and Herbelin, and give modular and syntactic proofs of strong normalisation. The target of the translations is a new meta-language for classical logic, named monadic λμ. This language is a monadic reworking of Parigot's λμ-calculus, where the monadic binding is confined to commands, thus integrating the monad with the classical features. Also, its μ-reduction rule is replaced by a rule expressing the interaction between monadic binding and μ-abstraction.

Our monadic translations produce very tight simulations of the respective fragments of ${\overline{\lambda}\mu\tilde{\mu}}$ within monadic λμ, with reduction steps of ${\overline{\lambda}\mu\tilde{\mu}}$ being translated in a 1–1 fashion, except for β steps, which require two steps. The monad of monadic λμ can be instantiated to the continuations monad so as to ensure strict simulation of monadic λμ within simply typed λ-calculus with β- and η-reduction. Through strict simulation, the strong normalisation of simply typed λ-calculus is inherited by monadic λμ, and then by cbn and cbv ${\overline{\lambda}\mu\tilde{\mu}}$, thus reproving strong normalisation in an elementary syntactical way for these fragments of ${\overline{\lambda}\mu\tilde{\mu}}$, and establishing it for our new calculus. These results extend to second-order logic, with polymorphic λ-calculus as the target, giving new strong normalisation results for classical second-order logic in sequent calculus style.

CPS translations of cbn and cbv ${\overline{\lambda}\mu\tilde{\mu}}$ with the strict simulation property are obtained by composing our monadic translations with the continuations-monad instantiation. In an appendix to the paper, we investigate several refinements of the continuations-monad instantiation in order to obtain in a modular way improvements of the CPS translations enjoying extra properties like simulation by cbv β-reduction or reduction of administrative redexes at compile time.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 23 , Issue 6 , December 2013 , pp. 1111 - 1162
Copyright
Copyright © Cambridge University Press 2013 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Asada, K. (2008) Extensional universal types for call-by-value. In: Ramalingam, G. (ed.) The 6th Asian Symposium on Programming Languages and Systems (APLAS 2008). Springer-Verlag Lecture Notes in Computer Science 5356 122–137.CrossRefGoogle Scholar
Barthe, G., Hatcliff, J. and Sørensen, M. H. (2001) Weak normalization implies strong normalization in a class of non-dependent pure type systems. Theoretical Computer Science 269 (1–2)317–361.CrossRefGoogle Scholar
Barthe, G. and Sørensen, M. H. (2000) Domain-free pure type systems. Journal of Functional Programming 10 (5)417–452.CrossRefGoogle Scholar
Curien, P.-L. and Herbelin, H. (2000) The duality of computation. In: Proceedings of ICFP 2000, IEEE 233–243. (Errata available from the second author's homepage.)CrossRefGoogle Scholar
Curien, P.-L. and Munch-Maccagnoni, G. (2010) The duality of computation under focus. In: Calude, C. S. and Sassone, V. (eds.) Theoretical Computer Science: Proceedings TCS 2010. IFIP Advances in Information and Communication Technology 323, Springer-Verlag 165–181.CrossRefGoogle Scholar
Danvy, O. and Filinski, A. (1992) Representing control: a study of the CPS transformation. Mathematical Structures in Computer Science 2 (4)361–391.CrossRefGoogle Scholar
David, R. and Nour, K. (2007) Arithmetical proofs of strong normalization results for symmetric λ-calculi. Fundamenta Informaticae 77 (4)489–510.Google Scholar
Dyckhoff, R. and Lengrand, S. (2007) Call-by-value λ-calculus and LJQ. Journal of Logic and Computation 17 (6)1109–1134.CrossRefGoogle Scholar
Espírito Santo, J., Matthes, R. and Pinto, L. (2007) Continuation-passing style and strong normalisation for intuitionistic sequent calculi. In: Ronchi Della Rocca, S. (ed.) Proceedings of TLCA 2007. Springer-Verlag Lecture Notes in Computer Science 4583 133–147.CrossRefGoogle Scholar
Espírito Santo, J., Matthes, R. and Pinto, L. (2009a) Continuation-passing style and strong normalisation for intuitionistic sequent calculi. Logical Methods in Computer Science 5 (2:11).Google Scholar
Espírito Santo, J., Matthes, R. and Pinto, L. (2009b) Monadic translation of intuitionistic sequent calculus. In: Berardi, S., Damiani, F. and de'Liguoro, U. (eds.) Post-Proceedings of TYPES 2008. Springer-Verlag Lecture Notes in Computer Science 5497 100–116.CrossRefGoogle Scholar
Fujita, K. (1999) Explicitly typed λμ-calculus for polymorphism and call-by-value. In: Girard, J.-Y. (ed.) Proceedings of TLCA 1999. Springer-Verlag Lecture Notes in Computer Science 1581 162–177.CrossRefGoogle Scholar
Geuvers, H. (1993) Logics and Type Systems, Proefschrift (Ph.D. thesis), University of Nijmegen.Google Scholar
Girard, J.-Y. (1971) Une extension de l'interprétation de Gödel à l'analyse, et son application à l'élimination des coupures dans l'analyse et la théorie des types. In: Fenstad, J. E. (ed.) Proceedings of the Second Scandinavian Logic Symposium, Studies in Logic and the Foundations of Mathematics 63, North-Holland 63–92.CrossRefGoogle Scholar
Harper, R. and Lillibridge, M. (1993) Polymorphic type assignment and CPS conversion. Lisp and Symbolic Computation 6 (3–4)361–380.CrossRefGoogle Scholar
Hatcliff, J. and Danvy, O. (1994) A generic account of continuation-passing styles. In: Proceedings of POPL 1994, ACM 458–471.Google Scholar
Herbelin, H. (2005) C'est maintenant qu'on calcule – au cœur de la dualité, Habilitation thesis, University Paris 11.Google Scholar
Hofmann, M. and Streicher, T. (2002) Completeness of continuation models for lambda-mu-calculus. Information and Computation 179 (2)332–355.CrossRefGoogle Scholar
Ikeda, S. and Nakazawa, K. (2006) Strong normalization proofs by CPS-translations. Information Processing Letters 99 163–170.CrossRefGoogle Scholar
Lengrand, S. (2003) Call-by-value, call-by-name, and strong normalization for the classical sequent calculus. In: Gramlich, B. and Lucas, S. (eds.) Post-Proceedings of WRS 2003. Electronic Notes in Theoretical Computer Science 86. (Erratum available from the author's homepage.)CrossRefGoogle Scholar
Matthes, R. (1999) Monotone fixed-point types and strong normalization. In: Gottlob, G., Grandjean, E. and Seyr, K. (eds.) Proceedings CSL, 12th International Workshop. Springer-Verlag Lecture Notes in Computer Science 1584 298–312.CrossRefGoogle Scholar
Moggi, E. (1991) Notions of computation and monads. Information and Computation 93 (1)55–92.CrossRefGoogle Scholar
Nakazawa, K. and Tatsuta, M. (2003) Strong normalization proof with CPS-translation for second order classical natural deduction. Journal of Symbolic Logic 68 (3)851–859. (Corrigendum in Journal of Symbolic Logic 68 (4) 1415–1416.)CrossRefGoogle Scholar
Parigot, M. (1992) λμ-calculus: an algorithmic interpretation of classic natural deduction. In: Voronkov, A. (ed.) Logic Programming and Automated Reasoning: Proceedings International Conference LPAR'92. Springer-Verlag Lecture Notes in Computer Science 624 190–201.CrossRefGoogle Scholar
Parigot, M. (1997) Proofs of strong normalisation for second order classical natural deduction. Journal of Symbolic Logic 62 (4)1461–1479.CrossRefGoogle Scholar
Plotkin, G. (1975) Call-by-name, call-by-value and the λ-calculus. Theoretical Computer Science 1 125–159.CrossRefGoogle Scholar
Polonovski, E. (2004) Strong normalization of ${\overline{\lambda}\mu\tilde{\mu}}$ with explicit substitutions. In: Walukiewicz, I. (ed.) Proceedings of FoSSaCS 2004. Springer-Verlag Lecture Notes in Computer Science 2987 423–437.CrossRefGoogle Scholar
Rocheteau, J. (2005) λμ-calculus and duality: call-by-name and call-by-value. In: Giesl, J. (ed.) Term Rewriting and Applications: Proceedings of RTA 2005. Springer-Verlag Lecture Notes in Computer Science 3467 204–218.CrossRefGoogle Scholar
Sabry, A. and Wadler, P. (1997) A reflection on call-by-value. ACM Transactions on Programming Languages and Systems 19 (6)916–941.CrossRefGoogle Scholar
Summers, A. J. (2011) Soundness and principal contexts for a shallow polymorphic type system based on classical logic. Logic Journal of the IGPL 19 (6)848–896.CrossRefGoogle Scholar
Urban, C. (2000) Classical Logic and Computation, Ph.D. thesis, University of Cambridge.Google Scholar