Alphaequivalent

Alphaequivalent, short for alpha-equivalence, is a fundamental concept in the lambda calculus and related formal systems. It describes when two lambda terms are considered the same except for the names of their bound variables. In alpha-equivalence, renaming bound variables does not change the meaning of a term, while free variables are left intact.

Two terms M and N are alpha-equivalent if one can be transformed into the other by a finite sequence of bound-variable renamings. For example, λx. x is alpha-equivalent to λy. y, and λx. λy. x y is alpha-equivalent to λa. λb. a b. These two terms have the same structure and binding pattern, only the names of the bound variables differ. By contrast, λx. x y is not alpha-equivalent to λx. y x, since renaming bound variables cannot swap the positions of x and y in the body where one is free.

Alpha-equivalence is an equivalence relation: it is reflexive, symmetric, and transitive. It is also a congruence with respect to the language’s constructors, meaning that alpha-equivalent subterms remain alpha-equivalent when placed in larger terms. This notion allows practitioners to treat terms that differ only by bound-variable names as identical in proofs, implementations, and formal reasoning.

In practice, alpha-conversion is the procedure used to rename bound variables to avoid name capture during substitution. The concept underpins many formal treatments of lambda terms and is a standard building block for defining beta and eta equivalence as well.