Strict sequencing of partial numeral computations
ID: strict-sequencing-of-partial-numeral-computations
The term beta-reduces to for every Church numeral . 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.
New to topics? Read the docs here!