lambdagent/docs/RESEARCH_GAP_ANALYSIS.md

研究差距分析：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 后条件未在类型系统中传播
完整 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 但未验证存储独立性。

所需实现：

# 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
-------	------------------	-------------	-------------
Paper I	λA DSL + Lint	10	9 (incl. new: static types + rewrite rules)
Paper II	Operational Semantics + CEK Machine	12	9 (incl. new: CEK+laws+confluence+cost)
Paper III	Type & Effect System	12	10 (incl. new: types+effects+handlers+graded)

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:

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

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

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