backup

作者：王垠

介绍一下我的研究方向吧。我的领域叫“程序语言”(programming languages)。世界上只有很少数人真正在做这方面的研究，所以很少有人理解这个专业是干什么的，就连我身边的朋友同学也几乎不知道。但是其实这是一个非常重要的领域。在我看来，它就是计算机科学的精髓所在。

程序语言的研究不是针对某一种语言，而是针对所有语言。它是一种基础性，普适性的研究。它专注于理解程序语言的本质，设计更为简单，合理和高效的语言，而不只是改进已有的语言。

从广义一点的角度来说，程序语言研究的东西其实是计算的本质。计算都需要基于某种“计算模型”，而程序语言就是用来描述这种计算模型的符号系统，所以程序语言跟计算的本质非常接近。其实，早期的程序语言研究直接导致了计算机科学的诞生。它的历史可以追溯到20世纪30年代甚至更早。最早的时候产生这个想法是因为人们想给数学提供一个可靠的“基础”(foundation of mathematics)。之前对数学的描述都使用一些稀奇古怪的数学记号，夹杂一些自然语言。这是非常脆弱，不可靠，而且难于理解的。不小心看错一个句子，你可能就会接受一个错误的证明，或者无法验证一个正确的证明。而且数学记号的设计也缺乏一致性，导致学习的障碍。所以有人就提出了这样的想法，想让数学的描述和证明完全的机械化，这样人就可以用机器，而不是用自己的脑子去验证证明的正确性。这就像现在大家都用计算器来做算术一样，基本不需要动脑筋。所以这个领域最早就是致力于帮助数学家偷懒的。

我每天都使用的一个概念叫 lambda calculus。它是一种非常简单的符号系统，可是几乎所有程序语言的所有构造，都可以用它来表示。通常当程序语言的构造被 lambda calculus 表示之后，问题就会变得清晰明了很多，甚至迎刃而解。这个东西是在1930年代由逻辑学家 Alonzo Church 发明的。Church 有很多学生，包括通常被认为是计算机科学鼻祖的图灵(Alan Turing)。当时还有其他一些重要的人物，比如 Church 的另外一个学生 Stephen Kleene。Lambda calculus 以及由它衍生出来的一些新的系统（比如 Martin-Löf 类型理论），构成了当今直觉主义逻辑 (intuitionistic logic) 的主要内容。

有人也许会觉得这种基础性的研究没有应用前景。确实，有些基础性的研究是扯淡，是不能应用的，但是其它一些却有很大的应用前景。举一个切身体会的例子就是我在 Google 实习的时候给他们做的一个东西。他们需要为 Python 做一个可以像 Eclipse 一样能够精确跳转到定义的工具。因为 Python 是动态类型的，所以这个工作的难度比起 Java 这样的静态类型语言来说要大很多。我的 manager (Steve) 本来打算让我去拿一个开源的软件比如 PyDev 来改一改，可是我发现这些软件都不能正确的跳转到定义，所以我打算从头设计一个静态分析系统。当我提出这个想法的时候，Steve 非常的担心。他觉得这是在12个星期的实习期内不可能完成的事情，因为通常来说这种东西需要一个团队好几年的工作。比如 Steve 告诉我，Google 的 JS Compiler（开源之后叫做 closure compiler)，花费了他们一个小组四年时间才完成，光是处理符号表的代码就有9000多行。但是我没有被他吓倒，我知道自己受到过什么样的训练。所以我在一个周末的时间内设计实现了这个系统的原型，让他相信我是有能力做出这个系统的。在12个星期之内，我完全的实现了这个系统。最后整个系统的代码，包括空行和注释在内，才仅仅4000行。其中处理符号表的部分只有600行（9000的15分之1）。而在这之前，我对 Python 语言的了解几乎为零。能做出这个东西是因为我对程序语言的一种本质性的理解，让我能够迅速的看清 Python 的语义，从而实现一个针对 Python 的抽象解释器 (abstract interpreter)，在某种程度上说也就是实现了 Python 语言。我也可以为任何一个其它的语言做同样的事情。现在，Google 每天都用这个工具处理它所有的 Python 代码，生成可精确跳转到定义的索引。

这个例子并不是程序语言研究最高精尖的应用。很多研究程序语言的人也进行一些程序验证和机器定理证明研究。简而言之，程序验证就是用机械化的逻辑来证明程序的正确性。这种证明与通常的单元测试(unit test)很不一样，在于它能 100% 的保证程序的正确，而测试的方法几乎总是会漏掉一些情况。这种研究在关键性的领域很有应用，比如航空航天，核电，武器，芯片设计等等。因为没有任何人愿意因为程序出错而坠毁一架飞机或者发射一颗核弹，所以他们愿意花很大的工夫保证控制程序的绝对正确。Intel的浮点运算bug当年导致好几亿美元的经济损失，所以在那以后很多芯片厂商都开始使用定理证明程序（比如 ACL2）来彻底的消灭某些芯片模块里可能存在的bug。这些定理证明程序里面的关键部分，就是程序语言的一些重要理论。当然必须指出，程序的很多性质是不可证明的，所以很多时候测试还是有必要的。

有些定理证明程序（比如 Coq，Isabelle, HOL）已经开始被应用于数学的证明。最著名的例子就是四色定理，被人重新用 Coq 证明了一次，从而完全的确保这个定理的正确性。有些数学家也开始使用这些工具。比如 Thomas Hales，他当年证明了开普勒猜想 (Kepler conjecture)，提交了一份 250 页的论文（外加 3GB 的程序，数据和结果）给数学界的权威期刊 Annals of Mathematics。经过一个由 12 位数学家组成的评委四年的验证工作，没能完全确定证明的正确性。虽然论文最后还是发表了，但是被评委们添了一行注释：“我们只有 99% 的把握相信他的证明。”这使得这个证明几乎完去了数学的意义。所以 Thomas Hales 很恼火，最后决定用一种机器定理证明程序来重新证明开普勒猜想。

其它重要的应用真是举不胜举。其实这个领域对我最重要的吸引力是它的思维方式。它让我透过现象看到本质，从而能够从根本上解决问题。至于我自己，故事还真多。在教授们的指导下，我做过各种各样有趣的东西，从逻辑式语言(logic programming)到编译器。现在我比较感兴趣的东西是类型系统 (type system)，supercompilation，自动定理证明和并行语言设计。我也利用程序语言的知识来思索其它领域的东西，或者做别的好玩的东西。具体的我以后再慢慢介绍。