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 鈥渉ole鈥?. 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.