Probably not. You should be able to evaluate an SK-expression from the bottom up (instead of top-down) if it is fully parenthesized. Something like this:
i.e., always evaluate the "innermost" expression, which will be the one without parentheses. I think something like this may work though I've not tested it.
I think that this does not work. For example, it does not reduce ((K((SK)K))K)
(UPDATE: or, better, (((K((SK)K))K)x)
Set up a recursive substitution to recognise functional equivalence of combinators (so that it could identify ``SKK and ``SKS as functionally equivalent).
Equivalent to the halting problem in the general case. Let an SK-expression simulate a Turing machine M on input x. Is it equivalent to the SK-expression that always returns true?
Yes, that's what I thought; but Stenlund
provides a finite system of equations for deciding—well, something. I thought that it was functional equivalence, but I must have misunderstood. I'll look it up when I've got my copy. (Incidentally, the combinator is KK