Lionel Vaux: fix wording

2013-06-25T14:41:46Z

fix wording

Olivier Laurent: Link to a formal account of nets.

2012-08-31T15:24:11Z

Link to a formal account of nets.

Lionel Vaux: Blanked the page

2012-08-31T11:17:57Z

Blanked the page

Show changes

Lionel Vaux: Created page with "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 out mos…"

2012-08-30T23:43:00Z

Created page with "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 out mos…"

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 out most of the tedious, uninteresting details (clearly not the
fanciest page of LLWiki).

== Preliminaries ==

=== The short story ===

* the general flavor is that of multiport interaction 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);
* 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.
=== Conventions ===

If <math>A</math> and <math>B</math> are sets, we write <math>A+B</math> for
<math>\{0\}\times A \cup \{1\}\times B</math>.
More generally,
<math>A_0+\cdots+A_n=\{0\}\times A \cup {\cdots} \cup \{n\}\times A_n</math>.
There are natural bijections <math>A+(B+C)\cong A+B+C \cong (A+B)+C</math>.

== Nets ==

=== Wires ===

A ''wiring'' is the data of a finite set <math>P</math> of ports
and of a partition <math>{W}</math> of <math>P</math> by pairs (the ''wires''):
if <math>\{p,q\}\in{W}</math>, we write <math>{W}(p)=q</math> and <math>{W}(q)=p</math>.
Hence a wiring is equivalently given by
an involutive permutation <math>{W}</math> of finite domain <math>P</math>,
without fixpoints (forall <math>p</math>, <math>{W}(p)\not=p</math>): the wires are then
the orbits.
Another equivalent presentation is to consider <math>{W}</math> as
a (simple, loopless, undirected) graph, with vertices in P,
all of degree 1.

We say two wirings are disjoint when their sets of ports are.
A ''connection'' between two disjoint wirings <math>W</math> and <math>W'</math> is
a partial injection <math>(I,I',f):P\pinj P'</math>: <math>I\subseteq P</math>,
<math>I'\subseteq P'</math> and <math>f</math> is a bijection <math>I\leftrightarrow I'</math>.
We then write <math>W\bowtie_f{{W}'}</math> for the wiring obtained
by identifying the ports pairwise mapped by <math>f</math>, and then
``straightening`` the paths thus obtained to recover wires:
notice this might also introduce loops and we write <math>\Inner{W}{W'}_f</math>
for the number of loops thus appeared.

We describe these operations a bit more formally.
Write <math>P = P_0\uplus I</math> and <math>P' = P_0'\uplus I'</math>.
Then consider the graph <math>W\dblcolon_f{{W}'}</math> with vertices in
<math>P\cup P'</math>, and such that
there is an edge between <math>p</math> and <math>q</math> iff
<math>q={W}(p)</math>,
<math>q={W'}(p)</math>,
<math>q=f(p)</math>,
<math>p=f(q)</math>:
in other words, <math>W\dblcolon_f{{W}'}=W\cup W'\cup f\cup f^{-1}</math>.
Vertices in <math>P_0\cup P'_0</math>
are of degree 1, and the others are of degree 2.
Hence maximal paths in <math>W\dblcolon_f{{W}'}</math> are of two kinds:

* straight paths, with both ends in <math>P_0\cup P_0'</math>;
* cycles, with vertices all in <math>I\cup I'</math>.
Then the wires in <math>W\bowtie_f{{W}'}</math> are the pairs <math>\{p,p'\}</math> such that
<math>p</math> and <math>p'</math> are the ends of a path in <math>W\dblcolon_f{{W}'}</math>.
And <math>\Inner{W}{W'}_{f}</math> is the number of
cycles in <math>W\dblcolon_f{{W}'}</math>, or more precisely
the number of support sets of cycles (i.e. we forget about the starting
vertice of cycles).

{{Lemma|
Consider three wirings <math>(P,W)</math>, <math>(P',W')</math> and <math>(P'',W'')</math>,
and two connections <math>(I,I',f):P\pinj P'</math> and
<math>(J',J'',g):P'\pinj P''</math> such that <math>I'\cap J'=\emptyset</math>.
Then

<math> (W\bowtie_f W')\bowtie_g W''=
W\bowtie_f(W'\bowtie_g W'')</math>

and

<math> \Inner{W}{W'}_{f}+\Inner{(W\bowtie_f{{W}'})}{{W}''}_g=
\Inner{W}{(W'\bowtie_g W'')}_f+\Inner{{W}'}{{W}''}_g.</math>
}}

{{Proof|
The first equation holds because open maximal paths in
<math>W\dblcolon_f{W\bowtie_g'}{{W}''}</math> correspond with those in
<math>W\dblcolon_f{(W'\dblcolon_g{{W}''})}</math>, hence in
<math>(W\dblcolon_f W')\dblcolon_g W''</math>, hence in
<math>{W\bowtie_f{{W}'}}\dblcolon_g{{W}''}</math>.
The second equation holds because both sides are two possible writings for
the number of loops in <math>{(W\dblcolon_f{{W}'})}\dblcolon_g{{W}''}</math>
}}

=== Nets ===

A ''signature'' is the data of a set
<math>\Sigma</math> of symbols, together with arity functions
<math>\alpha:\Sigma\to\mathbf{N}\setminus\{0\}</math> (number of
''active'' ports, or conclusions)
and <math>\pi:\Sigma\to\mathbf N</math> (number of
''passive'' ports, or hypotheses).
In the remaining, we assume
such a signature is given.

A ''cell'' <math>c</math> with ports in <math>P</math> is the data of
a symbol <math>\sigma\in\Sigma</math> and of two disjoint lists
of pairwise distinct ports:
<math>\alpha(c)\in P^{\alpha(\sigma)}</math>
is the list of ''active'' ports
and <math>\pi(c)\in P^{\pi(\sigma)}</math>
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
<math>P</math>. It follows from the definitions that each port <math>p\in P</math> appears in
exactly one wire and in at most one cell: we say <math>p</math> is ''free'' if it is
not part of a cell, and <math>p</math> is ''internal'' otherwise. We write <math>\textrm{fp}(R)</math> for
the set of free ports of a net <math>R</math>.

Generally, the “names” of internal ports of a net are not relevant, but free
ports matter most often: internal ports are the analogue of bound variables in
<math>\lambda</math>-terms.
More formally, an ''isomorphism'' from net <math>R</math> to net <math>R'</math>
is the data of a bijection of ports <math>\phi:P\leftrightarrow P'</math> and a bijection
of cells <math>\psi:C\leftrightarrow C'</math> such that:

* 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 ===

We say two nets are disjoint when their sets of ports are.
Let <math>R</math> and <math>R'</math> be disjoint nets, and <math>(I,I',f)</math> be a
connection between <math>W</math> and <math>W'</math>, such that
<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
<math>C\cup C'</math>.

{{Lemma|
Let <math>R_0</math>, <math>R_1</math> and <math>R'</math> be nets such that <math>R_0</math> and <math>R_1</math>
are disjoint from <math>R</math>,
<math>(I,I',f)</math> be a connection <math>\textrm{fp}(R_0)\pinj \textrm{fp}(R')</math>
and <math>\phi</math> an isomorphism <math>R_0\cong R_1</math> such that
<math>\phi(p)=\phi(p')</math> for all <math>p\in\textrm{fp}(R_0)\setminus I</math>.
Then <math>R_0\bowtie_f{R'}</math> is nominally isomorphic to
<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
such that <math>\textrm{fp}(r_0)=\textrm{fp}(r_1)</math>. Then an instance of this rule
is a pair <math>(R_0,R_1)</math> such that there exist:

* a nets <math>R'_0</math> and <math>R'_1</math> isomorphic to <math>r_0</math> and <math>r_1</math> respectively, namely <math>R'_i=\phi_i(r_i)</math>, so that moreover <math>\phi_0(p)=\phi_1(p)</math> for all <math>p\in\textrm{fp}(r_0)</math> (in particular, <math>\textrm{fp}(R'_0)=\textrm{fp}(R'_1)</math>);
* a net <math>R''</math>, disjoint from <math>R'_0</math> and <math>R'_1</math>;
* a connection <math>(\textrm{fp}(R'_0),J,f):\textrm{fp}(R'_0)\pinj \textrm{fp}(R'')</math>;
such that each <math>R_i</math> is nominally isomorphic to
<math>R'_i\bowtie_f{R''}</math>.

=== Typing ===

A typing system on signature <math>\Sigma</math> is the data of a
set <math>\Theta</math> of types, an involutive negation <math>\cdot\orth:\Theta\to\Theta</math>,
together with a typing discipline for each symbol, ''i.e.'' a relation
<math>\Theta(\sigma)\subseteq\Theta^{\alpha(\sigma)}\times\Theta^{\pi(\sigma)}</math>.
We then write <math>A_1,\cdots,A_{\pi(\sigma)}\vdash_\sigma
B_1,\cdots,B_{\alpha(\sigma)}</math> for <math>(\vec A,\vec B)\in\Theta(\sigma)</math>.

Then a ''typing'' for net <math>R=(P,W,C)</math> is a function <math>\tau:P\to \Theta</math>
such that:

* for all <math>p\in P</math>, <math>\tau(W(p))=\tau(p)\orth</math>;
* for all <math>c\in C</math> of symbol <math>\sigma</math>, <math>\tau(\pi(c))\vdash\tau(\alpha(c))\orth</math>;
where, in the last formula, we implicitly generalized
<math>\tau</math> to lists of ports and <math>\cdot\orth</math> to lists of formulas,
in the obvious, componentwise fashion.
The ''interface'' of the typed net <math>(R,\tau)</math> is then
the restriction of <math>\tau</math> to <math>\textrm{fp}(R)</math>.

The idea, is that a wire <math>{p,q}</math>, bears the type <math>\tau(q)</math> (resp. <math>\tau(p)</math>) in
the direction <math>(p,q)</math> (resp. <math>(q,p)</math>), so that a rule
<math>\vec A\vdash_\sigma \vec B</math> reads as an inference from passive inputs (hypotheses)
to active outputs (conclusions).

Observe that if <math>(R,\tau)</math> is a typed net, and
<math>\phi:R\leftrightarrow R'</math> is an isomorphism,
then <math>R'</math> is typed and its interface is <math>\tau\circ\phi^{-1}</math>:
in particular, if <math>\phi</math> is nominal, <math>R'</math> and <math>R</math> have the same interface.

Now let <math>(R,\tau)</math> and <math>(R',\tau')</math> be typed nets
and <math>(I,I',f)</math> a connection so that <math>\tau'\circ f</math> and
<math>\tau\orth=\cdot\orth\circ\tau</math> coincide on <math>I</math>.
Then this induces a typing of <math>R\bowtie_f{R'}</math>
preserving the interface on the remaining free ports.

=== Boxes ===

TODO

← Older revision		Revision as of 14:41, 25 June 2013
Line 1:		Line 1:
−	We can have a look at [[a formal account of nets]], but it is probably not the best way to learn about proof-nets if you have never seen them before.	+	We provide [[a formal account of nets]], but it is probably not the best way to learn about proof-nets if you have never seen them before.

← Older revision	Revision as of 15:24, 31 August 2012
Line 1:	Line 1:
	+	We can have a look at [[a formal account of nets]], but it is probably not the best way to learn about proof-nets if you have never seen them before.

Proof-nets - Revision history

Lionel Vaux: fix wording

Olivier Laurent: Link to a formal account of nets.

Lionel Vaux: Blanked the page

Lionel Vaux: Created page with "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 out mos…"