8
$\begingroup$

Every computable (total) function $f : \mathbb{N} \to \mathbb{N}$ is definable in untyped pure lambda calculus in the sense that there is a term $F$ such that, for every Church's numeral $c_n = \lambda s z. s^n(z)$, the term $F c_n$ normalizes to $c_{f(n)}$. Let us say that a term $F$ is strongly total if the term $F c_n$ is strongly normalizable for every Church's numeral $c_n$. Is every total computable function definable by a strongly total term? This question is similar to this one, but the trick that I described in my answer does not apply in this case since it produces terms which are not strongly total and I don't see how it can be fixed.

$\endgroup$

0

You must log in to answer this question.

Browse other questions tagged .