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

Bittar, Elias

Banach Center Publications, Tome 50 (1999), p. 179-225 / Harvested from The Polish Digital Mathematics Library

Résumé

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}}$.

Détail

Publié le : 1999-01-01

Zbl 0945.03083

EUDML-ID : urn:eudml:doc:208921

Bibliographie

[000] [Buch95] W. Buchholz, Proof-theoretic analysis of termination proofs, Annals of Pure and Applied Logic 75, 57-65, (1995). | Zbl 0844.03031

[001] [CRS94] E. A. Cichon, M. Rusinowitch and S. Selhab, Cut elimination in sequent calculus and rewriting, Rapport CRIN 94-R-038, (1994).

[002] [CRS96] E. A. Cichon, M. Rusinowitch and S. Selhab, Cut elimination and rewriting: termination proofs, Submitted.

[003] [Der82] Dershowitz, Orderings for term rewriting systems, Theoretical Computer Science, Vol. 17 (5), 279-301, (1982). | Zbl 0525.68054

[004] [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). | Zbl 0900.68283

[005] [DJS95] V. Danos, J.-B. Joinet and H. Schellinx, A new deconstructive logic: Linear Logic, Preprint 936, Department of Mathematics, Utrecht University, (1995). | Zbl 0895.03023

[006] [DP96] R. Dyckhoff and L. Pinto, Cut-elimination in a permutation-free sequent calculus for intuitionistic logic, Submitted, (August-1996).

[007] [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).

[008] [Hon96] Hongwei Xi, On Weak and Strong Normalisations, Research report 96-189, Dept. of Mathematical Sciences Carnegie Mellon University, (1996).

[009] [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). | Zbl 0758.03025

[010] [Gal93] J. Gallier, Constructive logics part I: a tutorial on proof systems and typed λ-calculi, Theoretical Computer Science, Vol. 110, 249-339, (1993). | Zbl 0772.03026

[011] [Gen35] G. Gentzen, Investigations into logical deduction, in: Gentzen Collected Works, E. Szabo (ed.), North Holland, (1969).

[012] [Gen38] G. Gentzen, New version of the consistency proof of elementary number theory, in: Gentzen Collected Works, E. Szabo (ed.), North Holland, (1969).

[013] [Gir87] J. Y. Girard, Proof theory and logical complexity, Bibliopolis, (1987).

[014] [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). | Zbl 0671.68002

[015] [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).

[016] [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).

[017] [Her95] H. Herbelin, Séquents qu'on calcule, Thèse de doctorat, Université Paris VII, (1995).

[018] [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).

[019] [Hof92] D. Hofbauer, Termination Proofs by Multiset Path Orderings Imply Primitive Recursive Derivation Lengths, Theoretical Computer Science, Vol. 105 (1), 129-140, (1992). | Zbl 0759.68045

[020] [Hue80] G. Huet, Confluent reductions: Abstract properties and applications to term rewriting systems, J. Assoc. Comput. Mach. Vol. 27 (4), 797-821, (1980). | Zbl 0458.68007

[021] [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).

[022] [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).

[023] [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).

[024] [Klo80] J. W. Klop, Combinatory reduction systems, PH.D. thesis, CWI, Amsterdamm Mathematical Center Tracts N°. 127.

[025] [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).

[026] [Kru60] J. B. Kruskal, Well-quasi-ordering, the Tree Theorem, and Vazsonyi's conjecture, Trans. Amer. Society, Vol. 95 210-225, (1960). | Zbl 0158.27002

[027] [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).

[028] [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).

[029] [Ned73] R. P. Nederpelt, Strong Normalization for a typed lambda calculus with lambda structured types, Ph.D. thesis, Tecnische Hogeschool Eindhoven, (1973).

[030] [O'D77] M. J. O'Donnell, Computing in systems described by equations, Lecture Notes in Computer Science, Vol. 58. Springer, Berlin, (1977).

[031] [Pab90] J.-F. Pabion, Cours de logique, D.E.A. Université Claude-Bernard, Lyon-1, (1990).

[032] [Par92] M. Parigot, λμ-calculus: an algorithmic interpretation of classical natural deduction, Lecture Notes in Computer Science, Vol. 624, 190-201, Springer, (1992).

[033] [Per82] L. C. P. D. Pereira, On the estimation of the length of normal derivations, Philosophical Studies 4, Akademilitteratur, Stockholm (1982).

[034] [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).

[035] [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).

[036] [Pra65] D. Prawitz, Natural deduction, a proof-theoretical study, Almquist & Wiskell, Stockholm (1965). | Zbl 0173.00205

[037] [Ros84] H. E. Rose, Subrecursion: functions and hierarchies, Clarendon Press, Oxford, (1984). | Zbl 0539.03018

[038] [Ros73] B.K. Rosen, Tree-manipulating systems and Church-Rosser theorems, Journal of the ACM, Vol. 20, 160-187, (1973). | Zbl 0267.68013

[039] [Sch51] K. Schütte, Beweistheoretische Erfassung der Unendlichen Induktion in der Zahlentheorie, Matematische Annalen, Vol. 122, 369-380, (1951). | Zbl 0042.00803

[040] [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).

[041] [Tah94] E. Tahhan Bittar, Bornes recursives pour la terminaison d'algorithmes, thèse de doctorat, Université Lyon1, (1994).

[042] [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) | Zbl 0874.68156

[043] [Wei94] A. Weiermann, Complexity Bounds for Some Finite Forms of Kruskal's Theorem, Journal of Symbolic Computation, Vol. 18 (5), 489-495, (1994).

[044] [Zan92] H. Zantema, Termination of Term Rewriting by Interpretation, technical report, Utrecht University, RUU-CS-92-14, (April-1992).