可计算形式：任务分解是一个（动态）CSP

上级：recursive-harness

"可能世界 / 坍缩"这幅图景，被形式化并做成可实现的东西之后：它就是一个（动态的）约束满足问题（Constraint Satisfaction Problem，CSP）。之前"拼图 / 数独"式的大白话讲的是直觉；这里给出的是机器。

结构 ⟨X, D, C⟩

变量 X = {x₁,…,xₙ}——每个 xᵢ 是分解过程暴露出来的一个选择点 / 子任务。X 随着你不断分解而增长 → 这是一个动态 CSP（变量随用随加）。
域 D——Dᵢ 是 xᵢ 的候选方法集合，分两种情况：
- 有限：Dᵢ = {m₁,…,m_k}（可枚举）；
- 无限：不枚举——用一个谓词 φᵢ 描述允许的集合（比如"字符串 ∧ 少于 60 字符 ∧ 措辞专业"），或者用一个生成器来采样候选。
约束 C——每个 c ∈ C 是定义在若干变量之上的一个关系，规定哪些方法组合是相容的。关系天生是双向的（固定 xᵢ 会约束 xⱼ，反之亦然）——这就是所谓"相互影响"，不需要额外的机制。

一个可能世界 = 一个满足全部 C 的完整赋值 A: X→values。世界的集合 = 该 CSP 的解集。

"坍缩" = 约束传播（弧一致性 / AC-3）： 当某个约束 c(xᵢ,xⱼ) 使 v∈Dᵢ 在 Dⱼ 中找不到任何相容的支持值，就把 v 删去；如此传播直到不动点。删掉一个值会杀死每一个用到它的世界。

□/◇ 作为（廉价）可计算量——附一条告诫

□P（被强制）≈ 该变量的域已经坍缩成单点（|Dᵢ|=1）；
◇P（仍开放）≈ 域中仍有多于一个值。

O(1) 时间内即可读出这些域。告诫： 这只是传播可见的被强制性——是对真正蕴涵关系的一个可靠但不完全的近似，并非真正的蕴涵。参见 deducible-not-known。

重访： 这条告诫现在是有代价的，不再只是被口头承认。传播可见的 □ 是一个证书——可靠、不完全、廉价——这恰恰就是 relaxation 中证书那根轴；到真正蕴涵之间的缺口，正是 P×C 所预算的东西（deducible-not-known）。而这个读出动作本身是一个 α ≈ 0 的机械门（operationalizing-tolerances），相对地，LLM 猜出来的蕴涵关系则是带有可测 α 的语义门——信任的这两个层级现在都变得清楚了。

收敛——一个可计算的 P×C 停止条件

不是"唯一解"。定义剩余解集的一个扩散度（剩余各域大小之积，或一个按利害加权的直径）。当

\text{spread}(D)\times\text{cost}\le\theta_{P\times C}.

时便停止。留存下来的各个世界之间的残余差异，已经低于利害的门槛（pc-well-founded-recursion）。

算法（一个 CSP 求解器 / 波函数坍缩）

solve(task):
    X, D, C ← decompose(task)          # LLM: emit variables / domains / constraints
    propagate(D, C)                     # AC-3: collapse incompatibles
    while spread(D) * cost > θ_PC:
        x ← argmin_{|D[x]|>1} |D[x]|     # fail-first / MRV: most-constrained var
        for v in candidates(D[x]):       # enumerate; if infinite, LLM samples
            assign x ← v
            propagate(D, C)              # cascading collapse
            if some domain emptied:      # dead end
                backtrack
            else if v exposes a sub-task:
                X,D,C ← (X,D,C) ∪ decompose(sub-task)   # recursion deepens
    return readoff(D)

标准配方：回溯搜索 + AC-3 传播 + fail-first 排序 + 用 P×C 作为终止 / 深度界限 + 分解不断加深的递归。 会终止：P×C 单调递减（良基），且传播在同一分支内只会删值（单调不返）。

LLM 恰好在三个接口处介入

接口	LLM 做什么	是否机械
`decompose(task)`	产出 `X, D, C`（有哪些子任务、方法、相容性约束）	隐性（靠的是品味 / 常识）
`candidates(Dᵢ)`	从一个无限域中采样若干候选	隐性
评估 `c(vᵢ,vⱼ)`	判断"这两个方法相容吗？"	机械型约束 → 交给代码（传播可靠）；语义型约束 → 交给 LLM（会出错）

其余的一切——传播、搜索、回溯、终止判定、读出 □/◇——都是纯计算。可写化 / 隐性之间的那条接缝（tacit-spec-as-spec-compression）恰好落在一个约束的评估是机械的、还是由 LLM 判断的这一点上。