nLab
alpha-equivalence

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.

Revised on June 21, 2012 21:30:32 by Mike Shulman (71.136.239.115)