6260 notes: termination1——decreases、模子与两次读数

termination1.dfy

六个函数,六把尺子,量的是同一条法律:**凡调用自己的东西,都欠一个"为何不永远调下去"的交代。**照例是底稿,不是教程:错误造句、当场的困惑原样留着,只把结论钉牢。

fib：把定义誊写成代码

// though Dafny gets this one "for free", we can still try
// providing our own decreases clause
function fib(n:nat) :nat
{
    if n < 2 then 1 else fib(n-1) + fib(n-2)
}

读函数:输入自然数 n, 输出自然数,如果输入的 n 比 2 小就输出 1,否则输出函数 fib(n-1) + fib(n-2) 的结果。

提问:为什么不写成否则输出 fib(n-1) 的结果?感觉这就没有求和的效果了，所以写两个 fib 的目的是引入加号吗？

"引入加号"是果不是因。因在定义:斐波那契数本身就是"前两项之和",fib(n-1) + fib(n-2) 是把这句数学定义直接誊写成代码。

老师注释的意思:fib 这种 Dafny 自动猜得中的,decreases 免写;"we can still try providing our own"——但仍可以手写出来,练手感、看清机制。实录:我把 decreases n 写在函数体前面(签名区),绿了,达到的正是这个目的。

插曲:clause 不是 statement

老师的意思是什么?我只看出来说我们可以写 decreases clause,那么 clause 的意思是语句吗,和 statement 相对吗?statement 是啥?

clause / statement,这组词值得掰清。clause 译作"从句",跟语法课上定语从句的"从句"是同一个词:requires ...、ensures ...、decreases ... 都是挂在函数签名上的修饰成分,住在函数头和 { 之间,描述这个函数的性质。statement 是"语句",住在 lemma 体或 method 体里面,是有执行顺序的动作(assert、引理调用、if 块)。

所以上次把 decreases 写进函数体里被 Parser 吐出来,用这对词说就是:把从句当语句用了。

datatype list：一个会传染的读错

datatype list<T> = Nil | Cons(T, list<T>)

读类型定义:类型为装着泛型的列表,构造为两种方式,一是空列表,二是空列表前接头。

后半句错了,而且是会传染的错。"空列表前接头"——不对。Cons(T, list<T>) 的第二个分量是任意列表,不是空列表:Cons(1, Cons(2, Nil)) 里外层 Cons 接的就是个非空列表。按这个读法,列表最长只能有一个元素,整栋楼就塌了。

正确读法:**"一个列表,要么是空表 Nil,要么是一个元素接在某个已有列表前面。"**这个"某个已有"就是递归定义的自指之处,也是归纳法基例加归纳步的来源。

length：从句够不着体内的名字

// similarly, what can we provide here?
function length<T>(l : list<T>) : nat
{
    match l case Nil => 0 case Cons(_,t) => 1 + length(t)
}

读函数:输入一个列表,输出一个自然数。中间计算头的数量 1,再加不断求尾巴长度的数量和,就算出来列表长度。

这次我写的是 decreases l。我原本想写 decreases t,因为递归就递归在 t 上,但是在 t 出场前写 t 不行,就写了 l。

"t 出场前不能写 t"——正是: 从句住在签名区,签名区只认识参数表里的名字 ,t 是 match 拆出来的体内变量,规格够不着它。这跟"ensures 里不许写体内的 n-1"是同一条铁律的两个案发现场: 签名区与函数体,两个作用域,体内的名字不许外漏。 改写 decreases l,绿。

〔勘误〕 当时记成"定义了 length 函数就可以写 decreases length(t)"——按上面这条铁律立不住,t 在签名区依旧不存在。查 termination1.dfy,老师这句话的原型是 ontoback 头上的注释(下一段代码里原文保留),写的是 length(l):length 一旦定义好,后面的列表函数都可以用 decreases length(l) 换掉 decreases l。模子换了件衣服,套的仍是参数。

为什么要学 decreases——lemma 也欠这笔账

提问:为什么我们要学 decreases clause?也是 lemma 体需要吗?为什么需要呢?

要,而且三小时前刚亲手写过。回看绿掉的 decreases_drop:它调用自己,凡调用自己的东西都欠一个"为何不永远调下去"的交代。函数欠,lemma 一样欠——lemma 的自我调用是引用归纳假设,若允许无穷引用,就成了"A 成立因为 A 成立"的循环论证,decreases 保证引用链条有限步触底,归纳才合法。那个 lemma 没手写 decreases,是因为 Dafny 默认猜 (n, l) 恰好猜中了。

终止性不是装饰,是整座大楼的地基——一个不终止的"函数"在逻辑里能推出任何谎话。

ontoback：减小的是入参,不是产出

// once length is defined you can always write
//   decreases length(l)
// instead of
//   decreases l
function ontoback<T>(l : list<T>, x : T) : list<T>
{
    match l
    case Nil => Cons(x,Nil)
    case Cons(h,t) => Cons(h, ontoback(t,x))
}

读函数:输入列表和列表元素,输出列表。如果输入的列表为空,就输出接了 x 为头的列表。如果输入的列表有头有尾,就把 x 接在尾巴上输出。于是整个函数的作用就是把 x 接在列表尾巴上。

手算 ontoback([1,2], 9)(记号:[1,2] 即 Cons(1, Cons(2, Nil))):

ontoback([1,2], 9)
  l = Cons(1, [2]),命中 Cons 分支
= Cons(1, ontoback([2], 9))          ← 本层答案没算完!里面还欠一个调用
  展开欠的那个:l = Cons(2, []),又命中 Cons 分支
= Cons(1, Cons(2, ontoback([], 9)))  ← 又欠一个
  展开:l = Nil,命中 Nil 分支,返回 Cons(9, Nil),债清了
= Cons(1, Cons(2, Cons(9, Nil)))
= [1,2,9]

那么这个函数好像在增加列表而不是在减小列表啊,什么东西在减小呢?

今天问得最好的一问,答案就踩在那行递归调用 ontoback(t, x) 上: 减小的是入参,不是产出。 输出爱多长多长,终止性从头到尾只审一件事:每次递归,喂进去的东西是否严格变小。这里喂进去的从 l 缩成 t,子结构,必减,故必停。产出和消耗是两本账,decreases 只查消耗那本。

核心定则:模子与两次读数

我加了 l 的长度变小这个从句,绿了。很诡异,难道形容某个量变小是在递归这个动作的上下文中吗?它的目的是保证递归逼近 base line 吗?所以和函数产出 l 长度增减无关,上下文并不是函数的产出?

三连问,答案是三连"对"。逐条盖章:

decreases 的上下文是不是递归动作?是,而且精确到只有一个检查点:每一处递归调用的门口。机器在那里停下,量一次尺寸——刚才进来的实参下,这个表达式多大;即将传进去的实参下,又多大——后者必须严格小于前者。除了这道门,decreases 对函数的任何地方都不看一眼。

目的是不是保证逼近 base case? 是,配上前提"不能无限变小"(nat 到 0 触底、列表拆到 Nil 触底),严格递减加有底,合起来就是有限步必停——这就是良基。

和产出无关? 无关,消耗与产出是两本账,审计只翻消耗那本。

钉成定则:decreases 表达式是一把模子,不是一个值。门口量尺寸时,机器把模子套两次——套在本层的 l 上得旧值,套在递归实参 t 上得新值(即 length(t)),比的是这两次套出来的结果。所以那个从句读出来不是"l 的长度在变小"这样一句进行时,而是一份合同:**"每穿过一次递归之门,把这个模子套在新旧实参上,新值必须小于旧值。"**变小的从来不是哪个变量,是跨层比较的两个读数。

这样一钉,前面攒的散点全部串成一条线:模子套的是实参,所以产出无关(ontoback 之问);模子写在签名区,所以只能用参数名,够不着体内的 t(length 的试错);模子可以是任意表达式,所以 100-x、!b、字典序都合法(本篇后半场);而 lemma 的自我调用同样过这道门,所以归纳合法(decreases_drop)。一个检查点,五个案发现场,全是同一条法律。

weird_append：参数变大的障眼法

// weird, *and* inefficient as well!
function weird_append<T>(l1 : list<T>, l2:list<T>) : list<T>
{
    match l2
    case Nil => l1
    case Cons(h,t) => weird_append(ontoback(l1,h), t)
}

手算:

weird_append([9], [1,2,3])
= weird_append([9,1], [2,3])     ← 欠条一
= weird_append([9,1,2], [3])     ← 欠条二
= weird_append([9,1,2,3], [])    ← 欠条三
= [9,1,2,3]                      ← Nil 结清,不开欠条

读函数:输入两个列表,输出一个列表。如果第二个列表为空,第一个列表就是输出结果。如果第二个列表有头有尾,那就输出第二个列表的头接在第一个列表后面,再接第二个列表的尾巴,等于第一个列表接第二个列表。等下,这个函数和 ontoback 一样只递归那一下吗?那这个过程中也是 l2 被打散成头和尾,l2 的长度变小了。绿了。

ontoback 就是 t 被传入 l 的位置接受 match 直到变成 Nil 呗。weird_append 就是 l2 的 t 接受 match。

后一句抓到了最要紧的动词——"传入 l 的位置"。这五个字就是递归的全部秘密:t 这一层是零件,下一层就坐上主位,接受同一场 match 审问;每坐一次主位就瘦一圈,瘦到 Nil,审问终止。

但绿归绿,造句里混进了一个错误的执行图像,不揪会在手写 append 类函数时反咬。错在这半句:"输出第二个列表的头接在第一个列表后面,再接第二个列表的尾巴"——听起来像这一层干了两件事:接了头,又接了尾。不对。看清 weird_append(ontoback(l1,h), t) 的分工:本层只干一件事——把 h 焊到 l1 屁股上;剩下的 t 原封不动,整个扔给下一层的自己。没有"再接尾巴"这个动作,只有"尾巴留给下辈子"。chunks 那篇的话原样适用: 每一层只切眼前一块,烂摊子丢给递归。 正确读法:"把 l2 的头搬到 l1 尾部,然后对'加长了的 l1'和'l2 的尾巴'重复同一件事,直到 l2 搬空。"它是个搬运工,一次搬一个,不是一次拼两段。

"和 ontoback 一样只递归那一下吗?"——问反了个方向,这俩在递归结构上还真不一样,值得对照:ontoback 递归在自家参数的子结构 t 上,标准的结构递归;weird_append 每层还额外调用了一次 ontoback 当工具人(那是普通函数调用,不参与终止审计),而它自己的递归调用里,第一个参数在变大——ontoback(l1,h) 比 l1 长。这正是此函数叫 weird 的原因,也是它存在的全部教学目的:默认模子按参数顺序套 (l1, l2),第一个读数不降反升,合同作废,于是逼你亲手指定"只套 l2"——decreases l2 或 decreases length(l2)。

最后把"l2 被打散成头和尾,l2 的长度变小了"再拧准一毫米——按"模子与两次读数"的讲法:l2 本身没变短,是模子这层套在 l2 上、下层套在 t 上,两个读数一比,降了。昨天钉的定则今天就能拿来给自己的句子挑刺。

up：合同只在门口翻开

function up(x:int) : int
    decreases (100 - x)
{
    if x > 100 then x else 1 + up(x + 1)
}

绿。参数 x 在变大(往 100 爬),度量造出"距离"100 - x 来降。这道有旧底子,写对不奇怪,但"写对"和"值这道题的全款"之间还差一问:

x = 200 传进来,度量是 100 - 200 = -100,负数。度量不是说好了"不能无限变小、必须有底"吗?负数哪来的底?为什么 Dafny 不但没红,连吭都不吭一声?

答案在自己钉过的定则里:门口,只查门口。度量合同的全部条款——新读数小于旧读数、旧读数不小于零——只在递归调用发生的那一刻核验。x = 200 时走的是 then 分支,直接返回 x,根本没有路过递归之门,合同压根没被翻开。而唯一开门的分支在 else 里,进那扇门的前提是 x <= 100,此时 100 - x >= 0,底就在那儿。所以这个表达式在函数定义域的大部分地方是负的,无所谓——**度量不必处处体面,只需在门口体面。**这跟"产出无关、只审消耗"是同一条法律的又一款。

M：bool 也能当尺子

function M(x:int, b:bool) : int
    decreases !b
{
    if b then x else M(x + 25, true)
}

这个没懂,按我理解如果 b 输入为真,那就输出 x,b 输入为假,那就输出 x + 25,停了,就递归这一步,没看出来什么在减小,要说也是真与假这个条件在变。等等,真为 1,假为 0,那就是离真的距离减小了,可是怎么表示呢,bool 类型不能加减。

这段独白几乎是全程正确的推理链——"变的是真与假"、"离真的距离在减小"——最后只在"bool 不能加减"这堵墙前停了脚。墙是纸糊的,两条路随便挑一条穿过去。

先修一处口径:"b 为假,输出 x + 25,停了"——不精确。b 为假时这一层不产出任何东西,它把 (x + 25, true) 递给下一层;下一层 b 已是 true,走 then 分支才真正停。所以递归恰好发生一次,不是零次——"层数边界"病历本添的一笔,差的还是那半层。而这一次递归就是全部案情:门口要量的,是"这一步里什么严格变小了"。

**第一条路:不用加减,Dafny 的模子天生认得 bool 的大小。**内建规矩一句话:false 小于 true。所以布尔值本身就能当度量——但直接写 decreases b 会死:递归这一步 b 从 false 变 true,读数从小变大,方向反了。取个反:decreases !b——门口两次读数,本层 !false = true,下层 !true = false,true 掉到 false,降了,盖章。"离真的距离在减小",翻译成机器话正是"!b 在从 true 掉向 false"。

第二条路:亲手造一个把 bool 折成数的模子。"真为 1,假为 0"——模子本来就是任意表达式:decreases if b then 0 else 1。本层 b = false 读数 1,下层 b = true 读数 0,1 掉到 0,同样盖章。这条路一根内建规矩都不靠,全凭 up 学的"度量可以是任意表达式"。

两条路等价,合起来说明一件更大的事:**度量不挑类型,只挑"能比大小且有底"。**自然数有底(0),列表有底(Nil),布尔有底(false)——凡是降无可降的东西都能当尺子。这就是"良基"三个字的全部野心:termination1 六道题用六种尺子,量的是同一条法律。

收尾:up 与 M 是镜像(口头账)

up 里参数在变大(x 爬向 100),度量造出"距离"来降;M 里参数在变真,度量造出"离真的距离"来降。老师连排这两题,就是要你看见:参数本身的走向无所谓,你永远有自由造一个朝下走的表达式。