A simple formalization of alpha-equivalence
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866909991273758720 |
|---|---|
| author | Apinis, Kalmer Ahman, Danel |
| author_facet | Apinis, Kalmer Ahman, Danel |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2507_10181 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | A simple formalization of alpha-equivalence Apinis, Kalmer Ahman, Danel Logic in Computer Science 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. |
| title | A simple formalization of alpha-equivalence |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2507.10181 |