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.
(1995-03-14)
Nearby terms:
naive « naive user « NAK « name capture »
named » named pipe » name resolution
|
