科技猎非确定性有限状态自动机开创者 Dana Scott：我获得图灵奖之前的 26 年
图注：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 这样总结道：在很大程度上，我的动力来自于我在教学上得到的激励，我很幸运拥有非常优秀的学生，他们中的许多人都成了与我非常亲密的朋友，最让我感动的，是这些学生带给我的启发。
雷峰网 (公众号：雷峰网)
雷峰网版权文章，未经授权禁止转载。详情见。
