<p>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.</p>

<p>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.</p>

<p>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.</p>

CC BY-SA 3.0
2015-08-28T11:57:42.943Z
2015-08-28T11:57:42.943Z
William Stirton
<p>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$.</p>

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

<lambda-calculus><combinatory-logic>
Is combinatory strong reduction equivalent to lambda beta-eta reduction?
Martha S.
# Is combinatory strong reduction equivalent to lambda beta-eta reduction?

(Asked by: username_0 on 2013-10-27)

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

**Tags:** lambda-calculus, combinatory-logic

---

## 1 answers

### Answer by username_1 on 2015-08-28. Score: 6

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.


---

