= Strict sequencing of partial numeral computations
{title2=$\mathrm{Force}=\lambda n.\lambda k.n(\lambda z.z)k$}
The term $\mathrm{Force}\,c_m\,K$ beta-reduces to $K$ for every <Church numeral> $c_m$. If its first argument has no <head normal form>, the whole application has no head normal form. Nesting this operation forces each represented inner computation before applying an outer function, implementing <composition of partial functions> even when an outer projection would discard an argument. The same guard makes <lambda definition of primitive recursion> strict in the preceding recursive value.
Back to article page
