用數學視角去看待編程

jopen 8年前發布 | 15K 次閱讀編程

http://blog.sina.com.cn/s/blog_4caedc7a0102w3qx.html

——第十七屆“二十一世紀的計算”學術研討會

圖靈獎得主 Leslie Lamport 的主題演講

大家好！今天我想和大家分享的是用數學的眼光看計算機系統。由于時間有限，我就從最簡單的系統——時鐘講起，這是最簡單的數字化系統。事實上，我不是講解真正意義上的時鐘，而是一比特的時鐘。在工程師眼里，一比特時鐘是這個樣子的：它是一個物理系統，用電壓來表征，是時間的函數。

相信只要學過物理或具備基本的科學常識，你就能看懂這樣的圖表。它的行為用電壓來表征，是時間的函數。現在，我們把它轉變成數字化系統。

從理想化的角度來看待時鐘的行為，無視這個模糊而復雜的時間和電壓圖，我們假設只有兩個數值 0 和 1 。時鐘能夠從一個狀態瞬間切換到另一個狀態。這樣的系統就稱為數字化系統。接著我們把連續的電壓曲線與時間去掉，大家不需要關注時間推進的速度是否正確，只需要關心從 0 到 1 ，從 1 到 0 ，周而復始的過程。也就是說我們不需要關心時鐘具體怎么走，只是把時鐘系統表述為一個序列或是一種行為，兩種狀態構成的一個序列，而這個狀態只是將數值分配到各個變量。

在我們這個例子里，只有一個變量，簡稱為 v 。在這里，有一個具體方法來指定各個狀態序列。首先指定一個初始狀態，然后是狀態切換 —— 如何從一個狀態轉換到另一個狀態則可以用多種方式表述，如編程符號。

指定初始狀態，指定 v 的值為 0 ，然后狀態切換。這可以用方程式來表述，也可以用自動機的方式來表述，比方說這樣，用小圓圈表示各個狀態，用箭頭表示各個狀態之間的切換方向，用有趣的圖片表示初始狀態。這就是人類發明的各種怪異的計算機語言。

我是數學家出身，所以我想采用一種我更擅長的方法——數學來說明。指定初始狀態，所指定的不過是一個狀態集。狀態切換就是兩種狀態之間的關系。集合和關系是數學的核心。那我們如何表示這個狀態集合呢？我會用一個謂詞，或是一個公式來描述狀態集合。狀態是為變量賦值，而狀態的謂詞則是包含這些變量的公式。例如，這是一個表述初始狀態的公式。非常簡單。這是兩個狀態之間的關系，這個也可以表述為一個謂詞，要注意這是基于一對狀態，而非一個狀態。所以，我用一種方法，你們也可以用很多不同的方法，本質上是同一種基本方法，即用一個公式既包含舊狀態，又包含新狀態。我會用 primed 的變量和 unprimed 的變量。 unprimed 的變量表述初始狀態下的變量值。 Primed 的變量表述第二個狀態下的變量值。

我們來舉一個例子。數值 v 和新狀態中 v prime 等于舊狀態中 v 的值加 1 對 2 取余，這就是數學的表示方式。所以我很明白地描述了一個簡單的系統，不用語言，不用圖片，什么都沒有，只用了兩個簡單的公式。還有什么能比這更簡潔？

用一個公式來說明，要實現這一點 , 就要引入一個時序邏輯（ Temporal Logic ）。時序邏輯公式不是關于狀態或狀態對的謂詞，而是行為的謂詞。記住，行為只是狀態的序列。狀態只是對變量的賦值。這很好理解。所以公式類似 vprime 等于 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 。其次下一部分，構造函數，表示對于行為中的所有狀態組合 vprime 等于 v 加 1 對 2 取余成立。所以，這與我先前用表述的完全一致。只用一個公式。

我們現在研究一下更復雜的情況，復雜度提高一倍，一個兩比特的時鐘。我們先從一比特時鐘開始，用電壓 v 和 t 來表示。我們現在加一個低階位。就變成了這樣。

不過這還是一個數字化系統，這樣我們就可以從實際的物理行為進行抽象，從理想化的角度認為各個狀態是離散的。這樣，就有兩個變量，分別是高階位數 v 和低階位數 w ，或者兩個變量非 0 即 1 。這樣我們就得到了系統行為， v 、 w 均從 0 開始，然后低階位開始變化，再變為 0 ，然后高階位開始變化，以此類推。

但如果是一個二比特時鐘，假設忽略第一個低階位，那么就變成一比特時鐘了。也就是說，如果把時鐘上的第二個指針遮掉，那么這就是一個由小時和分鐘組成的時鐘。好，兩位時鐘的行為是這樣的。如果忽略 w ，那么就是一個一比特時鐘。所以這就應該是一比特時鐘的行為。

不過這里有些不對勁。注意我們有兩個狀態 v=0 ，有兩個狀態 v=1 等等，但這些步驟是不允許的，因為每一個步驟都要滿足 vprime 等于 v 加 1 對 2 取余。為了解決這里出現的問題，我們就要讓公式允許“啞步”，也就是說不會改變 v 的值的步驟。因為歸根結底，狀態描述的是系統，只要狀態不變，什么都不會變。也就是說，如果你面前有這么一個一比特時鐘，你根本不知道是否有低階位發生變化。所以我的做法是改變規則，允許另一種情況。每一步要么滿足 vprime 等于 v 加 1 對 2 取余，要么滿足 vprime 等于 v 。所以我經常會這么做，引入一個符號，這個小方括號帶有下標，意思是“或下標未發生變化“。那么問題就來了，這一規則允許一種需要若干步驟才能完成的行為，但什么都不干，只是頓步。

這代表一個已經停止的時鐘，也就是時鐘的高階 v 指針停掉了，雖然時鐘可能發生這樣的事，但我們并不想讓時鐘停下來，我們就要加一個公式，永遠禁止頓步。把這些寫下來，我用兩個公式描述這個時鐘。第一個公式描述的是穩定部分，即時鐘的有限行為。然后另一個公式描述活躍部分，即描述行為的無限后綴。換一種說法，時鐘的穩定部分表示允許發生的情況，而活躍部分表示的是必須發生的情況。對于一比特時鐘，我其實可以把公式寫成這樣。如果你們還記得剛才寫下的那個公式，想一下那個構造函數表示什么含義，仔細思考，你們就會發現，需要無限的步驟才能使 v 變化，也就是說需要演算無限長的時間。實話告訴大家，我大概得花上 15 分鐘時間才把這些活躍度屬性的一般形式寫出來。時間關系，我們這里就不管活躍度了，穩定性是我們首先考慮的，也是大家一般首先擔心的。我們首先需要確保系統不會犯錯，不會產生錯誤的解答，然后再去考慮給出某種答案。為了方便之后使用，我把這個公式命名為時鐘公式。

現在，來描述另一個更有趣的系統。事實上，這是一個很重要的硬件信號編程系統，稱為兩步握手系統。大家知道，這樣一個系統可能位于電腦中的多個位置。各個進程之間利用兩根一位線路通信，我將其分別稱為 p 和 c 。

這里有兩個進程，我將其分別稱為嘀（ Tick ）和嗒（ Tock ）。初始謂詞表示， p 和 c 均等于 0 ，我們稱其為 I 。下一個狀態的關系是兩個公式的分離。

有兩種可能的步驟類型，需要完成一個嘀步驟或嗒步驟。嘀步驟在 p=c 時執行，與 p 形成互補，可從 0 變到 1 ，或從 1 變到 0 ，就像一比特時鐘一樣。同時使 c 保持不變 c 的新值 cprime 等于原值。嗒與嘀類似，不過嗒步驟在 p 等于 cprime 變量時也可能發生。所以在嗒步驟中初始狀態下 p 與 c 不同， c 加上 1 對 2 取余。 p 保持不變，將其記作 N 。這樣，握手協議就可以用這個公式描述，即初始謂詞構造函數，下一個狀態是子 p 和 c 的謂詞。記住，子 p 和 c 的含義是 pprime 和 cprime 等于 p 和 c ，對一個表達式取質數，就表示對表達式中的所有變量取質數。所以就相當于說 pprime c prime 等于 p c 只有在 p 和 c 都各自相等時這一對變量才相等。這就相當于說， p prime 等于 p ， c prime 等于 c 換句話說，這是一個頓步。這也就是說，每一步都是一個 N 步，或者使 p 和 c 保持不變，這樣就有了兩步握手協議。如果你們能想通，你們可以看到只有一個行為，沒有頓步，看起來大致是這個樣子。

好，現在數學公式有了。這個表達式有一點很好，就是可以進行各種神奇的演算，可以演算出很多東西。我要做的就是定義這個表達式。我將其稱為 v? ，定義為 p 加 c 對 2 取余。 v ? 是這些變量的函數，因此在每一個狀態下 v? 都有數值。

我們來看看在各個狀態下的 v ? 數值。

0 加 0 對 2 取余等于 0

1 加 0 對 2 取余等于 1

1 加 1 對 2 取余等于 0

可以想見會發生什么。事實上兩步握手對 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 年左右，而我在幾個月前才聽說。我給 EricVerhulst 寫了一封信，詢問體驗如何。他是這么答復的。他說 TLA+ 的抽象功能大大提高了架構的簡潔度。我很高興地聽他說，對比多年的 C 語言編程獲得的一手結果，代碼規模是一個先前系統版本代碼規模的十分之一。這很大程度上要歸功于他們采用了 TLA+ 進行系統設計和思考。

TLA+ 在亞馬遜網站網頁服務的系統設計中經常用到，幾年前還在 14 個真實的系統中使用，這些系統是亞馬遜網絡服務的組成部分。在《 ACM 通信》雜志 4 月刊上有一篇文章描述了他們使用 TLA+ 時的體驗。英特爾的四個設計小組也使用過 TLA+ 。我在英特爾的朋友已經離職，所以我不知道他們現在在做些什么。微軟也用過 TLA+ 。微軟工程師 DaveLangworthy 是這樣說的：利用高中學的簡單數學就可以找到程序中的缺陷，而在一個實際運行的服務器上，調試幾乎是不可能的。如果幾年前發現了這些錯誤，我們有充分的時間來修復。我們利用的東西都是在高中最晚大學就能學到的簡單方法，算術、集合、函數、一階邏輯等等，再加上 prime 和構造函數，這門語言中唯二小學數學里沒有的東西。如你們所見，非常簡單。所以，典型的系統規范，盡管一般要比兩步握手大一點，不過形式是一樣的——初始謂詞，構造函數，下一狀態關系，變量集合下標以及活躍度公式，大約都是十個這樣的變量。不過，變量可能是一組記錄，對數的函數，或相當復雜的東西；初始謂詞只是一些非常簡單的數學；規范的主要部分是下一狀態關系。我的意思是，不僅僅兩面握手協議的 6 行程序是這樣，一個典型工業規范中的一千行程序也是這樣。

不過，這仍然是簡單的數學， prime ，加上簡單的算術和一些集合、符號，諸如此類的時態邏輯可能有大約 15 個時態邏輯。工程師往往根本不管活躍度，因為他們覺得穩定性部分是最有可能發生錯誤的。他們更有可能構建一個顯示錯誤數字的時鐘，而不是一個停走的時鐘。所以需要在這方面采取措施，這也是規范的主要方面，事實上這些都是很簡單的數學。

Dave Langworthy 說他在高中就學過這些簡單的數學，你也有可能在大學里學到，總之都是很基礎的東西，不像 Mike 說的那么復雜，真的是很簡單的數學。我想引用 Dave 之前寫的第一句話，這些話都是 Dave 寫的，可能還有一些其它的表述沒有列出。這些是他們在某些背景下寫的， TLA+ 教會我如何思考。前亞馬遜員工 ChrisNewcombe ，他是《 ACM 通信》中那篇論文的作者之一，他說 TLA+ 改變了他的思維方式。 BrandonBatson ，我在英特爾的第一個朋友說學習用 TLA+ 寫規范的難點在于如何學會抽象思考，有了經驗后，工程師就能學會了，他們還添加、改進了各自設計的系統。

學會抽象思考其實不是 TLA+ 教會他們抽象思考，但計算機科學家和工程師都認為是語言的神奇力量，相信只要有了正確的語言，全世界的問題都能得到解決。所以，他們看到 TLA+ 時，看到 TLA+ 為他們帶來了了不起的結果時，他們都認為這是因為 TLA+ 是一門很贊的語言。但之所以能取得好的結果，并不是因為 TLA+ 本身， TLA+ 本身并沒有什么特別了不起的地方，而是因為他們學會了如何使用數學。真正讓他們學會思考的是數學的思維方式，而不是編程語言。編程語言可不會教會你抽象思考。還記得么，我們已經看到過多年使用 C 語言導致的洗腦效應。編程語言不會教會你抽象思考，也不是所有編程語言都像 C 語言那樣摧殘大腦。我不是讓大家拋棄編程語言。大家也知道，編程語言很復雜。它們的復雜是因為它們要解決復雜的問題。你寫的程序規模遠超一千行。你寫的程序可以在模型檢驗器中高效地執行，但數學無法高效執行。無論多么設計得多么精妙，沒有哪種編程語言能夠像小學數學這樣讓你覺得如此美妙而強大。也沒有哪種語言能像小學數學這樣簡單而又有富有表達能力。

所以從數學的意義上來看，小學數學比任何編程語言都更有表達能力。計算機工程師面臨的根本問題是復雜度。優秀的工程師能夠讓系統變得最簡。用來描述計算機系統的數學也很簡單。編程語言很復雜，這種復雜是有原因的。你們想看的話，我可以舉出各種各樣的復雜案例。就像對象這種東西，你仔細研究一下，會發現確實復雜。就這一點來說，有些人認為編程方法很復雜，但是編程語言很簡單。人們為了解釋編程語言，就賦予它們語義，他們給編程語言賦予數學中的語義，但從沒有人嘗試過給數學賦予編程語言中的語義。這么做沒多大意義，因為編程語言就是復雜的，無法實現簡化，你無法用復雜的語言進行思考。

要實現簡化，在實施前需要進行抽象思考。這就意味著在寫任何代碼前都要用數學方式思考。 TLA+ 教會你如何用數學方式思考，讓你用數學編寫規范。很少有工程師愿意嘗試。他們經過多年的“洗腦”，喜歡用自己的那套計算機理念，多年的計算機教育讓他們認為 C 語言是極其簡單的語言，而數學是非常復雜的東西。這真是本末倒置。

大學里需要教授數學思維。我想我知道學生們應該學什么，其實要學的也很簡單，只要看一下我說的，把一個系統看成狀態機，就像兩步握手協議初始謂詞，以及下一狀態關系在描述抽象狀態機。不過，是讓學生學會在初始謂詞和下一狀態關系的背景下用數學的方式描述狀態機。因為只要看一下各種編寫自動機編程語言的方式，如圖靈機等，無論是什么狀態機都可以用初始謂詞和下一狀態關系簡單地描述。將實施看作替換，因為你正在做的是實現某種東西，比如一個列表或是一個由指針組成的陣列，這一切實際上都是在實施替換。這與一比特時鐘中的那個一比特位的實施方式完全一樣，是由握手協議的兩個比特位進行實施。你所實施的是更為簡單的數學概念，就像一個列表或者序列，其中包含更復雜的對象組成，而這些對象又可以通過數學的方式進行描述，如陣列或指針。只要掌握了這些，大家就能用數學的方式來思考你所構建的系統了。