Abstract
We study preservation of β-strong normalization by λ d and λ dn , two confluent λ-calculi with explicit substitutions defined in [10]; the particularity of these calculi is that both have a composition operator for substitutions. We develop an abstract simulation technique allowing to reduce preservation of β-strong normalization of one calculus to that of another one, and apply said technique to reduce preservation of β-strong normalization of λ d and λ dn to that of λ f , another calculus having no composition operator. Then, preservation of β-strong normalization of λ f is shown using the same technique as in [2]. As a consequence, λ d and λ dn become the first λ-calculi with explicit substitutions having composition and preserving β- strong normalization. We also apply our technique to reduce preservation of β-strong normalization of the calculus λ v in [14] to that of λ f .
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
M. Abadi, L. Cardelli, P.-L. Curien, and J.-J. Lévy. Explicit substitutions. Journal of Functional Programming, 4(1):375–416, 1991.
Z.-El-A. Benaissa, D. Briaud, P. Lescanne, and J. Rouyer-Degli. λν, a calculus of explicit substitutions which preserves strong normalisation, 1995. Available from http://www.loria.fr/ lescanne/publications.html.
P.-L. Curien, T. Hardin, and J.-J. Lévy. Confluence properties of weak and strong calculi of explicit substitutions. Technical Report 1617, INRIA Rocquencourt, 1992.
P.-L. Curien, T. Hardin, and A. Ríos. Strong normalisation of substitutions. In MFCS'92, number 629 in LNCS, pages 209–218, 1992.
N. de Bruijn. Lambda-calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indag. Mat., 5(35):381–392, 1972.
N. de Bruijn. Lambda-calculus notation with namefree formulas involving symbols that represent reference transforming mappings. Indag. Mat., (40):384–356, 1978.
T. Ehrhard. Une sémantique catégorique des types dépendants. Application au calcul des constructions. Thèse de doctorat, Université de Paris VII, 1988.
M. C. F. Ferreira, D. Kesner and L. Puel. λ-calculi with explicit substitutions and composition which preserve β-strong normalization, 1996. Available via ftp at ftp.lri.fr/LRI/articles/kesner/psn.ps.gz.
T. Hardin and J.-J. Lévy. A confluent calculus of substitutions. In France-Japan Artificial Intelligence and Computer Science Symposium, 1989.
D. Kesner. Confluence properties of extensional and non-extensional λ-calculi with explicit substitutions. In Proc. of the Seventh Int. Conf. RTA, 1996. To appear.
F. Kamareddine and A. Ríos. The confluence of the λse-calculus via a generalized interpretation method. Technical report TR-1996-19, Dep. of Computing Science, University of Glasgow, 1996.
F. Kamareddine and A. Ríos. A λ-calculus à la de Bruijn with explicit substitutions. In Proc. of the Int. Symposium on Programming Language Implementation and Logic Programming, number 982 in LNCS. Springer-Verlag, 1995.
P. Lescanne. Personal Communication. 1996.
P. Lescanne. From 298-01 to λv, a journey through calculi of explicit substitutions. In Ann. ACM Symp. POPL, pages 60–69. ACM, 1994.
P.-A. Mellies. Four typed-lambda calculi with explicit substitutions may not terminate: the first examples, 1994. Draft.
P.-A. Mellies. Typed λ-calculi with explicit substitutions may not terminate. In M. Dezani-Ciancaglini and G. Plotkin, editors, Proc. of Int. Conf. TLCA, number 902 in LNCS, April 1995.
C. Muñoz. Confluence and preservation of strong normalisation in an explicit substitutions calculus. In Proc. of the Symposium LICS, 1996 To appear.
A. Ríos. Contribution à l'étude des λ-calculus avec substitutions explicites. Thèse de doctorat, Université de Paris VII, 1993.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ferreira, M.C.F., Kesner, D., Puel, L. (1996). λ-calculi with explicit substitutions and composition which preserve β-strong normalization. In: Hanus, M., Rodríguez-Artalejo, M. (eds) Algebraic and Logic Programming. ALP 1996. Lecture Notes in Computer Science, vol 1139. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61735-3_19
Download citation
DOI: https://doi.org/10.1007/3-540-61735-3_19
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61735-8
Online ISBN: 978-3-540-70672-4
eBook Packages: Springer Book Archive