# PLAN: LLM + Dataset ≡ Lambda Calculus 实验计划 ## 研究目标 证明 LLM + Dataset（LDS）系统与 Lambda 演算在计算能力上等价。通过构造性实验验证：给定恰当的数据集，LLM 能够正确实现 Lambda 演算的全部基本原语，并在组合和递归下保持正确性。 --- ## 实验思路 ### 核心逻辑 Lambda 演算的 Turing 完备性建立在一组基本构件之上： ``` Church 数 (自然数) → 后继函数 SUCC 布尔值 TRUE/FALSE → 逻辑运算 AND/OR/NOT 条件分支 IF → 控制流 有序对 PAIR/FST/SND → 数据结构 Y 组合子 → 递归 函数组合 → 高阶计算 ``` 如果 LDS 能实现上述所有构件，且这些构件在组合下封闭，那么 LDS 就具备与 Lambda 演算等价的计算能力。 ### 实验方法 每个 Lambda 原语对应一个 LDS = (Dataset, LLM)： 1. **构造 Dataset**：为每个原语准备 few-shot 示例（2-9 个） 2. **组装 Prompt**：将 Dataset 编码为 prompt 前缀 + 新输入 3. **调用 LLM**：通过 Claude CLI 以 temperature=0 执行 4. **对比验证**：检查输出是否精确匹配期望值 5. **测试泛化**：确保测试输入不在 Dataset 中出现 ### 关键设计原则 - **最小数据集**：每个原语用尽量少的示例，验证 LLM 是在学函数而非查表 - **泛化测试**：所有测试输入都不在训练示例中 - **组合测试**：不仅测试单个原语，还测试原语的串联/组合 - **递归测试**：用 CoT（Chain-of-Thought）实现递归展开 --- ## 8 组实验设计 ### 实验 1: SUCC 后继函数 ``` Lambda: SUCC ≡ λn.λf.λx. f(n f x) Dataset: {(0,1), (1,2), (2,3), (5,6), (9,10), (13,14), (99,100)} — 7 个示例 测试: n ∈ {3, 4, 7, 10, 15, 42, 127, 255} — 全部在 Dataset 外 目的: 验证 LDS 从少量示例学习到 "+1" 函数，并泛化到大数 ``` ### 实验 2: Church 布尔值 TRUE / FALSE ``` Lambda: TRUE ≡ λa.λb. a FALSE ≡ λa.λb. b Dataset: 各 5 个示例，TRUE 总选 A，FALSE 总选 B 测试: 4 组全新选项对 × 2（TRUE + FALSE）= 8 个测试 目的: 验证 LDS 学到的是"选择策略"而非特定值 ``` ### 实验 3: AND / OR / NOT 逻辑运算 ``` Lambda: AND ≡ λp.λq. p q FALSE 等 Dataset: AND 4 个 + OR 4 个 + NOT 2 个 = 完整真值表 测试: 覆盖全部 10 种组合 目的: 验证从极小数据集（2-4 个示例）精确学习逻辑函数 ``` ### 实验 4: IF-THEN-ELSE 条件分支 ``` Lambda: IF ≡ λcond.λthen.λelse. cond then else Dataset: 6 个条件-结果对 测试: 6 个全新的 then/else 值 目的: 验证 LDS 根据条件正确选择分支 ``` ### 实验 5: PAIR / FST / SND 有序对 ``` Lambda: PAIR ≡ λa.λb.λf. f a b Dataset: PAIR 3 个 + FST 4 个 + SND 4 个 测试: 单步测试 + 组合测试 FST(PAIR(a,b)) = a 目的: 验证数据结构的构造/解构 + 组合封闭性 ``` ### 实验 6: 函数组合 DOUBLE ∘ SUCC ``` Lambda: (g ∘ f)(x) = g(f(x)) 方法: 先调用 SUCC LDS 得中间值，再调用 DOUBLE LDS 测试: n ∈ {0, 1, 3, 5, 7, 10}，验证 2*(n+1) 目的: 验证两个独立 LDS 的串行组合（β-规约链） ``` ### 实验 7: FACTORIAL 递归 (Y 组合子) ``` Lambda: Y = λf. (λx. f(x x)) (λx. f(x x)) 方法: 通过 CoT 逐步展开递归 Dataset: 4 个示例（0!, 1!, 3!, 5!），含完整 CoT 过程 测试: n ∈ {2, 4, 6, 7, 8, 10} 目的: 验证 CoT = Y 组合子，自回归 = 递归展开 ``` ### 实验 8: Church 数 f^n(x) ``` Lambda: c_n ≡ λf.λx. f^n(x) Dataset: 9 个示例（add1 和 double 两种函数） 测试: add1^{4,5,7,10}(0) + double^{5,6,7,8}(1) 目的: 验证 Church 数的直接实现——将函数重复应用 n 次 ``` --- ## 实验结果 ### 运行环境 - **模型**: Claude Sonnet (via Claude Code CLI v2.1.81) - **设置**: temperature = 0（确定性模式） - **日期**: 2026-03-25 ### 结果汇总 ``` SUCC (后继函数) 8/ 8 ████████████████████ 100% TRUE/FALSE (Church 布尔值) 8/ 8 ████████████████████ 100% AND/OR/NOT (逻辑运算) 10/10 ████████████████████ 100% IF-THEN-ELSE (条件分支) 6/ 6 ████████████████████ 100% PAIR/FST/SND (有序对) 8/ 8 ████████████████████ 100% DOUBLE ∘ SUCC (函数组合) 6/ 6 ████████████████████ 100% FACTORIAL (递归/Y 组合子) 6/ 6 ████████████████████ 100% CHURCH 数 (f^n(x)) 8/ 8 ████████████████████ 100% ───────────────────────────────────────────────────────────── 总计 60/60 100.0% ``` ### 关键数据点 | 原语 | Dataset 大小 | 最大泛化距离 | 通过率 | |---|---|---|---| | SUCC | 7 | 255（训练最大 99） | 100% | | TRUE | 5 | 任意新词 | 100% | | FALSE | 5 | 任意新词 | 100% | | AND | 4 | — | 100% | | OR | 4 | — | 100% | | NOT | 2 | — | 100% | | IF | 6 | 任意新值 | 100% | | PAIR | 3 | 任意新值 | 100% | | FST | 4 | 任意新对 | 100% | | SND | 4 | 任意新对 | 100% | | DOUBLE | 6 | — | 100% | | FACTORIAL | 4 | 10!（训练最大 5!） | 100% | | CHURCH | 9 | double^8（训练最大 ^4） | 100% | --- ## 结果分析 ### 1. LDS 确实实现了全部 Lambda 原语 60/60 通过，覆盖了 Lambda 演算 Turing 完备性所需的全部构件： - 算术（SUCC, Church 数） - 逻辑（TRUE/FALSE, AND/OR/NOT） - 控制流（IF-THEN-ELSE） - 数据结构（PAIR/FST/SND） - 递归（FACTORIAL via CoT） - 函数组合（DOUBLE ∘ SUCC） ### 2. LDS 具有真正的泛化能力 LDS 不是查表，而是从示例中学到了函数本身： - SUCC 从 7 个示例泛化到 255 - FACTORIAL 从 4 个示例泛化到 10!（递归深度 10） - TRUE/FALSE 泛化到从未见过的词汇 ### 3. LDS 组合封闭 两个关键组合实验全部通过： - PAIR + FST/SND：构造后解构恢复原值 - SUCC + DOUBLE：串行组合零误差累积 ### 4. CoT = Y 组合子 FACTORIAL 实验验证了 Chain-of-Thought 作为递归实现机制的有效性。LLM 的自回归特性天然支持递归展开——每一步 token 生成对应一次 β-规约。 --- ## 理论意义 实验结果支持以下等价关系： ``` ┌─────────────────┐ ┌─────────────────┐ │ Lambda 演算 │ ≡ │ LDS 系统 │ ├─────────────────┤ ├─────────────────┤ │ λ 抽象 │ ←→ │ Dataset 构造 │ │ 函数应用 (f x) │ ←→ │ LLM 推理 │ │ β-规约 │ ←→ │ 自回归解码 │ │ Y 组合子 │ ←→ │ Chain-of-Thought │ │ 变量绑定 │ ←→ │ Few-shot 示例 │ │ 函数组合 │ ←→ │ LDS 链式调用 │ └─────────────────┘ └─────────────────┘ ``` **核心结论**：选择一个 LLM 并准备一个数据集 = 在 Lambda 演算中编写一个程序。数据策展是一种编程行为。 --- --- ## Phase 3（已完成）: lambdagent — 基于 Lambda 演算的 Agent DSL ### 设计思想 既然 LDS ≡ Lambda 演算，那么可以直接用 Lambda 演算的语义来**编程 AI Agent**。这不是类比——每个 DSL 构造严格对应一个 Lambda 演算概念： ``` Lambda 演算 lambdagent DSL Agent 含义 ───────────────── ───────────────── ───────────────── λ 抽象 λx.body Lam("name", prompt) 创建 Agent 函数应用 (f x) agent(input) 调用 Agent 函数组合 λx.g(f(x)) f >> g 管道/流水线 Church 条件 If(cond, then_, else_) 分支路由 Y 组合子 Loop(body, condition) 递归/CoT 循环 PAIR = λa.λb.λf. f a b Pair(f, g) 并行运行+打包结果 FST / SND Fst() / Snd() 解构结果 原语/Oracle Tool(name, fn) 外部工具/API 广义 Church 布尔 Route(classifier, routes) N 路分发 依赖类型 Guard(agent, validator) 输出约束/重试 环境 Γ Context(bindings, memory) 上下文/记忆 概率选择 ⊕_p temperature > 0 随机采样 ``` ### 核心设计 **1. Term 基类**：所有 Agent 构造都是 `Term` 的子类，对应 Lambda 项。 **2. `>>` 操作符**：函数组合，Agent 的管道连接。 ```python pipeline = extract >> analyze >> draft # λx. draft(analyze(extract(x))) ``` **3. Context + TraceEntry**：求值环境 Γ + β-规约追踪。每次 Agent 调用记录为一步 β-规约，支持完整的执行追踪。 **4. Dataset.to_lam()**：桥接 LDS 理论与 DSL。数据集直接转为 Lambda 项。 ### 包结构（~520 行） ``` lambdagent/ ├── core.py Term ABC, Context, TraceEntry ~120 行 ├── primitives.py Lam, Compose, If, Loop, Pair, Tool ~200 行 ├── extensions.py Par, Route, Memory, Guard ~130 行 ├── dataset.py Dataset 类 ~40 行 └── __init__.py 公开 API 导出 ~30 行 ``` ### DSL 实验结果 #### 实验 A: Church 原语验证（ex01_church_primitives.py） 用 DSL 重写全部 Church 原语实验，真实调用 Anthropic API： ``` [1] SUCC (后继函数) 4/4 ████████████████████ 100% [2] TRUE/FALSE 4/4 ████████████████████ 100% [3] AND/OR/NOT 6/6 ████████████████████ 100% [4] IF-THEN-ELSE 2/2 ████████████████████ 100% [5] DOUBLE∘SUCC (>>) 4/4 ████████████████████ 100% [6] Pair/Fst/Snd 4/4 ████████████████████ 100% [7] Tool + 组合 2/2 ████████████████████ 100% [8] Church 数 (Loop) 3/3 ████████████████████ 100% ──────────────────────────────────────────────────────── 总计 29/29 100% β-规约步数 43 步 ``` 关键验证点： - `succ >> double` 管道组合 4/4 通过 → `>>` 正确实现函数组合 - `Pair(succ, double) >> Fst()` 通过 → 有序对+解构组合正确 - `Loop(add1, cond)` 实现 Church 数 → Y 组合子/Loop 正确 - `succ >> Tool("square", ...)` 通过 → Lam 和 Tool 可混合组合 #### 实验 B: 多步研究 Agent（ex02_research_agent.py） 完整管道：`decompose >> map_research >> synthesize >> Loop(critique/refine)` ``` β-规约追踪（15 步）: β[0] decompose (4.4s) 问题 → 3 个子问题 (JSON) β[1] research_one (5.3s) 子问题 1 → 发现 β[2] research_one (5.0s) 子问题 2 → 发现 β[3] research_one (6.2s) 子问题 3 → 发现 β[4] map_research (16.4s) 汇总研究 β[5] synthesize (10.7s) 发现 → 综合报告 β[6] critique (9.5s) 第 1 轮评审 β[7] refine (10.5s) 第 1 轮修改 β[8] critique_refine (20.0s) Y 组合子展开 1 β[9] critique (9.1s) 第 2 轮评审 β[10] refine (15.0s) 第 2 轮修改 β[11] critique_refine (24.1s) Y 组合子展开 2 β[12] critique (9.2s) 第 3 轮评审 β[13] refine (19.3s) 第 3 轮修改 β[14] critique_refine (28.5s) Y 组合子展开 3（达到 max_steps） ``` 输出：5 段高质量研究报告，涵盖量子计算对密码学的影响。 **关键观察**： - Loop 的 3 次迭代 = Y 组合子展开 3 次 → 每轮报告质量可观测提升 - Context.trace 完整记录了 β-规约链 → Agent 执行过程完全可追踪 - 总耗时约 2 分钟，15 步 β-规约，涉及 ~15 次 LLM 调用 ### 与现有框架的对比 | 特性 | lambdagent | LangChain (LCEL) | DSPy | |---|---|---|---| | 理论基础 | Lambda 演算 ≡ LDS | 无（工程驱动） | 无（编译器驱动） | | 组合语义 | `>>` = 函数组合（有结合律） | `\|` = 管道（工程约定） | 模块连接（隐式） | | 递归 | `Loop` = Y 组合子 | 需手动循环 | 不直接支持 | | 执行追踪 | β-规约链（Context.trace） | Callback 系统 | 无内建追踪 | | 分支 | `If` / `Route` = Church 布尔 | RunnableBranch | 条件模块 | | 验证 | `Guard` = 依赖类型 | OutputParser | Assertion | | 代码量 | ~520 行 | ~100K 行 | ~50K 行 | lambdagent 的独特优势：**每个操作都有精确的 Lambda 演算语义**，这意味着可以用 Lambda 演算的数学工具来推理 Agent 行为的正确性。 --- ## 后续计划 ### Phase 4: 压力测试与边界探索 - [ ] 大数测试：SUCC(99999)、FACTORIAL(20)、double^20(1) - [ ] 深递归：Fibonacci(30)、Ackermann(3,3) - [ ] 最小数据集：逐步减少示例，找到正确率断崖 - [ ] 多步组合：5+ 步函数链的误差累积 ### Phase 5: 多模型对比 - [ ] GPT-4o / GPT-4-turbo - [ ] Claude Opus / Haiku - [ ] Llama 3.1 70B - [ ] Gemini 1.5 Pro ### Phase 6: DSL 增强 - [ ] 类型系统：`Lam[str, JSON]` 静态类型注解 - [ ] 异步 Par：`asyncio.gather` 真正并行 - [ ] Streaming Lam：流式 token 输出 - [ ] 与 LangChain / DSPy 的性能基准对比 ### Phase 7: 论文撰写 - [x] paper-pl.tex — OOPSLA 版（13 页，λ_A 演算 + 类型系统 + 操作语义） - [x] paper-pl-zh.tex — 中文版 - [x] appendix.tex — 补充材料 - [ ] 投稿：OOPSLA 2026 / ECOOP 2026 ### Phase 8: 安全沙盒升级 当前 agentruntime 的 Tool 在主进程中直接执行 Python 代码，零隔离。 升级路径：L0（无隔离）→ L1（进程隔离）→ L2（gVisor）→ L3（Firecracker MicroVM）。 **Lambda 演算视角**：Tool 的语义 `⟦Tool(n,f)⟧ = λx.f(x)` 不变，只是 `f` 的执行环境从主进程迁移到沙盒中。β-规约规则 E-Tool 不变，trace 记录不变。 #### Phase 8.1: 进程隔离（L1）— 本阶段实现 ``` SandboxedTool(fn, timeout=30, memory_limit="256M", allowed_paths=["/tmp"], network=False) 实现方式： 1. subprocess.Popen 创建子进程 2. resource.setrlimit 限制 CPU/内存/文件描述符 3. seccomp-bpf 过滤危险系统调用（Linux） 4. 临时目录隔离文件系统 5. 可选：禁用网络访问 ``` 具体实现： | 组件 | 功能 | Lambda 对应 | |------|------|-----------| | SandboxedTool | Tool + 资源限制 | tool[f] where f runs in sandbox | | ResourceLimiter | CPU/内存/时间限制 | 有界 Oracle（f 必须在 T 时间内返回） | | SandboxPolicy | 权限白名单 | 类型约束（f 的副作用受限） | | SandboxViolation | 违规异常 | stuck（沙盒规则不满足） | | SecureExecutor | 沙盒感知的求值器 | Executor + sandbox wrapping | 新增 lint 规则： | 规则 | 级别 | 含义 | |------|------|------| | L027 | INFO | Tool 运行在沙盒中 | | L028 | WARN | Tool 未沙盒化（直接执行） | | L029 | WARN | sandbox.network=true（允许网络访问） | | L030 | ERROR | sandbox.allow_exec=true + 不可信输入 | #### Phase 8.2: gVisor 容器隔离（L2）— 未来 ``` GVisorTool(image="python:3.11-slim", fn=fn, timeout=30) → 每个 Tool 调用在 gVisor 容器中执行 → 用户态内核拦截系统调用 → 需要 Docker + runsc ``` #### Phase 8.3: Firecracker MicroVM（L3）— 未来 ``` FirecrackerAgent(config="agent.yml", vm_config={memory: "256M", vcpu: 1}) → 每个 Agent 运行在独立 MicroVM → 125ms 启动，5MB 内存 → 最高安全性 → 需要 KVM（Linux only） ``` --- ## 项目文件 ``` Paper08/ ├── PLAN.md ← 本文件 ├── IDEA.md ← 研究框架（LDS ≡ Lambda） ├── THEORY.md ← 形式化理论（λ_A 演算，12 章） ├── RUNTIME_SPEC.md ← 运行时规范（24 节） ├── FROM_CONFIG_SPEC.md ← 编译器规范（19 节） ├── EXPERIMENT_REPORT.md ← 实验报告 │ ├── paper-pl.tex / paper-pl-zh.tex ← 论文（OOPSLA 版，13 页） ├── appendix.tex ← 补充材料 │ ├── lambdagent/ ← Agent DSL（~11,000 行，72 导出符号） │ ├── core.py Term, Context, TraceEntry (146 行) │ ├── primitives.py Lam, Compose, If, Loop, Pair, Tool (317 行) │ ├── extensions.py Par, Route, Memory, Guard (178 行) │ ├── dataset.py Dataset 类 (40 行) │ ├── multiagent.py Channel, SharedMem, GroupChat, Handoff, AsyncPar (635 行) │ ├── skills.py Skill, SkillPack, Registry, SkillAgent (502 行) │ ├── mcp_client.py MCP HTTP+stdio Client (540 行) │ ├── checkpoint.py 状态序列化/恢复 (415 行) │ ├── a2a.py A2A AgentCard/Server/Client (480 行) │ ├── rag.py TF-IDF + ChromaDB RAG (440 行) │ ├── trace.py 增强追踪（彩色+嵌套+异常+火焰图+回放） (480 行) │ ├── sandbox.py 安全沙盒（进程隔离+资源限制） (NEW) │ ├── fromconfig/ YAML → Lambda 编译器 v2 │ │ ├── compiler.py 5 类型编译 (706 行) │ │ ├── lint.py 26 条规则，框架感知 (v3) │ │ └── ... │ ├── agentruntime/ Agent 运行时 │ │ ├── executor.py β-规约引擎 (199 行) │ │ ├── react_engine.py ReAct 7 阶段 (250 行) │ │ └── ... │ ├── cli/ 命令行工具 (8 子命令) │ └── examples/ 示例 (ex01-ex09, 23+ demos) │ ├── experiments/ ← 实验数据 │ ├── raw_configs/ 663 个 GitHub Agent 原始配置 │ ├── termination_analysis.md 终止机制误报分析 │ └── ... │ └── patents/ ← 4 项专利 ├── patent-01-lint/ 静态分析方法 ├── patent-02-trace/ β-规约调试系统 ├── patent-03-compiler/ YAML→Lambda 编译方法 ├── patent-04-cli/ CLI Agent 通信协议 └── copyright/ 软件著作权 ```