A System of Interaction and Structure IV: The Exponentials and Decomposition

Lutz Strassburger (1) , Alessio Guglielmi (2)

1 PARSIFAL - Proof search and reasoning with logic specifications
2 CALLIGRAMME - Linear logic, proof networks and categorial grammars

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 a basic compositionality property of NEL, which we call decomposition. This result leads to a cut-elimination theorem, which is proved in the next paper of this series. To control the induction measure for the theorem, we rely on a novel technique that extracts from NEL proofs the structure of exponentials, into what we call !-?-Flow-Graphs.

Domaines: Logique en informatique [cs.LO]

Lutz Strassburger, Alessio Guglielmi. A System of Interaction and Structure IV: The Exponentials and Decomposition. ACM Transactions on Computational Logic, 2011, 12 (4), pp.23. ⟨10.1145/1970398.1970399⟩. ⟨inria-00441214⟩