The search for a reduction in combinatory logic equivalent to λβ-reduction

Combinatory logic (CL) is generally regarded as equivalent to λ-calculus (λ), and in most respects, it is. However, with respect to reduction, the equivalence is not complete. In CL, there is not, as yet, a reduction relation which is generally accepted as an equivalent to λβ-reduction in λ. There are some proposals for such a reduction, but so far none of them has as yet a complete syntactically useful characterization of the irreducible CL-terms. This paper is about the search for a reduction on CL equivalent to λβ-reduction.