\section{Interaction Nets}
\label{sec:interaction-nets}

\textit{Interaction Nets} (IN), introduced by Lafont~\cite{lafont1990interactionnets}, are a
graphical model of computation based on graph rewriting.

\subsection{Basic Concepts}
An IN is an undirected graph with labeled 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 connected to $x, y, z$ wires.}
	\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 an $\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 IN proceeds by rewriting the net using local \emph{interaction rules}. A rule
is defined only for an active pair, and for any pair of symbols, 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 the Peano addition rule.}
	\label{fig:rule-concrete-zero}
\end{figure}

\subsection{Properties}
IN possesses the following properties:
\begin{itemize}
	\item \textbf{Locality}: only active pairs can be rewritten.
	\item \textbf{Linearity}: each interaction rule rewrites a constant-size subgraph, independent of
		the overall size of the net.
	\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}