Advertisement

Cut Elimination for Classical Proofs as Continuation Passing Style Computation

  • Ichiro Ogata
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1538)

Abstract

We show that the one can consider proof of the Gentzen’s LK as the continuation passing style(CPS) programs; and the cut-elimination procedure for LK as computation. To be more precise, we observe that Strongly Normalizable(SN) and Church-Rosser(CR) cut-elimination procedure for (intuitionistic decoration of) LKT and LKQ, as presented in Danos et al.(1993), precisely corresponds to call-by-name(CBN) and call-by-value(CBV) CPS calculi, respectively. This can also be seen as an extension to classical logic of Zucker-Pottinger-Mints investigation of the relations between cut-elimination and normalization.

Keywords

Classical Logic Linear Logic Natural Deduction Derivation Rule Classical Proof 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [1]
    Martín Abadi, Luca Cardelli, P.-L. Curien, and Jean-Jacques Lévy. Explicit substitutions. In Conference Record of the Seventeenth Annual ACM Symposium on Principles of Programming Languages, pages 31–46, San Francisco, California, January 1990.Google Scholar
  2. [2]
    Vincent Danos. La Logique Linéaire Appliquée à l'étude de Divers Processus de Normalisation (Principalement du λ-Calcul). PhD thesis, University of Paris VII, June 1990.Google Scholar
  3. [3]
    Vincent Danos, Jean-Baptiste Joinet, and Harold Schellinx. Sequent calculi for second order logic. In J.-Y. Girard, Y. Lafont, and L. Regnier, editors, Advances in Linear Logic, pages 211–224. Cambridge University Press, 1995. Proceedings of the Workshop on Linear Logic, Ithaca, New York, June 1993.Google Scholar
  4. [4]
    Vincent Danos, Jean-Baptiste Joinet, and Harold Schellinx. A new deconstructive logic: linear logic. Journal of Symbolic Logic, 62(3), September 1997.Google Scholar
  5. [5]
    Phillipe deGroote. A cps-translation of the λμ-calculus. In Proceedings Trees in Algebra and Programming-CAAP’94, pages 85–99. Springer-Verlag LNCS 787, April 1994.CrossRefGoogle Scholar
  6. [6]
    Matthias Felleisen, Daniel P. Friedman, Eugene Kohlbecker, and Bruce Duba. Reasoning with continuations. In Proceedings, Symposium on Logic in Computer Science, pages 131–141, Cambridge, Massachusetts, 16–18 June 1986. IEEE Computer Society.Google Scholar
  7. [7]
    G. Gentzen. Untersuchungen über das logische schließen. Mathematische Zeitschrift, 39:176–210, 405–431, 1935.CrossRefMathSciNetGoogle Scholar
  8. [8]
    Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50:1–102, 1987.zbMATHCrossRefMathSciNetGoogle Scholar
  9. [9]
    Jean-Yves Girard. A new constructive logic: Classical logic. Mathematical Structures in Computer Science, 1:255–296, 1991.zbMATHMathSciNetCrossRefGoogle Scholar
  10. [10]
    Jean-Yves Girard. On the unity of logic. Annals of Pure and Applied Logic, 59:201–217, 1993.zbMATHCrossRefMathSciNetGoogle Scholar
  11. [11]
    Jean-Yves Girard, Yves Lafont, and P. Taylor. Proofs and Types. Cambridge Tracts in Theoretical Computer Science 7. Cambridge University Press, 1988.Google Scholar
  12. [12]
    Timothy G. Griffin. A formulae-as-types notion of control. In Conference Record of the Seventeenth Annual ACM Symposium on Principles of Programming Languages, pages 47–58, San Francisco, California, January 1990.Google Scholar
  13. [13]
    Hugo Herbelin. A λ-calculus structure ismorphic to gentzen-style sequent calculus structure. In L. Pacholski and J. Tiuryn, editors, Proceedings of the 1994 Annual Conference of the European Association for Computer Science Logic, Kazimierz, Poland, September 1994. Springer Verlag, LNCS 933.Google Scholar
  14. [14]
    Grigori Mints. Normal forms for sequent derivations. In Piergiorgio Odifreddi, editor, Kreiseliana-About and Around George Kreisel. A K Peters Ltd., March 1996.Google Scholar
  15. [15]
    Chetan R. Murthy. A computational analysis of Girard’s translation and LC. In Proceedings, Seventh Annual IEEE Symposium on Logic in Computer Science, pages 90–101, Santa Cruz, California, 22–25 June 1992. IEEE Computer Society Press.Google Scholar
  16. [16]
    Ichiro Ogata. Classical proofs as programs, cut elimination as computation. Manuscript, June 1998.Google Scholar
  17. [17]
    C.-H. L. Ong and C. A. Stewart. A curry-howard foundation for functional computation with control. In Proceedings of ACM SIGPLAN-SIGACT Symposium on Principle of Programming Languages, Paris, January 1997. ACM Press, 1997.Google Scholar
  18. [18]
    Michel Parigot. Free deduction: An analysis of “computations” in classical logic. In RCLP 1990/1991, pages 361–380, 1991.Google Scholar
  19. [19]
    Michel Parigot. Lambda-mu-calculus: An algorithmic interpretation of classical natural deduction. In LPAR 1992, pages 190–201, 1992.Google Scholar
  20. [20]
    Michel Parigot. Classical proofs as programs. In 3rd Kurt Gödel Colloquium, pages 263–276. Springer-Verlag LNCS 713, 1993.Google Scholar
  21. [21]
    Michel Parigot. Strong normalization for second order classical natural deduction. In Proceedings, Eighth Annual IEEE Symposium on Logic in Computer Science, pages 39–46, Montreal, Canada, 19–23 June 1993. IEEE Computer Society Press.Google Scholar
  22. [22]
    G. D. Plotkin. Call-by-name, call-by-value and the λ-calculus. Theoretical Computer Science, 1(2):125–159, December 1975.Google Scholar
  23. [23]
    G. Pottinger. Normalization as a homomorphic image of cut-elimination. Annals of Mathematical Logic, 12:323–357, 1977.zbMATHMathSciNetCrossRefGoogle Scholar
  24. [24]
    D. Prawitz. Natural Deduction, a Poof-Theoretical Study. Almquist and Wiksell, Stockholm, 1965.Google Scholar
  25. [25]
    Anne S. Troelstra. Lectures on Linear Logic. CSLI Lecture Notes 29, Center for the Study of Language and Information, Stanford, California, 1992.zbMATHGoogle Scholar
  26. [26]
    J. I. Zucker. Correspondence between cut-elimination and normalization, part i and ii. Annals of Mathematical Logic, 7:1–156, 1974.CrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • Ichiro Ogata
    • 1
  1. 1.Electrotechnical LaboratoryTsukubaJapan

Personalised recommendations