Submitted by Richard Statman
Statement. Word problem for combinators of orders less than 3.
The word problem for a set of combinators is to determine if two applicative combinations of members of are -equal. A proper combinator , with reduction rule , where is an applicative combination of is said to have order . We ask if the word problem for all proper combinators of orders less than 3 is decidable. The problem was originally proposed in [Statman, 1989].
Comments by Richard Statman: It is easy to see that the word problem for combinators of order 1 is decidable. More can be shown [Statman, 1988a]. In [Statman, 1989] it is shown that the word problem for Smullyan’s Lark combinator is solvable even though ﬁxed points always exist. In [Statman, 2000] we prove that the word problem for all co-compositors and ﬁnitely many instances of (ﬁnitely many) compositors is solvable. We have been led to the conjecture: The word problem for all proper combinators of order less than 3 (taken together in one system) is decidable. Some combinator of order 3 or more is necessary for a basis of proper combinators [Statman, 1986] but slightly beyond order 2 [Statman, 1988b] leads to undecidabilty.
Added “in proof”: This problem also occurs in the RTA LOOP as problem number 96.