Alpha Conversion

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.

Example

The following is a case of a alpha conversion:

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

References

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