丘奇和圖靈

丘奇（Alonzo Church）和圖靈（Alan Turing）是兩位對計算機科學具有最大影響力的人物，然而他們卻具有非常對立的觀點和相差很多的名氣。在我長達16年的計算機科學生涯中，總是感覺到自己的思想反反復復的徘徊于這兩個“陣營”之間。丘奇代表了“邏輯”和“語言”，而圖靈代表著“物理”和“機器”。在前面的8年中，我對丘奇一無所知，而在后面的8年中，我卻很少再聽到圖靈的名字。他們的觀點誰對誰錯，是一個無法回答的問題。完全投靠丘奇，或者完全投靠圖靈，貌似都是錯誤的做法。這是一種非常難說清楚的，矛盾的感覺，但是今天我試圖把自己的感悟簡要的介紹一下。

丘奇與圖靈之爭

想必世界上所有的計算機學生都知道圖靈的大名和事跡，因為美國計算機器學會（ACM）每年都會頒發(fā)“圖靈獎”，它被譽為計算機科學的最高榮譽。大部分的計算機學生都會在某門課程（比如“計算理論”）學習“圖靈機”的原理。然而，有多少人知道丘奇是什么人，他做出了什么貢獻，他與圖靈是什么樣的關系呢？我想恐怕不到一半的人吧。

如果你查一下數(shù)學家譜圖，就會發(fā)現(xiàn)丘奇其實是圖靈的博士導師。然而從 Andrew Hodges 所著的《圖靈傳》，你卻可以看到圖靈的心目中仿佛并沒有這個導師，仿佛自己的“全新發(fā)明”應得的名氣，被丘奇搶走了一樣（注意作者的用詞：robbed）。事實到底是怎樣的，恐怕誰也說不清楚。我只能說，貌似計算機科學從誕生之日開始就充滿了各種“宗教斗爭”。

雖然現(xiàn)在圖靈更加有名，然而在現(xiàn)實的程序設計中，卻是丘奇的理論在起著絕大部分的作用。據(jù)我的經(jīng)驗，丘奇的理論讓很多事情變得簡單，而圖靈的機器卻過度的復雜。丘奇所發(fā)明的 lambda calculus 以及后續(xù)的工作，是幾乎一切程序語言的理論基礎。而根據(jù)老一輩的計算機工程師們的描述，最早的計算機構架也沒有受到圖靈的啟發(fā)，那是一些電機工程師完全獨立的工作。然而有趣的是，繼承了丘奇衣缽的計算機科學家們拿到的那個大獎，仍然被叫做“圖靈獎”。我粗略的算了一下，在迄今所有的圖靈獎之中，程序語言的研究者占了近三分之一。

從圖靈機到 lambda calculus

圖靈機永遠的停留在了理論的領域，絕大多數(shù)被用在“計算理論”（Theory of Computation）中。計算理論其實包括兩個主要概念：“可計算性理論”（computability）和“復雜度理論”(complexity）。這兩個概念在通常的計算理論書籍（比如 Sipser 的經(jīng)典教材）里，都是用圖靈機來敘述的。在學習計算理論的時候，絕大多數(shù)的計算機學生恐怕都會為圖靈機頭痛好一陣子。

然而在做了研究生“計算理論”課程一個學期的 TA 之后我卻發(fā)現(xiàn)，其實幾乎所有計算理論的原理，都可以用 lambda calculus，或者程序語言和解釋器的原理來描述。所謂“通用圖靈機”（Universal Turing Machine），其實就是一個可以解釋自己的解釋器，叫做“元解釋器”（meta-circular interpreter）。在 Dan Friedman 的 B621 程序語言理論課程中，我最后的項目就是一個 meta-circular interpreter。這個解釋器能夠完全的解釋它自己，而且可以任意的嵌套（也就是說用它自己來解釋它自己，再來解釋它自己……）。然而我的“元解釋器”卻是基于 lambda calculus 的，所以我后來發(fā)現(xiàn)了一種方法，可以完全的用 lambda calculus 來解釋計算理論里面幾乎所有的定理。

我為這個發(fā)現(xiàn)寫了兩篇博文：《A Reformulation of Reducibility》和《Undecidability Proof of Halting Problem without Diagonalization》。我把 Sipser 的計算理論課本里面的幾乎整個一章的證明都用我自己的這種方式改寫了一遍，然后講給上課的學生。因為這種表示方法比起通常的“圖靈機+自然語言”的方式簡單和精確，所以收到了相當好的效果，好些學生對我說有一種恍然大悟的感覺。

我把這一發(fā)現(xiàn)告訴了我當時的導師 Amr Sabry。他笑了，說這個他早就知道了。他推薦我去看一本書，叫做《Computability and Complexity from a Programming Perspective》，作者是大名鼎鼎的 Neil Jones (他也是“Partial Evaluation”這一重要概念的提出者）。這本書不是用圖靈機，而是一種近似于 Pascal，卻又帶有 lambda calculus 的一些特征的語言（叫做 “WHILE 語言”）來描述計算理論。用這種語言，Jones 不但輕松的證明了所有經(jīng)典的計算理論定理，而且能夠證明一些使用圖靈機不能證明的定理。

我曾經(jīng)一直不明白，為什么可以如此簡單的解釋清楚的事情，計算理論需要使用圖靈機，而且敘述也非常的繁復和含糊。由于這些證明都出于資深的計算理論家們之手，讓我不得不懷疑自己的想法里面是不是缺了點什么?？墒窃诳吹搅?Jones 教授的這本書之后，我倍感欣慰。原來一切本來就是這么的簡單！

后來從 CMU 的教授 Robert Harper 的一篇博文《Languages and Machines》中，我也發(fā)現(xiàn) Harper 跟我具有類似的觀點，甚至更加極端一些。他強烈的支持使用 lambda calculus，反對圖靈機和其他一切機器作為計算理論的基礎。

從 lambda calculus 到電子線路

當我在 2012 年的 POPL 第一次見到 Neil Jones 的時候，他跟我解釋了許多的問題。當我問到他這本書的時候，他對我說：“我不推薦我的書給你，因為大部分的人都覺得 lambda calculus 難以理解?！盠ambda calculus 難以理解？我怎么不覺得呢？我覺得圖靈機麻煩多了。然后我才發(fā)現(xiàn)，由于經(jīng)過了這么多年的研究之后，自己對 lambda calculus 的理解程度已經(jīng)到了深入骨髓的地步，所以我已經(jīng)全然不知新手對它是什么樣的感覺。原來“簡單”這個詞，在具有不同經(jīng)歷的人頭腦里，有著完全不同的含義。

所以其實 Jones 教授說的沒錯，lambda calculus 也許對于大部分人來說不合適，因為對于它沒有一個好的入門指南。Lambda calculus 出自邏輯學家之手，而邏輯學家們最在行的，就是把很簡單的“程序”用天書一樣的公式表示出來。這難怪老一輩的邏輯學家們，因為他們創(chuàng)造那些概念的時候，計算機還不存在。但是如果現(xiàn)在還用那一堆符號，恐怕就有點落伍了。大部分人在看到 beta-reduction, alpha-conversion, eta-conversion, ... 這大堆的公式的時候，就已經(jīng)頭痛難忍了，怎么還有可能利用它來理解計算理論呢？

其實那一堆符號所表示的東西，終究超越不了現(xiàn)實里的物體和變化，最多不過再幻想一下“多種未來”或者“時間機器”。有了計算機之后，這些符號公式，其實都可以用數(shù)據(jù)結構和程序語言來表示。所以 lambda calculus 在我的頭腦里真的很簡單。每一個 lambda 其實就像是一個電路模塊。它從電線端子得到輸入，然后輸出一個結果。你把那些電線叫什么名字根本不重要，重要的是同一根電線的名字必須“一致”，這就是所謂的“alpha-conversion”的原理…… 不在這里多說了，如果你想深入的了解我心目中的 lambda calculus，也許可以看看我的另一篇博文《怎樣寫一個解釋器》，看看這個關于類型推導的幻燈片的開頭，或者進一步，看看如何推導出 Y combinator，或者看看《What is a program?》。你也可以看看 Matthias Felleisen 和 Matthew Flatt 的《Programming Languages and Lambda Calculi》。

所以，也許你看到了在我的頭腦里面并存著丘奇和圖靈的影子。我覺得丘奇的 lambda calculus 是比圖靈機簡單而強大的描述工具，然而我卻又感染到了圖靈對于“物理”和“機器”的執(zhí)著。我覺得邏輯學家們對 lambda calculus 的解釋過于復雜，而通過把它理解為物理的“電路元件”，讓我對 lambda calculus 做出了更加簡單的解釋，把它與“現(xiàn)實世界”聯(lián)系在了一起。

所以到最后，丘奇和圖靈這兩種看似矛盾的思想，在我的腦海里得到了和諧的統(tǒng)一。這些精髓的思想幫助我解決了許多的問題。感謝你們，計算機科學的兩位鼻祖。