8
$\begingroup$

$\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.

$\endgroup$

1 Answer 1

7
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.