Böhm tree

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,{{cite book|last=Church|first=Alonzo|title=The calculi of lambda-conversion|year=1941|publisher=Princeton University Press|isbn=0691083940|page=15}} 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.

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.{{sfn|Severi|de Vries|2011|p=1}}

The general construction is parameterized by a set $U$ of meaningless terms, which is required to satisfy the following axioms:{{cite book |last1=Kennaway |first1=Richard |last2=van Oostrom |first2=Vincent |last3=de Vries |first3=Fer-Jan |title=Algebraic and Logic Programming |chapter=Meaningless terms in rewriting |series=Lecture Notes in Computer Science |date=1996 |volume=1139 |pages=254–268 |doi=10.1007/3-540-61735-3_17|isbn=978-3-540-61735-8 |citeseerx=10.1.1.37.3616}}{{sfn|Severi|de Vries|2011|p=5}}

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

There are infinitely many sets of meaningless terms, but the ones most common in the literature are:{{sfn|Severi|de Vries|2011|p=2}}

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

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

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:{{sfn|Severi|de Vries|2011|p=6}}

1. BT(M) is $\backslash bot$, if M has no head normal form
2. $\backslash mathrm\{BT\}(M)\; =\; \backslash lambda\; x\_1.\backslash lambda\; x\_2.\backslash ldots\backslash lambda\; x\_n.y\; \backslash mathrm\{BT\}(M\_1)\; \backslash ldots\; \backslash mathrm\{BT\}(M\_m)$, if $M$ reduces in a finite number of steps to the head normal form $\backslash lambda\; x\_1.\backslash lambda\; x\_2.\backslash ldots\backslash lambda\; x\_n.y\; M\_1\; \backslash ldots\; M\_m$

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 $\backslash bot$.{{cite book|last=Barendregt|first=Henk P.|title=The Lambda Calculus : Its Syntax and Semantics|year=2012 |publisher=College Publications|location=London|isbn=9781848900660|pages=219–221}}

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:{{sfn|Severi|de Vries|2011|p=6}}

1. LLT(M) is $\backslash bot$, if M has no weak head normal form.
2. If $M$ reduces to the weak head normal form $y\; M\_1\; \backslash ldots\; M\_m$, then $\backslash mathrm\{LLT\}(M)\; =\; y\; \backslash mathrm\{LLT\}(M\_1)\; \backslash ldots\; \backslash mathrm\{LLT\}(M\_m)$.
3. If $M$ reduces to the weak head normal form $\backslash lambda\; x.N$, then $\backslash mathrm\{LLT\}(M)\; =\; \backslash lambda\; x.\backslash mathrm\{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:{{sfn|Severi|de Vries|2011|p=6}}

1. BerT(M) is $\backslash bot$, if M is root-active.
2. If $M$ reduces to a term $\backslash lambda\; x.N$, then $\backslash mathrm\{BerT\}(M)\; =\; \backslash lambda\; x.\backslash mathrm\{BerT\}(N)$.
3. If $M$ reduces to a term $N\; P$ where $N$ does not reduce to any abstraction $\backslash lambda\; x.\; Q$, then $\backslash mathrm\{BerT\}(M)\; =\; \backslash mathrm\{BerT\}(N)\; \backslash mathrm\{BerT\}(P)$.

{{Notelist}}

{{Reflist}}

{{refbegin}}

• {{cite book |first1=Gérard |last1=Huet |first2=H. |last2=Laulhère |chapter=Finite-state Transducers as Regular Böhm Trees |title=Theoretical Aspects of Computer Software |date=1997| volume=1281| pages=604–610| publisher=Springer |editor1-first=M. |editor1-last=Abadi |editor2-first=T. |editor2-last=Ito |series=LNCS |chapter-url=http://pauillac.inria.fr/~huet/PUBLIC/trans6.pdf |doi=10.1007/BFb0014570 |isbn=978-3-540-69530-1 |citeseerx=10.1.1.110.7910}}
• {{cite journal| author=Gérard Huet| title=Regular Böhm Trees| journal=Math. Struct. In Comp. Science| year=1998| volume=8 |issue=6 | pages=671–680| url=http://pauillac.inria.fr/~huet/PUBLIC/RBT2.pdf |doi=10.1017/S0960129598002643 |citeseerx=10.1.1.123.475| s2cid=15752309}}
• {{cite thesis |last=Ong |first=C.-H. Luke|date=31 May 1988|title=The Lazy Lambda Calculus: An Investigation into the Foundations of Functional Programming |type=PhD|publisher=University of London|oclc= 31204528|url=https://spiral.imperial.ac.uk/bitstream/10044/1/47211/2/Ong-CHL-1988-PhD-Thesis.pdf|access-date=23 September 2022}}
• {{cite book |last1=Sangiorgi |first1=Davide |last2=Walker |first2=David |title=The Pi-Calculus: A Theory of Mobile Processes |date=16 October 2003 |publisher=Cambridge University Press |isbn=978-0-521-54327-9 |language=en}}
• {{cite book |last1=Barendregt |first1=Henk P. |title=Handbook of Mathematical Logic |chapter=The Type Free Lambda Calculus |series=Studies in Logic and the Foundations of Mathematics |date=1977 |volume=90 |pages=1091–1132 |doi=10.1016/S0049-237X(08)71129-7|isbn=9780444863881 |s2cid=25828519 |hdl=2066/17225 |hdl-access=free }}
• {{cite book |last1=Severi |first1=Paula |last2=de Vries |first2=Fer-Jan |title=Logic, Language, Information and Computation |chapter=Decomposing the Lattice of Meaningless Sets in the Infinitary Lambda Calculus |series=Lecture Notes in Computer Science |date=2011 |volume=6642 |pages=210–227 |doi=10.1007/978-3-642-20920-8_22 |isbn=978-3-642-20919-2 |chapter-url=https://www.cs.le.ac.uk/people/fdv1/fdv1/Distribution/wollic2011.pdf |access-date=23 September 2022}}

{{refend}}

{{DEFAULTSORT:Bohm Tree}}

Category:Lambda calculus