元件生命週期與卸載順序
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】這是論文最重要的工程機制之一。base calculus 的 L-Unload 把「移除 provision」和「執行 inverse」放在一起，沒有為 consumer 的 teardown 留出區間。如果 provider 直接應用 inverse 釋放資源，而 consumer 還在用這個 provider 的依賴，就會出現「資料庫連線池被關閉、但事務還沒提交」的崩潰。
論文引入 Unloading 中間態和 guard ¬ relied_n(γ)（沒有 fiber 再依賴 n）來保證正確順序：
- L-Leave：Provider n 標記
Unloading，停止提供 coeffect（其 σ 離開σ_γ的 union），但保留自己的 committed view 和 inverse 未動； - Consumer m 偵測到依賴即將消失（target view 變為 ⊥ 或指向其他 fiber）；
- Consumer m 使用 committed view 中的舊依賴完成清理——因為
σ_γ只 unionActivefiber，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 不會死鎖：σ_γ 只 union Active fiber，一旦 L-Leave 標記 n，它的 table 離開 σ_γ，沒有 target view 能再指向 n，所有 committed 到 n 的 consumer 都被迫進入自己的 teardown，依賴圖沿 ≺ 關係向下傳遞，acyclicity + finite 保證 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 是 dynamic composition calculus 中的元件實例，承載 effect accumulator、committed view 和生命週期狀態機。兩者都借用「fiber」一詞的「輕量執行線索」含義，但理論框架完全不同。
下一步看這套機制在元理論上保證了什麼：形式化定理的工程翻譯。