From 5773af85890aef972f30b3c05caefb5c174fa827 Mon Sep 17 00:00:00 2001 From: gsv Date: Tue, 1 Oct 2024 15:28:18 +0300 Subject: [PATCH 1/3] [README] Breaf introduction to interaction nets. --- README.md | 51 +++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 51 insertions(+) diff --git a/README.md b/README.md index b0ada21..556b262 100644 --- a/README.md +++ b/README.md @@ -28,3 +28,54 @@ We use [Fourmolu](https://fourmolu.github.io/) as a formatter for Haskell source Our editor of choice is [VS Code](https://code.visualstudio.com/) with following extensions: - [Haskell](https://marketplace.visualstudio.com/items?itemName=haskell.haskell) + +## Interaction nets + +We use a variation of interaction nets that was proposer by Yves Lafont in 1989 in the paper ["Interaction nets"](https://dl.acm.org/doi/10.1145/96709.96718) as a base for our project. +Below we introduce basic definitions and discuss some assumptions that we use. + +Let $\Sigma$ is an alphabet of **agents**. +Let $Ar: \Sigma \to \mathbb{N}$ is an **arity function**. +We suppose that $0 \in \mathbb{N}$. +Each agent $l \in \Sigma$ has a one **primary port** and $Ar(l)$ **secondary ports**: $Ar(l) + 1$ ports in total. + +**Network** $\mathcal{n}$ over alphabet $\Sigma$ is an undirected graph where +- Each vertex is labelled with an agent and contains respective number of ports. +- Each edge is a connection between ports. +- Each port can be connected with not more then one port. + +$\mathcal{N}_{\Sigma}$ is a set of all possible networks over $\Sigma$. + +**Note** +- Network can contains ports that do not connected to other ports. The port without connection is a **free port**. $\mathcal{I}(\mathcal{n})$ is set of free ports of network $\mathcal{n}$ or an **interface of the network $\mathcal{n}$**. +- Network can consists of edges only. In this case, each end of edge is a free port. +- Network without vertices and edges is an **empty network**. + +The pair of nodes $a$ and $b$ that connected via primary ports (there is an edge that connects primary port of $a$ with primary port of $b$) is an **active pair**. +We use $a \bowtie b$ to denote that $a$ and $b$ is an active pair. + +Network $\mathcal{n}$ is in **normal form** if there is no active pairs in $\mathcal{n}$. + +**Reduction rule** $r \in \Sigma \times \Sigma \times \mathcal{N}_{\Sigma}$ is graph rewriting rule. +$\mathcal{R}$ is a set of reduction rules. +- If $(l_1,l_2,\mathcal{n}) \in \mathcal{R}$ then $(l_2, l_1,\mathcal{n}) \in \mathcal{R}$. +- If $(l_1,l_2,\mathcal{n}_1) \in \mathcal{R}$ and $(m_1, m_2,\mathcal{n}_2) \in \mathcal{R}$ then $(l_1,l_2) \neq (m_1,m_2)$. +- For all $(l_1,l_2,\mathcal{n}) \in \mathcal{R}$, $\mathcal{n}$ is in normal form. +- For all $(l_1,l_2,\mathcal{n}) \in \mathcal{R}$, $Ar(l_1) + Ar(l_2) = |\mathcal{I}(\mathcal{n})|$. + +Computation is an application of rewriting rules to active pairs. +If there is an active pair $a \bowtie b$ in network $\mathcal{n_0}$, where +- $a$ is labelled with $l_1$ +- $b$ is labelled with $l_2$ +- $r = (l_1, l_2, \mathcal{m}) \in \mathcal{R}$ + +then we can replace $a \bowtie b$ with $\mathcal{m}$ and get new network $\mathcal{n_1}$. +Thus, computation is a sequence of steps of the form $\mathcal{n_i} \xrightarrow{r} \mathcal{n_{i+1}}$. +Computation finishes when network in normal form. + +Active pair $a \bowtie b$ is **realizable** if there is a sequence + +$\mathcal{n_0} \xrightarrow{r_0} \ldots \xrightarrow{r_{k-1}} \mathcal{n_k} \ \ $ + +, $r_i \in \mathcal{R}$, such that $\mathcal{n}_k$ contains $a \bowtie b$. +We assume that for the given network $\mathcal{n}$ and rules set $\mathcal{R}$, $\mathcal{R}$ contains rules for all **realizable** active pairs. From 74408711e4771ed2638526eb8d6ad35093ddf92a Mon Sep 17 00:00:00 2001 From: gsv Date: Wed, 2 Oct 2024 16:11:09 +0300 Subject: [PATCH 2/3] [README] Math layout. --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 556b262..4d389f3 100644 --- a/README.md +++ b/README.md @@ -75,7 +75,7 @@ Computation finishes when network in normal form. Active pair $a \bowtie b$ is **realizable** if there is a sequence -$\mathcal{n_0} \xrightarrow{r_0} \ldots \xrightarrow{r_{k-1}} \mathcal{n_k} \ \ $ +$$\mathcal{n_0} \xrightarrow{r_0} \ldots \xrightarrow{r_{k-1}} \mathcal{n_k},$$ , $r_i \in \mathcal{R}$, such that $\mathcal{n}_k$ contains $a \bowtie b$. We assume that for the given network $\mathcal{n}$ and rules set $\mathcal{R}$, $\mathcal{R}$ contains rules for all **realizable** active pairs. From 896007caa4779bf8401fd47a279261e144525ddb Mon Sep 17 00:00:00 2001 From: Semyon Date: Wed, 2 Oct 2024 16:32:47 +0300 Subject: [PATCH 3/3] [README] Obsolete comma. Co-authored-by: Nikolai Ponomarev --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 4d389f3..421e34f 100644 --- a/README.md +++ b/README.md @@ -77,5 +77,5 @@ Active pair $a \bowtie b$ is **realizable** if there is a sequence $$\mathcal{n_0} \xrightarrow{r_0} \ldots \xrightarrow{r_{k-1}} \mathcal{n_k},$$ -, $r_i \in \mathcal{R}$, such that $\mathcal{n}_k$ contains $a \bowtie b$. +$r_i \in \mathcal{R}$, such that $\mathcal{n}_k$ contains $a \bowtie b$. We assume that for the given network $\mathcal{n}$ and rules set $\mathcal{R}$, $\mathcal{R}$ contains rules for all **realizable** active pairs.