译自 Expressing formal proofs in a computer language: Y Scheme 。除非特殊声明，下文中『我』指原文作者 Oleg Kiselyov
正文
我们发现算法语言不但可以用来实现算法，也可以用来描述算法的复杂性或其他某些属性的命题，并且可以给出这些命题的严格证明。下面引用的两篇 USENET 的文章表明，Scheme 可以用于形式化推理 Scheme 自身写成的代码。
第一篇文章提出了关于某个优先队列的实现的一个猜想，并且形式化证明了该猜想。该文章为下一篇文章奠定了基础，而下一篇文章则对『形式化证明』这一概念进行反思。我认为不可思议的一点是，我们用同一种语言同时做到了：
- 实现算法
- 描述『算法在特定情况下将构建出什么形状的树结构』的命题
- 通过数学归纳法严格证明上述命题
另一篇发布于 2003 年 9 月的文章表明，Scheme 宏展开器是个很好的证明助手。
我们真的可以用 Scheme 进行『思考』。
参考
该文章（译文下附）于 1998 年十月 12 日星期一 23:51:39 GMT 以 《Can one prove complexity of priority queues?》为题发布于新闻组 comp.lang.scheme 。
该文章（译文下附）于 1998 年十月 18 日星期日 20:58:45 以《Expressing formal proofs in a computer language: Y Scheme》为题发布于新闻组 comp.lang.scheme 与 theory.sci.logic。
该文章（译文暂缺）展示了宏展开器有助于证明关于与 (call/cc call/cc) 这样的表达式相关的定理。其中的证明依赖于 syntax-rules 宏执行的 CPS 变换。另一个宏消除了部分 A-可约式（administrative redexes），使得判断两项是否相等变简单了。
附件译文 1
From: oleg@pobox.com
Subject: Expressing formal proofs in a computer language: Y Scheme
Date: Sun, 18 Oct 1998 20:58:45 GMT Keywords: algorithm analysis, priority queue, formal proof, complexity, Scheme
Newsgroups: comp.lang.scheme,comp.theory,sci.logic
Organization: Deja News - The Leader in Internet Discussion
Summary: Scheme as a language to conduct formal proofs of algorithms expressed in Scheme
（其余邮件标头已省略）
Phil Bewig 在十月八日的回复中写道：
我实现的优先队列使用了 Sleator 和 Tarjan 发明的斜堆（手头没有引用链接，但有必要的话我可以找出来）对于 n 个连续的插入和删除花费的总时间应该是 nlog(n)。这段简单的代码 看起来 是线性时间复杂度，但实际上任何单个操作的均摊时间复杂度都是对数级。
我将证明您的说法错误，在一种 特定 的情况下，Phil Bewig 实现的优先队列的插入操作的时间和空间复杂度都是线性级，不存在均摊。因此，在特定情况下这一系列插入的总时间将是平方级。
首先引用 Phil Bewig 原始消息中与本讨论相关的三个函数：
(define priqueue-nil '())
(define priqueue-merge
(lambda (pq-left pq-right)
(cond
((null? pq-left) pq-right)
((null? pq-right) pq-left)
((< (car pq-left) (car pq-right))
(list (car pq-left) pq-right
(priqueue-merge (cadr pq-left) (caddr pq-left))))
((null? (cadr pq-right))
(list (car pq-right) pq-left (caddr pq-right)))
(else
(list (car pq-right) (cadr pq-right)
(priqueue-merge pq-left (caddr pq-right)))))))
(define priqueue-insert
(lambda (k pq)
(priqueue-merge (list k priqueue-nil priqueue-nil) pq)))
然后是我的论点。
定义：
(define (PQ k)
(if (zero? k) priqueue-nil
(priqueue-insert k (PQ (- k 1)))))
(define (PQ-map f pq)
(if (null? pq) '()
(list (f (car pq)) (PQ-map f (cadr pq)) (PQ-map f (caddr pq)))))
(define (plus2 x) (+ x 2))
定理 A：对于 n，当 n 为奇数时，(PQ n) 有以下结构。而当 n 为偶数时，也有类似结构（去掉最右侧的叶子节点）：
(PQ n) = (list 1 '(2 () ()) (PQ-map plus2 (PQ (- n 2))) ;; n>2
(PQ 1) = '(1 () ())
(PQ 2) = '(1 (2 () ()) ())
证明：讨论基本情况
(PQ 3) => (1 (2 () ()) (3 () ()))
;; 或 (list 1 '(2 () ()) (PQ-map plus2 (PQ 1)))
(PQ 4) => (1 (2 () ()) (3 (4 () ()) ()))
;; 或 (list 1 '(2 () ()) (PQ-map plus2 (PQ 2)))
运用数学归纳法，我们先假设命题对某个大于等于 3 的 k 值成立，即优先队列具有以下形式：
(PQ k) = (list 1 '(2 () ()) (PQ-map plus2 (PQ (- k 2))) ;; ①
然后证明定理对 k+1 的情况也成立，考虑插入第 (k+1) 个元素时，由 priqueue-insert 定义得
(priqueue-merge (list (+ k 1) '() '()) (PQ k)))
跟踪 priqueue-merge 的函数体如何执行，其参数为：
pq-left = (list (+ k 1) '() '())
pq-right = (PQ k) ;; ②
可知 (car pq-left) 等于 (+ k 1) 而 (car pq-right) 等于 1。此外 (cadr pq-right) 等于非空列表 '(2 () ())。因此 priqueue-merge 函数执行时在 cond 分支处会跳转到 else 子句从而返回：
(list 1 '(2 () ())
(priqueue-merge (list (+ k 1) '() '()) (caddr pq-right)))
即
(list 1 '(2 () ()) (priqueue-insert (+ k 1) (caddr pq-right)))
别忘了 pq-right 等于 (PQ k)（②），将 (PQ k) 代入后可以运用归纳假设（①）重写上式，重写后的式子里我们重新得到了：
(list 1 '(2 () ()) (priqueue-insert (+ k 1) (PQ-map plus2 (PQ (- k 2))))) ;; ③
我们可以在保证求值结果相同的前提下交换 PQ-map 和 priqueue-insert/priqueue-merge之间的求值顺序，上式中 priqueue-insert 子式等价于：
(PQ-map plus2 (priqueue-insert (- k 1) (PQ (- k 2)))) ;; ④
由 PQ 的定义得 (priqueue-insert (- k 1) (PQ (- k 2))) 等价 (PQ (- k 1))，联合 PQ 的定义与 ③，④ 可得：
(list 1 '(2 () ()) (PQ-map plus2 (PQ (- k 1))))
证毕。
定理 B：令 pqn 为 (PQ n)，则求值 (priqueue-insert (+ n 1) pqn) 需调用 priqueue-merge 函数 floor(n/2)+1 次。
证明：回顾定理 A 的证明过程，我们讨论了 (PQ n) 的具体形式
(PQ 3) => (1 (2 () ()) (3 () ()))
;; 或 (list 1 '(2 () ()) (PQ-map plus2 (PQ 1)))
(PQ 4) => (1 (2 () ()) (3 (4 () ()) ()))
;; 或 (list 1 '(2 () ()) (PQ-map plus2 (PQ 2)))
;; (priqueue-insert 2 (PQ 1)) 调用 1 次 priqueue-merge
;; (priqueue-insert 3 (PQ 2)) 调用 2 次 priqueue-merge
;;（在此不包括求值 (PQ 2) 过程中调用 priqueue-merge 的次数）
如上所示，(priqueue-insert (+ k 1) (PQ k)) 会调用 priqueue-merge 然后返回
(list 1 '(2 () ())
(priqueue-merge (list (+ k 1) '() '()) (caddr pq-right)))
可以看出为了求值该表达式，我们需要在非尾调用位置调用 priqueue-merge（意味着每次调用它都会增长栈空间）。其调用的次数等于求值下式中调用 priqueue-merge 的次数：
(priqueue-insert (- k 1) (PQ (- k 2)))
同理用数学归纳法，易证其次数为 floor((k-2)/2)+1。因此
(priqueue-insert (+ k 1) (PQ k))
需要调用 1 + floor((k-2)/2) + 1 = floor(k/2) + 1 次 priqueue-merge，证毕。
附件译文 2
From: oleg@pobox.com
Date: Sun, 18 Oct 1998 20:58:45 GMT
Subject: Expressing formal proofs in a computer language: Y Scheme
Newsgroups: comp.lang.scheme,comp.theory,sci.logic
Organization: Deja News - The Leader in Internet Discussion
Summary: Scheme as a language to conduct formal proofs of algorithms expressed in Scheme
（其余邮件标头已省略）
本文要讨论的是『用于讨论语言』的语言：我们如何推理一段代码的正确性？如何证明算法的实现是正确的？要用什么样的语言来证明？ML 有个奇妙的性质：它是一种可以轻松表达相关命题的推理过程的语言1。本文旨在说明 Scheme 也有同样的能力，Scheme 可以用来形式化地描述并且证明 Scheme 编写的算法的一些性质。因此 Scheme 也是它自己的元语言。
首先要讨论的是，人们通常如何推理算法和程序的正确性？随便举两个例子。FFT 算法，可以称得上是最美丽的算法。是 Cooley 和 Tukey 在其原始论文用诸如求和符号和二三级的下标这样的标准的数学符号推导而出的。任何 FFT 算法实现，只要忠实地按正确的顺序计算原论文提到的所有和与乘积，就是正确的实现。而 Dijkstra 最短路径算法则通过在纸上绘制图和已到达的顶点集来解释算法。它也用集合论符号进行了形式化证明。同理，只要『遵循着算法证明』来实现算法，就是正确的实现。
上述典型例子表明，算法通常用常规的代数/集合论语言来描述命题和构造性的证明，然后用另一种算法语言在计算机上实现。如果我们始终使用『同一种语言』，似乎有一种更直接的方法可以表达算法，描述有关算法正确性的命题，并且证明这些命题。
有一天，我试图 形式化 证明某优先队列（堆）的 Scheme 实现的空间与时间复杂度问题。我猜想该算法在某组不幸的输入数据下，构建的数据结构（二叉树）是不平衡的。当然，我必须证明猜想。鉴于本文仅讨论『证明』的形式，因此不赘述证明本身。我已将完整证明发布在 comp.lang.scheme 上，也可以在这里获得。
我先以传统方法开始，把在特定的输入情况下算法构建出来的二叉树画在纸上。但我突然意识到我可以简洁地把我的猜想描述为如下形式
(PQ n) = (list 1 '(2 () ()) (PQ-map plus2 (PQ (- n 2))) ;; n>2
(PQ 1) = '(1 () ())
(PQ 2) = '(1 (2 () ()) ())
如果我要在期刊或论文中发表这些。我会把 (PQ n) 写成 $PQ_n$ ，并定义其为连续插入从 1 到 n 元素形成的队列，我会使用更奇怪的符号替代 PQ-map、plus2，甚至可能把 (list ...) 表达式画成一个树节点。上面描述的猜想类似于用常规数学符号表达的猜想。然而最显著的不同是。(PQ n) 和 (PQ-map) 有如下定义
(define (PQ k)
(if (zero? k) priqueue-nil
(priqueue-insert k (PQ (- k 1)))))
(define (PQ-map f pq)
(if (null? pq) '()
(list (f (car pq)) (PQ-map f (cadr pq)) (PQ-map f (caddr pq)))))
它们都是 合法的 Scheme 函数。priqueue-insert 是我正在研究的函数，PQ 是描述了这个函数创建的队列的某个属性的函数。因此，我的猜想是一段合法的 Scheme 代码，而且可以接受特定的 n 输入并求值。在开始正式的形式化证明之前，请允许我小试牛刀，以说明我并非是在痴人说梦。我用 Scheme 求值下列表达式：
(equal?
(PQ 42)
(list 1 '(2 () ()) (PQ-map plus2 (PQ 40))))
Scheme 解释器返回 #t。那么，我继续通过数学归纳法进行证明，假设上述断言对(PQ k) 成立，要证明对于其对 (PQ (+ k 1)) 也成立，我要手动追踪(priqueue-insert (+ k 1) (PQ k)) 是如何执行的－－本质上我是在『部分地』或『符号上地』对 (PQ (+ k 1)) 求值。其中 k 是未绑定的自由变量，即归纳变量。通过手动追踪代码－－追踪控制流，变量绑定，在条件分支点处作出判断并确保这些判断可证明，我人工完成了 Scheme 解释器的大部份工作。既然我们用 Scheme 描述了定理，也用 Scheme 进行证明，那我们是否可以直接用 Scheme 解释器来完成这些工作呢？当然，某些判断，尤其是遇到自由变量时，需要人工指导解释器作出。这个问题我思考过，但是没能得出答案。此外，本文并不打算牵扯太多形式化定理证明器有关的内容。本文只是举了个例子，表明如何 使用 算法语言来描述命题和进行 形式化 证明。我们真的可以用Scheme 进行『思考』。这样做的好处是在某些特殊的或者更形式化的场景下，我们可以借助 Scheme 解释器的力量。
我必须为本文没有提供更积极或者更通用的结论就草草结束而抱歉。因为本文只是一次对『证明的形式』的深思，言者所以在意，得意而忘言。
译后注
当我们讨论计算机证明时，类型论爱好者可能会立即想到『依值类型（dependent type）』或者『Curry-Howard 同构』。基于类型论的指导思想，人们开发了 LCF、HOL、Isabelle、Coq、Adga、Lean……等等一系列定理证明器。但是，是否存在一种更简洁的方式思考计算机证明呢？计算机证明是否可以独立于类型存在？
1971 年，Robert S. Boyer 与 J Strother Moore（读者可能已经知道了他们发明的字符串匹配算法）在爱丁堡大学开始开发 NQTHM 定理证明器。NQTHM 定理证明器使用动态类型的 Lisp 语言开发，因而使用下列方式描述命题（引用自 Wikipedia）
(DEFN TIMES (X Y)
(IF (ZEROP X)
0
(PLUS Y (TIMES (SUB1 X) Y))))
(prove-lemma commutativity-of-times (rewrite)
(equal (times x z) (times z x)))
其形式类似于下列程序
(define times
(lambda (x y)
(if (zero? x)
0
(+ y (times (- x 1) y)))))
(define commutativity-of-times
(lambda (x z)
(equal? (times x z) (times z x))))
如果我们可以在运行 commutativity-of-times 之前就知道这个函数总是返回 #t。那么说明这个函数对应的命题（乘法交换律）成立。NQTHM 通过一系列的『项重写（term rewriting）』规则，包括内部预定义的规则以及人机交互过程中输入的新规则，将命题 commutativity-of-times 改写为对于任意的 x 与 z，(equal (times x z) (times z x)) 恒返回 t 的程序，这些改写的步骤便是命题的证明
NQTHM，以及 Common Lisp 写的其继承者 ACL2，被称为『Boyer-Moore 风格的定理证明器』，对这种定理证明器感兴趣的读者，可以阅读著名小人书系列作者 Dan P. Friedman 写的《The Little Prover》。
参考
ML 语言最早被开发为 LCF 定理证明系统的“元语言” ↩︎