Name capture
<reduction> In
beta reduction, when a term containing a
free occurrence of a variable v is substituted into another term where v is bound the free v becomes spuriously bound or "captured".
E.g.
(\ x . \ y . x y) y
-->
\ y . y y (WRONG)
This problem arises because two distinct variables have the same name.
The most common solution is to rename the bound variable using
alpha conversion:
(\ x . \ y' . x y') y --> \ y' . y y'
Another solution is to use
de Bruijn notation.
Note that the argument expression, y, contained a
free variable.
The whole expression above must therefore be notionally contained within the body of some
lambda abstraction which binds y.
If we never reduce inside the body of a lambda abstraction (as in reduction to
weak head normal form) then name capture cannot occur.
