During evaluation of lambda calculus, we often need to perform substitutions of variables or expressions. To evaluate the application (λx.e1) e2 (where e1 and e2 are arbitrary expressions) we would need to replace occurrences of x inside e1 with e2 (notation: e1 {e2\x}). Normally substitutions are applied recursively, but since the expressions involved in the substitution might share variable names, the meaning of the resulting expression might change if we are not careful.

For example, suppose we were to evaluate (λx.λy.x y) y. If we were to directly substitute y for x in λy.x y, we would get λy.y y. This changes the meaning of the expression, because the y which we wanted to substitute was originally a free variable; it is not the same y that is bound as an argument to the lambda. In our resulting incorrect expression, the y we substituted became bound, or captured under the lambda - we want to avoid this by doing something called capture-avoiding substitution.

To perform capture-avoiding substitution on λv1.e1 {e2\v2} (where v1 and v2 are arbitrary variables), there are two things we need to check to make sure the variable names do not conflict.

1. We need to make sure that v1 and v2 are not the same variable name. If they are, then we need to rename v1 to something else. This is because performing a simple substitution would also replace variables bound under the abstraction for v1 with e2, which would be incorrect.
2. We need to make sure that v1 is not in the free variables of of e2. If it is, then we need to rename v1 to something else. This is because performing a simple substitution would cause occurrences of v1 inside e2 to become bound (as in the example earlier).

Once we have made sure there are no conflicts, we can continue applying the substitution recursively (λv1.(e1 {e2\v2})).

To correctly perform substitution for the earlier example, we would rename the y in λy.x y to something else that does not conflict (like z), then perform the substitution.

(λx.λy.x y) y -> λy.x y {y\x} -> λz.x z {y\x} -> λz.(x z {y\x}) -> λz.y z

To define things more formally, the complete rules for substitution would be as follows:

• v1 {e\v2} -> e if v1 == v2, otherwise v1
• e1 e2 {e3\v} -> (e1 {e3\v}) (e2 {e3\v})
• λv1.e1 {e2\v2} -> λv1.(e1 {e2\v2}) where v1 != v2 and v1 is not in the free variables of e2.