判定器

在可計算性理論中，總是停機的機器也叫做判定器（Sipser，1996年）或全圖靈機（Kozen，1997年）是對所有輸入總是停機的圖靈機。

因為它總是停機，這個機器有能力判定給定字符串是否是一個形式語言的成員。可由這種機器判定的語言類精確的是遞歸語言的集合。但是由於停機問題，判定任意圖靈機是否在任意輸入上停機的問題自身是不可判定的判定問題(參見哥德爾不完備定理)。

全圖靈機可計算的函數

在實踐中，很多有價值的函數都是用總是停機的機器可計算的。通過限制它的流控制能力就可以強制機器對所有輸入都停機，使得沒有程序可以導致機器進入無窮迴圈。作為平凡的例子，實現有限判定樹的機器將總是停機。

不要求機器完全免除循環能力來保證停機。如果我們限制循環為有可預測的有限大小，我們可以表達所有原始遞歸函數(Meyer and Ritchie, 1967)。Brainerd 和 Landweber (1974) 的玩具程式語言 PL- {GOTO} 就是這種機器的一個例子。

我們可以進一步的定義能確保更複雜的函數總是停機的一個程式語言。例如，不是原始遞歸函數的阿克曼函數，但它是通過帶有在它的參數上的簡約排序的項重寫系統可計算的全可計算函數(Ohlebusch, 2002, pp.67)。

與偏圖靈機的關係

一般的圖靈機可以計算偏函數。有關於偏圖靈機和全圖靈機之間關係的兩個問題:

1. 所有用偏圖靈機可計算的偏函數都可以被擴展(就是說擴大它的定義域)成為全可計算函數嗎?
2. 有可能改變圖靈機的定義使得特定類的全圖靈機計算所有全可計算函數?

對這兩個問題的答案都是否定的。

下列定義證明了對總是停機的機器是可計算的函數不包括所有偏可計算函數的擴展，這蘊涵了上述第一個問題有否定答案。這個問題密切關係於停機問題的算法上不可解。

定理。有不能擴展成全圖靈機可計算函數的圖靈可計算偏函數。特別是偏函數 f，它被定義得使 f(n) = m，若且唯若帶有附標 n 的圖靈機停機於輸入 0 並輸出 m，它沒有到全可計算函數的擴展。

反證法進行證明。如果 g 是擴展 f 的全可計算函數，則 g 將對某個圖靈機是可計算的；固定 e 作為這樣一個機器的附標。使用Kleene遞歸定理建造一個圖靈機 M，它在輸入 0 上模擬運行在 M 的一個附標 n_M 上的帶有附標 e 的機器(因此機器 M 可以生成自身的一個附標；這是遞歸定理扮演的角色)。通過假定，這個模擬將最終返回一個答案。定義 M 使得如果 g(n_M) = m 則M 的返回值是 m + 1。因此 f(n_M)，M 在輸入 0 上的真返回值將不等於 g(n_M)。這矛盾於 g 擴展 f 的假定。

第二個問題在本質上問是否有另一個合理的計算模型只計算全函數並計算所有全可計算函數。非形式的說，如果這種模型存在，則它的每個計算機都可以被一個圖靈機模擬。因此如果這個新計算模型由一序列機器 $M_{1},M_{2},\ldots$ 組成，則會有計算全函數的圖靈機的遞歸可枚舉序列 $T_{1},\ldots T_{2},\ldots$，因而所有全可計算函數都對機器 T_i 之一是可計算的。這是不可能的，因為機器 $T$ 可以被構造的使得在輸入 i 上機器 T 返回 $T_{i}(i)+1\,$。那麼 T 將是全機器，因為每個 T_i 是全的，並且由 T 可計算的函數不能出現在列表中。這證明了第二個問題有否定的答案。

全圖靈機的附標的集合

有附標 e 的圖靈機是否在所有輸入上停機的判定問題是不可判定的。事實上，這個問題位於算術層次的 $\Pi _{2}^{0}$ 級別。因此這個問題嚴格的比停機問題更困難，它問有附標 e 的機器是否停機在輸入 0 上。直覺的說，在不可解決性上的這個困難在於每個「全機器」問題的實例提出無限多個停機問題的實例。

引用

• Brainerd, W.S., Landweber, L.H. (1974), Theory of Computation, Wiley.
• Meyer, A.R., Ritchie, D.M. (1967), The complexity of loop programs, Proc. of the ACM National Meetings, 465.
• Sipser, M. (1996), Introduction to the Theory of Computation, PWS Publishing Co.
• Kozen, D.C. (1997), Automata and Computability, Springer.
• Ohlebusch, E. (2002), Advanced Topics in Term Rewriting, Springer.