[TYPES] connectedness and acyclicity in IMLL proof nets

[Aurelien Pardon]

Dear all,

Has anyone already noticed that a switching of an intuitionistic
multiplicative linear logic (IMLL) proof-structure is acyclic iff it
is connected (in the sense of the Danos-Regnier correctness criterion
of proof nets) ?

A simple corollary is: "An IMLL proof-structure is correct if all its
switchings are connected or acyclic."



Here is a simple proof:

We assume a set of propositional variables V.

IMLL formulas are built from the following syntax:
F ::= v | I | F -o F | F x F
where v is a variable belonging to V, "-o" stands for the linear implication
and "x" for the tensor.

The leaves of a formula F are the occurrences of variables and I's. Its sets of
positive leaves F+ and negative leaves F- are inductively defined by:
v+ = {v}		v- = \emptyset
I+ = {I}		I- = \emptyset
(A x B)+ = A+ + B+	(A x B)- = A- + B-
(A -o B)+ = A- + B+	(A -o B)- = A+ + B-,
where + is coproduct.

As proof-structures on the IMLL sequent

   F1,...,Fn |- F

are in one-to-one correspondence with proof-structures on the sequent

  |- (F1 x ... x Fn) -o F,

one being correct iff the other is, we don't loose generality by
considering only IMLL proof-structures on a single formula.  Such an
IMLL proof-structure is then an IMLL formula together with a "leaf"
function from negative leaves to positive leaves, bijective and
label-preserving on variables.

The graph G = (V,E) of a proof-structure is the "glueing" of the
formula's graph and the leaf function's graph.  More precisely, its
vertices are the leaves and the connectives of the formula; its edges
are the edges of the syntax tree (between connectives or between a
connective and a leaf), plus the edges of the leaf function's graph
(between leaves).

A switching (V,E') of G is obtained by removing one of the two
auxiliary edges of each positive "-o" and negative "x" in G.  This
corresponds to the notion of switching in MLL nets by the translation
from IMLL formulas to MLL formulas: A -o B |----> A* par B (where *
stands for linear negation).

By induction, it is easy to prove that, in an IMLL formula F, there
are as many negative leaves as switched connectives (denoted by F_s)
and one more positive leaf than there are non-switched connectives
(denoted by F_ns).

The induction may be summed up in a table (best viewed with a
fixed-width font):

       |      |F+|   |     |F-|    |        |F_s|       |        |F_ns|      |
------------------------------------------------------------------------------
v      |       1     |      0      |          0         |          0         |
I      |       1     |      0      |          0         |          0         |
A x B  | |A+| + |B+| | |A-| + |B-| |   |A_s| + |B_s|    | |A_ns| + |B_ns| +1 |
A -o B | |A-| + |B+| | |A+| + |B-| | |A_ns| + |B_s| + 1 |   |A_s| + |B_ns|   |

Thus, by induction, we have:

       |  |F-| - |F_s| | |F+| - |F_ns| |
----------------------------------------
v      |        0      |       1       |
I      |        0      |       1       |
A x B  |        0      |       1       |
A -o B |        0      |       1       |

The graph T of the IMLL formula is a tree, thus its number of vertices exceed
its number of edges by one.

G contains exactly |F-| more edges, arising from the leaf function,
than T.  Any switching of G contains exactly |F_s| less edges than G
(one edge of each switched connective is removed).

Thus, any switching (V,E') satisfies that |V| = |E'| + 1.  It is a
well-known result of graph theory that this implies the equivalence
between connectedness and acyclicity.