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:
`s/\(S([^()])([^()])([^()])\)/($1($3($2$3)))/;
s/\(K([^()])([^()])\)/$1/;
s/\(I([^()])\)/$1/;
`

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)` to

`(SK)K` (UPDATE: or, better,

`(((K((SK)K))K)x)` to

`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`.)

Comment onRe^2: Turing completeness and regular expressionsSelectorDownloadCode