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

From MaRDI portal
scientific article
Language Label Description Also known as
English
A solution to Curry and Hindley's problem on combinatory strong reduction
scientific article

    Statements

    A solution to Curry and Hindley's problem on combinatory strong reduction (English)
    0 references
    0 references
    27 April 2009
    0 references
    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)].''
    0 references
    0 references
    0 references
    0 references
    0 references
    combinatory logic
    0 references
    extensionality
    0 references
    strong combinatory reduction
    0 references
    confluence
    0 references
    0 references