Alpha Equivalence

Definition

Alpha equivalence (or α-equivalence) is an equivalence relation on expressions stating that two terms are equal if they differ only in the names of bound variables.

In Lambda Calculus and Type Theory, alpha equivalence formalizes the principle that the choice of bound variable names does not affect the meaning of an expression.

Two terms are alpha equivalent, written $s{\equiv }_{\alpha }t$, if one can be obtained from the other by consistently renaming bound variables.

Alpha Conversion

Alpha conversion (or α-conversion) is the operation of renaming bound variables. For example:

$\lambda x.e{\equiv }_{\alpha }\lambda y.e[y/x]$

provided $y\notin \text{FV}(e)$ (i.e., $y$ is fresh and does not appear free in $e$).

Examples

Lambda Abstractions

$\lambda x.x{\equiv }_{\alpha }\lambda y.y$

Both represent the identity function, differing only in parameter name.

$\lambda x.\lambda y.x+y{\equiv }_{\alpha }\lambda a.\lambda b.a+b$

The nested abstractions can have their bound variables renamed independently.

Avoiding Capture

Alpha conversion is essential for avoiding variable capture during Substitution:

$(\lambda y.x)[y/x]/{\equiv }_{\alpha }\lambda y.y$

Instead, we must first alpha-convert: $\lambda y.x{\equiv }_{\alpha }\lambda z.x$, then substitute:

$(\lambda z.x)[y/x]{\equiv }_{\alpha }\lambda z.y$

Non-Equivalent Terms

$\lambda x.y/{\equiv }_{\alpha }\lambda x.z$

These differ in their free variables, not just bound variable names.

$\lambda x.x/{\equiv }_{\alpha }\lambda x.y$

The first is a closed term, the second contains a free variable $y$.

Formal Definition

Alpha equivalence can be defined inductively on term structure:

• $x{\equiv }_{\alpha }x$ for any variable $x$
• $st{\equiv }_{\alpha }{s}^{\prime }{t}^{\prime }$ if $s{\equiv }_{\alpha }{s}^{\prime }$ and $t{\equiv }_{\alpha }{t}^{\prime }$
• $\lambda x.s{\equiv }_{\alpha }\lambda y.t$ if $s{\equiv }_{\alpha }t[y/x]$ and $y$ is fresh for $s$

Properties

• Alpha equivalence is an equivalence relation (reflexive, symmetric, transitive)
• Alpha equivalent terms have the same free variables: if $s{\equiv }_{\alpha }t$, then $\text{FV}(s)=\text{FV}(t)$
• Alpha equivalence is preserved under substitution: if $s{\equiv }_{\alpha }t$, then $s[u/x]{\equiv }_{\alpha }t[u/x]$
• Beta reduction respects alpha equivalence: if $s{\equiv }_{\alpha }t$ and $s{\to }_{\beta }{s}^{\prime }$, then there exists $t^{\prime }$ such that $t{\to }_{\beta }{t}^{\prime }$ and $s^{\prime }{\equiv }_{\alpha }{t}^{\prime }$

Identification Up to Alpha

In practice, terms are typically identified up to alpha equivalence. This means:

• Two terms differing only in bound variable names are considered identical
• Implementations use techniques like de Bruijn indices or locally nameless representations to avoid explicit alpha conversion
• Type checkers and proof assistants treat alpha-equivalent terms as definitionally equal

In Dependent Type Theory

Alpha equivalence extends to dependent types:

${\Pi }_{x:A}B(x){\equiv }_{\alpha }{\Pi }_{y:A}B[y/x]$

${\Sigma }_{x:A}B(x){\equiv }_{\alpha }{\Sigma }_{y:A}B[y/x]$

provided the renaming is capture-avoiding.

Related Concepts

• Bound Variable: Variables whose names can be changed via alpha conversion
• Free Variable: Variables that are preserved by alpha equivalence
• Substitution: The operation underlying alpha conversion
• Scope: The region affected by variable renaming
• Lambda Calculus: The foundational system where alpha equivalence is defined
• Variable: The syntactic objects being renamed
• Beta Reduction: A reduction that respects alpha equivalence