Advertisement

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

  • Pierluigi MinariEmail author
Chapter
Part of the Synthese Library book series (SYLI, volume 412)

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

  1. Barendregt, H. P. (1984). The lambda calculus, its syntax and semantics (Revised ed.). Amsterdam: North-Holland.Google Scholar
  2. Curry, H. B., & Feys, R. (1958). Combinatory logic (Vol. I). Amsterdam: North-Holland.Google Scholar
  3. David, R. (2009). A direct proof of the confluence of combinatory strong reduction. Theoretical Computer Science, 410, 4204–4201.CrossRefGoogle Scholar
  4. 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
  5. 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
  6. Hindley, J. R., & Seldin, J. P. (2008). Lambda-calculus and combinators, an introduction. London/New York: Cambridge University Press.CrossRefGoogle Scholar
  7. Lercher, B. (1967). Strong reduction and normal forms in combinatory logic. Journal of Symbolic Logic, 32, 213–223.CrossRefGoogle Scholar
  8. Minari, P. (2004). Analytic combinatory calculi and the elimination of transitivity. Archive for Mathematical Logic, 43, 159–191.CrossRefGoogle Scholar
  9. 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
  10. 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
  11. Minari, P. (2009). A solution to Curry and Hindley’s problem on combinatory strong reduction. Archive for Mathematical Logic, 48, 385–424.CrossRefGoogle Scholar
  12. Troelstra, A. S., & Schwichtenberg, H. (2000). Basic proof theory (2nd ed.). Cambridge: Cambridge University Press.CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.Section of Philosophy, Department DILEFUniversità di FirenzeFlorenceItaly

Personalised recommendations