Solution to the Range Problem for Combinatory Logic

Abstract

The λ-theory ℋ is obtained from β-conversion by identifying all closed unsolvable terms (or, equivalently, terms without head normal form). The range problem for the theory ℋ asks whether a closed term has always (up to equality in ℋ) either an infinite range or a singleton range (that is, it is a constant function). Here we give a solution to a natural version of this problem, giving a positive answer for the theory ℋ restricted to Combinatory Logic. The method of proof applies also to the Lazy λ-Calculus.