Strong normalization proofs for cut elimination in Gentzen's sequent calculi

Elias Bittar

Banach Center Publications (1999)

  • Volume: 46, Issue: 1, page 179-225
  • ISSN: 0137-6934

Abstract

top
We define an equivalent variant L K s p of the Gentzen sequent calculus L K . In L K s p weakenings or contractions can be performed in parallel. This modification allows us to interpret a symmetrical system of mix elimination rules L K s p by a finite rewriting system; the termination of this rewriting system can be machine checked. We give also a self-contained strong normalization proof by structural induction. We give another strong normalization proof by a strictly monotone subrecursive interpretation; this interpretation gives subrecursive bounds for the length of derivations. We give a strong normalization proof by applying orthogonal term rewriting results for a confluent restriction of the mix elimination system L K s p .

How to cite

top

Bittar, Elias. "Strong normalization proofs for cut elimination in Gentzen's sequent calculi." Banach Center Publications 46.1 (1999): 179-225. <http://eudml.org/doc/208921>.

@article{Bittar1999,
abstract = {We define an equivalent variant $LK_\{sp\}$ of the Gentzen sequent calculus $LK$. In $LK_\{sp\}$ weakenings or contractions can be performed in parallel. This modification allows us to interpret a symmetrical system of mix elimination rules $_\{LK_\{sp\}\}$ by a finite rewriting system; the termination of this rewriting system can be machine checked. We give also a self-contained strong normalization proof by structural induction. We give another strong normalization proof by a strictly monotone subrecursive interpretation; this interpretation gives subrecursive bounds for the length of derivations. We give a strong normalization proof by applying orthogonal term rewriting results for a confluent restriction of the mix elimination system $_\{LK_\{sp\}\}$.},
author = {Bittar, Elias},
journal = {Banach Center Publications},
keywords = {cut elimination; strong normalization; term rewriting systems},
language = {eng},
number = {1},
pages = {179-225},
title = {Strong normalization proofs for cut elimination in Gentzen's sequent calculi},
url = {http://eudml.org/doc/208921},
volume = {46},
year = {1999},
}

TY - JOUR
AU - Bittar, Elias
TI - Strong normalization proofs for cut elimination in Gentzen's sequent calculi
JO - Banach Center Publications
PY - 1999
VL - 46
IS - 1
SP - 179
EP - 225
AB - We define an equivalent variant $LK_{sp}$ of the Gentzen sequent calculus $LK$. In $LK_{sp}$ weakenings or contractions can be performed in parallel. This modification allows us to interpret a symmetrical system of mix elimination rules $_{LK_{sp}}$ by a finite rewriting system; the termination of this rewriting system can be machine checked. We give also a self-contained strong normalization proof by structural induction. We give another strong normalization proof by a strictly monotone subrecursive interpretation; this interpretation gives subrecursive bounds for the length of derivations. We give a strong normalization proof by applying orthogonal term rewriting results for a confluent restriction of the mix elimination system $_{LK_{sp}}$.
LA - eng
KW - cut elimination; strong normalization; term rewriting systems
UR - http://eudml.org/doc/208921
ER -

References

top
  1. [Buch95] W. Buchholz, Proof-theoretic analysis of termination proofs, Annals of Pure and Applied Logic 75, 57-65, (1995). Zbl0844.03031
  2. [CRS94] E. A. Cichon, M. Rusinowitch and S. Selhab, Cut elimination in sequent calculus and rewriting, Rapport CRIN 94-R-038, (1994). 
  3. [CRS96] E. A. Cichon, M. Rusinowitch and S. Selhab, Cut elimination and rewriting: termination proofs, Submitted. 
  4. [Der82] Dershowitz, Orderings for term rewriting systems, Theoretical Computer Science, Vol. 17 (5), 279-301, (1982). Zbl0525.68054
  5. [DJ90] N. Dershowitz and J. P. Jouannaud, Rewrite Systems, in: Handbook of Theoretical Computer Science, J. Van Leeween (ed.), Vol. B, 243-320, Elsevier, Amsterdam, (1990). Zbl0900.68283
  6. [DJS95] V. Danos, J.-B. Joinet and H. Schellinx, A new deconstructive logic: Linear Logic, Preprint 936, Department of Mathematics, Utrecht University, (1995). Zbl0895.03023
  7. [DP96] R. Dyckhoff and L. Pinto, Cut-elimination in a permutation-free sequent calculus for intuitionistic logic, Submitted, (August-1996). 
  8. [Dra88] A. G. Dragalin, Mathematical intuitionism, introduction to proof theory, Vol. 67 of Translations of Mathematical Monographs, 185-199, American Mathematical Society, (1988), (translation of an article that appeared in 1978). 
  9. [Hon96] Hongwei Xi, On Weak and Strong Normalisations, Research report 96-189, Dept. of Mathematical Sciences Carnegie Mellon University, (1996). 
  10. [Gal91] Gallier, What’s so Special about Kruskal’s Theorem and the Ordinal Γ 0 ?, A Survey of Some Results in Proof Theory, Annals of Pure and Applied Logic, Vol. 53, 199-260, (1991). Zbl0758.03025
  11. [Gal93] J. Gallier, Constructive logics part I: a tutorial on proof systems and typed λ-calculi, Theoretical Computer Science, Vol. 110, 249-339, (1993). Zbl0772.03026
  12. [Gen35] G. Gentzen, Investigations into logical deduction, in: Gentzen Collected Works, E. Szabo (ed.), North Holland, (1969). 
  13. [Gen38] G. Gentzen, New version of the consistency proof of elementary number theory, in: Gentzen Collected Works, E. Szabo (ed.), North Holland, (1969). 
  14. [Gir87] J. Y. Girard, Proof theory and logical complexity, Bibliopolis, (1987). 
  15. [GLT89] J. Y. Girard, Y. Lafont and P. Taylor, Proofs and types, Vol. 7 of Cambridge Tracts in Theoretical Computer Science, Cambridge university press, (1989). Zbl0671.68002
  16. [Gra92] B. Gramlich, Relating innermost, weak, uniform and modular termination of term rewriting systems, in: International Conf. on Logic Programming and Automated Reasoning, St. Petersburg, A. Voronkov (ed.), Vol. 624, Lecture Notes in Artificial Intelligence, 285-296, Springer, (1992). 
  17. [Gro93] Ph. de Groote, The conservation theorem revisited, in: International Conf. on Typed Lambda Calculi and applications, Vol. 664, Lecture Notes in Artificial Intelligence, 163-178, Springer, (1993). 
  18. [Her95] H. Herbelin, Séquents qu'on calcule, Thèse de doctorat, Université Paris VII, (1995). 
  19. [HL92] G. Huet and J.-J. Lévy. Computations In Orthogonal Rewrites Systems I, in: Computational Logic: Essays in Honour of Alan Robinson, J. Lassez and G. Plotkin (eds.), chapter 11, 395-414, MIT Press, Cambridge, Massachussets. (1992). 
  20. [Hof92] D. Hofbauer, Termination Proofs by Multiset Path Orderings Imply Primitive Recursive Derivation Lengths, Theoretical Computer Science, Vol. 105 (1), 129-140, (1992). Zbl0759.68045
  21. [Hue80] G. Huet, Confluent reductions: Abstract properties and applications to term rewriting systems, J. Assoc. Comput. Mach. Vol. 27 (4), 797-821, (1980). Zbl0458.68007
  22. [Joi93] J. B. Joinet, Etude de la normalisation du calcul des séquents classique à travers la logique linéaire, Thèse de doctorat, Université Paris VII, (1993). 
  23. [KW94] A. J. Kfoury and J. B. Wells, New notions of reduction and non-semantic proofs of β-strong normalization in typed λ-calculi, Technical Report 94-014, Computer Science Department, Boston University, (1994). 
  24. [KL80] S. Kamin and J. J. Lévy, Two generalizations of the recursive path ordering, unpublished note, Dept. of Computer Science, Univ. of Illinois, Urbana, IL, (1980). 
  25. [Klo80] J. W. Klop, Combinatory reduction systems, PH.D. thesis, CWI, Amsterdamm Mathematical Center Tracts N°. 127. 
  26. [Klo92] J. W. Klop, Term Rewriting Systems, in: Handbook of Logic in Computer Science, S. Abramsky, D. Gabbay, and T. Maibaum (eds.), Vol. 2, chapter 1, 2-117, Clarendon Press, Oxford, (1992). 
  27. [Kru60] J. B. Kruskal, Well-quasi-ordering, the Tree Theorem, and Vazsonyi's conjecture, Trans. Amer. Society, Vol. 95 210-225, (1960). Zbl0158.27002
  28. [Les90] P. Lescanne, Implementation of completion by transition rules + control: ORME, in: Proc. 2nd International Workshop on Algebraic and Logic Programming, Nancy, Vol. 463, Lectures Notes in Computer Science, 262-269, Springer, (1990). 
  29. [MZ94] A. Middeldorp and H. Zantema, Simple Termination Revisited, in: Proc. of the 12th International Conference on Automated Deduction, CADE'94, Nancy, Lecture Notes in Artificial Intelligence 814, pp. 451-465, (1994). 
  30. [Ned73] R. P. Nederpelt, Strong Normalization for a typed lambda calculus with lambda structured types, Ph.D. thesis, Tecnische Hogeschool Eindhoven, (1973). 
  31. [O'D77] M. J. O'Donnell, Computing in systems described by equations, Lecture Notes in Computer Science, Vol. 58. Springer, Berlin, (1977). 
  32. [Pab90] J.-F. Pabion, Cours de logique, D.E.A. Université Claude-Bernard, Lyon-1, (1990). 
  33. [Par92] M. Parigot, λμ-calculus: an algorithmic interpretation of classical natural deduction, Lecture Notes in Computer Science, Vol. 624, 190-201, Springer, (1992). 
  34. [Per82] L. C. P. D. Pereira, On the estimation of the length of normal derivations, Philosophical Studies 4, Akademilitteratur, Stockholm (1982). 
  35. [Pfe94] F. Pfenning, A Structural proof of cut elimination and its representation in a logical framework, report CMU-CS-94-218, Carnegie Mellon University, (1994). 
  36. [Pin93] L. Pinto, Cut formulae and logic programming, in: Extensions of Logic Programming, R. Dyckhoff (ed.), Lecture Notes in Artificial Intelligence, Vol. 798, 282-300, Springer, (1994). 
  37. [Pra65] D. Prawitz, Natural deduction, a proof-theoretical study, Almquist & Wiskell, Stockholm (1965). Zbl0173.00205
  38. [Ros84] H. E. Rose, Subrecursion: functions and hierarchies, Clarendon Press, Oxford, (1984). Zbl0539.03018
  39. [Ros73] B.K. Rosen, Tree-manipulating systems and Church-Rosser theorems, Journal of the ACM, Vol. 20, 160-187, (1973). Zbl0267.68013
  40. [Sch51] K. Schütte, Beweistheoretische Erfassung der Unendlichen Induktion in der Zahlentheorie, Matematische Annalen, Vol. 122, 369-380, (1951). Zbl0042.00803
  41. [Tah92] E. Tahhan Bittar, Gentzen cut elimination for propositional sequent calculus by rewriting derivations, preprint Laboratoire de Logique, d'Algorithmique et d'Informatique de Clermont 1, N°. 16, (1992). 
  42. [Tah94] E. Tahhan Bittar, Bornes recursives pour la terminaison d'algorithmes, thèse de doctorat, Université Lyon1, (1994). 
  43. [Wei93] A. Weiermann, Termination proofs for term rewriting systems by lexicographic path orderings imply multiply recursive derivation lengths, Theoretical Computer Science, Vol. 139(1&2), 355-362, (1995) Zbl0874.68156
  44. [Wei94] A. Weiermann, Complexity Bounds for Some Finite Forms of Kruskal's Theorem, Journal of Symbolic Computation, Vol. 18 (5), 489-495, (1994). 
  45. [Zan92] H. Zantema, Termination of Term Rewriting by Interpretation, technical report, Utrecht University, RUU-CS-92-14, (April-1992). 

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.