Return to 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 to an axiom, and there would be a further step eliminating a cut on 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$.

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$.

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 them as the the left one and right one. 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 rleft 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 to an axiom, and there would be a further step eliminating a cut on 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 two pars) is to label one delta cell with a tensor and the other with a par, obtaining something which is not correct: there is a "bad" cycle going through the cut and the axiom connecting the auxilary ports of $c$ and $d$.

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 to an axiom, and there would be a further step eliminating a cut on 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$.

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 them as the the left one and right one. 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 occurrences of $\delta$, 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 rleft 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 to an axiom, and there would be a further step eliminating a cut on an axiom). So the result certainly has no vicious circle. However, there is no way to label $\mu$ an obtain a proof net: whatever you do, you will always find a "bad" cycle going through the cut and the axiom connecting the auxilary ports of $c$ and $d$.

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 them as the the left one and right one. 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 rleft 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 to an axiom, and there would be a further step eliminating a cut on 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 two pars) is to label one delta cell with a tensor and the other with a par, obtaining something which is not correct: there is a "bad" cycle going through the cut and the axiom connecting the auxilary ports of $c$ and $d$.