讨厌算法的程序员 2 | 证明算法的正确性

第1篇介绍了插入排序算法,这里要提出一个问题:学习算法仅仅是积累一个又一个的算法实现吗?

当然不是。比算法本身更重要也更基础的,是对算法的分析:能够证明其正确性,能够理解其效率。这也是自行设计新算法的基础。如果学了一堆算法的实现,而不能判断算法的优劣,或者靠死记硬背记住了各个算法的复杂度等性能指标,那么随着时间的流逝,这一切都是要还给课本的。

01

算法的正确性

正确性

当我们设计或者实现完成一个算法后,如何证明它是正确的呢?

对于程序员来说,司空见惯的做法是,我们会找几个测试用例,也就是事先定义好的输入输出,然后把输入送进程序里跑一下。如果算法能自动结束,且输出和预期一致,我们就认为算法是ok的。

可是我们无法穷举输入,如何能确定未来的某一输入就一定会有正确的输出呢?靠测试用例是无法保障算法的正确性的。

02

循环不变式

下面介绍能够证明算法正确性的“循环不变式”。

它的英文名是loop invariant,就是正确的算法在循环的各个阶段,总是存在一个固定不变的特性。找出这个特性并证明其固定不变,从而推断出算法是正确的。

具体的说,必须证明循环不变式满足下面三个性质:

  • 初始化:循环的第一次迭代之前,不变式为真;
  • 保持:循环的某次迭代之前不变式为真,下次迭代之前其仍然为真;
  • 终止:循环终止时,不变式依然成立。

这个过程类似于数学归纳法,为了证明某条性质成立,需要证明一个基本情况和一个归纳步。第一步“初始化”可以对应“基本情况”,第二步“保持”对应于“归纳步”。而第三步“终止”也许是最重要的,因为我们将用终止时循环不变式来证明算法的正确性。

这里定义循环不变式的窍门就是:结合导致循环终止的条件一起定义循环不变式。

03

证明插入排序的正确性

利用上一节的“循环不变式”,我们证明第1篇中介绍的插入排序的正确性。

对于插入排序,一开始我们就注意到其在玩扑克牌中的应用,这里面有一个关键的认知:我们手中已经摸到的牌始终是排好序的,也就是我们找到的循环不变式:A[1 ‥ j-1]在循环的三个阶段均为有序。无论在循环前,循环中,还是循环后,它都是不变的。

INSERTION-SORT(A) 1 for j = 2 to A.length 2 key = A[j] 3 // Insert A[j] into the sorted sequence A[1..j-1]. 4 i = j - 1 5 while i > 0 and A[i] > key 6 A[i + 1] = A[i] 7 i = i - 1 8 A[i + 1] = key

插入排序

证明如下:

1、初始化:首先证明在第一次循环迭代之前(当j = 2时),循环不变式成立。此时,A[1 ‥ j-1]中仅由一个元素A[1]组成,“有序性”当然是成立的。从上图中(a)中,有序数组中只有5一个元素;

2、保持:其次处理第二条性质:证明每次迭代保持循环不变式。在循环的每次迭代过程中,A[1 ‥ j-1]的“有序性”仍然保持。上图中所有的黑色块左侧子数组永远都是有序的;

3、终止:最后研究在循环终止时发生了什么。导致外层for循环终止的条件是j > A.length=n,此时j = n + 1。在循环不变式的表述中将j用n+1代替,那么A[1 ‥ j-1]的“有序性”,就是A[1 ‥ n]有序,这就证明了最终的整个数组是排序好的。上图中(f)表明整个数组已经排好序。

以后,我们还会用到循环不变式来证明其他算法的正确性。

原文发布于微信公众号 - 人工智能LeadAI(atleadai)

原文发表时间:2017-09-22

本文参与腾讯云自媒体分享计划,欢迎正在阅读的你也加入,一起分享。

发表于

我来说两句

0 条评论
登录 后参与评论

相关文章

来自专栏PingCAP的专栏

Succinct Data Structure

最近看了一篇论文 SuRF: Practical Range Query Filtering with Fast Succinct Tries,里面提到使用一种...

2326
来自专栏窗户

最多7次比较解决5个数的排序问题的解法

  这一篇是上一篇《12(13)个球1个不同重量称3次称出的详细分析》的姊妹篇,分析手段同出一辙,此题源于《算法导论》。   和上面一样分析,5个数的排列总共有...

18710
来自专栏数说工作室

统计师的Python日记【第5天:Pandas,露两手】

本文是【统计师的Python日记】第5天的日记 回顾一下: 第1天学习了Python的基本页面、操作,以及几种主要的容器类型; 第2天学习了python的函数、...

4087
来自专栏机器学习算法与Python学习

0-1整数规划与隐枚举法-感受剪枝的魅力

前一段时间一直在谈支持向量机,一直到上次给出了改进版的最小二乘支持向量机在实际工程问题中的应用为止算是告一段落了,从今天开始将以斯坦福大学-吴恩达教授的机器学习...

3104
来自专栏深度学习自然语言处理

【python】读取json文件

最近要打个比赛,在处理数据的时候,发现数据竟然是json文件的,于是上网查了下,展示给大家O.O

922
来自专栏TensorFlow从0到N

讨厌算法的程序员 1 - 插入排序

什么是算法 在说插入排序之前,我们了解下《算法导论》对算法的从两种不同角度的定义。 一般性解释: 算法是定义良好的计算过程,它取一个或一组值作为输入,并产生...

3184
来自专栏TensorFlow从0到N

讨厌算法的程序员 2 - 证明算法的正确性

第1篇介绍了插入排序算法,这里要提出一个问题:学习算法仅仅是积累一个又一个的算法实现吗? 当然不是。比算法本身更重要也更基础的,是对算法的分析:能够证明其正确...

2565
来自专栏数说工作室

统计师的Python日记【第3天:Numpy你好】

本文是【统计师的Python日记】第3天的日记 回顾一下,第1天学习了Python的基本页面、操作,以及几种主要的容器类型;第2天学习了python的函数、循环...

37812
来自专栏来自地球男人的部落格

NLTK之朴素贝叶斯分类器

由于学习需要,最近开始接触NLTK,使用最简单的Naive Bayes Classifier,但是写代码过程中各种错误和不顺,现将其记录于此。 之前并不知道分类...

1899
来自专栏自然语言处理

程序员眼中的统计学5

定义:若具有性质A的事件有m个,具有性质B的事件有n个,则具有性质A或性质B的事件有m+n个。

663

扫描关注云+社区