技術要約：残留プロセス挙動のためのストーン・チェッフ（Stone–Čech）収集意味論

1. 問題提起

無限の計算は、それが実行するアクションのシーケンスによって完全に特徴付けられるだけでなく、一連の残留プロセス（各遷移の後に実行されるべき残りのプロセス）も残していく。有限の計算や単純なサイクルに落ち着く計算は十分に理解されているが、無限の実行は複雑な長期的挙動を示すことがある：

• 安定した発散 (Stable divergence): 単一のプロセスまたは有限のサイクルに落ち着く。
• 混合的な回帰 (Mixed recurrence): 特定の状態を無限に何度も訪れる一方で、未訪問の新しい状態の無限定なシーケンスも訪問する。
• 脱出 (Escape): （並列コンポーネントの数の増加などの）観測空間のあらゆる有限の部分を離れていく（例：単一の残留プロセスが回帰することなく、無限定に成長する）。

課題は、これら多様な残留テイル（residual tails）に対して共通の意味論的形式を提供することである。標準的な極限集合は、非コンパクト空間（シーケンスが極限を持たない可能性がある場合）では機能せず、単純な回帰カウントは「脱出」挙動を捉えることができない。さらに、意味論は観測の下で頑健である必要がある。完全な意味論的オブジェクトは直接検査するには大きすぎるため、連続的な観測（リソースカウンタや様相述語など）に対して適切に振る舞わなければならない。

2. 手法

本論文は、フィルタリングされたストーン・チェッフ収集意味論を構築する。核心となる手法は、無限の実行を観測のストリームとして扱い、その漸近的挙動を観測空間のストーン・チェッフコンパクト化へと写像することである。

2.1 構成

• フィルタリングされた時間: 実行（run）は、$T$ を適切なフィルタ $\mathcal{F}$（「大きな」集合を指定するもの）を備えた時間インデックスの集合とし、$X$ をティホノフ観測空間とする写像 $a: T \to X$ として定義される。
• ストーン・チェッフの意味: 実行の意味は、以下のコンパクト集合である：
  $$M^F_X(a) = \beta a[\text{Ext}(\mathcal{F})] = \bigcap_{F \in \mathcal{F}} \text{cl}_{\beta X} a[F] \subseteq \beta X$$
  ここで、$\text{Ext}(\mathcal{F})$ は $\mathcal{F}$ を拡張する $T$ 上の超フィルタの集合であり、$\beta a$ はコンパクト化への連続拡張である。
• 解釈:
  • 逐次的な時間（$T=\mathbb{N}$）かつ余有限フィルタの場合、これは $\beta X$ におけるテイル・クラスター集合 (tail-cluster set) を与える。
  • $X$ が離散的かつ有限である場合、$M^F_X(a)$ は無限に訪問される状態の集合となる。
  • $X$ が離散的かつ無限である場合（例：$\mathbb{N}$）、その意味は $X^* = \beta X \setminus X$ に含まれる点を含み、「無限への脱出」を表すことができる。

2.2 観測による読み取り

この意味論は、連続的な観測 $f: X \to Y$ を通じて読み取られるように設計されている。関手性 (functoriality) により、観測された実行の意味は、元の意味の像となる：
$$M^F_Y(f \circ a) = \beta f[M^F_X(a)]$$

• クロープ（Clopen）観測: クロープ集合 $C \subseteq X$ について、包含関係 $M^F_X(a) \subseteq \text{cl}_{\beta X} C$ は最終的な真理性 (eventual truth)（実行は最終的に $C$ 内にある）に対応し、非空な交わりは回帰 (recurrence)（実行は $C$ を無限に訪問する）に対応する。
• リソース観測: 整数値のリソースマップ（例：並列コンポーネントのカウント）は、自然数の剰余部分（$\mathbb{N}^*$）へ写像することで、無限定な脱出を検出できる。

2.3 非決定性と公平性

• 非決定性: この意味論は、実行に敏感な (run-sensitive) 意味（各実行ごとのコンパクト集合の集合）と、平坦化された (flattened) 意味（すべての漸近点の和集合）を区別する。
• 公平性 (Fairness): 公平性と進捗の仮定は、時間フィルタを強化することによって扱われる。公平な意味は、特定の進捗集合を含む超フィルタに限定することで計算される。
• 関係的性質: 同時並行的な観測間の相関（例：2つのプロセスが並行して動作している場合）を保持するために、この構成は個々の意味の積を取るのではなく、積空間 $\beta(X_1 \times \dots \times X_k)$ をコンパクト化する。

3. 主要な貢献と結果

3.1 一般理論

1. テイル不変性 (Tail Invariance): 意味は、フィルタに含まれない集合上の実行の変化（ストリーム内の有限個の項の変更など）に対して不変である。
2. 関手性 (Functoriality): 連続的な観測は構成と可換であり、有限の商、様相論理、およびリソースマップを単一のコンパクトな対象から導出することを可能にする。
3. 時相論理: この構成は、時相様相 $\Box_\infty A$（最終的な真理性）および $\Diamond_\infty A$（回帰）に対して、コンパクト化における集合の包含および交わりという直接的な位相的読み取りを提供する。

3.2 CCS (Calculus of Communicating Systems) への適用

本論文はこの枠組みをCCSに適用する。ここでは、無限の実行は構造的合同類としてのプロセスのストリームとして捉えられる。

• 挙動の分類: 意味論は以下を区別する：
  • 安定した発散: 単集合（例：$A \xrightarrow{a} A$）。
  • 有限回帰的発散: 有限集合（例：$P$ と $Q$ の間を交互に遷移する）。
  • 無限定な残留増大: $\beta \text{CCS} \setminus \text{CCS}$ に完全に含まれる集合（例：$G \xrightarrow{a} G|G \xrightarrow{a} G|G|G \dots$）。
  • 混合挙動: 主的な（回帰的な）点と非主的な（脱出する）点の組み合わせ。
• 残留テイル法則 (Residual-Tail Laws): 有限プレフィックス選択ラッパー（$\alpha_1.P_1 + \dots + \alpha_k.P_k$ の形式を持つプロセス）に対して、漸近的な残留意味はリーフ（葉）の意味の和集合になることを証明している。有限のプレフィックスやガード付き展開は、テイルの意味には影響を与えない。
• 法則の境界: これらの法則は、任意のCCSコンテキストに対して合同 (congruence) ではないことを示す。具体的には、並行合成と同期は、プレフィックスが消費される前にそれが関連する状況を作り出す可能性がある（例：プレフィックス $a.0$ は環境と同期してループを有効にできるが、$0$ はできない）。したがって、この意味論は完全な文脈的同値ではなく、「残留テイル」の意味論である。

3.3 計算的インターフェース

$\beta X$ は非可算であり、有効に列挙可能ではないため、本論文は有限の観測商を通じた計算的インターフェースを提供する：

• 有限のブール代数によるプロセス述語は、有限の商空間を誘導する。
• コンパクトな意味のこの商空間における像は、まさに回帰的な抽象状態の集合である。
• 有限の遷移グラフの場合、これは強連結成分 (SCC) 解析に帰着する。 「エッジ・フェア (edge-fair)」な規約の下では、公平な意味は到達可能な終端SCCに対応する。
• リソース観測可能量: 無限定な脱出は、リソースマップ（例：プロセスサイズ）が無限に増大すること、すなわちコンパクトな意味が $\mathbb{N}$ のストーン・チェッフ剰余にランディングすることを確認することで、計算的に検出される。

4. 意義と主張

本論文は、残留プロセス挙動のための統一された、コンパクトな収集意味論を提供すると主張しており、それは以下の特性を持つ：

1. 回帰の一般化: 有限空間における通常の回帰や、コンパクト空間における極限集合を包含しつつ、「脱出」が発生する非コンパクト空間へと拡張している。
2. 観測の統一: 有限の商、様相論理、およびリソース測定を単一のコンパクトな対象の連続的な像として扱うことで、異なる抽象化レベル間での一貫性を保証している。
3. テイル同値性の明確化: 有限のプレフィックスを（テイルにおいて）消去できる条件に関する正確な法則を確立し、並行合成がこの同値性を破る境界を明示的に特定している。
4. 計算を可能にする: 抽象的で計算不可能なコンパクトな対象と、具体的な有限の検証技術（SCC解析）およびリソースモニタリングとの間の架け橋となる。

この構成は、意味論的担体（semantic carrier）として提示されている。すなわち、コンパクトな対象自体を直接検査するのではなく、その射影（観測を通じて）が、分析、公平性チェック、および無限の挙動の検証のための実効的なインターフェースを提供するのである。