Abstract
The paper surveys ideas, results and applications of a novel proof-theoretical approach to equational theories of untyped operations (including combinatory logic CL and Lambda-calculus) we developed in the last 15 years. The approach is based on the introduction and the proof-theoretical investigation of “analytic” proof systems for such theories. Analyticity is due to a main result of transitivity elimination, yielding as a consequence a non trivial streamlining of the proof-theory of the corresponding theories and a number of applications. Among these, a positive solution to an open problem concerning the theory of combinatory strong reduction which was raised about 60 years ago by H.B. Curry.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
In Curry’s terminology (cf. Curry and Feys 1958, sect. 5 C ff.) ‘pure’ is ‘proper’, and ‘linear’ is ‘not having a duplicative effect’.
- 2.
A substitution rule is not needed, as far as axioms are given in a schematic form.
- 3.
\(\mathbb {X}\) is recursive iff the map \(n\mapsto k_{\mathsf {F}_n}\) is recursive, and \(\left <d_{\mathsf {F}_n}\right >_{n\geq 0}\) is a recursive sequence of T X-terms.
- 4.
In such a way, see Lemma 4.8, that (Ext)-free derivations are transformed into τ-free and (Ext)-free derivations of the same end-equation.
- 5.
The motivation is that if I is defined, as in CL, out of K and S (I := S K K) instead of being taken as a primitive combinator, then (because of the fact that S K K I does hold) one has I ≡S K K K I K K(K I K)K… and so there is combinatory term in strong normal form (λ ∗ x.x ≡S K K) which is not strongly irreducible. As soon as the variant with I as a primitive combinator is adopted, it holds that strongly irreducible terms are in strong normal form (Normal Form Theorem, first proved by Curry (Curry and Feys 1958); a shorter proof is due to Hindley and Lercher 1970), and conversely (Converse Normal Form Theorem, Lercher 1967).
- 6.
Here is the inductive definition of λ ∗ x.t:
$$\displaystyle \begin{aligned}\lambda^* x.t := \left\{ \begin{array}{ll} \mathsf{I}, & \text{if }\text{ (a) }{t\equiv x}, \\ t', & \text{if }\text{ (b) }{t\equiv t'x}\text{ with }{x\notin V(t')}, \\ \mathsf{K} t, & \text{if }\text{ (c) }{x\notin V(t)}; \\ \mathsf{S}(\lambda^* x.t_1)(\lambda^* x.t_2), & \text{if }\text{ (d) }{t\equiv t_1t_2}\text{ and (b), (c) do not apply.} \end{array} \right. \end{aligned} $$ - 7.
Indeed, it is easy to verify that if tx ↠βη r and x∉V (t) then one of the following cases does hold: either r has the form r′x with x∉V (r′) and t ↠βη r′, or (ii) r is not of that form and t ↠βη λx.r.
- 8.
Another direct confluence proof, independent and indeed very different from ours, has been given in the same year by René David (2009).
- 9.
Here is Hindley’s statement of the problem: “The βη-strong reduction is the combinatory analogue of βη-reduction in λ-calculus. It is confluent. Its only known confluence-proof is very easy […], but it depends on the having already proved the confluence of λβη-reduction. Thus the theory of combinators is not self-contained at present. Is there a confluence proof independent of λ-calculus?”
- 10.
\(N_E = \frac {( \mathtt {c}(E)+1)( \mathtt {c}(E)+2)}{2}\cdot \mathtt {i}(E)+(\mathtt {a}(E)+1)\cdot (\mathtt {c}(E)+1)\) where, for E ≡ (t = s): c(E) := the number of occurrences of combinators in ts, \(\mathtt {i}(E):=\max \left \{k_{\mathsf {F}}\mid \mathsf {F}\text{ occurs in }ts\right \}\), and \(\mathtt {a}(E):=\min (\mathtt {w}(t),\mathtt {w}(s))\).
References
Barendregt, H. P. (1984). The lambda calculus, its syntax and semantics (Revised ed.). Amsterdam: North-Holland.
Curry, H. B., & Feys, R. (1958). Combinatory logic (Vol. I). Amsterdam: North-Holland.
David, R. (2009). A direct proof of the confluence of combinatory strong reduction. Theoretical Computer Science, 410, 4204–4201.
Hasegawa, R., Paolini, L. & Urzyczyn, P., eds. (2006). TLCA (Typed Lambda Calculi and Applications) list of open problems. http//tlca.di.unito.it/opltlca/
Hindley, J. R., & Lercher, B. (1970). A short proof of Curry’s normal form theorem. Proceedings of American Mathematical Society, 24, 808–810.
Hindley, J. R., & Seldin, J. P. (2008). Lambda-calculus and combinators, an introduction. London/New York: Cambridge University Press.
Lercher, B. (1967). Strong reduction and normal forms in combinatory logic. Journal of Symbolic Logic, 32, 213–223.
Minari, P. (2004). Analytic combinatory calculi and the elimination of transitivity. Archive for Mathematical Logic, 43, 159–191.
Minari, P. (2005). Proof-theoretical methods in combinatory logic and λ-calculus. In S. B. Cooper, B. Löwe, & L. Torenvliet (Eds.), CiE 2005: New computational paradigms (ILLC X-2005-01, pp. 148–157). Amsterdam: ILLC.
Minari, P. (2007). Analytic proof systems for λ-calculus: The elimination of transitivity, and why it matters. Archive for Mathematical Logic, 46, 159–184.
Minari, P. (2009). A solution to Curry and Hindley’s problem on combinatory strong reduction. Archive for Mathematical Logic, 48, 385–424.
Troelstra, A. S., & Schwichtenberg, H. (2000). Basic proof theory (2nd ed.). Cambridge: Cambridge University Press.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this chapter
Cite this chapter
Minari, P. (2019). Analytic Equational Proof Systems for Combinatory Logic and λ-Calculus:A Survey. In: Centrone, S., Negri, S., Sarikaya, D., Schuster, P.M. (eds) Mathesis Universalis, Computability and Proof. Synthese Library, vol 412. Springer, Cham. https://doi.org/10.1007/978-3-030-20447-1_13
Download citation
DOI: https://doi.org/10.1007/978-3-030-20447-1_13
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-20446-4
Online ISBN: 978-3-030-20447-1
eBook Packages: Religion and PhilosophyPhilosophy and Religion (R0)