函数式编程的另类指南(3)

By | September 8, 2013

The following part is not maintained anymore. Please go to 函数式程序设计的另类指南 for the whole translation.

以下内容不再更新,浏览全部翻译,请访问 函数式程序设计的另类指南


原文链接:Functional Programming For The Rest of Us
原文作者:Vyacheslav Akhmechet

历史一瞥

再次启动时间机器,这次我们回到二十世纪30年代。大萧条正在蹂躏着那个新旧交替的时代。空前的经济下滑影响着几乎所有阶层的家庭。只有少数人还能够保持着饥谨危机前的安逸,比如普林斯顿大学的数学家们。

歌特式的新办公室给普林斯罩上天堂般的幸福光环。来自世界各地的逻辑学家被邀请到此成立一个新学部。那时的美国民众已很难弄到一块面包,但是在普林斯顿,你可以在高高的穹顶下、精致雕凿的木质墙饰边,整日的品茶讨论,或在楼外的林荫中款款慢步。

阿隆左·丘奇(Alonzo Church)就是其中一位享受这种近于奢华的数学家。他在普林斯顿获得本科学位后被邀继续留在研究生院攻读。阿隆左认为普林斯顿的建筑过于浮华,所以他很少一边喝茶一边与人讨论数学,他也不喜欢到林中散步。他有些孤僻,因为似乎只有一个人时他才能以最高的效率工作。尽管如此,他仍与另一些同样居住在普林斯顿的人保持着联系,比如阿兰·图灵(Alan Turing),约翰·冯·诺依曼(John von Neumann),和库尔特·冈特(Kurt Gödel)。

这四个人都对形式系统很感兴趣。他们致力于解决抽象的数学难题,而不太留意现实的世界。这些难题的共同之处就是计算:如果计算机能有无限的计算能力,哪些问题可以被解决?哪些问题可以被自动解决?哪些问题依旧无法解决?为什么不能被解决?基于不同设计的各种计算机是否具有相同的计算能力?

通过和其它人的合作,阿隆左·丘奇提出了一个被称为lambda演算的形式系统。这个系统本质上是一种程序设计语言。它可以运行在具有无限计算能力的机器上。lambda演算由一些函数构成,这些函数的输入输出也是函数。函数用希腊字母lambda标识,因此整个形式系统也叫lambda。通过这一形式系统,阿隆左就可以对上述诸多问题进行推理并给出结论性的答案。

在同一时间,阿兰·图灵也在进行着相似的工作。他提出了一个完全不同的形式系统(现在被称为图灵机),并使用这一系统得出了和阿隆左相似的结论。事后证明,图灵机和lambda的演算能力是等价的。

我们的故事本可到此结束。如果第二次世界大战没有在那时打响,我现在就可以歇笔,而你也可以浏览下一个页面了。那时整个世界笼罩在战争的火光和硝烟之中,美国陆军和海军大量使用炮弹。为了改进炮弹的精确度,部队雇佣了大批数学家通过计算微分方程来给出弹道发射的轨迹。很显然这项工作人力浩繁,因此人们开始着手开发各种设备来攻克这个难关。第一个解出了弹道轨迹的机器是IBM的Mark I——它重达5吨,有75万个部件,每秒可以完成三次操作。

竞争当然没有就此结束。1949年,EDVAC(Electronic Discrete Variable Automatic Computer)被推出并获得了巨大的成功。这是冯·诺依曼架构的第一个具体实现,实际上也是图灵机的第一个实现。而与此同时,阿隆左·丘奇则没有那么幸运。

二十世纪五十年代,一位MIT的教授John McCarthy(也是普林斯顿毕业生)对阿隆左·丘奇的工作产生了兴趣。1958年,他发布了Lisp语言(List Processing language)。Lisp的不同之处在于,它在冯·诺依曼计算机上实现了阿隆左·丘奇的lambda演算!很多计算机科学家开始意识到Lisp的表达能力。1973年,MIT人工智能实验室的一帮程序员开发了被称为Lisp机器的硬件,于是阿隆左的lambda演算系统终于在硬件上实现了!

Leave a Reply

Your email address will not be published. Required fields are marked *