判定器

在可计算性理论中，总是停机的机器也叫做判定器（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.