Abstract
In this note we work with untyped lambda terms under β-conversion and consider the possibility of extending Böhm’s theorem to infinite RE (recursively enumerable) sets. Böhm’s theorem fails in general for such sets \(\mathcal{V}\) even if it holds for all finite subsets of it. It turns out that generalizing Böhm’s theorem to infinite sets involves three other superficially unrelated notions; namely, Church’s delta, numeral systems, and Ershov morphisms. Our principal result is that Böhm’s theorem holds for an infinite RE set \(\mathcal{V}\) closed under beta conversion iff \(\mathcal{V}\) can be endowed with the structure of a numeral system with predecessor iff there is a Church delta (conditional) for \(\mathcal{V}\) iff every Ershov morphism with domain \(\mathcal{V}\) can be represented by a lambda term.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Barendregt, H.: The Lambda Calculus, its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics, vol. 103. North-Holland Publishing Co., Amsterdam (1984) (revised edition)
Barendsen, E.: Theoretical pearls: an unsolvable numeral system in lambda calculus. J. Funct. Programming 1(3), 367–372 (1991)
Böhm, C.: Alcune proprietà delle forme β n -normali nel λK-calcolo. Technical Report 696, Istituto per le Applicazioni del Calcolo (IAC), Viale del Policlinico 137, 00161 Rome, Italy (1968)
Böhm, C., Dezani-Ciancaglini, M., Peretti, P., Ronchi, S.: A discrimination algorithm inside λβ-calculus. Theoret. Comput. Sci. 8(3), 271–291 (1979)
Coppo, M., Dezani-Ciancaglini, M., Ronchi, S. (Semi-)separability of finite sets of terms in Scott’s D ∞-models of the λ-calculus. In: Ausiello, G., Böhm, C. (eds.) ICALP 1978. LNCS, vol. 62, pp. 142–164. Springer, Heidelberg (1978)
Ershov, Y.L.: Theorie der Numerierungen I, II, III. Zeitschr. math. Logik Grundl. Math. 19, 289–388 (1973); 21, 473-584 (1975); 23, 289–371 (1977)
Intrigila, B.: Some results on numerical systems in λ-calculus. Notre Dame J. Formal Logic 35(4), 523–541 (1994)
Jacopini, G.: A condition for identifying two elements of whatever model of combinatory logic. In: Böhm, C. (ed.) Lambda-Calculus and Computer Science Theory. LNCS, vol. 37, pp. 213–219. Springer, Heidelberg (1975)
Ronchi della Rocca, S.: Discriminability of infinite sets of terms in the D ∞-models of the λ-calculus. In: Astesiano, E., Böhm, C. (eds.) CAAP 1981. LNCS, vol. 112, pp. 350–364. Springer, Heidelberg (1981)
Statman, R.: Morphisms and partitions of V-sets. In: Gottlob, G., Grandjean, E., Seyr, K. (eds.) CSL 1998. LNCS, vol. 1584, pp. 313–322. Springer, Heidelberg (1999)
Statman, R., Barendregt, H.: Applications of Plotkin-terms: partitions and morphisms for closed terms. J. Funct. Programming 9(5), 565–575 (1999)
Visser, A.: Numerations, lambda calculus, and arithmetic, In: [?], pp. 259-284 (1980)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Statman, R., Barendregt, H. (2005). Böhm’s Theorem, Church’s Delta, Numeral Systems, and Ershov Morphisms. In: Middeldorp, A., van Oostrom, V., van Raamsdonk, F., de Vrijer, R. (eds) Processes, Terms and Cycles: Steps on the Road to Infinity. Lecture Notes in Computer Science, vol 3838. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11601548_5
Download citation
DOI: https://doi.org/10.1007/11601548_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-30911-6
Online ISBN: 978-3-540-32425-6
eBook Packages: Computer ScienceComputer Science (R0)