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

ABSTRACT. It has often been remarked that the metatheory of strong reduction >-, the combinatory analogue of βη-reduction -->>βη in λ-calculus, is rather complicated. In particular, although the confluence of >- is an easy consequence of -->>βη 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 >-, 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 >- immediately follows from the main result of the present paper, namely that a certain analytic proof system G_e[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[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.