邱奇-圖靈論題

邱奇-圖靈論題（英語：Church–Turing thesis，又稱邱奇-圖靈猜想，邱奇論題，邱奇猜想，圖靈論題）是一個關於可計算性理論的假設。該假設論述了關於函數特性的，可有效計算的函數值（用更現代的表述來說--在算法上可計算的)。簡單來說，邱奇-圖靈論題認為「任何在算法上可計算的問題同樣可由圖靈機計算」。

20世紀上半葉，對可計算性進行公式化表示的嘗試有：

• 美國數學家阿隆佐·邱奇創建了稱為λ演算的方法來定義函數。
• 英國數學家阿蘭·圖靈創建了可對輸入進行運算的理論機器模型，現在被稱為通用圖靈機。
• 邱奇以及數學家斯蒂芬·科爾·克萊尼和邏輯學家J. Barkley Rosser（英語：J. Barkley Rosser）一起定義了一類函數， 這種函數的值可使用遞歸方法計算。

這三個理論在直覺上似乎是等價的--它們都定義了同一類函數。因此，計算機科學家和數學家們相信，可計算性的精確定義已經出現。邱奇-圖靈論題的非正式表述說：如果某個算法是可行的，那這個算法同樣可以被圖靈機，以及另外兩個理論所實現。

雖然這三個理論被證明是等價的，但是其中的前提假設--「能夠有效計算」是一個模糊的定義。因此，雖然這個假說已接近完全，但仍然不能由公式證明。

假說前提

已知的三種計算過程（遞歸，λ演算和圖靈機）都是等價的--這三種方法定義了同一類函數。這導致數學家和計算機科學家相信可計算性的概念可由上述三種等價的計算過程描述。簡單來講，邱奇-圖靈論題認為如果某種方法（算法）可進行運算，那麼該運算也可被圖靈機執行（也可被遞歸定義的函數或λ函數執行）。

邱奇-圖靈論題是對計算特性進行描述的一種陳述，故而不能被嚴格證明。雖然上面提到的三種計算過程可被證明為等價的，但是邱奇-圖靈論題最根本的前提--聲稱一個函數是「可有效計算的」究竟意味着什麼--在某種意義上是不甚明確的直覺結果。所以，該論題依然是一個假想。

儘管邱奇-圖靈論題不能被證明，到目前為止它仍然受到近乎全面的接受。

正式闡述

Rosser於1939年對「可有效計算性」進行了如下的解讀：「很明顯CC和RC（邱奇和Rosser的論據）的成立依賴於對『有效性』的嚴格定義。『有效的方法』主要是指該方法的每一步都可被事先確定，而且該方法可在有限的步數之內生成結果」。因此，『有效性』實際上包含兩層含義：

1. 產生一種確定的，或者所需的效果
2. 能夠產生計算結果

接下來， 術語「可有效演算的」意味着「由任何直觀上有效的方法產生的」，而術語「可有效計算的」意味着「由圖靈機或任何等價的機械設備產生的」。圖靈本人對此的定義由他在1939年的博士論文「基於有序數的邏輯系統」的腳註中給出：

「^†我們應該使用『可計算函數』來表示一個可被機器計算的函數， 使用『可有效演算的』來指代那些並未特別指明的直觀想法。」

這可以轉述如下：

任何可有效演算的函數都是可計算函數。

圖靈則是如此描述的：

「當一個函數的值可由某種純機械計算步驟得到時， 它就是可有效演算的函數...應該這樣認識： 可計算性和可有效演算性是不同的。」

等價形式

本論題的另外一種說法就是邏輯和數學中的有效或機械方法可由圖靈機來表示。通常我們假定這些方法必須滿足以下的要求：

1. 一個方法由有限多簡單和精確的指令組成，這些指令可由有限多的符號來描述。
2. 該方法總會在有限的步驟內產生出一個結果。
3. 基本上人可以僅用紙張和鉛筆來執行。
4. 該方法的執行不需人類的智慧來理解和執行這些指令。

此類方法的一個範例便是用於確定兩個自然數的最大公約數的歐基里德算法。

「有效方法」這個想法在直覺上是清楚的，但卻沒有在形式上加以定義，因為什麼是「一個簡單而精確的指令」和什麼是「執行這些指令所需的智力」這兩個問題並沒有明確的答案。（如需歐幾里得算法之外的範例，請參見數論中的有效結果。）

起源

在他1936年的論文「論可計算數字，及其在判定性問題（德語：Entscheidungsproblem）中的應用」中，阿蘭·圖靈試圖通過引入圖靈機來形式地展示這一想法。在此篇論文中，他證明了「判定性問題」是無法解決的。幾個月之前，阿隆佐·邱奇在「關於判定性問題的解釋」（A Note on the Entscheidungsproblem）一文中證明出了一個相似的論題，但是他採用遞歸函數和Lambda可定義函數來形式地描述有效可計算性。Lambda可定義函數由阿隆佐·邱奇和斯蒂芬·克萊尼（Church 1932, 1936a, 1941, Kleene 1935）提出，而遞歸函數由庫爾特·哥德爾（Kurt Gödel）和雅克·埃爾布朗（Jacques Herbrand，Gödel 1934, Herbrand 1932）提出。這兩個機制描述的是同一集合的函數，正如邱奇和克林（Church 1936a, Kleene 1936）所展示的正整數函數那樣。在聽說了邱奇的建議後，圖靈很快就證明了他的圖靈機實際上描述的是同一集合的函數（Turing 1936, 263ff）.y

影響

之後用於描述有效計算的許多其他機制也被提了出來，比如寄存器機、埃米爾·波斯特（Emill Post）的波斯特系統，組合子邏輯以及馬爾可夫算法（Markov 1960）等。所有這些體系都已被證明在計算上和圖靈機擁有基本相同的能力；類似的系統被稱為圖靈完全。因為所有這些不同的試圖描述算法的努力都導致了等價的結果，所以現在普遍認為邱奇－圖靈論題是正確的。但是，該論題不具有數學定理一般的地位，也無法被證明；說是定理不如說是個將可計算性等同於圖靈機的提議。如果能有一個方法能被普遍接受為一個有效的算法但卻無法在圖靈機上允許，則該論題也是可以被駁斥的。

在20世紀初期，數學家們經常使用一種非正式的說法即可有效計算，所以為這個概念尋找一個好的形式描述也是十分重要的。當代的數學家們則使用圖靈可計算（或簡寫為可計算）這一定義良好的概念。由於這個沒有定義的用語在使用中已經淡去，所以如何定義它的問題已經不是那麼重要了。

哲學內涵

邱奇－圖靈論題對於心智哲學（philosophy of mind）有很多寓意，但是對於該論題的很多哲學解讀存在曲解。哲學學者B. Jack Copeland認為關於圖靈機是否可模擬確定的物理過程的問題仍沒有得到解答。他進一步聲稱關於這些物理過程是否在人類的智能機制中起到作用的問題也是未決的。有很多重要而懸而未決的問題也涵蓋了邱奇－圖靈論題和物理學及超計算（hypercomputation）的可能性之間的關係。應用到物理學上，該論題有很多可能的意義：

1. 宇宙是一台圖靈機（由此，在物理上對非遞歸函數的計算是不可能的）。該論述被定義為大邱奇－圖靈論題。
2. 宇宙不是一台圖靈機（也就是說，物理的定律不是圖靈可計算的），但是不可計算的物理事件卻不能阻礙創建超計算機（hypercomputer）的可能性。比如，一個在物理上包含實數而非可計算實數的宇宙就可以被劃為此類。
3. 宇宙是一台超計算機，而且建造物理設備來實現這一特性並以之計算非遞歸函數是可能的。比如，一個懸而未決的問題是我們無法確定量子力學（quantum mechanical）的事件是否圖靈可計算的，儘管諸如量子圖靈機之類的嚴格模型實際上等價於確定性圖靈機（但並不一定在效率上等價）。約翰·盧卡斯和羅傑·潘洛斯曾經建議說人的心靈可能是量子力學和非算法計算的結果，儘管並沒有科學證據支持這一提議。

實際上在這三類之外或其中還有許多其他的技術上的可能性，但這三類只是為了闡述這一概念。

不可計算函數

我們可以正式定義不可計算的函數。一個有名的例子是忙碌的海狸函數。該函數接受輸入n，返回具有n個狀態的圖靈機在停機之前所能打印的最大符號數量。找到忙碌的海狸函數的上限等於解決停機問題，該問題已被確定不能使用圖靈機解決。由於海狸很忙函數不能被圖靈機計算， 邱奇-圖靈論題斷言該函數不能使用任何方法進行有效計算。

有一些模型可用於計算（邱奇-圖靈）不可計算函數：即所謂的超計算機。Mark Burgin認為類似歸納性圖靈機的超遞歸算法（super-recursive algorithms）可用於反證邱奇-圖靈論題。他的論述依賴於對算法更廣泛的定義， 這種定義上的擴展使得一些歸納性圖靈機包含的不可計算函數變得可計算。這種對邱奇-圖靈論題的解讀與計算機科學的常規解讀不同，把超遞歸算法歸於邱奇-圖靈意義上的算法的這種看法並未受到相關領域的廣泛接受。

參考文獻

• An unsolvable problem of elementary number theory 中譯本 （頁面存檔備份，存於互聯網檔案館）
• Church, Alonzo. A set of Postulates for the Foundation of Logic. Annals of Mathematics. 1932, 33 (2): 346–366. JSTOR 1968337. doi:10.2307/1968337.
• Church, Alonzo. An Unsolvable Problem of Elementary Number Theory. American Journal of Mathematics. 1936, 58 (58): 345–363. JSTOR 2371045. doi:10.2307/2371045.
• Church, Alonzo. A Note on the Entscheidungsproblem. Journal of Symbolic Logic. 1936, (1): 40–41.
• Church, Alonzo. The Calculi of Lambda-Conversion. Princeton: Princeton University Press. 1941.
• Gödel, Kurt. On Undecidable Propositions of Formal Mathematical Systems. Davis, M. (編). The Undecidable. Kleene and Rosser (lecture note-takers); Institute for Advanced Study (lecture sponsor). New York: Raven Press. 1965 [1934].
• Herbrand, Jacques. Sur la non-contradiction de l'arithmétique. Journal fur die reine und angewandte Mathematik. 1932, (166): 1–8.
• Hofstadter, Douglas R. Chapter XVII: Church, Turing, Tarski, and Others. Gödel, Escher, Bach: an Eternal Golden Braid.
• Kleene, Stephen Cole. A Theory of Positive Integers in Formal Logic. American Journal of Mathematics. 1935, 57 (57): 153–173 & 219–244. JSTOR 2372027. doi:10.2307/2372027.
• Kleene, Stephen Cole. Lambda-Definability and Recursiveness. Duke Mathematical Journal. 1936, (2): 340–353.
• The Theory of Algorithms. American Mathematical Society Translations. 1960, 2 (15): 1–14 [1954].
• Turing, A.M. On Computable Numbers, with an Application to the Entscheidungsproblem. Proceedings of the London Mathematical Society. 2. 1936, 42: 230–2651937. doi:10.1112/plms/s2-42.1.230.（and Turing, A.M. On Computable Numbers, with an Application to the Entscheidungsproblem: A correction. Proceedings of the London Mathematical Society. 2. 1938, 43 (6): 544–5461937. doi:10.1112/plms/s2-43.6.544.）
• Pour-El, M.B.; Richards, J.I. Computability in Analysis and Physics. Springer Verlag. 1989. 引文使用過時參數coauthors (幫助)