λCalculi with Explicit Substitutions Preserving Strong Normalization |
| |
Authors: | Maria C. F. Ferreira Delia Kesner Laurence Puel |
| |
Affiliation: | (1) Dep. de Informática, Fac. de Ciências e Tecnologia, Univ. Nova de Lisboa, Quinta da Torre, P-2825 Monte da Caparica, Portugal, (e-mail: cf@di.fct.unl.pt), PT;(2) CNRS and Laboratoire de Recherche en Informatique, Bat 490, Université de Paris-Sud, F-91405 Orsay Cedex, France, (e-mail: {kesner,puel}@lri.fr), FR |
| |
Abstract: | This paper studies preservation of β-strong normalization by two different confluent λ-calculi with explicit substitutions defined in [96]; the particularity of these calculi, called λ d and λ dn respectively, is that both have a (weak) composition operator for substitutions. We apply an abstract simulation technique to reduce preservation of β-strong normalization of λ d and λ dn to that of another calculus, called λ f 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 (weak) composition and preserving β-strong normalization. As an aside, we also show how to apply our technique to reduce preservation of β-strong normalization of the calculus λ v in [20] to that of λ f . Received: August 19, 1997; revised version: November 13, 1998 |
| |
Keywords: | λ -Calculus, Explicit substitutions, Preservation of strong normalization |
本文献已被 SpringerLink 等数据库收录! |
|