Is combinatory strong reduction equivalent to lambda beta-eta reduction?

Question

I'm familiar with the correspondence between combinatory logic and $\lambda$-calculus at equality level, ie $=_{\beta\eta}$ corresponds to $=_s$ (the equivalence relation generated by strong reduction) and that there is also a combinatory equality $=_{C\beta}$ corresponding to $=_\beta$ in $\lambda$.

However, I'm having trouble understanding what happens at reduction level. In particular, is it true that Curry's strong reduction corresponds to $\rightarrow_{\beta\eta}$? For instance, could we use strong reduction to "evaluate" (up to $\beta\eta$) $\lambda$-terms? Also, if I understand correctly, is it even harder to come up with a combinatory reduction equivalent to $\rightarrow_\beta$?

Answer 1

The answer to the second question is yes, beta-reduction is harder to imitate than beta-eta-reduction. There is an article by J P Seldin in "Theoretical Computer Science" (2011) I think that discusses the problems to which beta-reduction gives rise.

As to the question, "could we use strong reduction to evaluation lambda terms?", the correspondence is not as neat as you might wish. There is a mapping called the H-transformation that takes lambda terms to combinatory terms and which preserves the relation "reduces to", but it is not one-to-one and therefore not invertible. So if you start with a lambda term M and find its image H(M) under the H-transformation and you can reduce H(M) to a normal form, you will know that M also has a normal form, but it may not be entirely easy to find it. In the other direction, there is a mapping called the lambda-transformation that takes combinatory terms to lambda terms but it is not onto and is not the inverse of the H-transformation. It also does not preserve the reduction relation, unlike the H-transformation.

All the above information is found in sections 6E and 6F of "Combinatory Logic Volume I" by Curry and Feys and in chapter 9 of "Lambda Calculus and Combinators" by Hindley and Seldin. Hindley also wrote an article published in MLQ in 1977 that discusses these things in more detail.