# Alpha-equivalence

### From The Twelf Project

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.

**Failed to parse (PNG conversion failed;
check for correct installation of latex, dvips, gs, and convert): e ::= x \mid \lambda x.\, e \mid e_1\ e_2**

Alpha-equivalence for terms **Failed to parse (PNG conversion failed;
check for correct installation of latex, dvips, gs, and convert): \texttt{}e**

is the least congruence relationFailed to parse (PNG conversion failed;

**check for correct installation of latex, dvips, gs, and convert): \texttt{}e_1 =_\alpha e_2**

closed under theFailed to parse (PNG conversion failed;

**check for correct installation of latex, dvips, gs, and convert): \texttt{}\alpha**

axiom:

**Failed to parse (PNG conversion failed;
check for correct installation of latex, dvips, gs, and convert): {(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.

Twelf'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.