In the lambda calculus an *α-conversion*
is used to rename variables.
We can define α-conversion as an abstraction:

` ``λx.λy.(x y)`

Note that λ-terms which are syntactically equal modulo α-conversion are considered to be equivalent. One use of α-conversion is the rewriting of λ-terms to avoid parasitic bindings introduced by the β-reduction.

The following is a case of a alpha conversion:

(λx.λy.(x y) λz.M) →_{β}λy.(λz.M y) →_{β}λy.M[z/y]

W. Kluge. *Abstract Computing Machines. A Lambda Calculus Perspective.* Springer, 2005.

Copyright © 2014 Barry Watson. All rights reserved.