Mathesis Universalis, Computability and Proof pp 235-253 | Cite as

# Analytic Equational Proof Systems for Combinatory Logic and *λ*-Calculus:A Survey

## 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.

## References

- 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 - David, R. (2009). A direct proof of the confluence of combinatory strong reduction.
*Theoretical Computer Science, 410*, 4204–4201.CrossRefGoogle 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 - Hindley, J. R., & Seldin, J. P. (2008). Lambda-calculus and combinators, an introduction. London/New York: Cambridge University Press.CrossRefGoogle Scholar
- Lercher, B. (1967). Strong reduction and normal forms in combinatory logic.
*Journal of Symbolic Logic, 32*, 213–223.CrossRefGoogle Scholar - Minari, P. (2004). Analytic combinatory calculi and the elimination of transitivity.
*Archive for Mathematical Logic, 43*, 159–191.CrossRefGoogle 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 - Minari, P. (2007). Analytic proof systems for
*λ*-calculus: The elimination of transitivity, and why it matters.*Archive for Mathematical Logic, 46*, 159–184.CrossRefGoogle Scholar - Minari, P. (2009). A solution to Curry and Hindley’s problem on combinatory strong reduction.
*Archive for Mathematical Logic, 48*, 385–424.CrossRefGoogle Scholar - Troelstra, A. S., & Schwichtenberg, H. (2000).
*Basic proof theory*(2nd ed.). Cambridge: Cambridge University Press.CrossRefGoogle Scholar