decomposition and splitting for NEL

Hi Frogs,

In preparation for the exciting developments in quantum causal evolution, 
we revised the old paper "A System of Interaction and Structure IV: The 
Exponentials" on the normalisation theory of NEL.

Encouraged from referees, we split the paper into two parts, one about 
decomposition and the other about splitting. We think that this makes the 
whole matter clearer and more accessible. Please do not cite the old 
paper, the new ones are better.

Comments of any kind are very welcome.

Best regards,
Alessio and Lutz

----------------------------------------

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

L. Strassburger and A. Guglielmi

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

URL: 
<http://www.lix.polytechnique.fr/Labo/Lutz.Strassburger/papers/NEL-decomposition.pdf>

----------------------------------------

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

A. Guglielmi and L. Strassburger

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

URL: 
<http://www.lix.polytechnique.fr/Labo/Lutz.Strassburger/papers/NEL-splitting.pdf>

----------------------------------------