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. This interpretation is inadequate, however, for procedures that do not terminate after a finite number of steps, but nonetheless have an intuitive meaning. Consider, for example, a procedure for computing the decimal expansion of pi|; if implemented appropriately, it can provide partial output as it "runs", and this ongoing output is a natural way to assign meaning to the computation. This is in contrast to, say, a program that loops infinitely without ever providing output. These two procedures have very different intuitive meanings. Since a computation described using lambda calculus is the process of reducing a lambda term to its normal form, this normal form itself is the result of the computation, and the entire process may be considered as "evaluating" the original term. For this reason Church's original suggestion was that the meaning of the computation a lambda term should be the normal form it reduces to, and that terms which do not have a normal form are meaningless. This suffers exactly the inadequacy described above. Extending the analogy, however, if "trying" to reduce a term to its normal form would give "in the limit" an infinitely long lambda term, that object could be considered this result. No such term exists in the lambda calculus, of course, and so Böhm trees are the objects used in this place.
Informal definition
A Böhm-like tree is a directed acyclic graph having some vertices labelled with lambda terms of the form λx1.λx2...λxn.y, where exactly onevertex has no parent, all other vertices have exactly one parent, every vertex has a finite number of children, and every unlabeled vertex has no children. Let us have the following notions for Böhm-like trees A, B:
λx.A is A with λx. prepended to the label at its root
B is A
AB is a tree obtained from A by adding B as a new rightmost child of the root node
On a vertex with label λx1...λxn.y, y occurs free at that vertex if λy does not appear in the label of that vertex or any of its ancestors
# If the root node of A has the label x and children C1...Cn, A is...Cn
# If the root node of A is not labeled with x, A is...Cn
The Böhm tree BT of a lambda term M can then be "computed" as follows.
BT is a single node labelled with x
BT is λx.BT
BT is BTBT
Note that this procedure implies 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, the procedure may "grow" some subtrees infinitely, or it may get "stuck in a loop" attempting to produce a result for part of the tree, which is the source of unlabeled leaf nodes. For this reason the procedure should be understood as applying all steps in parallel, with the resulting tree given "in the limit" of applying the procedure infinitely. For example, the procedure does not grow trees at all for BT or for BT, which corresponds to a single unlabeled root node. Similarly, the procedure does not terminate for BT, but the tree is nonetheless different from the former examples.
