$Δ$-Nets: Interaction-Based System for Optimal Parallel $λ$-Reduction

技術要約：$\Delta$-Nets：最適な並列 $\lambda$-簡約のための相互作用ベースのシステム

問題提起
本論文は、$\lambda$-計算における最適な並列簡約（optimal parallel reduction）を実現するという、長年の謎に取り組んでいる。$\lambda$-計算は計算の基礎的なモデルであるが、その置換機械としての性質は逐次的であるため、共有（重複する部分式）や消去（破棄される部分式）を含むすべての項に対して最適な簡約を表現するには不十分である。

これらをグラフ簡約やインタラクション・ネット（Lamping、Gonthierらによるもの）を用いて解決しようとする従来の試みは、「インデックス付きファン」や「デリミタ（括弧やクロワッサン）」による「内部共有（interior sharing）」のメカニズムを導入した。しかし、既存のアルゴリズムには以下の決定的な非効率性が存在する：

1. デリミタの蓄積： デリミタが簡約中に蓄積し、ファン間の相互作用を圧倒してしまい、不要なメモリ使用量や計算ステップを引き起こす。
2. 無制限の増大： Lambdascopeのようなシステムでは、デリミタのインデックスが無制限に増大し、兄弟スコープが永続的に保持されるため、非正規化の場合に停止できず、空間複雑度が増大する。
3. グローバルな順序の欠如： 既存のアルゴлоリズムは、正規化される $\lambda$ 項に関連するすべてのネットが実際に正規化されることを保証するために必要な、グローバルな簡約順序を確立できていない。
4. 冗長性： 共有のない項を表すネットにおいてさえ、デリミタが機能的な目的を持たずに存在している。

核心となる課題は、いかにして、デリミタの蓄積によるオーバーヘッドや停止不能を招くことなく、複数の、重なり合う、あるいは再帰的な共有コンテキストを管理するかである。

手法：$\Delta$-Nets モデル
著者は、$\lambda$ 項をネットへと、またネットから $\lambda$ 項へと全単射によって変換するように設計された、インタラクション・ネットに基づく新しいユニバーサル並列計算モデルである $\Delta$-Nets を提案している。このシステムは、部分構造 $\lambda$-カルキュライに対応する4つのサブシステムに分解される：

• $\Delta$L-Nets: 線形（ファンのみ）。
• $\Delta$A-Nets: アフィン（ファンとイレイザー）。
• $\Delta$I-Nets: 関連（ファンとレプリケーター）。
• $\Delta$K-Nets: 完全（ファン、イレイザー、およびレプリケーター）。

モデルの核となるのは、3種類のエージェント・タイプである：

1. ファン (Fans): 2つの補助ポートを持つ。
2. イレイザー (Erasers): 補助ポートを持たない。
3. レプリケーター (Replicators): 可変数の補助ポートを持ち、それぞれに整数「レベル $\delta$」と非負整数「レベル」が関連付けられている。

主要なメカニズム:

• 相互作用ルール:
  • 消滅 (Annihilation): 同一のエージェント（同じレベル、ポート数、および $\delta$ を持つもの）は消滅する。
  • 消去 (Erasure): 異なるエージェントがイレイザーと相互作用する場合、それらは消去される。
  • 交換 (Commutation): 異なるエージェントは互いに通り抜ける。決定的なことに、レプリケーターがファンと相互作用する場合、レプリケーターはコピーされ、ファンの複製がレプリケーターの各ポートに対して行われる。2つの異なるレプリケーターが相互作用する場合、それらは相対的なレベルとポート $\delta$ に基づいて互いを複製する。
• レプリケーター: このエージェントは、以前はインデックス付きファンやデリミタに分散していた情報を集約する。これにより、単一のエージェント・タイプで任意の共有スコープを扱うことが可能になる。
• 標準化ルール (Canonicalization Rules): 収束性と最適性を確保するために、非相互作用ルールを導入する：
  • 未ペアのレプリケーターの結合 (Unpaired Replicator Merging): 木構造における連続する未ペアのレプリケーターを結合する。
  • 未ペアのレプリケーターの減衰 (Unpaired Replicator Decay): イレイザーに接続された補助ポートを排除する。
  • グローバル消去 (Global Erasure): 消去を伴うシステムにおいて、切断されたサブネットを除去する最終ステップ。
• 簡約戦略: システムは 逐次左外側簡約順序 (sequential leftmost-outermost reduction order) を採用する。この順序は、レプリケーターの結合が可能な限り早期に行われ、かつ未ペアのレプリケーターを含む交換が時期尚早に適用されないようにするために極めて重要である。

主な貢献と結果

1. 最適な並列簡約: 本論文は、最適な並列 $\lambda$-簡約のためのアルゴリズムを提示している。このシステムは、レヴィ（Lévy）が構想した簡約特性、すなわち「後に不要となる簡約は行われず、必要な簡約は二度と行われない」という特性を達成していると主張している。
2. 定数メモリ使用量: 以前のモデルではデリミタの蓄積が、例えば $(\lambda x. x x)(\lambda y. y y)$ のような項の簡約において無制限の空間増大を招くが、$\Delta$-Nets モデルは、レプリケーターによる情報の集約と不要なデリミタの排除により、このような項に対して定数メモリ使用量を示す。
3. 完全な収束性 (Perfect Confluence): コアとなる相互作用システムは「完全な収束性」（1ステップ・ダイヤモンド特性）を有しており、あらゆる正規化する相互作用順序が、同じステップ数で同じ結果を生む。
4. チャーチ–ロッサーの収束性 (Church–Rosser Confluence): 相互作用ルールと標準化ルール（特に左外側順序と結合）を組み合わせることで、システムは、正規化される $\lambda$ 項に関連するすべてのネットが正規化され、一意の標準形を生成することを保証する。
5. $\lambda$-計算の投影: 本論文は、$\lambda$-計算が $\Delta$-Netsの投影として理解できることを確立している。$\Delta$-Netsにおける追加の自由度（具体的には、$\lambda$-計算には存在しない柔軟な共有構造）により、システムは最適な簡約を実現できるが、制限された共有構造を持つ$\lambda$-計算ではそれができない。

意義と主張
本論文は、$\Delta$-Netsが「画期的な明快さ」をもって、最適な $\lambda$-簡約という「長年の謎」を解決したと主張している。デリミタを多用する従来のインタラクション・ネットのアプローチから脱却することで、モデルは以下への道を開く：

• より効率的で高性能な並列プログラミング言語の実装。
• システムの完全な収束性と局所的な相互作用ルールを活用できる新しいコンピュータ・アーキテクチャ。
• $\lambda$-計算を、独立した実体としてではなく、より強力で最適な並列システム（$\Delta$-Nets）の制限された投影として理解するための基礎的な理解。

著者は、このモデルが単なる理論的な改善ではなく、最適簡約アルゴリズムの実装においてプログラミング言語の中核として利用することを阻んできた非効率性の実用的な解決策であることを強調している。システムは、統一されたレプリケーター・エージェントと厳格な簡約順序を通じて、構造的なオーバーヘッドの蓄積を防ぎ、共有コンテキストの管理を簡素化することで、これを実現している。