A solution to Curry and Hindley’s problem on combinatory strong reduction

Archive for Mathematical Logic 48 (2):159-184 (2009)

Abstract

It has often been remarked that the metatheory of strong reduction $\succ$ , the combinatory analogue of βη-reduction ${\twoheadrightarrow_{\beta\eta}}$ in λ-calculus, is rather complicated. In particular, although the confluence of $\succ$ is an easy consequence of ${\twoheadrightarrow_{\beta\eta}}$ being confluent, no direct proof of this fact is known. Curry and Hindley’s problem, dating back to 1958, asks for a self-contained proof of the confluence of $\succ$ , one which makes no detour through λ-calculus. We answer positively to this question, by extending and exploiting the technique of transitivity elimination for ‘analytic’ combinatory proof systems, which has been introduced in previous papers of ours. Indeed, a very short proof of the confluence of $\succ$ immediately follows from the main result of the present paper, namely that a certain analytic proof system G e [ $\mathbb {C}$ ] , which is equivalent to the standard proof system CL ext of Combinatory Logic with extensionality, admits effective transitivity elimination. In turn, the proof of transitivity elimination—which, by the way, we are able to provide not only for G e [ $\mathbb {C}$ ] but also, in full generality, for arbitrary analytic combinatory systems with extensionality—employs purely proof-theoretical techniques, and is entirely contained within the theory of combinators

Download options

PhilArchive



    Upload a copy of this work     Papers currently archived: 72,743

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Analytics

Added to PP
2013-11-23

Downloads
45 (#255,670)

6 months
1 (#387,390)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Pierluigi Minari
Università degli Studi di Firenze

References found in this work

Combinatory Logic, Volume I.Haskell B. Curry, Robert Feys & William Craig - 1959 - Philosophical Review 68 (4):548-550.
Introduction to Combinatory Logic.J. Roger Hindley - 1972 - Cambridge University Press.
Axioms for Strong Reduction in Combinatory Logic.Roger Hindley - 1967 - Journal of Symbolic Logic 32 (2):224-236.
Strong Reduction and Normal Form in Combinatory Logic.Bruce Lercher - 1967 - Journal of Symbolic Logic 32 (2):213-223.
Analytic Combinatory Calculi and the Elimination of Transitivity.Pierluigi Minari - 2004 - Archive for Mathematical Logic 43 (2):159-191.

View all 11 references / Add more references

Citations of this work

Add more citations

Similar books and articles

Analytic Combinatory Calculi and the Elimination of Transitivity.Pierluigi Minari - 2004 - Archive for Mathematical Logic 43 (2):159-191.
The Church-Rosser Property in Symmetric Combinatory Logic.Katalin Bimbó - 2005 - Journal of Symbolic Logic 70 (2):536 - 556.
Combinatory Reduction Systems.Jan Willem Klop - 1963 - Mathematisch Centrum.
Introduction to Combinatory Logic.J. Roger Hindley - 1972 - Cambridge University Press.
NP-Completeness of a Combinator Optimization Problem.M. S. Joy & V. J. Rayward-Smith - 1995 - Notre Dame Journal of Formal Logic 36 (2):319-335.
Compact Bracket Abstraction in Combinatory Logic.Sabine Broda & Luís Damas - 1997 - Journal of Symbolic Logic 62 (3):729-740.
Axioms for Strong Reduction in Combinatory Logic.Roger Hindley - 1967 - Journal of Symbolic Logic 32 (2):224-236.
The Church-Rosser Property in Dual Combinatory Logic.Katalin Bimbó - 2003 - Journal of Symbolic Logic 68 (1):132-152.
Combinatory Logic.Haskell B. Curry - 1958 - Amsterdam: North-Holland Pub. Co..