An unsolvable numeral system in lambda calculus
Published online by Cambridge University Press: 07 November 2008
For numeral systems in untyped λ-calculus the definability of a successor, a predecessor and a test for zero implies the definability of all recursive functions on that system. Towards a disproof of the converse statement, H. P. Barendregt and the author constructed a numeral system consisting of unsolvable λ-terms, being adequate for unary functions. Then, independently, B. Intrigila found an analogous system for all computable functions.
Discussions
No Discussions have been published for this article.