A System of Interaction and Structure V: The Exponentials and Splitting - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Pré-Publication, Document De Travail Année : 2009

A System of Interaction and Structure V: The Exponentials and Splitting

Résumé

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. System NEL is Turing-complete, it is able to directly express process algebra sequential composition and it faithfully models causal quantum evolution. In this paper, we show cut elimination for NEL, based on a property that we call splitting. NEL is presented in the calculus of structures, which is a deep-inference formalism, because no Gentzen formalism can express it analytically. The splitting theorem shows how and to what extent we can recover a sequent-like structure in NEL proofs. Together with the decomposition theorem, proved in the previous paper of the series, this immediately leads to a cut-elimination theorem for NEL.
Fichier principal
Vignette du fichier
NEL-splitting.pdf (311.33 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

inria-00441254 , version 1 (15-12-2009)
inria-00441254 , version 2 (28-01-2015)

Identifiants

  • HAL Id : inria-00441254 , version 1

Citer

Alessio Guglielmi, Lutz Strassburger. A System of Interaction and Structure V: The Exponentials and Splitting. 2009. ⟨inria-00441254v1⟩
373 Consultations
285 Téléchargements

Partager

Gmail Facebook X LinkedIn More