A simple formalization of alpha-equivalence

TL;DR

The paper addresses how to formalize $\alpha$-equivalence for untyped $\lambda$-terms with a grounded, inductive approach amenable to teaching and formal reasoning. It introduces context-indexed relations $\langle xs; x \rangle =_v\alpha \langle l; y \rangle$ and $\langle xs; t \rangle =_\alpha \langle l; u \rangle$, proving them to be a robust equivalence and congruence, and develops a relational specification for substitution alongside a capture-avoiding substitution function. A central substitution lemma is proved using a combination of SubstAlphaMain and a variable-refresh mechanism, supported by a decision procedure for $\alpha$-equivalence and a comparison with de Bruijn indices. The work is fully formalized in the Rocq Prover, with code and a GitHub repository, demonstrating the feasibility and educational value of inductive $\alpha$-equivalence in formal lambda-calculus work. The approach provides concrete, mechanized proofs of core properties and a practical substitution framework suitable for teaching and verification.

Abstract

While teaching untyped $λ$-calculus to undergraduate students, we were wondering why $α$-equivalence is not directly inductively defined. In this paper, we demonstrate that this is indeed feasible. Specifically, we provide a grounded, inductive definition for $α$-equivalence and show that it conforms to the specification provided in the literature. The work presented in this paper is fully formalized in the Rocq Prover.

Figures (1)

• Figure 1: Inference rules for $\alpha$-equivalence.

Theorems & Definitions (5)

• Example 3.1
• Example 5.1
• Example 8.1
• Example 8.2
• Example 9.1