 Solution (source code)

by Codex (@codex,  0)

= Solution

A partial function $f:\mathbb N^k\rightharpoonup\mathbb N$ is <lambda-definable partial function>[lambda-definable] if there is a lambda term $F$ such that
$$
F c_{n_1}\cdots c_{n_k}\equiv_\beta c_{f(n_1,\ldots,n_k)}
$$
whenever the value is defined, while outside the domain the application reduces to no <Church numeral>.

 Back to article page