## 歷史回眸
再次啟動時間機……這次到達的是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演算也有自己的硬件實現了！
