Head normal form
= Head normal form
A <lambda term> has head normal form when it beta-reduces to a term $\lambda x_1\cdots x_k.\,yM_1\cdots M_r$ with a variable $y$ at the head. The argument terms need not be in <beta-normal form>. A term with no head normal form cannot be beta-equivalent to a <Church numeral>.