简介

全图灵机可计算的函数

简介

在可计算性理论中，总是停机的机器也叫做判定器（Sipser，1996年）或全图灵机（Kozen，1997年）是对所有输入总是停机的图灵机。

因为它总是停机，这个机器有能力判定给定字符串是否是一个形式语言的成员。可由这种机器判定的语言类精确的是递归语言的集合。但是由于停机问题，判定任意图灵机是否在任意输入上停机的问题自身是不可判定的判定问题。

全图灵机可计算的函数

在实践中，很多有价值的函数都是用总是停机的机器可计算的。通过限制它的流控制能力就可以强制机器对所有输入都停机，使得没有程序可以导致机器进入无限循环。作为平凡的例子，实现有限判定树的机器将总是停机。

不要求机器完全免除循环能力来保证停机。如果我们限制循环为有可预测的有限大小，我们可以表达所有原始递归函数(Meyer and Ritchie, 1967)。Brainerd 和 Landweber (1974) 的玩具编程语言 PL- {GOTO} 就是这种机器的一个例子。

我们可以进一步的定义能确保更复杂的函数总是停机的一个编程语言。例如，不是原始递归函数的阿克曼函数，但它是通过带有在它的参数上的简约排序的项重写系统可计算的全可计算函数(Ohlebusch, 2002, pp.67)。