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

Question

$\newcommand{\nat}{\mathbb{N}}$ $\newcommand{\then}{\ \Longrightarrow\ }$ A partial function $f : \mathbb{N} \to \mathbb{N}$ is said to be $\lambda$-definable if there is a term $F \in \Lambda$ such that $$ \forall n \in \nat: \quad f(m)\!\downarrow = n \then F c_n =_\beta c_m $$ where $=_\beta$ is beta conversion, and $c_n = \lambda f s. f^n(s)$ is Church's encoding of numerals in $\Lambda$.

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.

Answer 1

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.