Submitted by Richard Statman
Statement. Which results on one-step effective strategies carry over from combinatory logic to lambda-calculus?
The following results on reduction and conversion strategies in combinatory logic are surveyed in [Statman, 1997]:
These results all apply to the combinator calculus and many seem to depend on the fact that residuals of disjoint redexes remain disjoint. The questions, however, appear to be more subtle for lambda terms where each one-step reduction can create a much more radical change in structure.
[Statman, 1997] Statman, R. (1997). Effective reduction and conversion strategies for combinators. In Rewriting Techniques and Applications, volume 1232 of Lecture Notes in Computer Science, pages 299–307. Springer-Verlag.