Call-by-name reduction and cut-elimination in classical logic. (English) Zbl 1136.03036

Summary: We present a version of Herbelin’s \(\overline{\lambda}\mu\)-calculus in the call-by-name setting to study the precise correspondence between normalization and cut-elimination in classical logic. Our translation of \(\lambda \mu \)-terms into a set of terms in the calculus does not involve any administrative redexes, in particular \(\eta \)-expansion on \(\mu \)-abstraction. The isomorphism preserves \(\beta ,\mu \)-reduction, which is simulated by a local-step cut-elimination procedure in the typed case, where the reduction system strictly follows the “cut = redex” paradigm. We show that the underlying untyped calculus is confluent and enjoys the PSN (preservation of strong normalization) property for the isomorphic image of \(\lambda \mu \)-calculus, which in turn yields a confluent and strongly normalizing local-step cut-elimination procedure for classical logic.


03F05 Cut-elimination and normal-form theorems
03B05 Classical propositional logic
03B40 Combinatory logic and lambda calculus
03B70 Logic in computer science
Full Text: DOI


[1] Baader, F.; Nipkow, T., Term rewriting and all that, (1998), Cambridge University Press
[2] Bloo, R.; Geuvers, H., Explicit substitution: on the edge of strong normalization, Theoretical computer science, 211, 375-395, (1999) · Zbl 0913.68130
[3] Curien, P.-L.; Herbelin, H., The duality of computation, (), 233-243 · Zbl 1321.68146
[4] Danos, V.; Joinet, J.-B.; Schellinx, H., LKQ and LKT: sequent calculi for second order logic based upon dual linear decompositions of classical implication, (), 211-224 · Zbl 0829.03031
[5] Danos, V.; Joinet, J.-B.; Schellinx, H., A new deconstructive logic: linear logic, The journal of symbolic logic, 62, 755-807, (1997) · Zbl 0895.03023
[6] R. Dyckhoff, C. Urban, Strong normalisation of Herbelin’s explicit substitution calculus with substitution propagation, in: Proceedings of WESTAPP’01, 2001, pp. 26-45 · Zbl 1036.03036
[7] Dyckhoff, R.; Urban, C., Strong normalization of herbelin’s explicit substitution calculus with substitution propagation, Journal of logic and computation, 13, 689-706, (2003) · Zbl 1036.03036
[8] Espírito Santo, J., Revisiting the correspondence between cut elimination and normalisation, (), 600-611 · Zbl 0973.03073
[9] Girard, J.-Y., Linear logic, Theoretical computer science, 50, 1-102, (1987) · Zbl 0625.03037
[10] Herbelin, H., A \(\lambda\)-calculus structure isomorphic to Gentzen-style sequent calculus structure, (), 61-75 · Zbl 1044.03509
[11] H. Herbelin, Séquents qu’on calcule. Thèse de Doctorat, Université Paris 7, 1995
[12] Herbelin, H., Explicit substitutions and reducibility, Journal of logic and computation, 11, 429-449, (2001) · Zbl 0984.03014
[13] S. Kamin, J.-J. Lévy, Attempts for generalizing the recursive path orderings. Handwritten paper, University of Illinois, 1980
[14] Lengrand, S., Call-by-value, call-by-name, and strong normalization for the classical sequent calculus, () · Zbl 1270.68070
[15] Lengrand, S.; Dyckhoff, R.; McKinna, J., A sequent calculus for type theory, (), 441-455 · Zbl 1225.03010
[16] Parigot, M., \(\lambda \mu\)-calculus: an algorithmic interpretation of classical natural deduction, (), 190-201 · Zbl 0925.03092
[17] Parigot, M., Proofs of strong normalisation for second order classical natural deduction, The journal of symbolic logic, 62, 1461-1479, (1997) · Zbl 0941.03063
[18] Polonovski, E., Strong normalization of \(\overline{\lambda} \mu \widetilde{\mu}\)-calculus with explicit substitutions, (), 423-437 · Zbl 1126.03307
[19] Rocheteau, J., \(\lambda \mu\)-calculus and duality: call-by-name and call-by-value, (), 204-218 · Zbl 1078.68018
[20] C. Urban, Classical Logic and Computation, Ph.D. Thesis, University of Cambridge, 2000
[21] Wadler, P., Call-by-value is dual to call-by-name, (), 189-201 · Zbl 1315.68060
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.