Submitted by Richard Statman
Statement. Basis Decision Problem.
The basis decision problem, originally stated in [Statman, 1993], is to decide whether a given ﬁnite set of proper combinators is combinatorially complete. (A proper combinator [Barendregt, 1984, p. 184] is one of the form , where contains no lambda, and .) It follows from Theorem 4 in [Statman, 1986] that the problem is undecidable for ﬁnite sets of normal (possibly improper) combinators. A good solution would be an abstraction algorithm, parameterized by a given set of combinators, which returned an error message on non-bases. Broda and Damas have proved that in the linear case the problem is decidable [Broda and Damas, 1997].