Explicit renaming of bound variables

TL;DR

This paper introduces a lambda calculus framework with explicit substitutions and named variables, where bound variable renaming during substitution is handled through special reductions that can be postponed.

Contribution

It proposes a novel lambda calculus with explicit renaming mechanisms that allow delayed renaming during substitutions.

Findings

Renaming of bound variables can be explicitly controlled and delayed.

The calculus provides a new approach to handling variable renaming in lambda calculus.

Potential applications in optimizing substitution processes in functional programming.

Abstract

We present some lambda calculus with explicit substitutions and named variables. The characteristic feature of this calculus is as follows: renaming of bound variables when performing substitutions is done using special reductions and may be delayed.