非確定性有限狀態自動機開創者 Dana Scott：我獲得圖靈獎之前的 26 年

• 2022 年 7 月 25 日
• AI

圖註：Dana Scott

作為一位在上世紀早期獲得圖靈獎的科學家，Dana Scott 是個典型的通才式科學家，他的研究涉及電腦科學家、數學和哲學等多個領域，他在自動機理論、模態邏輯、模型論、集合論和程式語言理論等問題上做出了開創性的貢獻，尤其是域理論（domain theory），它分析電腦程式語言所必不可少的一種數學理論。

如今的 Dana Stewart Scott 已經 89 歲，從 CMU 退休後一直居住在加州伯克利。本文講述了他在獲得圖靈獎之前 26 年求學、科研與教學生涯。在加州伯克利分校、普林斯頓大學、芝加哥大學、斯坦福大學、牛津大學等地，Scott 先後結識了一批偉大的數學家、電腦理論學家，並受到了他們的深刻影響。他曾師從邏輯學家 Alfred Tarski 和圖靈的導師 Alonzo Church，Rabin 是他的師兄。70 年代，他遇到程式語言設計先驅 Christopher Strachey，與他的合作奠定了現代程式語言語義學方法的基礎。

起於音樂的數學之旅

Scott 於 1932 年出生於加利福尼亞州伯克利，一家人住在蘇珊維爾附近的一個農場，後來搬到了斯托克頓市。如今的他還記得，1941 年 12 月 7 日那天，街上的賣報聲不絕於耳：「號外！號外！快來看啊：珍珠港被轟炸了」。

學生時期，Scott 對音樂產生了極大的興趣，他學會了演奏單簧管，還上過一些鋼琴課。在學習樂器的過程中，他開始思考樂器是如何發出聲音的。他從樂隊老師那裡得到一本書「Science of Musical Sounds」（《音樂的聲音科學》），他被這本書吸引住了。書中的數學知識又激發了他對數學的興趣，叔叔給了他一本微積分的書，他便埋頭啃了起來。

Scott 經常光顧周圍總是塵土飛揚的州立圖書館。他在那裡發現了 Helmholtz 關於聲學和音樂理論的書，受其啟發，他在高中慢慢地研究起了對數和傅里葉級數。高年級的時候，他做了一個關於聲學的小項目，最終獲得了西屋獎學金。

對 Scott 而言，音樂在他的一生中佔有極其重要的地位，他的妻子、女兒和孫女也都是專業級的古典音樂家。

而在學習數學的路上，Scott 從高中數學老師那裡得到了非常多的鼓勵，所以高中時的他就下定決心，如果有機會上大學，一定要主修數學。Scott 的父母都沒有上過大學，而他很幸運地獲得了一筆小額獎學金，足夠他進入加州大學伯克利分校學習。在他的所有直系親屬中，他是第二個獲得大學學位的人。

1950 年進入伯克利後，Scott 報名參加了邏輯入門課程，任課教師是哲學系主任 Paul Marhenke 教授。這門課對 Scott 來說不算難，他也開始喜歡上了邏輯學。升入大二後，Scott 修了更多哲學系 Benson Mates 教授的課，兩人成了關係很好的朋友。Benson Mates 推薦他讀 Alfred Tarski 的作品，Tarski 是全球邏輯學的領導者，此前他在波蘭逃脫了猶太人的迫害，後來進入伯克利做數學教授。

圖註：Alfred Tarski

大學前兩年，Scott 的生活仍比較拮据，為了養活自己，他在校圖書館的期刊室打工。在那裡，他讀了很多符號邏輯期刊上的文章，但幾乎所有文章他都看不大懂，除了 Jan Kalicki 有關真值表的那篇論文。1951 年，Kalicki 應 Tarski 的邀請來到伯克利。Scott 報名參加了他的方程理論課程，Kalicki 自己竟然讀了他的論文感到既驚訝又高興。後來，兩人就合寫了一些關於方程理論的論文，而 Tarski 也早已在研究這些理論。Scott 談起他與 Kalicki 的合作：我們的理論是「完整的」，因為它們必須在不崩潰的情況下才能進一步擴展，因此可以推導出所有方程。

非常不幸的是，在 Scott 認識 Kalicki 第二年的時候，Kalicki 在一場車禍中喪生。這位朋友和導師的離去，給 Scott 帶來了很大的打擊。Scott 回憶，Kalicki 是一位非常了不起的教師，和許多數學家一樣，他可以在沒有任何筆記的情況下授課。那個時期，Scott 已經進入了 Tarski 的圈子裡，大三的時候，他繼續參加 Tarski 的課程和研討會。

後來，Scott 開始學習形式理論，他找到了 Paul Rosenbloom 寫的關於數理邏輯的小書。其中一章是關於 Haskell Curry 的組合器和 Alonzo Church 的 lambda 演算。Scott 花了很多時間弄清楚組合器如何組合，以及它們如何通過方程式進行相互複製，那段時間，他整個晚上都會做關於組合器的噩夢。Scott 回憶，我不知道關於組合器的噩夢是不是加深了我對 lambda 演算的興趣，但這些噩夢確實是一個起點。

1954 年，Scott 留在伯克利繼續攻讀博士，師從 Tarski 。

一開始，Tarski 聘請他擔任助理來對自己的早期著作做翻譯和校對工作。Scott 感到這項工作實在太無聊了，逐漸心生怠惰。可想而知，最後 Tarski 氣憤地解僱了他。從這以後，兩人逐漸變得疏遠。

一位教授聽說了 Scott 的困境，便跟他說：「你為什麼不考慮去別的地方？普林斯頓大學的 Norman Steenrod 正好來這裡訪問，去見見他吧。」最終 Scott 獲得了這位教授的推薦，第二年，他便去了普林斯頓。

正在思考 lambda 演算問題的 Scott，很想得到 Alonzo Church 教授的指導，Church 早期提出了基於無類型限制的 lambda 演算的邏輯系統，他認為這能解決導致羅素悖論的弗雷格系統中的問題，但後來被證明行不通。Scott 認為，Church 其實對此感到很挫敗，這導致他一直都迴避這件事，從來不與學生討論。 

圖註：Alonzo Church

值得一提的是，艾倫·圖靈曾是二戰前 Church 的博士生。當時，Church 很固執地讓 Turing 在他關於超限計算的所有工作中都使用 lambda 演算。後來圖靈曾對此抱怨，但為了獲得博士學位，他不得不聽從導師的要求。Scott 坦言，他覺得這兩人其實關係一直不怎麼親近，而且，在他讀研究生的時候，從來沒聽導師談起過圖靈。

不過，Church 對 Scott 的博士論文選題倒沒有加以干涉。通常情況下， Church 會與學生們討論各自感興趣的研究領域，然後放手讓他們去做。對於 Church 的放養式指導，Scott 很不客氣地說，Church 主要是糾正了他論文中的拼寫錯誤。在與 Tarski 發生過不愉快之後，他與 Church 之間的合作又變得不順利了。

1958 年夏天，Scott 在普林斯頓大學的博士學位後，就到高級研究所（Institute for Advanced Study）里馮·諾依曼建造的電腦上做一些編程工作。當他來普林斯頓讀博的時候，馮·諾依曼就已經躺在了醫院裡，所以一直沒有機會見到他。馮·諾依曼去世後，他建造的那台電腦被轉移到普林斯頓，Scott 解釋，這是因為高級研究所一直都不想做工程方面的事情。

圖註：現代電腦之父馮·諾伊曼

Scott 被聘請在這台電腦上做一個項目，他和一起合作的同事選擇了五格骨牌（Pentominoes）的幾何難題。受到 Dick 和 Emma Lehmer 在伯克利開發的回溯演算法的啟發，他們認為完全能夠解決這個難題。

然而，學校很快發現，讓這台機器運轉起來，實在太昂貴了。靜電管受濕度的影響很大，而普林斯頓是個濕度很高的地方，所以，在馮·諾依曼機器上工作的最佳時間是凌晨 3 點。最後到了秋季的時候，學校再也不願讓他們繼續了，於是關閉了電腦。

回顧在普林斯頓的時光，Scott 既十分懷念又感到些許的遺憾：「普林斯頓是一個非常令人興奮的地方，因為有很多數學家到那裡工作或訪問，師資力量非常強大，但回想起來，如果我那時候能更多地利用我在普林斯頓學到的東西就好了。」

與 Michael Rabin 的合作

與 Scott 一起獲得圖靈獎的 Michael Rabin，當時是 Church 的另一位博士生，兩人讀博期間成了非常要好的朋友。1957 年，他們被選中在 IBM 約克鎮高地研究中心進行暑期實習，一起研究有限狀態自動機問題。

圖註：Michael Rabin

一開始，他們感到無從下手，最終還是決定從模型理論和結構的角度來切入。那時，幾篇關於自動機的論文激發了他們對這個方向的興趣。回想起來，Scott 也說不清他們是怎麼想到做非確定性自動機（nondeterministic automata）的，也許是因為他們在試圖創建狀態來控制各種決策時總是遇到難題。

非確定性自動機與概率自動機不同。當它從一種狀態轉換到另一種狀態時，它可以做出許多選擇，而不是特定的一種選擇。所以，不必擔心有行不通的路徑，因為只需找到其中一條成功的路徑。為了證明非確定性自動機接受與確定性自動機相同的字元串集，我們可以將所有狀態的冪集視為新狀態，並在狀態集上定義轉換函數。當然，狀態的數量呈指數增長。非確定性自動機有時更好用，因為它們需要的狀態要少得多。

夏天結束時，Scott 和 Rabin 一起參加了康奈爾大學的一個邏輯學會議，幾乎所有邏輯領域的學者都出席了那次會議。他們報告了關於自動機的工作，而且又準備了一篇論文在下一學年提交。他們的工作收到的評價很好，諸如「證明得很好，而且很簡潔」之類，不過回想起來，Scott 記得當時並沒有太多人對他們的方法顯示出特別的熱情。

從芝加哥到伯克利

在普林斯頓的最後一個學年，Scott 曾遇到了從芝加哥大學來訪的 Paul Halmos。兩人在代數邏輯方面有著共同的興趣，也是在 Halmos 的推動下，Scott 被邀請以非終身講師的身份去到芝加哥，在那裡擔任講師，直到 1960 年。

剛到芝加哥大學任教時，Scott 遇到了 Stanley Tennenbaum。他對 Scott 影響很大，兩人一起做了很多工作。Tennenbaum 發現不存在滿足一階算術定律的可計算非標準模型，從而為 Emil Post 在遞歸函數理論中的問題提出了一個簡潔的證明，在今天被稱為「Tennenbaum 定理」。不過，由於一場盜竊，他們合作的大部分工作都未得以發表。Tennenbaum 的車被人闖入，那個裝著他們所有文件的盒子被盜走，筆記全部丟失了。Scott 後來肯定地說：當小偷看到盒子里是什麼時，這些筆記肯定在 10 分鐘內就被丟棄了，所以它們從未得見天日。

在芝加哥的兩年任期結束時，Scott 與 Tarski 建立了全面的和解。所以在 1960 年夏天，Scott 回到伯克利，並且獲得了新成立的米勒研究所的獎學金。在超乘積及其與大基數的關係問題上，他做了許多工作。在 1961 年發表的一篇論文中，Scott 證明了可測基數與哥德爾關於「所有集合都是可構造」的觀點相矛盾。非常巧合的是，當時布拉格一位才華橫溢的年輕邏輯學家 Petr Vopnka 也在同一時間發現了同樣的證據。

Rabin 去伯克利休假一年，這期間，Scott 和他又一起度過了非常愉快的時光。Rabin 發現了 Trakhtenbrot 定理的一個新證明，即在有限結構中為真的一階句子的集合是不可公理化的、不可枚舉的。兩人還一起合作，取得了一些其他成果。不過這也是兩人的最後一次合作，Rabin 之後去了耶路撒冷，後來轉去哈佛。

比利時的數值分析師 René De Vogelaere 當時也在伯克利。他非常熱衷於宣傳使用 ALGOL 進行編程。在伯克利，Scott 還結識了許多來訪問的邏輯學家。斯坦福大學的 John Myhill 和他合作了一篇關於「序數可定義性」（Ordinal Definability）的論文，表明可遺傳的序數可定義集合形成了滿足選擇公理的集合論模型。哥德爾看到這項工作後說：「哦，我幾年前就想到了。但我對可構造集合的證明要重要得多，我從來沒有告訴過任何人。」 Scott 對此感到有些無奈：「好吧，就這樣了」。

在斯坦福研究布爾值模型

1963 年，John Myhill 離開了斯坦福，所以斯坦福也就空出了一個職位。而此時的 Scott 在伯克利正經歷著許多不愉快。伯克利的數學系正在大力引進教師、擴展規模，並且開始對 Tarski 有一定程度的敵意，因為他正大力推動邏輯學的發展。Scott 決定擺脫這種環境。

暑假期間，Scott 經常去斯坦福與 Patrick Suppes 一起工作。50 年代 Scott 在伯克利讀本科時，就修讀過他的課程，後來兩人成了親密的朋友。Suppes 一直對如何將邏輯應用於數學心理學感興趣，兩人在 1958 年合作寫了一篇將測量理論與概率論聯繫起來的論文，Scott 在其中的貢獻主要是在模型理論方面。

在 60 年代初期，斯坦福大學的 Georg Kreisel 教授開始定期訪問斯坦福，正是他說服了 Scott 從伯克利搬到斯坦福。

在斯坦福，像 Georg Kreisel 這樣的數學家開始倡導電腦科學在學科上應該更獨立一些。以經典應用數學為主的數學系很樂意放棄數值分析的傳統，來幫助組建新系。當時，Don Knuth 離開加州理工學院，加入斯坦福。麻省理工學院的 John McCarthy 也來斯坦福創辦了他的人工智慧實驗室。Scott 倒沒有直接參与電腦科學系的籌建，但他認識在那裡的每個成員。

從芝加哥大學來到斯坦福的 Paul Cohen 發明了「forcing」，僅僅在少量資訊的基礎上就成功賦予了函數一些性質。而且，他不僅可以將其擴展到整數上的函數，還可以擴展到超有限域，並且他還用它來證明了連續統假設（Continuum Hypothesis）((f)) 獨立於集合論公理。當時，所有人都被他的工作驚呆了。伯克利的 Robert Solovay 經常訪問斯坦福，為的是能與 Cohen 交流研究，他們觀察到，「forcing」 的概念可以為關於集合論的陳述賦予布爾值。

在 1966 年的新年假期中，Scott 對自己說：「「等等。我為什麼不首先從一個合適的布爾代數開始，然後用它來解釋集合論，並以不同的方式來證明連續統假設的獨立性？」最終，這個想法在論文中得以呈現，並獲得了 1972 年 Leroy P. Steele 獎。

程式語言理論研究

Scott 在 1970 年代與程式語言設計先驅 Christopher Strachey 的合作奠定了現代程式語言語義學方法的基礎。與 Strachey 的相識是在阿姆斯特丹大學。

圖註：Christopher Strachey

從 1968 年開始，Scott 在阿姆斯特丹大學休了兩年學術假。期間，他還認識了 Aad van Wijngaarden，他是 ALGOL 語言的設計者之一 。

這年夏天，Scott 參加了關於編程形式化描寫的 IFIP 工作組。在那裡，Scott 聽了很多關於語言設計的話題之後，後來又遇到了 Strachey，看到他的語言設計方法後，Scott 對思考電腦語言產生了濃厚的興趣。

Scott 原本已經決定從阿姆斯特丹搬回普林斯頓，但由於對這些新問題的興趣，他特別請求了哲學系讓我在 1969 年秋季的第一個學期休假，這樣就可以去牛津大學訪問並與 Strachey 一起工作。

在遞歸函數理論方面，Scott 有很豐富的研究經驗。在斯坦福，他講授過自動機理論。許多人都已經寫過關於遞歸函數空間上的運算符的文章。Scott 發現，Strachey 在形式上非常依賴 Church 的無類型 lambda 演算，便跟他說：「如果你考慮有類型的運算，結果就會好得多。」為此，Scott 還專門寫了一篇關於可計算函數邏輯 (LCF)的論文，目的就是為了說服 Strachey 去使用一種數學基礎簡單且可以擴展的方法。Strachey 也馬上很愉快地採用了這種思路。

在斯坦福大學，Scott 遇到的一個困難是那裡的數學系非常注重經典分析，而對邏輯的發展並不真正感興趣。他數學和哲學之間感受到了一種分裂，邏輯在數學中並不是特別受歡迎。

在 1968 年離開普林斯頓的哲學教授 Donald Davidson，後來到阿姆斯特丹訪問，並邀請 Scott 去普林斯頓。

Strachey 於 1970 年代初到普林斯頓拜訪 Scott，那段時間，他們完成了一篇數學語義學（mathematical semantics）方向的論文。這個方向後來被稱為「指稱語義學」（denotational semantics），以便與 Tony Hoare 所提倡的「公理語義學」（axiomatic semantics）和 Gordon Plotkin 所提倡的「操作語義」（operational semantics）區分開來。不過今天，這三種語義學已經融合在了一起，要考慮的是從哪些方面進行分析或證明，或者為某種實現奠定基礎。

在普林斯頓時，正生著病的哥德爾找到 Scott， 請他幫忙保存未發表的筆記，其中有他基於模態邏輯對「上帝存在」的本體論證明。Scott 其實不同意這個結論，他認為，如果你假設你想證明什麼，那你最終就會證明它。不過，有一次，Scott 在未經哥德爾許可的情況下於普林斯頓的一次研討會上談到了這一點，哥德爾的想法因此被公布出來，並被廣泛討論。

圖註：哥德爾

1972 年春天，Scott 很驚訝地收到牛津大學副校長的來信，信中邀請他到牛津做數理邏輯研究。那時，他和家人剛剛搬到普林斯頓，這麼快就又要再次搬家，但 Strachey 和他團隊的工作做得很出色，所以 Scott 決定接受這份邀請。

然而，Strachey 在 1975 年初病倒了，因為寫作那篇獲得 1974 年亞當斯獎（Adams Prize）的論文實在是一項非常艱巨的任務。那年 5 月，Strachey 英年早逝，Scott 為無法再與這位優秀學者合作而感到非常悲傷。

在 1976 年 10 月 20 日的休斯頓，Scott 與 Rabin 在 ACM 年會上一同接受圖靈獎的榮譽。Rabin 的演講題目是「計算複雜性」(Complexity of Computations)，Scott 則就「邏輯與程式設計語言」（Logic and Programming Language）發表了演講……

回顧自己的研究生涯，Scott 這樣總結道：在很大程度上，我的動力來自於我在教學上得到的激勵，我很幸運擁有非常優秀的學生，他們中的許多人都成了與我非常親密的朋友，最讓我感動的，是這些學生帶給我的啟發。

雷峰網