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 . YY (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' . YY' 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)