Constructive proofs of the range property in lambda calculus (Q1314345): Difference between revisions

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.