# Böhm tree

In the study of denotational semantics of the lambda calculus, Böhm trees, Lévy-Longo trees, and Berarducci trees are (potentially infinite) tree-like mathematical objects that capture the "meaning" of a term up to some set of "meaningless" terms.

## Motivation

A simple way to read the meaning of a computation is to consider it as a mechanical procedure consisting of a finite number of steps that, when completed, yields a result. In particular, considering the lambda calculus as a rewriting system, each beta reduction step is a rewrite step, and once there are no further beta reductions the term is in normal form. We could thus, naively following Church's suggestion, say the meaning of a term is its normal form, and that terms without a normal form are meaningless. For example the meanings of I = λx.x and I I are both I. This works for any strongly normalizing subset of the lambda calculus, such as a typed lambda calculus.
This naive assignment of meaning is however inadequate for the full lambda calculus. The term Ω =(λx.x x)(λx.x x) does not have a normal form, and similarly the term X=λx.xΩ does not have a normal form. But the application Ω (K I), where K denotes the standard lambda term λx.λy.x, reduces only to itself, whereas the application X (K I) reduces with normal order reduction to I, hence has a meaning. We thus see that not all non-normalizing terms are equivalent. We would like to say that Ω is less meaningful than X because applying X to a term can produce a result but applying Ω cannot.
Böhm trees may also be applied in the context of the infinitary lambda calculus, which includes infinitely large terms. In this context, the term N N, where N = λx.I(xx), reduces to both to I (I (...)) and Ω, hence there are also issues with confluence of normalization.

## Sets of meaningless terms

The general construction is parameterized by a set $U$ of meaningless terms, which is required to satisfy the following axioms:
* Root-activeness: Every root-active term is in $U$. A term $M$ is root-active if for all $M{\stackrel {*}{\to }}N$ there exists a redex $(\lambda x.P)Q$ such that $N{\stackrel {*}{\to }}(\lambda x.P)Q$.
* Closure under β-reduction: For all $M\in U$, if $M{\stackrel {*}{\to }}N$ then $N\in U$.
* Closure under substitution: For all $M\in U$ and substitutions $\sigma$, $M\sigma \in U$.
* Overlap: For all $\lambda x.M\in U$, $(\lambda x.M)N\in U$ .
* Indiscernibility: For all $M,N$, if $N$ can be obtained from $M$ by replacing a set of pairwise disjoint subterms in $U$ with other terms of $U$, then $M\in U$ if and only if $N\in U$.
* Closure under β-expansion. For all $N\in U$, if $M{\stackrel {*}{\to }}N$, then $M\in U$. Some definitions leave this out, but it is useful.
There are infinitely many sets of meaningless terms, but the ones most common in the literature are:
* The set of terms without head normal form
* The set of terms without weak head normal form
* The set of root-active terms, i.e. the terms without top normal form or root normal form. Since root-activeness is assumed, this is the smallest set of meaningless terms.
Note that Ω is root-active and therefore $\mathbf {\Omega } \in U$ for every set of meaningless terms $U$.

## λ⊥-terms

The set of λ-terms with ⊥ (abbreviated λ⊥-terms) is defined coinductively by the grammar $M=\bot \mid x\mid (\lambda x.M)\mid (MM)$. This corresponds to the standard infinitary lambda calculus plus terms containing $\bot$. Beta-reduction on this set is defined in the standard way. Given a set of meaningless terms $U$, we also define a reduction to bottom: if $M[\bot \mapsto \mathbf {\Omega } ]\in U$ and $M\neq \bot$, then $M\to \bot$. The λ⊥-terms are then considered as a rewriting system with these two rules; thanks to the definition of meaningless terms this rewriting system is confluent and normalizing.
The Böhm-like "tree" for a term may then be obtained as the normal form of the term in this system, possibly in an infinitary "in the limit" sense if the term expands infinitely.

### Böhm trees

The Böhm trees are obtained by considering the λ⊥-terms where the set of meaningless terms consists of those without head normal form. More explicitly, the Böhm tree BT(M) of a lambda term M can be computed as follows:
* BT(M) is $\bot$, if M has no head normal form
* $\mathrm {BT} (M)=\lambda x_{1}.\lambda x_{2}.\ldots \lambda x_{n}.y\mathrm {BT} (M_{1})\ldots \mathrm {BT} (M_{m})$, if $M$ reduces in a finite number of steps to the head normal form $\lambda x_{1}.\lambda x_{2}.\ldots \lambda x_{n}.yM_{1}\ldots M_{m}$
For example, BT(Ω)=⊥, BT(I)=I, and BT(λx.xΩ)=λx.x⊥.
Determining whether a term has a head normal form is an undecidable problem. Barendregt introduced a notion of an "effective" Böhm tree that is computable, with the only difference being that terms with no head normal form are not marked with $\bot$.
Note that computing the Böhm tree is similar to finding a normal form for M. If M has a normal form, the Böhm tree is finite and has a simple correspondence to the normal form. If M does not have a normal form, normalization may "grow" some subtrees infinitely, or it may get "stuck in a loop" attempting to produce a result for part of the tree, which produce infinitary trees and meaningless terms respectively. Since the Böhm tree may be infinite the procedure should be understood as being applied co-recursively or as taking the limit of an infinite series of approximations.

### Lévy-Longo trees

The Lévy-Longo trees are obtained by considering the λ⊥-terms where the set of meaningless terms consists of those without weak head normal form. More explicitly, the Lévy-Longo tree LLT(M) of a lambda term M can be computed as follows:
* LLT(M) is $\bot$, if M has no weak head normal form.
* If $M$ reduces to the weak head normal form $yM_{1}\ldots M_{m}$, then $\mathrm {LLT} (M)=y\mathrm {LLT} (M_{1})\ldots \mathrm {LLT} (M_{m})$.
* If $M$ reduces to the weak head normal form $\lambda x.N$, then $\mathrm {LLT} (M)=\lambda x.\mathrm {LLT} (N)$/

### Berarducci trees

The Berarducci trees are obtained by considering the λ⊥-terms where the set of meaningless terms consists of the root-active terms. More explicitly, the Berarducci tree BerT(M) of a lambda term M can be computed as follows:
* BerT(M) is $\bot$, if M is root-active.
* If $M$ reduces to a term $\lambda x.N$, then $\mathrm {BerT} (M)=\lambda x.\mathrm {BerT} (N)$.
* If $M$ reduces to a term $NP$ where $N$ does not reduce to any abstraction $\lambda x.Q$, then $\mathrm {BerT} (M)=\mathrm {BerT} (N)\mathrm {BerT} (P)$.