# 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/                      软件著作权
```
