Advertisement

Calculus of classical proofs I

  • Ken-etsu Fujita
Session 8
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1345)

Abstract

We introduce a simple natural deduction system of classical propositional logic called λ exc v , and prove the computational properties of the system based on a call-by-value strategy. We show (1) a strict fragment of gl exc v that is complete with respect to classical provability, and the computational meaning of the existence of such a fragment; (2) a simple exit mechanism by the use of a proof of Peirce's law, and some examples using classical proofs as programs; (3) the Church-Rosser property; (4) the CPS-translation from λ exc v to λ and its correctness with respect to conversions; (5) a computational use of the logical inconsistency in λ exc v , extended with a certain signature.

Keywords

Classical Logic Reduction Rule Exception Handling Classical Propositional Logic Annual IEEE Symposium 
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.
    Andou, Y.: A Normalization-Procedure for the First Order Classical Natural Deduction with Full Logical Symbols. Tsukuba Journal of Mathematics 19 1 (1995) 153–162Google Scholar
  2. 2.
    Barendregt, H.P.: The Lambda Calculus Its Syntax and Semantics (revised edition). North-Holland (1984)Google Scholar
  3. 3.
    Barendregt, H.P.: Lambda Calculi with Types. Handbook of Logic in Computer Science Vol. II. Oxford University Press (1992) 1–189Google Scholar
  4. 4.
    Barbanera, F. and Berardi, S.: Extracting Constructive Context from Classical Logic via Control-like Reductions. LNCS 664 (1993) 45–59Google Scholar
  5. 5.
    Coquand, T.: An Analysis of Girard's Paradox. Proc. 1st Logic in Computer Science (1986) 227–236Google Scholar
  6. 6.
    De Groote, P.: On the Relation between the λμ-Calculus and the Syntactic Theory of Sequential Control. LNAI 822 (1994) 31–43Google Scholar
  7. 7.
    De Groote, P.: A Simple Calculus of Exception Handling. LNCS 902 (1995) 201–215Google Scholar
  8. 8.
    Felleisen, M., Friedman, D.P., Kohlbecker, E. and Duba, B.: Reasoning with Continuations. Proc. Annual IEEE Symposium on Logic in Computer Science (1986) 131–141Google Scholar
  9. 9.
    Felleisen, M. and Hieb, R.: The Revised Report on the Syntactic Theories of Sequential Control and State. Theoretical Computer Science 103 (1992) 131–141CrossRefGoogle Scholar
  10. 10.
    Fujita, K.: On Embedding of Classical Substructural Logics. Proc. Theory of Rewriting Systems and Its Applications Kyoto University RIMS 918 (1995) 178–195Google Scholar
  11. 11.
    Fujita, K.: μ,-Head Form Proofs and its Application to Programming. Computer Software 14 2 (1997) 71–75Google Scholar
  12. 12.
    Fujita, K.: μ-Head Form Proofs with at Most Two Formulas in the Succedent. Transactions of Information Processing Society of Japan 38 6 (1997) 1073–1082Google Scholar
  13. 13.
    Fujita, K.: Calculus of Classical Proofs from Programming Viewpoint. Kyoto University RIMS 1010 (1997) 7–34Google Scholar
  14. 14.
    Griffin, T.G.: A Formulae-as-Types Notion of Control. Proc. 17th Annual ACM Symposium on Principles of Programming Languages (1990) 47–58Google Scholar
  15. 15.
    Harper, R., Duba, B.F. and MacQueen, D.: Typing First-Class Continuations in ML. J. Functional Programming 3 (4) (1993) 465–484Google Scholar
  16. 16.
    Hayashi, S. and Nakano, H.: PX A Computational Logic. The MIT Press (1988)Google Scholar
  17. 17.
    Howard, W.: The Formulae-as-Types Notion of Constructions. To H.B.Curry: Essays on combinatory logic, lambda-calculus, and formalism. Academic Press (1980) 479–490Google Scholar
  18. 18.
    Howe, D.J.: The Computational Behaviour of Girard's Paradox. Proc. 2nd Logic in Computer Science (1987) 205-214Google Scholar
  19. 19.
    Kobayashi, S.: Monads, Modality and Curry-Howard Principle. Proc. 10th Japan Society for Software Science and Technology (1993) 225–228Google Scholar
  20. 20.
    Lillibridge, M.: Exceptions Are Strictly More Powerful Than Call/CC. Carnegie Mellon University CMU-CS-95-178 (1995)Google Scholar
  21. 21.
    Milner, R., Tofte, M. and Harper, R.: The Definition of Standard ML. The MIT Press (1990)Google Scholar
  22. 22.
    Murthy, C.R.: An Evaluation Semantics for Classical Proofs. Proc. 6th Annual IEEE Symposium on Logic in Computer Science (1991) 96–107Google Scholar
  23. 23.
    Nakano, H.: Logical Structures of the Catch and Throw Mechanism. PhD thesis University of Tokyo (1995)Google Scholar
  24. 24.
    Nordstr6m, B., Petersson, K. and Smith, J.M.: Programming in Martin-Löf's Type Theory An Introduction. Clarendon Press (1990)Google Scholar
  25. 25.
    Ong, C.-H.L.: A Semantic View of Classical Proofs: Type-Theoretic, Categorical, and Denotational Characterizations. Linear Logic '96 Tokyo Meeting (1996)Google Scholar
  26. 26.
    Ong, C.-H.L. and Stewart, C.A.: A Curry-Howard Foundation for Functional Computation with Control. Proc. 24th Annual ACM SIGPLAN-SIGACT Symposium of Principles of Programming Languages (1997)Google Scholar
  27. 27.
    Parigot, M.: μ-Calculus: An Algorithmic Interpretation of Classical Natural Deduction. LNCS 624 (1992) 190–201Google Scholar
  28. 28.
    Parigot, M.: Classical Proofs as Programs. LNCS 713 (1993) 263–276Google Scholar
  29. 29.
    Parigot, M.: Strong Normalization for Second Order Classical Natural deduction. Proc. 8th Annual IEEE Symposium on Logic in Computer Science (1993)Google Scholar
  30. 30.
    Plotkin, G.: Call-by-Name, Call-by-Value and the λ-Calculus. Theoretical Computer Science 1 (1975) 125–159CrossRefGoogle Scholar
  31. 31.
    Prawitz, D.: Natural Deduction: A Proof-Theoretical Study. Almgvist&Wiksell (1965)Google Scholar
  32. 32.
    Rehof, N.J. and Sorensen, M.H.: The λΔ-Calculus. LNCS 789 (1994) 516–542Google Scholar
  33. 33.
    Seldin, J.P.: Normalization and Excluded Middle I. Studia Logica XLVIII 2 (1989) 193–217Google Scholar
  34. 34.
    Szabo, M.E.: The Collected Papers of Gerhard Gentzen. North-Holland (1969)Google Scholar
  35. 35.
    Takahashi, M.: Parallel Reductions in λ-Calculus. J. Symbolic Computation 7 (1989) 113–123Google Scholar
  36. 36.
    Takeuti, G.: Proof Theory (second edition). North-Holland (1987)Google Scholar
  37. 37.
    Tonino, H. and Fujita, K.: On the adequacy of representing higher order intuitionistic logic as a pure type system. Annals of Pure and Applied Logic 57 (1992) 251–276CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • Ken-etsu Fujita
    • 1
  1. 1.Kyushu Institute of TechnologyIizukaJapan

Personalised recommendations