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

Combinatory logic (CL) is generally regarded as equivalent to lambda-calculus (lambda.), 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 lambda beta-reduction in A. 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 lambda beta-reduction. (C) 2011 Elsevier B.V. All rights reserved.