Mechanising Böhm Trees and λη-Completeness

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