Hostname: page-component-6bf8c574d5-j5c6p Total loading time: 0 Render date: 2025-03-04T12:03:55.640Z Has data issue: false hasContentIssue false
  • English
  • Français

Strong cut-elimination in sequent calculus using Klop's ι-translation and perpetual reductions

Published online by Cambridge University Press:  12 March 2014

Morten Heine Sørensen  and
PaweŁ Urzyczyn
Morten Heine Sørensen
Affiliation:
Formalit, Byenden 32, 4660 Store Heddinge, Denmark, E-mail: [email protected]
PaweŁ Urzyczyn
Affiliation:
University of Warsaw, Institute of Informatics, Banacha2, 02-097 Warszawa, Poland, E-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

There is a simple technique, due to Dragalin. for proving strong cut-elimination for intuitionistic sequent calculus, but the technique is constrained to certain choices of reduction rules, preventing equally natural alternatives. We consider such a natural, alternative set of reduction rules and show that the classical technique is inapplicable. Instead we develop another approach combining two of our favorite tools—Klop's ι-translation and perpetual reductions.

These tools are of independent interest and have proved useful in a variety of settings; it is therefore natural to investigate, as we do here, what they have to offer the field of sequent calculus.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 73 , Issue 3 , September 2008 , pp. 919 - 932
Copyright
Copyright © Association for Symbolic Logic 2008

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

[1]Abadi, M., Cardelli, L., Curien, P.-L., and Lévy, J.-J., Explicit substitutions, Journal of Functional Programming, vol. 1 (1991), no. 4, pp. 375–416.CrossRefGoogle Scholar
[2]Barendregt, H.P., The lambda calculus: Its syntax and semantics, second, revised ed., North-Holland, 1984.Google Scholar
[3]Barthe, G., Hatcliff, J., and Sørensen, M.H., Weak normalization implies strong normalization in a class of non-dependent pure type systems, Theoretical Computer Science, vol. 269 (2001), no. 1-2, pp. 317–361.CrossRefGoogle Scholar
[4]Bonelli, E., Perpetuality in a named lambda calculus with explicit substitutions, Mathematical Structures in Computer Science, vol. 11 (2001), no. 1, pp. 47–90.CrossRefGoogle Scholar
[5]Curien, P.-L and Herbelin, H., The duality of computation, International conference on functional programming, ACM Press, 2000, pp. 233–243.Google Scholar
[6]Dyckhoff, R. and Urban, C., Strong normalization of Herbelin's explicit substitution calculi with substitution propagation, Journal of Logic and Computation, vol. 13 (2003), pp. 59–76.CrossRefGoogle Scholar
[7]Gørtz, I.L., Reuss, S., and Sørensen, M.H., Strong normalization from weak normalization by translation into the lambda-I-calculus, Higher-Order and Symbolic Computation, vol. 16 (2003), no. 3, pp. 253–285.CrossRefGoogle Scholar
[8]Herbelin, H., A λ-calculus structure isomorphic to Gentzen-style sequent calculus structure, Computer science logic 1994 (Pacholski, L. and Tiuryn, J., editors), Lecture Notes in Computer Science, vol. 933, Springer-Verlag, 1995, pp. 61–75.Google Scholar
[9]Ikeda, S. and Nakazawa, K., Strong normalization proofs by CPS-translations, Information Processing Letters, vol. 99 (2006), no. 4, pp. 163–170.CrossRefGoogle Scholar
[10]Kikuchi, K., A direct proof of strong normalization for an extended Herbelin's calculus, Functional and logic programming (Kameyama, Y. and Stuckey, P.J., editors), Lecture Notes in Computer Science, vol. 2998, Springer, 2004, pp. 244–259.CrossRefGoogle Scholar
[11]Kikuchi, K., On a local-step cut-elimination procedure for the intuitionistic sequent calculus, Logic for programming, artificial intelligence, and reasoning, Lecture Notes in Computer Science, vol. 4246, Springer, 2006, pp. 120–134.CrossRefGoogle Scholar
[12]Kikuchi, K. and Lengrand, S., Strong normalisation of cut-elimination that simulates β-reduction, International conference on foundations of software science and computation structures (Amadio, R., editor), Lecture Notes in Computer Science, vol. 4962, Springer-Verlag, 2008, pp. 380–394.Google Scholar
[13]Lengrand, S., Call-by-value, call-by-name, and strong normalization for the classical sequent calculus, Electronic notes in theoretical computer science (Gramlich, B. and Lucas, S., editors), vol. 86, Elsevier, 2003.Google Scholar
[14]Lengrand, S., Induction principles as the foundation of the theory of normalisation: Concepts and techniques, Technical report, PPS Laboratory, Université Paris 7, 2005.Google Scholar
[15]Polonovski, E., Strong normalization of -calculus with explicit substitutions, International conference on foundations of software science and computation structures (Walukiewicz, I., editor), Lecture Notes in Computer Science, vol. 2987, Springer, 2004, pp. 423–437.CrossRefGoogle Scholar
[16]van Raamsdonk, F., Severi, P., Sørensen, M.H.B., and Xi, H., Perpetual reductions in λ-calculus, Information and Computation, vol. 149 (1999), no. 2, pp. 173–225.CrossRefGoogle Scholar
[17]Sørensen, M.H., Strong normalization from weak normalization in typed λ-calculi, Information and Computation, vol. 133 (1997), no. 1, pp. 35–71.CrossRefGoogle Scholar
[18]Sørensen, M.H. and Urzyczyn, P., Lectures on the Curry-Howard isomorphism, Studies in Logic and the Foundations of Mathematics, vol. 149, Elsevier, 2006.Google Scholar
[19]Urban, C. and Bierman, C., Strong normalisation of cut-elimination in classical logic, Fundamenta Informaticae, vol. 45 (2001), no. 1-2, pp. 123–155.Google Scholar
[20]Vestergaard, R. and Wells, J., Cut rules and explicit substitutions, Mathematical Structures in Computer Science, vol. 11 (2001), no. 1, pp. 131–168.CrossRefGoogle Scholar
[21]Xi, H., Weak and strong beta normalisations in typed λ-calculi, Typed Lambda Calculus and Applications (Groote, P. de and Hindley, J.R., editors), Lecture Notes in Computer Science, vol. 1210, Springer-Verlag, 1997, pp. 390–404.CrossRefGoogle Scholar