<p>Your observation about cut-elimination being faithfully represented in the unlabelled interaction nets is correct.  However, the answer to your question is no.</p>

<p>Let us call $\delta$ the unique agent of the system. Such an agent is binary; we distinguish its two auxiliary ports by referring to as <em>left</em> and <em>right</em>. We call <em>cell</em> an occurrence of the agent in a net. The interaction rule between two $\delta$ cells $c$ and $d$ is as follows: the two cells disappear and two wires are created, each connecting that which was the left (resp. right) port of $c$ to the left (resp. right) port of $d$.</p>

<p>Consider now the net $\mu$ composed of two $\delta$ cells, call them $c$ and $d$, such that:</p>

<ul>
<li>their principal ports are connected by a wire (there is a cut);</li>
<li>the right auxiliary port of $c$ is connected by a wire with the left auxiliary port of $d$ (there is an axiom between them);</li>
<li>the other two auxiliary ports (the left of $c$ and the right of $d$) are free (in proof net syntax, this means they are connected with two axioms with one free conclusion each).</li>
</ul>

<p>Observe that $\mu$ reduces in one step to a wire (in proof nets syntax, the net reduces in two steps to an axiom).  So the result certainly has no vicious circle.  However, the only sensible way to label $\mu$ (by "sensible" I mean avoiding ill-typed things like a cut between two tensors or between two pars) is to label one delta cell with a tensor and the other with a par, obtaining a net which is not correct: there is a "bad" cycle going through the cut and the axiom connecting the auxilary ports of $c$ and $d$.</p>

CC BY-SA 4.0
2018-05-18T18:33:51.530Z
I hope the description of the net is clear, a picture would be much better (and much more concise) but I can't draw one now.  I will if I have some time later...
Damiano Mazza
CC BY-SA 4.0
2018-05-19T00:29:17.317Z
A concise notation: $ \mu = \{ \delta(e_1,e_2) \frown \delta(e_2,e_3) \} $. Variables denote edges, $e_1$ and $e_3$ are free. Rewrites to $ \mu' = \{ e_1 \frown e_2, e_2 \frown e_3 \} = \{e_1 \frown e_3\}$
Łukasz Lew
CC BY-SA 4.0
2018-05-19T00:39:36.073Z
Thank you Damiano, your counter-example is crisp and useful to me. Are you aware of a "type system" different than MLL that would capture a larger family of correct (normalization, no cycles) single actor interaction nets? I am aware of systems that handle whole abstract part of Lamping algorithm such as "Linear Logic by Levels" etc. but these treat the copying node implicitely and separately  from 'lambda-application' node.
Łukasz Lew
CC BY-SA 4.0
2018-05-22T08:17:04.913Z
Denis Bechet proved that [MLL with mix is maximal with respect to acyclicity](http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.2.8039&rep=rep1&type=pdf): no set of nets strictly containing all correct nets (i.e. proof nets, with mix) can be deadlock-free. In other words, throw in just one non-correct net and you'll immediately get vicious circles.  If by "single actor interaction nets" you mean a system admitting a forgetful functor into the system defined in my answer (only the $\delta$ agent with its annihilation rule), then this puts a serious limitation on what you can do.
Damiano Mazza
CC BY-SA 4.0
2018-05-18T18:02:38.147Z
2018-05-22T08:19:15.687Z
2018-05-22T08:19:15.687Z
Damiano Mazza
<p>There are various criteria for the correctness of multiplicative proof nets.
In <a href="http://lipn.fr/~guerrini/mysite/sites/default/files/biblio/LICS99.pdf" rel="nofollow noreferrer">Correctness of Multiplicative Proof Nets is Linear</a>, Stefano Guerrini nicely describes few of them with an efficient algorithm.</p>

<p>We can erase the difference between par and tensor connectives and treat it as an interaction net with a single node (agent) type.
In such a net we still can perform cut elimination faithfully as the procedure does not depend on the node labeling (by par and tensor). Is that right?</p>

<p>Assuming that's right let's consider the converse problem.
Let's have an interaction net with single agent type that normalizes. Further assume that the normalized net has no vicious cycles.</p>

<p><em>Is it always possible to assign par-tensor labeling to the un-normalized net so that we obtain a correct proof net? Is there an efficient 'labeling' inference algorithm?</em></p>

CC BY-SA 4.0
2018-05-18T07:17:41.527Z
[This question](https://cstheory.stackexchange.com/questions/32083/is-it-possible-to-unambiguously-read-back-%CE%BB-terms-from-interaction-nets-without) might be related.
Łukasz Lew
<linear-logic><interaction-nets>
Is the set of Multiplicative Proof Nets a proper subset of set of well formed single-agent Interaction Nets?
Łukasz Lew
# Is the set of Multiplicative Proof Nets a proper subset of set of well formed single-agent Interaction Nets?

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

There are various criteria for the correctness of multiplicative proof nets.
In [Correctness of Multiplicative Proof Nets is Linear](http://lipn.fr/~guerrini/mysite/sites/default/files/biblio/LICS99.pdf), Stefano Guerrini nicely describes few of them with an efficient algorithm.

We can erase the difference between par and tensor connectives and treat it as an interaction net with a single node (agent) type.
In such a net we still can perform cut elimination faithfully as the procedure does not depend on the node labeling (by par and tensor). Is that right?

Assuming that's right let's consider the converse problem.
Let's have an interaction net with single agent type that normalizes. Further assume that the normalized net has no vicious cycles.

*Is it always possible to assign par-tensor labeling to the un-normalized net so that we obtain a correct proof net? Is there an efficient 'labeling' inference algorithm?*

**Tags:** linear-logic, interaction-nets

> **Comments:**
> **username_0**: [This question](https://cstheory.stackexchange.com/questions/32083/is-it-possible-to-unambiguously-read-back-%CE%BB-terms-from-interaction-nets-without) might be related.  

---

## 1 answers

### Answer by username_1 on 2018-05-18. Score: 3 | Accepted answer

Your observation about cut-elimination being faithfully represented in the unlabelled interaction nets is correct. However, the answer to your question is no.

Let us call $\delta$ the unique agent of the system. Such an agent is binary; we distinguish its two auxiliary ports by referring to as *left* and *right*. We call *cell* an occurrence of the agent in a net. The interaction rule between two $\delta$ cells $c$ and $d$ is as follows: the two cells disappear and two wires are created, each connecting that which was the left (resp. right) port of $c$ to the left (resp. right) port of $d$.

Consider now the net $\mu$ composed of two $\delta$ cells, call them $c$ and $d$, such that:

* their principal ports are connected by a wire (there is a cut);
* the right auxiliary port of $c$ is connected by a wire with the left auxiliary port of $d$ (there is an axiom between them);
* the other two auxiliary ports (the left of $c$ and the right of $d$) are free (in proof net syntax, this means they are connected with two axioms with one free conclusion each).

Observe that $\mu$ reduces in one step to a wire (in proof nets syntax, the net reduces in two steps to an axiom). So the result certainly has no vicious circle. However, the only sensible way to label $\mu$ (by "sensible" I mean avoiding ill-typed things like a cut between two tensors or between two pars) is to label one delta cell with a tensor and the other with a par, obtaining a net which is not correct: there is a "bad" cycle going through the cut and the axiom connecting the auxilary ports of $c$ and $d$.

> **Comments:**
> **username_1**: I hope the description of the net is clear, a picture would be much better (and much more concise) but I can't draw one now.  I will if I have some time later...  
> **username_0**: A concise notation: $ \mu = \{ \delta(e_1,e_2) \frown \delta(e_2,e_3) \} $. Variables denote edges, $e_1$ and $e_3$ are free. Rewrites to $ \mu' = \{ e_1 \frown e_2, e_2 \frown e_3 \} = \{e_1 \frown e_3\}$  
> **username_0**: Thank you Damiano, your counter-example is crisp and useful to me. Are you aware of a "type system" different than MLL that would capture a larger family of correct (normalization, no cycles) single actor interaction nets? I am aware of systems that handle whole abstract part of Lamping algorithm such as "Linear Logic by Levels" etc. but these treat the copying node implicitely and separately  from 'lambda-application' node.  
> **username_1**: Denis Bechet proved that [MLL with mix is maximal with respect to acyclicity](http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.2.8039&rep=rep1&type=pdf): no set of nets strictly containing all correct nets (i.e. proof nets, with mix) can be deadlock-free. In other words, throw in just one non-correct net and you'll immediately get vicious circles.  If by "single actor interaction nets" you mean a system admitting a forgetful functor into the system defined in my answer (only the $\delta$ agent with its annihilation rule), then this puts a serious limitation on what you can do.  

---

