The search for a reduction in combinatory logic equivalent to -reduction
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.
- \(c\beta\)-Machine with \(\lambda \beta\)-reduction
- A set of postulates for the foundation of logic. II
- Abstraction problems in combinatory logic: A compositive approach
- Combinatory logic. Vol. II
- Combinatory Reductions and Lambda Reductions Compared
- scientific article; zbMATH DE number 5318491 (Why is no real title available?)
- scientific article; zbMATH DE number 3280068 (Why is no real title available?)
- New sets of postulates for combinatory logics
- On pseudo-c normal form in combinatory logic
- Some Additions to the Theory of Combinators
- Some Advances in the Combinatory Theory of Quantification
- The inconsistency of certain formal logics
- The Paradox of Kleene and Rosser
- Une nouvelle C-réduction dans la logique combinatoire
- On pseudo-c normal form in combinatory logic
- Combinatory weak reduction in lambda calculus
- \(c\beta\)-Machine with \(\lambda \beta\)-reduction
- Combinatory logic with polymorphic types
- Strong reduction of combinatory calculus with streams
- The Church Rosser theorem for strong reduction in combinatory logic
- On adding (ξ) to weak equality in combinatory logic
- scientific article; zbMATH DE number 3909737 (Why is no real title available?)
- scientific article; zbMATH DE number 4045104 (Why is no real title available?)
- scientific article; zbMATH DE number 4045707 (Why is no real title available?)
- Effective reduction and conversion strategies for combinators
- The search for a reduction in combinatory logic equivalent to -reduction. II.
- The Church-Rosser property in symmetric combinatory logic
- Une nouvelle C-réduction dans la logique combinatoire
This page was built for publication: The search for a reduction in combinatory logic equivalent to \(\alpha\beta\)-reduction
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q654911)
