Abstract
This work presents an extension with cuts of Schwichtenberg’s multiary sequent calculus. We identify a set of permutative conversions on it, prove their termination and confluence and establish the permutability theorem. We present our sequent calculus as the typing system of the generalised multiary λ-calculus λ J m, a new calculus introduced in this work. λ J m corresponds to an extension of λ-calculus with a notion of generalised multiary application, which may be seen as a function applied to a list of arguments and then explicitly substituted in another term. Proof-theoretically the corresponding typing rule encompasses, in a modular way, generalised eliminations of von Plato and Herbelin’s head cuts.
Both authors are supported by FCT through the Centro de Matemática da Universidade do Minho, Braga, Portugal
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
R. Dyckhoff and L. Pinto, Permutability of inferences in intuitionistic sequent calculi, Theoretical Computer Science, 212 (1999) 141–155.
J. Espírito Santo, Conservative extensions of the λ-calculus for the computational interpretation of sequent calculus, PhD thesis, University of Edinburgh, 2002.
J. Espírito Santo, An isomorphism between a fragment of sequent calculus and an extension of natural deduction, in: M. Baaz and A. Voronkov (Eds.), Proc. of LPAR’02, 2002, Springer-Verlag, Lecture Notes in Artificial Intelligence, vol. 2514, 354–366.
H. Herbelin, A λ-calculus structure isomorphic to a Gentzen-style sequent calculus structure, in: L. Pacholski and J. Tiuryn (Eds.), Proceedings of CSL’94, 1995, Springer-Verlag, Lecture Notes in Computer Science, vol. 933, 61–75.
F. Joachimski and R. Matthes, Short proofs of normalisation for the simply typed λ-calculus, permutative conversions and Gödel’s T, (accepted for publication in Archive for Mathematical Logic).
G. Pottinger, Normalization as a homomorphic image of cut-elimination, Annals of Mathematical Logic 12 (1977) 323–357.
H. Schwichtenberg, Termination of permutative conversions in intuitionistic Gentzen calculi, Theoretical Computer Science, 212 (1999) 247–260.
J. von Plato, Natural deduction with general elimination rules, Annals of Mathematical Logic, 40 (2001) 541–567.
J. Zucker, The correspondence between cut-elimination and normalization, Annals of Mathematical Logic 7 (1974) 1–112.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Santo, J.E., Pinto, L. (2003). Permutative Conversions in Intuitionistic Multiary Sequent Calculi with Cuts. In: Hofmann, M. (eds) Typed Lambda Calculi and Applications. TLCA 2003. Lecture Notes in Computer Science, vol 2701. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44904-3_20
Download citation
DOI: https://doi.org/10.1007/3-540-44904-3_20
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40332-6
Online ISBN: 978-3-540-44904-1
eBook Packages: Springer Book Archive