Endpoint Sufficiency Behavioral Quotients

技術要約：プロベナンス（由来）の忘却はいつ正当化されるか？

問題提起
生成システムは、しばしば複数の抽象レベルで表現可能なオブジェクトを生成する。ある表現は「可視的な終端（visible endpoint）」（最終的なオブジェクト）のみを捉えるが、別の表現は完全な「プロベナンス（由来）」（系譜、マージ・イベント、依存構造）を保持する。終端表現はより軽量であるが、システムの許容規則がリネージ（系譜）に依存している場合、それが誤った状態記述となるリスクがある。本稿が扱う核心的な問題は、プロベナンス情報が、システムの法的な将来の振る舞いを変えることなく、いつ安全に忘却され得るのかを決定することである。具体的には、終端への射影（endpoint projection）が、法的な遷移を決定するために十分な情報を保持しているのはどのような場合か、そして破棄可能なプロベナンスの最大量はいくらであるか、という問いを立てている。

本稿は、「終端の十分性（endpoint sufficiency）」は単一の均一な概念であるという暗黙の仮定に異議を唱える。そして、この概念が観察レベル（即座に有効なルールのみを重視するか、有限のルール・ラベルの列（トレース）を重視するか、あるいは将来の可能性の全分岐構造を重視するか）によって異なることを実証する。

手法
著者は、**法的な生成遷移システム（Lawful Generative Transition Systems: LGTS）**を用いて問題を定式化する。LGTSは、以下のタプル $T = (S, \Sigma, \to, U, X, \cong_X)$ として定義される：

• $S$ は、プロベナンスで装飾された発生（occurrence）の集合。
• $\Sigma$ は、ルール・ラベルの集合。
• $\to$ は、法的なラベル付き遷移関係。
• $U: S \to X$ は、発生を可視的なオブジェクトへと写像する終端射影。
• $\cong_X$ は、可視オブジェクト上の同値関係。

本研究では、終端同値関係（$\equiv_U$、ここで $s \equiv_U t \iff U(s) \cong_X U(t)$）と、様々な振る舞いの同値性との関係を分析する。分析は、以下の3つの異なる観察レベルを通じて行われる：

1. 有効性（Enabled Sufficiency）: 即座に利用可能なルール・ラベルの集合を保持すること。
2. トレースの十分性（Trace Sufficiency）: すべての有限のルール・ラベルの列（トレース）の集合を保持すること。
3. 商（分岐）の十分性（Quotient/Branching Sufficiency）: 終端同値関係をモジュロとした、分岐的な遷移構造を保持すること。

本稿では、トレース同値、強双模倣（strong bisimulation）、余帰納法（coinduction）、および分割細分化（partition refinement）を含む標準的なプロセス・セマンティクスのツールを用い、これらを終端とプロベナンスの境界に特化して適用している。

主要な貢献と結果

1. 厳格な三段階の階層構造
本稿は、これら3つの十分性のレベルが区別され、以下の厳格な階層を形成することを確立する：
$$\text{Quotient Sufficiency} \implies \text{Trace Sufficiency} \implies \text{Enabled Sufficiency}$$

• 有効性の十分性は最も弱く、同値な終端が同じ有効な次の一手の集合を持つことのみを要求する。
• トレースの十分性は、同値な終端が同じ有限のルール・ラベル列を生成することを要求する。
• 商（分岐）の十分性は最も強く、任意のラベルに対する到達可能な終端クラスの集合が、特定のプロベナンス履歴ではなく、現在の終端クラスにのみ依存することを要求する。

2. 十分性のための正確な基準
本稿は、各レベルにおいて終端射影が十分となるための精密な数学的基準を提供する：

• トレース・レベル: 射影がトレースに対して十分であるための必要十分条件は、終端同値がトレース同値の部分集合であること（$\equiv_U \subseteq \equiv_{tr}$）である。
• 分岐レベル: 射影が商に対して十分であるための必要十分条件は、終端同値が強双模倣同値であることである。これは、任意の2つの終端同値な状態において、一方からのあらゆる遷移が、別の（かつ終端同値な）状態への遷移によって一致可能であることを意味する。

3. 標準的な修復（Canonical Repairs）と最大忘却
生の終端同値が十分性を満たさない場合、本稿は、可視的な終端を尊重しつつ、望ましい振る舞いを保持する最も粗い状態の細分化を特定する、2つの「標準的な修復」を提案する：

• 線形時間（トレース）に対して: 関係 $E^U_{tr} = \equiv_U \cap \equiv_{tr}$ は、終端を尊重し、かつ有限のトレースを保持する最大の同値関係である。これは、終端は同値であるが、その将来の振る舞いがルール・ラベルのトレースとして区別できない発生を特定する。
• 分岐時間（正確な商）に対して: $\approx_U$ と定義される関係（すべての終端尊重型強双模倣の和集合）は、最大の終端尊重型強双模倣である。商システム $T / \approx_U$ は、**最大に粗い正確な分岐商（maximally coarse exact branching quotient）**である。
  • 普遍性: 他のあらゆる正確な終端尊重型商は、この標準的な商を細分化する。したがって、$\approx_U$ は、正確な分岐セマンティクスを維持しながら忘却できるプロベナンスの最大量を表している。

4. アルゴリズムによる計算
有限システムにおいて、本稿は $\approx_U$ を計算するための停止する分割細分化手順を記述する。このアルゴリズムは、終端同値のクラスによる分割から開始し、「シグネチャ（後続ブロックの集合：各ラベルに対する到達可能なブロックの集合）」に基づいて反復的に細分化を行う。この手順は、$\approx_U$ に対応する分割において安定する。

5. 入れ子状の再帰的組換え生成（NRRG）への適用
本稿は、これらの結果を、プロベナンスで装飾されたNRRGの特定のフレームワークに適用する。ここでは、2つの発生（$e_G$ と $e_H$）が同じ可視グラフ終端（$I \to A \to B$）を共有しているが、その組換え的な系譜（recombinant ancestry）が異なるという、証拠となる事例を提示する。

• $e_G$ では、系譜により、境界に接触する書き換えルール（$R_B$）が可能となる。
• $e_H$ では、系譜により、$R_B$ が禁止される。
• 結果: 分割細分化アルゴリズムは、第1ラウンドにおいて $e_G$ と $e_H$ を分離する。これは、終端の同型性が、有効性のレベルにおいてさえも、振る舞いの同値性を意味しないことを示しており、提案された細分化手順が、必要な区別を正しく特定できることを実証している。

意義と主張
本稿は、「プロベナンスをすべて保持するか、あるいは完全に破棄するか」という二者択一の要求を、「正当な忘却のための正確な基準」へと置き換えることを主張している。

• 運用的残差（Operational Residue）: 生の終端クラスと、精緻化されたクラス（$\approx_U$ または $E^U_{tr}$）との差異は、プロベナンスの「運用的残差」を構成する。すなわち、将来の遷移空間において依然として活動的な歴史的情報である。
• 抽象の正確性（Abstraction Exactness）: 本研究は、抽象化の問題を、単なる健全性（過剰近似）としてではなく、選択されたセマンティクスに対する正確性として再定義する。生の商（raw quotient）は、双模倣を確認せずに状態を統合することで、特定の発生にとって不当な振る舞い（膨張）を生じさせる可能性がある。
• ドメイン非依存性: 結果は、システムが終端射影を持つラベル付き遷移システムとしてモデル化できる限り、プロベナンスが系譜に依存するあらゆるシステム（ソフトウェアの状態、法的文書、科学的主張など）に適用可能な形式的基準として提示される。

結論として、プロベナンスは、選択された法的な将来のセマンティクスを変更しない発生の区別に対して、正確に消去され得る。最大に安全な消去の後に残るのは、歴史的な装飾ではなく、真の**生成状態（generative state）**である。