Alphaequivalence

Alpha-equivalence, denoted by ≡α, is the equivalence relation on lambda terms that identifies terms that differ only in the names of their bound variables. It formalizes the idea that the specific identifiers used for bound variables are irrelevant to the meaning of a term. Two lambda terms M and N are alpha-equivalent if one can be obtained from the other by a finite sequence of alpha-conversions, which are renamings of bound variables within abstractions, provided that such renaming avoids variable capture and preserves free variables.

Example: (λx. x) and (λy. y) are alpha-equivalent. More generally, (λx. λy. x) is alpha-equivalent to (λa. λb. a). In contrast, renaming that would cause a difference in binding structure, or renaming a bound variable to collide with a free variable, is not allowed; renaming is performed so that the binding relationships remain the same and free variables are preserved. For instance, λx. x y is alpha-equivalent to λz. z y, but not to λz. y z.

Alpha-equivalence is a foundational concept in the lambda calculus and related formalisms. It allows comparison of terms modulo renaming, and it underpins substitution, reduction, and the definition of term equality. Practical implementations often use mechanisms such as De Bruijn indices to eliminate variable names altogether and expose binding structure directly.