Abstract
The Böhm tree is a critical notion in untyped λ-calculus, capturing the semantics of β-reduction. It underpins the proof that the equational theory of βη-equivalence is Hilbert-Post complete.
This paper presents the first formalisation of this result, following the classic text by Barendregt. It includes a coinductive definition of Böhm trees, and then uses the “Böhm out” technique to prove a restricted version of Böhm’s separability theorem, which leads to the completeness theorem.
Carrying out the proofs in HOL4, we develop a new technology to generate fresh names occurring in Böhm trees. We also simplify Barendregt’s approach, avoiding comparing Böhm trees, and leveraging more modern proofs about η-reduction (due to Takahashi).
Along the way, we also present the first mechanised proof that terms having head-normal forms are exactly those that are solvable (due to Wadsworth).
This paper presents the first formalisation of this result, following the classic text by Barendregt. It includes a coinductive definition of Böhm trees, and then uses the “Böhm out” technique to prove a restricted version of Böhm’s separability theorem, which leads to the completeness theorem.
Carrying out the proofs in HOL4, we develop a new technology to generate fresh names occurring in Böhm trees. We also simplify Barendregt’s approach, avoiding comparing Böhm trees, and leveraging more modern proofs about η-reduction (due to Takahashi).
Along the way, we also present the first mechanised proof that terms having head-normal forms are exactly those that are solvable (due to Wadsworth).
| Original language | English |
|---|---|
| Title of host publication | 16th International Conference on Interactive Theorem Proving (ITP 2025) |
| Editors | Yannick Forster, Chantal Keller |
| Place of Publication | Saarbrücken/Wadern, Germany |
| Publisher | Schloss Dagstuhl – Leibniz-Zentrum für Informatik |
| Pages | 28:1-28:18 |
| Number of pages | 18 |
| ISBN (Electronic) | 978-3-95977-396-6 |
| DOIs | |
| Publication status | Published - Sept 2025 |
| Event | 16th International Conference on Interactive Theorem Proving, ITP 2025 - Reykjavik, Iceland Duration: 28 Sept 2025 → 1 Oct 2025 Conference number: 16th https://icetcs.github.io/frocos-itp-tableaux25/itp/ (Conference Website ) https://drops.dagstuhl.de/entities/volume/LIPIcs-volume-352 (Conference Proceedings) |
Publication series
| Name | Leibniz International Proceedings in Informatics (LIPIcs) |
|---|---|
| Publisher | Schloss Dagstuhl – Leibniz-Zentrum für Informatik |
| Volume | 352 |
Conference
| Conference | 16th International Conference on Interactive Theorem Proving, ITP 2025 |
|---|---|
| Abbreviated title | ITP 2025 |
| Country/Territory | Iceland |
| City | Reykjavik |
| Period | 28/09/25 → 1/10/25 |
| Other | The ITP conference series is concerned with all aspects of interactive theorem proving, ranging from theoretical foundations to implementation aspects and applications in program verification, security, and the formalization of mathematics. This will be the 16th conference in the ITP series, while predecessor conferences from which it has evolved have been going since 1988. |
| Internet address |
|