In the study of denotational semantics of the lambda calculus, Böhm trees,^{[lower-alpha 1]} Lévy-Longo trees,^{[1][2][lower-alpha 2]} and Berarducci trees^[3] 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,^[4] 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.

In the infinitary lambda calculus, 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.^[5]

Sets of meaningless terms

We define a set ${\displaystyle U}$ of meaningless terms as follows:^[6][7]

• Root-activeness: Every root-active term is in ${\displaystyle U}$. A term ${\displaystyle M}$ is root-active if for all ${\displaystyle M{\stackrel {*}{\to }}N}$ there exists a redex ${\displaystyle (\lambda x.P)Q}$ such that ${\displaystyle N{\stackrel {*}{\to }}(\lambda x.P)Q}$.
• Closure under β-reduction: For all ${\displaystyle M\in U}$, if ${\displaystyle M{\stackrel {*}{\to }}N}$ then ${\displaystyle N\in U}$.
• Closure under substitution: For all ${\displaystyle M\in U}$ and substitutions ${\displaystyle \sigma }$, ${\displaystyle M\sigma \in U}$.
• Overlap: For all ${\displaystyle \lambda x.M\in U}$, ${\displaystyle (\lambda x.M)N\in U}$ .
• Indiscernibility: For all ${\displaystyle M,N}$, if ${\displaystyle N}$ can be obtained from ${\displaystyle M}$ by replacing a set of pairwise disjoint subterms in ${\displaystyle U}$ with other terms of ${\displaystyle U}$, then ${\displaystyle M\in U}$ if and only if ${\displaystyle N\in U}$.
• Closure under β-expansion. For all ${\displaystyle N\in U}$, if ${\displaystyle M{\stackrel {*}{\to }}N}$, then ${\displaystyle M\in U}$. Some definitions leave this out, but it is useful.^[8]

There are infinitely many sets of meaningless terms, but the ones most common in the literature are:^[9]

• 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 ${\displaystyle \mathbf {\Omega } \in U}$ for every set of meaningless terms ${\displaystyle U}$.

λ⊥-terms

The set of λ-terms with ⊥ (abbreviated λ⊥-terms) is defined coinductively by the grammar ${\displaystyle M=\bot \mid x\mid (\lambda x.M)\mid (MM)}$. This corresponds to the standard infinitary lambda calculus plus terms containing ${\displaystyle \bot }$. Beta-reduction on this set is defined in the standard way. Given a set of meaningless terms ${\displaystyle U}$, we also define a reduction to bottom: if ${\displaystyle M[\bot \mapsto \mathbf {\Omega } ]\in U}$ and ${\displaystyle M\neq \bot }$, then ${\displaystyle 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.^[7]

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.

Notes

References