Two expressions are '''Alpha''''''Equivalent''' if one can be obtained from the other by non-clashing substitution of FreeVariable names.

''\x.\y.xyz'' is Alpha Equivalent to ''\a.\b.abz''

but 

''\x.\y.xyz'' is equivalent to neither ''\a.\b.abc'' nor ''\a.\a.aaz''

----

Example: With the RefactoringBrowser, when you do an Extract Method, it determines if there is another method in the class or superclasses  that has the same structure. If there is, it offers to make a call to it rather than creating a new method. It basically uses what is known as AlphaEquivalence. Meaning that ''the two methods can have different variable names as long as they are used in the same manner''.

----

Because of AlphaEquivalence a CaptureAvoidingRenaming is usually assumed to be implicitly done when performing e.g. BetaReduction or substitution in LambdaCalculus. 

A way to avoid the need for CaptureAvoidingRenaming is to always rename to a CanonicalLambdaForm (which means, that the names can be dropped on the lambda actually).

Example:

''\x.\y.xyz'' becomes ''\a.\b.abz'' which can be shortened to ''\\abz''.

''\n.\a.\q.xqza'' becomes ''\a.\b.\c.xczb'' which can be shortened to ''\\\xczb''.

(The 'canonical' order abcdefg... is assumed).

This is usually less readable, but better suited for automatical processing.