判定器

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

基本介紹

• 中文名：判定器
• 外文名：Sipser
• 性質：圖靈機的一種
• 領域：計算機

簡介

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

全圖靈機可計算的函式

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

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

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

與偏圖靈機的關係

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

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的假定。

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

全圖靈機的附標的集合

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