阿隆佐·丘奇与λ演算系统

历史一瞥

再次启动时间机器，这一次的旅行近了很多，我们回到 1930 年代。大萧条正在蹂躏着这个半新不旧的时代。空前的经济下挫影响着几乎所有阶层的家庭生活，只有少数人还能够保持着饥谨危机前的安逸。一些人就如此幸运地位列其中，我们关心的是普林斯顿大学的数学家们。

采用了歌特式风格设计建造的新办公室给普林斯顿罩上天堂般的幸福光环，来自世界各地的逻辑学家被邀请到普林斯顿建设一个新的学部。虽然彼时的美国民众已很难弄到一餐面包，普林斯顿的条件则是可以在高高的穹顶下，精致雕凿的木质墙饰边上整日的品茶讨论或款款漫步于楼外的林荫之中。

阿隆佐·丘奇就是一个在这种近于奢侈的环境中生活着的数学家。他在普林斯顿获得本科学位后被邀留在研究生院继续攻读。阿隆佐认为那里的建筑实属浮华，所以他很少一边喝茶一边与人讨论数学，他也不喜欢到林中散步。

阿隆佐是一个孤独者：因为只有一个人时他才能以最高的效率工作。虽然如此，他仍与一些普林斯顿人保持着定期联系，其中包括阿伦·图灵、约翰·冯·诺依曼和库尔特·哥德尔。

这四个人都对形式系统很感兴趣，而不太留意现实世界，以便致力于解决抽象的数学难题。他们的难题有些共同之处：都是探索关于计算的问题。如果我们有了无限计算能力的机器，哪些问题可以被解决？我们可以使他们自动地得以解决吗？是否还是有些问题无法解决？为什么？不同设计的各种机器是否具有相同的计算能力？

通过和其它人的合作，阿隆佐·丘奇提出了一个被称为 λ 演算（lambda calculus）的形式系统。这个系统本质上是一种虚拟的机器的编程语言，他的基础是一些以函数为参数和返回值的函数。函数用希腊字母 λ 标识，这个形式系统因此得名。利用这一形式系统，阿隆佐就可以对上述诸多问题推理并给出结论性的答案。

独立于阿隆佐，阿伦·图灵也在进行着相似的工作，他提出了一个不同的形式系统（现在被称为图灵机），并使用这一系统独立地给出了和阿隆佐相似的结论。后来人们证明图灵机和 λ 演算能力等同。

如果第二次世界大战没有在那时打响，我们的故事本可以到此结束，我会就此歇笔，而你也将浏览到下一个页面。彼时整个世界笼罩在战争的火光和硝烟之中，美国陆军和海军前所未有的大量使用炮弹，为了改进炮弹的精确度，部队组织了大批的科学家持续地计算微分方程以解出弹道发射轨迹。在渐渐意识到这个任务用人力手工完成太耗精力后，人们开始着手开发各种设备来攻克这个难关。第一个解出了弹道轨迹的机器是 IBM 制造的 Mark I，它重达 5 吨，有 75 万个组件，每秒可以完成三次操作。

竞争当然没有就此结束，1949 年，EDVAC（Electronic Discrete Variable Automatic Computer，爱达瓦克）推出并获得了极大的成功。这是对冯·诺依曼架构的第一个实践实例，实际上也是图灵机的第一个现实实现。那一年开始好运与阿隆佐·丘奇无缘。

直到 1950 年代将尽，一位 MIT 的教授 John McCarthy（也是普林斯顿毕业生）对阿隆佐·丘奇的工作产生了兴趣。1958年，他公开了表处理语言 Lisp。Lisp 是对阿隆佐·丘奇的 λ 演算系统的实现，但同时它工作在冯·诺依曼计算机上！很多计算机科学家认识到了 Lisp 的表达能力。1973 年，MIT 人工智能实验室的一组程序员开发了被称为 Lisp 机器的硬件－阿隆佐 λ 演算的硬件实现！