Problem # 8

Submitted by Richard Statman
Date: 1993
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]:

• There is an effective one-step cofinal reduction strategy.
• There is an effective one-step Church-Rosser strategy.
• There is an effective one-step enumeration strategy (a strategy which lists all the combinators convertible to a given one).
• There is no effective confluence function (computing a common reduct of any given terms and ).

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.

References for # 8