HVMの理論的な基礎となっている計算モデルInteraction Combinatorの論文を読んでいく

1.1 インタラクションネット

セルには1つの記号(simbol)が書かれており、1つの 主要ポート(principal port) とn個(n \geq 0)の 補助ポート(auxiliary ports) からなる。これらn+1個のポートは互いに区別される。このメモでは、セルcに対して主要ポートをc_0、補助ポートをc_1, c_2, \ldots, c_nと書くことにする。

インタラクションネットとは、有限個のセルのポートとどのセルにも属さない有限個の自由ポート(free port)を繋いだもの。ただし、1つのポートは2つ以上のポートに接続されることはない。

形式的に書くと、インタラクションネットとは以下からなる5つ組(X,C,\Sigma,l,W)

• X: 自由ポートの有限集合
• C: セルの有限集合
• \Sigma: 記号の有限集合
• l: C \rightarrow \Sigma: 各セルの記号を表す関数
• (c_s, c'_t) \in W: ワイヤー(= ポートの繋がり)の有限集合

として表せそう？ただし、この記述は元の論文と異なる。

1.2 インタラクション

お互いの主要ポート同士で接続されている2つのセルc, c'はセルの記号の組(l(c), l(c'))ごとに定まるルールによって簡約される。この時、ポートの接続は向きを持たないので、組(l(c), l(c'))と組(l(c'), l(c))は同じルールを表す。
セルcの補助ポートの数をn、セルc'の補助ポートの数をmとしたとき、簡約によって得られる(部分)インタラクションネットはn+m個の自由ポートを持つ。

Propotion 1. [弱合流性]

インタラクションネットの簡約関係は弱合流性を持つ。このことから、インタラクションネットは停止すれば必ず一意な結果を持つことがわかる（ \because 弱合流性 + 停止性 = 合流性。合流性と停止性から正規系が書き換え戦略によらず一意である）。

メモ

PDFには"strong confluence property"(強合流性)と書いてあるが、Proposition 1.のステートメントで述べられているのは弱合流性のことだと思われる。

1.3-1.5 インタラクションネットの具体例

インタラクションネットで以下のものをエミュレートする例について書かれている。

• 1.3節：チューリングマシン
• 1.4節：自分自身と両隣の状態によって状態を変化させる一次元セルオートマトン
• 1.5節：自然数の和と積

特に自然数の演算とかよくできてるなあという感想。この辺からラムダ計算っぽさを感じる。

1.6 既約ネット(reduced net)

カット(cuts)

カット とは、主要ポート同士が接続された2つのセルのこと。可約カット(reducible cut) とは、カットであって2つのセルのシンボルの組(\alpha, \beta)に簡約のためのルールが定まっているもののこと。簡約不可能なカット(irreducible cut) とは可約カットではないカットのこと。簡約不可能なカットは消えない。

パス

セルc^1, c^2, \ldots, c^nについて、それぞれの主要ポートc^i_0が次のセルの補助ポートc^{i+1}_t (t \geq 1)に接続されているとき、これらを長さnの主要パスとよぶ。

長さnの閉じた主要パスを、長さnの悪循環(vacious circle) と呼ぶ。悪循環も既約カットと同様に消えない。

既約ネット

あるネットが簡約不可能なカットや悪循環を含まないとき、それを既約ネット と呼ぶ。簡約不可能なネットは簡約不可能なカットや悪循環を含むので必ずしも既約であるとは限らないが、既約ネットは簡約不可能である。