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

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. [ABSTRACT FROM AUTHOR]