Böhm tree

A Böhm tree is a (potentially infinite) tree-like mathematical object that can be used to provide denotational semantics (the "meaning") for terms of the lambda calculus (and programming languages in general by using translations to lambda calculus). It is named after Corrado Böhm.

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. 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 $π$ ; 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 (described by) a lambda term should be the normal form it reduces to, and that terms which do not have a normal form are meaningless.^[1] 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 (if such a thing existed), 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 (possibly infinite) directed acyclic graph having some vertices labelled with lambda terms of the form λx₁.λx₂...λx_n.y (n may be 0), where exactly one vertex (the "root") 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
(λx A) B is A[x:=B] (see below)
A B (where the label on the root node of A has no binders) is a tree obtained from A by adding B as a new rightmost child of the root node
On a vertex with label λx₁...λx_n.y, y occurs free at that vertex if λy does not appear in the label of that vertex or any of its ancestors
The capture-avoiding substitution A[x:=B] is:
1. (λx.A)[x:=B] is λx.A
2. (λy.A)[x:=B] (x and y are different) is λz.A[y:=z][x:=B] where z is not in A and not free in B (it may remain y if y is not free in B)
3. If the root node of A has the label x and children C₁...C_n, A[x:=B] is ((B C₁[x:=B]) C₂[x:=B])...C_n[x:=B]
4. If the root node of A is not labeled with x (it could be unlabeled), A[x:=B] is ((A C₁[x:=B]) C₂[x:=B])...C_n[x:=B]

The Böhm tree BT(M) of a lambda term M can then be "computed" as follows.^{[note 1]}

BT(x) is a single node labelled with x
BT(λx.M) is λx.BT(M)
BT(M N) is BT(M)BT(N)

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( $Ω I$ ), which corresponds to a single unlabeled root node.

Similarly, the procedure does not terminate for BT( $λ x . x Ω$ ), but the tree is nonetheless different from the former examples.

Notes

↑ The presentation given here avoids the use of solvability or head normal forms, but is otherwise that of an "effective" Böhm tree.^[2]

References

↑ Church, Alonzo (1941). The calculi of lambda-conversion. Princeton: Princeton University Press. p. 15. ISBN 0691083940.
↑ Barendregt, Henk P. The Lambda Calculus : Its Syntax and Semantics. London: College Publications. pp. 219–221,486–487. ISBN 9781848900660.

Gérard Huet, H. Laulhère (Sep 1997). "Finite-state Transducers as Regular Böhm Trees". In M. Abadi and T. Ito. Theoretical Aspects of Computer Software (PDF). LNCS. 1281. Springer. pp. 604–610.
Gérard Huet (1998). "Regular Böhm Trees" (PDF). Math. Struct. in Comp. Science. 8: 671–680.

This article is issued from Wikipedia - version of the 7/18/2014. The text is available under the Creative Commons Attribution/Share Alike but additional terms may apply for the media files.