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

From the author's abstract: ``Curry and Hindley's problem, dating back to 1958, asks for a self-contained proof of the confluence of \(\succ\) [the combinatory analogue of \(\beta \eta \)-reduction \({\twoheadrightarrow_{\beta\eta}}\) in \(\lambda \)-calculus], one which makes no detour through \(\lambda\)-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 [\textit{P. Minari}, ``Analytic combinatory calculi and the elimination of transitivity'', Arch. Math. Logic 43, No.~2, 159--191 (2004; Zbl 1060.03033); ``Proof-theoretical methods in combinatory logic and \(\lambda\)-calculus'', talk presented at CiE 2005: New computational paradigms, Amsterdam, 2005; ``Analytic proof systems for \(\lambda\)-calculus: the elimination of transitivity, and why it matters'', Arch. Math. Logic 46, No.~5--6, 385--424 (2007; Zbl 1117.03020)].''