## 历史回眸
再次启动时间机……这次到达的是20世纪30年代，离今天近了很多。无论[新](http://zh.wikipedia.org/wiki/%E6%96%B0%E5%A4%A7%E9%99%B8)[旧](http://zh.wikipedia.org/wiki/%E8%88%8A%E5%A4%A7%E9%99%B8)大陆，经济大萧条都造成了巨大的破坏。社会各阶层几乎每一个家庭都深受其害。只有极其少数的几个地方能让人们免于遭受穷困之苦。几乎没有人能够幸运的在这些避难所里度过危机，注意，我说的是几乎没有，还真的有这么些幸运儿，比如说当时普林斯顿大学的数学家们。
新建成的哥特式办公楼给普林斯顿大学带来一种天堂般的安全感。来自世界各地的逻辑学者应邀来到普林斯顿，他们将组建一个新的学部。正当大部分美国人还在为找不到一片面包做晚餐而发愁的时候，在普林斯顿却是这样一番景象：高高的天花板和木雕包覆的墙，每天品茶论道，漫步丛林。 一个名叫[阿隆佐·邱奇](http://zh.wikipedia.org/zh/%E9%98%BF%E9%9A%86%E4%BD%90%C2%B7%E9%82%B1%E5%A5%87)(Alonzo Church)的年轻数学家就过着这样优越的生活。阿隆佐本科毕业于普林斯顿后被留在研究院。他觉得这样的生活完全没有必要，于是他鲜少出现在那些数学茶会中也不喜欢到树林里散心。阿隆佐更喜欢独处：自己一个人的时候他的工作效率更高。尽管如此他还是和普林斯顿学者保持着联系，这些人当中有[艾伦·图灵](http://zh.wikipedia.org/zh/%E8%89%BE%E4%BC%A6%C2%B7%E5%9B%BE%E7%81%B5)、[约翰·冯·诺伊曼](http://zh.wikipedia.org/zh/%E7%BA%A6%E7%BF%B0%C2%B7%E5%86%AF%C2%B7%E8%AF%BA%E4%BC%8A%E6%9B%BC)、[库尔特·哥德尔](http://zh.wikipedia.org/zh-hant/%E5%BA%93%E5%B0%94%E7%89%B9%C2%B7%E5%93%A5%E5%BE%B7%E5%B0%94)。
这四个人都对形式系统感兴趣。相对于现实世界，他们更关心如何解决抽象的数学问题。而他们的问题都有这么一个共同点：都在尝试解答关于计算的问题。诸如：如果有一台拥有无穷计算能力的超级机器，可以用来解决什么问题？它可以自动的解决这些问题吗？是不是还是有些问题解决不了，如果有的话，是为什么？如果这样的机器采用不同的设计，它们的计算能力相同吗？
在与这些人的合作下，阿隆佐设计了一个名为[lambda演算](http://zh.wikipedia.org/wiki/%CE%9B%E6%BC%94%E7%AE%97)的形式系统。这个系统实质上是为其中一个超级机器设计的编程语言。在这种语言里面，函数的参数是函数，返回值也是函数。这种函数用希腊字母lambda（[λ](http://en.wikipedia.org/wiki/Lambda)），这种系统因此得名4。有了这种形式系统，阿隆佐终于可以分析前面的那些问题并且能够给出答案了。
除了阿隆佐·邱奇，艾伦·图灵也在进行类似的研究。他设计了一种完全不同的系统（后来被称为[图灵机](http://zh.wikipedia.org/zh/%E5%9B%BE%E7%81%B5%E6%9C%BA)），并用这种系统得出了和阿隆佐相似的答案。到了后来人们证明了图灵机和lambda演算的能力是一样的。
如果二战没有发生，这个故事到这里就应该结束了，我的这篇小文没什么好说的了，你们也可以去看看有什么其他好看的文章。可是二战还是爆发了，整个世界陷于火海之中。那时的美军空前的大量使用炮兵。为了提高轰炸的精度，军方聘请了大批数学家夜以继日的求解各种差分方程用于计算各种火炮发射数据表。后来他们发现单纯手工计算这些方程太耗时了，为了解决这个问题，各种各样的计算设备应运而生。IBM制造的Mark一号就是用来计算这些发射数据表的第一台机器。Mark一号重5吨，由75万个零部件构成，每一秒可以完成3次运算。
战后，人们为提高计算能力而做出的努力并没有停止。1949年第一台电子离散变量自动计算机诞生并取得了巨大的成功。它是[冯·诺伊曼设计架构](http://zh.wikipedia.org/zh/%E5%86%AF%C2%B7%E8%AF%BA%E4%BC%8A%E6%9B%BC%E7%BB%93%E6%9E%84)的第一个实例，也是一台现实世界中实现的图灵机。相比他的这些同事，那个时候阿隆佐的运气就没那么好了。
到了50年代末，一个叫John McCarthy的MIT教授（他也是普林斯顿的硕士）对阿隆佐的成果产生了兴趣。1958年他发明了一种列表处理语言（Lisp），这种语言是一种阿隆佐lambda演算在现实世界的实现，而且它能在冯·诺伊曼计算机上运行！很多计算机科学家都认识到了Lisp强大的能力。1973年在MIT人工智能实验室的一些程序员研发出一种机器，并把它叫做Lisp机。于是阿隆佐的lambda演算也有自己的硬件实现了！
