Alpha Equivalence

Two expressions are AlphaEquivalent 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.