Editing Lambda calculus (section)

==== Capture-avoiding substitutions ====
Suppose <math>t</math>, <math>s</math> and <math>r</math> are lambda terms, and <math>x</math> and <math>y</math> are variables.
The notation <math>t[x := r]</math> indicates substitution of <math>r</math> for <math>x</math> in <math>t</math> in a ''capture-avoiding'' manner. This is defined so that:
* <math>x[x := r] = r</math> ; with <math>r</math> substituted for <math>x</math>, <math>x</math> becomes <math>r</math>
* <math>y[x := r] = y</math> if <math>x \neq y</math> ; with <math>r</math> substituted for <math>x</math>, <math>y</math> (which is not <math>x</math>) remains <math>y</math>
* <math>(t s)[x := r] = (t[x := r])(s[x := r])</math> ; substitution distributes to both sides of an application
* <math>(\lambda x.t)[x := r] = \lambda x.t</math> ; a variable bound by an abstraction is not subject to substitution; substituting such variable leaves the abstraction unchanged
* <math>(\lambda y.t)[x := r] = \lambda y.(t[x := r])</math> if <math>x \neq y</math> and <math>y</math> does not appear among the free variables of <math>r</math> (<math>y</math> is said to be "[[fresh variable|fresh]]" for <math>r</math>) ; substituting a variable which is not bound by an abstraction proceeds in the abstraction's body, provided that the abstracted variable <math>y</math> is "fresh" for the substitution term <math>r</math>.

For example, <math>(\lambda x.x)[y := y] = \lambda x.(x[y := y]) = \lambda x.x</math>, and <math>((\lambda x.y)x)[x := y] = ((\lambda x.y)[x := y])(x[x := y]) = (\lambda x.y)y</math>.

The freshness condition (requiring that <math>y</math> is not in the [[#Free and bound variables|free variables]] of <math>r</math>) is crucial in order to ensure that substitution does not change the meaning of functions.

For example, a substitution that ignores the freshness condition could lead to errors: <math>(\lambda x.y)[y := x] = \lambda x.(y[y := x]) = \lambda x.x</math>. This erroneous substitution would turn the constant function <math>\lambda x.y</math> into the identity <math>\lambda x.x</math>.

In general, failure to meet the freshness condition can be remedied by alpha-renaming first, with a suitable fresh variable.
For example, switching back to our correct notion of substitution, in <math>(\lambda x.y)[y := x]</math> the abstraction can be renamed with a fresh variable <math>z</math>, to obtain <math>(\lambda z.y)[y := x] = \lambda z.(y[y := x]) = \lambda z.x</math>, and the meaning of the function is preserved by substitution.