In beta reduction, when a term containing a free occurrence of a variable v iSSubStituted into another term where v iS bound the free v becomeSSpuriouSly 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)
