catflap.org Online Dictionary Query

  name capture
       
           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)