Name capture

<reduction> 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".


(\ 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.

< Previous Terms Terms Containing name capture Next Terms >
nailed to the wall
nailing jelly
naive user
alpha conversion
beta reduction
De Bruijn notation
name capture
Weak Head Normal Form
named pipe
name resolution
name service switching