Skip to main content
3 of 4
deleted 9 characters in body
Damiano Mazza
  • 5.6k
  • 1
  • 25
  • 36

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

Damiano Mazza
  • 5.6k
  • 1
  • 25
  • 36