簡介
在可計算性理論中,總是停機的機器也叫做判定器(Sipser,1996年)或全圖靈機(Kozen,1997年)是對所有輸入總是停機的圖靈機。
因為它總是停機,這個機器有能力判定給定字元串是否是一個形式語言的成員。可由這種機器判定的語言類精確的是遞歸語言的集合。但是由於停機問題,判定任意圖靈機是否在任意輸入上停機的問題自身是不可判定的判定問題。
全圖靈機可計算的函式
在實踐中,很多有價值的函式都是用總是停機的機器可計算的。通過限制它的流控制能力就可以強制機器對所有輸入都停機,使得沒有程式可以導致機器進入無限循環。作為平凡的例子,實現有限判定樹的機器將總是停機。
不要求機器完全免除循環能力來保證停機。如果我們限制循環為有可預測的有限大小,我們可以表達所有原始遞歸函式(Meyer and Ritchie, 1967)。Brainerd 和 Landweber (1974) 的玩具程式語言 PL- {GOTO} 就是這種機器的一個例子。
我們可以進一步的定義能確保更複雜的函式總是停機的一個程式語言。例如,不是原始遞歸函式的阿克曼函式,但它是通過帶有在它的參數上的簡約排序的項重寫系統可計算的全可計算函式(Ohlebusch, 2002, pp.67)。