RFC-027a: 终止检查的显式测度

摘要

RFC-027 §7 把终止检查的判据定为精化类型（精化即进验证模式），§6.9 给出显式测度的语言形态（内置谓词 Terminates，与 Int、Never 同属核心原语）。两件都是语言设计，属于宿主 RFC，已定稿。

本子 RFC 承接落地机制：义务如何从计算结构生成、判定管线如何编排、诊断如何在推不出时给出方向、互递归的测度如何共享（SCC 优化）、错误码如何注册。不再重复语言语义，只定机制。

动机

为什么需要子 RFC

判据（精化类型进验证模式）与形态（Terminates 写在类型位）已在 RFC-027 定案，粒度为语言级。余下的问题粒度过细，写进宿主会把正文撑散：

义务从哪来（递归调用点、循环回边、路径守卫）
测度返回元组时如何比较（字典序展开）
良基性与严格递减是两条独立义务还是合一
自动探索与显式测度如何共存于同一条管线
互递归时同一测度如何避免重复书写与重复验证
推不出时如何给出方向而不是直接拒绝

触发

方向由 #318 触发：非结构递归（gcd 类非直接递减、相互递归、归并分区）超出测度探索的模板序列（RFC-027 §6.2–6.5 四策略均以「有界类型的变量」或「目标类型 + 交换操作」为输入），且无法在不破坏可读性的前提下改写为可分析的迭代模式。RFC-027「开放问题」节的再讨论条款在此激活。

提案

与自动探索的关系

显式测度不是另一条管线，而是探索失败后的输入。给出测度后仍走同一台 SMT 验证同一组义务；不成立则报错并附反例。全自动优先不变：探索永远先跑，用户介入只发生在探索失败之后。

这决定了两条路径共享全部下游机制——义务生成、SMT 判定、字典序展开、诊断格式都只有一份实现。

义务生成

对函数 f 与测度 m，生成两条独立义务，逐递归调用点（含 SCC 内跨函数调用）展开：

良基性：m(args) >= 0——测度落在自然数上；测度返回非自然数类型时，取该类型上适定序的下界。从参数精化推导，推不出时进入残余义务。
严格递减：每个调用点 m(callee_args) < m(caller_args)，在路径守卫下判定——守卫来自该调用点所在的分支条件，复用 RFC-009a 路径条件收集。

两条独立而非合一，理由是失败方向不同：良基性失败说明测度取值域不对（如 Int 可能为负），递减失败说明递归参数没朝该方向走。诊断需要区分，才能给出正确的检查方向（见「诊断」节）。

循环同理，把「调用点」换成「回边」：循环体的每条执行路径上 m(下一轮状态) < m(本轮状态)，守卫来自循环条件与体内分支。

字典序展开：m 返回元组 (m₁, …, mₖ) 时，义务按字典序比较展开为析取链——(m₁' < m₁) ∨ (m₁' == m₁ ∧ m₂' < m₂) ∨ …。展开在义务生成侧完成，SMT 侧保持线性片段，不依赖求解器对字典序的原生支持。

测度自身必须可编译期求值：m 必须是常量折叠或结构递归可证的函数——禁止把终止问题递归推给另一个未证函数（防无穷回归）。病态测度由既有 E4012（常量递归过深）与结构检查拦住。

判定管线

1. 形参递减（结构递归，最强路径，先试）
2. 测度探索：四策略模板序列（RFC-027 §6.2–6.5），找到一个即停止
3. 探索成功 → 生成义务 → SMT 判定 → Proved
4. 探索失败 → 检查类型位是否给出显式测度（Terminates）
     有 → 取该测度生成义务 → SMT 判定
     无 → E4021（终止无法证明，附建议的检查方向）
5. 义务被 SMT 判伪 → E4022（测度不成立，附反例）

1–3 级是 RFC-027 既定路径，本 RFC 新增第 4 级与两条错误码。整条管线只在精化类型触发时运行（RFC-027 §7）——无精化的普通类型不生成任何义务。

锚点：一元与二元形态

RFC-027 §6.9 定了两个元数，本 RFC 说明各自的落点：

形态	锚点	落点
`Terminates(m)`	所在绑定的名字	定义处默认形态——自递归函数、循环
`Terminates(FnType, m)`	显式函数类型	需要显式指明测度归属于哪个函数类型时（测度定义在别处、同一测度服务多个计算）

两者不是两种构造，是同一谓词的两个元数：终止义务总是落在「精化所在的类型位所标注的那段计算」上。互递归不必用二元形态——两个函数各写各的一元形态即可，共享关系由 SCC 识别（见下节）。

SCC：测度共享优化

互递归的一组函数（调用图上的强连通分量）若共享同一测度，跨函数边的义务为 m_callee(callee_args) < m_caller(caller_args)，成员共享测度时退化为同测度递减。

这是优化，不是正确性前置：不共享时各函数各写测度、各自闭环即可通过。SCC 的价值是认出「这一组用的是同一个测度」，免去重复书写与重复验证。

需要新建函数级调用图与 SCC 收集——现有 TypeDepGraph 记录的是变量间类型标注依赖（RFC-027 §6.1 的 VC 触发器），是变量级图，不可复用。

示例

gcd：非结构递归

yaoxiang

// 测度：普通函数，可单测、可复用
gcd_measure: (a: Int, b: Int) -> Int = { b }

gcd: Terminates((a: Int, b: Int) -> Int, gcd_measure) = {
    if b == 0 { return a }
    return gcd(b, a % b)
}

义务生成：

良基性：gcd_measure(a, b) >= 0 即 b >= 0——从形参精化 NonNegative(b) 直接导出
严格递减：唯一递归调用点 gcd(b, a % b)，路径守卫 b != 0，义务 gcd_measure(b, a % b) < gcd_measure(a, b)；代入测度体展开为 a % b < b
SMT：验证否定 b != 0 ∧ a % b >= b 不可满足 → Proved

循环：匿名构造获得指称

yaoxiang

loop: (n: Int) -> Int = {
    mut i = 0
    acc: Terminates(n - i) = while i < n {
        i = i + 1
    }
    return acc
}

Terminates(m) 精化的就是循环体尾表达式的值类型，锚点由绑定名 acc 提供——循环因此可被指称，不再有「匿名构造无从指称」的死角。这也解释了两个元数的统一性：义务总是落在精化所在的类型位所标注的那段计算上，函数与循环没有区别。

义务：回边上 (n - i') < (n - i)，守卫 i < n，i' = i + 1 代入得 1 > 0，恒真 → Proved。

互递归：SCC 共享测度

yaoxiang

nat: (n: Int) -> Int = { n }

is_even: Terminates(nat) = {
    if n == 0 { return true }
    return is_odd(n - 1)
}
is_odd: Terminates(nat) = {
    if n == 0 { return false }
    return is_even(n - 1)
}

两个函数各带一元形态的 Terminates(nat)。SCC 收集后识别出二者共享同一测度，跨函数边义务 nat(n - 1) < nat(n) 即在守卫 n != 0 下恒真，两函数一次验证闭环。

若不做 SCC 识别，两函数各自验证同一义务仍然通过——只是重复了一次。这印证了 SCC 的定位是优化。

诊断

良基性推不出时，不直接拒绝，而是建议检查方向。 这与递减义务失败的诊断必须区分：前者指向测度取值域，后者指向递归参数。三类失败各自的建议：

失败	建议方向
良基性推不出	测度是否在可能的取值上成立下界（如 `Int` 测度是否需要 `>= 0`）
严格递减判伪	递归参数是否真的朝测度递减的方向走；附 SMT 反例
无测度且探索失败	提示可为该计算绑定名字并在类型位提供测度（RFC-027 §6.9）

反例呈现按 RFC-013 诊断消息规范。非线性的路径守卫下，Sat 反例可能不直观——记录为已知限制，随 RFC-013 迭代。

错误码

对齐 E4xxx 证明失败家族（E4018 精化谓词违反、E4020 需要证明函数）：

提案码	名称	触发
E4021	终止无法证明	探索失败且类型位无显式测度（提示提供 `Terminates` 测度）
E4022	测度不成立	测度义务被 SMT 判伪（附反例）

最终编号以实现时 RFC-013 注册表实况为准（段位合法性由 build.rs 门槛保证）。

诊断层既有缺陷

现行实现中，范围内终止失败以 E8001「内部编译器错误」 的形式报出（Unproven 被按 ICE 格式化）——终止检查不是 ICE，占用该码位既误导用户又掩盖真实故障。本 RFC 一并修正：范围内终止失败走 E4021/E4022，ICE 码位归还给真正的内部错误。

编译器改动

组件	改动
`typecheck/layers/termination.rs`	接口统一化（探索路径与显式测度路径共用义务生成与判定）；接入 Z3（生产管线注入，`with_z3` 目前仅存在于单测）
函数调用图 + SCC（新建）	全仓无跨函数调用图——`TypeDepGraph` 是变量级类型依赖，不可复用。新建函数级调用图与 SCC 收集，供互递归测度共享
义务生成	新增：良基性 / 严格递减两条义务、路径守卫注入、字典序展开
证明管道（RFC-009a / #292）	复用 `ConstExpr → SMTLib` 链路与 `Mod` 等算子映射，无后端改动
`util/diagnostic/codes/e4xxx.rs`	新增 E4021/E4022 注册（经 RFC-013 注册表，build.rs 门槛生效）
locales ×6	两个新码的六语言模板
诊断层	范围内终止失败从 E8001 迁出，改走证明失败家族

向后兼容性

此前因终止检查被拒、但无精化标注的程序：新判据下不进验证模式，直接编译通过——有意的放松，只放宽不收紧。
此前因终止检查被拒、且有精化标注的程序：补写测度后可通过。
结构递归正例、既有终止测试：期望输出不变。

权衡

优点

零新语法：测度写在类型位，复用精化谓词应用机制；无 decreases 类语法位。
证明域行为对齐：终止域补上与正确性域一致的兜底通道，但落点不同——正确性域证不出的命题在体里写证明函数，终止域探索不出的测度在类型位声明。两者机制同一（皆为精化类型应用）。
复用基建：义务是线性算术加路径守卫，走 #292 已接通的管道，无新后端。
循环获得指称：绑定名即锚点，循环与函数在义务生成上完全同构，不需要为循环设计特例。

缺点与风险

前置基建量不小于「接线」：函数级调用图与 SCC 收集需新建，Z3 亦未接入生产管线。SCC 部分可延期（它是优化），调用图部分与 SCC 同源，延期则互递归只能各写各的测度——仍可通过，只是重复验证。
显式测度是低频路径的书写负担：两件套（测度函数 + 类型位声明）比内联标注啰嗦。接受——兜底是低频路径，且换来测度可复用、可单测。
良基性义务的噪声：测度返回 Int 时每次都要证 >= 0。缓解：参数精化若已给出下界则自动导出；推不出时才进残余义务，且只给方向不拒绝。
反例质量：非线性守卫下的 Sat 反例不直观。已知限制。
Terminates 是唯一编译器代写体的谓词：偏离「谓词体全部可用户书写」的纯度。理由：它的断言（每个调用点/回边的测度递减）长在计算结构里，用户写的谓词引用不到函数体或循环体。内置面收敛为一个名字，机制零新增。

替代方案

with decreases (b) 内联标注语法：本 issue 早期提案，已撤回。「终止检查不留标注语法口子」是 RFC-027 的定案决策，内联标注会把未支持的终止模式变成语法位而非类型位，与「一切都是 YaoXiang 函数、一切由类型检查器验证」的世界观相左。
独立证明函数（gcd_proof 返回 Terminates(f, m)，按返回类型扫描发现）：早期设计。作废——它引入了「发现机制」「命名约定」「多候选取首个」「证明函数体内的名字如何解析」四类复杂度，而这些都是因为把证明放到了体外。改为写在类型位后，四类复杂度全部消失。
只让测度入型（Terminates(m)），取消二元形态：更短，但失去「显式指明测度归属」的表达位（测度定义在别处、同一测度服务多个计算时无处安放）。两个元数是同一谓词的两个元数，保留成本近乎零。
不做兜底、要求用户改写为可分析的迭代模式：即现状。gcd / 归并分区 / 相互递归无法在不破坏可读性的前提下改写——这正是再讨论条款的触发条件。

非目标

不新增语法/关键字/标注位。
不做测度自动合成的通用化扩展（四策略维持 RFC-027 既定计划，超出射程走显式测度）。通用测度推断属于「发现」的不可判定侧，只能约定模板边界，不能承诺完备。
不与 RFC-009a 借用命题联合求解（各自独立判定，共享后端）。
不做依赖类型层面的总性验证（totality checking）。
不强制测度返回自然数类型（不追求 Lean 的 WellFoundedRelation 类型类机制）——测度返回类型不受限，良基性作为独立义务交给精化推导或 SMT。

阶段与验收

[ ] 义务生成（良基性 / 严格递减、路径守卫注入、字典序展开）
[ ] 显式测度接线（Terminates 一元与二元形态的锚点解析、类型位测度提取）
[ ] SMT 判定接线（复用 #292 管道，生产管线注入 Z3）
[ ] 函数级调用图 + SCC 收集（测度共享优化）
[ ] E4021/E4022 注册 + 六语言 locales
[ ] 诊断层修正：范围内终止失败从 E8001 迁出，改走证明失败家族
[ ] E2E：正例（gcd / 循环 Terminates(n - i) / is_even-is_odd 互递归）/ 负例（测度不成立 → E4022；无测度 → E4021）/ 结构递归零回归
[ ] 判据回归：无精化标注的递归与循环不再被终止检查拒绝；有精化标注时义务照常触发
[ ] 验收演示：写一个测度不成立的声明 → 编译失败且反例可读；改对后通过

关联

#318（本 RFC 的立项 issue）、#251（父里程碑 P1）
RFC-027（宿主：§7 精化类型判据、§6.1–6.5 测度探索四策略、§6.9 显式测度、§开放问题再讨论条款）
RFC-009a / #292（共享 SMT 管道与路径条件收集——基建前提）
RFC-013（错误码注册表与证明失败语义家族）

RFC-027a: 终止检查的显式测度 ​

摘要 ​

动机 ​

为什么需要子 RFC ​

触发 ​

提案 ​

与自动探索的关系 ​

义务生成 ​

判定管线 ​

锚点：一元与二元形态 ​

SCC：测度共享优化 ​

示例 ​

gcd：非结构递归 ​

循环：匿名构造获得指称 ​

互递归：SCC 共享测度 ​

诊断 ​

错误码 ​

诊断层既有缺陷 ​

编译器改动 ​

向后兼容性 ​

权衡 ​

优点 ​

缺点与风险 ​

替代方案 ​

非目标 ​

阶段与验收 ​

关联 ​

RFC-027a: 终止检查的显式测度

摘要

动机

为什么需要子 RFC

触发

提案

与自动探索的关系

义务生成

判定管线

锚点：一元与二元形态

SCC：测度共享优化

示例

gcd：非结构递归

循环：匿名构造获得指称

互递归：SCC 共享测度

诊断

错误码

诊断层既有缺陷

编译器改动

向后兼容性

权衡

优点

缺点与风险

替代方案

非目标

阶段与验收

关联