Alpha equivalence equalities

AbstractProgramming languages and logics, which are pervasive in Computer Science, have syntax which involves variable binding constructors. As such, reasoning about such languages in general, and formal reasoning in particular (such as within a theorem prover), requires frameworks within which the syntax may be properly represented. One key requirement is a correct representation of α-equivalence.The current literature provides a number of different definitions of the notion of α-equivalence. The formal definitions may be nameless as in the approach of de Bruijn, or have explicit names, as in the approaches that use either a renaming/substitution axiom, or instead use a notion of variable swapping.The first contribution of this paper is to draw together five definitions of α-equivalence relations and to prove formally and in detail, but using mathematics, that the relations are all equal. There are two key reasons for doing this: Firstly, the literature has many examples of proofs of results involving α-equivalence which contain technical errors. Such examples concern both the application of α-equivalence, and the meta-theory of α-equivalence itself. Secondly, the literature does not currently contain detailed presentations of such results. The point of giving the detail is partly to avoid falling into common error-traps, but mainly to provide clear mathematical machinery that will be useful to those working in the area. This includes systems of inductive rules and proofs by induction, and clear accounts of the key lemmas that support the main proofs.The second contribution is to provide two definitions of α-equivalence relations over (program) contexts, namely expressions with a single meta-variable (or “hole”). One of the definitions is already in the literature, and the other is new. We prove some basic properties of α-equivalence on contexts, and show that the two definitions give rise to the same relation