The search for a reduction in combinatory logic equivalent to \(\alpha\beta\)-reduction (Q654911)

Combinatory logic (CL) is generally regarded as equivalent to lambda-calculus. However, with respect to reduction, the equivalence is not complete. In CL there is no, as yet, reduction relation which is generally accepted as an equivalent to beta-reduction in lambda-calculus. This paper is about the past, present and future search for a reduction on CL equivalent to beta-reduction. Section 1 starts by recalling the basic definitions regarding combinatory logic and lambda-calculus. In particular, the author recalls the notions of beta(-eta)-reduction and combinatory weak reduction and the translations of lambda-calculus into combinatory logic and vice versa. In particular there are many possible algorithms to implement the abstraction of variables in combinatory terms, and each of these algorithms induces a different mapping of lambda-terms into combinatory terms. During the exposition, the author also retraces the research of H. B. Curry who, as he says, looked for these correspondences only in the light of comparing the equational theories of the two systems, rather than being interested in a comparison of the reductions. The section ends by recalling how it is possible to augment the basic equational calculus for CL in order to obtain combinatory beta-eta-equality, which is accepted as the equivalent of beta-eta conversion (under the mapping that translates CL into the lambda-calculus) and called eta-strong reduction. In Section 2 the author briefly explains how Curry got interested in combinatory reduction, due to his pioneering connection between type assignment systems and normalization, and how he designed his strong eta-reduction of combinatory terms, proving that this reduction in CL is equivalent to beta-eta-reduction in lambda-calculus. However, Curry still had a problem: finding a reduction in CL equivalent to beta-reduction in lambda-calculus. The author explains why this was a major obstacle for Curry himself. Section 3 consists of a description of some good properties for a reduction in CL that could be considered equivalent to beta-reduction in lambda-calculus. The very concept of such a reduction, called beta-strong reduction, would be vague without those guidelines. These properties were enumerated by \textit{J. R. Hindley} in [``Curry's last problem: imitating lambda-beta-reduction in combinatory logic'', presented to the meeting of the British Logic Colloquium, Wales UK, 1999, 23--25 (1999)]. Section 4 contains an exposition of three proposals: the first one due to Curry [\textit{H. B. Curry, J. R. Hindley} and \textit{J. P. Seldin}, Combinatory logic. Vol. II. Amsterdam-London: North-Holland Publishing Company (1972; Zbl 0242.02029)], the second one to J. P. Seldin and the third one to \textit{M. Mezghiche} [Theor. Comput. Sci. 31, 151--163 (1984; Zbl 0557.03009)]. The author points out the weaknesses of each one of these proposals. In particular they all fail in fulfilling Hindley's requirements, for example for the lack of a syntactical and ``useful'' (to quote the author's words) characterization of irreducible CL-terms. Section 5 explains some problems encountered by researchers in writing a computer program that implements the proposals for beta-strong reduction. This task is not yet completely settled, while it has been accomplished for Curry's eta-strong reduction (a tool is available online at \url{http://pages.cpsc.ucalgary.ca/~nicholss/research/cl_web/cl_web.php}). Section 6, the last one, discusses possible modifications to the three approaches explained in Section 4, at the same time posing questions about their effect. In all cases, the author asserts the need for further investigations. To conclude, the appendix of the paper contains a full account of Curry's interest in CL, including the motivations that led him in his investigations initially about conversion and eventually about reduction.