×

zbMATH — the first resource for mathematics

Monadic translation of classical sequent calculus. (English) Zbl 1311.68042
Summary: 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 \({\lambda}{\mu}\). This language is a monadic reworking of Parigot’s \({\lambda}{\mu}\)-calculus, where the monadic binding is confined to commands, thus integrating the monad with the classical features. Also, its \({\mu}\)-reduction rule is replaced by a rule expressing the interaction between monadic binding and \({\mu}\)-abstraction.
Our monadic translations produce very tight simulations of the respective fragments of \(\overline{\lambda}\mu\tilde\mu\) within monadic \({\lambda}{\mu}\), with reduction steps of \(\overline{\lambda}\mu\tilde\mu\) being translated in a \(1-1\) fashion, except for \({\beta}\) steps, which require two steps. The monad of monadic \({\lambda}{\mu}\) can be instantiated to the continuations monad so as to ensure strict simulation of monadic \({\lambda}{\mu}\) within simply typed \({\lambda}\)-calculus with \({\beta}\)- and \({\eta}\)-reduction. Through strict simulation, the strong normalisation of simply typed \({\lambda}\)-calculus is inherited by monadic \({\lambda}{\mu}\), 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 \({\lambda}\)-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 \({\beta}\)-reduction or reduction of administrative redexes at compile time.
MSC:
68N18 Functional programming and lambda calculus
03B40 Combinatory logic and lambda calculus
03F05 Cut-elimination and normal-form theorems
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] DOI: 10.1093/jigpal/jzq013 · Zbl 1259.03046 · doi:10.1093/jigpal/jzq013
[2] Electronic Notes in Theoretical Computer Science 86 (2003)
[3] DOI: 10.1006/inco.2001.2947 · Zbl 1096.03011 · doi:10.1006/inco.2001.2947
[4] Proceedings of POPL 1994 pp 458– (1994)
[5] DOI: 10.1007/BF01019463 · doi:10.1007/BF01019463
[6] DOI: 10.1007/978-3-540-73228-0_11 · Zbl 1167.03012 · doi:10.1007/978-3-540-73228-0_11
[7] DOI: 10.1016/S0049-237X(08)70843-7 · doi:10.1016/S0049-237X(08)70843-7
[8] DOI: 10.1093/logcom/exm037 · Zbl 1133.03030 · doi:10.1093/logcom/exm037
[9] Fundamenta Informaticae 77 pp 489– (2007)
[10] DOI: 10.1007/3-540-48959-2_13 · doi:10.1007/3-540-48959-2_13
[11] DOI: 10.1017/S0960129500001535 · doi:10.1017/S0960129500001535
[12] DOI: 10.1007/978-3-642-02444-3_7 · Zbl 1246.03027 · doi:10.1007/978-3-642-02444-3_7
[13] Theoretical Computer Science: Proceedings TCS 2010. IFIP Advances in Information and Communication Technology 323 pp 165– (2010) · Zbl 1202.68091 · doi:10.1007/978-3-642-15240-5_13
[14] Logical Methods in Computer Science 5 (2009)
[15] DOI: 10.1017/S0956796800003750 · Zbl 0979.03013 · doi:10.1017/S0956796800003750
[16] DOI: 10.1016/S0304-3975(01)00012-3 · Zbl 0983.68029 · doi:10.1016/S0304-3975(01)00012-3
[17] DOI: 10.1007/978-3-540-89330-1_9 · Zbl 05488149 · doi:10.1007/978-3-540-89330-1_9
[18] DOI: 10.1145/267959.269968 · doi:10.1145/267959.269968
[19] DOI: 10.1007/978-3-540-32033-3_16 · doi:10.1007/978-3-540-32033-3_16
[20] DOI: 10.1007/978-3-540-24727-2_30 · doi:10.1007/978-3-540-24727-2_30
[21] DOI: 10.1016/0304-3975(75)90017-1 · Zbl 0325.68006 · doi:10.1016/0304-3975(75)90017-1
[22] DOI: 10.2307/2275652 · Zbl 0941.03063 · doi:10.2307/2275652
[23] DOI: 10.1007/BFb0013061 · doi:10.1007/BFb0013061
[24] DOI: 10.2178/jsl/1058448444 · Zbl 1058.03060 · doi:10.2178/jsl/1058448444
[25] DOI: 10.1016/0890-5401(91)90052-4 · Zbl 0723.68073 · doi:10.1016/0890-5401(91)90052-4
[26] DOI: 10.1007/10703163_20 · doi:10.1007/10703163_20
[27] DOI: 10.1016/j.ipl.2006.03.009 · Zbl 1185.68625 · doi:10.1016/j.ipl.2006.03.009
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.