不可解問題—停機問題證實

圖靈在1936年就指出，圖靈機並非什麼都能計算。最著名的例子就是停機問題，即沒有計算機能經過查看一段代碼就知道本身是會永遠執行下去仍是會最終中止。——摘自《可能與不可能的邊界：P/NP問題趣史》

前言

　　咱們都見過計算機屏幕上出現一個表明忙碌的小沙漏，不知道這是表明計算機死機了，仍是在進行長時間的計算。用戶該立刻重啓機器呢，仍是再等一下子？若是能有一個算法，告訴咱們計算機是否是陷入了某種無窮循環該有多好！那是很好，但那也是不可能的。——摘自《可能與不可能的邊界:P/NP問題趣史》

概念

　　不可解問題(Undecidable Decision Problem)指的是這樣一種問題：它不管如何也不可能有一個正確的算法來解決。雖然難以想象，但這種問題被證實確實是存在的。圖靈在1936年提出了第一個不可解問題的實例：停機問題（The Halting Problem）。

　　停機問題（The Halting Problem）是問，輸入一段程序代碼和一個針對此程序的輸入，可否編程判斷運行這個程序後程序是否會終止。
　　這個問題的答案是否認的。也就是說，不可能有一種算法能夠正確判斷一個指定的程序運行後，給予指定的輸入，程序最後出不出得來。換句話說，停機問題（The Halting Problem）是一個不可解問題。

停機問題的直觀解釋

　　不可能設計這樣一個萬能程序，它能斷定一切程序（包括它本身）會不會死循環。

證實

 　　證實過程很是簡單，假設The Halting Problem是有解的，而且已經用程序實現了，那麼咱們只須要再編寫一個程序Program Bug，就會發現存在矛盾。

　　反證：既然解決The Halting Problem的算法已經實現了，那麼咱們必定能定義一個函數

Function Halting(a,b:input_type):boolean;

　　其中，a是讀入的程序源碼，b是輸入數據。這個函數的功能就是返回對於指定的程序源碼和輸入數據，程序是否能順利退出。等價爲「輸入一段代碼A和一個針對A的輸入a，可否編程B判斷A（a）是不是死循環」。
　　下面編寫一個程序：

Program Bug;
var
    code:input_type;
begin
   get(code);   //讀入code
   if halting(code,code) then repeat until false
      else halt;
end.

　　如今運行Bug這個程序，而且輸入Bug這個程序自己的代碼。這樣，halting(code,code)其實質就是在判斷這個Bug程序自己了。若是The Halting Problem認爲Bug程序會正常退出，那麼就讓程序進入一個死循環，不然當即退出程序。矛盾產生。

造一個圖靈機D  描述 
       「永遠的在野派」   它 「反對 一切 當權派」
這個D 總與 當局唱 對臺戲，
     它本身當權時, 本身也反對本身， 引發矛盾

圖靈停機問題

問題：能不能設計一個程序P，判斷出任意一個程序X是否會在輸入Y的狀況下陷入死循環？

設P(X,Y)表示P判斷程序X在輸入爲Y時的結果。若是X存在死循環，那麼P(X,Y)就輸出一個yes。若是X不存在死循環，那麼P(X,Y)就輸出一個no。這樣的P(X,Y)存在嗎？

某個程序X在輸入Y上停機，就是說X不存在着死循環；

若是不停機就是存在着死循環。

假設程序P存在。那麼咱們能夠根據P設計一個新的程序Q以下，其中X是任何一段程序的編碼：

Program Q(X){
    m=P(X,X)
    do while(m==no)//m=no意味着X不存在死循環
    ……
    ……
    enddo
    if m==yes then return;//m=yes意味着X不存在死循環
}

輸入任何一段程序X，調用函數P(X,X)並獲得返回值m，若是m=no，意味着P判斷出程序X做用到X自身不存在死循環。那麼Q就不停的作do while和enddo之間的語句。若是m=yes，表示P判斷出程序X在以X爲輸入時存在死循環，此時，函數Q運行結束。

問Q這個程序做用到Q自身的編碼上也就是Q(Q)會不會死循環呢？

假設Q(Q)會發生死循環，那麼P(Q,Q)就會返回yes.也就是m=yes，所以Q函數立刻結束，也就是程序Q(Q)沒有發生死循環。→矛盾！ 假設Q(Q)不發生死循環，那麼P(Q,Q)應該返回no，也就是m=no，這樣程序就會進入do while循環，而這個循環顯然是一個死循環。於是Q(Q)發生了死循環。→矛盾！

不管Q(Q)會不會發生死循環，都會產生矛盾。

假設P(X,Y)可以判斷任意程序X在輸入Y的時候是否死循環是錯誤的。也就是說這樣的程序P(X,Y)不存在。

停機問題與停機定理

停機問題：任給圖靈機程序P和一組輸入數據I，是否存在單個程序，接受P和I做爲其輸入，並在有限步後停機，並在帶上的最後作出說明，P在處理I時是否將在有限步後中止？

停機定理（1936）：給定一任意的圖靈機程序P和一組任意的輸入數據I，不存在單個的圖靈機程序，它在有限多步後停機，並告訴咱們P是否結束輸入數據I的處理。

證實：反證假設，存在這樣一個圖靈機TM(P,I)，它能夠斷定程序P在輸入I的狀況下是否可停機：若P在輸入I時可停機，TM(P,I)輸出「停機」，不然，TM(P,I)輸出「死循環」。

　　顯然，TM(P,I)自己可被視程序P_TM，也可做爲輸入I_TM，故TM(P,I)能夠斷定當將I_TM做爲P_TM的輸入時，P_TM是否會停機。

　　現考慮一個與TM(P,I)相反的圖靈機TM-bar(P,I):首先，它調用TM(P_TM,I_TM)。若TM(P_TM,I_TM)輸出「死循環」，則輸出「停機」，不然輸出「死循環」。

　　再考慮運行TM(P_TM-bar,I_TM-bar)時的情形。若TM(P_TM-bar,I_TM-bar)輸出「停機」，則它輸出「死循環」若TM(P_TM-bar,I_TM-bar)輸出「死循環」，則它輸出「停機」。總產生矛盾。

哥德爾定理和停機定理之間有什麼關係？

　　參考：康托爾、哥德爾、圖靈——永恆的金色對角線

參考文獻：

https://wenku.baidu.com/view/ad82e57b31b765ce05081490.html?sxts=1540116131874

http://www.matrix67.com/blog/archives/55