On the word problem for combinators

In 1936 Alonzo Church observed that the word problem for combinators is undecidable. He used his student Kleene's representation of partial recursive functions as lambda terms. This illustrates very well the point that word problems are good problems in the sense that a solution either way - decidable or undecidable - can give useful information. In particular, this undecidability proof shows us how to program arbitrary partial recursive functions as combinators. I never thought that this result was the end of the story for combinators. In particular, it leaves open the possibility that the unsolvable problem can be approximated by solvable ones. It also says nothing about word problems for interesting fragments i.e., sets of combinators not combinatorially complete. Perhaps the most famous subproblem is the problem for S terms. Recently, Waldmann has made significant progress on this problem. Prior, we solved the word problem for the Lark, a relative of S. Similar solutions can be given for the Owl (S * ) and Turing's bird U. Familiar decidable fragments include linear combinators and various sorts of typed combinators. Here we would like to consider several fragments of much greater scope. We shall present several theorems and an open problem.