Lambda definition of unbounded minimization
= Lambda definition of unbounded minimization
For a lambda-definable partial $g(\mathbf x,n)$, a fixed-point search term tests $n=0,1,2,\ldots$ 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.