DROPS

Document

DOI: 10.4230/LIPIcs.ITP.2025.28

Mechanising Böhm Trees and λη-Completeness

Authors: Chun Tian and Michael Norrish

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

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).

Cite as

Chun Tian and Michael Norrish. Mechanising Böhm Trees and λη-Completeness. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 28:1-28:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{tian_et_al:LIPIcs.ITP.2025.28,
  author =	{Tian, Chun and Norrish, Michael},
  title =	{{Mechanising B\"{o}hm Trees and \lambda\eta-Completeness}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{28:1--28:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.28},
  URN =		{urn:nbn:de:0030-drops-246269},
  doi =		{10.4230/LIPIcs.ITP.2025.28},
  annote =	{Keywords: untyped \lambda-calculus, B\"{o}hm trees, higher-order logic, theorem proving}
}

Search Results

Documents authored by Tian, Chun

Mechanising Böhm Trees and λη-Completeness

Abstract

Cite as

Thanks for your feedback!

Could not send message