Does this variant of Multiplicative Linear Logic with mix rule enjoy cut elimination?

Question

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 'real' deadlocks. 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 $ (notation defined in the footnote): $$ \{\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 \}$$

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 \} $$

Example of a deadlock: $a \frown \mu(a,b)$.

Questions:

1. Does the described type system, when applied in an obvious way to the interaction net, eliminates the possibility of deadlocks?
2. Does the type system enjoy cut elimination?
3. Are these two questions equivalent?
4. Are there any publications about it?

Footnote

Notation for the nets:

• Net is a set of links.
• 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',
• $\frown$ is commutative.
• Two connected edges are just an edge: $\{\ldots, a \frown b, b\frown c, \ldots \} \rightsquigarrow \{\ldots, a \frown c, \ldots \}$

Answer 1

For question 1, if by "deadlock" you mean "non-trivial vicious circle", then the answer is obviously yes, simply because a non-trivial vicious circle cannot be typed: you will have a cut between a formula $A$ and a formula $F$ containing $A^\bot$ as strict subformula, so it is impossible that $F=A^\bot$. But this is kind of trivial: by refusing a priori to consider cyclic wires as deadlocks, you are eliminating the only possible typed deadlock, so of course you are deadlock-free...

For question 2, there are definitely problems with your sequent calculus. First, I assume that you are working with orthogonality defined by $(A\cdot B)^\bot=A^\bot\cdot B^\bot$. Then, you have that the formula $A^\bot\cdot A$ is essentially self-dual and, since it is provable, you have a proof of the empty sequent. But your inference rules (except cut) still verify the subformula property, which means that there is no cut-free proof of the empty sequent. In other words, you are forgetting the rule $$\frac{}{\vdash}$$ Without this rule, cut-elimination does not hold. There is a further problem though, namely that you cannot represent the cut-elimination steps inside the sequent calculus: in other words, as a type system, you do not have subject reduction. For that, you need to consider a unary cut rule: $$\frac{\vdash\Gamma,A^\bot,A}{\vdash\Gamma}$$ Note that, like the tensor rule, the binary cut rule is derivable from this one (and mix).

For question 3, I assume that you are asking whether the system captures your notion of deadlock-freedom. Since you are excluding cyclic wires a priori (i.e., you are artifically adding a cut-elimination rule that makes them disappear) the the answer is, again, trivially yes: a net normalizes (with your additional reduction rule) to what Lafont calls a reduced net (no vicious circle, no active pair) iff it is typable in the above system. This is provable by standard arguments: subject reduction/subject expansion and typability of reduced nets.

For question 4, I doubt anyone has published anything because this system is so degenerate that I honestly do not see what its interest may be. In fact, one may further simplify the types by eliminating duality altogether: there is no negation, formulas are just $$A,B::=\alpha\mathrel |A\cdot B$$ and axioms/cuts introduce/eliminate pairs of equal formulas. This system, albeit logically trivial (because of self-duality), has the same normalization property as above. It boils down to the so-called relational semantics of MLL, which is applicable to untyped structures too, in which tensor equals par.

Regarding your search for a Danos-Regnier correctness criterion for single-agent nets, there is not much to be said: if you make cyclic wires disappear "by fiat", then the self-dual "typing" above suffices and correctness criteria play no role; if you stick to the standard definitions, then there can be no meaningful correctness criterion: every one-conclusion net cut with itself generates cyclic wires.