Games, mobile processes, and functionss -- alternating, concurrent, and well-bracketed semantics

技術的概要：ゲーム、モバイルプロセス、および関数

問題設定
本論文は、高階言語のための 2 つの主要な意味論的枠組みである操作意味論的ゲーム意味論（OGS）と$\pi$-計算（特に内部$\pi$-計算、$I\pi$）との間の、緊密で形式的な対応の欠如に対処する。両モデルとも$\lambda$-計算項の振る舞いを特徴づけるために用いられるが、その構成において著しく異なる。OGS は、環境との相互作用を表す構成から構成的に導出されるプログラムの意味を与える内包的モデルを提供し、交互性や適切に括弧付けられた性質などの特性を強調する傾向がある。一方、$\pi$-計算は、ミルナーの符号化を通じて関数をプロセスとしてモデル化し、代数的構造や双シミュレーションなどのプロセス等価性を活用する。著者らは、未定義の呼出し値（call-by-value）$\lambda$-計算（$\Lambda_V$）および呼出し名（call-by-name）に対して、これらのモデル間の正確な操作対応を確立し、それらが同一の振る舞的等価性を誘導し、一方の手法が他方に転用可能であることを実証することを目的としている。

手法
著者らは、$\Lambda_V$の操作意味論を、3 つの異なる OGS 変種と 2 つの$I\pi$変種と比較分析する：

1. OGS 変種:
   • 交互 OGS（A-OGS）: プログラム（プレイヤー）と環境（オポネント）の間の厳密な交互性を強制する。
   • 並行 OGS（C-OGS）: 構成内で複数の項が並列に実行されることを許可する。
   • 適切に括弧付けられた OGS（WB-OGS）: 継続に対してスタック規律を強制し、オポネントが後入れ先出し（LIFO）の順序で応答することを制限する。
2. $I\pi$変種:
   • 標準$I\pi$LTS: 内部$\pi$-計算の標準的なラベル付き遷移システム。
   • 出力優先$I\pi$LTS（opLTS）: 入力動作が出力または内部動作の待機がない場合のみ可視となるように制約された LTS で、逐次性の制約を強制する。

核心的な手法には、OGS の構成（環境および実行中の項を含む）から$I\pi$プロセスへの写像（$\mathcal{V}$）を定義することが含まれる。この写像は$\lambda$-項のミルナーの符号化を拡張するものである。著者らはその後、特定の条件下で OGS における遷移が$I\pi$における遷移に対応し（逆もまた同様）、操作対応定理を証明する。決定的な点として、彼らは$I\pi$から導入された「〜まで（up-to）」の手法（具体的には「文脈まで（up-to context）」および「合成まで（up-to composition）」）を用いて、OGS における双シミュレーション証明を簡略化する。また、プロセス計算における並行合成に類似して、トレースのインターリーブをモデル化するための OGS 構成に対するテンソル積を導入する。

主要な貢献

1. 操作対応: 本論文は、以下の間の緊密な操作対応を確立する：

   • 出力優先 LTS（opLTS）下での A-OGS と$I\pi$。
   • 標準 LTS 下での C-OGS と$I\pi$。
     これらの対応は、内部縮退を考慮するために展開関係（$\lesssim$）を用いて、強遷移および弱遷移の両方に対して成立する。

2. 等価性の一致: 著者らは、これらすべてのモデルによって$\lambda$-項に誘導される振る舞的等価性が一致することを証明する。具体的には：

   • A-OGS、C-OGS、および$I\pi$（標準および opLTS の両方）におけるトレース等価性と双シミュレーションは、すべて$\Lambda_V$項に対して同一の関係を定義する。
   • この誘導された等価性は、ラッセンの熱心な正規形双シミュレーション（しばしばラッセンの木として視覚化される）として特定される。
   • 完全なトレース（終了する相互作用を記述するトレース）については、交互、並行、および適切に括弧付けられた OGS の意味論もまた一致する。

3. 手法の転用:

   • 合成まで（Up-to Composition）: 著者らは、$I\pi$からの「文脈まで」および「展開」の手法を OGS へ導入する。彼らは OGS に対して**「合成まで」**と呼ばれる新規手法を定義し、これにより複雑な構成を素の構成要素（シングルトン構成）に分割し、それらについて独立に推論することを双シミュレーション証明で可能にする。
   • 合同性と構成的性質: $I\pi$との対応を活用することで、論文は OGS に対する合同性性質（例：$M \sim N$ならば$C[M] \sim C[N]$）を導き出し、トレースのインターリーブを計算する構成のためのテンソル積を定義する。

4. ストアに対する完全抽象化: 適切に括弧付けられた OGS における完全なトレースの研究は、可変ストアを持つ$\lambda$-計算の文脈的等価性と結びつけられる。本論文は、$\lambda$-項を$I\pi$へ符号化することが、ストア拡張された$\lambda$-計算で記述された文脈に関する完全抽象化の結果をもたらすことを示す。

5. 呼出し名への拡張: 本論文は、未定義の呼出し名$\lambda$-計算に対する同様の対応を概説し、誘導された等価性がレヴィ・ロンゴ木と一致することを示す。

結果

• 定理 6.7 および 7.3: 対応する LTS 下での OGS 構成と$I\pi$プロセス間の操作対応を確立する。
• 系 6.12 および 7.7: $\lambda$-項に対して、A-OGS、C-OGS、および$I\pi$におけるトレース等価性と双シミュレーションが同一であることを示す。
• 定理 8.1: 「合成まで」の手法を用いて、C-OGS 双シミュレーションがラッセンの熱心な正規形双シミュレーションと一致することを直接証明する。
• 定理 12.2: 完全トレース等価性が WB-OGS、A-OGS、および C-OGS 間で同一であることを証明する。
• 補題 7.16 および定理 7.17: $I\pi$から導入された C-OGS に対する「縮退および合成までの双シミュレーション」の健全性を証明する。

重要性
本論文は、その主要な重要性を OGS と$\pi$-計算の間の「緊密かつ正確な対応」の確立にあると主張する。この接続により、2 つのモデル間の結果および手法の転用が可能となる。具体的には：

• OGS が、ゲーム理論的枠組み内で直接発展させることがしばしば困難である$\pi$-計算の豊富な代数的構造および強力な証明手法（up-to 手法など）の恩恵を受けることを可能にする。
• $\pi$-計算が、OGS の源言語との近接性および特定の計算効果（制御演算子やストアなど）をモデル化する柔軟性の恩恵を受けることを可能にする。
• $\lambda$-計算の意味論に対する統一的な視点を提供し、OGS における「意味論的立方体」の条件（交互性、適切に括弧付けられた性質）と、$I\pi$における逐次性の制約（opLTS 経由）が、同じ基盤となる振る舞的等価性（呼出し値に対するラッセンの木）を特徴づける表裏一体のものであることを示す。

著者らは、ゲーム意味論とプロセス計算機との間の類推は以前に探求されてきた（例えば、戦略をプロセスへ翻訳するなど）と指摘するが、この研究は、関数の解釈の直接比較および OGS に対する新たな結果を導出するための証明手法の体系的転用において、独自のものであると述べている。