 Böhm tree

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.