Bridging de Bruijn Indices and Variable Names in Explicit Substitutions Calculi

Calculi of explicit substitutions have almost always been presented using de Bruijn indices with the aim of avoiding -conversion and being as close to machines as possible. De Bruijn indices however, though very suitable for the machine, are di cult to human users. This is the reason for a renewed interest in systems of explicit substitutions using variable names. Formal systems of explicit substitutions using variable names is a new area however and we believe, it 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. In our aim to do so, we provide the t-calculus: a -calculus a la de Bruijn which can be translated into a -calculus with explicit substitutions written with variables names. We present explicitly this translation and use it to obtain preservation of strong normalisationfor t. Moreover, we show several properties ...

• Type: Journal
• Year: 1998
• Where: IGPL
• Authors: Fairouz Kamareddine, Alejandro Ríos
• Keywords: Explicit Substitutions, IGPL 1998, Machine, Variable Names