One-Step Strategies in Lambda Calculus

A one-step strategy effectively selects one available contraction from a reducible lambda term. Determine which combinatory-logic constructions have lambda-calculus analogues, specifically:

1. an effective cofinal one-step reduction strategy;

2. an effective one-step strategy witnessing the Church--Rosser property;

3. an effective strategy that enumerates the relevant reducts;

4. a proof that no effective confluence function exists, if the corresponding combinatory-logic obstruction persists.