<p>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 <em>strict</em> subformula, so it is impossible that $F=A^\bot$. But this is kind of trivial: by refusing <em>a priori</em> to consider cyclic wires as deadlocks, you are eliminating the only possible typed deadlock, so of course you are deadlock-free...</p>

<p>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).</p>

<p>For question 3, I assume that you are asking whether the system captures your notion of deadlock-freedom.  Since you are excluding cyclic wires <em>a priori</em> (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 <em>reduced</em> 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.</p>

<p>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 <em>relational semantics</em> of MLL, which is applicable to untyped structures too, in which tensor equals par.</p>

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

CC BY-SA 4.0
2018-05-28T05:42:27.640Z
Damiano, thank you for your answer, I learned from it a lot.
Łukasz Lew
CC BY-SA 4.0
2018-05-30T18:32:27.033Z
Damiano, do you have a paper that you would recommend as a good intro to relational semantics? Preferably in the context of linear logic.
Łukasz Lew
CC BY-SA 4.0
2018-05-31T02:43:08.643Z
Is relation semantics same as  Kripke semantics?
Łukasz Lew
CC BY-SA 4.0
2018-06-01T07:36:24.593Z
The relational semantics is not a *truth* semantics (a semantics of formulas, like Kripke semantics) but a *denotational* semantics (a semantics of *proofs*).  It is sort of a degenerate version of coherence spaces.  Unfortunately there is no formal account of it in the literature, except the appendix of [this paper](https://www.irif.fr/~ehrhard//pub/finite.pdf) by Thomas Ehrhard.  In short, if you take the self-dual version of the system I described and collect all the typings you can give with it to a proof $\pi$, the resulting set is (isomorphic to) the relational semantics of $\pi$.
Damiano Mazza
CC BY-SA 4.0
2018-05-26T06:15:23.400Z
2018-05-26T06:15:23.400Z
Damiano Mazza
<p>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.</p>

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

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

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

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

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

<p>$$ 
\{\ldots, a \frown b, b \frown a, \ldots, \} \rightsquigarrow 
\{\ldots, a \frown a, \ldots \} \rightsquigarrow 
\{\ldots, \ldots \}
$$ </p>

<p>Example of a deadlock: $a \frown \mu(a,b)$.</p>

<p><strong>Questions:</strong></p>

<ol>
<li><em>Does the described type system, when applied in an obvious way to the interaction net, eliminates the possibility of deadlocks?</em></li>
<li><em>Does the type system enjoy cut elimination?</em></li>
<li><em>Are these two questions equivalent?</em></li>
<li><em>Are there any publications about it?</em></li>
</ol>

<p><strong>Footnote</strong></p>

<p>Notation for the nets:</p>

<ul>
<li>Net is a set of links.</li>
<li>Variables denote edges. </li>
<li>$ e \frown \mu(a,b)$ represents an a node $\mu$  with two auxiliary edges $a, b$ and a principal edge $e$.</li>
<li>Each variable is present in the set <em>exactly 1 or 2 times</em>, 1 means it is a 'free edge', </li>
<li>$\frown$ is commutative.</li>
<li>Two connected edges are just an edge: $\{\ldots, a \frown b, b\frown c, \ldots \} \rightsquigarrow \{\ldots, a \frown c, \ldots \}$</li>
</ul>

CC BY-SA 4.0
2018-05-26T02:10:32.100Z
[Related question](https://cstheory.stackexchange.com/questions/40805/is-the-set-of-multiplicative-proof-nets-a-proper-subset-of-set-of-well-formed-si?rq=1) and a relevant [Denis Bechet's paper](http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.2.8039&rep=rep1&type=pdf).
Łukasz Lew
<lo.logic><linear-logic><interaction-nets>
Does this variant of Multiplicative Linear Logic with mix rule enjoy cut elimination?
Łukasz Lew
# Does this variant of Multiplicative Linear Logic with mix rule enjoy cut elimination?

(Asked by: username_0 on 2018-05-25)

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

**Tags:** lo.logic, linear-logic, interaction-nets
> **Comments:**
> **username_0**: [Related question](https://cstheory.stackexchange.com/questions/40805/is-the-set-of-multiplicative-proof-nets-a-proper-subset-of-set-of-well-formed-si?rq=1) and a relevant [Denis Bechet's paper](http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.2.8039&rep=rep1&type=pdf).  

---

## 1 answers

### Answer by username_1 on 2018-05-26. Score: 4 | Accepted answer

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.

> **Comments:**
> **username_0**: Damiano, thank you for your answer, I learned from it a lot.  
> **username_0**: Damiano, do you have a paper that you would recommend as a good intro to relational semantics? Preferably in the context of linear logic.  
> **username_0**: Is relation semantics same as  Kripke semantics?  
> **username_1**: The relational semantics is not a *truth* semantics (a semantics of formulas, like Kripke semantics) but a *denotational* semantics (a semantics of *proofs*).  It is sort of a degenerate version of coherence spaces.  Unfortunately there is no formal account of it in the literature, except the appendix of [this paper](https://www.irif.fr/~ehrhard//pub/finite.pdf) by Thomas Ehrhard.  In short, if you take the self-dual version of the system I described and collect all the typings you can give with it to a proof $\pi$, the resulting set is (isomorphic to) the relational semantics of $\pi$.  

---

