形式定理の工学的翻訳
論文 §4.4 は六つの中核メタ理論定理を与える。本稿では証明は並べず、各定理を「実際の Agent Runtime にとって何を意味するか」に翻訳する。Confluence の理解が本論文全体の価値を理解する鍵である。
六定理の工学的翻訳表
[論文原文の結論 §4.4]
| 定理 | 節番号 | 工学的翻訳 |
|---|---|---|
| Preservation（Thm 59） | §4.4.1 | 任意の規則適用後も registry は well-formed を維持する：親ポインタは registry 内に収まり、異なる fiber の provision は互いに素で、committed view は installed fiber にしか指さない。工学的意味：ランタイムは決して「宙に浮いた fiber 参照」や「二つのプラグインが同時に 'database' を提供している」といった状態にならない。 |
| Recovery Exactness（Thm 61） | §4.4.2 | pairwise independence の前提で、fiber n の episode [b, u] に対し、その accumulator を適用した結果は「n を一度もロードしていない」時の状態と等しい（control fields を除く）。工学的意味：プラグインをアンロードした後の環境状態は、それが一度も存在しなかったのと等価——HMR やプラグインのホット置換にとって極めて重要。 |
| Ordering（Thm 63） | §4.4.3 | Provider は Consumer より先に活性化し、後にアンロードしなければならない；Consumer が episode 全体で読む依存解決（committed view）は不変である。工学的意味：接続プールを閉じる前にすべてのコネクションが返却済み；データベースを閉じる前にすべてのトランザクションがコミット済み；「競合状態で consumer が半閉じの provider を読む」ことは起きない。 |
| Resolution Coherence（Thm 64） | §4.4.3 | 一つの transition の全 iteration は同じ committed view の下で走る；途中で target が変化した場合、Active へ完了遷移するか、L-Divert/L-Raise で Unloading に入り完全にロールバックするかのいずれか。工学的意味：非同期でコンポーネントをロード中に「半旧半新」にはならない——一部の effect が旧依存、別の一部が新依存を使うことはない。 |
| Progress（Thm 66） | §4.4.4 | ≺ が非巡回、len(e_n) ≤ K、fiber 名が有限という前提で、non-quiescent 状態には必ず適用可能な規則があり、各 fiber のステップ数は有界である。工学的意味：システムはデッドロックしない（guard は必ず解放される）；設定変更のたびに最終的に安定状態に到達する。 |
| Confluence（Thm 73） | §4.4.5 | pairwise independence、component total on provision、no failure の前提で、何度ロード/アンロード/置換を行っても、最終的な設定が同じなら、安定状態は最終設定からゼロ起動した状態と等価である。工学的意味：動的歴史は痕跡を残さない——Agent が自分自身のコンポーネントを繰り返し置換した後の状態は、最終設定で一括起動した状態と等価。「自己進化 Agent」の理論的基石である。 |
Confluence：動的歴史は痕跡を残さない
Confluence はこの理論のクライマックスであり、独立に展開する価値がある。
直感的な表現：システムが任意の回数の動的ロード、アンロード、置換を経た後、最終的な設定が同じである限り、その安定状態は最終設定でゼロから起動した時に得られる状態と等価であるべきである。
自己進化 Agent にとって、これは次を意味する：仮に Agent が実行中にツール A を三回置換し、Skill B を二回アンロードして再インストールし、サブ Agent C の isolation realm を調整したとしても、最終的なコンポーネント設定が「あるクリーン起動」と同じであれば、ランタイムの安定状態（どのコンポーネントが活性か、各 committed view、蓄積された環境状態）はそのクリーン起動と等価である。動的歴史はいかなる痕跡も残さない。
これは他の DI/HMR フレームワークにはない保証である：
- 従来の DI はランタイム置換をサポートせず、Confluence の対象がない；
- HMR は開発者による状態移行関数の手書きが必要で、移行が正しいかについて形式保証がない；
- コンテナオーケストレーションの「再起動 = クリーン」は全状態を粗粒度で破棄するだけで、同粒度の等価ではない。
[論文原文の結論 §4.4.5] Confluence の前提に注意：
- pairwise independence：effect 同士は独立または可換（Def 19）；
- component total on provision：すべての component が宣言したすべての key を実際にインストールする（Def 69）；
- no failure：failure シナリオを除外。
[論文原文の結論 §4.4.5] Confluence は failure シナリオを除外する（§4.3.4 の L-Raise）——failure は真の分岐源だからである：あるスケジュールは fail し別のスケジュールは succeed するかもしれないが、Cor 62 は failed fiber の state への寄与が 0 であることを保証する（失敗コンポーネントの副作用は完全にロールバックされ、他の fiber に影響しない）。したがって「失敗」は状態一貫性を破らないが、二つの動的経路が分岐する（一方に失敗あり、もう一方になし）原因にはなる。
この証明体系が保証しないこと
[論文原文の結論 §6.1, §6.3] 形式証明は Context を通じて管理される副作用のみをカバーする。以下は保証しない：
- 開発者の書いた inverse が必ず正しいこと（witness 条件
g(δ)=γは義務であり検証されない）； - Context 外の副作用（グローバル変数、ファイル、データベース、外部システムの直接変更）がロールバックできること；
- 外部 emission（ネットワークリクエスト、メッセージ、メール、決済）が自動でロールバックできること——これらは一度発射されるとシステム境界を越える；
- 信頼できないプラグインの安全性——Context 級の権限制御はプロセス/コンテナ/WASM サンドボックスに代わらない；
- failure シナリオ下の Confluence（明示的に除外）；
- 依存 key のバージョン互換性と構造互換性（§6.6 オープン問題）。
前提と限界の詳細は 限界と総合評価 を参照。この理論が DeepSeek Harness にどう落ちるかは DeepSeek Harness との関係 を参照。