5
$\begingroup$

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$?

$\endgroup$
6
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.