name capture

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