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)