In logic and type theory, α\alpha-equivalence is the principle that two syntactic expressions (types, terms, propositions, contexts, whatever) are equivalent for all purposes if their only difference is the renaming of bound variables.

Depending on the technicalities of how variables are managed, α\alpha-equivalence may be a necessary axiom, a provable theorem, or entirely trivial. In any case, it is often (usually? always?) seen as a technicality devoid of conceptual interest. However, it can be a technically nontrivial task to implement α\alpha-conversion (which is necessary to avoid capture of free variables upon substitution) when programming logic or type theory into a computer.

Last revised on June 21, 2012 at 21:30:32. See the history of this page for a list of all contributions to it.