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.