Analytic Equational Proof Systems for Combinatory Logic and λ-Calculus:A Survey
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.
- Barendregt, H. P. (1984). The lambda calculus, its syntax and semantics (Revised ed.). Amsterdam: North-Holland.Google Scholar
- Curry, H. B., & Feys, R. (1958). Combinatory logic (Vol. I). Amsterdam: North-Holland.Google Scholar
- Hasegawa, R., Paolini, L. & Urzyczyn, P., eds. (2006). TLCA (Typed Lambda Calculi and Applications) list of open problems. http//tlca.di.unito.it/opltlca/Google Scholar
- Hindley, J. R., & Lercher, B. (1970). A short proof of Curry’s normal form theorem. Proceedings of American Mathematical Society, 24, 808–810.Google Scholar
- 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.Google Scholar