Return to Question

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:

• Does the described type system, when applied in an obvious way to the interaction net, eliminates the possibility of deadlocks?
• Does the type system enjoy cut elimination?
• Are these two questions equivalent?
• 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 \}$

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

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 vicious ones. 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 $: $$ \{\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 \}$$

In this notation:

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

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

Does the described type system, when applied in an obvious way to the interaction net, eliminates the possibility of deadlocks?

Does the type system enjoy cut elimination?

Are these two questions equivalent?

Are there any publications about it?

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:

• Does the described type system, when applied in an obvious way to the interaction net, eliminates the possibility of deadlocks?
• Does the type system enjoy cut elimination?
• Are these two questions equivalent?
• 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 \}$

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 vicious ones. 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 $: $$ \{\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 \}$$

In this notation:

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

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

Does the described type system, when applied in an obvious way to the interaction net, eliminates the possibility of deadlocks? Example of a deadlock: $a \frown \mu(a,b)$ ?

Does the type system enjoy cut elimination?

Are these two questions equivalent?

Are there any publications about it ?

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 vicious ones. 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 $: $$ \{\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 \}$$

In this notation:

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

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

Does the described type system, when applied in an obvious way to the interaction net, eliminates the possibility of deadlocks?

Does the type system enjoy cut elimination?

Are these two questions equivalent?

Are there any publications about it?