Crab213's Blog.

A Discipline of Programming 1: 系统与形式记号

2016/07/05

本书简介

以前曾经在图书馆看到过此书,当即就觉得很对胃口,可能与我研究过抽象代数有关。这本数更像是一本数学数,我认为它比《算法导论》更为严谨,本书展示了抽象与形式系统结合之后的威力。这本书并没有高深的算法,它主要是作者对编程的思考。

状态空间(state space)及其约束

如果有稍微有点数学背景,甚至说只要上数学课稍微认真过一点,就会发现状态空间的思想无处不在,最典型的就是概率论中的样本空间。

我们从集合的角度看待变量的所有可能状态,这就是状态空间,与向量空间,样本空间是同本同源的。这样做的好处是,我们可以用预言(prediction)来过滤这个集合,筛选集合中的元素。因此,我们可以用一个预言(prediction)来表示特定的状态集合。举个例子,比如A是一个可以表示0-9的个位数的变量,那么它的状态空间就是0-9这十个数字的集合,预言

A = 1 or A = 3

可以表示由1和3这两个数组成的状态集合。

形式记号(formal notion)及其语义(semantic)

我们的编程语言其实是一种形式记号,它与自然语言有本质不同。也许我们将编程语言称作语言是不恰当的,编程语言需要精准表达我们需要的计算步骤,这就牵扯到了语义。编程语言的语义应当是确定的,不能像自然语言那么随性,有歧义。这就要求每一个记号应当有它自己明确的语义。

本书中深刻探讨了编程语言的语义,并设计了一个迷你的编程语言,并对语义进行的严格的数学定义,证明的诸多定理。从我的经验的来看,任何抽象都是建立在具像的基础之上。一个很抽象的表达式,如果结合具体的事物来理解,就能看出作者想要表达出来的思想。

系统

可以粗略认为系统是一个小机器,我们给他一个输入,称为“初始状态”,他就能给我们一个输出。从这个意义上讲,我们的形式记号可以看作一个机器,它将一个初始状态转变成一个终止状态。说成白话,给机器一堆变量,机器可以改变变量的值,这些变量的值就是状态。注意,这个过程并不一定,也有可能这个机器不能正确生成终止状态的情况发生,最简单得例子就是死循环。

我们称可以重复从一个初始状态得到一个确定结果的机器称作确定性机器(deterministic machine),不能重复得到结果的机器称作非确定性机器。

本书中使用了一种很高明的方法定义了一种迷你编程语言。首先,我们的目的很明确,我们希望使用一个形式记号来表示一个系统。比如inc i这条,我们可以让他表示将i的值自增1。但是这样做就落入俗套了,市面上真的不缺这种东西,就像作者书中提到的,这样做就如同eight这个符号一般,我们约定俗称的知道他就是八。而形式系统真正的力量就是我们可以用简单的规则处理复杂的系统,inc i这样的表示完全没有规则可言。

我们的程序就是多个系统的串联,这个是简单的顺序执行模型。我们给最前面的一个系统一个初始状态,然后状态层层传递,直到最后一个系统给出最终状态。也就是说,我们可以从初始状态和终止状态入手。我们用前条件(pre-condition)来表示初始初始状态,使用后条件(post-conditon)来表示终止状态。这里不要搞混了,文中预言(prediction)和条件(condition)是混用的,亦即前后条件是使用预言将两个状态集合具像化的表示出来。

现在就明了了,我们的任务变成了如何将后条件与前条件联系起来,亦即如何用一个条件表示另一个条件。作者反其道行之,使用后条件表示前条件,这就引出了最弱前条件(weakest pre-condition)。一个条件越弱,那么它包含的状态就越多,最弱前条件就是所有是后条件满足的初始状态的集合。记作:

wp(S,R)

式中S是系统,R表示后条件。

CATALOG
  1. 1. 本书简介
  2. 2. 状态空间(state space)及其约束
  3. 3. 形式记号(formal notion)及其语义(semantic)
  4. 4. 系统