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 ?