Hostname: page-component-76fb5796d-vvkck Total loading time: 0 Render date: 2024-04-25T15:55:34.164Z Has data issue: false hasContentIssue false
  • English
  • Français

A system of interaction and structure V: the exponentials and splitting

Published online by Cambridge University Press:  30 March 2011

ALESSIO GUGLIELMI  and
LUTZ STRAßBURGER
ALESSIO GUGLIELMI
Affiliation:
Department of Computer Science, University of Bath, Bath BA2 7AY, United Kingdom Email: alessio@guglielmi.name
LUTZ STRAßBURGER
Affiliation:
INRIA Saclay–Île-de-France and École Polytechnique, Laboratoire d'Informatique (LIX), Rue de Saclay, 91128 Palaiseau Cedex, France Email: lutz@lix.polytechnique.fr
Get access Rights & Permissions [Opens in a new window]

Abstract

System NEL is the mixed commutative/non-commutative linear logic BV augmented with linear logic's exponentials, or, equivalently, it is MELL augmented with the non-commutative self-dual connective seq. NEL is presented in deep inference, because no Gentzen formalism can express it in such a way that the cut rule is admissible. Other recent work shows that system NEL is Turing-complete, and is able to express process algebra sequential composition directly and model causal quantum evolution faithfully. In this paper, we show cut elimination for NEL, based on a technique that we call splitting. The splitting theorem shows how and to what extent we can recover a sequent-like structure in NEL proofs. When combined with a ‘decomposition’ theorem, proved in the previous paper of this series, splitting yields a cut-elimination procedure for NEL.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 21 , Issue 3 , June 2011 , pp. 563 - 584
Copyright
Copyright © Cambridge University Press 2011

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

Abramsky, S. and Jagadeesan, R. (1994) Games and full completeness for multiplicative linear logic. Journal of Symbolic Logic 59 (2)543–574.CrossRefGoogle Scholar
Andreoli, J.-M. (1992) Logic programming with focusing proofs in linear logic. Journal of Logic and Computation 2 (3)297–347.Google Scholar
Blute, R., Panangaden, P. and Straßburger, L. (2008) The logic BV and quantum causality. In: Trends in Logic VI: Logic and the foundations of physics: space, time and quanta.Google Scholar
Blute, R., Panangaden, P. and Slavnov, S. (2009) Deep inference and probablistic coherence spaces.CrossRefGoogle Scholar
Blute, R. F., Guglielmi, A., Ivanov, I. T., Panangaden, P. and Straßburger, L. (2010) A logical basis for quantum evolution and entanglement.Google Scholar
Bruscoli, P. (2002) A purely logical account of sequentiality in proof search. In: Stuckey, P. J. (ed.) Logic Programming, 18th International Conference. Springer-Verlag Lecture Notes in Artificial Intelligence 2401302–316.Google Scholar
Brünnler, K. (2003) Atomic cut elimination for classical logic. In: Baaz, M. and Makowsky, J. A. (eds.) CSL 2003. Mathematical Structures in Computer Science 280386–97.Google Scholar
Brünnler, K. and Tiu, A. (2001) A local system for classical logic. In: Nieuwenhuis, R. and Voronkov, A. (eds.) LPAR 2001. Springer-Verlag Lecture Notes in Artificial Intelligence 2250347–361.Google Scholar
Fleury, A. and Retoré, C. (1994) The mix rule. Mathematical Structures in Computer Science 4 (2)273–285.Google Scholar
Girard, J.-Y. (1987) Linear logic. Theoretical Computer Science 50 1–102.Google Scholar
Girard, J.-Y. (2001) Locus solum: From the rules of logic to the logic of rules. Mathematical Structures in Computer Science 11 (3)301–506.Google Scholar
Guglielmi, A. (2007) A system of interaction and structure. ACM Transactions on Computational Logic 8 (1).Google Scholar
Guglielmi, A. and Gundersen, T. (2008) Normalisation control in deep inference via atomic flows. Logical Methods in Computer Science 4 (1:9)1–36.Google Scholar
Guglielmi, A. and Straßburger, L. (2002) A non-commutative extension of MELL. In: Baaz, M. and Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2002. Springer-Verlag Lecture Notes in Artificial Intelligence 2514231–246.Google Scholar
Guglielmi, A., Gundersen, T. and Parigot, M. (2010a) A proof calculus which reduces syntactic bureaucracy. In: Lynch, C. (ed.) 21st International Conference on Rewriting Techniques and Applications. Leibniz International Proceedings in Informatics (LIPIcs) 6, Schloss Dagstuhl–Leibniz-Zentrum für Informatik 135–150.Google Scholar
Guglielmi, A., Gundersen, T. and Straßburger, L. (2010b) Breaking paths in atomic flows for classical logic. In: Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science (LICS 2010), IEEE Computer Society 284–293.Google Scholar
Guglielmi, A. and Straßburger, L. (2001) Non-commutativity and MELL in the calculus of structures. In: Fribourg, L. (ed.) Computer Science Logic, CSL 2001. Springer-Verlag Lecture Notes in Computer Science 214254–68.Google Scholar
Kahramanoğulları, O. (2004) System BV without the equalities for unit. In: Aykanat, C., Dayar, T. and Körpeoğlu, I. (eds.) 19th International Symposium on Computer and Information Sciences, ISCIS 2004. Springer-Verlag Lecture Notes in Computer Science 3280986–995.Google Scholar
Kahramanoğulları, O. (2006) Reducing nondeterminism in the calculus of structures. In: Hermann, M. and Voronkov, A. (eds.) LPAR 2006. Springer-Verlag Lecture Notes in Artificial Intelligence 4246272–286.Google Scholar
Kahramanoğulları, O. (2008a) System BV is NP-complete. In: deQueiroz, R. Queiroz, R. and Macintyre, A. (eds.) 12th Workshop on Logic, Language, Information and Computation. Annals of Pure and Applied Logic 152 (1-3) 107–121.Google Scholar
Kahramanoğulları, O. (2008b) Interaction and depth against nondeterminism in proof search.Google Scholar
Miller, D. (1996) Forum: A multiple-conclusion specification logic. Theoretical Computer Science 165 201–232.Google Scholar
Okada, M. (1999) Phase semantic cut-elimination and normalization proofs of first- and higher-order linear logic. Theoretical Computer Science 227 (1-2)333–396.Google Scholar
Retoré, C. (1993) Réseaux et Séquents Ordonnés, Ph.D. thesis, Université Paris VII.Google Scholar
Retoré, C. (1997) Pomset logic: A non-commutative extension of classical linear logic. In: deGroote, Ph Groote, Ph. and Hindley, J. R. (eds.) Typed Lambda Calculus and Applications, TLCA'97. Springer-Verlag Lecture Notes in Computer Science 1210300–318.Google Scholar
Straßburger, L. (2003a) Linear Logic and Noncommutativity in the Calculus of Structures, Ph.D. thesis, Technische Universität Dresden.Google Scholar
Straßburger, L. (2003b) MELL in the Calculus of Structures. Theoretical Computer Science 309 (1-3)213–285.Google Scholar
Straßburger, L. (2003c) System NEL is undecidable. In: De Queiroz, R.Pimentel, E. and Figueiredo, L. (eds.) 10th Workshop on Logic, Language, Information and Computation (WoLLIC). Electronic Notes in Theoretical Computer Science 84.Google Scholar
Straßburger, L. and Guglielmi, A. (2009) A system of interaction and structure IV: The exponentials and decomposition.Google Scholar
Tiu, A. (2006) A system of interaction and structure II: The need for deep inference. Logical Methods in Computer Science 2 (2)1–24.Google Scholar