λυ, a calculus of explicit substitutions which preserves strong normalisation

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.