分享

［编者注： This article is published on behalf of the author of Dr Yungang Bao。］

1912年“计算机科学之父”阿伦•图灵(Alan Turing)诞生。1930年代，计算机先驱们齐聚普林斯顿小镇，图灵、邱奇（Alonzo Church）、冯诺依曼（John von Neumann）、哥德尔（Kurt Gödel）、克林（Stephen Kleene）……。 2012年，普林斯顿大学举行了“世纪图灵纪念庆典”，邀请了20位嘉宾（包括8位图灵奖得主）介绍计算机科学的前世今生。
普林斯顿的校园里一下子多了一群耄耋老人，他们在向后人回忆当年图灵、邱奇等先驱在普林斯顿开拓计算机科学的那一幕幕往事，仿佛让人感觉回到了上世纪30~50年代那个“激情燃烧”的岁月。然而，当听到邱奇的学生80岁的斯科特教授（Dana Scott） (1976年图灵奖得主)多次黯然感慨，“这也许是我人生最后一次机会在公开场合向大家分享当年和导师邱奇一起学习、工作、生活的回忆了……”，“请再给我一个机会，我想最后再以个人身份讲一下邱奇的故事，他真是一个非常好的人，我当时就是住在他家里……”，又让人感觉到老人们似乎想在图灵百年之际向世人谢幕。此时，所有人都会安静下来，默默地聆听他们的回忆，然后报以最热烈的掌声，来表达发自内心的感动和敬意。

1. 图灵机的偶然与必然
斯科特教授是邱奇的学生，他也许是这个世界上距离那段历史最近的人了。斯科特教授的报告介绍了λ算子的过去和现在，递归函数以及图灵机之间的故事，中间不断向听众透露许多不为人知的佚事，现场气氛非常欢快。

邱奇在1930年代初提出λ算子，核心思想是“万物皆可为函数”。邱奇给出一组无类型（untyped）的函数定义规则（因为无类型而无法区分函数与参数，所以λ算子会产生递归），然后又加了几条规则，试图用函数来形式化整个逻辑系统。但后来他的学生克林发现这套逻辑系统不一致。邱奇非常失望，把整个逻辑部分全都抛掉，在1935年只把λ算子部分发表了。所以，λ算子对邱奇本人来说是一段很痛苦的经历，再也不想向其他人提及。斯科特教授说，他在普林斯顿读书的时候，从来没有听导师谈过λ算子。

1936年5月，图灵也发表了著名论文《论可计算数及其在判定问题上的应用》（On Computable Numbers, with an Application to the Entscheidungsproblem），提出了图灵机。随后图灵来到了普林斯顿大学跟邱奇读博士。这段时间，他又证明了图灵机和λ算子也是等价的。而在1936年前后，克林提出了一般递归函数（General Recursive Functions），后来邱奇证明和λ算子也是等价的。因此，图灵机、λ算子和一般递归函数都是等价的。

当时在普林斯顿高等研究院的冯诺伊曼在了解了图灵的工作后立刻意识到其重要性，他极力邀请图灵博士毕业后继续留在普林斯顿工作，但图灵非常想家，还是婉言拒绝了。随后1945年，在距离普林斯顿不远的宾夕法尼亚大学，第一台电子计算机ENIAC诞生了。但它太难操作了，人们开始寻找高效的编程方式。于是从1950年代开始，人们开始设计高级语言。1957年，巴克斯（John Backus）带领团队率先发明了第一个高级语言Fortran。与此同时，麦卡锡（John McCathy）则受λ算子启发，在1958年设计出了LISP语言。邱奇肯定不曾想过，曾经因为逻辑不一致而几乎被他抛弃的λ算子成了计算机高级语言的基础。

历史总是充满了各种巧合。在1936年以前的几千年人类文明中，人们从来没有思考过“什么是可计算的”这个问题，但在1935～1936年的一年间，却一下子提出了三种等价的理论，这岂不是太巧合了？紧随斯科特教授，来自英国爱丁堡大学的沃德尔（Philip Wadler）教授在第二个报告《邱奇的巧合》（ Church’s Coincidences）一开始就提出了这个发人深省的问题。事实上，人类科技史中诸如此类的巧合比比皆是，沃德尔教授又举了好几个例子。比如，牛顿在1666年发明了微积分，而莱布尼茨在1675年也独立发明了微积分；达尔文在1859年提出进化论，而华莱士（Alfred Wallace）其实在1855年也提出了相同的理论；而贝尔和格雷（Elisha Gray）在神奇地在1876年的同一天提交了电话发明专利。

表面上历史充满了各种巧合，但如果把这些巧合放回当时的历史背景下，我们就会发现它们的出现又是必然的。今天我们将它们视为巧合是因为后人割裂了历史，只记住了少许闪光点而忽略了知识变迁过程中的幕后推手。

为了揭示图灵机巧合的必然性，沃德尔教授向听众还原了计算理论变迁的那段辉煌的历史。故事要回溯到1900年希尔伯特提出的23个数学问题，其中第2个问题是能否机械化地证明算术公理系统的一致性。1928年，希尔伯特又进一步提出了判定问题（Entscheidungsproblem），即能否找到一个算法自动地判定谓词（一阶）逻辑表达式是真还是假。1931年，哥德尔提出了不完备性定理，他构造了一个命题——“这个命题是不可证明的”，对希尔伯特的第2个问题给出了一个否定的答案。为了证明不完备定理，哥德尔写出了第一个“计算机程序”（哥德尔的程序只是用逻辑公式去形式化了几个步骤，并未定义编程规则）来验证一个命题是否能被证明。人们又从哥德尔的“程序”中觉察到希尔伯特判定问题也可能不存在答案，即没有这样的算法或不可计算。但要想证明这点，首要的是定义清楚什么是算法（或什么是有效可计算性，Effective Computability）。

全世界的数学家们都在思考可计算性定义问题，普林斯顿的数学家们也不例外。1932年，邱奇给出了第一个定义——λ算子，他本希望用λ算子来形式化逻辑系统。那时，克林正在普林斯顿大学跟邱奇攻读博士学位，也在思考可计算性定义问题。当邱奇提出λ算子后，克林发现λ算子能表示整数算术系统，这似乎是可计算性的定义了。他和哥德尔讲了这个想法，但哥德尔并不认为这定义了可计算性。克林不服，向哥德尔下了战书——如果这个定义不对，那请把你的定义拿出来，我能证明两者是等价的。1934年，哥德尔在普林斯顿高等研究院的报告中提出了一般递归函数概念。当时，刚博士毕业的克林记下了笔记。两年后（1936年），克林将一般递归函数具体化，并证明了和他之前的定义是等价的。随后邱奇又证明一般递归函数和λ算子也是等价的，并用λ算子证明了希尔伯特判定问题是不可计算的。不过“狡黠”的哥德尔还不肯承认，狡辩道，也许我的定义是错误的。

1935年的英国剑桥大学，纽曼（Max Newman）教授正在给一个关于希尔伯特判定问题的报告。他总结道，现在解决判定问题的关键就是找到可计算性的定义。23岁的图灵也在报告现场，他便开始独自思考这个问题。1936年，他发表了划时代的论文《论可计算数及其在判定问题上的应用》，用图灵机来定义可计算性（或算法），然后用图灵机重写了哥德尔在1931年的那个“程序”，也证明了希尔伯特判定问题是不可计算的。尽管图灵的证明方法比邱奇晚了几个月，但却更直观、更易于理解，而且更像一台可操作的机器。

在1936年前后的一年间提出三种完全等价的可计算性定义，都源自于希尔伯特的判定问题。到此，听众们恍然大悟又若有所思–这段经典的历史对我们又有何启发呢？我们又能在人类知识变迁历史中扮演什么角色呢？

2. 大科学（Great Science）
2000年图灵奖得主现清华大学的姚期智教授做了一场精彩的关于量子计算的报告。姚教授坦诚地说，现在自己也无法预言量子计算机何时能实用，但认为量子计算符合他定义的大科学标准。

什么是大科学？姚教授认为有两个参考标准：1）大科学是多学科交叉产生的；2）大科学伴随着颠覆性技术的出现。

姚教授举了两个例子。一个是X射线晶体学。1895年，伦琴发现X光；1912年冯-劳埃通过X衍射证明了X是波；1913年，布拉格父子提出用X射线来测晶体结构的方法；于是到了1920年代，人们开始用X射线来测金属、离子以及大分子的结构。随后人们开始讲X衍射技术应用到了生物领域，终于1950年代发现了DNA双螺旋结构，开辟了生物研究新疆界。

另一个是计算机科学。二十世纪初，希尔伯特提出数学的机械化证明。1936年图灵机出现，但只是理论模型。1945年，电子计算机发明，随后肖克利等发明了晶体管，从此计算机的运算速度便按照摩尔定律飞速发展，这是数学和半导体技术的结合。毫无疑问，这两个例子都是伟大的科学，它们彻底地改变了人们的知识和生活。

回到姚教授的报告主题，他认为量子计算正是X射线晶体学与计算机科学的结合，并举了一个非常有趣的例子。以西蒙问题（Simon’s Problem）为例，假设F(x)会将2个不同n位的0-1比特串x和s映射到同一个值，即F(x+s)=F(x)，那么给定x，如何找到对应的s？传统的算法需要对F(x)进行2n次查询操作。量子计算则可以把F(x)和F(x+s)看做是两个晶体，然后用光线去照射，这样就可以根据不同的干涉条纹，然后就可以得到s。这样的操作只需要3n个光子就可以，其中的原理和用X射线衍射结果反推出晶体结构很相似。另一方面，世界各个国家都在量子计算研究投入很大的经费，量子器件的发展速度也超乎大多数人的想象。例如，目前已经有技术能实现14个粒子的量子纠缠；现在已出现传输单个光子的技术，这就意味着可以利用单个光子发送量子信号。姚教授认为，虽然很多人对量子计算表示怀疑，但从事量子计算的科学家们却要乐观的多。

姚教授做研究遵循大科学的标准，过往的经历也使他更坚信做研究应该选择有价值的问题。姚教授2004年回清华前是在普林斯顿大学开展研究工作，过去两年我很幸运有机会也在普林斯顿大学做访问博士后，所以这里的科研价值观，我也有些体会。在普林斯顿，很多教授和学生都非常自信，认为只要他们决定去做一件事，就一定能做好。另一方面大家又意识到，做一件琐屑的小事，所花的精力其实并不比有价值的大事少。因此，在这种自信心和价值观的支持下，他们就敢于去尝试一些很有挑战的问题，有时甚至会跨很大的方向。

李凯教授的研究经历就是一个很好的例子。他博士工作首次提出了软件分布式共享内存（Distributed Shared Memory，DSM）思想，到普林斯顿后又做了硬件共享内存系统SHRIMP，之后研究用多个投影仪组成可扩展显示墙（Scalable Diaplay Wall），后来又转到研究基于内容的多媒体搜索技术。而创办Data Domain公司时则进入存储领域，研制出世界上第一个数据冗余存储产品。如今，他和脑科学领域专家合作，开展脑科学计算的前沿研究。虽然不是所有的项目都像DSM和Data Domain那样成功，但通过开展这些有挑战的项目，积累了许多高质量论文（h-index为64），培养了不少出色的人才，也在同行中建立了学术威望。

3. “定义”的力量
2010年图灵奖得主哈佛的瓦伦特（Leslie Valiant）教授介绍了他对计算机科学的独特观点，并回顾了他的研究历程。瓦伦特教授是机器学习的鼻祖。上世纪七八十年代，人工智能还是以构建专家系统为主。专家系统的思想就是通过建立大量规则来指导计算机推理，但很快便发现人工建立规则是一件非常艰难的任务。当研究人员一筹莫展时，瓦伦特教授提出让计算机自己学习规则的思想，成为数据挖掘和机器学习奠基性的工作。

机器学习并不是我的研究领域，所以了解并不多。但瓦伦特教授的报告充满了想象力，给我很多联想和启发。他认为图灵不仅仅是一位数学家、计算机科学家，更像是一位自然科学家，而计算机科学也可看作是一门自然科学。他在幻灯片上摘出了图灵1948年的论文《智能机器》（Intelligent Machinery）中一段话，“… genetical or evolutionary search by which a combination of genes is looked for, the criterion being survival value.”，然后说图灵所思考的已经超越了计算机科学，可以归到自然科学范畴了。报告中，他又说道其实机器学习的必要性和意义图灵早就在1948年就指出来了，许多听众感到有些茫然。只见瓦伦特教授翻到一页幻灯片，又摘出了图灵那篇《智能机器》 中的一段文字，其中有这么一句话“the learning of languages would be the most impressive”。瓦伦特教授稍加解读，众人顿时恍然大悟，不禁感慨图灵真如神一般高不可及，而学术大师们则像神父一样能读懂神的思想，向世人传达神的指示。

瓦伦特教授的报告中提到好几个有趣的定义，比如什么是学习，什么是进化。这些高度抽象的概念，瓦伦特教授却能用数学进行漂亮的形式化定义，令人叹为观止。很多难题无从下手时，正是因为问题没有定义清楚，而巧妙的定义经常另辟蹊径，帮助人们找到解决问题的关键。有个笑话从反面诠释了定义的能量。一位哲学教授将一把椅子提到讲台上，对学生们说，今天哲学课考试题目是–证明这把椅子不存在。学生们开始冥思苦想，但只过五分钟有位学生即交卷了。教授一看，答卷上只有五个字，但连声称绝，打了满分。这五个字是——＂什么是椅子？＂

这让我联想起在普林斯顿时与李凯教授的一次讨论。当时，我们希望对比两个程序行为是否相似，这听起来也是一个无从下手的问题。于是李凯教授让我先去定义“什么是程序行为？、“什么是相似？”当我把这些问题定义清楚后，解决思路就明确了。这次经历也让我深刻体会到只有将问题定义的越清晰，才能找到明确的解决方法。

如果说好的定义是解决问题的关键，那伟大的定义往往开辟新的领域。这样的例子在计算机科学发展史上比比皆是。除了瓦伦特教授定义了什么是学习开创机器学习领域外，还有图灵用图灵机定义了什么是可计算，开创了整个计算科学领域；香农（Claude Shannon）通过不确定的概率定义了什么是信息，开创了信息论；里维斯特（Ron Rivest）等通过概率上的不可区分性（indistinguishability）定义了什么是安全，开创了计算机时代的安全领域。

4. 互联的未来
纪念活动的高潮是普林斯顿校友，Google前CEO、现Google董事会主席斯密特（Eric Schmit）的报告，可容纳400人的报告厅座无虚席，甚至有人坐在台阶上。

斯密特报告的主题是未来，他给现场听众描绘了一幅美好的未来蓝图。未来智能手机将越来越便宜，如今已经有几十美元的Andriod手机了。未来的市场主要会在发展中国家，如今中国、印度每年智能手机都是以几千万的速度在增长，而非洲国家也会成为新兴市场。未来将会有30亿新网民加入到互联网，这蕴含着巨大的应用需求，同时也带来巨大的创造力。斯密特还畅想了一系列新兴应用，比如无人驾驶汽车、穿戴式设备等。

报告结束后留了半个多小时提问，大家非常踊跃。有人问Google是否能帮助设立诺贝尔计算奖，Google的数字货币计划是什么，未来该如何学习快速发展的技术，互联世界和现实世界的区别，Google在如何帮助发展中国家，还有人提问请斯密特给本科生一些建议…… 我也起身问了一个关于Google X实验室的问题，并开玩笑式的问怎么才能进Google X实验室。斯密特说，有人泄露Google X的信息，Google X实验室细节仍然是机密，所以他可以透露无人驾驶汽车项目，但不能再说更多其他的项目，不过请想象一下Google X的研究人员正在整合计算机科学、硬件和新设备，那也许会对Google X有一些感觉。事实上，Google X确实很秘密，存在好多年而不为人所知，即使是Google员工。直到2011年11月纽约时报泄露有关信息，外界才得以了解。Google X项目都是非常激进，比如无人驾驶车、Google 眼镜、机器人巡逻队、甚至太空电梯。上期CCCF刊登的CACM译文《谷歌的混合研究方法》（Google’s Hybrid Approach to Research）中提到工程与研究并重的混合研究模式会更倾向于低风险的短期项目，而专注长远影响的Google X实验室则是对混合模式的补充。

斯密特提到的很多观点和我最近读的戴曼迪斯（Peter Diamandis）的《Abundance：The Future Is Better Than You Think》一书中很多观点一致。事实上，斯密特和戴曼迪斯本来就是私交很好的朋友，他们甚至最近和Google的创始人佩奇（Larry Page）、《阿凡达》导演卡梅隆（James Cameron）一起宣布创办了Planetary Resources公司，目标是太空采矿！

斯密特和戴曼迪斯对未来的判定并不是凭空臆想。如果跳出某项具体技术，从更广阔的时空来观察技术本身的发展，就会发现技术发展也有规律。比如，笔者之前在CCCF上刊登的《谁推动信息产业发展》文章中引用了美国科学院的一份报告，该报告分析了19个计算机技术的发展史，从而得出基础研究与产业化互动的一些规律。而《Abundance》一书给读者呈现了另一条有趣的规律——产生巨大影响的技术都是指数发展型技术（Exponential Technologies）。

在科技史上有很多成功利用这条规律预测未来的例子。例如1953年美国空军分析了从1911年飞机发明到1953年之间飞机加速技术发展曲线，发现飞行器发动机的加速度增长是指数发展的，并预测1970年左右人类便能登上月球。这个判断是在1953年做出来的，这在当时是难以想象的，因为最乐观的估计也认为登上月球至少还需要50年（2000年左右）。

而摩尔定律是计算机领域都熟知的另一个例子。1965年摩尔（Godern Moore）在一篇文章中用1959年到1965年的5个点画出了一条直线，并成功预测未来10年（到1975年）半导体技术的发展趋势，即单个芯片晶体管数目将每12个月翻一番（后来修正为每18个月）。一个又一个十年过去了，摩尔定律在过去的50年里都有效，并还会持续到至少2020年。

从技术层面上去判断一项技术是否为指数型技术需要极远的眼界和很深的造诣，往往只有摩尔这样的大师才能做到。我的一个观点是，技术的成本也许是一个简单有效的判断依据，即在相同的性能下价格是否在不断下降，或在相同的价格下性能是否在不断提高？当然技术的潜力还依赖于市场饱和度。所以，综合技术成本和市场饱和度两方面的因素来看，智能手机和互联网确实还有很大的潜力，尤其是中国广大的农村市场和其他发展中国家。

5. 结语
2012年即将过去，世界各地的图灵纪念活动也都逐渐落下帷幕。这些纪念活动让我们这些和图灵本没有时空交集的晚辈也能感受那个造就伟大图灵的时代，这是一个伟大的时代，希尔伯特，邱奇、哥德尔、冯诺依曼……
那我们所处的时代是伟大的时代吗？图灵知道他所处的时代是伟大的吗？图灵已逝，我们不得而知。但我有一个猜想，也许哥德尔不完备定理的第二点（公理系统的一致性不能在其内部被证明）也适用于历史系统——历史舞台上的扮演者无法证明自己所处的时代是伟大的。

分享

分享

[编者注：Gernot 的这篇 blog 介绍了一些 NICTA 和 OK-lab 的故事。关于，NICTA 和 OK-lab 的来历，读者如果感兴趣，可以阅读我以前写的这篇文章 General Dynamics 收购 Open Kernel Labs (OK Labs). Gernot 在这篇博客中说到高通最早和 NICTA 合作的时候有两个需求, 一个是需要一个有内存隔离的，实时的，高速内核。另一个是这个内核可以在 ARM 上虚拟化 Linux。 ERTOS (Gernot 的 group) 当时作的 L4 正好满足这个需求，而且L4 是开源的。 随着 高通和 NICTA 合作的规模扩大， NICTA 作为一个研究机构， 已经不能，也不应该提供相应的服务，这个时候，NICTA spin-off OK-lab 出去去作 okl4 的商业化工作。 NICTA 继续作 sel4 的研究工作。 当 sel4 研究工作接近结束的时候，又可以利用 OK-lab 来商业化。这样就形成了一个正反馈的系统。]

原文来自 http://microkerneldude.wordpress.com/2012/10/02/giving-it-away-part-2-on-microkernels-and-the-national-interes/

阅读全文»

分享

分享

不知道多少人见过这本书的封面，不知道多少人从这本书开始折腾操作系统。大家管这本书叫 Lions book. 书的作者，John Lions 98 年去世. 他把 UNIX 介绍到澳大利亚，建立第一个 UNIX Group。在这本书的基础上，他在 UNSW 开了第一个真刀真枪干操作系统的课程。在96年之前，这本书只能在地下流传，但是人手一本。

2006 年，UNSW 的 Alumni 在 UNSW 设立了一个 title， John Lions Chair of Operating Systems. Prof. Gernot Heiser,  OK Labs 的 founder, 成了第一个 Chair. 91 年 DiSy group 建立, Gernot 带着两个 PhD students 开始和 Jochen Liedtke (L4的设计人）合作，把 L4 带到 澳大利亚，开了 Advanced Operating System 的课程。 这门课从 97 年开始带出了一批能 hack kernel 的学生。 比如这篇 thesis, Single Kernel Stack L4, 就是出于一名本科生，相关的代码运行在 okl4 中。

2002 年，NICTA 建立，这个机构的宗旨就是鼓励研究人员把研究成果商业化。Gernot 等在 NICTA 建立了 ERTOS group. 2006 年，OK Labs 这个 startup 正式建立，公司的主力正是这门课程中发现和培训出的学生们。OK Labs 主要卖基于 okl4 kernel 的操作系统，提供 安全 和 高性能虚拟化。 最早是跑在高通的基带芯片里边，我猜测是高通的遗留代码太大且不好改，所以可以在 okl4 上跑高通自己的 RTOS, 然后遗留代码继续跑在 RTOS 上边。爱立信，摩托罗拉等也采用过 OK Labs 的产品。现在有10几亿台设备中在跑 okl4.  有一次，我的 supervisor 和  NICTA 的人聊天，说起了他们这个最成功的 startup, NICTA 的人拿出 ipad2, 打开 copyright 部分，然后翻啊翻，翻啊翻，终于找到了 okl4 。

兵分两路，商业化 okl4 的同时， ERTOS 进行着一个大胆的 research project,  L4.verified, 证明操作系统的正确性 (证明 L4 的实现是和 specification 一致的），就是说 在一定的前提下，这个 kernel 的实现是 bug free的。他们的论文, seL4: Formal verification of an OS kernel, 也获得了 SOSP 09 年的 best paper. 现在他们也在致力于把这些工作商业化。这个 Group 也从一开始 一个 faculty, 两个 phd students 的组变成了超级大组。

除了 mobile phone 领域, OK Labs 一直给 military 方面的公司做项目。同时他们也在做汽车上整个系统的虚拟化工作。最终，这个公司被 General Dynamics 收购。

在21世纪，折腾一个只卖操作系统的公司，还能活下来，卖出去，我觉得是个了不起的事情。尤其是在澳大利亚，这个没有硅谷的地方。

这一切的开始，就是 Prof. John Lions 和 他的书。愿大宋的教授能有此心。

分享