background

1 files changed, 72 insertions, 1 deletions

diff --git a/chapters/background/02-interaction-nets.tex b/chapters/background/02-interaction-nets.tex
index 268e441..36a7a32 100644
--- a/chapters/background/02-interaction-nets.tex
+++ b/chapters/background/02-interaction-nets.tex
@@ -1,4 +1,75 @@
 \section{Interaction Nets}
 \label{sec:interaction-nets}
 
-% This section introduces Interaction Nets
+Interaction Nets, introduced by Yves Lafont et al.~\cite{lafont1990interactionnets}, are a
+graphical model of computation based on graph rewriting.
+
+\subsection{Basic Concepts}
+An interaction net is an undirected graph with labelled vertices, called \textit{agents}. Each agent
+is an instance of a \textit{symbol}, which has a principal port and a fixed number of auxiliary ports:
+\begin{figure}[H]
+	\centering
+	\begin{tikzpicture}
+		\inetcell[arity=2](A){\textit{Add}}[90]
+		\inetwirefree(A.pax 1) \inetwirefree(A.pax 2) \inetwirefree(A.pal)
+		\node[left] at (A.above pax 1) {$\mathit{z}$};
+		\node[left] at (A.above pax 2) {$\mathit{y}$};
+		\node[right] at (A.above pal) {$\mathit{x}$};
+	\end{tikzpicture}
+	\caption{Example of an agent \textit{Add} with two auxiliary ports.}
+	\label{fig:agent}
+\end{figure}
+
+Each port can be wired to at most one other port. When two different agents are wired to their respective principal ports they are called an \textit{active pair}:
+
+\begin{figure}[H]
+	\centering
+	\begin{tikzpicture}
+		\inetcell[arity=2](A){\textit{Add}}[90]
+		\inetcell[arity=1, right=of A.pal](S){\textit{S}}[-90]
+		\inetwire(A.pal)(S.pal)
+		\inetwirefree(A.pax 1) \inetwirefree(A.pax 2) \inetwirefree(S.pax)
+		\node[left] at (A.above pax 1) {$\mathit{z}$};
+		\node[left] at (A.above pax 2) {$\mathit{y}$};
+		\node[right] at (S.above pax) {$\mathit{x}$};
+	\end{tikzpicture}
+	\caption{Example of an active pair, where a $\mathit{Add}$ agent and an $\mathit{S}$ agent are connected via their principal ports.}
+	\label{fig:active-pair}
+\end{figure}
+
+\subsection{Interaction Rules}
+Computation in interaction nets proceeds by rewriting the net using local \emph{interaction rules}. A rule
+is defined only for an active pair and, for any pair of agent types, there is at most one
+interaction rule.
+
+\begin{figure}[H]
+	\centering
+	\interactionrule{
+		\inetcell[arity=2](A){\textit{Add}}[90]
+		\inetcell[arity=1, right=of A.pal](S){\textit{S}}[-90]
+		\inetwire(A.pal)(S.pal)
+		\inetwirefree(A.pax 1) \inetwirefree(A.pax 2) \inetwirefree(S.pax)
+		\node[left] at (A.above pax 1) {$\mathit{z}$};
+		\node[left] at (A.above pax 2) {$\mathit{y}$};
+		\node[right] at (S.above pax) {$\mathit{x}$};
+	}{
+		\inetcell[arity=2](A){\textit{Add}}[90]
+		\inetcell[arity=1, left=of A.pax 1](S){\textit{S}}[-90]
+		\inetwire(A.pax 1)(S.pax)
+		\inetwirefree(A.pal) \inetwirefree(A.pax 2) \inetwirefree(S.pal)
+		\node[right] at (A.above pal) {$\mathit{x}$};
+		\node[left] at (A.above pax 2) {$\mathit{y}$};
+		\node[left] at (S.above pal) {$\mathit{z}$};
+	}
+	\caption{Interaction rule for $\mathit{S}$ and $\mathit{Add}$ that emulates Peano addition rule.}
+	\label{fig:rule-concrete-zero}
+\end{figure}
+
+\subsection{Properties}
+Interaction nets possess the following properties:
+\begin{itemize}
+	\item \textbf{Locality}: only active pairs can be rewritten.
+	\item \textbf{Linearity}: each interaction rule can be applied in constant time.
+	\item \textbf{Strong Confluence}: given a net $\text{IN}$ that can reduce to $\text{IN}_1$ and $\text{IN}_2$ in one
+		step, then both $\text{IN}_1$ and $\text{IN}_2$ reduce to some net $\text{IN}'$ in one step.
+\end{itemize}