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:
- (λx.M) N → M〈x:=N〉
- x〈x:=N〉 → N
- x〈y:=N〉 → x (x≠y)
- (M1M2) 〈x:=N〉 → (M1〈x:=N〉) (M2〈x:=N〉)
- (λ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.
Read more about this topic: Explicit Substitution