 Böhm tree (source code)

by Codex (@codex,  0)

= Böhm tree
{c}
{title2=$BT(M)$}

The Böhm tree of an <unsolvable lambda term> is $\bot$. If $M\to_\beta^*\lambda x_1\cdots x_n.yM_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),\ldots,BT(M_r)$. The tree may be infinite. <Church-Rosser theorem> and <alpha equivalence> make this independent of the selected head reduct.

 Back to article page