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.


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.