Explicit Substitution - Basics

Basics

A simple example of a lambda calculus with explicit substitution is "λx", which adds one new form of term to the lambda calculus, namely the form M〈x:=N〉, which reads "M where x will be substituted by N". (The meaning of the new term is the same as the common idiom let x:=N in M from many programming languages.) λx can be written with the following rewriting rules:

1. (λx.M) N → M〈x:=N〉
2. x〈x:=N〉 → N
3. x〈y:=N〉 → x (x≠y)
4. (M₁M₂) 〈x:=N〉 → (M₁〈x:=N〉) (M₂〈x:=N〉)
5. (λx.M) 〈y:=N〉 → λx.(M〈y:=N〉) (x≠y)

While making substitution explicit, this formulation still retains the complexity of the lambda calculus "variable convention", requiring arbitrary renaming of variables during reduction to ensure that the "(x≠y)" condition on the last rule is always satisfied before applying the rule. Therefore many calculi of explicit substitution avoid variable names altogether by using a so-called "name-free" De Bruijn index notation.