# 研究差距分析：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 | 10 | 9 (含新增: 静态类型+重写规则) | 1 (Coq) | **~95%** |
| **论文 II** | 操作语义 + CEK 机器 | 12 | 9 (含新增: CEK+代数定律+合流+成本) | 3 (概率预言机/互模拟/求值上下文) | **~80%** |
| **论文 III** | 类型与效果系统 | 12 | 10 (含新增: 类型+效果+处理器+分级) | 2 (精化类型/完整15规则) | **~70%** |

> **更新 (2026-04-04)**: P0 (4项) + P1 (4项) 全部实现，共 175 个测试通过。
> 新增文件: `types.py`, `effects.py`, `store_analysis.py`, `handlers.py`, `cost_grade.py`, `rewrite.py`
> 升级文件: `cek_machine.py`, `core.py`, `primitives.py`, `extensions.py`, `multiagent.py`, `compiler.py`

---

## 2. 论文 I（λA DSL + Lint）— 覆盖率 ~95%

### 已实现

| 理论贡献 | 实现 | 文件 |
|---------|------|------|
| 11 个项构造器 | 13 个 Python 类（Term 子类） | `primitives.py`, `extensions.py` |
| 类型系统 `Γ; Σ ⊢ e : τ` | ✅ 静态 T-Compose 检查 + Json(S) 子类型 + 运行时 isinstance | `types.py` (44 tests) |
| `from_config` 编译器（YAML → λA） | 5 类型分派 + T-Compose 编译时检查 | `fromconfig/compiler.py` |
| Lint 工具（16 规则，L001–L025） | 框架感知 lint v3，含 L004a/b/c/d | `fromconfig/lint.py` |
| GitHub 大规模 lint 验证 | 2,225 YAML → 881 有效配置 → 835 成功 lint，786 (94.1%) 触发 ≥1 ERROR（含跨框架误报，实际缺陷率估计 ~65-70%） | `docs/research/THEORY.md` §7.0 |
| 终止定理 5.4 | `maxSteps` 运行时强制执行 | `primitives.py`（Loop） |
| 语义忠实性测试 | 125/125 + 175 新测试通过 | `lambdagent/tests/` |
| **语义保持变换** | ✅ 6 条代数定律作为 AST 重写规则 | `rewrite.py` (14 tests) |

### 差距

| 差距 | 描述 | 影响 |
|------|------|------|
| ~~**语义保持变换**~~ | ✅ 已通过 `rewrite.py` 实现（Thm 36-41） | ~~无法自动重构~~ |
| ~~**静态类型检查**~~ | ✅ 已通过 `types.py` T-Compose 检查实现 | ~~仅运行时捕获~~ |
| **Coq 机械化** | 论文证明仅存在于纸面 | 形式化保证的可信度较低 |

---

## 3. 论文 II（操作语义 + CEK 机器）— 覆盖率 ~80%

### 已实现

| 理论贡献 | 实现 | 状态 |
|---------|------|------|
| β-归约执行器 | `Executor.reduce()`，基于 isinstance 分派 | ✅ 覆盖全部 11 个构造 |
| ReAct 7 阶段大步规则（B-React） | `ReActEngine` + `TerminationOracle` | ✅ 完成 |
| 轨迹记录 | 每次 LLM/工具调用记录在 `TraceEntry` 中 | ✅ 完成 |
| CEK 机器（定义 27） | IfK/RouteK/CompK/LoopK/PairLK/PairRK/GuardK/MemK 全部 continuation 帧 | ✅ `cek_machine.py`（21 tests） |
| Yield 机制（§5） | CEK handler 集成 + `run_async()` | ✅ LLM/Tool 调用经由 handler 路由 |
| 成本向量 `c = (τ, λ, μ)` | CEK 每步跟踪 CostVector + `cost_summary()` | ✅ 按 CEK 规范实现 |
| 成本单调性（命题 23） | `CostMonotonicityViolation` 每步断言 `c' ≥ c` | ✅ 运行时不变量强制执行 |
| 对合流定理（命题 30） | `writes(f) ∩ writes(g) = ∅` 检查 + `ctx.fork()` 隔离 | ✅ `store_analysis.py`（20 tests） |
| 6 条代数定律（定理 36–41） | Identity 消除、路由分配、Loop 简化、Guard 反模式警告 | ✅ `rewrite.py`（14 tests） |

### 差距

| 差距 | 理论基础 | 影响 | 优先级 |
|------|---------|------|--------|
| **概率预言机 `O_{θ,T}`** | 定义 10：`O_{θ,T}: V* → Δ(V*)` | 无法建模 T>0 行为；无分布级推理 | P2 |
| **标记互模拟** | 第 7.1 节：概率上下文等价 | 无法形式化验证两个 agent 行为等价 | P2 |
| **显式求值上下文（定义 17）** | 7 种按值调用的上下文形式 | 隐含在 CEK continuation 中；非独立数据结构 | P2 |
| ~~**CEK 机器作为主执行器**~~ | ~~第 5 节~~ | ✅ 已实现 IfK/RouteK + handler + async | ~~P1~~ |
| ~~**6 条代数定律**~~ | ~~定理 36–41~~ | ✅ 已实现为 AST 重写规则 | ~~P1~~ |
| ~~**对合流定理**~~ | ~~命题 30~~ | ✅ writes() 分析 + ctx.fork() | ~~P0~~ |
| ~~**成本向量单调性**~~ | ~~命题 23~~ | ✅ CostMonotonicityViolation | ~~P1~~ |

---

## 4. 论文 III（类型与效果系统）— 覆盖率 ~70%

### 已实现

| 理论贡献 | 实现 | 状态 |
|---------|------|------|
| T-Compose 规则 `B <: B'` | `>>` 操作符构造时检查 `output(f) <: input(g)` | ✅ `types.py` — `check_compose_types()` (44 tests) |
| Json(S) 类型（定义 2） | LamType + T_JSON(schema) 复用 JSON Schema | ✅ `types.py` — `T_JSON()`, `parse_type_annotation()` |
| 子类型关系 `<:`（定义 5） | 宽度/深度子类型 + 数值层级 + 联合/元组类型 | ✅ `types.py` — `is_subtype()` |
| 15 条类型规则（§3.3） | T-Compose 已实现；Pair→元组类型；其他通过 `input_type`/`output_type` 属性支持 | ✅ 核心规则已覆盖（T-Compose, T-Pair, T-Sub） |
| 效果代数 `(ε, ·, pure)`（定义 6-7） | pure/llm(m)/io/state(s) + serial(·)/parallel(∥)/iterate(εⁿ) | ✅ `effects.py` (35 tests) |
| 效果子类型格（定义 9） | `pure ≤ state ≤ io ≤ llm` + `effect_leq()` + `max_effect()` | ✅ `effects.py` |
| 效果推断（§4） | `infer_effect_for_term()` 覆盖全部 11 个构造 | ✅ `effects.py` |
| 代数效果处理器（§6） | ProductionHandler / TestHandler / TraceHandler + `with_handler()` | ✅ `handlers.py` (23 tests) |
| 处理器类型保持 | 切换 handler 后 `input_type`/`output_type` 不变 | ✅ 测试验证 |
| 分级类型 `(p, t, l, m)`（定义 11-12） | `CostGrade` + `estimate_cost()` + 4 条组合规则 | ✅ `cost_grade.py` (18 tests) |

### 差距

| 差距 | 理论基础 | 影响 | 优先级 |
|------|---------|------|--------|
| **精化类型 `{x:τ|P(x)}`** | T-Guard 输出类型编码后条件 | Guard 后条件未在类型系统中传播 | P2 |
| **完整 15 条规则逐一实现** | T-Lam, T-App, T-If, T-Route, T-Loop, T-Guard, T-Memory, T-Val, T-Var | 部分规则（T-If, T-Route 等）仅有框架支持，未强制执行类型检查 | P2 |
| ~~**T-Compose 规则**~~ | ~~核心规则~~ | ✅ `types.py` is_subtype + check_compose_types | ~~P0~~ |
| ~~**Json(S) 类型**~~ | ~~定义 2~~ | ✅ T_JSON(schema) 结构子类型 | ~~P0~~ |
| ~~**子类型关系**~~ | ~~定义 5~~ | ✅ is_subtype() 宽度/深度/数值 | ~~P0~~ |
| ~~**效果代数**~~ | ~~定义 6-7~~ | ✅ effects.py serial/parallel/iterate | ~~P0~~ |
| ~~**代数效果处理器**~~ | ~~§6~~ | ✅ handlers.py 三种处理器 | ~~P0~~ |
| ~~**分级类型**~~ | ~~定义 11-12~~ | ✅ cost_grade.py 静态成本预测 | ~~P1~~ |
| ~~**效果子类型格**~~ | ~~定义 9~~ | ✅ effect_leq() + max_effect() | ~~P1~~ |
| ~~**处理器类型保持**~~ | ~~定理~~ | ✅ 测试验证 handler 切换保持类型 | ~~P1~~ |

---

## 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 — 关键（理论到实践的基础）

- [x] **实现 T-Compose 类型检查**（论文 III §3.3.3）✅ `lambdagent/types.py` — 44 tests
  - 为 YAML schema 添加 `inputType` / `outputType` 标注
  - 实现 `is_subtype()` 及 Json(S) 结构子类型
  - 在 `compiler.py` 中检查组合边界
  - 错误信息应引用论文 III T-Compose 规则

- [x] **实现效果标注**（论文 III §4）✅ `lambdagent/effects.py` — 35 tests
  - 定义效果枚举：`pure | llm(m) | io | state(s)`
  - 实现串行 `·`、并行 `∥`、迭代 `εⁿ` 组合
  - 编译期间为每个 Term 标注计算效果
  - 为 YAML schema 添加 `effectAnnotation` 字段

- [x] **强制执行 Pair 存储独立性**（论文 II 命题 30）✅ `lambdagent/store_analysis.py` — 20 tests
  - 为全部 11 个构造实现 `writes(term)` 分析
  - 在 `AsyncPar` 执行前添加存储独立性检查
  - 实现 `ctx.fork()` 以便每个并行分支有独立的 Context 副本
  - 修复 `AsyncPar` 线程安全问题（迁移至 `asyncio`）

- [x] **实现代数效果处理器**（论文 III §6）✅ `lambdagent/handlers.py` — 23 tests
  - 定义效果签名：`LLM`、`ToolIO`、`State`、`Cost`
  - 实现三种标准处理器：`ProductionHandler`、`TestHandler`、`TraceHandler`
  - 允许在 `Runtime.execute()` 级别注入处理器
  - 通过测试证明处理器类型保持：切换处理器保持类型安全

### P1 — 重要（核心引擎升级）

- [x] **将 CEK 机器提升为主执行器**（论文 II §5）✅ `lambdagent/cek_machine.py` — 21 tests
  - 用 CEK 状态机替换递归 `Executor.reduce()`
  - 实现 Yield 作为 `async/await` 以实现非阻塞 LLM/工具调用
  - 实现所有 continuation 帧（定义 27）：`compK`、`loopK`、`pairLK`、`pairRK`、`guardK`、`memK`
  - 确保 CEK ↔ 小步对应性（定理 28）

- [x] **实现分级成本预测**（论文 III §4.3）✅ `lambdagent/cost_grade.py` — 18 tests
  - 定义 `CostGrade = (p: float, t: int, l: float, m: float)`
  - 实现分级组合规则（定义 11–12）
  - 编译时为每个 agent 流水线计算最坏情况成本
  - 在 API 中暴露成本预测：`POST /api/v1/agents/{id}/cost-estimate`

- [x] **实现代数定律作为重写规则**（论文 II 定理 36–41）✅ `lambdagent/rewrite.py` — 14 tests
  - 在编译器中实现 6 条定律作为 AST 重写 pass
  - 添加 identity 消除（左/右单位元定律）
  - 添加路由分配优化
  - 对 Guard 分配反模式发出警告（命题 42）

- [x] **精确成本向量累积**（论文 II 定义 5）✅ 集成于 `cek_machine.py` cost_summary() + CostMonotonicityViolation
  - 按 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 | Core Contribution | Total Items | Implemented | Remaining Gaps | Coverage |
|-------|------------------|-------------|-------------|----------------|----------|
| **Paper I** | λA DSL + Lint | 10 | 9 (incl. new: static types + rewrite rules) | 1 (Coq) | **~95%** |
| **Paper II** | Operational Semantics + CEK Machine | 12 | 9 (incl. new: CEK+laws+confluence+cost) | 3 (prob. oracle / bisimulation / eval ctx) | **~80%** |
| **Paper III** | Type & Effect System | 12 | 10 (incl. new: types+effects+handlers+graded) | 2 (refinement types / full 15 rules) | **~70%** |

> **Update (2026-04-04)**: P0 (4 items) + P1 (4 items) all implemented, 175 tests passing.
> New files: `types.py`, `effects.py`, `store_analysis.py`, `handlers.py`, `cost_grade.py`, `rewrite.py`
> Upgraded: `cek_machine.py`, `core.py`, `primitives.py`, `extensions.py`, `multiagent.py`, `compiler.py`

---

## 2. Paper I (λA DSL + Lint) — Coverage ~95%

### Implemented

| Theoretical Contribution | Implementation | Files |
|--------------------------|----------------|-------|
| 11 term constructors | 13 Python classes (Term subclasses) | `primitives.py`, `extensions.py` |
| Type system `Γ; Σ ⊢ e : τ` | ✅ Static T-Compose checking + Json(S) subtyping + runtime isinstance | `types.py` (44 tests) |
| `from_config` compiler (YAML → λA) | 5-type dispatch + T-Compose compile-time checking | `fromconfig/compiler.py` |
| Lint tool (16 rules, L001–L025) | Framework-aware lint v3 with L004a/b/c/d | `fromconfig/lint.py` |
| GitHub large-scale lint validation | 2,225 YAML → 881 valid configs → 835 linted, 786 (94.1%) triggered ≥1 ERROR (includes cross-framework false positives; est. true defect rate ~65-70%) | `docs/research/THEORY.md` §7.0 |
| Termination theorem 5.4 | `maxSteps` enforced at runtime | `primitives.py` (Loop) |
| Semantic faithfulness tests | 125/125 + 175 new tests passing | `lambdagent/tests/` |
| **Semantic-preserving transforms** | ✅ 6 algebraic laws as AST rewrite rules | `rewrite.py` (14 tests) |

### Gaps

| Gap | Description | Impact |
|-----|-------------|--------|
| ~~**Semantic-preserving transformations**~~ | ✅ Implemented via `rewrite.py` (Thm 36-41) | ~~Cannot auto-refactor~~ |
| ~~**Static type checking**~~ | ✅ Implemented via `types.py` T-Compose checking | ~~Runtime only~~ |
| **Coq mechanization** | Paper proofs are on paper only | Lower trustworthiness of formal guarantees |

---

## 3. Paper II (Operational Semantics + CEK Machine) — Coverage ~80%

### 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 (Definition 27) | IfK/RouteK/CompK/LoopK/PairLK/PairRK/GuardK/MemK — all continuation frames | ✅ `cek_machine.py` (21 tests) |
| Yield mechanism (§5) | CEK handler integration + `run_async()` | ✅ LLM/Tool calls routed through handler |
| Cost vector `c = (τ, λ, μ)` | CEK per-step CostVector + `cost_summary()` | ✅ Per CEK spec |
| Cost monotonicity (Proposition 23) | `CostMonotonicityViolation` asserts `c' ≥ c` each step | ✅ Runtime invariant enforced |
| Pair confluence (Proposition 30) | `writes(f) ∩ writes(g) = ∅` check + `ctx.fork()` isolation | ✅ `store_analysis.py` (20 tests) |
| 6 algebraic laws (Theorems 36–41) | Identity elimination, route distribution, loop simplification, Guard anti-pattern warning | ✅ `rewrite.py` (14 tests) |

### 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 |
| **Labeled bisimulation** | Section 7.1: probabilistic contextual equivalence | Cannot formally verify two agents are behaviorally equivalent | P2 |
| **Explicit evaluation contexts (Def. 17)** | 7 context forms for call-by-value | Implicit in CEK continuations; not a standalone data structure | P2 |
| ~~**CEK Machine as primary executor**~~ | ~~Section 5~~ | ✅ IfK/RouteK + handler + async | ~~P1~~ |
| ~~**6 algebraic laws**~~ | ~~Theorems 36–41~~ | ✅ AST rewrite rules | ~~P1~~ |
| ~~**Pair confluence**~~ | ~~Proposition 30~~ | ✅ writes() analysis + ctx.fork() | ~~P0~~ |
| ~~**Cost monotonicity**~~ | ~~Proposition 23~~ | ✅ CostMonotonicityViolation | ~~P1~~ |

---

## 4. Paper III (Type & Effect System) — Coverage ~70%

### Implemented

| Theoretical Contribution | Implementation | Status |
|--------------------------|----------------|--------|
| T-Compose rule `B <: B'` | `>>` operator checks `output(f) <: input(g)` at construction time | ✅ `types.py` — `check_compose_types()` (44 tests) |
| Json(S) types (Definition 2) | LamType + T_JSON(schema) reusing JSON Schema | ✅ `types.py` — `T_JSON()`, `parse_type_annotation()` |
| Subtype relation `<:` (Definition 5) | Width/depth subtyping + numeric hierarchy + union/tuple types | ✅ `types.py` — `is_subtype()` |
| 15 type rules (§3.3) | T-Compose implemented; Pair→tuple type; others via `input_type`/`output_type` properties | ✅ Core rules covered (T-Compose, T-Pair, T-Sub) |
| Effect algebra `(ε, ·, pure)` (Def. 6-7) | pure/llm(m)/io/state(s) + serial(·)/parallel(∥)/iterate(εⁿ) | ✅ `effects.py` (35 tests) |
| Effect subtype lattice (Definition 9) | `pure ≤ state ≤ io ≤ llm` + `effect_leq()` + `max_effect()` | ✅ `effects.py` |
| Effect inference (§4) | `infer_effect_for_term()` covers all 11 constructs | ✅ `effects.py` |
| Algebraic effect handlers (§6) | ProductionHandler / TestHandler / TraceHandler + `with_handler()` | ✅ `handlers.py` (23 tests) |
| Handler type preservation | Type annotations unchanged across handler switches | ✅ Test-verified |
| Graded types `(p, t, l, m)` (Def. 11-12) | `CostGrade` + `estimate_cost()` + 4 composition rules | ✅ `cost_grade.py` (18 tests) |

### Gaps

| Gap | Theoretical Basis | Impact | Priority |
|-----|-------------------|--------|----------|
| **Refinement types `{x:τ\|P(x)}`** | T-Guard output type encodes postcondition | Guard postconditions not propagated through type system | P2 |
| **Complete 15 rules individually** | T-Lam, T-App, T-If, T-Route, T-Loop, T-Guard, T-Memory, T-Val, T-Var | Some rules (T-If, T-Route etc.) have framework support but no enforced type checking | P2 |
| ~~**T-Compose rule**~~ | ~~Core rule~~ | ✅ `types.py` is_subtype + check_compose_types | ~~P0~~ |
| ~~**Json(S) types**~~ | ~~Definition 2~~ | ✅ T_JSON(schema) structural subtyping | ~~P0~~ |
| ~~**Subtype relation**~~ | ~~Definition 5~~ | ✅ is_subtype() width/depth/numeric | ~~P0~~ |
| ~~**Effect algebra**~~ | ~~Definition 6-7~~ | ✅ effects.py serial/parallel/iterate | ~~P0~~ |
| ~~**Algebraic effect handlers**~~ | ~~§6~~ | ✅ handlers.py three handlers | ~~P0~~ |
| ~~**Graded types**~~ | ~~Definition 11-12~~ | ✅ cost_grade.py static cost prediction | ~~P1~~ |
| ~~**Effect subtype lattice**~~ | ~~Definition 9~~ | ✅ effect_leq() + max_effect() | ~~P1~~ |
| ~~**Handler type preservation**~~ | ~~Theorem~~ | ✅ Test-verified handler switch preserves types | ~~P1~~ |

---

## 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)

- [x] **Implement T-Compose type checking** (Paper III §3.3.3) ✅ `lambdagent/types.py` — 44 tests
  - 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

- [x] **Implement effect annotations** (Paper III §4) ✅ `lambdagent/effects.py` — 35 tests
  - 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

- [x] **Enforce Pair store-independence** (Paper II Proposition 30) ✅ `lambdagent/store_analysis.py` — 20 tests
  - 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`)

- [x] **Implement algebraic effect handlers** (Paper III §6) ✅ `lambdagent/handlers.py` — 23 tests
  - 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)

- [x] **Promote CEK Machine to primary executor** (Paper II §5) ✅ `lambdagent/cek_machine.py` — 21 tests
  - 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)

- [x] **Implement graded cost prediction** (Paper III §4.3) ✅ `lambdagent/cost_grade.py` — 18 tests
  - 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`

- [x] **Implement algebraic laws as rewrite rules** (Paper II Theorems 36–41) ✅ `lambdagent/rewrite.py` — 14 tests
  - 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)

- [x] **Precise cost vector accumulation** (Paper II Definition 5) ✅ integrated in `cek_machine.py` cost_summary() + CostMonotonicityViolation
  - 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.
