4
$\begingroup$

There are various criteria for the correctness of multiplicative proof nets. In Correctness of Multiplicative Proof Nets is Linear, 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?

Improve this question
$\endgroup$
1

1 Answer 1

Reset to default
3
$\begingroup$

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

Improve this answer
$\endgroup$
4
  • $\begingroup$ 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... $\endgroup$
    – Damiano Mazza
    Commented May 18, 2018 at 18:33
  • $\begingroup$ 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\}$ $\endgroup$
    – Łukasz Lew
    Commented May 19, 2018 at 0:29
  • $\begingroup$ 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. $\endgroup$
    – Łukasz Lew
    Commented May 19, 2018 at 0:39
  • 1
    $\begingroup$ Denis Bechet proved that MLL with mix is maximal with respect to acyclicity: 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. $\endgroup$
    – Damiano Mazza
    Commented May 22, 2018 at 8:17

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.