zbMATH — the first resource for mathematics

A solution to Curry and Hindley’s problem on combinatory strong reduction. (English) Zbl 1172.03009
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 [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)].”

03B40 Combinatory logic and lambda calculus
03F05 Cut-elimination and normal-form theorems
03F07 Structure of proofs
Full Text: DOI
[1] Barendregt H.P.: The Lambda Calculus, its Syntax and Semantics, Revised edn. North-Holland, Amsterdam (1984) · Zbl 0551.03007
[2] Curry H.B., Feys R.: Combinatory Logic, vol. I. North-Holland, Amsterdam (1958) · Zbl 0081.24104
[3] Curry H.B., Hindley J.R., Seldin J.P.: Combinatory Logic, vol. II. North-Holland, Amsterdam (1972) · Zbl 0242.02029
[4] Hindley J.R.: Axioms for strong reduction in combinatory logic. J. Symb. Log. 32, 224–236 (1967) · Zbl 0153.00603 · doi:10.2307/2271660
[5] Hindley, R.: Review of Loewen [12], [13], [14]. MR0248022 (40 #1279a), MR0248023 (40 #1279b), MR0248024 (40 #1279c)
[6] Hindley, R.: Problem # 1, TLCA (Typed Lambda Calculi and Applications) List of Open Problems. http://tlca.di.unito.it/opltlca/
[7] Hindley R., Lercher B.: A short proof of Curry’s normal form theorem. Proc. Am. Math. Soc. 24, 808–810 (1970) · Zbl 0195.02101
[8] Hindley J.R., Lercher B., Seldin J.P.: Introduction to Combinatory Logic. Cambridge University Press, London (1972) · Zbl 0269.02005
[9] Hindley J.R., Seldin J.P.: Lambda-Calculus and Combinators, an Introduction. Cambridge University Press, London (2008) · Zbl 1149.03016
[10] Lercher B.: Strong reduction and normal forms in combinatory logic. J. Symb. Log. 32, 213–223 (1967) · Zbl 0153.00602 · doi:10.2307/2271659
[11] Lercher B.: The decidability of Hindley’s axioms for strong reduction. J. Symb. Log. 32, 237–239 (1967) · Zbl 0153.00701 · doi:10.2307/2271661
[12] Loewen K.: A standardization theorem for strong reduction. Notre Dame J. Formal Logic 9, 271–283 (1968) · Zbl 0195.30702 · doi:10.1305/ndjfl/1093893462
[13] Loewen K.: Modified strong reduction in combinatory logic. Notre Dame J. Formal Logic 9, 265–270 (1968) · Zbl 0195.30701 · doi:10.1305/ndjfl/1093893461
[14] Loewen K.: The Church Rosser theorem for strong reduction in combinatory logic. Notre Dame J. Formal Logic 9, 299–302 (1968) · Zbl 0191.30803 · doi:10.1305/ndjfl/1093893514
[15] Minari P.: Analytic combinatory calculi and the elimination of transitivity. Arch. Math. Logic 43, 159–191 (2004) · Zbl 1060.03033 · doi:10.1007/s00153-003-0203-1
[16] Minari, P.: Proof-theoretical methods in combinatory logic and \(\lambda\)-calculus. In: Cooper, S.B., Löwe, B., Torenvliet, L., CiE 2005: New Computational Paradigms, pp. 148–157. ILLC X-2005-01, Amsterdam (2005)
[17] Minari P.: Analytic proof systems for \(\lambda\)-calculus: the elimination of transitivity, and why it matters. Arch. Math. Logic 46, 385–424 (2007) · Zbl 1117.03020 · doi:10.1007/s00153-007-0039-1
[18] Stenlund S.: Combinators, Lambda Terms, and Proof Theory. Reidel, Dordrecht (1972) · Zbl 0248.02032
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.