Computer Dictionary Online

Medical Dictionary   Law Dictionary   Legal Dictionary   Website Design

0  1  2  3  4  5  6  7  8  9  a  b  c  d  e  f  g  h  i  j  k  l  m  n  o  p  q  r  s  t  u  v  w  x  y  z 

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.


Contact the Computer Dictionary Online  ::  Link to the Computer Dictionary Online  ::  Disclaimer for Computer Dictionary Online

Computer Dictionary Online
Copyright © 2017