A formal account of nets - Revision history

Lionel Vaux: /* The short story */

2013-06-25T14:43:20Z

‎The short story

Lionel Vaux: a draft definition of boxes

2012-09-06T09:49:02Z

a draft definition of boxes

Lionel Vaux: fixed missing items (bug in mouliwiki)

2012-09-06T08:50:43Z

fixed missing items (bug in mouliwiki)

Lionel Vaux: various fixes and complements on connections

2012-09-06T08:50:09Z

various fixes and complements on connections

Lionel Vaux: /* Conventions */ … were useless

2012-09-01T07:05:09Z

‎Conventions: … were useless

Lionel Vaux at 11:18, 31 August 2012

2012-08-31T11:18:21Z

Show changes

Lionel Vaux: stub

2012-02-15T16:16:29Z

stub

New page

The aim of this page is to provide a common framework for describing linear
logic proof nets, interaction nets, multiport interaction nets, and the likes,
while factoring most of the tedious, uninteresting details (clearly not the
fanciest page of LLWiki).

== The short story ==

* the general flavor is that of multiport interaction nets;
* cuts are thus wires rather than cells/links:
this fits with the intuition of GoI,
but not with usual presentations of proof nets;
* the top/down or passive/active orientation of cells
is related with the distinction between premisses and conclusions of rules,
(and in that sense, a cut is not a logical rule, but the focus of interaction
between two rules);
* when representing proof nets, we introduce axioms as cells.

== Nets ==

== Plugging ==

=== The particular case of proof-like nets ===

== Rewriting ==

== Boxes ==

@@ Line 11: / Line 11: @@
 * the top/down or passive/active orientation of cells is related with the distinction between premisses and conclusions of rules, (and in that sense, a cut is not a logical rule, but the focus of interaction between two rules);
 * cuts are thus wires rather than cells/links: this fits with the intuition of GoI, but not with the most common presentations of proof nets;
-* because the notion of subnet is not trivial in multiport interaction nets, and to avoid the use of geometric conditions (boxes must not overlap but can be nested), we introduce boxes as particular cells);
+* because the notion of subnet is not trivial in multiport interaction nets, and to avoid the use of geometric conditions (boxes must not overlap but can be nested), we introduce boxes as particular cells;
 * when representing proof nets, we introduce axioms explicitly as cells, so that axiom-cuts do not vanish.
 == Nets ==

@@ Line 11: / Line 11: @@
 * the top/down or passive/active orientation of cells is related with the distinction between premisses and conclusions of rules, (and in that sense, a cut is not a logical rule, but the focus of interaction between two rules);
 * cuts are thus wires rather than cells/links: this fits with the intuition of GoI, but not with the most common presentations of proof nets;
 * when representing proof nets, we introduce axioms explicitly as cells, so that axiom-cuts do not vanish.
 == Nets ==
@@ Line 205: / Line 206: @@
 === Boxes ===
-TODO
+A signature with boxes is the data of a signature <math>\Sigma</math>, together

@@ Line 121: / Line 121: @@
 * for all <math>p\in P</math>, <math>W'(\phi(p))=\phi(W(p))</math>;
 * for all <math>c\in C</math>:
 * <math>L=L'</math>.
 Observe that under these conditions  <math>\psi</math> is uniquely induced by <math>\phi</math>.

@@ Line 104: / Line 104: @@
 is the list of ''passive'' ports.
-A ''net'' is the data of a wiring <math>(P,W)</math> and of a set <math>C</math> of disjoint cells on
+A ''net'' is the data of a wiring <math>(P,W)</math>, of a set <math>C</math> of disjoint cells on
-<math>P</math>. It follows from the definitions that each port <math>p\in P</math> appears in
+<math>P</math>, and of a number <math>L\in\mathbf N</math> (the number of ''loops''). It follows
-exactly one wire and in at most one cell: we say <math>p</math> is ''free'' if it is
+from the definitions that each port <math>p\in P</math> appears in exactly one wire and in
-not part of a cell, and <math>p</math> is ''internal'' otherwise. We write <math>\textrm{fp}(R)</math> for
+at most one cell: we say <math>p</math> is ''free'' if it is not part of a cell, and
-the set of free ports of a net <math>R</math>.
+<math>p</math> is ''internal'' otherwise. Moreover, we say <math>p</math> is ''dangling'' if
 Generally, the “names” of internal ports of a net are not relevant, but free
@@ Line 119: / Line 119: @@
 * for all <math>p\in P</math>, <math>W'(\phi(p))=\phi(W(p))</math>;
 * for all <math>c\in C</math>:
 Observe that under these conditions  <math>\psi</math> is uniquely induced by <math>\phi</math>.
 We say that the isomorphism <math>\phi</math> is ''nominal'' if moreover <math>p\in\textrm{fp}(R)</math>
 implies <math>p=\phi(p)</math>.
-=== Rewriting ===
+=== Subnets ===
 We say two nets are disjoint when their sets of ports are.
@@ Line 130: / Line 131: @@
 <math>I\subseteq \textrm{fp}(R)</math> and <math>I'\subseteq \textrm{fp}(R')</math>.
 We then write <math>R\bowtie_f{R'}</math> for the net
-with wiring <math>W\bowtie_f{W'}</math> and cells
+with wiring <math>W\bowtie_f{W'}</math>, cells
-<math>C\cup C'</math>.
+<math>C\cup C'</math> and loops <math>\Inner{R}{R'}_f=L+L'+\Inner{W}{W'}_f</math>.
 {{Lemma|
@@ Line 142: / Line 143: @@
 <math>R_1\bowtie_{f\circ\phi^{-1}}{R'}</math>.
 }}
 A ''net rewriting rule'' is a pair <math>(r_0,r_1)</math> of nets

@@ Line 12: / Line 12: @@
 * cuts are thus wires rather than cells/links: this fits with the intuition of GoI, but not with the most common presentations of proof nets;
 * when representing proof nets, we introduce axioms explicitly as cells, so that axiom-cuts do not vanish.
 == Nets ==