docs: add Chinese translation to RESEARCH_GAP_ANALYSIS.md

Full bilingual (zh-CN / en) gap analysis for easier reading by Chinese-speaking team members.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

RESEARCH_GAP_ANALYSIS.md

@@ -0,0 +1,647 @@
+# 研究差距分析：lambdagentpaas 与 Agent 编程范式论文对照
+
+> **日期**：2026-04-04
+> **分支**：`research`
+> **分析论文**：
+> - **论文 I**：lambdagent：一种形式化的 LLM Agent 组合 DSL（λA 类型化 Lambda 演算 + Lint）
+> - **论文 II**：LLM Agent 程序的操作语义（23 条概率归约规则、Agent CEK 机器、充分性定理）
+> - **论文 III**：LLM Agent 组合的类型与效果系统（15 条类型规则、效果代数、分级类型用于成本预测）
+
+---
+
+## 1. 实现覆盖总结
+
+| 论文 | 核心贡献 | 实现状态 | 覆盖率 |
+|------|---------|---------|--------|
+| **论文 I** | λA DSL + Lint | 接近完成 | **~90%** |
+| **论文 II** | 操作语义 + CEK 机器 | 部分完成 | **~55%** |
+| **论文 III** | 类型与效果系统 | 几乎未实现 | **~10%** |
+
+---
+
+## 2. 论文 I（λA DSL + Lint）— 覆盖率 ~90%
+
+### 已实现
+
+| 理论贡献 | 实现 | 文件 |
+|---------|------|------|
+| 11 个项构造器 | 13 个 Python 类（Term 子类） | `lambdagent/primitives.py`, `extensions.py` |
+| 类型系统 `Γ; Σ ⊢ e : τ` | 运行时 isinstance 分派（无静态检查） | `lambdagent/core.py` |
+| `from_config` 编译器（YAML → λA） | 5 类型分派，999 LOC | `lambdagent/fromconfig/compiler.py` |
+| Lint 工具（16 规则，L001–L025） | 框架感知 lint v3，含 L004a/b/c/d | `lambdagent/fromconfig/lint.py` |
+| 835 GitHub 配置评估 | 已完成，94.1% 缺陷率 | `docs/`，评估脚本 |
+| 终止定理 5.4 | `maxSteps` 运行时强制执行 | `lambdagent/primitives.py`（Loop） |
+| 语义忠实性测试 | 125/125 通过 | `lambdagent/tests/` |
+
+### 差距
+
+| 差距 | 描述 | 影响 |
+|------|------|------|
+| **语义保持变换** | 无用于安全重构的等式理论 | 无法自动重构 agent 组合 |
+| **静态类型检查** | 论文中有类型系统但未在编译时强制执行 | 类型不匹配仅在运行时被捕获 |
+| **Coq 机械化** | 论文证明仅存在于纸面 | 形式化保证的可信度较低 |
+
+---
+
+## 3. 论文 II（操作语义 + CEK 机器）— 覆盖率 ~55%
+
+### 已实现
+
+| 理论贡献 | 实现 | 状态 |
+|---------|------|------|
+| β-归约执行器 | `Executor.reduce()`，基于 isinstance 分派 | ✅ 覆盖全部 11 个构造 |
+| ReAct 7 阶段大步规则（B-React） | `ReActEngine` + `TerminationOracle` | ✅ 完成 |
+| 轨迹记录 | 每次 LLM/工具调用记录在 `TraceEntry` 中 | ✅ 完成 |
+| CEK 机器 | `cek_machine.py`（420 LOC） | ⚠️ 存在但非主运行时 |
+| 成本向量 `c = (τ, λ, μ)` | 轨迹记录 token/时长 | ⚠️ 未按 CEK 规范实现 |
+
+### 差距
+
+| 差距 | 理论基础 | 影响 | 优先级 |
+|------|---------|------|--------|
+| **概率预言机 `O_{θ,T}`** | 定义 10：`O_{θ,T}: V* → Δ(V*)` | 无法建模 T>0 行为；无分布级推理 | P2 |
+| **CEK 机器作为主执行器** | 第 5 节：用于异步预言机调用的 Yield 机制 | 当前同步执行器在 LLM 调用时阻塞；CEK Yield 自然映射到 async/await | P1 |
+| **6 条代数定律未被利用** | 定理 36–41：结合律、单位元、循环展开、路由分配、对称性 | 无法优化或等价检查 agent 组合 | P1 |
+| **对合流定理未被强制执行** | 命题 30：`writes(f) ∩ writes(g) = ∅` 是调度无关性的前提 | `AsyncPar` 存在线程安全问题；无存储独立性检查 | P0 |
+| **标记互模拟** | 第 7.1 节：概率上下文等价 | 无法形式化验证两个 agent 行为等价 | P2 |
+| **求值上下文（定义 17）** | 7 种按值调用的上下文形式 | 隐含在递归 reduce 中；非显式/不可检查 | P2 |
+| **成本向量单调性（命题 23）** | 每步之后 `c' ≥ c` 分量递增 | 未精确跟踪；仅有事后轨迹统计 | P1 |
+
+---
+
+## 4. 论文 III（类型与效果系统）— 覆盖率 ~10%
+
+### 已实现
+
+| 理论贡献 | 实现 | 状态 |
+|---------|------|------|
+| MCP 工具 JSON Schema | MCP 工具有 schema 声明 | ⚠️ 存在但编译器忽略了 |
+| 运行时类型检查 | 执行器中的 `isinstance` | ⚠️ 仅运行时，非静态 |
+
+### 差距
+
+| 差距 | 理论基础 | 影响 | 优先级 |
+|------|---------|------|--------|
+| **15 条类型规则** | 第 3.3 节：T-Lam, T-App, T-Compose, T-If, T-Route, T-Loop, T-Pair, T-Fst/Snd, T-Tool, T-Guard, T-Memory, T-Val, T-Var, T-Sub | `f >> g` 即使 `output(f)` 与 `input(g)` 不兼容也能编译——运行时崩溃并浪费费用 | **P0** |
+| **Json(S) 类型** | 定义 2：复用 JSON Schema 作为结构化类型语言 | MCP 工具已声明 JSON Schema 但未用于类型检查 | P0 |
+| **子类型关系 `<:`** | 定义 5：Str <: Json(string)，JSON 对象的宽度/深度子类型 | 组合边界无子类型检查 | P0 |
+| **效果代数 `(ε, ·, pure)`** | 定义 6–7：pure, llm(m), io, state(s)，串行(·)、并行(∥)、迭代(εⁿ) | 无法追踪 agent 产生什么效果；无法区分纯与有副作用的 agent | **P0** |
+| **代数效果处理器** | 第 6 节（论文 III）：生产、测试、轨迹处理器 | 测试需要调用真实 LLM API；无法在效果层面 mock；无环境切换 | **P0** |
+| **分级类型 `(p, t, l, m)`** | 定义 11–12：成功概率、token 数、延迟、成本作为静态上界 | 执行前无成本预测；开发者只能从账单中得知成本 | **P1** |
+| **效果子类型格** | 定义 9：`pure ≤ ε` 对所有 ε 成立；单调性（命题 10） | 无效果级组合安全 | P1 |
+| **处理器类型保持** | 定理（处理器切换保持类型安全） | 无法保证安全的处理器替换 | P1 |
+| **精化类型 `{x:τ|P(x)}`** | T-Guard 输出类型编码后条件 | Guard 后条件未在类型系统中传播 | P2 |
+| **T-Compose 规则 `B <: B'`** | 核心规则：`f: A →^ε1 B, g: B' →^ε2 C, B <: B'` | **最具影响力的缺失特性** — 静态防止错误组合 | **P0** |
+
+---
+
+## 5. 论文如何解决核心痛点
+
+### 痛点："Agent 无法高效并行工作"
+
+**论文 II 命题 30（对合流）**：在存储独立性（`writes(f) ∩ writes(g) = ∅`）条件下，`Pair(f, g)` 无论调度策略（左优先、右优先、交错）如何，都产生相同的输出分布。
+
+**当前差距**：`multiagent.py` 中的 `AsyncPar` 使用 `ThreadPoolExecutor` 但未验证存储独立性。
+
+**所需实现**：
+```python
+# multiagent.py — AsyncPar 安全检查
+def apply(self, input_str, ctx):
+    # 强制执行论文 II 命题 30 的前提条件
+    for i, a in enumerate(self.agents):
+        for j, b in enumerate(self.agents):
+            if i < j and not writes(a).isdisjoint(writes(b)):
+                raise StoreConflictError(
+                    f"对合流要求存储独立性："
+                    f"{a.name} 与 {b.name} 写入重叠的键"
+                )
+    # 每个分支 fork 上下文（独立的 Γ 和 trace）
+    results = await asyncio.gather(*[
+        agent.apply_async(input_str, ctx.fork())
+        for agent in self.agents
+    ])
+    return results
+```
+
+### 痛点："Agent 无法跨业务需求复用"
+
+**论文 III T-Compose 规则**：`f >> g` 要求 `output(f) <: input(g)`。没有此检查，在新流水线中复用 agent 可能会静默失败。
+
+**当前差距**：agent 无类型标注；组合边界无编译时检查。
+
+### 痛点："Agent 无法高效协作"
+
+**论文 III 效果代数 + 处理器**：同一 agent，不同执行环境：
+
+| 处理器 | llm(m) | io | state(s) |
+|--------|--------|-----|----------|
+| **生产** | 真实 LLM API 调用 | 真实工具执行 | Redis/PostgreSQL |
+| **测试** | Mock 响应（确定性） | Mock 工具 | 内存字典 |
+| **轨迹** | 真实调用 + 完整日志 | 真实调用 + I/O 记录 | 真实存储 + 审计轨迹 |
+
+**当前差距**：无处理器机制。测试总是调用真实 API。无法在不修改 agent 代码的情况下切换执行语义。
+
+### 痛点："无法在运行前预测成本"
+
+**论文 III 分级类型（定义 11–12）**：
+
+| 组合 | 概率 | Token 数 | 延迟 | 成本 |
+|------|------|---------|------|------|
+| 串行 `g1 · g2` | `p1 × p2` | `t1 + t2` | `l1 + l2` | `m1 + m2` |
+| 并行 `g1 ∥ g2` | `p1 × p2` | `t1 + t2` | `max(l1, l2)` | `m1 + m2` |
+| 迭代 `gⁿ` | `pⁿ` | `n × t` | `n × l` | `n × m` |
+| Guard `(k 次重试)` | `1-(1-p)^k` | `k × t` | `k × l` | `k × m` |
+
+**当前差距**：成本仅在执行后通过轨迹统计得知。无静态估算。
+
+---
+
+## 6. 代数定律 — 未被利用的优化潜力
+
+论文 II 证明了 6 条代数定律（定理 36–41），可实现安全的、语义保持的 agent 重构：
+
+| 定律 | 表述 | 实际用途 |
+|------|------|---------|
+| **组合结合律** | `(f >> g) >> h ≡ f >> (g >> h)` | 重新分组流水线是安全的 |
+| **左单位元** | `Id >> f ≡ f` | 消除 identity agent |
+| **右单位元** | `f >> Id ≡ f` | 消除尾部 identity |
+| **循环展开** | `Loop(b, c, n) ≡ If(c, Id, b >> Loop(b, c, n-1))` | 安全地展开/折叠循环 |
+| **路由分配** | `Route(c, {li: fi}) >> g ≡ Route(c, {li: fi >> g})` | 将后处理推入分支 |
+| **对对称性** | `Pair(f, g) ≡ swap ∘ Pair(g, f)` | 并行分支与顺序无关 |
+
+**非定律（命题 42）**：`Guard(a, P, k) >> g ≢ Guard(a >> g, P', k)` — Guard 不满足对组合的分配律。这是开发者在没有形式化指导下可能踩入的正确性陷阱。
+
+**当前差距**：这些定律均未实现为重写规则或优化 pass。
+
+---
+
+## 7. 待办清单
+
+### P0 — 关键（理论到实践的基础）
+
+- [ ] **实现 T-Compose 类型检查**（论文 III §3.3.3）
+  - 为 YAML schema 添加 `inputType` / `outputType` 标注
+  - 实现 `is_subtype()` 及 Json(S) 结构子类型
+  - 在 `compiler.py` 中检查组合边界
+  - 错误信息应引用论文 III T-Compose 规则
+
+- [ ] **实现效果标注**（论文 III §4）
+  - 定义效果枚举：`pure | llm(m) | io | state(s)`
+  - 实现串行 `·`、并行 `∥`、迭代 `εⁿ` 组合
+  - 编译期间为每个 Term 标注计算效果
+  - 为 YAML schema 添加 `effectAnnotation` 字段
+
+- [ ] **强制执行 Pair 存储独立性**（论文 II 命题 30）
+  - 为全部 11 个构造实现 `writes(term)` 分析
+  - 在 `AsyncPar` 执行前添加存储独立性检查
+  - 实现 `ctx.fork()` 以便每个并行分支有独立的 Context 副本
+  - 修复 `AsyncPar` 线程安全问题（迁移至 `asyncio`）
+
+- [ ] **实现代数效果处理器**（论文 III §6）
+  - 定义效果签名：`LLM`、`ToolIO`、`State`、`Cost`
+  - 实现三种标准处理器：`ProductionHandler`、`TestHandler`、`TraceHandler`
+  - 允许在 `Runtime.execute()` 级别注入处理器
+  - 通过测试证明处理器类型保持：切换处理器保持类型安全
+
+### P1 — 重要（核心引擎升级）
+
+- [ ] **将 CEK 机器提升为主执行器**（论文 II §5）
+  - 用 CEK 状态机替换递归 `Executor.reduce()`
+  - 实现 Yield 作为 `async/await` 以实现非阻塞 LLM/工具调用
+  - 实现所有 continuation 帧（定义 27）：`compK`、`loopK`、`pairLK`、`pairRK`、`guardK`、`memK`
+  - 确保 CEK ↔ 小步对应性（定理 28）
+
+- [ ] **实现分级成本预测**（论文 III §4.3）
+  - 定义 `CostGrade = (p: float, t: int, l: float, m: float)`
+  - 实现分级组合规则（定义 11–12）
+  - 编译时为每个 agent 流水线计算最坏情况成本
+  - 在 API 中暴露成本预测：`POST /api/v1/agents/{id}/cost-estimate`
+
+- [ ] **实现代数定律作为重写规则**（论文 II 定理 36–41）
+  - 在编译器中实现 6 条定律作为 AST 重写 pass
+  - 添加 identity 消除（左/右单位元定律）
+  - 添加路由分配优化
+  - 对 Guard 分配反模式发出警告（命题 42）
+
+- [ ] **精确成本向量累积**（论文 II 定义 5）
+  - 按 CEK 步骤跟踪 `c = (tokens, latency, cost)`
+  - 将成本单调性（命题 23）作为运行时不变量验证
+  - 在轨迹输出中暴露每步成本
+
+### P2 — 锦上添花（研究完整性）
+
+- [ ] **概率预言机建模**（论文 II 定义 10）
+- [ ] **标记互模拟用于程序等价**（论文 II §7.1）
+- [ ] **显式求值上下文**（论文 II 定义 17）
+- [ ] **精化类型传播**（论文 III T-Guard）
+- [ ] **Coq 机械化**（论文 I §9，论文 II §10）
+- [ ] **完整概率充分性验证**（论文 II 定理 33）
+
+---
+
+## 8. 实现依赖图
+
+```
+P0: T-Compose 类型检查
+  └──> P0: 效果标注（效果是函数类型 τ1 →^ε τ2 的一部分）
+        └──> P0: 代数效果处理器（处理器实现效果签名）
+              └──> P1: 分级成本预测（分级扩展效果为定量上界）
+
+P0: Pair 存储独立性
+  └──> P1: CEK 机器（CEK Yield 实现真正的异步并行）
+
+P1: 代数定律作为重写
+  └──> P2: 标记互模拟（互模拟经验性验证定律正确性）
+
+P1: CEK 机器
+  └──> P1: 精确成本向量（CEK 按转换跟踪成本）
+        └──> P1: 分级成本预测（运行时成本验证静态预测）
+```
+
+### 推荐实现顺序：
+
+```
+第一阶段（基础）：
+  1. T-Compose 类型检查 + Json(S) 子类型
+  2. 全部 11 个构造的效果标注
+  3. Pair 存储独立性强制执行 + ctx.fork()
+
+第二阶段（引擎）：
+  4. CEK 机器作为主执行器（Yield → async/await）
+  5. 代数效果处理器（生产/测试/轨迹）
+  6. 精确成本向量跟踪
+
+第三阶段（优化）：
+  7. 分级成本预测（静态）
+  8. 代数定律作为重写规则
+  9. Identity 消除 + 路由分配
+
+第四阶段（研究）：
+  10. 概率预言机建模
+  11. 标记互模拟
+  12. Coq 机械化
+```
+
+---
+
+## 9. 核心洞察
+
+三篇论文为如何让 agent 并行工作、可复用、高效协作提供了**完整的理论答案**：
+
+| 关注点 | 理论解决方案 | 论文 |
+|--------|------------|------|
+| 并行安全 | 对合流定理 + 存储独立性 | 论文 II 命题 30 |
+| 复用安全 | 通过 T-Compose 的静态类型检查 | 论文 III §3.3.3 |
+| 成本控制 | 分级类型 `(p, t, l, m)` | 论文 III §4.3 |
+| 环境切换 | 代数效果处理器 | 论文 III §6 |
+| 安全重构 | 6 条代数定律 | 论文 II 定理 36–41 |
+| 语义等价 | 标记概率互模拟 | 论文 II §7.1 |
+
+**最大的差距是论文 III 的类型与效果系统——几乎完全未实现。** 这是"agent 无法高效协作"这一感受的根本原因：没有静态检查，组合只能靠试错。
+
+---
+---
+
+# Research Gap Analysis: lambdagentpaas vs. Agent Programming Paradigm Papers
+
+> **Date**: 2026-04-04
+> **Branch**: `research`
+> **Papers Analyzed**:
+> - **Paper I**: lambdagent: A Formally-Grounded DSL for LLM Agent Composition (λA typed Lambda calculus, lint)
+> - **Paper II**: Operational Semantics for LLM Agent Programs (23 probabilistic reduction rules, Agent CEK Machine, adequacy)
+> - **Paper III**: A Type and Effect System for LLM Agent Composition (15 type rules, effect algebra, graded types for cost prediction)
+
+---
+
+## 1. Implementation Coverage Summary
+
+| Paper | Core Contribution | Implementation Status | Coverage |
+|-------|------------------|----------------------|----------|
+| **Paper I** | λA DSL + Lint | Near-complete | **~90%** |
+| **Paper II** | Operational Semantics + CEK Machine | Partial | **~55%** |
+| **Paper III** | Type & Effect System | Minimal | **~10%** |
+
+---
+
+## 2. Paper I (λA DSL + Lint) — Coverage ~90%
+
+### Implemented
+
+| Theoretical Contribution | Implementation | Files |
+|--------------------------|----------------|-------|
+| 11 term constructors | 13 Python classes (Term subclasses) | `lambdagent/primitives.py`, `extensions.py` |
+| Type system `Γ; Σ ⊢ e : τ` | Runtime isinstance dispatch (no static checking) | `lambdagent/core.py` |
+| `from_config` compiler (YAML → λA) | 5-type dispatch, 999 LOC | `lambdagent/fromconfig/compiler.py` |
+| Lint tool (16 rules, L001–L025) | Framework-aware lint v3 with L004a/b/c/d | `lambdagent/fromconfig/lint.py` |
+| 835 GitHub config evaluation | Completed, 94.1% defect rate | `docs/`, evaluation scripts |
+| Termination theorem 5.4 | `maxSteps` enforced at runtime | `lambdagent/primitives.py` (Loop) |
+| Semantic faithfulness tests | 125/125 passing | `lambdagent/tests/` |
+
+### Gaps
+
+| Gap | Description | Impact |
+|-----|-------------|--------|
+| **Semantic-preserving transformations** | No equational theory for safe refactoring | Cannot auto-refactor agent compositions |
+| **Static type checking** | Type system exists in paper but not enforced at compile time | Type mismatches only caught at runtime |
+| **Coq mechanization** | Paper proofs are on paper only | Lower trustworthiness of formal guarantees |
+
+---
+
+## 3. Paper II (Operational Semantics + CEK Machine) — Coverage ~55%
+
+### Implemented
+
+| Theoretical Contribution | Implementation | Status |
+|--------------------------|----------------|--------|
+| β-reduction executor | `Executor.reduce()` with isinstance dispatch | ✅ Covers all 11 constructs |
+| ReAct 7-stage big-step rule (B-React) | `ReActEngine` with `TerminationOracle` | ✅ Complete |
+| Trace recording | Every LLM/tool call recorded in `TraceEntry` | ✅ Complete |
+| CEK Machine | `cek_machine.py` (420 LOC) | ⚠️ Exists but NOT the main runtime |
+| Cost vector `c = (τ, λ, μ)` | Trace records token/duration | ⚠️ Not per CEK spec |
+
+### Gaps
+
+| Gap | Theoretical Basis | Impact | Priority |
+|-----|-------------------|--------|----------|
+| **Probabilistic oracle `O_{θ,T}`** | Definition 10: `O_{θ,T}: V* → Δ(V*)` | Cannot model T>0 behavior; no distribution-level reasoning | P2 |
+| **CEK Machine as primary executor** | Section 5: Yield mechanism for async oracle calls | Current sync executor blocks on LLM calls; CEK Yield maps naturally to async/await | P1 |
+| **6 algebraic laws not exploited** | Theorems 36–41: associativity, unit, loop-unfold, route-distribute, pair-symmetry | No optimization or equivalence checking of agent compositions | P1 |
+| **Pair confluence theorem not enforced** | Proposition 30: `writes(f) ∩ writes(g) = ∅` required for schedule-independence | `AsyncPar` has thread-safety issues; no store-independence check | P0 |
+| **Labeled bisimulation** | Section 7.1: probabilistic contextual equivalence | Cannot formally verify two agents are behaviorally equivalent | P2 |
+| **Evaluation contexts (Definition 17)** | 7 context forms for call-by-value | Implicit in recursive reduce; not explicit/inspectable | P2 |
+| **Cost vector monotonicity (Proposition 23)** | `c' ≥ c` component-wise after each step | Not tracked precisely; only post-hoc trace statistics | P1 |
+
+---
+
+## 4. Paper III (Type & Effect System) — Coverage ~10%
+
+### Implemented
+
+| Theoretical Contribution | Implementation | Status |
+|--------------------------|----------------|--------|
+| MCP tool JSON Schema | MCP tools have schema declarations | ⚠️ Exists but compiler ignores it |
+| Runtime type checks | `isinstance` in executor | ⚠️ Runtime only, not static |
+
+### Gaps
+
+| Gap | Theoretical Basis | Impact | Priority |
+|-----|-------------------|--------|----------|
+| **15 type rules** | Section 3.3: T-Lam, T-App, T-Compose, T-If, T-Route, T-Loop, T-Pair, T-Fst/Snd, T-Tool, T-Guard, T-Memory, T-Val, T-Var, T-Sub | `f >> g` compiles even when `output(f)` is incompatible with `input(g)` — crashes at runtime after spending money | **P0** |
+| **Json(S) types** | Definition 2: reuse JSON Schema as structural type language | MCP tools already declare JSON Schema but it's not used for type checking | P0 |
+| **Subtype relation `<:`** | Definition 5: Str <: Json(string), width/depth subtyping for JSON objects | No subtype checking at composition boundaries | P0 |
+| **Effect algebra `(ε, ·, pure)`** | Definition 6–7: pure, llm(m), io, state(s) with serial (·), parallel (∥), iteration (εⁿ) | No tracking of what effects an agent produces; cannot distinguish pure from effectful agents | **P0** |
+| **Algebraic effect handlers** | Section 6 (of Paper III): production, test, trace handlers | Testing requires calling real LLM APIs; cannot mock at effect level; no environment switching | **P0** |
+| **Graded types `(p, t, l, m)`** | Definition 11–12: success probability, token count, latency, cost as static bounds | No cost prediction before execution; developers only learn cost from bills | **P1** |
+| **Effect subtype lattice** | Definition 9: `pure ≤ ε` for all ε; monotonicity (Proposition 10) | No effect-level composition safety | P1 |
+| **Handler type preservation** | Theorem (handler switching preserves type safety) | Cannot guarantee safe handler replacement | P1 |
+| **Refinement types `{x:τ|P(x)}`** | T-Guard output type encodes postcondition | Guard postconditions not propagated through type system | P2 |
+| **T-Compose rule `B <: B'`** | Core rule: `f: A →^ε1 B, g: B' →^ε2 C, B <: B'` | **The single most impactful missing feature** — prevents bad compositions statically | **P0** |
+
+---
+
+## 5. How Papers Address the Core Pain Points
+
+### Pain Point: "Agents can't work in parallel efficiently"
+
+**Paper II Proposition 30 (Pair Confluence)**: Under store independence (`writes(f) ∩ writes(g) = ∅`), `Pair(f, g)` produces the same output distribution regardless of scheduling strategy (left-first, right-first, interleaved).
+
+**Current gap**: `AsyncPar` in `multiagent.py` uses `ThreadPoolExecutor` without verifying store independence. Thread-safety issues are flagged in `ENGINEERING_GAP_ANALYSIS.md` as P1.
+
+**Required implementation**:
+```python
+# multiagent.py — AsyncPar safety check
+def apply(self, input_str, ctx):
+    # Enforce Paper II Proposition 30 precondition
+    for i, a in enumerate(self.agents):
+        for j, b in enumerate(self.agents):
+            if i < j and not writes(a).isdisjoint(writes(b)):
+                raise StoreConflictError(
+                    f"Pair confluence requires store independence: "
+                    f"{a.name} and {b.name} write to overlapping keys"
+                )
+    # Fork context per branch (independent Γ and trace)
+    results = await asyncio.gather(*[
+        agent.apply_async(input_str, ctx.fork())
+        for agent in self.agents
+    ])
+    return results
+```
+
+### Pain Point: "Agents can't be reused across different business needs"
+
+**Paper III T-Compose rule**: `f >> g` requires `output(f) <: input(g)`. Without this check, reusing an agent in a new pipeline may silently break.
+
+**Current gap**: No type annotations on agents; no compile-time checking of composition boundaries.
+
+**Required implementation**:
+```yaml
+# Agent with type declarations (Paper III Definition 1)
+skillId: web-research
+inputType: Str
+outputType: Json(object({results: array(string), sources: array(string)}))
+effectAnnotation: llm(qwen3-max) · io
+costGrade: {p: 0.95, t: 2000, l: 3.5, m: 0.02}
+```
+
+```python
+# compiler.py — Type checking at composition
+def compile_chain(steps):
+    for i in range(len(steps) - 1):
+        f_out = infer_output_type(steps[i])
+        g_in = infer_input_type(steps[i + 1])
+        if not is_subtype(f_out, g_in):
+            raise AgentTypeError(
+                f"Pipeline type mismatch at step {i}: "
+                f"{f_out} is not subtype of {g_in}"
+            )
+```
+
+### Pain Point: "Agents can't collaborate efficiently"
+
+**Paper III Effect Algebra + Handlers**: Same agent, different execution environments:
+
+| Handler | llm(m) | io | state(s) |
+|---------|--------|-----|----------|
+| **Production** | Real LLM API call | Real tool execution | Redis/PostgreSQL |
+| **Test** | Mock responses (deterministic) | Mock tools | In-memory dict |
+| **Trace** | Real call + full logging | Real call + I/O recording | Real store + audit trail |
+
+**Current gap**: No handler mechanism. Testing always hits real APIs. No way to switch execution semantics without changing agent code.
+
+### Pain Point: "No way to predict cost before running"
+
+**Paper III Graded Types (Definition 11–12)**:
+
+| Composition | Probability | Tokens | Latency | Cost |
+|-------------|-------------|--------|---------|------|
+| Serial `g1 · g2` | `p1 × p2` | `t1 + t2` | `l1 + l2` | `m1 + m2` |
+| Parallel `g1 ∥ g2` | `p1 × p2` | `t1 + t2` | `max(l1, l2)` | `m1 + m2` |
+| Iteration `gⁿ` | `pⁿ` | `n × t` | `n × l` | `n × m` |
+| Guard `(k retries)` | `1-(1-p)^k` | `k × t` | `k × l` | `k × m` |
+
+**Current gap**: Cost is only known after execution via trace statistics. No static estimation.
+
+---
+
+## 6. Algebraic Laws — Untapped Optimization Potential
+
+Paper II proves 6 algebraic laws (Theorems 36–41) that enable safe, semantic-preserving agent refactoring:
+
+| Law | Statement | Practical Use |
+|-----|-----------|---------------|
+| **Composition associativity** | `(f >> g) >> h ≡ f >> (g >> h)` | Regrouping pipelines is safe |
+| **Left unit** | `Id >> f ≡ f` | Eliminate identity agents |
+| **Right unit** | `f >> Id ≡ f` | Eliminate trailing identity |
+| **Loop unfolding** | `Loop(b, c, n) ≡ If(c, Id, b >> Loop(b, c, n-1))` | Safe to unfold/fold loops |
+| **Route distribution** | `Route(c, {li: fi}) >> g ≡ Route(c, {li: fi >> g})` | Push post-processing into branches |
+| **Pair symmetry** | `Pair(f, g) ≡ swap ∘ Pair(g, f)` | Parallel branches are order-independent |
+
+**Non-law (Proposition 42)**: `Guard(a, P, k) >> g ≢ Guard(a >> g, P', k)` — Guard does NOT distribute over composition. This is a correctness trap that developers may fall into without formal guidance.
+
+**Current gap**: None of these laws are implemented as rewrite rules or optimization passes.
+
+---
+
+## 7. TODO List
+
+### P0 — Critical (Theory-to-Practice Foundation)
+
+- [ ] **Implement T-Compose type checking** (Paper III §3.3.3)
+  - Add `inputType` / `outputType` annotations to YAML schema
+  - Implement `is_subtype()` with Json(S) structural subtyping
+  - Check composition boundaries in `compiler.py`
+  - Error messages should reference Paper III T-Compose rule
+
+- [ ] **Implement effect annotations** (Paper III §4)
+  - Define effect enum: `pure | llm(m) | io | state(s)`
+  - Implement serial `·`, parallel `∥`, iteration `εⁿ` composition
+  - Annotate each Term with computed effect during compilation
+  - Add `effectAnnotation` field to YAML schema
+
+- [ ] **Enforce Pair store-independence** (Paper II Proposition 30)
+  - Implement `writes(term)` analysis for all 11 constructs
+  - Add store-independence check before `AsyncPar` execution
+  - Implement `ctx.fork()` for independent Context copies per parallel branch
+  - Fix thread-safety issues in `AsyncPar` (migrate to `asyncio`)
+
+- [ ] **Implement algebraic effect handlers** (Paper III §6)
+  - Define effect signatures: `LLM`, `ToolIO`, `State`, `Cost`
+  - Implement three standard handlers: `ProductionHandler`, `TestHandler`, `TraceHandler`
+  - Allow handler injection at `Runtime.execute()` level
+  - Prove (test) handler type preservation: switching handler preserves type safety
+
+### P1 — Important (Core Engine Upgrade)
+
+- [ ] **Promote CEK Machine to primary executor** (Paper II §5)
+  - Replace recursive `Executor.reduce()` with CEK state machine
+  - Implement Yield as `async/await` for non-blocking LLM/tool calls
+  - Implement all continuation frames (Definition 27): `compK`, `loopK`, `pairLK`, `pairRK`, `guardK`, `memK`
+  - Ensure CEK ↔ small-step correspondence (Theorem 28)
+
+- [ ] **Implement graded cost prediction** (Paper III §4.3)
+  - Define `CostGrade = (p: float, t: int, l: float, m: float)`
+  - Implement graded composition rules (Definitions 11–12)
+  - Compute worst-case cost at compile time for each agent pipeline
+  - Expose cost prediction in API: `POST /api/v1/agents/{id}/cost-estimate`
+
+- [ ] **Implement algebraic laws as rewrite rules** (Paper II Theorems 36–41)
+  - Implement 6 laws as AST rewrite passes in compiler
+  - Add identity elimination (left/right unit laws)
+  - Add route distribution optimization
+  - Warn on Guard distribution anti-pattern (Proposition 42)
+
+- [ ] **Precise cost vector accumulation** (Paper II Definition 5)
+  - Track `c = (tokens, latency, cost)` per CEK step
+  - Verify cost monotonicity (Proposition 23) as runtime invariant
+  - Expose per-step cost in trace output
+
+### P2 — Nice-to-Have (Research Completeness)
+
+- [ ] **Probabilistic oracle modeling** (Paper II Definition 10)
+  - Model `O_{θ,T}: V* → Δ(V*)` for temperature > 0
+  - Implement path probability tracking (Definition 15)
+  - Enable distribution-level reasoning for T > 0
+
+- [ ] **Labeled bisimulation for program equivalence** (Paper II §7.1)
+  - Implement trace-based equivalence checking
+  - Two agents are equivalent if they produce same observable label sequences
+  - Use for automated regression testing of agent refactoring
+
+- [ ] **Explicit evaluation contexts** (Paper II Definition 17)
+  - Make evaluation contexts first-class (inspectable AST nodes)
+  - Enable "where are we in the pipeline?" debugging
+
+- [ ] **Refinement type propagation** (Paper III T-Guard)
+  - Propagate Guard postconditions `{x:B|P(x)}` through subsequent compositions
+  - Enable downstream agents to rely on Guard's verified output
+
+- [ ] **Coq mechanization** (Paper I §9, Paper II §10)
+  - Mechanize type safety (Progress + Preservation) in Coq
+  - Mechanize adequacy theorem in Coq
+  - Increases trustworthiness of formal guarantees
+
+- [ ] **Full probabilistic adequacy verification** (Paper II Theorem 33)
+  - Extend experiment 5 (5 programs, 1000 runs each) to broader program space
+  - Validate χ² goodness-of-fit across diverse agent compositions
+
+---
+
+## 8. Implementation Dependency Graph
+
+```
+P0: T-Compose type checking
+  └──> P0: Effect annotations (effects are part of function types τ1 →^ε τ2)
+        └──> P0: Algebraic effect handlers (handlers implement effect signatures)
+              └──> P1: Graded cost prediction (grades extend effects with quantitative bounds)
+
+P0: Pair store-independence
+  └──> P1: CEK Machine (CEK Yield enables true async parallel)
+
+P1: Algebraic laws as rewrites
+  └──> P2: Labeled bisimulation (bisimulation verifies law correctness empirically)
+
+P1: CEK Machine
+  └──> P1: Precise cost vectors (CEK tracks cost per transition)
+        └──> P1: Graded cost prediction (runtime cost validates static prediction)
+```
+
+### Recommended implementation order:
+
+```
+Phase 1 (Foundation):
+  1. T-Compose type checking + Json(S) subtyping
+  2. Effect annotations on all 11 constructs
+  3. Pair store-independence enforcement + ctx.fork()
+
+Phase 2 (Engine):
+  4. CEK Machine as primary executor (with Yield → async/await)
+  5. Algebraic effect handlers (production/test/trace)
+  6. Precise cost vector tracking
+
+Phase 3 (Optimization):
+  7. Graded cost prediction (static)
+  8. Algebraic laws as rewrite rules
+  9. Identity elimination + route distribution
+
+Phase 4 (Research):
+  10. Probabilistic oracle modeling
+  11. Labeled bisimulation
+  12. Coq mechanization
+```
+
+---
+
+## 9. Key Insight
+
+The three papers provide a **complete theoretical answer** to the question of how to make agents work in parallel, be reusable, and collaborate efficiently:
+
+| Concern | Theoretical Solution | Paper |
+|---------|---------------------|-------|
+| Parallel safety | Pair confluence theorem + store independence | Paper II Prop. 30 |
+| Reuse safety | Static type checking via T-Compose | Paper III §3.3.3 |
+| Cost control | Graded types `(p, t, l, m)` | Paper III §4.3 |
+| Environment switching | Algebraic effect handlers | Paper III §6 |
+| Safe refactoring | 6 algebraic laws | Paper II Thm. 36–41 |
+| Semantic equivalence | Labeled probabilistic bisimulation | Paper II §7.1 |
+
+**The largest gap is Paper III's type and effect system — almost entirely unimplemented.** This is the root cause of the feeling that "agents can't collaborate efficiently": without static checks, composition is trial-and-error.