The word problem for Smullyan's lark combinator is decidable (Q1114668)

Smullyan's ``lark combinator'' L (Curry's BWB) is specified by the reduction rule Lxy\(\to x(yy)\). LL defines the paradoxical combinator Y. The author shows that several other interesting combinators can be defined in terms of L only. The main part of the paper involves showing that the problem of deciding whether two applicative combinators of L are equal is solvable.