04 · AIN：Agent Interaction Nets 计算模型

轨道 B 的语义核心。目标：在保留交互网纯核（局部性、强合流、线性）的前提下，补上 Agent 需要的状态、同步、效果、位置、失败、成本六件事，并明确哪些性质仍然成立。

4.1 设计压力

把标准交互网直接拿来跑 Agent，会在六个地方断裂：

AIN 的策略：纯核不动，扩展分层。每一层扩展都有独立的语义与类型，不污染纯子集。

┌──────────────────────────────────────────────┐
│  L6  Cost / Budget / Scheduling policy       │
├──────────────────────────────────────────────┤
│  L5  Supervision / Error / Compensation      │
├──────────────────────────────────────────────┤
│  L4  Locations / Remote wires / Migration    │
├──────────────────────────────────────────────┤
│  L3  Effects (LLM / Tool / Human)            │
├──────────────────────────────────────────────┤
│  L2  Synchronization (Join / Select / Gate)  │
├──────────────────────────────────────────────┤
│  L1  Stateful agents (state-indexed cells)   │
├──────────────────────────────────────────────┤
│  L0  Pure interaction nets (γ/δ/ε + constrs) │
└──────────────────────────────────────────────┘

4.2 形式定义

一个 AIN 网是七元组：

N = (C, W, Σ, S, ℓ, F, policy)

• C：有限 cell 集合。
• Σ：agent 签名；每个 α ∈ Σ 有 arity 与端口名。
• S：状态域；每个 cell c 有状态 s(c) ∈ S_{α(c)}。
• W：wire 集合；每条 wire 连接两个端口；每个端口至多一条。
• ℓ : C → Loc：位置（节点 id）。
• F：free ports（接口）。
• policy：调度策略/预算/优先级标注（可继承）。

cell：

c = (α, s, p₀, p₁…pₙ)

• p₀：principal port（v1 的用户 agent 恰好一个）。
• p₁…pₙ：auxiliary ports，带名字与类型。
• 对 multiport cell（L2），P(c) 是 principal port 的有序集合。

活跃对：一条 wire 连接两个 principal port。对 multiport，活跃"配置"是一组 wire，连接规则模式中所有 principal port。

规则：

rule α[s](x₁…xₘ) ⋈ β[t](y₁…yₙ) => N'

• s,t 是状态模式（可绑定变量）。
• 对每对 (α,β)，至多一条规则；状态由编译器展开为互斥的 agent 类型（见 4.3），因此不违反"每对至多一条"。
• N' 的 free ports 恰好是 x₁…xₘ, y₁…yₙ。

归约：删除活跃对，插入 N'，按端口名对接外部线。

范式：无活跃对（可能仍有 effect pending / remote message in flight；见 4.9 的 quiescence）。

4.3 L1：状态——把状态编码进类型

问题：标准 IN 的规则只按 agent 类型匹配；Agent 需要"同一角色、不同阶段"。

方案：state-indexed agents。

agent Planner<S> {
  ports { inbox: ?Task; llm: !LLM; out: !Plan }
  state Idle | Thinking { draft: Text } | Done { plan: Plan }
}

编译后展开为：

Planner_Idle, Planner_Thinking, Planner_Done

每个状态是一个不同的 agent 符号；规则表按 (Planner_Idle, Task)、(Planner_Thinking, LLMResult) 等生成。这样：

• 规则仍然"每对至多一条"。
• 纯核的强合流保持。
• 状态转移就是 cell 类型的改变（旧 cell 被规则替换为新 cell）。

对于运行时内部 cell（Effect、Supervisor、Remote），允许可变状态（Pending(job) 等），因为它们不在纯子集里；它们的语义由运行时协议定义，不参与纯合流定理。

4.4 L2：同步——受控的 multiport

标准 IN 无法表达"等两个输入都到齐"。Mazza 的 multiport IN 允许一个 cell 有多个 principal port；活跃对是多对多。我们只引入三种受控形式：

Join(k)

Join(k) : (T₁, …, Tₖ) → T

• k 个 principal port；每个连接到一条消息 wire。
• 当 k 个消息都到达时点火一次，消费全部，产生一个 tuple/结果。
• 类型：⊗ᵏ T → T。
• 用途：fan-in、map-reduce 的 reduce 阶段、barrier。

Select(k)

Select(k) : (T₁, …, Tₖ) → T ⊕ Cancelled

• k 个 principal port；第一个到达的消息获胜，其余被取消。
• 需要取消协议：每个未获胜的输入收到 Cancel；上游必须支持取消（Effect/Agent 的 cancel 端口）。
• 类型：⊕ᵏ T → T（内部选择的外部化）。
• 用途：race、超时、投机执行、多模型投票（第一个成功）。

Gate / Barrier(k)

• Barrier(k)：收齐 k 个信号后，向 k 个输出各发一个信号（广播释放）。
• Gate：一个开关 cell，只有 open 时消息通过；用于人工审批、限流。

类型与死锁

• Join/Select 的端口类型必须满足 session 对偶；例如 Join 的输入是 ?T，上游是 !T。
• 对树形协议（无循环等待），well-typed 网满足 progress（不会卡死）。
• 环形协议需要显式顺序（给 cell 一个全局 rank，或使用 session 的 rec 加 guard），v1 先用静态检查拒绝潜在环。
• 这部分的形式化在 specs/ain-sync.md；实现先用保守检查 + 运行时超时兜底。

为什么不用完整 multiport IN？完整版表达力等价于 π 演算，但规则匹配/调度/类型都复杂得多。v1 只需要同步原语；保留未来升级到完整 multiport 的接口。

4.5 L3：Effects——把副作用变成显式节点

Effect cell：

Effect<Op> {
  principal req : ?Request<Op>
  auxiliary res : !Response<Op>
  auxiliary cancel : ?Cancel
  state Idle | Pending(JobId) | Cancelled
}

生命周期：

1. Idle 收到 Request → 创建 job j，cell 变 Pending(j)。
2. 运行时异步执行 Op（LLM/HTTP/tool/human）。
3. 完成 → 在 res 上注入 Result(v)；cell 回 Idle（可复用）或 Done（一次性）。
4. 失败 → 注入 Error(e)；按策略重试。
5. Cancel → 运行时取消（若支持），注入 Cancelled。

Effect 描述：

effect llm(model: Text, prompt: Text, max_tokens: Nat) -> Completion
effect http(method: Method, url: Url, body: Bytes) -> Response
effect tool(name: Text, args: Json) -> Json
effect human(form: Form) -> Decision

语义：带标签的迁移

N --(eff req j)--> N'          (cell → Pending)
N --(eff done j v)--> N''      (result injected)

Effect log：

{ job_id, op, input_hash, model, params, output_hash, output,
  started_at, ended_at, cost, idempotency_key, retries, node }

• 重放时，Effect 不重新执行；直接按 job_id 从 log 注入结果。
• job_id 由 (net prefix hash, cell id, request hash, attempt) 决定；同一输入重放稳定。
• 对非确定性输出（LLM 温度、工具外部状态），log 是唯一事实来源。
• 隐私：log 可配置只存 hash + 加密的 output；或存引用（对象存储）。

流式：Response 可以是 Stream<Chunk> cell；每个 chunk 是一条消息，Agent 可以增量处理；背压由通道窗口控制。

幂等：外部工具调用带 idempotency_key；运行时维护去重表；重试不重复扣费（对支持幂等的 API）。

4.6 L4：分布——cell 归属 + 远程通道

不变量：

每个 cell 在任意时刻恰好属于一个节点；只有 owner 能点火的规则的 LHS 中包含该 cell 的活跃对。

跨节点线：不共享内存；编译为 Remote 通道：

Cell A (node 1) ── wire ── Cell B (node 2)
        │                        │
   SendProxy ── QUIC/gRPC ── RecvProxy

• 每个方向一个有序通道；消息带 (net_id, wire_id, seq, payload)。
• 接收端把消息注入为本地 Message cell，形成本地活跃对。
• 因此跨节点没有分布式锁：所有点火都是本地的；远程只是消息传递。

迁移（v1 可选，v2 必需）：

• 触发：负载不均、数据驻留、节点下线。
• 过程：暂停 owner（lease）→ 序列化 cell + 邻接 proxy → 目标节点恢复 → 更新路由 → 释放 lease。
• 安全：epoch/fencing token 防止双 owner。
• 代价：迁移成本计入调度器；小 cell 优先。

放置：

• 初始：按 agent 声明/租户/数据位置。
• 动态：基于通信图（谁和谁交互多）做图分区；目标是最小化跨节点 wire。
• v1 先用静态放置 + 一致性哈希；v2 做在线迁移。

故障：

• 节点失联 → owner 的 cell 丢失；supervisor 从检查点/重放恢复。
• 远程消息至少一次；接收端按 (wire_id, seq) 去重。
• 网络分区：v1 选择 CP（停止少数派写入）或 AP（可用但可能重复）需按场景配置；默认 CP + 明确错误。

4.7 L5：失败与监督

Error cell：

Error<E> { principal port; payload: E }

• 规则可以产生 Error 而不是正常结果。
• Try cell：连接一个计算和一个 handler；捕获 Error 并转换为正常值。
• Timeout cell：包装一个 Effect/子网，超时注入 Error<Timeout>。

Supervisor cell：

Supervisor {
  children: [ChildSpec]
  policy: RestartOne | RestartAll | Stop | Escalate
  max_restarts: Nat
  window: Duration
}

• 子 Agent 的 Exit(Ok|Error) 消息连到 supervisor 的 principal port。
• 按策略重启：重新实例化子网（复制 ChildSpec），保留/重置状态。
• 重启计数超限 → 升级到父 supervisor 或终止。
• 这是 Erlang/OTP 的语义，但在图上显式化：supervision tree 就是一张网。

补偿：

• Compensate cell：记录已完成的副作用，失败时按逆序调用补偿 effect。
• 对 LLM/工具，补偿通常是"发消息/回滚外部状态"，不是事务。

重试：

• Effect 级：max_attempts, backoff, jitter, retry_on。
• 规则级：不自动重试（纯规则不应失败）；失败只来自 effect/supervisor。
• 幂等键保证重试安全。

4.8 L6：成本与预算

成本向量：

cost(step) = (
  interactions,     // 纯计算
  input_tokens,     // LLM
  output_tokens,
  usd,              // 外部计费
  latency_us,
  energy_j         // 可选
)

每个规则模板声明静态成本；每个 effect 声明动态成本（按模型/工具定价表）。

Budget cell：

Budget {
  principal spend : ?Spend
  auxiliary status : !Status
  remaining: { tokens, usd, wall_time }
}

• Agent 在发起 effect 前先 spend；不足则收到 Denied，必须走降级路径（更小模型/缓存/人工）。
• 预算可嵌套：父预算 → 子 Agent 子预算；超额向上传播。
• 账本：每个 step/effect 记 (agent_id, task_id, tenant, cost)；可导出。

调度目标：

minimize  makespan
subject to  Σ cost ≤ budget
            deadline_i ≤ d_i
            fairness(tenant)

• v1：EDF（deadline）+ WFQ（fairness）+ 预算准入；关键路径优先。
• v2：基于通信图/成本的启发式放置；可选 RL/学习型策略（保持可解释）。

4.9 操作语义（小步）

(STEP)      N ≡ N₀[a ⋈ b]   rule(a,b) = N'   N₀[N'] ≡ N₁
            -------------------------------------------------
            N → N₁

(EFF-REQ)   c = Effect<Op> at Idle, msg = Request(op, input)
            -------------------------------------------------
            N → N[c ↦ Pending(j)]   with j = job(op,input)

(EFF-DONE)  job j completes with v
            -------------------------------------------------
            N → N[inject Result(v) at c.res; c ↦ Idle]

(EFF-FAIL)  job j fails with e
            -------------------------------------------------
            N → N[inject Error(e) at c.res; c ↦ Idle]

(REMOTE)    wire w = (a@n₁, b@n₂)
            -------------------------------------------------
            N → N[send(w, msg) to n₂]

(RECV)      message (w, seq, payload) arrives at n₂
            -------------------------------------------------
            N → N[inject Message(payload) at b]

(MIGRATE)   lease(c) acquired; state(c) serialized
            -------------------------------------------------
            N → N[c @ n₂]

可观察性：trace 是标签序列；纯 step 的标签是 (redex, rule)；effect 是 (job, req/done)；remote 是 (wire, seq)。

静止（quiescence）：没有活跃对、没有 pending effect、没有 in-flight remote message。正常终止 = quiescent + 所有接口已消费/关闭。

4.10 类型系统（概要）

Types     T ::= Unit | Bool | Nat | Text | Bytes | Json | Data | Port | Agent
PortType  P ::= !T.S | ?T.S | !T | ?T
Session   S ::= end | !T.S | ?T.S | ⊕{lᵢ:Sᵢ} | &{lᵢ:Sᵢ} | rec X.S | X
EffectRow E ::= ∅ | {op} ∪ E
AgentType A ::= Agent<α, S, P₁…Pₙ, E>

判断：

Γ ⊢ net : Δ          (线性：Γ/Δ 中每个端口恰好一次)
Γ ⊢ rule : (α,β) → E (规则引入的 effect 行)

规则：

• 线性：wire 的两端各消费一个端口；free port 不能重复出现。
• session 对偶：!T.S 只能接 ?T.S；⊕ 只能接 &。
• effect 子行：规则/agent 声明的 effect 必须被运行时 handler 覆盖；未声明的 effect 是类型错误。
• 预算：@budget(n) 标注；类型检查只保证"声明了预算"，运行时保证"不超支"。
• 状态：Agent<S> 的 S 必须是有限 ADT；编译器展开。
• multiport：Join(k) 要求 k 个输入类型可组合；Select(k) 要求输出类型一致 + 可取消。

v1 实现子集：

• 单态 + 简单泛型（List<T>, Result<T,E>）。
• session 只支持 !/?/end + 递归（无 &/⊕ 的完整子类型）。
• effect row 显式声明，不做推断（后续加）。
• 线性检查是保守的：拒绝可能需要别名分析的网。

4.11 Agent 模式 → 网构造

一个 3 Agent 流水线的网

Question ──▶ Researcher ──draft──▶ Critic ──verdict──▶ Writer ──▶ Report
                  │                    │                  │
                  └──── LLM cap ───────┴──── LLM cap ────┘

• Researcher 的 out 连到 Critic 的 in；Critic 的 out 连到 Writer 的 in。
• 三个 agent 各自有一个 LLM capability 端口；能力由宿主注入，不能凭空访问网络。
• 如果 Critic 失败，Supervisor 重启它；Researcher 的 draft 可以缓存复用（结构化共享）。
• Budget 挂在流水线入口，按 token/$ 分配。

4.12 与其他模型的关系

4.13 开放理论问题

1. Effectful 合流：在 effect 交错下，最终网是否只依赖于 effect log？需要定义"可交换的 effect"与"因果序"。
2. Multiport 死锁自由：树形协议已有经典结果；带环/递归的 session 在 AIN 上的判定条件？
3. 分布精化：远程通道的异步语义与集中式语义的 bisimulation 需要哪些假设（FIFO、可靠、无分区）？
4. 成本最优调度：在 DAG/图上的 EDF+WFQ 近似比；预算约束下的在线算法。
5. 线性与共享的边界：Agent 需要共享上下文，但线性端口不允许别名；用 Sup/显式 dup 还是 Ref？哪种对 LLM 工作负载更自然？
6. 读回/可解释性：如何把一张巨大的 Agent 网折叠成人类可读的"为什么"（类似 IC 的 collapse）？

这些问题不阻塞 v1；v1 用保守子集 + 运行时检查 + 属性测试，论文/形式化随后补。

在 GitHub 编辑本文