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 freevariable. The whole expression above must therefore be

notionally contained within the body of some lambdaabstraction which binds y. If we never reduce inside the

body of a lambda abstraction (as in reduction to weak headnormal form) then name capture cannot occur.

(1995-03-14)