alpha conversion
<theory> In {lambda-calculus} and {reduction}, the renaming of
a {formal parameter} in a {lambda abstraction}. This does not
change the meaning of the abstraction. For example:
\ x . x+1 <--> \ y . y+1
If the {actual argument} to a lambda abstraction contains
instances of the abstraction's formal parameter then it is
necessary to rename the parameter before applying the
abstraction to avoid {name capture}.
(1995-05-10)