A simple formalization of alpha-equivalence

TL;DR

This paper presents a grounded, inductive formalization of alpha-equivalence in untyped lambda calculus, making it more accessible for teaching and formal verification, and fully formalized in the Rocq Prover.

Contribution

It introduces the first inductive definition of alpha-equivalence that aligns with standard specifications and is suitable for formal proof environments.

Findings

Inductive definition of alpha-equivalence conforms to literature standards

Formalization in Rocq Prover demonstrates practical applicability

Facilitates teaching and formal reasoning about lambda calculus

Abstract

While teaching untyped $\lambda$-calculus to undergraduate students, we were wondering why $\alpha$-equivalence is not directly inductively defined. In this paper, we demonstrate that this is indeed feasible. Specifically, we provide a grounded, inductive definition for $\alpha$-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.