In Multiplicative Linear Logic (MLL), addition of the mix rule eliminates 'connectedness' from Danos-Regnier criterion. I'm investigating how the criterion changes if we do not distinguish between tensor and par.

Let's take a MLL inference rules with the mix rule and forget the difference between tensor and par:

$$ \frac{}{\vdash A, A^\bot} \;\mathtt{id} $$ $$ \frac{\vdash \Gamma_1, A\quad \vdash \Gamma_2, A^\bot}{\vdash \Gamma_1, \Gamma_2} \;\mathtt{cut} $$ $$ \frac{\vdash \Gamma_1 \quad \vdash \Gamma_2}{\vdash \Gamma_1, \Gamma_2} \;\mathtt{mix}$$ $$ \frac{\vdash \Gamma, A, B}{\vdash \Gamma, A \cdot B} \;\mathtt{par}$$ The tensor rule is obsolete as it can be derived from the mix and par rules: $$ \frac{\vdash \Gamma_1, A\quad \vdash \Gamma_2, B}{\vdash \Gamma_1, \Gamma_2, A \cdot B} \;\mathtt{tensor} $$

My intuition is that not all proof-structures are valid i.e. some variant of Danos-Regnier criterion for this system still is necessary. The intuition is that it admits cycles but only the trivial ones, not vicious ones. But I don't know how to formalize it, so I'll move to cut elimination formalization.

The above, might be considered a type system for an interaction net with a single self-annihilating node $ \mu $: $$ \{\ldots, e \frown \mu (a_1, a_2), e \frown \mu (b_1, b_2), \ldots, \} \rightsquigarrow \{\ldots, a_1 \frown b_1, a_2 \frown b_2, \ldots \}$$

In this notation:

• Variables denote edges.
• $ e \frown \mu(a,b)$ represents an a node $\mu$ with two auxiliary edges $a, b$ and a principal edge $e$.
• Each variable is present in the set exactly 1 or 2 times, 1 means it is a 'free edge',

Let's extend standard cut-elimination procedure with one more rule: the trivial cycle, made from identity and cut only, disappears:

$$ \{\ldots, a \frown b, b \frown a, \ldots, \} \rightsquigarrow \{\ldots, a \frown a, \ldots \} \rightsquigarrow \{\ldots, \ldots \} $$

Does the described type system, when applied in an obvious way to the interaction net, eliminates the possibility of deadlocks? Example of a deadlock: $a \frown \mu(a,b)$ ?

Does the type system enjoy cut elimination?

Are these two questions equivalent?

Are there any publications about it ?