formalnets.tex

% \section{A formal account of nets}\label{a-formal-account-of-nets}

The aim of this chapter 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 chapter of this document).

\section{Preliminaries}\label{preliminaries}

\subsection{The short story}\label{the-short-story}

\begin{itemize}
\item
  the general flavor is that of multiport interaction nets;
\item
  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);
\item
  cuts are thus wires rather than cells/links: this fits with the
  intuition of \hyperref[geometry-of-interaction]{geometry of interaction (GoI)},
  but not with the most common presentations of proof nets;
\item
  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;
\item
  when representing proof nets, we introduce axioms explicitly as cells,
  so that axiom-cuts do not vanish.
\end{itemize}

\section{Nets}\label{nets}

\subsection{Wires}\label{wires}

A \emph{wiring} is the data of a finite set \(P\) of ports and of a
partition \({W}\) of \(P\) by pairs (the \emph{wires}): if
\(\{p,q\}\in{W}\), we write \({W}(p)=q\) and \({W}(q)=p\). Hence a
wiring is equivalently given by an involutive permutation \({W}\) of
finite domain \(P\), without fixpoints (forall \(p\), \({W}(p)\not=p\)):
the wires are then the orbits. Another equivalent presentation is to
consider \({W}\) 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
\emph{connection} between two disjoint wirings \(W\) and \(W'\) is a
partial injection \((I,I',f):P\pinj P'\): \(I\subseteq P\),
\(I'\subseteq P'\) and \(f\) is a bijection \(I\cong I'\). We then write
\(W\bowtie_f{{W}'}\) for the wiring obtained by identifying the ports
pairwise mapped by \(f\), and then ``straightening'' the paths thus
obtained to recover wires: notice this might also introduce loops and we
write \(\Inner{W}{W'}_f\) for the number of loops thus appeared.

We describe these operations a bit more formally. Write
\(P = P_0\uplus I\) and \(P' = P_0'\uplus I'\). Then consider the graph
\(W\dblcolon_f{{W}'}\) with vertices in \(P\cup P'\), and such that
there is an edge between \(p\) and \(q\) iff \(q={W}(p)\) or
\(q={W'}(p)\) or \(q=f(p)\) or \(p=f(q)\): in other words,
\(W\dblcolon_f{{W}'}=W\cup W'\cup f\cup f^{-1}\). Vertices in
\(P_0\cup P'_0\) are of degree 1, and the others are of degree 2. Hence
maximal paths in \(W\dblcolon_f{{W}'}\) are of two kinds:
\begin{itemize}
\item straight paths, with both ends in \(P_0\cup P_0'\);
\item cycles, with vertices all in \(I\cup I'\).
\end{itemize}
Then the wires in \(W\bowtie_f{{W}'}\) are the pairs \(\{p,p'\}\) such
that \(p\) and \(p'\) are the ends of a path in \(W\dblcolon_f{{W}'}\).
And \(\Inner{W}{W'}_{f}\) is the number of cycles in
\(W\dblcolon_f{{W}'}\), or more precisely the number of support sets of
cycles (i.e. we forget about the starting vertice of cycles).

\begin{lemma}
Consider three wirings \((P,W)\), \((P',W')\) and
\((P'',W'')\), and two connections \((I,I',f):P\pinj P'\) and
\((J',J'',g):P'\pinj P''\) such that \(I'\cap J'=\emptyset\). Then
\begin{equation*}
(W\bowtie_f W')\bowtie_g W'' = W\bowtie_f(W'\bowtie_g W'')
\end{equation*}
and
\begin{equation*}
\Inner{W}{W'}_{f}+\Inner{(W\bowtie_f{{W}'})}{{W}''}_g = \Inner{W}{(W'\bowtie_g W'')}_f+\Inner{{W}'}{{W}''}_g.
\end{equation*}
\end{lemma}
  
\begin{proof}
The first equation holds because open maximal paths
in \(W\dblcolon_f{W'\bowtie_g}{{W}''}\) correspond with those in
\(W\dblcolon_f{(W'\dblcolon_g{{W}''})}\), hence in
\((W\dblcolon_f W')\dblcolon_g W''\), hence in
\({W\bowtie_f{{W}'}}\dblcolon_g{{W}''}\). The second equation holds
because both sides are two possible writings for the number of loops in
\({(W\dblcolon_f{{W}'})}\dblcolon_g{{W}''}\).
\end{proof}

\subsection{Nets}

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

A \emph{cell} \(c\) with ports in \(P\) is the data of a symbol
\(\sigma\in\Sigma\) and of two disjoint lists of pairwise distinct
ports: \(\alpha(c)\in P^{\alpha(\sigma)}\) is the list of \emph{active}
ports and \(\pi(c)\in P^{\pi(\sigma)}\) is the list of \emph{passive}
ports.

A \emph{net} is the data of a wiring \((P,W)\), of a set \(C\) of
disjoint cells on \(P\), and of a number \(L\in\mathbf N\) (the number
of \emph{loops}). It follows from the definitions that each port
\(p\in P\) appears in exactly one wire and in at most one cell: we say
\(p\) is \emph{free} if it is not part of a cell, and \(p\) is
\emph{internal} otherwise. Moreover, we say \(p\) is \emph{dangling} if
\(p\) is free and \(W(p)\) is internal. We write \(\textrm{fp}(R)\) for
the set of free ports of a net \(R\).

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 \(\lambda\)-terms. More formally, an
\emph{isomorphism} from net \(R\) to net \(R'\) is the data of a
bijection of ports \(\phi:P\cong P'\) and a bijection of cells
\(\psi:C\cong C'\) such that:

\begin{itemize}
\item for all \(p\in P\), \(W'(\phi(p))=\phi(W(p))\);
\item for all \(c\in C\):
  \begin{itemize}
  \item \(\sigma_{\psi(c)}=\sigma_c\),
  \item for all \(i\in\{0,\dotsc,\alpha(\sigma_c)-1\}\), \(\alpha(\psi(c))_i=\phi(\alpha(c)_i)\),
  \item for all \(j\in\{0,\dotsc,\pi(\sigma_c)-1\}\), \(\pi(\psi(c))_j=\phi(\pi(c)_j)\);
  \end{itemize}
\item \(L=L'\).
\end{itemize}

Observe that under these conditions \(\psi\) is uniquely induced by
\(\phi\). We say that the isomorphism \(\phi\) is \emph{nominal} if
moreover \(p\in\textrm{fp}(R)\) implies \(p=\phi(p)\).

\subsection{Subnets}\label{subnets}

We say two nets are disjoint when their sets of ports are. Let \(R\) and
\(R'\) be disjoint nets, and \((I,I',f)\) be a connection between \(W\)
and \(W'\), such that \(I\subseteq \textrm{fp}(R)\) and
\(I'\subseteq \textrm{fp}(R')\). We then write \(R\bowtie_f{R'}\) for
the net with wiring \(W\bowtie_f{W'}\), cells \(C\cup C'\) and loops
\(\Inner{R}{R'}_f=L+L'+\Inner{W}{W'}_f\). We say this connection is
\emph{orthogonal} if \(\Inner{W}{W'}_f=0\), and it is \emph{modular} if
the ports in \(I\cup I'\) are all dangling: a modular connection is
always orthogonal.

We say \(R_0\) is a \emph{subnet} of \(R\), if there exists a net \(R'\)
and a connection \((I,I',f)\) between \(R_0\) and \(R'\) such that
\(R=R_0\bowtie_f{R'}\).

\begin{lemma}
Let $R_0$, $R_1$ and $R'$ be nets such that $R_0$ and $R_1$
are disjoint from $R$,
$(I,I',f)$ be a connection $\textrm{fp}(R_0)\pinj \textrm{fp}(R')$
and $\phi$ an isomorphism $R_0\cong R_1$ such that
$\phi(p)=\phi(p')$ for all $p\in\textrm{fp}(R_0)\setminus I$.
Then $R_0\bowtie_f{R'}$ is nominally isomorphic to
$R_1\bowtie_{f\circ\phi^{-1}}{R'}$.
\end{lemma}

\subsection{Rewriting}\label{rewriting}

A \emph{net rewriting rule} is a pair \((r_0,r_1)\) of nets such that
\(\textrm{fp}(r_0)=\textrm{fp}(r_1)\). Then an instance of this rule is
a pair \((R_0,R_1)\) such that there exist:
\begin{itemize}
\item nets \(R'_0\) and \(R'_1\) isomorphic to \(r_0\) and \(r_1\)
  respectively, namely \(R'_i=\phi_i(r_i)\), so that moreover
  \(\phi_0(p)=\phi_1(p)\) for all \(p\in\textrm{fp}(r_0)\) (in
  particular, \(\textrm{fp}(R'_0)=\textrm{fp}(R'_1)\));
\item a net \(R''\), disjoint from \(R'_0\) and \(R'_1\);
\item a connection \((\textrm{fp}(R'_0),J,f):\textrm{fp}(R'_0)\pinj \textrm{fp}(R'')\);
\end{itemize}
such that each \(R_i\) is nominally isomorphic to \(R'_i\bowtie_f{R''}\).

\subsection{Typing}

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

Then a \emph{typing} for net \(R=(P,W,C)\) is a function
\(\tau:P\to \Theta\) such that:

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

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

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

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

\subsection{Boxes}\label{boxes}

A signature with boxes is the data of a signature \(\Sigma\), together
with a \emph{box arity} \(\beta(\sigma)\) for all symbol
\(\sigma\in\Sigma\).

Then a net on signature with boxes \((\Sigma,\beta)\) is the same as a
net \(R\) on \(\Sigma\) plus, for each cell \(c\) of \(R\), the data
\(\beta(c)\) of a \(\beta(\sigma_c)\)-tuple of nets (with boxes) with
free ports the internal ports of \(c\).


%%% Local Variables:
%%% mode: latex
%%% TeX-master: "main"
%%% End: