コンポーネントライフサイクルとアンロード順序
Revertible Effects は「ロールバック」を解決し、Reactive Coeffects は「依存変化の感知」を解決する。両者がコンポーネントインスタンス上で協調するには、完全なライフサイクル状態機械が必要である。論文 §4.3 がこの機構を与え、Provider/Consumer のアンロード順序が最も重要な工学的詳細である。
完全状態機械
[論文原文の結論 §4.3 Def 49] コンポーネント（fiber）の完全ライフサイクル状態機械：
七つの L- 原語：
| 原語 | トリガ | 意味 |
|---|---|---|
| L-Begin | target ≠ ⊥ かつ fiber が Inactive | Reloading に入り、committed view を記録し、effect iterator を起動 |
| L-Iter | Reloading 中、target = ω、iterator が Just(i') を産出 | 一回の iteration の effect を適用し、inverse を累算器に複合 |
| L-Finish | Reloading 中、iterator が Nothing を産出 | すべての effect のインストール完了、Active に遷移 |
| L-Divert | Reloading 中、target ≠ ω（依存が変化） | 現 iteration を中止/着陸させ、Unloading に入る（abort または land 後 unload） |
| L-Raise | iteration がエラー ξ を送出 | ξ を携えて Unloading に入る；以降の L-Unload が既存の累算器を適用 |
| L-Leave | Active 中、target ≠ ω | Unloading をマークするが inverse は適用せず、coeffect の提供を停止 |
| L-Unload | Unloading 中、¬ relied_n(γ) | 累算器 g を適用し、Inactive に遷移 |
Provider と Consumer のアンロード順序
[論文原文の結論 §4.3.1] これは論文で最も重要な工学的機構の一つである。基本計算体系の L-Unload は「provision の削除」と「inverse の実行」を一緒に行い、consumer の teardown のための区間を残さない。もし provider が直接 inverse を適用して資源を解放した時、consumer がまだその provider の依存を使っていると、「データベース接続プールが閉じたのにトランザクションが未コミット」といったクラッシュが起きる。
論文は Unloading 中間状態と guard ¬ relied_n(γ)（n に依存する fiber がもういない）を導入し、正しい順序を保証する：
- L-Leave：Provider n は
Unloadingをマークし、coeffect の提供を停止（その σ はσ_γの union から外れる）が、自身の committed view と inverse はそのまま保持； - Consumer m は依存が間もなく消失することを検出（target view が ⊥ になるか他の fiber を指す）；
- Consumer m は committed view 内の旧依存を使ってクリーンアップを完了する——
σ_γはActivefiber だけを union するため、Unloadingfiber のバインディングは他の fiber から見えないが、consumer 自身の committed view は依然としてそれを指している； L-Unloadは guard¬ relied_n(γ)が満たされた時に実行される——すなわち n に依存するすべての consumer が deactivate 済み；- Provider n はこの時になって初めて自身の inverse を実行し、資源を解放する。
この機構は以下を解決する：
- 接続プールを閉じる前に接続の返却を待つ
- データベースを閉じる前にトランザクションのコミットを待つ
- Tool Provider をアンロードする前にそれを使用中の Agent を待つ
- 親コンポーネント退出時に子コンポーネントへカスケードクリーンアップ
[論文原文の結論 §4.4.4 Thm 66] guard はデッドロックしない：σ_γ は Active fiber だけを union し、L-Leave で n をマークすると、そのテーブルは σ_γ から離れ、どの target view も n を指せなくなり、n に committed したすべての consumer は自身の teardown に追い込まれる；依存グラフは ≺ 関係に沿って下向きに伝播し、非循環性 + 有限性が guard 解放を保証する（Progress 定理 参照）。
Inertia：非同期読み込み中に依存が変化したらどうするか
[論文原文の結論 §4.3.3] 現代の effect はしばしば非同期である（fetch、ファイル IO、サブ Agent 呼び出し）。iteration が飛行中（async Future）になったら、それは land しなければならず、abort できない。飛行中に target view が変化した場合、L-Divert は「着陸してから unload」分岐しか選べず、「iteration を中止」することはできない——iteration が一度 Future にコミットされるとキャンセル不能だからである。
三つの関連概念：
- Inertia（慣性）：飛行中の transition ハンドル、キャンセル不能、着陸を待つしかない；
- Iteration boundary：L-Divert が介入する粒度——iteration 境界でのみ target 変化を検査；
- Partial rollback：蓄積された inverse は適用され、未完了部分はロールバック；
- reload と unload の相互リンク：
reload完了後に target が変化していれば連鎖的にunloadに、unload完了後に target が変化していれば連鎖的にreloadに（Algorithm 5）。
この機構は、非同期読み込み中のコンポーネントで「半旧半新」が起こらないことを保証する——Active に遷移して完了するか、L-Divert/L-Raise で Unloading に入り完全にロールバックするかのいずれかである（Resolution Coherence 定理 に対応）。
理論と実装の対応表
[論文原文の結論 §5.1 Table 2] 論文の形式概念から Cordis 実装への対応：
| 理論概念 | Cordis 実装 |
|---|---|
| Unified Context Γ∞ | ctx、第一級コンテキスト |
| Revertible Effect | ctx.effect(callback) |
| Coeffect の登録とアクセス | ctx.set(key, value) / ctx.get(key) |
| Component Instantiation | ctx.use(component, config) |
| Dependency Specification | fiber.inject（理論上の d） |
| Inverse Accumulator | fiber.dispose |
| Committed View | fiber.committed |
| Target View | fiber.target（refresh が再計算） |
| Isolation | ctx.isolate(key, realm) |
| Interception | ctx.intercept(key, metadata) |
| Inertia | fiber.inertia（飛行中の transition ハンドル） |
| Lifecycle State | fiber.state（LOADING=Reloading, FAILED=Inactive(ξ)） |
Fiber と React Fiber の違い
[原文に基づく推論] 論文 Def 44 は fiber をコンポーネントの一回のインスタンス化として定義し、(d, p, e, π, σ, τ, θ) を携える——親 fiber、自身の coeffect 表、retirement マーカー、ライフサイクル状態。これは React Fiber とは名前が似ているだけ概念が異なる：React Fiber は React 内部の reconciliation 単位であり、コンポーネントツリー走査状態を保持する；Cordis Fiber は動的合成計算体系におけるコンポーネントインスタンスであり、effect 累算器、committed view、ライフサイクル状態機械を保持する。両者とも "fiber" の「軽量実行スレッド」の意味を借りているが、理論的枠組みは完全に異なる。
次は、この機構がメタ理論的に何を保証するかを見る：形式定理の工学的翻訳。