[Next] [Previous] [Up]

#### Problem # 8

Submitted by Richard Statman

Date: 1993

Statement. Which results on one-step effective strategies carry over from
combinatory logic to lambda-calculus?

[PRINT this PROBLEM]

The following results on reduction and conversion strategies in combinatory logic
are surveyed in [Statman, 1997]:

- There is an effective one-step coﬁnal 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 conﬂuence 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

[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.

[Next] [Previous] [Up]

Last modified: July 21, 2014