posted on 1996-01-01, 00:00authored byRichard Statman
Abstract: "We shall prove the following results concerning effective reduction and conversion strategies for combinators. (1) There is an effective one-step cofinal reduction strategy (answering a question of Barendregt [2] 13.6.6). (2) There is no effective confluence function but there is an effective one-step confluence strategy (answering a question of Isles reported in [1]). (3) There is an effective one-step enumeration strategy (answering an obvious question). (4) There is an effective one-step Church-Rosser conversion strategy ('almost' answering a question of Bergstra and Klop [3])."