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

Alessio Guglielmi, L Straburger

Research output: Contribution to journal › Article

13 Citations (Scopus)
60 Downloads (Pure)

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.
Original languageEnglish
Pages (from-to)563-584
Number of pages22
JournalMathematical Structures in Computer Science
Volume21
Issue number3
DOIs
Publication statusPublished - Jun 2011

Fingerprint

Algebra
Cut-elimination
Linear Logic
Decomposition
Express
Chemical analysis
Interaction
Causal Model
Process Algebra
Decomposition Theorem
Turing
Series
Theorem

Cite this

A system of interaction and structure V: the exponentials and splitting. / Guglielmi, Alessio; Straburger, L.

In: Mathematical Structures in Computer Science, Vol. 21, No. 3, 06.2011, p. 563-584.

Research output: Contribution to journal › Article

Guglielmi, A & Straburger, L 2011, 'A system of interaction and structure V: the exponentials and splitting', Mathematical Structures in Computer Science, vol. 21, no. 3, pp. 563-584. https://doi.org/10.1017/S096012951100003X
Guglielmi A, Straburger L. A system of interaction and structure V: the exponentials and splitting. Mathematical Structures in Computer Science. 2011 Jun;21(3):563-584. https://doi.org/10.1017/S096012951100003X
Guglielmi, Alessio ; Straburger, L. / A system of interaction and structure V: the exponentials and splitting. In: Mathematical Structures in Computer Science. 2011 ; Vol. 21, No. 3. pp. 563-584.
@article{085d1ad2ac174227b187961964f3548d,
title = "A system of interaction and structure V: the exponentials and splitting",
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.",
author = "Alessio Guglielmi and L Straburger",
year = "2011",
month = "6",
doi = "10.1017/S096012951100003X",
language = "English",
volume = "21",
pages = "563--584",
journal = "Mathematical Structures in Computer Science",
issn = "0960-1295",
publisher = "Cambridge University Press",
number = "3",

}

TY - JOUR

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

AU - Guglielmi, Alessio

AU - Straburger, L

PY - 2011/6

Y1 - 2011/6

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=79956140311&partnerID=8YFLogxK

UR - http://journals.cambridge.org/action/displayJournal?jid=MSC

U2 - 10.1017/S096012951100003X

DO - 10.1017/S096012951100003X

M3 - Article

VL - 21

SP - 563

EP - 584

JO - Mathematical Structures in Computer Science

JF - Mathematical Structures in Computer Science

SN - 0960-1295

IS - 3

ER -

Access to Document