Bridging de Bruijn indices and variable names in explicit substitutions calculi

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. [19]) that possesses the updating mechanism of the calculi a la lambda-sigma.

0 Responses to “Bridging de Bruijn indices and variable names in explicit substitutions calculi”

  1. Leave a Comment

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s

%d bloggers like this: