A simple formalization of alpha-equivalence

Kalmer Apinis, Danel Ahman

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…