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$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.