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.

翻译：在向本科生教授无类型λ-演算时，我们曾思考为何α-等价未被直接归纳定义。本文证明了这种定义方式确实是可行的。具体而言，我们为α-等价提供了一个基于基础的归纳定义，并证明其符合文献中给出的规范。本文提出的工作已在Rocq Prover中完成形式化验证。