In the study of denotational semantics of the lambda calculus, Böhm trees, Lévy-Longo trees,[1] [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.
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.
We define a set
U
U
M
M\stackrel{*}{\to}N
(λx.P)Q
N\stackrel{*}{\to}(λx.P)Q
M\inU
M\stackrel{*}{\to}N
N\inU
M\inU
\sigma
M\sigma\inU
λx.M\inU
(λx.M)N\inU
M,N
N
M
U
U
M\inU
N\inU
N\inU
M\stackrel{*}{\to}N
M\inU
There are infinitely many sets of meaningless terms, but the ones most common in the literature are:
Note that '''Ω''' is root-active and therefore
\Omega\inU
U
The set of λ-terms with ⊥ (abbreviated λ⊥-terms) is defined coinductively by the grammar
M=\bot\midx\mid(λx.M)\mid(MM)
\bot
U
M[\bot\mapsto\Omega]\inU
M ≠ \bot
M\to\bot
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.
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:
\bot
BT(M)=λx1.λx2.\ldotsλxn.yBT(M1)\ldotsBT(Mm)
M
λx1.λx2.\ldotsλxn.yM1\ldotsMm
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.
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:
\bot
M
yM1\ldotsMm
LLT(M)=yLLT(M1)\ldotsLLT(Mm)
M
λx.N
LLT(M)=λx.LLT(N)
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:
\bot
M
λx.N
BerT(M)=λx.BerT(N)
M
NP
N
λx.Q
BerT(M)=BerT(N)BerT(P)