1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
|
\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}
|
