丘奇（Alonzo Church）和圖靈（Alan Turing）是兩位對計算機科學具有最大影響力的人物，然而他們卻具有非常對立的觀點和相差很多的名氣。在我長達16年的計算機科學生涯中，總是感覺到自己的思想反反復復的徘徊於這兩個“陣營”之間。丘奇代表了“邏輯”和“語言”，而圖靈代表着“物理”和“機器”。在前面的8年中，我對丘奇一無所知，而在后面的8年中，我卻很少再聽到圖靈的名字。他們的觀點誰對誰錯，是一個無法回答的問題。完全投靠丘奇，或者完全投靠圖靈，貌似都是錯誤的做法。這是一種非常難說清楚的，矛盾的感覺，但是今天我試圖把自己的感悟簡要的介紹一下。
丘奇與圖靈之爭
想必世界上所有的計算機學生都知道圖靈的大名和事跡，因為美國計算機器學會（ACM）每年都會頒發“圖靈獎”，它被譽為計算機科學的最高榮譽。大部分的計算機學生都會在某門課程（比如“計算理論”）學習“圖靈機”的原理。然而，有多少人知道丘奇是什么人，他做出了什么貢獻，他與圖靈是什么樣的關系呢？我想恐怕不到一半的人吧。
如果你查一下數學家譜圖，就會發現丘奇其實是圖靈的博士導師。然而從 Andrew Hodges 所著的《圖靈傳》，你卻可以看到圖靈的心目中仿佛並沒有這個導師，仿佛自己的“全新發明”應得的名氣，被丘奇搶走了一樣（注意作者的用詞：robbed）。事實到底是怎樣的，恐怕誰也說不清楚。我只能說，貌似計算機科學從誕生之日開始就充滿了各種“宗教斗爭”。
雖然現在圖靈更加有名，然而在現實的程序設計中，卻是丘奇的理論在起着絕大部分的作用。據我的經驗，丘奇的理論讓很多事情變得簡單，而圖靈的機器卻過度的復雜。丘奇所發明的 lambda calculus 以及后續的工作，是幾乎一切程序語言的理論基礎。而根據老一輩的計算機工程師們的描述，最早的計算機構架也沒有受到圖靈的啟發，那是一些電機工程師完全獨立的工作。然而有趣的是，繼承了丘奇衣缽的計算機科學家們拿到的那個大獎，仍然被叫做“圖靈獎”。我粗略的算了一下，在迄今所有的圖靈獎之中，程序語言的研究者占了近三分之一。
從圖靈機到 lambda calculus
圖靈機永遠的停留在了理論的領域，絕大多數被用在“計算理論”（Theory of Computation）中。計算理論其實包括兩個主要概念：“可計算性理論”（computability）和“復雜度理論”(complexity）。這兩個概念在通常的計算理論書籍（比如 Sipser 的經典教材）里，都是用圖靈機來敘述的。在學習計算理論的時候，絕大多數的計算機學生恐怕都會為圖靈機頭痛好一陣子。
然而在做了研究生“計算理論”課程一個學期的 TA 之后我卻發現，其實幾乎所有計算理論的原理，都可以用 lambda calculus，或者程序語言和解釋器的原理來描述。所謂“通用圖靈機”（Universal Turing Machine），其實就是一個可以解釋自己的解釋器，叫做“元解釋器”（meta-circular interpreter）。在 Dan Friedman 的 B621 程序語言理論課程中，我最后的項目就是一個 meta-circular interpreter。這個解釋器能夠完全的解釋它自己，而且可以任意的嵌套（也就是說用它自己來解釋它自己，再來解釋它自己……）。然而我的“元解釋器”卻是基於 lambda calculus 的，所以我后來發現了一種方法，可以完全的用 lambda calculus 來解釋計算理論里面幾乎所有的定理。
我為這個發現寫了兩篇博文：《A Reformulation of Reducibility》和《Undecidability Proof of Halting Problem without Diagonalization》。我把 Sipser 的計算理論課本里面的幾乎整個一章的證明都用我自己的這種方式改寫了一遍，然后講給上課的學生。因為這種表示方法比起通常的“圖靈機+自然語言”的方式簡單和精確，所以收到了相當好的效果，好些學生對我說有一種恍然大悟的感覺。
我把這一發現告訴了我當時的導師 Amr Sabry。他笑了，說這個他早就知道了。他推薦我去看一本書，叫做《Computability and Complexity from a Programming Perspective》，作者是大名鼎鼎的 Neil Jones (他也是“Partial Evaluation”這一重要概念的提出者）。這本書不是用圖靈機，而是一種近似於 Pascal，卻又帶有 lambda calculus 的一些特征的語言（叫做 “WHILE 語言”）來描述計算理論。用這種語言，Jones 不但輕松的證明了所有經典的計算理論定理，而且能夠證明一些使用圖靈機不能證明的定理。
我曾經一直不明白，為什么可以如此簡單的解釋清楚的事情，計算理論需要使用圖靈機，而且敘述也非常的繁復和含糊。由於這些證明都出於資深的計算理論家們之手，讓我不得不懷疑自己的想法里面是不是缺了點什么。可是在看到了 Jones 教授的這本書之后，我倍感欣慰。原來一切本來就是這么的簡單！
后來從 CMU 的教授 Robert Harper 的一篇博文《Languages and Machines》中，我也發現 Harper 跟我具有類似的觀點，甚至更加極端一些。他強烈的支持使用 lambda calculus，反對圖靈機和其他一切機器作為計算理論的基礎。這也難怪，因為 Harper 跟丘奇是“直系”的學術血統關系：Alonzo Church -> Stephen Kleene -> Robert Constable -> Robert Harper。其中 Stephen Kleene 是圖靈的師兄，也是一個超級聰明的人。
從 lambda calculus 到電子線路
當我在 2012 年的 POPL 第一次見到 Neil Jones 的時候，他和藹的跟我解釋了許許多多的問題。當我問到他這本書的時候，他對我說：“我不推薦我的書給你，因為大部分的人都覺得 lambda calculus 難以理解。”Lambda calculus 難以理解？我怎么不覺得呢？我覺得圖靈機麻煩多了。然后我才發現，由於經過了這么多年的研究之后，自己對 lambda calculus 的理解程度已經到了深入骨髓的地步，所以我已經全然不知新手對它是什么樣的感覺。原來“簡單”這個詞，在具有不同經歷的人頭腦里，有着完全不同的含義。
所以其實 Jones 教授說的沒錯，lambda calculus 也許對於大部分人來說不合適，因為對於它沒有一個好的入門指南。Lambda calculus 出自邏輯學家之手，而邏輯學家們最在行的，就是把很簡單的“程序”用天書一樣的公式表示出來。這難怪老一輩的邏輯學家們，因為他們創造那些概念的時候，計算機還不存在。但是如果現在還用那一堆符號，恐怕就有點落伍了。大部分人在看到 beta-reduction, alpha-conversion, eta-conversion, ... 這大堆的公式的時候，就已經頭痛難忍了，怎么還有可能利用它來理解計算理論呢？
其實那一堆符號所表示的東西，終究超越不了現實里的物體和變化，最多不過再幻想一下“多種未來”或者“時間機器”。有了計算機之后，這些符號公式，其實都可以用數據結構和程序語言來表示。所以 lambda calculus 在我的頭腦里真的很簡單。每一個 lambda 其實就像是一個電路模塊。它從電線端子得到輸入，然后輸出一個結果。你把那些電線叫什么名字根本不重要，重要的是同一根電線的名字必須“一致”，這就是所謂的“alpha-conversion”的原理…… 不在這里多說了，如果你想深入的了解我心目中的 lambda calculus，也許可以看看我的另一篇博文《怎樣寫一個解釋器》，看看這個關於類型推導的幻燈片的開頭，或者進一步，看看如何推導出Y combinator，或者看看《What is a program?》。你也可以看看 Matthias Felleisen 和 Matthew Flatt 的《Programming Languages and Lambda Calculi》。
所以，也許你看到了在我的頭腦里面並存着丘奇和圖靈的影子。我覺得丘奇的 lambda calculus 是比圖靈機簡單而強大的描述工具，然而我卻又感染到了圖靈對於“物理”和“機器”的執着。我覺得邏輯學家們對 lambda calculus 的解釋過於復雜，而通過把它理解為物理的“電路元件”，讓我對 lambda calculus 做出了更加簡單的解釋，把它與“現實世界”聯系在了一起。
所以到最后，丘奇和圖靈這兩種看似矛盾的思想，在我的腦海里得到了和諧的統一。這些精髓的思想幫助我解決了許多的問題。感謝你們，計算機科學的兩位鼻祖。
摘自：https://blog.csdn.net/beswkwangbo/article/details/15812467
以下摘自：https://www.cnblogs.com/dcdcbigbig/p/10282224.html
關於邱奇-圖靈論題的一點思考
這道題起源於計算機科學史上一個非常著名的問題——邱奇-圖靈論題，這個論題是可計算性理論的基石，關於它的思考與證明幾乎貫穿了整個計算機科學史，涵蓋了數學、算法理論、數學邏輯學甚至哲學上的廣大深刻內容，直至今日還不斷有討論的聲音。今天因為這題去詳細了解了一下邱奇-圖靈論題，切實的感覺到了這個問題的偉大和影響深遠之處。
邱奇-圖靈論題的觀點表明，任何算法都可以由一台圖靈機來執行，即以任何編程語言編寫的算法都可以被翻譯（編譯？）成一台圖靈機，反之亦然，因此任何一種編程語言都足夠用來有效的表達任何算法。
邱奇-圖靈論題最早來源於阿蘭·圖靈和阿隆佐·邱奇關於判定性問題能否被解決的證明，當時邱奇首先利用遞歸函數和“可定義”函數來形式化地描述了有效可計算性，緊接着圖靈證明了“判定性問題”是不可解的（不可解問題最著名的一個例子是停機問題，詳解我或許會寫一篇博客？），根據邱奇對有效可計算性的描述，圖靈又證明了圖靈機所描述的是同一集合的函數（即任意語言集合）。
對這一論題的觀點進行延伸，可以得出一個結論：數學和邏輯學中的所有有效運算方法均可以用一台圖靈機來表示和演算，通常這些方法需要滿足：
1.由有限多的精確指令組成，每一條指令都可以由有限多的符號來描述；
2.每個方法都會在有限步驟內產生結果；（關於這一條的爭議貌似跟NP完備性問題有關……請不要問我）
3.該方法的執行不需要人類的智慧理解，即只需要按照給出的指令計算即可得出結果；
其中一個范例可以參考自遞歸的歐幾里得算法。
在圖靈之后，陸續有許多科學家也提出了不同的描述有效計算的機制，但所有這些體系都已經被證明是圖靈完全的，即在計算和證明上和圖靈機是幾乎等價的，所以普遍認為邱奇-圖靈論題是正確的。但是一個嚴重的漏洞是該論題並沒有被嚴謹證明，只是無法找到一個圖靈機不允許的有效算法，卻沒能證明不存在這樣的算法。因此可以說“有效可計算性”這個詞的定義也是不嚴謹的，而現在的數學家們大都對這個問題避而不談，改用另一個定義良好的詞——“圖靈可計算性”來描述可計算性。筆者認為這樣在問題定義還不清晰的基礎上去頻繁使用是非常“危險”的，因為定義的一點破綻可能會導致整個計算機科學體系的崩塌（參見第二，第三次數學危機）。
在哲學方面，邱奇-圖靈論題的意義非常深刻，涉及到宇宙的本質和超計算的可能性。
1.廣義的邱奇-圖靈論題認為宇宙是一台圖靈機，可以存儲無限精度的實數，如果這樣定義，則宇宙中不存在實數，只存在可計算數；由上，如果該定義為真，則在物理上對非遞歸函數的計算是不可能的；
2.宇宙不是一台圖靈機，則物理定律都不是圖靈可計算的，但在此基礎上建立“超計算機”並不是不可能的；
3.宇宙是一台（量子）超計算機，則可以通過物理設備來控制這一特征來計算非遞歸函數，即量子力學中的事件都是圖靈可計算的，由量子比特構成的系統都是圖靈完備的，甚至有人認為人的心智就是量子演算的結果；
拋去哲學上的問題不談，筆者認為邱奇-圖靈論題最偉大的地方在於辨清了計算，圖靈機和編程語言的關系，把計算機科學和其它科學領域划清了界限，對“算法”本身給出了精確的定義，以及對於“有效運算”和可計算性的探討，令人對“計算機”這一概念有更充分的理解。可以說整個計算機科學的理論根基都是由這一論題發展起來的，現在我們寫的每一行代碼與其都有不可或缺的聯系。
（部分摘自百度百科）
一些資料：
https://www.zhihu.com/question/21579465/answer/106995708
https://wenku.baidu.com/view/b1bb8eade009581b6ad9eb41.html
https://www.cnblogs.com/zhangzefei/p/9743546.html