Movatterモバイル変換

[0]ホーム
URL:

Skip to main content

Advertisement

Springer Nature Link
Log in

A λ-calculus structure isomorphic to Gentzen-style sequent calculus structure

  • Conference paper
  • First Online:

Part of the book series:Lecture Notes in Computer Science ((LNCS,volume 933))

Included in the following conference series:

Abstract

We consider a λ-calculus for which applicative terms have no longer the form (...((u u1)u2)...un) but the form (u [u1;...;un]), for which [u1;...;un] is a list of terms. While the structure of the usual λ-calculus is isomorphic to the structure of natural deduction, this new structure is isomorphic to the structure of Gentzen-style sequent calculus. To express the basis of the isomorphism, we consider intuitionistic logic with the implication as sole connective. However we do not consider Gentzen's calculus LJ, but a calculus LJT which leads to restrict the notion of cut-free proofs in LJ. We need also to explicitly consider, in a simply typed version of this λ-calculus, a substitution operator and a list concatenation operator. By this way, each elementary step of cutelimination exactly matches with aβ-reduction, a substitution propagation step or a concatenation computation step.

Though it is possible to extend the isomorphism to classical logic and to other connectives, we do not treat of it in this paper.

This research was partly supported by ESPRIT Basic Research Action “Types for Proofs and Programs” and by Programme de Recherche Coordonnées “Mécanisation du raisonnement”.

This is a preview of subscription content,log in via an institution to check access.

Access this chapter

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. V. Breazu Tanen, D. Kesner, L. Puel: “A typed pattern calculus”,IEEE Symposium on Logic in Computer Science, Montréal, Canada, June 1993, pp 262–274.

    Google Scholar 

  2. V. Danos, J-B. Joinet, H. Schellinx: “LKQ and LKT: Sequent calculi for second order logic based upon dual linear decompositions of classical implication”, inProceedings of the Workshop on Linear Logic, Cornell, edited by J-Y. Girard, Y. Lafont, L. Régnier, 1993.

    Google Scholar 

  3. A. G. Dragalin:Mathematical Intuitionism: Introduction to Proof Theory, Translations of mathematical monographs, Vol 67, Providence, R.I.: American Mathematical Society, 1988.

    Google Scholar 

  4. J. Gallier: “Constructive logics, part I: A tutorial on proof systems and typed λ-calculi”,Theoretical Computer Science, Vol 110, 1993, pp 249–339.

    Article  Google Scholar 

  5. J.-Y. Girard: “A new constructive logic: classical logic”,Mathematical Structures in Computer Science, Vol 1, 1991, pp 255–296.

    Google Scholar 

  6. J-Y. Girard: “On the Unity of Logic”,Annals of Pure and Applied Logic, Vol 59, 1993, pp 201–217.

    Article  Google Scholar 

  7. G. Huet: “Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems”,Journal of the Association for Computing Machinery, Vol 27, 1980, pp 797–821.

    Google Scholar 

  8. Z. Benaissa, D. Briaud, P. Lescanne, J. Rouyer-Degli, “λν, a calculus of explicit substitutions which preserves strong normalisation”, submitted toJournal of Functional Programming, 1995.

    Google Scholar 

  9. G. Mints: “Normal forms for sequent derivations”, Private communication, 1994.

    Google Scholar 

  10. G. Pottinger: “Normalization as a homomorphic image of cut-elimination”,Annals of mathematical logic), Vol 12, 1977, pp 323–357.

    Google Scholar 

  11. D. Prawitz:Natural Deduction, a Proof-sTheoretical Study, Almquist and Wiksell, Stockholm, 1965, pp 90–91

    Google Scholar 

  12. W. A. Howard, “The Formulae-as-Types Notion of Constructions”, in J.P. Seldin and J.R. Hindley Eds,To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Academic Press, 1980 (unpublished manuscript of 1969).

    Google Scholar 

  13. P. Wadler: “A Curry-Howard isomorphism for sequent calculus”, Private communication, 1993.

    Google Scholar 

  14. J. I. Zucker: “Correspondence between cut-elimination and normalization, part I and II”,Annals of mathematical logic, Vol 7, 1974, pp 1–156.

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LITP, University Paris 7, 2 place Jussieu, 78252, Paris Cedex 05, France

    Hugo Herbelin

  2. INRIA-Rocquencourt, B.P. 105, 78153, Le Chesnay Cedex, France

    Hugo Herbelin

Authors
  1. Hugo Herbelin

    You can also search for this author inPubMed Google Scholar

Editor information

Leszek Pacholski Jerzy Tiuryn

Rights and permissions

Copyright information

© 1995 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Herbelin, H. (1995). A λ-calculus structure isomorphic to Gentzen-style sequent calculus structure. In: Pacholski, L., Tiuryn, J. (eds) Computer Science Logic. CSL 1994. Lecture Notes in Computer Science, vol 933. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0022247

Download citation

Publish with us

[8]ページ先頭
©2009-2025 Movatter.jp