×

zbMATH — the first resource for mathematics

Constructive proofs of the range property in lambda calculus. (English) Zbl 0796.03020
The range property, conjectured in 1968 by Böhm, says that the range of a combinator \(F\), that is the set of all terms \(F A\) modulo \(\beta\)- convertibility, is either a singleton or an infinite set. This paper recalls first the classical (nonconstructive) proofs and then gives two constructive proofs. The first one adds to Böhm’s idea of using a fixed point the coding of lambda-terms by natural numbers. The second is based on Ershov numerations. This leads to a generalization of the range theorem due to Statman.

MSC:
03B40 Combinatory logic and lambda calculus
03D45 Theory of numerations, effectively presented structures
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Barendregt, H.P., The lambda calculus, its syntax and semantics, (), revised edition · Zbl 0467.03010
[2] Barendregt, H.P., Theoretical pearls: self-interpretation in lambda calculus, J. funct. programming, 1, 2, 229-234, (1991)
[3] Barendregt, H.P., Theoretical pearls: representing “undefined” in lambda calculus, J. funct. programming, 2, 3, 367-374, (1992) · Zbl 0816.03007
[4] Barendsen, E., Fixed-point theorems in lambda calculus and recursion theory, (1992), Dept. of Computer Science, Toernooiveld 1, 6525 ED Nijmegen The Netherlands, manuscript
[5] Böhm, C., Alcune proprietà delle forme β-η-normali nel λ-K-calcolo, No. 696, (1968), Pubblicazioni dell’Istituto per le Applicazioni del Calcolo Via del Policlinico 127, Roma
[6] Coppo, M.; Dezani-Ciancaglini, M.; della Rocca, S.Ronchi, (semi-) separability of finite sets of terms in Scott’s D∞-models of the λ-calculus, (), 142-164 · Zbl 0394.03021
[7] Ershov, Y., Theorie der numerierungen, Z. math. logik grundlag. math., Z. math. logik grundlag. math., Z. math. logik grundlag. math., 23, 289-371, (1977) · Zbl 0374.02028
[8] Plotkin, G., The λ-calculus is ω-incomplete, J. symbolic logic, 39, 313-317, (1974) · Zbl 0299.02029
[9] Rogers, H., Theory of recursive functions and effective computability, () · Zbl 0183.01401
[10] Visser, A., Numerations, λ-calculus and arithmetic, (), 259-284
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.