[Next]  [Previous]  [Up]

#### Problem # 3 [SOLVED]

Submitted by Richard Statman
Date: 1981
Statement. Does the range property hold for the theory ? Problem Origin. The problem was ﬁrst posed by Henk Barendregt .

[PRINT this PROBLEM]

Consider the least lambda theory which equates all unsolvable terms. Take any combinator . Prove that either , for all closed , , or there are inﬁnitely many closed , such that no two of terms are equated under . This problem, known as the range problem for , is stated as Conjecture 20.2.8 in [Barendregt, 1984].

Comments by Richard Statman: Different researchers have different takes on this problem. Mine are the following.

• If we can compute functions recursive in the jump of 0 then the range property holds. The word problem for is -complete but there is no good notion of -computability that allows the “computation” of those number theoretic function recursive in jump of 0. If one knew such a notion of computability then one could copy the usual recursion theoretic proof of the range property for beta-eta.
• If we can construct solvable Plotkin terms then the range property fails. Take a Kleene enumerator such that and is the -th solvable term. Then one can construct Plotkin terms and such that if then  This is for the beta-eta theory. If and can be constructed to be solvable then we would have a term with a range of size for .

Solution: A negative solution has been presented by A. Polonsky in 2010 and published in [Polonsky, 2012], who constructs a term F with a two-element range. In contrast, Intrigila and Statman [Intrigila and Statman, 2011] showed that the range property for Combinatory Logic is true.

##### References for # 3

[Barendregt, 1984]    Barendregt, H. (1984). The Lambda Calculus. Its Syntax and Semantics. North-Holland, second edition.

[Intrigila and Statman, 2011]    Intrigila, B. and Statman, R. (2011). Solution to the range problem for combinatory logic. Fundamenta Informaticae, 111(2):203–222.

[Polonsky, 2012]    Polonsky, A. (2012). The range property fails for H. Journal of Logic and Computation, 77(4):1195–1210.

[Next]  [Previous]  [Up]
Last modified: July 21, 2014