01 · 交互网最小完备读本

目的：给实现者一份"够用且准确"的理论基线；给 Netbook 一份可直接改成讲稿的提纲。 不是论文综述；完整文献见 09-bibliography.md。

1.1 从字符串重写到图重写

传统计算模型（图灵机、λ 演算）默认"计算是全局的"：替换一个变量要遍历整个项，复制要复制整棵子树。

交互网换了一个假设：

• 计算对象是图：Agent（cell）通过端口用线连接。
• 计算步骤是局部重写：只有两个 principal 端口相连的 Agent（活跃对）才能点火。
• 规则只看到这两个 Agent 和它们的辅助端口；图的其他部分完全不受影响。

这带来三个直接后果：

1. 天然并行：不相交的活跃对可以同时点火。
2. 强合流：点火顺序不影响最终结果（若终止）。
3. 复制/擦除是显式的图操作，不是隐式的全局遍历。

1.2 形式定义

一个交互网 N = (C, W, F)：

• C：有限个 cell。每个 cell 有类型 α ∈ Σ、一个 principal port、以及 ar(α) 个 auxiliary ports。
• W：wire 的集合。每条 wire 连接两个端口；每个端口至多接一条 wire。
• F：free ports（未连接的端口），它们构成网的接口（interface）。

记法：

α(x₁, …, xₙ)

表示一个类型为 α 的 cell，principal port 隐式地朝向"外面"，xᵢ 是辅助端口连接的子网/线。

活跃对（active pair）：两个 cell 的 principal port 被一条 wire 直接相连。记作 α ⋈ β。

交互规则（interaction rule）：对每一对（无序）{α, β}，至多一条规则：

α(x₁,…,xₘ) ⋈ β(y₁,…,yₙ)  =>  N'

其中 N' 的 free ports 恰好是 x₁…xₘ, y₁…yₙ。

归约：删除活跃对的两个 cell 及连接它们的 wire，把 N' 插入，并把 N' 的 free ports 与原来的外部线对接。

范式（normal form）：不存在活跃对的网。

交互系统（interaction system）：签名 Σ（每个符号的 arity）+ 规则集。

关键约束：每对 Agent 至多一条规则。这保证了归约是确定的（没有规则冲突），也是强合流的前提。若需要"按状态分支"，要把状态编码进 Agent 类型（见 4.3）。

1.3 归约、合流与范式

Lafont 1989 的核心定理：

强合流（strong confluence）：若 N → N₁ 且 N → N₂（两个不同的活跃对），则存在 N₃ 使得 N₁ →* N₃ 且 N₂ →* N₃。

直观理解：两个活跃对要么不相交（点火互不影响，显然可交换），要么共享一个 cell（此时一个点火后另一个仍在，且结果可交换）。这就是"局部性"带来的菱形性质。

推论：

• 范式唯一（如果存在）：任何两个最大归约序列到达同一个范式。
• 策略无关：归约策略不影响结果，只影响代价/并行度。这与 λ 演算形成鲜明对比（call-by-name vs call-by-value 可能一个终止一个不终止）。
• 不保证终止：δ ⋈ γ 的某些组合可以形成循环；交互网是图灵完备的。

重要区分：

1.4 交互组合子（Interaction Combinators）

Lafont 1997 给出了一个极小的通用系统：

Σ = { ε, δ, γ }
ar(ε) = 0
ar(δ) = ar(γ) = 2

• γ：constructor，把两个资源合成一个（可理解为二元节点/应用）。
• δ：duplicator，把一个资源复制成两份。
• ε：eraser，丢弃一个资源。

规则（精确接线）

以下用 α(a,b) 表示一个二元 cell，a,b 是它的两个辅助端口；ε 没有辅助端口。

1. 同符号湮灭（annihilation）

γ(a,b) ⋈ γ(c,d)   =>   a—c,  b—d
δ(a,b) ⋈ δ(c,d)   =>   a—c,  b—d

两个 cell 消失，辅助端口两两对接。

2. 异符号交换（commutation）

γ(a,b) ⋈ δ(c,d)   =>
    δ(x,y) ⋈ a
    δ(z,w) ⋈ b
    γ(x,z) ⋈ c
    γ(y,w) ⋈ d

即：旧的两个 cell 消失，换成一个"方块"——两个新的 δ、两个新的 γ；每个旧辅助端口接到一个新 cell 的 principal port，新 cell 之间交叉接线。

（这与 HVM2 论文中的 (A B) ~ {C D} → {x y} ~ A, {z w} ~ B, (x z) ~ C, (y w) ~ D 是同一规则，只是端口命名不同。）

3. 擦除（erasure）

ε ⋈ ε            =>   （空）
ε ⋈ γ(a,b)       =>   ε ⋈ a,  ε ⋈ b
ε ⋈ δ(a,b)       =>   ε ⋈ a,  ε ⋈ b

擦除会沿着结构传播：一个 ε 遇到二元 cell，就变成两个 ε 继续擦除其子树。

通用性

Lafont 证明：任何交互系统都可以翻译到交互组合子；交互组合子是图灵完备的，并且保持复杂度类与并行度（在编码意义下）。因此：

• 只要实现 γ/δ/ε 三条规则，就拥有了一个通用计算基质。
• 其他所有 Agent（包括我们的 Agent、Tool、LLM）都是"语法糖/扩展符号"，最终可以编码到组合子，或在运行时作为原生符号获得更好的性能。

一个非终止例子

δ(ε, x) ⋈ γ(x, ε)

经过交换/擦除会回到自身（Wikipedia 上有一个经典例子）。这说明合流不等于终止；运行时必须有 step/time/fuel 限制。

1.5 编码 λ 演算与最优归约

直觉映射

Lamping / 最优归约

Lamping 1989 给出了第一个按 Lévy 意义最优的 λ 归约算法；Gonthier–Abadi–Lévy 1992 用 geometry of interaction 解释了它；Asperti–Guerrini 1998 是系统教材。

关键机制：

• sharing graph：用 fan/duplicator 节点显式表示"同一子项被两处使用"。
• brackets / fans / oracle：控制复制的层级，避免复制不该复制的东西；读回（read-back）时消去。
• 最优性：不重复归约被共享的 redex；某些项可以获得指数级加速（Church numeral、Fibonacci 等）。
• 代价：bookkeeping 有开销；Lawall–Mairson 1996 指出"最优"不等于"对所有项都更快"。工程上要按工作负载选择。

Interaction Calculus（IC）：更可编程的变体

HVM 系列使用的 Interaction Calculus 把 λ 项直接写成带全局变量、仿射变量、superposition/duplication 的项：

Term ::= x | * | λx.t | (t t) | &L{a,b} | !&L{x,y}=t; u

• λx.t：抽象（变量仿射，最多用一次）。
• (t t)：应用。
• &L{a,b}：带标签 L 的 superposition（两个可能值/分支）。
• !&L{x,y}=t; u：duplication，把 t 复制给 x,y。

核心规则（详见 HVM3 IC.md）：

(λx.f a)        =>  x ← a; f                    (APP-LAM)
(&L{a,b} c)     =>  !&L{c0,c1}=c; &L{(a c0),(b c1)}   (APP-SUP)
!&L{r,s}=*; K   =>  r←*, s←*; K                  (DUP-ERA)
!&L{r,s}=λx.f; K => r←λx0.f0, s←λx1.f1, x←&L{x0,x1};
                     !&L{f0,f1}=f; K             (DUP-LAM)
!&L{x,y}=&L{a,b}; K => x←a, y←b; K               (DUP-SUP 同标签)
!&L{x,y}=&R{a,b}; K => 交叉复制                    (DUP-SUP 异标签)

为什么它对实现友好：

• 变量仿射且全局唯一 → 替换就是一次原子写，不需要遍历项、不需要处理变量捕获。
• 复制/叠加是显式构造 → 共享与分支都是一等公民。
• 可以单线程解释，也可以并行归约；HVM2 用 64-bit term + 原子链接做到了每核数亿次交互。

本项目的选择：

• Netbook 的教学主线用 γ/δ/ε（最直观、最少概念）。
• Ainet 的运行时核心采用"带标签二元 cell + 原生构造子/数字 + effect/join cell"的网 IR，语义上覆盖 IC；λ 编码作为前端的一个编译路径，而不是运行时的唯一表示。

1.6 并发语义：redex 图与调度

给定网 N，构造 redex 图：

• 顶点：当前所有活跃对。
• 边：两个活跃对共享至少一个 cell（冲突）。
• 独立集：可以同时点火的活跃对集合。

调度器的工作就是不断选择独立集、点火、更新 redex 图。关键量：

强合流保证：不同调度策略得到同一范式。但代价不同：

• 贪心策略可能制造大量可并行但无用的工作（例如先复制再丢弃）。
• 最优策略需要知道哪些 redex 会被丢弃；这正是 Lamping/Asperti 的 bracket/oracle 要解决的问题。
• 对 Agent 工作负载，还要叠加 effect 的延迟与成本（见 4.8）。

1.7 为什么标准交互网不能直接做并发系统

这是本项目最重要的"反面教材"。Mazza 2006 的博士论文指出：

交互网是完全异步的：组件之间的同步完全是局部的。它没有全局同步机制，因此无法表达冲突、等待、死锁——而这些正是并发系统的核心。

具体缺口：

Mazza 的解决方案是 multiport interaction nets（INMPP）：

• cell 可以有多个 principal port；活跃对可以是多对多。
• 这是标准交互网的保守扩展（标准网是 k=1 的特例）。
• 表达能力等价于 π 演算；可以给出完全局部、异步的 π 编码。
• 可以表达同步、选择、死锁，并研究死锁自由（deadlock freedom）。

本项目的方案（详见 04）：

1. 纯核保持标准二元交互网（合流、可编码、可验证）。
2. 加一组受控的 multiport cell：Join(k)、Select(k)、Gate、Barrier，只用于同步，且有 session 类型约束。
3. 加 Effect cell：把 LLM/工具/人工调用变成显式的请求-响应节点，运行时挂起/恢复。
4. 加 Location：cell 有归属节点；跨节点线变成有序通道；活跃对只在 owner 上点火。
5. 加 Supervisor/Error：失败是图上的显式值，监督是图上的显式 cell。
6. 加 Budget/Cost：每个规则/effect 带成本；调度器在预算约束下优化。

一句话：不要把交互网硬拗成 actor；把 actor 需要的东西做成交互网的显式扩展，并证明纯子集仍然合流。

1.8 类型、线性逻辑与 session

交互网最初就是线性逻辑 proof net 的推广：

proof net 的正确性（Danos–Regnier 判据）保证图确实对应一个证明；在交互网里对应"类型系统/极化系统"，可以排除某些死锁与无意义循环。

对 Agent 基础设施更有用的是 session types：

S ::= end | !T.S | ?T.S | ⊕{lᵢ:Sᵢ} | &{lᵢ:Sᵢ} | rec X.S | X

• !T.S：发送 T，继续 S。
• ?T.S：接收 T，继续 S。
• ⊕：内部选择（发送方选分支）。
• &：外部选择（接收方提供分支）。
• 对偶性：!T.S 的对偶是 ?T.S，⊕ 的对偶是 &。

把 session 类型赋给端口，可以得到：

• 协议安全：不会发错类型、不会在错误时机关闭。
• 死锁自由（对良类型、树形协议）：经典的 progress 定理。
• 因果顺序：即使运行时并行，消息的可观察顺序由类型约束。

Ainet 的类型系统（05）会采用：线性端口 + session 协议 + effect row + 成本标注。完整的形式化与证明放在 specs/，v1 先实现可判定的子集。

1.9 复杂度与代价模型

交互网不是"免费午餐"：

• 交互数是算法层面的工作度量；不同编码可能差指数级。
• 最优归约可能引入大量 bookkeeping；对某些项比 naive 更慢。
• 并行度受关键路径限制；不是交互数少就一定快。
• Agent 场景还要加：LLM token/美元、网络 RTT、工具配额、人工审批延迟。

因此 Ainet 的代价向量至少是：

cost(step) = (interactions, tokens_in, tokens_out, usd, latency_us, energy)

调度目标不是单一"最短时间"，而是在预算/截止时间/公平性约束下的多目标优化（详见 06.4）。

1.10 常见误解

1.11 推荐阅读路径

1. 入门：Lafont, Interaction Nets (POPL 1989)；Gay 的 diploma thesis。
2. 组合子：Lafont, Interaction Combinators (1997)。
3. 最优归约：Lamping 1989；Gonthier–Abadi–Lévy 1992；Asperti–Guerrini 1998（书）。
4. 并发扩展：Mazza 2006 博士论文（第 4–6 章）；Alexiev 1999；Khalil 2003。
5. 工程实现：HVM2 论文（2024）；Inpla 文档；Vine/Ivy/IVM。
6. 类型/session：Honda 1993；Caires–Pfenning 2010；Wadler 2012（session types 教程）。

完整链接见 09-bibliography.md。

在 GitHub 编辑本文