name capture

1 definition found

name capture - Free On-line Dictionary of Computing (26 May 2007) :

  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)