Alpha-equivalence

Alpha-equivalence is a notion of equivalence on terms with binding structure. It captures the notion that the names of bound variables are unimportant; all that matters is the binding structure they induce.

Consider the untyped lambda-calculus.

$e ::= x \mid \lambda x.\, e \mid e_1\ e_2$

Alpha-equivalence for terms $\texttt{}e$ is the least congruence relation $\texttt{}e_1 =_\alpha e_2$ closed under the $\texttt{}\alpha$ axiom:

${(y \not = x \,and\, y \not\in \mathit{FV}(e)) \over \lambda x.\, e =_\alpha \lambda y.\, [y/x]e}\alpha$

Alpha-equivalence generalizes in a straightforward manner to any term language with binding structure.

STELF’s notion of term equality respects alpha-equivalence; when an object-language is represented using higher-order abstract syntax, the representation enjoys alpha-equivalence for free.