Enumerators of lambda terms are reducing constructively Original Research Article

A closed λ-term E is called an enumerator if ∀M ϵ /gL/dg /gTn ϵ N E/drn/dl = β M. Here Λ° is the set of closed λ-terms, N is the set of natural numbers and the /drn/dl are the Church numerals λfx./tfnx. Such an E is called reducing if moreover ∀M ϵ /gL/dg /gTn ϵ N E/drn/dl /a/gb M. In 1983 I conjectured that every enumerator is reducing. An ingenious recursion theoretic proof of this conjecture by Statman is presented in Barendregt (1992). The proof is not intuitionistically valid, however. Dirk van Dalen has encouraged me to find intuitionistic proofs whenever possible. In the lambda calculus this is usually not difficult. In this paper an intuitionistic version of Statmans proof will be given. It took me somewhat longer to find it than in other cases.