邱奇論題是一個關於可計算性理論的假設。該假設論述了關於函式特性的，可有效計算的函式值（用更現代的表述來說--在算法上可計算的)。簡單來說，邱奇-圖靈論題認為“任何在算法上可計算的問題同樣可由圖靈機計算”。
基本介紹
- 中文名：丘奇論題
- 外文名：Church’s thesis
- 提出者：丘奇
- 時間：1935
- 別名：邱奇-圖靈論題
- 套用學科：數學 計算機
假說前提,正式闡述,等價形式,起源,影響,哲學內涵,不可計算函式,
假說前提
已知的三種計算過程（遞歸，λ演算和圖靈機）都是等價的--這三種方法定義了同一類函式。這導致數學家和計算機科學家相信可計算性的概念可由上述三種等價的計算過程描述。簡單來講，邱奇-圖靈論題認為如果某種方法（算法）可進行運算，那么該運算也可被圖靈機執行（也可被遞歸定義的函式或λ函式執行）。
邱奇-圖靈論題是對計算特性進行描述的一種陳述，故而不能被嚴格證明。雖然上面提到的三種計算過程可被證明為等價的，但是邱奇-圖靈論題最根本的前提--聲稱一個函式是“可有效計算的”究竟意味著什麼--在某種意義上是不甚明確的直覺結果。所以，該論題依然是一個假想。
儘管邱奇-圖靈論題不能被證明，它仍然受到近乎全面的接受。
正式闡述
Rosser於1939年對“可有效計算性”進行了如下的解讀：“很明顯CC和RC（邱奇和Rosser的論據）的成立依賴於對‘有效性’的嚴格定義。‘有效的方法’主要是指該方法的每一步都可被事先確定，而且該方法可在有限的步數之內生成結果”。因此，‘有效性’實際上包含兩層含義：
（1）產生一種確定的，或者所需的效果；
（2）能夠產生計算結果。
接下來， 術語“可有效演算的”意味著“由任何直觀上有效的方法產生的”，而術語“可有效計算的”意味著“由圖靈機或任何等價的機械設備產生的”。圖靈本人對此的定義由他在1939年的博士論文“基於有序數的邏輯系統”的腳註中給出：“我們應該使用‘可計算函式’來表示一個可被機器計算的函式， 使用‘可有效演算的’來指代那些並未特別指明的直觀想法。”
這可以轉述為：任何可有效演算的函式都是可計算函式。
圖靈則是如此描述的：“當一個函式的值可由某種純機械計算步驟得到時， 它就是可有效演算的函式...應該這樣認識： 可計算性和可有效演算性是不同的。”
等價形式
本論題的另外一種說法就是邏輯和數學中的有效或機械方法可由圖靈機來表示。通常我們假定這些方法必須滿足以下的要求：
- 一個方法由有限多簡單和精確的指令組成，這些指令可由有限多的符號來描述。
- 該方法總會在有限的步驟內產生出一個結果。
- 基本上人可以僅用紙張和鉛筆來執行。
- 該方法的執行不需人類的智慧來理解和執行這些指令。
“有效方法”這個想法在直覺上是清楚的，但卻沒有在形式上加以定義，因為什麼是“一個簡單而精確的指令”和什麼是“執行這些指令所需的智力”這兩個問題並沒有明確的答案。（如需歐幾里得算法之外的範例，請參見數論中的有效結果。）
起源
在他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）。
20世紀上半葉，對可計算性進行公式化表示的嘗試有：
美國數學家阿隆佐·邱奇創建了稱為λ演算的方法來定義函式。英國數學家阿蘭·圖靈創建了可對輸入進行運算的理論機器模型，被稱為通用圖靈機。邱奇以及數學家史蒂芬·科爾·克萊尼和邏輯學家J. Barkley Rosser一起定義了一類函式， 這種函式的值可使用遞歸方法計算。
這三個理論在直覺上似乎是等價的--它們都定義了同一類函式。因此，計算機科學家和數學家們相信，可計算性的精確定義已經出現。邱奇-圖靈論題的非正式表述說：如果某個算法是可行的，那這個算法同樣可以被圖靈機，以及另外兩個理論所實現。
雖然這三個理論被證明是等價的，但是其中的前提假設--“能夠有效計算”是一個模糊的定義。因此，雖然這個假說已接近完全，但仍然不能由公式證明。
影響
之後用於描述有效計算的許多其他機制也被提了出來，比如暫存器機、埃米爾·波斯特（Emill Post）的波斯特系統，組合子邏輯以及馬爾可夫算法（Markov 1960）等。所有這些體系都已被證明在計算上和圖靈機擁有基本相同的能力；類似的系統被稱為圖靈完全。因為所有這些不同的試圖描述算法的努力都導致了等價的結果，所以普遍認為邱奇－圖靈論題是正確的。但是，該論題不具有數學定理一般的地位，也無法被證明；說是定理不如說是個將可計算性等同於圖靈機的提議。如果能有一個方法能被普遍接受為一個有效的算法但卻無法在圖靈機上允許，則該論題也是可以被駁斥的。
在20世紀初期，數學家們經常使用一種非正式的說法即可有效計算，所以為這個概念尋找一個好的形式描述也是十分重要的。當代的數學家們則使用圖靈可計算（或簡寫為可計算）這一定義良好的概念。由於這個沒有定義的用語在使用中已經淡去，所以如何定義它的問題已經不是那么重要了。
哲學內涵
邱奇－圖靈論題對於心智哲學（philosophy of mind）有很多寓意，但是對於該論題的很多哲學解讀存在曲解。哲學學者B. Jack Copeland認為關於圖靈機是否可模擬確定的物理過程的問題仍沒有得到解答。他進一步聲稱關於這些物理過程是否在人類的智慧型機制中起到作用的問題也是未決的。有很多重要而懸而未決的問題也涵蓋了邱奇－圖靈論題和物理學及超計算（hypercomputation）的可能性之間的關係。套用到物理學上，該論題有很多可能的意義：
- 宇宙是一台圖靈機（由此，在物理上對非遞歸函式的計算是不可能的）。該論述被定義為大邱奇－圖靈論題。
- 宇宙不是一台圖靈機（也就是說，物理的定律不是圖靈可計算的），但是不可計算的物理事件卻不能阻礙創建超計算機（hypercomputer）的可能性。比如，一個在物理上包含實數而非可計算實數的宇宙就可以被劃為此類。
實際上在這三類之外或其中還有許多其他的技術上的可能性，但這三類只是為了闡述這一概念。
不可計算函式
我們可以正式定義不可計算的函式。一個有名的例子是海狸很忙函式。該函式接受輸入n，返回具有n個狀態的圖靈機在停機之前所能列印的最大符號數量。找到海狸很忙函式的上限等於解決停機問題，該問題已被確定不能使用圖靈機解決。由於海狸很忙函式不能被圖靈機計算， 邱奇-圖靈論題斷言該函式不能使用任何方法進行有效計算。
有一些模型可用於計算（邱奇-圖靈）不可計算函式：即所謂的超計算機。Mark Burgin認為類似歸納性圖靈機的超遞歸算法（super-recursive algorithms）可用於反證邱奇-圖靈論題。他的論述依賴於對算法更廣泛的定義， 這種定義上的擴展使得一些歸納性圖靈機包含的不可計算函式變得可計算。這種對邱奇-圖靈論題的解讀與計算機科學的常規解讀不同，把超遞歸算法歸於邱奇-圖靈意義上的算法的這種看法並未受到相關領域的廣泛接受。
