图灵奖得主Leslie Lamport教你如何用数学思维编程

第十七届“二十一世纪的计算大会”

图灵奖得主Leslie Lamport主题演讲

大家好！今天我想和大家分享的是用数学的眼光看计算机系统。由于时间有限，我就从最简单的系统——时钟讲起，这是最简单的数字化系统。事实上，我不是讲解真正意义上的时钟，而是一比特的时钟。在工程师眼里，一比特时钟是这个样子的：它是一个物理系统，用电压来表征，是时间的函数。

相信只要学过物理或具备基本的科学常识，你就能看懂这样的图表。它的行为用电压来表征，是时间的函数。现在，我们把它转变成数字化系统。

从理想化的角度来看待时钟的行为，无视这个模糊而复杂的时间和电压图，我们假设只有两个数值0和1。时钟能够从一个状态瞬间切换到另一个状态。这样的系统就称为数字化系统。接着我们把连续的电压曲线与时间去掉，大家不需要关注时间推进的速度是否正确，只需要关心从0到1，从1到0，周而复始的过程。也就是说我们不需要关心时钟具体怎么走，只是把时钟系统表述为一个序列或是一种行为，两种状态构成的一个序列，而这个状态只是将数值分配到各个变量。

在我们这个例子里，只有一个变量，简称为v。在这里，有一个具体方法来指定各个状态序列。首先指定一个初始状态，然后是状态切换 —— 如何从一个状态转换到另一个状态则可以用多种方式表述，如编程符号。

指定初始状态，指定v的值为0，然后状态切换。这可以用方程式来表述，也可以用自动机的方式来表述，比方说这样，用小圆圈表示各个状态，用箭头表示各个状态之间的切换方向，用有趣的图片表示初始状态。这就是人类发明的各种怪异的计算机语言。

我是数学家出身，所以我想采用一种我更擅长的方法——数学来说明。指定初始状态，所指定的不过是一个状态集。状态切换就是两种状态之间的关系。集合和关系是数学的核心。那我们如何表示这个状态集合呢？我会用一个谓词，或是一个公式来描述状态集合。状态是为变量赋值，而状态的谓词则是包含这些变量的公式。例如，这是一个表述初始状态的公式。非常简单。这是两个状态之间的关系，这个也可以表述为一个谓词，要注意这是基于一对状态，而非一个状态。所以，我用一种方法，你们也可以用很多不同的方法，本质上是同一种基本方法，即用一个公式既包含旧状态，又包含新状态。我会用primed的变量和unprimed的变量。unprimed的变量表述初始状态下的变量值。Primed的变量表述第二个状态下的变量值。

我们来举一个例子。数值v和新状态中v prime等于旧状态中v的值加1对2取余，这就是数学的表示方式。所以我很明白地描述了一个简单的系统，不用语言，不用图片，什么都没有，只用了两个简单的公式。还有什么能比这更简洁？

用一个公式来说明，要实现这一点,就要引入一个时序逻辑（Temporal Logic）。时序逻辑公式不是关于状态或状态对的谓词，而是行为的谓词。记住，行为只是状态的序列。状态只是对变量的赋值。这很好理解。所以公式类似v prime等于v加1对2取余，记住这个公式是状态对的谓词。所以，这个时序公式为真的前提是当且仅当行为对前两个状态为真。作为一种特殊情况，v=0中没有primed的变量。所以这只是第一个状态的谓词。所以当且仅当第一个声明中v=0为真时，它才为真。

接下来，我要介绍一个单一时序，公式，一个时序运算符，构造函数运算符。当且仅当构造函数F对某种行为和它的所有后缀为真时，构造函数F才为真。所以例如构造函数v=0有什么含义？当且仅当v=0在对行为的每一个后缀为真时，构造函数v=0才对行为为真。不过v=0对行为为真究竟是什么意思？它的意思是，当且仅当在行为的初始状态下为真时v=0才成立。所以当且仅当v=0对行为的每一种后缀初始状态均为真时，v=0才成立。行为的每一个状态都是某个后缀的初始状态，后缀的行为在该状态下开始。所以当且仅当v=0对行为的每一个状态都为真时，v=0才成立。所以，这里的原理都很简单。所以，我要做的就是把这两个公式利用这个构造函数运算符，把它们转换成一个单一的公式。那么，这代表什么呢？这个公式对于这个行为为真。这是两个公式的结合。当且仅当两个公式都成立时才成立。所以，第一个公式v=0表示在行为的第一个状态中v=0。其次下一部分，构造函数，表示对于行为中的所有状态组合v prime等于v加1对2取余成立。所以，这与我先前用表述的完全一致。只用一个公式。

我们现在研究一下更复杂的情况，复杂度提高一倍，一个两比特的时钟。我们先从一比特时钟开始，用电压v和t来表示。我们现在加一个低阶位。就变成了这样。

不过这还是一个数字化系统，这样我们就可以从实际的物理行为进行抽象，从理想化的角度认为各个状态是离散的。这样，就有两个变量，分别是高阶位数v和低阶位数w，或者两个变量非0即1。这样我们就得到了系统行为，v、w均从0开始，然后低阶位开始变化，再变为0，然后高阶位开始变化，以此类推。

但如果是一个二比特时钟，假设忽略第一个低阶位，那么就变成一比特时钟了。也就是说，如果把时钟上的第二个指针遮掉，那么这就是一个由小时和分钟组成的时钟。好，两位时钟的行为是这样的。如果忽略w，那么就是一个一比特时钟。所以这就应该是一比特时钟的行为。

不过这里有些不对劲。注意我们有两个状态v=0，有两个状态v=1等等，但这些步骤是不允许的，因为每一个步骤都要满足v prime等于v加1对2取余。为了解决这里出现的问题，我们就要让公式允许“哑步”，也就是说不会改变v的值的步骤。因为归根结底，状态描述的是系统，只要状态不变，什么都不会变。也就是说，如果你面前有这么一个一比特时钟，你根本不知道是否有低阶位发生变化。所以我的做法是改变规则，允许另一种情况。每一步要么满足v prime等于v加1对2取余，要么满足v prime等于v。所以我经常会这么做，引入一个符号，这个小方括号带有下标，意思是“或下标未发生变化“。那么问题就来了，这一规则允许一种需要若干步骤才能完成的行为，但什么都不干，只是顿步。

这代表一个已经停止的时钟，也就是时钟的高阶v指针停掉了，虽然时钟可能发生这样的事，但我们并不想让时钟停下来，我们就要加一个公式，永远禁止顿步。把这些写下来，我用两个公式描述这个时钟。第一个公式描述的是稳定部分，即时钟的有限行为。然后另一个公式描述活跃部分，即描述行为的无限后缀。换一种说法，时钟的稳定部分表示允许发生的情况，而活跃部分表示的是必须发生的情况。对于一比特时钟，我其实可以把公式写成这样。如果你们还记得刚才写下的那个公式，想一下那个构造函数表示什么含义，仔细思考，你们就会发现，需要无限的步骤才能使v变化，也就是说需要演算无限长的时间。实话告诉大家，我大概得花上15分钟时间才把这些活跃度属性的一般形式写出来。时间关系，我们这里就不管活跃度了，稳定性是我们首先考虑的，也是大家一般首先担心的。我们首先需要确保系统不会犯错，不会产生错误的解答，然后再去考虑给出某种答案。为了方便之后使用，我把这个公式命名为时钟公式。

现在，来描述另一个更有趣的系统。事实上，这是一个很重要的硬件信号编程系统，称为两步握手系统。大家知道，这样一个系统可能位于电脑中的多个位置。各个进程之间利用两根一位线路通信，我将其分别称为p和c。

这里有两个进程，我将其分别称为嘀（Tick）和嗒（Tock）。初始谓词表示，p和c均等于0，我们称其为I。下一个状态的关系是两个公式的分离。

有两种可能的步骤类型，需要完成一个嘀步骤或嗒步骤。嘀步骤在p=c时执行，与p形成互补，可从0变到1，或从1变到0，就像一比特时钟一样。同时使c保持不变c的新值c prime等于原值。嗒与嘀类似，不过嗒步骤在p等于c prime变量时也可能发生。所以在嗒步骤中初始状态下p与c不同，c加上1对2取余。p保持不变，将其记作N。这样，握手协议就可以用这个公式描述，即初始谓词构造函数，下一个状态是子p和c的谓词。记住，子p和c的含义是p prime和c prime 等于p和c，对一个表达式取质数，就表示对表达式中的所有变量取质数。所以就相当于说p prime c prime 等于p c只有在p和c都各自相等时这一对变量才相等。这就相当于说，p prime 等于p，c prime 等于c 换句话说，这是一个顿步。这也就是说，每一步都是一个N步，或者使p和c保持不变，这样就有了两步握手协议。如果你们能想通，你们可以看到只有一个行为，没有顿步，看起来大致是这个样子。

好，现在数学公式有了。这个表达式有一点很好，就是可以进行各种神奇的演算，可以演算出很多东西。我要做的就是定义这个表达式。我将其称为v ̅，定义为p加c对2取余。v ̅是这些变量的函数，因此在每一个状态下v ̅都有数值。

可以想见会发生什么。事实上两步握手对v ̅造成的变化与一比特时钟对v造成的变化完全一样。我们可以证明这一点，这也是数学的奇妙之处——你总是能够证明。不过，我们首先要从数学上说明其中的具体含义。现在来定义(Clk) ̅，公式指定了(Clk) ̅，除了v ̅替换为v。数学公式美妙的地方就在于一种非常重要的运算——替换，无论是编程语言还是自动机之类的都无法进行替换运算，但数学可以。那么我们把带v ̅的(Clk) ̅替换为p，把v ̅的定义替换成v。所以两步握手系统，使v ̅发生的变化，与一比特时钟使v发生的变化一样，只有在行为满足这个(Clk) ̅公式时这一点才成立。所以两步握手系统使v ̅发生变化，与一比特时钟使v变化的方式一样，表明每一位都满足公式Hsk，满足(Clk) ̅公式。或换一种说法，在数学里Hsk公式表示(Clk) ̅。所以，这个文字表述有着简单明确的数学含义。

我可以花上10分钟来写出这个定理的完美证明，简单而严谨的证明不是我们的目标。大家也知道，工程师主要是设计系统的，严谨、简单的证明不是你们的目标。不过这些证明表明你们把事情做对了。如果能够给出证明，握手协议代表时钟协议应该不成问题。如果握手协议不能代表时钟协议，那就有问题了。那么这个公式代表什么含义？两步握手在替换情形下成为了一比特时钟？其实换一种说法，你们实现或优化了一个语句。替换是一个基本的数学概念，在你说某某成为了某某时，这是实现的基础。从基础角度说，有一个定理跟这个定理很像，Hsk代表(Clk) ̅。在编程语言中没有替换的概念。你们可以试试看在赋值语句中替换x，让x获得一个值，这完全行不通。但你可以在自动机下替换，或在一些古怪的计算机语言下进行替换。

有一种语言就可以实现替换。这种语言叫做TLA+，原因很有意思。在TLA+中写握手协议，就是这个样子的。跟我之前写的基本差不多。当然了，也并非完全一样，因为在TLA+里写了取余，而没法写p=c=0。这是一个缩写，代表两个公式p=0和c=0。声明变量，p和c为变量。这将导入整数模运算，如加和百分比运算，嵌入到这一语言中。这些运算在标准模块中定义，获得例示，并导入到几乎每一个规范中。这有点像样板文件。这是这个两步握手协议的TLA+规范。这是一个精美的印刷版本，但其实是你们实际打出来的。你么可以看到，差别不是很大。这就是全部了。如果你问类型声明在哪里？事实上没有类型声明。你们在数学课上有看到过类型声明吗？在某种意义上，类型是一种普通、简单的数学，类型的正确性其实是一个很容易证明的定理。类型的正确性表示p和c始终为0或1，而这就是定义。握手协议代表p始终是0、1集合的一个元素。c是0、1集合的一个元素。还有一个小程序定理来证明，或让我们的工具来检验小定理。

时间有限，我只能给大家演示一个简化的样例，而TLA+是一门真正的语言，而不是简化的案例。它拥有工业级强度的工具。有一个模型检验功能。无穷尽地对系统的小实例进行检验。如果你们试过，你们就知道这不会很有意思。我有这个千处理器系统，我可以用它建立三处理器系统，但这对发现bug非常有效，因为在这三个处理器系统中可以检测所有可能的行为。另外还带有证据检验功能。证明真实系统的正确性总是耗资巨大，在实践中不具备可行性。比如现在环绕彗星的航天器，就是欧洲宇航局的罗塞塔太空飞船，是一个模拟，可以显示彗星表面的登陆车。Virtuoso实时操作系统控制罗塞塔上的多个仪器设备。这个东西就是用TLA+设计的。

这些都是Virtuoso开发团队负责人说的。之前我对此一无所知。这个项目已经进行了10年左右，而我在几个月前才听说。我给Eric Verhulst写了一封信，询问体验如何。他是这么答复的。他说TLA+的抽象功能大大提高了架构的简洁度。我很高兴地听他说，对比多年的C语言编程获得的一手结果，代码规模是一个先前系统版本代码规模的十分之一。这很大程度上要归功于他们采用了TLA+进行系统设计和思考。

TLA+在亚马逊网站网页服务的系统设计中经常用到，几年前还在14个真实的系统中使用，这些系统是亚马逊网络服务的组成部分。在《ACM通信》杂志4月刊上有一篇文章描述了他们使用TLA+时的体验。英特尔的四个设计小组也使用过TLA+。我在英特尔的朋友已经离职，所以我不知道他们现在在做些什么。微软也用过TLA+。微软工程师Dave Langworthy是这样说的：利用高中学的简单数学就可以找到程序中的缺陷，而在一个实际运行的服务器上，调试几乎是不可能的。如果几年前发现了这些错误，我们有充分的时间来修复。我们利用的东西都是在高中最晚大学就能学到的简单方法，算术、集合、函数、一阶逻辑等等，再加上prime和构造函数，这门语言中唯二小学数学里没有的东西。如你们所见，非常简单。所以，典型的系统规范，尽管一般要比两步握手大一点，不过形式是一样的——初始谓词，构造函数，下一状态关系，变量集合下标以及活跃度公式，大约都是十个这样的变量。不过，变量可能是一组记录，对数的函数，或相当复杂的东西；初始谓词只是一些非常简单的数学；规范的主要部分是下一状态关系。我的意思是，不仅仅两面握手协议的6行程序是这样，一个典型工业规范中的一千行程序也是这样。

不过，这仍然是简单的数学，prime，加上简单的算术和一些集合、符号，诸如此类的时态逻辑可能有大约15个时态逻辑。工程师往往根本不管活跃度，因为他们觉得稳定性部分是最有可能发生错误的。他们更有可能构建一个显示错误数字的时钟，而不是一个停走的时钟。所以需要在这方面采取措施，这也是规范的主要方面，事实上这些都是很简单的数学。

Dave Langworthy说他在高中就学过这些简单的数学，你也有可能在大学里学到，总之都是很基础的东西，不像Mike说的那么复杂，真的是很简单的数学。我想引用Dave之前写的第一句话，这些话都是Dave写的，可能还有一些其它的表述没有列出。这些是他们在某些背景下写的，TLA+教会我如何思考。前亚马逊员工Chris Newcombe，他是《ACM通信》中那篇论文的作者之一，他说TLA+改变了他的思维方式。Brandon Batson，我在英特尔的第一个朋友说学习用TLA+写规范的难点在于如何学会抽象思考，有了经验后，工程师就能学会了，他们还添加、改进了各自设计的系统。

学会抽象思考其实不是TLA+教会他们抽象思考，但计算机科学家和工程师都认为是语言的神奇力量，相信只要有了正确的语言，全世界的问题都能得到解决。所以，他们看到TLA+时，看到TLA+为他们带来了了不起的结果时，他们都认为这是因为TLA+是一门很赞的语言。但之所以能取得好的结果，并不是因为TLA+本身，TLA+本身并没有什么特别了不起的地方，而是因为他们学会了如何使用数学。真正让他们学会思考的是数学的思维方式，而不是编程语言。编程语言可不会教会你抽象思考。还记得么，我们已经看到过多年使用C语言导致的洗脑效应。编程语言不会教会你抽象思考，也不是所有编程语言都像C语言那样摧残大脑。我不是让大家抛弃编程语言。大家也知道，编程语言很复杂。它们的复杂是因为它们要解决复杂的问题。你写的程序规模远超一千行。你写的程序可以在模型检验器中高效地执行，但数学无法高效执行。无论多么设计得多么精妙，没有哪种编程语言能够像小学数学这样让你觉得如此美妙而强大。也没有哪种语言能像小学数学这样简单而又有富有表达能力。

所以从数学的意义上来看，小学数学比任何编程语言都更有表达能力。计算机工程师面临的根本问题是复杂度。优秀的工程师能够让系统变得最简。用来描述计算机系统的数学也很简单。编程语言很复杂，这种复杂是有原因的。你们想看的话，我可以举出各种各样的复杂案例。就像对象这种东西，你仔细研究一下，会发现确实复杂。就这一点来说，有些人认为编程方法很复杂，但是编程语言很简单。人们为了解释编程语言，就赋予它们语义，他们给编程语言赋予数学中的语义，但从没有人尝试过给数学赋予编程语言中的语义。这么做没多大意义，因为编程语言就是复杂的，无法实现简化，你无法用复杂的语言进行思考。

要实现简化，在实施前需要进行抽象思考。这就意味着在写任何代码前都要用数学方式思考。TLA+教会你如何用数学方式思考，让你用数学编写规范。很少有工程师愿意尝试。他们经过多年的“洗脑”，喜欢用自己的那套计算机理念，多年的计算机教育让他们认为C语言是极其简单的语言，而数学是非常复杂的东西。这真是本末倒置。

大学里需要教授数学思维。我想我知道学生们应该学什么，其实要学的也很简单，只要看一下我说的，把一个系统看成状态机，就像两步握手协议初始谓词，以及下一状态关系在描述抽象状态机。不过，是让学生学会在初始谓词和下一状态关系的背景下用数学的方式描述状态机。因为只要看一下各种编写自动机编程语言的方式，如图灵机等，无论是什么状态机都可以用初始谓词和下一状态关系简单地描述。将实施看作替换，因为你正在做的是实现某种东西，比如一个列表或是一个由指针组成的阵列，这一切实际上都是在实施替换。这与一比特时钟中的那个一比特位的实施方式完全一样，是由握手协议的两个比特位进行实施。你所实施的是更为简单的数学概念，就像一个列表或者序列，其中包含更复杂的对象组成，而这些对象又可以通过数学的方式进行描述，如阵列或指针。只要掌握了这些，大家就能用数学的方式来思考你所构建的系统了。