Alpha-equivalence

From The Twelf Project
Jump to: navigation, search

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.

Alpha-equivalence for terms is the least congruence relation closed under the axiom:

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.