Proof Nets for PiL (Full Version)

技術的概要：PiL のための証明網

問題提起
本論文は、第一次乗法的加法線形論理（MALL1）を拡張した論理系であるPiLにおける証明に対して、標準的なグラフベースの表現を提供するという課題に取り組む。PiL は、$\pi$-計算におけるプロセスの浅いエンコーディングを提供するために導入され、特にレースフリーかつデッドロックフリーなプロセスに対する choreographic programming の完全性を証明するために用いられる。

核心的な難しさは、PiL の固有の演算子にある：

1. $\blacktriangleleft$ 演算子： 非可換・非結合かつ自己双対な結合子であり、逐次合成をモデル化する。
2. 名目量化子（$\new$ および $\ya$）： 名前束縛と鮮明性をモデル化する量化子であり、変数の使用を厳密に管理し、名目が最大でも 1 つの双対量化子のペアによって共有されることを保証する必要がある。

MALL に対する既存の証明網形式（ギヤールの網やコンフリクト網など）は、加法、量化子、および非可換・非結合的な結合子の組み合わせに直面して困難に陥る。さらに、標準的なシークエント計算の導出は、独立した規則の入れ替えにより非標準的（非単一）となり、プロセス実行ツリーの背後にある意味論を曖昧にする。本論文は、これらの入れ替えを単一の構文対象に縮約しつつ、名目量化子と$\blacktriangleleft$演算子の特定の制約を処理する証明網を定義することを目的とする。

手法
著者は、コンフリクト網を基礎的な枠組みとして採用し、これを PiL の第一次設定に拡張する。手法は以下の 3 つの主要な構成要素からなる：

1. 構造の定義（前構造と証明網）：

   • リンクと双対化子： 著者はリンク（部分シークエント間の公理的な接続）を定義し、これらを双対化子（置換）に関連付ける。双対化子は、リンク内の変数を存在量化または名目量化の証人へ写像し、双対性を強制するとともに、量化子によって要求される統一を処理する。
   • ココ木（Coco-trees）： 基礎となる構造は「調和 - 対立木（concord-conflict tree）」（ココ木）であり、その葉はリンクで、内部ノードは調和（$\smile$）または対立（$\#$）関係でラベル付けされる。
   • 統合（Coalescence）： 証明構造を単一の葉という自明な形に還元する書き換え手続き（統合）が定義される。このプロセスは、シークエント導出のボトムアップ構築を模倣する。証明網とは、自明な前構造への統合経路を持つ証明構造として定義される。

2. 正しさの判定と逐次化：

   • 多項式時間正しさ判定基準： 構造が有効な証明網であるための必要十分条件として、それが統合可能であることが多項式時間で判定される基準が確立される。
   • 逐次化手続き： 有効な証明網を PiL におけるシークエント計算の導出へ逆変換する手続きが提供される。これにより、論理に対する網形式の完全性が証明される。
   • 証明変換アルゴリズム： PiL の導出をコンフリクト網へ変換するアルゴリズムが提示され、健全性が確立される。

3. スライス網と平坦化：

   • より標準的な形式を達成するために、著者はスライス網を導入する。これは、基礎となるココ木が「平坦」（根に高々 1 つの$\#$-ノードを含む）であるコンフリクト網の部分クラスである。
   • 平坦化手続きは、調和ノードを対立ノードの上に移動させる書き換え規則として定義される。著者は、平坦化が強く正規化可能であり、合流性を持ち、かつ統合性を保存することを証明する。これにより、任意のコンフリクト網を一意の標準的なスライス網へ変換することが可能となる。

主要な貢献

• PiL に対するコンフリクト網の定義： 加法、第一次量化子、および非可換・非結合的な$\blacktriangleleft$結合子を組み合わせた論理に対する最初の証明網形式を定義する。
• 多項式時間正しさ判定： 証人写像付きの Coco 木の統合に基づき、多項式時間（具体的には$O(n^5)$）の正しさ判定基準を提供する。
• 逐次化と変換： PiL シークエント導出と証明網間の双方向変換を確立し、網が健全かつ完全であることを証明する。
• 標準的表現（スライス網）： スライス網と平坦化手続きを導入し、すべてのコンフリクト網が一意のスライス網に還元されることを証明する。
• 標準性に関する結果： 論文は 2 つの異なるレベルの標準性を証明する：
  • 局所的標準性： コンフリクト網は、局所的な規則の入れ替え（独立した規則の交換）をモジュールとした導出の標準的表現を提供する。
  • 強標準性： スライス網は、局所的および非局所的な規則の入れ替えの両方をモジュールとした標準的表現を提供する。

結果

• 定理 1： シークエント$\Gamma$が PiL で証明可能であるための必要十分条件は、$\Gamma$に対するコンフリクト網が存在することである。
• 定理 2： 平坦化は統合性を保存し、コンフリクト網からスライス網への変換が妥当性を維持することを保証する。
• 定理 3： シークエント$\Gamma$が PiL で証明可能であるための必要十分条件は、$\Gamma$に対するスライス網が存在することである。
• 定理 4：
  • 2 つの導出$D$と$D'$が局所的に同値（$D \approx D'$）であるための必要十分条件は、それらに関連するコンフリクト網が同型であることである。
  • 2 つの導出$D$と$D'$が強同値（$D \simeq D'$）であるための必要十分条件は、それらに関連するスライス網が同型であることである。

意義と主張
本論文は、PiL に対する証明網がシークエント計算の導出の標準的表現を提供し、独立した規則の入れ替えのみによって異なる導出のクラスを実効的に縮約すると主張する。これはプロセス計算の意味論にとって重要である。なぜなら：

• 独立した動作の順序がプロセスの意味に影響を与えないという$\pi$-計算における実行ツリーの意味論と整合するからである。
• 局所的標準性（分岐の順序が重要な文脈に関連する）と強標準性（分岐の順序が関係ない同値性、例えば双シミュレーションに関連する）を区別するからである。
• 証明網を実行ツリーの代表として扱い、無関係なインターリーブを無視しつつ、競合状態のような観測可能な現象を保持することで、並行システムと choreographies の意味論を研究するための新たなツールの開発の基盤を提供するからである。

著者は明示的に、この研究ではカット除去を扱っていないと述べている。彼らの焦点は、計算ツリーを表すカットフリー証明にあるからである。彼らは、PiL に対するカット除去には、名目量化子とストアの非自明な処理が必要であり、それは将来の課題に委ねられると指摘している。同様に、彼らは自らの枠組みが一般的な第一次 MALL に拡張可能であることを示唆しているが、本論文において一般の場合を解決したとは主張していない。