← 研踪 PaperTrailarXiv:2507.10181 · v7
A simple formalization of alpha-equivalence
首次提交 2025-07-14 19:42
版本更新 2026-11-05 21:18
雷达观测 2026-11-06 12:09
摘要
While teaching untyped $λ$-calculus to undergraduate students, we were left 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.
观测到的版本
相邻记录可能跳过中间版本；首次发现 v2 及以上也会标为版本更新。
v7 · 2026-11-05 21:18 · 最新观测版本
A simple formalization of alpha-equivalence
While teaching untyped $λ$-calculus to undergraduate students, we were left 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.
查看此版本解读 →查看此版本原文 ↗v6 · 2026-11-04 21:00
A simple formalization of alpha-equivalence
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.
查看此版本解读 →查看此版本原文 ↗