6260 notes: 词典序度量、互递归、终止性与第一份归纳证明

例 1 doTheWork：词典序度量，顺序是命门

datatype classlist = NoneLeft | Cons(string, classlist)

// 课上原话：不关心这个函数怎么算，只要它返回一个数。
// Dafny 允许"无体函数"，当作未知但确定的函数。
function classHours (s : string) : nat

function doTheWork(currClassHoursLeft : nat, classesAfterThat : classlist) : bool
  decreases classesAfterThat, currClassHoursLeft   // ★ 主导量写在前
{
    if currClassHoursLeft == 0 then
        match classesAfterThat
        case NoneLeft => /* hooray! */ true
        case Cons(cname, rest) => doTheWork(classHours(cname), rest)
    else doTheWork(currClassHoursLeft - 1, classesAfterThat)
}

语义：手头这门课还剩 currClassHoursLeft 小时作业，后面排着课表 classesAfterThat。函数没有可变变量，"进度"只能靠把新状态作为参数传给下一次调用来体现。

两条递归各自在干什么。else 分支：课没干完，干掉一小时——小时数减 1，课表原样传下去。Cons(cname, rest) 分支：课干完了且课表非空，match 把第一门课的名字拆给 cname、剩余课表拆给 rest，然后开工下一门——小时数不是减出来的，是重新装填成 classHours(cname)，课表缩短为 rest。

设 classHours("A") == 2、classHours("B") == 1，从 doTheWork(2, Cons("B", NoneLeft)) 走一遍：

度量。 第 3 步小时数从 0 跳回一个未知的大数，单看它不下降；但每次跳上去的代价是课表少一门。于是课表是"金牌"（主导量）、小时数是"银牌"：金牌变小则银牌随便涨；金牌持平时银牌必须变小。任何一步恰好落在这两种赢法之一。

为什么必须手写。 默认度量按参数声明顺序取，即 (currClassHoursLeft, classesAfterThat)——在装填那一处第一位从 0 涨上去，直接判负。必须亲手倒过来：decreases classesAfterThat, currClassHoursLeft。

例 2 sumTree / sumTreeList：子结构式互递归，白送

datatype list<T> = Nil | Cons (T, list<T>)
datatype tree = Node(element : int, children : list<tree>)

function sumTree(t : tree) : int
{
    t.element + sumTreeList(t.children)
}

function sumTreeList(trees : list<tree>) : int
{
    match trees
    case Nil => 0
    case Cons(t, ts) => sumTree(t) + sumTreeList(ts)
}

这个 tree 没有 Lf：每棵树都是一个 Node，带一个整数和一张孩子列表，孩子可以任意多。所谓叶子，就是孩子列表为 Nil 的节点。

为什么必须两个函数。 站在一个 Node 上，手里是一个 int 和一张 list<tree>：列表不是树，sumTree 自己吃不下，得交给专吃 list<tree> 的 sumTreeList；而列表每一格里装的又是树，只能递回去交给 sumTree。两个类型互相嵌套，逼出两个函数互相调用——互递归不是技巧，是数据类型的形状逼出来的。

sumTree(整棵树)
= 1 + sumTreeList( [Node(2,Nil), Node(3,...)] )   ← 树交出孩子列表
= 1 + sumTree(Node(2,Nil)) + sumTreeList(...)     ← 列表拆出头和尾
= ... = 1 + 2 + 3 + 4 = 10

为什么白送。 看每一次跨函数调用，传出去的参数从哪来：t.children 拆自 t；t 和 ts 拆自 Cons(t, ts)。零件严格小于整体，有限的值拆一层少一层，必然见底。这和单函数结构递归是同一条原理，只是拆的动作分摊在两个函数身上，Dafny 自动看穿，一个 decreases 都不用写。

判据一句话：递归传出去的东西，是拆出来的，还是造出来的。 拆的免费；造的（比如 doTheWork 里的 classHours(cname)）自己付账。

例 3 SumFrom / SumFromNeg：手写度量 + 补前置条件

// 目标：SumFrom(i,n) = i - (i+1) + (i+2) - ... +/- n
// 例如 SumFrom(3,5) = 3 - 4 + 5 = 4
function SumFrom(i: int, n: int): int
  requires i <= n        // ★ 禁止 i 从 n 的右边出发
  decreases n - i        // ★ 度量 = 离终点的距离
{
  if i == n then n else i + SumFromNeg(i + 1, n)
}
function SumFromNeg(i: int, n: int): int
  requires i <= n        // ★ 互递归的两边都要写
  decreases n - i
{
  if i == n then -n else -i + SumFrom(i + 1, n)
}

lemma sum35() ensures SumFrom(3,5) == 4 {}

在算什么。 正负交替的求和，交替的是 符号。每一步做的事不一样（这步加正、下步加负），而函数没有变量存"当前该取什么符号"——于是把符号编码进"现在轮到谁干活"：SumFrom 贴正号，SumFromNeg 贴负号，干完把 i+1 抛给对方。这个性质在展开序列里可见：

SumFrom(3,5)
= 3 + SumFromNeg(4,5)
= 3 + (-4 + SumFrom(5,5))
= 3 + (-4 + 5) = 4

对照例 2：那边是被数据形状逼成互递归，这边是被行为交替逼成。两种成因，同一种结构。

度量为什么是 n - i。 每次递归 i 在变大，不能做度量；真正缩小的是离终点的距离 n - i。凡"往上数到某个界"的递归（upList、upToNList 同款），度量都是"界减计数器"。

为什么还要 requires。 decreases 的完整规矩是：每步严格变小， 且旧值非负 。若从 SumFrom(7,5) 出发，i 越爬越远永远撞不上 n——真的不停机；度量 n - i 变成 -2、-3、-4，一直在"减"，但负数可以无限减下去。所以必须用 requires i <= n 把这种输入禁掉，且两个函数都可能被外部调用，两边都要写。之前的例子里非负是白送的（nat、列表长度），这里 n - i 是 int，这条规矩第一次咬人——终止性可能依赖前置条件，decreases 和 requires 是一份合同的两半。

跨函数怎么验账。 在 SumFrom(i,n) 调 SumFromNeg(i+1, n) 处，Dafny 做三件事：取被调方度量代入实参得 n-(i+1)；与调用方当前度量 n-i 比，严格小 1 ✓；验旧值非负 n-i >= 0，由 requires 给出 ✓。反方向对称。

前置条件在递归调用处也要付。 递归调用也是调用，得证明实参满足对方的 requires，即 i+1 <= n：进递归分支说明 i != n，加上本方前置 i <= n，得 i < n，整数上即 i+1 <= n。这条推理 Dafny 自动完成，但设计 requires 时"递归调用处它还立得住吗"是必查项。

本例增量（对照例 1、例 2）。 一：度量可以是算式，不必是参数——看到计数器往上爬，反射性地写"界 − 计数器"。二：严格下降 + 旧值非负，缺一不可。三：互递归的账跨函数结算，前置条件在递归调用处同样要付。Lab3 Q16 fib_loop 直接考这套（题面明说 add a decreases and a requires clause）。自查标准：合上文件，能独立给 fib_loop 写出那两行，并说清每一行防的是哪种死法。

附加题 sumClosedForm：第一份归纳证明

lemma sumClosedForm(i:int, n:int)
  requires i <= n
  decreases n - i
  ensures SumFrom(i,n)    ==  (if (n-i) % 2 == 0 then n - (n-i)/2 else -((n-i+1)/2))
  ensures SumFromNeg(i,n) == -(if (n-i) % 2 == 0 then n - (n-i)/2 else -((n-i+1)/2))
{
  if i == n {
    // 基例：SumFrom(n,n) == n，公式给 n - 0/2 == n，Dafny 自动核对
  } else {
    sumClosedForm(i + 1, n);   // 归纳假设：对更近一步的 (i+1, n) 成立
  }
}

公式从哪来。 和式共 n−i+1 项，相邻两项 (i) - (i+1) 恰好配成 −1。项数为偶（n−i 为奇）：全部配完，结果 −(n−i+1)/2；项数为奇（n−i 为偶）：配完剩个 +n，结果 n − (n−i)/2。验算 SumFrom(3,5)：n−i=2 为偶，5 − 2/2 = 4，对上。第二条 ensures 说 SumFromNeg 逐项符号相反，整个和差一个负号。

为什么两条 ensures 捆在一个 lemma 里。 函数互递归，证 SumFrom 的公式中途必然需要关于 SumFromNeg 的知识；拆成两个引理会互相等对方，谁也起不了步。捆成一个，归纳假设一次性同时供货——证明的形状跟着函数的形状走，这是条通则。

lemma 体里调自己 = 取用归纳假设。 lemma 体是语句的世界，调用一个 lemma 是一条语句，效果是把它的 ensures 作为已知事实注入当前上下文（前提是实参满足它的 requires）。手写归纳证明说"假设对更小的成立"；在 Dafny 里这不是说出来的，是调自己调出来的。有了归纳假设，剩下是纯整数代数，SMT 自己扛；基例分支为空，展开即得。

为什么 lemma 也要 requires 和 decreases。 requires i <= n：ensures 里谈论了带前置条件的函数，想合法提到它就得先满足入场券。decreases n - i：lemma 调自己也是递归，同样要过验模具的门，防的是循环论证——归纳假设必须在严格更小的实例上取用。

模板骨架（往后所有递归证明的形状）：

lemma 关于f的性质(与f相同的参数)
  requires 与f相同的前置
  decreases 与f相同的度量
  ensures  要证的等式
{
  基例分支 { /* 通常为空 */ }
  递归分支 { 调自己(更小的实参); /* = 取用归纳假设 */ }
}

Lab3 Q13/Q14、Lab4 Q11/Q12/Q14/Q15 全是这个骨架的实例，差别只在取用的不是自己，而是 lengthAppend、member_append、subset_member 这些别人——但"调用 lemma = 注入已知事实"的动作一模一样。

例 4 ackermann：词典序再现，默认顺序会反

function ackermann(n : nat, m : nat) : nat
  decreases m, n         // ★ m 主导，写在前
{
    if m == 0 then n + 1
    else if n == 0 then ackermann(1, m - 1)
    else ackermann (ackermann(n - 1, m), m - 1)
}

语义：m 是运算的级别，n 是操作数。 逐级展开：m=0 是加一；m=1 算出 n+2，约等于加法；m=2 算出 2n+3，约等于乘法；m=3 是 2^(n+3)−3，约等于幂。模式：每一级运算是把下一级反复迭代出来的——加法是反复加一，乘法是反复加法，Ackermann 把"反复"本身递归化。

三行代码各是一句话：m == 0 分支是塔的地基（加一）；n == 0 分支是迭代的初值条款（起点 = 下一级作用在 1 上）；核心行读作"第 m 级在 n 上 = 第 m 级在 n−1 上的结果，再施加一次第 m−1 级运算"，对照 3 × n = (3 × (n−1)) + 3 即可认出。

逐个调用点对账。 当前度量 (m, n)，规则同奖牌榜：先比金牌 m，m 严格变小则银牌随便涨；m 持平才看 n，n 必须严格变小。

1. ackermann(1, m-1) → (m-1, 1)：金牌降，银牌跳到 1 随它去 ✓。
2. 外层 ackermann(ackermann(n-1,m), m-1) → (m-1, 天文数字)：第一参数爆炸式变大——不重要，金牌降 ✓。词典序威力的极致：主位在降，副位可以任意爆炸。
3. 内层 ackermann(n-1, m) → (m, n-1)：金牌持平，银牌降 ✓。这一处就是 m 单独做度量不够的原因。

缺 m 则第 2 处死，缺 n 则第 3 处死——两个都不可省，顺序不可换。

为什么必须手写。 默认按参数声明顺序取度量，即 decreases n, m；拿它验第 2 处，金牌位 n 涨了，直接判负。不是 Dafny 看不出下降，是它猜错了主次。语义上金牌 m 就是运算级别、银牌 n 就是迭代进度——decreases m, n 是函数语义的直译。度量写对的前提，从来是先懂函数在干嘛。