Finite Böhm approximant
= Finite Böhm approximant
A finite Böhm approximant is $\bot$ or a finite <lambda term> in the grammar $\lambda x_1\cdots x_n.yA_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 $\bot$; bottom reduction contracts $\bot N$ and $\lambda x.\bot$ to $\bot$. Its interpretation in the <graph model of lambda calculus> is included in that of the original term.