 Finite Böhm approximant

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.