|
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)
|
