λν, a calculus of explicit substitutions which preserves strong normalisation
- 1 January 1996
- journal article
- research article
- Published by Cambridge University Press (CUP) in Journal of Functional Programming
- Vol. 6 (5), 699-722
- https://doi.org/10.1017/s0956796800001945
Abstract
Explicit substitutions were proposed by Abadi, Cardelli, Curien, Hardin and Lévy to internalise substitutions into λ-calculus and to propose a mechanism for computing on substitutions. λν is another view of the same concept which aims to explain the process of substitution and to decompose it in small steps. It favours simplicity and preservation of strong normalisation. This way, another important property is missed, namely confluence on open terms. In spirit, λν is closely related to another calculus of explicit substitutions proposed by de Bruijn and called CλξΦ. In this paper, we introduce λν, we present CλξΦ in the same framework as λν and we compare both calculi. Moreover, we prove properties of λν; namely λν correctly implements β reduction, λν is confluent on closed terms, i.e. on terms of classical λ-calculus and on all terms that are derived from those terms, and finally λν preserves strong normalisation in the following sense: strongly β normalising terms are strongly λν normalising.Keywords
This publication has 1 reference indexed in Scilit:
- From λσ to λυPublished by Association for Computing Machinery (ACM) ,1994