By Fairouz Kamareddine and Alejandro Rios, in the Logic Journal of the Interest Group in Pure and Applied Logic, available from Fairouz Kamareddine’s website:
Calculi of explicit substitutions have almost always been presented using de Bruijn indices with the aim of avoiding alpha-conversion and being as close to machines as possible. De Bruijn indices however, though very suitable for the machine, are difficult to human users. This is the reason for a renewed interest in systems of explicit substitutions using variable names. We believe that the study of these systems should not develop without being well-tied to existing work on explicit substitutions. The aim of this paper is to establish a bridge between explicit substitutions using de Bruijn indices and using variable names and to do so, we provide the lambda-t-calculus: a lambda-calculus a la de Bruijn which can be translated into a lambda-calculus with explicit substitutions written with variables names. We present explicitly this translation and use it to obtain preservation of strong normalisation for lambda-t. Moreover, we show several properties of lambda-t, including confluence on closed terms and e#ciency to simulate beta-reduction. Furthermore, lambda-t is a good example of a calculus written in the lambda-s-style (cf. ) that possesses the updating mechanism of the calculi a la lambda-sigma.