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.
This naive assignment of meaning is however inadequate for the full lambda calculus.
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.
This corresponds to the standard infinitary lambda calculus plus terms containing
The Böhm trees are obtained by considering the λ⊥-terms where the set of meaningless terms consists of those without head normal form.
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
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.
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 Berarducci tree BerT(M) of a lambda term M can be computed as follows:[10]