A Diagrammatic Axiomatisation of Behavioural Distance of Nondeterministic Processes

以下は、Różowski、Piedleu、Silva、Zanasi による論文「A Diagrammatic Axiomatisation of Behavioural Distance of Nondeterministic Processes（非決定性プロセスの振る舞い距離の図式的公理化）」の詳細な技術的要約である。

1. 問題定義

本論文は、非決定性プロセスの振る舞いを定量的に比較するという課題に取り組んでいる。

• 文脈: 従来のプロセス代数やオートマトン理論は、同値性（例えば、双シミュレーション、言語同値）のブーリアンな概念に依存している。これらは有用であるが、確率的または定量的側面を伴う現代のシステムにはあまりに硬直的であり、単に同一かどうかだけでなく、2 つの振る舞いがどの程度離れているかを測定する必要がある。
• 具体的なギャップ: 振る舞い距離は確率的システムや決定性オートマトン（DFA）に対して研究されてきたが、非決定性プロセス（特にミルナーのチャート）に対して、健全かつ完全な公理的枠組みが存在しない。
• 課題: 非決定性は、言語同値から双シミュレーションへと意味論的焦点をシフトさせる。既存の代数的構文（バインダ付き正規式など）は、複雑な代入メカニズムなしにこれらの振る舞いを構成的に捉えることに苦労する。さらに、非決定性システムへの定量的推論の拡張には、計量の「ハウスドルフリフティング」の処理が必要であり、これを公理化することは技術的に困難である。

2. 手法

著者らは、プロセスの振る舞いを表現し推論するために、ストリングダイアグラム（対称モノイダル圏の図形的言語）を用いた図式的アプローチを採用している。

• 意味モデル（チャート）: 本論文は、受入状態を可変出力に置き換えることで有限状態非決定性オートマトン（NFA）を一般化したミルナーのチャートに焦点を当てている。意味論は、擬計量構造を備えた正規振る舞い（$\Omega$）の圏上で定義される。
• 計量の定義: 振る舞い距離は余代数枠組みを通じて定義される。これには以下が利用される：
  1. 遷移リフティング: 状態上の計量を遷移（ラベル付き辺と可変出力）上の計量にリフティングする。
  2. ハウスドルフリフティング: 遷移の集合への計量リフティング（非決定性を処理するため）。
  3. 不動点特徴付け: 距離は、擬計量の格子上の単調作用素の最小不動点である。これは双シミュレーションの層別化（ヘネシー・ミルナー論理）によって具体的に特徴付けられ、2 つのプロセスが深度$n$まで双シミュレーション可能だが$n+1$ではそうでない場合、距離は$2^{-n}$となる。
• 構文（ストリングダイアグラム）: 著者らは構文としてストリングダイアグラムを使用する。この選択は以下を提供する：
  • 変数自由な表現: 再帰は、明示的なバインダと代入ではなく、フィードバックループ（トレース）によって処理される。
  • 構成的意味論: ダイアグラムは正規振る舞いの圏的構造に自然に写像される。
  • Int 構成: 双方向的なデータフロー（入力/出力）とフィードバックループを処理するために、著者らはInt 構成を利用して、振る舞いのトレース付きモノイダル圏をコンパクト閉圏に変換し、局所的なワイヤーの曲げを可能にする。

3. 主要な貢献

A. 定量的推論システム

本論文は、振る舞い距離の上限を導出するための定量的等式規則（推論システム）のセットを提案する（$s \equiv_\epsilon t$）。

• 標準的計量規則: 反射律、対称律、三角不等式、および「連続性」規則（すべての$\epsilon' > \epsilon$に対して$s \equiv_{\epsilon'} t$であれば、$s \equiv_\epsilon t$である）。
• 構成的規則: 非拡大性を保存する逐次合成および並列合成（テンソル）の規則。
• ドメイン固有規則:
  • (Pref): 動作$a$によるプレフィックスは距離を半分にする（$d(a.s, a.t) = \frac{1}{2}d(s, t)$）。これは、2 つのプロセスを区別するには 1 つのステップが必要という直観を捉える。
  • (Codel): 初期状態を持たないダイアグラム（デッドロック）は、空のチャートから距離 0 にある。
  • 等式公理: 強双シミュレーション（距離 0）を捉える公理のセット（A1-B11）。これには、非決定性選択、変数のマージ、再帰（コンウェイ理論の公理）の法則が含まれる。

B. 健全性と完全性

中心的な技術的達成は、推論システムが健全かつ完全であることを証明することである。

• 健全性（定理 16）: 導出可能なすべての定量的等式$f \equiv_\epsilon g$は有効である（すなわち、実際の振る舞い距離$d(\llbracket f \rrbracket, \llbracket g \rrbracket) \leq \epsilon$）。
• 完全性（定理 31）: 2 つのダイアグラム間の振る舞い距離が$\leq \epsilon$であれば、提案された規則を用いて等式$f \equiv_\epsilon g$が導出可能である。
  • 証明戦略: 完全性の証明には、任意のダイアグラムを正規形（有限プレチャートを表す）に変換する作業が含まれる。その後、ハウスドルフリフティングの計算と不動点反復（クレイニーの定理）を、推論規則を用いて構文的にシミュレートする。連続性（Cont）規則は、構文的近似と正確な極限の間のギャップを埋めるために決定的である。

C. 圏的構造

本論文は、正規振る舞いの圏（$\text{RegBeh}$）がコンウェイ理論（特定の種類のトレース付きモノイダル圏）であり、擬計量構造によって擬計量空間の圏（$\text{PMet}$）上の** enriched category**（ enriched 圏）であることを確立している。これにより、すべての圏的演算（合成、テンソル、トレース/ダガー）が非拡大であることが保証される。

4. 結果

• 形式的特徴付け: 本論文は、出力を伴う非決定性プロセスであるミルナーのチャートに対する振る舞い距離の最初の完全な公理化を提供する。
• 計量の構文的シミュレーション: 著者らは、遷移の集合間のハウスドルフ距離のような複雑な計量計算が、ストリングダイアグラムの純粋な構文操作を通じてシミュレート可能であることを示している。
• 例示的応用: 本論文には、2 つの特定のチャート（1 つは 2 つの'a'後にデッドロック、もう 1 つは無限の'a'）が正確に$1/4$の距離にあることを証明する詳細な導出が含まれている。これは、再帰を展開し、(Pref) 規則を 2 回適用することで達成される。

5. 意義

• 理論と実践の架け橋: ブーリアン同値から定量的距離へ移行することで、この作業は「ほぼ同値」という概念が意味を持つシステム（近似システムの検証や確率的システムなど）のよりニュアンスのある分析を可能にする。
• 統合された図式的枠組み: ストリングダイアグラムの使用は、従来のプロセス代数に見られる変数束縛と代入の複雑さを回避する。これは、決定性、非決定性、確率的、重み付きなど、さまざまな計算モデルにおける同値性と距離の公理化のための統合枠組みへの道筋を示唆している。
• 将来の作業の基盤: 本論文は、振る舞い距離がさらに重要となる重み付き遷移システムや確率的オートマトンへのこれらの結果の拡張の基礎を築いている。また、デコンパイルアルゴリズムの推論やガード付きクレイニー代数（GKAT）への潜在的な応用も示唆している。
• 理論的進展: 余代数振る舞い計量、定量的等式論理、図的代数を結びつけ、これら分野がプロセス理論の長年の課題を解決するためにどのように統合できるかを示している。

要約すると、本論文は、非決定性プロセスの抽象的な余代数定義を、具体的で図式的かつ完全に公理化された計算体系へと成功裏に翻訳し、プロセス振る舞いに関する定量的推論がストリングダイアグラムの構文操作を通じて完全に実行可能であることを証明している。