相互作用ネットワーク

インタラクションネットは、フランスの数学者イヴ・ラフォンが1989年に考案した計算のグラフィカルモデルであり^{[ 1 ]、}線形論理の証明構造の一般化として考案されました。インタラクションネットシステムは、エージェントタイプのセットとインタラクションルールのセットによって指定されます。インタラクションネットは、計算がインタラクションネットの多くの部分で同時に実行でき、同期が不要であるという意味で、本質的に分散型の計算モデルです。後者は、この計算モデルにおける還元の強力な合流特性によって保証されます。したがって、インタラクションネットは、大規模並列処理のための自然言語を提供します。インタラクションネットは、効率的な閉包還元^{[ 2 ]や、レヴィの意味で最適なラムダスコープ[ 3 ]}など、ラムダ計算の多くの実装の中核を成しています。

インタラクションネットは、エージェントとエッジから構成されるグラフのような構造です。

タイプのエージェント${\displaystyle \alpha }$そしてアリティと共に$\displaystyle ar(\alpha )=n\geq 0$主要港が1つあり、${\displaystyle n}$補助ポート。どのポートも最大で1つのエッジに接続できます。どのエッジも正確に2つのポートに接続されます。どのエッジにも接続されていないポートはフリーポートと呼ばれます。フリーポートはまとめて相互作用ネットのインターフェースを形成します。すべてのエージェントタイプはセットに属します。${\displaystyle \Sigma }$署名と呼ばれる。

エッジのみで構成される相互作用ネットワークは配線と呼ばれ、通常は次のように表記されます。${\displaystyle \omega }$木​${\displaystyle t}$その根とともに${\displaystyle x}$帰納的にエッジとして定義される${\displaystyle x}$または代理人として${\displaystyle \alpha }$自由主要港を有する${\displaystyle x}$および補助ポート${\displaystyle x_{i}}$他の木の根とつながっている$t_i$。

相互作用ネットワークの基本的な構造は、図式的に以下のように表すことができます。

2 つのエージェントがそれぞれの主ポートで相互に接続されると、アクティブ ペアが形成されます。アクティブ ペアの場合、アクティブ ペアが別の相互作用ネットに書き換える方法を記述する相互作用ルールを導入できます。アクティブ ペアのない相互作用ネットは、正規形式であると言われます。${\displaystyle \Sigma }$（と${\displaystyle {\text{ar}}:\Sigma \rightarrow \mathbb {N} }$エージェントに対して定義された一連の相互作用ルールとともに、その上で定義されたもの${\displaystyle \alpha \in \Sigma }$これらは一体となって相互作用システムを構成する。

相互作用ネットワークのテキスト表現は相互作用計算^{[ 4 ]}と呼ばれ、プログラミング言語と見なすことができる。

帰納的に定義された木は、次の用語に対応します。${\displaystyle t::=\alpha (t_{1},\dots ,t_{n})\ |\ x}$相互作用計算において、${\displaystyle x}$それは名前と呼ばれます。

あらゆる相互作用ネットワーク${\displaystyle N}$前述の配線とツリープリミティブを使用して、以下のように再描画できます。

これは相互作用計算において構成に対応する

${\displaystyle c\equiv \langle t_{1},\dots ,t_{m}\ |\ v_{1}=w_{1},\dots ,v_{n}=w_{n}\rangle }$、

どこ$t_i$、${\displaystyle v_{i}}$、 そして${\displaystyle w_{i}}$は任意の項です。順序付けられたシーケンス$t_1,...,t_m$左側はインターフェースと呼ばれ、右側には順序付けされていない方程式の多重集合が含まれる。${\displaystyle v_{i}=w_{i}}$配線${\displaystyle \omega }$これは名前に変換され、各名前は構成内で正確に2回出現する必要があります。

まるで${\displaystyle \lambda }$-計算、相互作用計算には、${\displaystyle \alpha }$-変換と置換は構成上で自然に定義されます。具体的には、任意の名前の出現箇所は、後者が特定の構成に存在しない場合、新しい名前に置き換えることができます。構成は、以下の範囲で同等とみなされます。${\displaystyle \alpha }$-変換。次に、置換${\displaystyle t[x:=u]}$名前を置き換えた結果${\displaystyle x}$学期中${\displaystyle t}$別の用語で${\displaystyle u}$もし${\displaystyle x}$用語にちょうど 1 回出現します${\displaystyle t}$。

あらゆる相互作用ルールは、以下のように図式的に表現できます。

どこ${\displaystyle \alpha ,\beta \in \Sigma }$、そして相互作用ネットワーク${\displaystyle N}$右側は、配線とツリープリミティブを使用して再描画され、相互作用計算に変換されます。${\displaystyle \alpha [v_{1},\dots ,v_{m}]\bowtie \beta [w_{1},\dots ,w_{n}]}$ラフォン記法を用いる。

相互作用計算では、相互作用ネット上で定義されたグラフ書き換えから得られるよりも詳細に構成上の縮小を定義します。つまり、${\displaystyle \alpha [v_{1},\dots ,v_{m}]\bowtie \beta [w_{1},\dots ,w_{n}]}$以下の削減：

$\displaystyle \langle {\vec {t}}\ |\ \alpha (t_{1},\dots ,t_{m})=\beta (u_{1},\dots ,u_{n}),\Delta \rangle \rightarrow \langle {\vec {t}}\ |\ t_{1}=v_{1},\dots ,t_{m}=v_{m},u_{1}=w_{1},\dots ,u_{n}=w_{n},\Delta \rangle }$

相互作用と呼ばれる。方程式の1つが次の形式である場合${\displaystyle x=u}$間接参照を適用することで、名前の別の出現箇所を置き換えることができます。${\displaystyle x}$ある意味で${\displaystyle t}$:

${\displaystyle \langle \dots t\dots \ |\ x=u,\Delta \rangle \rightarrow \langle \dots t[x:=u]\dots \ |\ \Delta \rangle }$ または ${\displaystyle \langle {\vec {t}}\ |\ x=u,t=w,\Delta \rangle \rightarrow \langle {\vec {t}}\ |\ t[x:=u]=w,\Delta \rangle }$。

方程式${\displaystyle x=t}$デッドロックと呼ばれるのは、${\displaystyle x}$用語で発生する${\displaystyle t}$一般的には、デッドロックのない相互作用ネットのみが考慮されます。相互作用と間接性は、構成上の縮約関係を定義します。構成が${\displaystyle c}$通常の形態に縮小する${\displaystyle c'}$方程式が残っていない場合は、次のように表されます。${\displaystyle c\downarrow c'}$。

相互作用ネットワークは、以下の特性から恩恵を受ける。

• 局所性（アクティブなペアのみが書き換え可能）
• 線形性（各相互作用ルールは一定時間内に適用できる）
• 強い合流はワンステップダイヤモンド特性としても知られています（もし${\displaystyle c\rightarrow c_{1}}$そして${\displaystyle c\rightarrow c_{2}}$、 それから${\displaystyle c_{1}\rightarrow c'}$そして${\displaystyle c_{2}\rightarrow c'}$一部の人にとって${\displaystyle c'}$)

これらの特性が相まって、大規模な並列処理が可能となる。

他のあらゆる相互作用システムをシミュレートできる最も単純な相互作用システムの1つは、相互作用コンビネータです。そのシグネチャは${\displaystyle \Sigma =\{\epsilon ,\delta ,\gamma \}}$と$\displaystyle \text{ar}}(\epsilon )=0}$そして${\displaystyle {\text{ar}}(\delta )={\text{ar}}(\gamma )=2}$。 エージェント${\displaystyle \epsilon }$リソースを削除する消しゴムと見なすことができる。${\displaystyle \delta }$複製機として。${\displaystyle \gamma }$コンストラクタとして、2 つのリソースを受け取り、3 番目のリソースを返します。加算や乗算などの二項演算から、ラムダ計算における一般的な関数適用まで、あらゆるものを表現できます。${\displaystyle f}$そして${\displaystyle x}$生産する${\displaystyle f\,x}$^{[ 5 ]}これらのエージェントの相互作用ルールは次のとおりです。

• ${\displaystyle \epsilon \bowtie \alpha [\epsilon ,\dots ,\epsilon ]}$消去と呼ばれる。
• ${\displaystyle \delta [\alpha (x_{1},\dots ,x_{n}),\alpha (y_{1},\dots ,y_{n})]\bowtie \alpha [\delta (x_{1},y_{1}),\dots ,\delta (x_{n},y_{n})]}$重複と呼ばれる。
• ${\displaystyle \delta [x,y]\bowtie \delta [x,y]}$そして${\displaystyle \gamma [x,y]\bowtie \gamma [y,x]}$消滅と呼ばれる。

消去と複製のルールは、図式的に以下のように表すことができます。

非終結型の相互作用ネットワークで、自身に還元されるものの例を示す。相互作用計算における対応する構成から始まるその無限還元シーケンスは以下のとおりである。

${\displaystyle {\begin{aligned}&\langle \varnothing \ |\ \delta (\epsilon ,x)=\gamma (x,\epsilon )\rangle \rightarrow \\&\langle \varnothing \ |\ \epsilon =\gamma (x_{1},x_{2}),\ x=\gamma (y_{1},y_{2}),\ x=\delta (x_{1},y_{1}),\ \epsilon =\delta (x_{2},y_{2})\rangle \rightarrow ^{*}\\&\langle \varnothing \ |\ x_{1}=\epsilon ,\ x_{2}=\epsilon ,\ x=\gamma (y_{1},y_{2}),\ x=\delta (x_{1},y_{1}),\ x_{2}=\epsilon ,\ y_{2}=\epsilon \rangle \rightarrow ^{*}\\&\langle \varnothing \ |\ \delta (\epsilon ,x)=\gamma (x,\epsilon )\rangle \rightarrow \dots \end{aligned}}}$

相互作用ネットワークは本質的に決定論的であり、非決定論的な計算を直接モデル化することはできません。非決定論的な選択を表現するには、相互作用ネットワークを拡張する必要があります。実際には、エージェントを1つ導入するだけで十分です。${\displaystyle {\text{amb}}}$^{[ 6 ]} 2つの主要ポートと以下の相互作用ルールを持つ：

この特別なエージェントは曖昧な選択を表し、任意の数の主ポートを持つ他のエージェントをシミュレートするために使用できます。たとえば、${\displaystyle {\text{ParallelOr}}}$引数のいずれかが真であれば、他の引数で行われる計算とは無関係に真を返すブール演算。

• 相互作用の幾何学
• グラフ書き換え
• ラムダ計算
• 線形グラフ文法
• 線形論理
• プルーフネット

• Asperti, Andrea; Guerrini, Stefano (1998).関数型プログラミング言語の最適実装. Cambridge Tracts in Theoretical Computer Science. Vol.  45. Cambridge University Press. ISBN 9780521621120。
• Fernández, Maribel (2009). 「相互作用に基づく計算モデル」. 『計算モデル：計算可能性理論入門』 . Springer Science & Business Media. pp. 107–130 . ISBN  9781848824348。

• de Falco, Marc. "tikz-inet. 相互作用ネットを描画するためのtikzベースのマクロセット" .
• de Falco, Marc. 「INL. Interaction Nets Laboratory」 .
• ビラサ、ミゲル。「INblobs。インタラクション ネットのエディターおよびインタープリター」。
• Asperti, Andrea. "The Bologna Optimal Higher-Order Machine" . GitHub .
• サリフメトフ、アントン（2018年3月22日）。「インタラクションネットのためのJavaScriptエンジン」。
• サリフメトフ、アントン。「マクロラムダ計算」。
• 謝宇恒。「iNet、相互作用ネットワークを探索するための言語とインタラクティブな遊び場」。