name capture

name capture

(reduction)In beta reduction, when a term containing afree occurrence of a variable v is substituted into anotherterm 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 thesame name. The most common solution is to rename the boundvariable 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 benotionally contained within the body of some lambda abstraction which binds y. If we never reduce inside thebody of a lambda abstraction (as in reduction to weak head normal form) then name capture cannot occur.