# Is every total computable function definable by a normalizing lambda term?


It is well-known that every partial computable function is $\lambda$-definable. However, whenever a particular recursive definition of the function $f$ makes use of the $\mu$-operator (minimization), then the $\lambda$-term corresponding to that definition will contain a fixed point combinator, hence not be normalizing in general.

On the other hand, large classes of total recursive functions can be $\lambda$-defined by normalizing terms. For example, Girard showed that every function which is provably total in higher-order arithmetic can be defined by a term typable in the system $F\omega$, and every term in this system is normalizing.

Yes, you can actually encode all computable functions by normalizable terms since it is always possible to turn a term into a normal form which computes the same function on Church's numerals. We just need to put $n (\lambda x. x)$ in front of every lambda in your term, where $n$ is the argument of the function. Formally, define function $r$ as follows: \begin{align*} r(n, x) & = x \\ r(n, \lambda x. t) & = n (\lambda x. x) (\lambda x. r(n, t)) \\ r(n, f a) & = r(n, f) r(n, a) \end{align*} Now, if we have a term $F$, then we can define $F'$ as $\lambda n. r(n, F n)$. Clearly, $F'$ is a normal form and, for every natural number $n$, terms $F c_n$ and $F' c_n$ are $\beta$-equivalent.