Lambda-definable function

A function $g:{\mathbb{N}}^k\to \mathbb{N}$ is lambda-definable when some combinator $G$ satisfiesfor every tuple of natural numbers.

The successor function is lambda-defined on Church numerals bybecause $\mathrm{Succ}{c}_n{\equiv }_{\beta }{c}_{n+1}$.

Using a fixed-point combinator, Church Boolean conditionals, a zero test, and a predecessor term, lambda-definable $g$ and $h$ giveNormal-order beta reduction evaluates only the selected conditional branch, so this term implements primitive recursion on Church numerals.

A partial function is lambda-definable when one lambda term maps Church numerals in its domain to the numeral of the output and produces no numeral on inputs outside its domain.

For a lambda-definable partial $g(\mathbf{x},n)$, a fixed-point search term tests $n=0,1,2,\dots$ and returns the first $n$ for which $g(\mathbf{x},n)=0$. If no such value is reached, reduction produces no Church numeral. This realizes unbounded minimization and therefore makes every partial recursive function lambda-definable.