Sources: background card; Maziarz et al., Hashing Modulo Alpha-Equivalence, PLDI 2021, arXiv:2105.02856
Theory (CT-ML wiki): Abstract Syntax with Binding
Two terms are α-equivalent, written , if they differ only in the names of bound variables. λx. x and λy. y are the same function; the names are artefacts of how the term was written down.
For a system that identifies code by hashing its syntax, α-equivalence is the first normalisation that must happen. If it does not, renaming a loop counter changes a definition’s identity and every dependent’s identity with it — which defeats the purpose. The requirement is:
The standard implementation is to eliminate names for bound variables entirely, using de Bruijn indices (or a locally nameless representation: indices for bound variables, hashes for free ones). Then α-equivalent terms are structurally identical, and the implication above holds by construction rather than by a separate check.
Note that the converse is deliberately not claimed. Many pairs of terms are semantically equal without being α-equivalent; those need definitional equality or an equivalence edge.