Abstract
Herbelin presented (at CSL’94) an explicit substitution calculus with a sequent calculus as a type system, in which reduction steps correspond to cut-elimination steps. The calculus, extended with some rules for substitution propagation, simulates β-reduction of ordinary λ-calculus. In this paper we present a proof of strong normalization for the typable terms of the calculus. The proof is a direct one in the sense that it does not depend on the result of strong normalization for the simply typed λ-calculus, unlike an earlier proof by Dyckhoff and Urban.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abadi, M., Cardelli, L., Curien, P.-L., Lévy, J.-J.: Explicit substitutions. Journal of Functional Programming 1, 375–416 (1991)
Bloo, R.: Preservation of strong normalisation for explicit substitution. Computing Science Report 95-08, Eindhoven University of Technology (1995)
Bloo, R.: Preservation of Termination for Explicit Substitution. PhD thesis, Eindhoven University of Technology (1997)
Bloo, R., Geuvers, H.: Explicit substitution: on the edge of strong normalization. Theoretical Computer Science 211, 375–395 (1999)
Bloo, R., Rose, K.H.: Preservation of strong normalisation in named lambda calculi with explicit substitution and garbage collection. In: Proceedings of CSN 1995 (Computing Science in the Netherlands), pp. 62–72 (1995)
Bonelli, E.: Perpetuality in a named lambda calculus with explicit substitutions. Mathematical Structures in Computer Science 11, 47–90 (2001)
Dougherty, D., Lescanne, P.: Reductions, intersection types, and explicit substitutions. Mathematical Structures in Computer Science 13, 55–85 (2003)
Dyckhoff, R., Pinto, L.: Proof search in constructive logic. In: Cooper, S.B., Truss, J.K. (eds.) Proceedings of the Logic Colloquium 1997. London Mathematical Society Lecture Note Series, vol. 258, pp. 53–65. Cambridge University Press, Cambridge (1997)
Dyckhoff, R., Urban, C.: Strong normalisation of Herbelin’s explicit substitution calculus with substitution propagation. In: Proceedings of WESTAPP 2001, pp. 26–45 (2001)
Dyckhoff, R., Urban, C.: Strong normalization of Herbelin’s explicit substitution calculus with substitution propagation. Journal of Logic and Computation 13, 689–706 (2003)
Espírito Santo, J.: Revisiting the correspondence between cut elimination and normalisation. In: Welzl, E., Montanari, U., Rolim, J.D.P. (eds.) ICALP 2000. LNCS, vol. 1853, pp. 600–611. Springer, Heidelberg (2000)
Herbelin, H.: A λ-calculus structure isomorphic to Gentzen-style sequent calculus structure. In: Pacholski, L., Tiuryn, J. (eds.) CSL 1994. LNCS, vol. 933, pp. 61–75. Springer, Heidelberg (1995)
Herbelin, H.: Explicit substitutions and reducibility. Journal of Logic and Computation 11, 429–449 (2001)
Joachimski, F., Matthes, R.: Short proofs of normalization for the simply typed λ-calculus, permutative conversions and Gödel’s T. Archive for Mathematical Logic 42, 59–87 (2003)
Melliès, P.-A.: Typed λ-calculi with explicit substitutions may not terminate. In: Dezani-Ciancaglini, M., Plotkin, G. (eds.) TLCA 1995. LNCS, vol. 902, pp. 328–334. Springer, Heidelberg (1995)
Ritter, E.: Characterising explicit substitutions which preserve termination. In: Girard, J.-Y. (ed.) TLCA 1999. LNCS, vol. 1581, pp. 325–339. Springer, Heidelberg (1999)
Tait, W.W.: Intensional interpretations of functionals of finite type I. The Journal of Symbolic Logic 32, 198–212 (1967)
Troelstra, A.S., Schwichtenberg, H.: Basic Proof Theory, 2nd edn. Cambridge Tracts in Theoretical Computer Science, vol. 43. Cambridge University Press, Cambridge (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kikuchi, K. (2004). A Direct Proof of Strong Normalization for an Extended Herbelin’s Calculus. In: Kameyama, Y., Stuckey, P.J. (eds) Functional and Logic Programming. FLOPS 2004. Lecture Notes in Computer Science, vol 2998. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24754-8_18
Download citation
DOI: https://doi.org/10.1007/978-3-540-24754-8_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-21402-1
Online ISBN: 978-3-540-24754-8
eBook Packages: Springer Book Archive