Böhm trees are a device used in the semantic analysis of the untyped λ-calculus.
There is an entire chapter about Böhm trees in Barendregt's book [Barendregt 1984, ch. 10].
Let M be an untyped term. We consider its behaviour under head reduction.
-
If M has no head normal form, then we define its Böhm tree to be the 'empty tree'
BT(M)=⊥
-
If M has a head normal form λx1,…,xn.yM1…Mm, we define its Böhm tree BT(M) to be
Notice the following things, especially about the nontrivial case.
- It may be infinitely deep (but not wide). In fact, this is a definition by coinduction.
- It may also be written in a term-like notation (see examples below).
- BT(Ω)=⊥
- BT(λx.x)=λx.x.
- BT(λx.xΩ)=λx.x⊥
Böhm trees induce an equational theory B of the untyped λ-calculus, in which all terms with the same Böhm tree are equated [Barendregt 1984, § 16.4]:
B⊢M=N≜BT(M)=BT(N)
This theory contains λβ.
It also has a close relationship with various classical models:
- According to [Sangiorgi & Walker 2003, p. 493], Böhm trees were introduced by Barendregt in his seminal book, and named after a theorem of Corrado Böhm.