Böhm tree ($BT(M)$)

The Böhm tree of an unsolvable lambda term is $\perp$. If $M{\to }_{\beta }^{\ast }\lambda x_1\cdots x_n.y{M}_1\cdots M_r$ is a head normal form, its Böhm tree has root label $\lambda x_1\cdots x_n.y$ and ordered children $BT(M_1),\dots ,BT(M_r)$. The tree may be infinite. Church-Rosser theorem and alpha equivalence make this independent of the selected head reduct.

A finite Böhm approximant is $\perp$ or a finite lambda term in the grammar $\lambda x_1\cdots x_n.y{A}_1\cdots A_r$, obtained by pruning a Böhm tree. Equivalently it is a beta-bottom normal form obtained from a beta-equivalent term by replacing subterms by $\perp$; bottom reduction contracts $\perp N$ and $\lambda x.\perp$ to $\perp$. Its interpretation in the graph model of lambda calculus is included in that of the original term.

A Böhm transformation is a finite composition of capture-avoiding substitutions and lambda applications to chosen auxiliary terms. It can extract a finite-address subtree of a Böhm tree as a substitution instance of the corresponding argument term.

For a finite path in a Böhm tree, choose $q$ at least the head arity at every preceding node. Replace relevant variables by $U_q=\lambda z_1\cdots z_{q}w.w{z}_1\cdots z_q$. After exposing each node, supply its initial bound variables with $U_q$, pad its $m$ arguments to $q$, and apply the projection $\lambda z_1\cdots z_q.z_i$ selecting the next child. Each step returns that child with accumulated substitutions, so iteration reaches a substitution instance of the chosen subtree. Tupling preserves all children until selection, even when the same variable occurs at several nodes.

Two distinct closed lambda terms in normal form for both beta reduction and eta conversion admit a separating context that maps them respectively to the two Church Booleans. Finite Böhm trees and the Böhm-out lemma isolate their first genuine head disagreement. The qualification about eta conversion matters: distinct beta-normal forms that are eta-equivalent cannot be separated this way.