Search in: Word
Vietnamese keyboard: Off
Virtual keyboard: Show
Computing (FOLDOC) dictionary
name capture
Jump to user comments
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.