证明

译自 Expressing formal proofs in a computer language: Y Scheme 。除非特殊声明，下文中『我』指原文作者 Oleg Kiselyov 正文 我们发现算法语言不但可以用来实现算法，也可以用来描述算法的复杂性或其他某些属性的命题，并且可以给出这些命题的严格证明。下面引用的两篇 USENET 的文章表明，Scheme 可以用于形式化推理 Scheme 自身写成的代码。 第一篇文章提出了关于某个优先队列的实现的一个猜想，并且形式化证明了该猜想。该文章为下一篇文章奠定了基础，而下一篇文章则对『形式化证明』这一概念进行反思。我认为不可思议的一点是，我们用同一种语言同时做到了： 实现算法 描述『算法在特定情况下将构建出什么形状的树结构』的命题 通过数学归纳法严格证明上述命题 另一篇发布于 2003 年 9 月的文章表明，Scheme 宏展开器是个很好的证明助手。 我们真的可以用 Scheme 进行『思考』。 参考 A USENET article formally proving complexity of one particular implementation of priority queues. 该文章（译文下附）于 1998 年十月 12 日星期一 23:51:39 GMT 以 《Can one prove complexity of priority queues?》为题发布于新闻组 comp.lang.scheme 。 A USENET article reflecting on the one above 该文章（译文下附）于 1998 年十月 18 日星期日 20:58:45 以《Expressing formal proofs in a computer language: Y Scheme》为题发布于新闻组 comp....