图灵停机问题

此词条由范星辰翻译。

In computability theory, the halting problem is the problem of determining, from a description of an arbitrary computer program and an input, whether the program will finish running, or continue to run forever. Alan Turing proved in 1936 that a general algorithm to solve the halting problem for all possible program-input pairs cannot exist.

In computability theory, the halting problem is the problem of determining, from a description of an arbitrary computer program and an input, whether the program will finish running, or continue to run forever. Alan Turing proved in 1936 that a general algorithm to solve the halting problem for all possible program-input pairs cannot exist.

在可计算性理论中，停机问题是从任意一个计算机程序的描述和一个输入来确定程序是否会完成运行，或者永远继续运行。阿兰 · 图灵在1936年证明了解决所有可能的程序输入对的停机问题的一般算法是不存在的。

【最终版】在可计算性理论中，停机问题是指从对任意计算机程序和输入的描述中确定程序是否将结束运行，或继续永远运行的问题。艾伦·图灵在1936年证明，解决所有可能的程序输入对停机问题的通用算法是不存在的。

For any program f that might determine if programs halt, a "pathological" program g, called with some input, can pass its own source and its input to f and then specifically do the opposite of what f predicts g will do. No f can exist that handles this case. A key part of the proof is a mathematical definition of a computer and program, which is known as a Turing machine; the halting problem is undecidable over Turing machines. It is one of the first cases of decision problems proven to be unsolvable. This proof is significant to practical computing efforts, defining a class of applications which no programming invention can possibly perform perfectly.

For any program f that might determine if programs halt, a "pathological" program g, called with some input, can pass its own source and its input to f and then specifically do the opposite of what f predicts g will do. No f can exist that handles this case. A key part of the proof is a mathematical definition of a computer and program, which is known as a Turing machine; the halting problem is undecidable over Turing machines. It is one of the first cases of decision problems proven to be unsolvable. This proof is significant to practical computing efforts, defining a class of applications which no programming invention can possibly perform perfectly.

对于任何可能决定程序是否停止的程序，一个“病态的”程序 g，带有一些输入，可以将它自己的源和输入传递给 f，然后具体地做与 f 预测的相反的事情。没有 f 可以处理这种情况。证明的一个关键部分是计算机和程序的数学定义，也就是所谓的图灵机; 停机问题在图灵机上是不可判定的。这是决策问题被证明无法解决的首批案例之一。这一证明对实际计算工作具有重要意义，它定义了一类任何编程发明都不可能完美执行的应用程序。

【最终版】对于任何可能决定程序是否停止的程序f，一个“病态的”程序g，通过一些输入调用，可以将它自己的源和输入传递给f，然后特别地做f预测g将做的相反的事情。没有f可以处理这种情况。证明的关键部分是计算机和程序的数学定义，这被称为图灵机;在图灵机上，停机问题是无法确定的。这是首批被证明无法解决的决策问题之一。这个证明对于实际的计算工作是很重要的，它定义了任何编程发明都不可能完美执行的一类应用程序。 Jack Copeland (2004) attributes the introduction of the term halting problem to the work of Martin Davis in the 1950s.

The halting problem is a decision problem about properties of computer programs on a fixed Turing-complete model of computation, i.e., all programs that can be written in some given programming language that is general enough to be equivalent to a Turing machine. The problem is to determine, given a program and an input to the program, whether the program will eventually halt when run with that input. In this abstract framework, there are no resource limitations on the amount of memory or time required for the program's execution; it can take arbitrarily long and use an arbitrary amount of storage space before halting. The question is simply whether the given program will ever halt on a particular input.

停机问题是关于固定的图灵完全计算模型上的计算机程序性质的决策问题，也就是说，所有程序都可以用某种给定的编程语言编写，这种编程语言的通用性足以等价于一台图灵机。问题是确定，给定一个程序和程序的一个输入，程序是否最终在运行该输入时停止。在这个抽象的框架中，程序执行所需的内存和时间没有资源限制; 它可以花费任意长的时间，并且在停止之前使用任意数量的存储空间。问题很简单，给定的程序是否会在某个特定的输入上停止。

【最终版】停机问题是在一个固定的图灵完备计算模型上，即用某种给定的程序语言编写的所有程序的性质的决策问题，该语言的通用性足以与图灵机相当。问题是，给定一个程序和一个程序的输入，当运行该输入时，程序是否最终会停止。在这个抽象的框架中，对于程序执行所需的内存或时间没有资源限制;在停止之前，它可以花费任意长的时间和使用任意数量的存储空间。问题很简单，给定的程序是否会在特定的输入时停止。

Background背景

For example, in pseudocode, the program

例如，在伪代码中，程序

【最终版】例如，在伪代码中，程序

The halting problem is a decision problem about properties of computer programs on a fixed Turing-complete model of computation, i.e., all programs that can be written in some given programming language that is general enough to be equivalent to a Turing machine. The problem is to determine, given a program and an input to the program, whether the program will eventually halt when run with that input. In this abstract framework, there are no resource limitations on the amount of memory or time required for the program's execution; it can take arbitrarily long and use an arbitrary amount of storage space before halting. The question is simply whether the given program will ever halt on a particular input.

while (true) continue

当(真)继续

【最终版】停机问题是在一个固定的图灵完备计算模型上，即用某种给定的程序语言编写的所有程序的性质的决策问题，该语言的通用性足以与图灵机相当。问题是，给定一个程序和一个程序的输入，当运行该输入时，程序是否最终会停止。在这个抽象的框架中，对于程序执行所需的内存或时间没有资源限制;在停止之前，它可以花费任意长的时间和使用任意数量的存储空间。问题很简单，给定的程序是否会在特定的输入时停止。

For example, in pseudocode, the program

does not halt; rather, it goes on forever in an infinite loop. On the other hand, the program

它不会停止，而是永远在无限循环中运行。另一方面，这个项目

【最终版】例如，在伪代码中，程序

不停止;相反，它会在一个无限循环中无限持续下去。另一方面，程序

while (true) continue

print "Hello, world!"

“你好，世界！””

【最终版】而(真)继续

打印“你好，世界！”

does not halt; rather, it goes on forever in an infinite loop. On the other hand, the program

does halt.

停下来。

【最终版】不停止;相反，它会在一个无限循环中无限持续下去。另一方面，程序

并停止。

print "Hello, world!"

While deciding whether these programs halt is simple, more complex programs prove problematic. One approach to the problem might be to run the program for some number of steps and check if it halts. But if the program does not halt, it is unknown whether the program will eventually halt or run forever. Turing proved no algorithm exists that always correctly decides whether, for a given arbitrary program and input, the program halts when run with that input. The essence of Turing's proof is that any such algorithm can be made to contradict itself and therefore cannot be correct.

虽然决定这些程序是否停止很简单，但是更复杂的程序证明是有问题的。解决这个问题的一个方法可能是运行一些步骤的程序，并检查它是否停止。但是如果程序没有停止，那么程序最终是停止还是永远运行就不得而知了。图灵证明了没有一种算法能够总是正确地决定，对于给定的任意程序和输入，程序在运行该输入时是否停止。图灵证明的本质是，任何这样的算法都可能自相矛盾，因此不可能是正确的。

【最终版】虽然判断这些程序是否停止很简单，但更复杂的程序被证明是有问题的。解决这个问题的一种方法可能是运行程序若干步，并检查它是否停止。但如果程序不停止，则不知道程序最终会停止还是永远运行。图灵证明，对于给定的任意程序和输入，没有一种算法能够总是正确地决定程序在运行时是否会停止。图灵证明的本质是，任何这样的算法都可能自相矛盾，因此不可能是正确的。

does halt.

While deciding whether these programs halt is simple, more complex programs prove problematic. One approach to the problem might be to run the program for some number of steps and check if it halts. But if the program does not halt, it is unknown whether the program will eventually halt or run forever. Turing proved no algorithm exists that always correctly decides whether, for a given arbitrary program and input, the program halts when run with that input. The essence of Turing's proof is that any such algorithm can be made to contradict itself and therefore cannot be correct.

Some infinite loops can be quite useful. For instance, event loops are typically coded as infinite loops.

一些无限循环是非常有用的。例如，事件循环通常被编码为无限循环。

【最终版】虽然判断这些程序是否停止很简单，但更复杂的程序被证明是有问题的。解决这个问题的一种方法可能是运行程序若干步，并检查它是否停止。但如果程序不停止，则不知道程序最终会停止还是永远运行。图灵证明，对于给定的任意程序和输入，没有一种算法能够总是正确地决定程序在运行时是否会停止。图灵证明的本质是，任何这样的算法都可能自相矛盾，因此不可能是正确的。

有些无限循环非常有用。例如，事件循环通常被编码为无限循环。

However, most subroutines are intended to finish (halt).

但是，大多数子程序都打算完成(暂停)。

【最终版】然而，大多数子程序的目的是完成(停止)。

Programming consequence编程的后果

In particular, in hard real-time computing,

特别是在硬实时计算中,

【最终版】特别是在硬实时计算中，

programmers attempt to write subroutines that are not only guaranteed to finish (halt),

程序员试图编写不仅保证完成(暂停)的子程序,

【最终版】程序员试图编写的子例程不仅保证完成(停止)，

Some infinite loops can be quite useful. For instance, event loops are typically coded as infinite loops.

but are also guaranteed to finish before a given deadline.

但也保证能在给定的截止日期前完成。

【最终版】有些无限循环非常有用。例如，事件循环通常被编码为无限循环。

但也保证在规定的期限前完成。

However, most subroutines are intended to finish (halt).

In particular, in hard real-time computing,

programmers attempt to write subroutines that are not only guaranteed to finish (halt),

but are also guaranteed to finish before a given deadline.

【最终版】然而，大多数子程序的目的是完成(停止)。

特别是在硬实时计算中，

程序员试图编写的子例程不仅保证完成(停止)，

但也保证在规定的期限前完成。

Minsky notes, however, that a computer with a million small parts, each with two states, would have at least 2^1,000,000 possible states:

然而，明斯基指出，一台有100万个小部件的计算机，每个小部件有两个状态，至少会有2个 < sup > 1,000,000个 可能状态:

【最终版】然而，明斯基指出，一台有一百万个小部件的计算机，每个部件都有两个状态，将至少有两千一百万种可能的状态:

Sometimes these programmers use some general-purpose (Turing-complete) programming language,

This is a 1 followed by about three hundred thousand zeroes ... Even if such a machine were to operate at the frequencies of cosmic rays, the aeons of galactic evolution would be as nothing compared to the time of a journey through such a cycle (Minsky 1967 p. 25):

这是一个1后面跟着大约30万个0..。即使这样一台机器能够在宇宙射线的频率下运转，星系演化的亿万年也比不上这样一个周期的旅行时间(明斯基，1967年，第25页) :

【最终版】有时这些程序员使用一些通用的(图灵完备的)编程语言，

这是一个1后面跟着大约30万个0……即使这样的机器在宇宙射线的频率下运行，与经过这样一个周期的旅行所花费的时间相比，数十亿年的银河进化将是微不足道的(明斯基1967 p. 25):

but attempt to write in a restricted style—such as MISRA C or SPARK—that makes it easy to prove that the resulting subroutines finish before the given deadline.模板:Cn

Minsky states that although a machine may be finite, and finite automata "have a number of theoretical limitations":

明斯基指出，尽管机器可能是有限的，但有限自动机“有一些理论上的局限性” :

【最终版】但是试图写一个受限style-such MISRA - C或火花很容易证明,由此产生的子程序给定的截止日期前完成。

明斯基指出，尽管机器可能是有限的，而有限自动机“有一些理论局限性”:

Other times these programmers apply the rule of least power—they deliberately use a computer language that is not quite fully Turing-complete. Frequently, these are languages that guarantee all subroutines finish, such as ...the magnitudes involved should lead one to suspect that theorems and arguments based chiefly on the mere finiteness [of] the state diagram may not carry a great deal of significance. (Minsky p. 25)

所涉及的程度会使人怀疑，主要基于状态图的有限性的定理和论证可能没有多大意义。

【最终版】其他时候，这些程序员应用最小功率规则——他们故意使用一种完备的计算机语言但是里面所包含的图灵机确是不完备的。通常情况下，这些语言都是为了保证子程序的完成，其中所涉及的量级甚至使人怀疑，那些量级主要基于状态图的有限性定理，这些状态图本身可能没有携带太大的意义。

Common pitfalls常见的陷阱

It can also be decided automatically whether a nondeterministic machine with finite memory halts on none, some, or all of the possible sequences of nondeterministic decisions, by enumerating states after each possible decision.

通过在每个可能的决策之后列举状态，还可以自动决定一个内存有限的不确定性机器是否停止任何、部分或全部可能的不确定性决策序列。

【最终版】它还可以通过枚举每个可能的决策之后的状态，自动决定具有有限内存的不确定性机器是否停止于无、部分或所有可能的非确定性决策序列上。

The difficulty in the halting problem lies in the requirement that the decision procedure must work for all programs and inputs. A particular program either halts on a given input or does not halt. Consider one algorithm that always answers "halts" and another that always answers "does not halt". For any specific program and input, one of these two algorithms answers correctly, even though nobody may know which one. Yet neither algorithm solves the halting problem generally.

【最终版】停机问题的难点在于，决策过程必须对所有程序和输入都有效。一个特定的程序要么在给定的输入上停止，要么不停止。假设一种算法总是回答“停止”，而另一种算法总是回答“不停止”。对于任何特定的程序和输入，这两种算法中的一种会正确回答，即使没有人知道是哪一种。然而，这两种算法一般都不能解决停机问题。

There are programs (interpreters) that simulate the execution of whatever source code they are given. Such programs can demonstrate that a program does halt if this is the case: the interpreter itself will eventually halt its simulation, which shows that the original program halted. However, an interpreter will not halt if its input program does not halt, so this approach cannot solve the halting problem as stated; it does not successfully answer "does not halt" for programs that do not halt.

【最终版】有些程序(解释器)可以模拟给定的任何源代码的执行。在这种情况下，这样的程序可以证明程序确实会停止:解释器本身最终会停止其模拟，这表明原来的程序停止了。然而，如果解释器的输入程序没有停止，它就不会停止，所以这种方法不能解决如上所述的停止问题;对于那些不停止的项目，它没有成功地回答“不停止”。

The halting problem is historically important because it was one of the first problems to be proved undecidable. (Turing's proof went to press in May 1936, whereas Alonzo Church's proof of the undecidability of a problem in the lambda calculus had already been published in April 1936 [Church, 1936].) Subsequently, many other undecidable problems have been described.

停机问题具有重要的历史意义，因为它是首先被证明为无法判定的问题之一。(图灵的证明在1936年5月付印，而阿隆佐 · 丘奇关于 lambda 微积分中一个问题不可判定性的证明在1936年4月已经发表。)随后，许多其他不可判定的问题也被描述。

【最终版】停机问题在历史上很重要，因为它是第一个被证明是不可决定的问题之一。(图灵的证明在1936年5月付印，而Alonzo Church对lambda微积分中一个问题的不可判定性的证明已经在1936年4月发表[Church, 1936]。)随后，又叙述了许多其他无法决定的问题。

The halting problem is theoretically decidable for linear bounded automata (LBAs) or deterministic machines with finite memory. A machine with finite memory has a finite number of configurations, and thus any deterministic program on it must eventually either halt or repeat a previous configuration:

...any finite-state machine, if left completely to itself, will fall eventually into a perfectly periodic repetitive pattern. The duration of this repeating pattern cannot exceed the number of internal states of the machine... (italics in original, Minsky 1967, p. 24)

【最终版】对于线性有界自动机(LBAs)或具有有限内存的确定性机器，停机问题在理论上是可判定的。具有有限内存的机器具有有限数量的配置，因此，它上的任何确定性程序最终都必须停止或重复之前的配置:

.．.任何有限状态机，如果完全放任自流，最终将落入一个完美的周期性重复模式。这种重复模式的持续时间不能超过机器内部状态的数量…

Minsky notes, however, that a computer with a million small parts, each with two states, would have at least 2^1,000,000 possible states:

This is a 1 followed by about three hundred thousand zeroes ... Even if such a machine were to operate at the frequencies of cosmic rays, the aeons of galactic evolution would be as nothing compared to the time of a journey through such a cycle (Minsky 1967 p. 25):

【最终版】然而，明斯基指出，一台有一百万个小部件的计算机，每个部件都有两个状态，将至少有两千一百万种可能的状态:

这是一个1后面跟着大约30万个0……即使这样的机器在宇宙射线的频率下运行，与经过这样一个周期的旅行所花费的时间相比，数十亿年的银河进化将是微不足道的。

Minsky states that although a machine may be finite, and finite automata "have a number of theoretical limitations":

...the magnitudes involved should lead one to suspect that theorems and arguments based chiefly on the mere finiteness [of] the state diagram may not carry a great deal of significance. (Minsky p. 25)

【最终版】明斯基指出，尽管机器可能是有限的，而有限自动机“有一些理论局限性”:

.．.所涉及的量应该使人怀疑，主要基于状态图的有限性的定理和论证可能没有太大的意义。

It can also be decided automatically whether a nondeterministic machine with finite memory halts on none, some, or all of the possible sequences of nondeterministic decisions, by enumerating states after each possible decision.

【最终版】它还可以通过枚举每个可能的决策之后的状态，自动决定具有有限内存的不确定性机器是否停止于无、部分或所有可能的非确定性决策序列上。

History历史

The halting problem is historically important because it was one of the first problems to be proved undecidable. (Turing's proof went to press in May 1936, whereas Alonzo Church's proof of the undecidability of a problem in the lambda calculus had already been published in April 1936 [Church, 1936].) Subsequently, many other undecidable problems have been described.

【最终版】停机问题在历史上很重要，因为它是第一个被证明是不可决定的问题之一。(图灵的证明在1936年5月付印，而Alonzo Church对lambda微积分中一个问题的不可判定性的证明已经在1936年4月发表[Church, 1936]。)随后，又叙述了许多其他无法决定的问题。

Timeline时间轴

• 1900: David Hilbert poses his "23 questions" (now known as Hilbert's problems) at the Second International Congress of Mathematicians in Paris. "Of these, the second was that of proving the consistency of the 'Peano axioms' on which, as he had shown, the rigour of mathematics depended". (Hodges p. 83, Davis' commentary in Davis, 1965, p. 108)

• 1920–1921: Emil Post explores the halting problem for tag systems, regarding it as a candidate for unsolvability. (Absolutely unsolvable problems and relatively undecidable propositions – account of an anticipation, in Davis, 1965, pp. 340–433.) Its unsolvability was not established until much later, by Marvin Minsky (1967).

In his original proof Turing formalized the concept of algorithm by introducing Turing machines. However, the result is in no way specific to them; it applies equally to any other model of computation that is equivalent in its computational power to Turing machines, such as Markov algorithms, Lambda calculus, Post systems, register machines, or tag systems.

在图灵最初的证明中，图灵通过引入图灵机使算法的概念形式化。然而，这个结果并不是特定于他们的; 它同样适用于任何其他在计算能力上等同于图灵机的计算模型，比如马尔可夫算法，Lambda 演算，Post 系统，寄存器机器，或者标签系统。

【最终版】1900年，在巴黎举行的第二届国际数学家大会上，大卫·希尔伯特提出了他的“23个问题”(现在被称为希尔伯特问题)。"第二个问题是证明"皮亚诺公理"的一致性，正如他所证明的，数学的严谨性依赖于"(Hodges，第83页，Davis的评论，Davis, 1965，第108页)

1920-1921: Emil Post研究了标签系统的停止问题，将其视为不可解决的候选者。(绝对无法解决的问题和相对无法决定的命题——对预期的解释，戴维斯，1965，第340-433页)它的不可解性直到很久以后才由马文·明斯基(1967)确立。

在他最初的证明中，图灵通过引入图灵机来形式化算法的概念。然而，结果并不是针对他们的;它同样适用于计算能力与图灵机相当的任何其他计算模型，如马尔可夫算法、Lambda演算、Post系统、寄存器机或标记系统。

• 1928: Hilbert recasts his 'Second Problem' at the Bologna International Congress. (Reid pp. 188–189) Hodges claims he posed three questions: i.e. #1: Was mathematics complete? #2: Was mathematics consistent? #3: Was mathematics decidable? (Hodges p. 91). The third question is known as the Entscheidungsproblem (Decision Problem). (Hodges p. 91, Penrose p. 34)

• 1930: Kurt Gödel announces a proof as an answer to the first two of Hilbert's 1928 questions [cf Reid p. 198]. "At first he [Hilbert] was only angry and frustrated, but then he began to try to deal constructively with the problem... Gödel himself felt—and expressed the thought in his paper—that his work did not contradict Hilbert's formalistic point of view" (Reid p. 199)

What is important is that the formalization allows a straightforward mapping of algorithms to some data type that the algorithm can operate upon. For example, if the formalism lets algorithms define functions over strings (such as Turing machines) then there should be a mapping of these algorithms to strings, and if the formalism lets algorithms define functions over natural numbers (such as computable functions) then there should be a mapping of algorithms to natural numbers. The mapping to strings is usually the most straightforward, but strings over an alphabet with n characters can also be mapped to numbers by interpreting them as numbers in an n-ary numeral system.

重要的是，形式化允许将算法直接映射到算法可以操作的某种数据类型。例如，如果形式主义允许算法在字符串上定义函数(比如图灵机) ，那么这些算法应该有一个到字符串的映射; 如果形式主义允许算法在自然数上定义函数(比如可计算函数) ，那么应该有一个算法到自然数的映射。映射到字符串通常是最简单的，但是字母表上有 n 个字符的字符串也可以通过解释为 n 元数字系统中的数字来映射到数字。

【最终版】1928年:希尔伯特在博洛尼亚国际会议上重新阐述了他的“第二个问题”。(Reid pp. 188-189) Hodges声称他提出了三个问题:第一:数学是完整的吗?2 .数学是一致的吗?#3:数学是可决定的吗?霍奇斯(p。91)。第三个问题被称为“决策问题”。(霍奇斯，91页，彭罗斯，34页)

1930:库尔特Gödel宣布一个证明作为希尔伯特1928年提出的前两个问题的答案[cf Reid p. 198]。“一开始他(希尔伯特)只是生气和沮丧，但后来他开始尝试建设性地处理问题……Gödel自己在他的论文中感觉并表达了这样的想法:他的工作与希尔伯特的形式主义观点并不矛盾”(Reid p. 199)。

重要的是，形式化允许将算法直接映射到算法可以操作的某些数据类型。例如,如果形式允许算法定义函数在字符串(如图灵机),那么应该有一个映射这些算法的字符串,如果形式允许算法定义函数在自然数(如可计算函数),那么应该有一个自然数的映射算法。到字符串的映射通常是最直接的，但是包含n个字符的字母表上的字符串也可以通过将它们解释为n-ary数字系统中的数字来映射为数字。

• 1931: Gödel publishes "On Formally Undecidable Propositions of Principia Mathematica and Related Systems I", (reprinted in Davis, 1965, p. 5ff)

• 19 April 1935: Alonzo Church publishes "An Unsolvable Problem of Elementary Number Theory", wherein he identifies what it means for a function to be effectively calculable. Such a function will have an algorithm, and "...the fact that the algorithm has terminated becomes effectively known ..." (Davis, 1965, p. 100)

• 1936: Church publishes the first proof that the Entscheidungsproblem is unsolvable. (A Note on the Entscheidungsproblem, reprinted in Davis, 1965, p. 110.)

• 7 October 1936: Emil Post's paper "Finite Combinatory Processes. Formulation I" is received. Post adds to his "process" an instruction "(C) Stop". He called such a process "type 1 ... if the process it determines terminates for each specific problem." (Davis, 1965, p. 289ff)

• 1937: Alan Turing's paper On Computable Numbers With an Application to the Entscheidungsproblem reaches print in January 1937 (reprinted in Davis, 1965, p. 115). Turing's proof departs from calculation by recursive functions and introduces the notion of computation by machine. Stephen Kleene (1952) refers to this as one of the "first examples of decision problems proved unsolvable".

The conventional representation of decision problems is the set of objects possessing the property in question. The halting set

决策问题的常规表示是具有问题属性的对象集合。停顿集

【最终版】1931年:Gödel发表《数学原理与相关系统的形式不可定命题》(1965年在Davis再版，第5ff页)

1935年4月19日:阿朗佐·丘奇出版了《初等数论的一个不可解的问题》，在这本书中，他确定了一个函数是可以有效计算的。这样的函数将有一个算法，并且“…算法已经终止的事实被有效地知道了……”(戴维斯，1965，第100页)

1936年:教会发表了第一个证明，判罪问题是不可解决的。(《关于判择问题的注释》，转载于Davis, 1965年，第110页。)

1936年10月7日:Emil Post的论文《有限组合过程》。收到提法一“。Post在他的“过程”中添加了一个指令“(C)停止”。他称这种过程为“1型……如果它确定的过程为每个特定的问题终止。”(Davis, 1965，第289ff页)

1937年1月，艾伦·图灵的论文《论可计算数及其在可判命题问题中的应用》付印(戴维斯出版社1965年再版，第115页)。图灵的证明脱离了递归函数计算，引入了机器计算的概念。斯蒂芬·克林(Stephen Kleene, 1952)将此称为“第一个被证明是无法解决的决策问题的例子”。

决策问题的传统表示是具有问题属性的对象集合。停止集

• 1939: J. Barkley Rosser observes the essential equivalence of "effective method" defined by Gödel, Church, and Turing (Rosser in Davis, 1965, p. 273, "Informal Exposition of Proofs of Gödel's Theorem and Church's Theorem")

K = {(i, x) | program i halts when run on input x}

K = {(i，x) | program i halts when run on input x }

• 1943: In a paper, Stephen Kleene states that "In setting up a complete algorithmic theory, what we do is describe a procedure ... which procedure necessarily terminates and in such manner that from the outcome we can read a definite answer, 'Yes' or 'No,' to the question, 'Is the predicate value true?'."

represents the halting problem.

表示停机问题。

【最终版】1939: J. Barkley Rosser观察到Gödel、Church和Turing定义的“有效方法”的本质等价性(Rosser在Davis, 1965，第273页，“Gödel定理和Church定理的证明的非正式阐述”)。

K = {(i, x) |程序i在输入x上运行时停止}

K = {(i,x) |程序i在输入x上运行时停止}

1943年:在一篇论文中，Stephen Kleene指出:“在建立一个完整的算法理论时，我们所做的是描述一个过程……这个过程必然终止，并且通过这种方式，我们可以从结果中对"谓词的值是真吗"这个问题读到一个肯定的回答"是"或"不是"

表示停机问题。

• 1952: Kleene (1952) Chapter XIII ("Computable Functions") includes a discussion of the unsolvability of the halting problem for Turing machines and reformulates it in terms of machines that "eventually stop", i.e. halt: "... there is no algorithm for deciding whether any given machine, when started from any given situation, eventually stops." (Kleene (1952) p. 382)

• 1952: "Martin Davis thinks it likely that he first used the term 'halting problem' in a series of lectures that he gave at the Control Systems Laboratory at the University of Illinois in 1952 (letter from Davis to Copeland, 12 December 2001)." (Footnote 61 in Copeland (2004) pp. 40ff)

This set is recursively enumerable, which means there is a computable function that lists all of the pairs (i, x) it contains. However, the complement of this set is not recursively enumerable.

这个集合是递归可枚举的，这意味着有一个可计算函数列表它包含的所有对(i，x)。然而，这个集合的补集并不是递归的可枚举的。

【最终版】1952: Kleene(1952)第十三章(“可计算函数”)讨论了图灵机停止问题的不可解性，并将其重新表述为“最终停止”的机器，即停止:“…没有一种算法可以决定任何一台给定的机器，在任何给定的情况下启动时，是否最终停止。”(克林(1952)第382页)

1952年:“马丁·戴维斯认为，他可能是在1952年在伊利诺伊大学控制系统实验室的一系列讲座中首次使用‘停止问题’这个术语的(2001年12月12日，戴维斯写给科普兰的信)。”(Copeland(2004)第40ff页脚注61)

这个集合是递归可枚举的，这意味着有一个可计算的函数列出了它包含的所有对(i, x)。然而，这个集合的补集不是递归可枚举的。

Formalization形式化

There are many equivalent formulations of the halting problem; any set whose Turing degree equals that of the halting problem is such a formulation. Examples of such sets include:

停机问题有许多等价公式，任何图灵度等于停机问题的集合就是这样的公式。这类集合的例子包括:

【最终版】停机问题有许多等价的表述;任何其图灵度等于停机问题的集合就是这样一个公式。这类集合的例子包括:

In his original proof Turing formalized the concept of algorithm by introducing Turing machines. However, the result is in no way specific to them; it applies equally to any other model of computation that is equivalent in its computational power to Turing machines, such as Markov algorithms, Lambda calculus, Post systems, register machines, or tag systems.

【最终版】在他最初的证明中，图灵通过引入图灵机来形式化算法的概念。然而，结果并不是针对他们的;它同样适用于计算能力与图灵机相当的任何其他计算模型，如马尔可夫算法、Lambda演算、Post系统、寄存器机或标记系统。

What is important is that the formalization allows a straightforward mapping of algorithms to some data type that the algorithm can operate upon. For example, if the formalism lets algorithms define functions over strings (such as Turing machines) then there should be a mapping of these algorithms to strings, and if the formalism lets algorithms define functions over natural numbers (such as computable functions) then there should be a mapping of algorithms to natural numbers. The mapping to strings is usually the most straightforward, but strings over an alphabet with n characters can also be mapped to numbers by interpreting them as numbers in an n-ary numeral system.

【最终版】重要的是，形式化允许将算法直接映射到算法可以操作的某些数据类型。例如,如果形式允许算法定义函数在字符串(如图灵机),那么应该有一个映射这些算法的字符串,如果形式允许算法定义函数在自然数(如可计算函数),那么应该有一个自然数的映射算法。到字符串的映射通常是最直接的，但是包含n个字符的字母表上的字符串也可以通过将它们解释为n-ary数字系统中的数字来映射为数字。

Representation as a set表示为一个集合

The proof that the halting problem is not solvable is a proof by contradiction. To illustrate the concept of the proof, suppose that there exists a total computable function halts(f) that returns true if the subroutine f halts (when run with no inputs) and returns false otherwise. Now consider the following subroutine:

停机问题无法解决的证据是一个反证法。为了说明证明的概念，假设存在一个完全的可计算函数停止(f) ，如果子例程 f 停止(当没有输入时)并返回 false，那么它返回 true。现在考虑下面的子程序:

【最终版】停止问题不可解的证明是矛盾证明。为了说明证明的概念，假设存在一个总可计算函数停止(f)，如果子例程f停止(在没有输入的情况下运行)，则返回true，否则返回false。现在考虑下面的子例程:

Main article: Decision problem

< syntaxhighlight lang = " python" > 

The conventional representation of decision problems is the set of objects possessing the property in question. The ''halting set''

def g():

() :

: ''K'' = {(''i'', ''x'') | program ''i'' halts when run on input ''x''}

    if halts(g):

如果中止(g) :

represents the halting problem.

        loop_forever()

循环永远()

</syntaxhighlight >

This set is recursively enumerable, which means there is a computable function that lists all of the pairs (i, x) it contains. However, the complement of this set is not recursively enumerable.

【最终版】这个集合是递归可枚举的，这意味着有一个可计算的函数列出了它包含的所有对(i, x)。然而，这个集合的补集不是递归可枚举的。

halts(g) must either return true or false, because halts was assumed to be total. If halts(g) returns true, then g will call loop_forever and never halt, which is a contradiction. If halts(g) returns false, then g will halt, because it will not call loop_forever; this is also a contradiction. Overall, halts(g) can not return a truth value that is consistent with whether g halts. Therefore, the initial assumption that halts is a total computable function must be false.

Halts (g)必须返回 true 或 false，因为 halts 被假定为 total。如果 halt (g)返回 true，那么 g 将永远调用 loop _ 而且永远不会停止，这是一个矛盾。如果 halt (g)返回 false，那么 g 将停止，因为它不会永远调用 loop; 这也是一个矛盾。总的来说，停止(g)不能返回与 g 是否停止一致的真值。因此，最初的假设，停止是一个完全的可计算函数，肯定是错误的。

【最终版】暂停(g)必须返回true或false，因为暂停被假定为全部。如果halts(g)返回true，那么g将调用loop_forever并永不停止，这是一个矛盾。如果halts(g)返回false，那么g将停止，因为它不会调用loop_forever;这也是一个矛盾。总的来说，halt (g)不能返回一个与g是否halt一致的真值。因此，初始假设halts是一个完全可计算的函数肯定是错误的。

There are many equivalent formulations of the halting problem; any set whose Turing degree equals that of the halting problem is such a formulation. Examples of such sets include:

• {i | program i eventually halts when run with input 0}

The method used in the proof is called diagonalization - g does the opposite of what halts says g should do. The difference between this sketch and the actual proof is that in the actual proof, the computable function halts does not directly take a subroutine as an argument; instead it takes the source code of a program. The actual proof requires additional work to handle this issue. Moreover, the actual proof avoids the direct use of recursion shown in the definition of g.

证明中使用的方法被称为对角化-g 做了与停止说 g 应该做的相反的事。这个示意图和实际证明的不同之处在于，在实际证明中，可计算函数中止并不直接将子例程作为参数，而是采用程序的源代码。实际的证明需要额外的工作来处理这个问题。此外，实际证明避免了直接使用递归的定义。

【最终版】停机问题有许多等价的表述;任何其图灵度等于停机问题的集合就是这样一个公式。这类集合的例子包括:

{i |程序最终停止运行时输入0}

在证明中使用的方法被称为对角化——g所做的与停止说g应该做的相反。这个草图和实际的证明之间的区别是，在实际的证明中，可计算函数停止不直接采取一个子程序作为参数;相反，它接受程序的源代码。实际的证明需要额外的工作来处理这个问题。而且，实际证明避免了直接使用g的定义中所示的递归。

• {i | there is an input x such that program i eventually halts when run with input x}.

【最终版】{i |有一个输入x，使得程序i在运行输入x时最终停止运行}。

Proof concept证据的概念

The concept above shows the general method of the proof; this section will present additional details. The overall goal is to show that there is no total computable function that decides whether an arbitrary program i halts on arbitrary input x; that is, the following function h is not computable (Penrose 1990, p. 57–63):

上面的概念展示了证明的一般方法; 本节将提供更多的细节。总体目标是证明不存在总可计算函数来决定一个任意程序是否在任意输入 x 上停止运行; 也就是说，下面的函数 h 是不可计算的(Penrose 1990，p. 57-63) :

【最终版】上述概念给出了证明的一般方法;本节将介绍更多的细节。总的目标是要证明，没有一个完全可计算的函数来决定任意程序i是否在任意输入x上停止;即下列函数h是不可计算的(Penrose 1990, p. 57-63):

The proof that the halting problem is not solvable is a proof by contradiction. To illustrate the concept of the proof, suppose that there exists a total computable function halts(f) that returns true if the subroutine f halts (when run with no inputs) and returns false otherwise. Now consider the following subroutine:

[math]\displaystyle{ h(i,x) = \lt math \gt h (i，x) = \lt syntaxhighlight lang="python"\gt \begin{cases} 开始{ cases } def g(): 1 & \text{if } \text{ program }i\text{ halts on input }x, \\ 1 & text { if } text { program } i text { halt on input } x, if halts(g): 0 & \text{otherwise.} 0 & text { otherwise. } loop_forever() \end{cases} }[/math]

结束{ cases } </math >

</syntaxhighlight>

【最终版】停止问题不可解的证明是矛盾证明。为了说明证明的概念，假设存在一个总可计算函数停止(f)，如果子例程f停止(在没有输入的情况下运行)，则返回true，否则返回false。现在考虑下面的子例程:

Here program i refers to the i th program in an enumeration of all the programs of a fixed Turing-complete model of computation.

这里程序 i 指的是一个固定的图灵完全计算模型的所有程序的枚举中的第 i 个程序。

【最终版】这里程序i指的是一个固定图灵完备计算模型中所有程序的枚举中的第i个程序。

halts(g) must either return true or false, because halts was assumed to be total. If halts(g) returns true, then g will call loop_forever and never halt, which is a contradiction. If halts(g) returns false, then g will halt, because it will not call loop_forever; this is also a contradiction. Overall, halts(g) can not return a truth value that is consistent with whether g halts. Therefore, the initial assumption that halts is a total computable function must be false.

2em; width: 2.7in; background: white; " >

Here program i refers to the i th program in an enumeration of all the programs of a fixed Turing-complete model of computation.

f(i,j)		f (i，j) Sketch of proof素描的证明	i 6 style = “ background: # f2f2f2; ” | i
		1 2f2f2; width: 24.75; ” | 1	2 2f2f2; width: 24.75; ” | 2 [math]\displaystyle{ h(i,x) = | style="background:#f2f2f2; width:24.75;"| 3 2f2f2; width: 24.75; ” | 3 \begin{cases} | style="background:#f2f2f2; width:24.75;"| 4 2f2f2; width: 24.75; ” | 4 1 & \text{if } \text{ program }i\text{ halts on input }x, \\ | style="background:#f2f2f2; width:24.75;"| 5 2f2f2; width: 24.75; ” | 5 0 & \text{otherwise.} | style="background:#f2f2f2; width:24.75;"| 6 2f2f2; width: 24.75; ” | 6 \end{cases} }[/math]
j 2f2f2; height: 12px; width: 18.75; “ rowspan = 6 valign = center | j	1 2f2f2; ” | 1	1 “ style = ”背景: # ffc000; “ | 1 0 0 0 0 f(i,j) 1 1 i 0 0 1 1 1 2 2 2f2f2; ” | | 2 3 0 0 4 0 “ style = ”背景: # ffc000; “ | 0 5 0 0 6 1 1 0 0 j 0 0 1 1 3 2f2f2; ” | | 3 0 0 0 0 1 1 1 0 “ style = ”背景: # ffc000; “ | 0 0 1 1 1 0 0 1 1 2 0 4 2f2f2; ” | 4 0 1 1 0 0 0 1 0 0 0 1 “ style = ”背景: # ffc000; “ | 1 0 0 0 0 0 3 0 5 2f2f2; ” | | 5 1 0 0 0 0 0 1 0 0 0 1 1 1 1 “ style = ”背景: # ffc000; “ | 1 1 1 4 1 6 2f2f2; ” | 6 0 1 1 0 1 1 1 0 0 0 0 0 0 1 1 0 “ style = ”背景: # ffc000; “ | 0 5 0 12px; | 0 0 1 1 1 6 1 1 12px; | 0 f(i,i) [ style = “ background: # ffc000; ”][ i，i ] 0 1 “ style = ”背景: # ffc000; “ | 1 1 0 “ style = ”背景: # ffc000; “ | 0 0 0 “ style = ”背景: # ffc000; “ | 0 1 “ style = ”背景: # ffc000; “ | 1 1 “ style = ”背景: # ffc000; “ | 1 0 “ style = ”背景: # ffc000; “ | 0 12px; | g(i) 99ff8b; ” | g (i) U 99ff8b; ” | u 0 99ff8b; ” | 0 0 99ff8b; ” | 0 U 99ff8b; ” | u U 99ff8b; ” | u f(i,i) 0 99ff8b; ” | 0 1

| style="background:#ffc000;"| 0

Possible values for a total computable function f arranged in a 2D array. The orange cells are the diagonal. The values of f(i,i) and g(i) are shown at the bottom; U indicates that the function g is undefined for a particular input value.

2 d 数组排列的总可计算函数 f 的可能值。橙色的单元格是对角线。F (i，i)和 g (i)的值显示在底部; u 表示函数 g 没有为特定的输入值定义。

| style="background:#ffc000;"| 0

| style="background:#ffc000;"| 1

| style="background:#ffc000;"| 1

The proof proceeds by directly establishing that no total computable function with two arguments can be the required function h. As in the sketch of the concept, given any total computable binary function f, the following partial function g is also computable by some program e:

证明的过程是直接确定任何带有两个参数的可计算函数都不能是所需的函数 h。在概念的示意图中，给定任意可计算的二元函数 f，下面的部分函数 g 也可由某些程序计算:

| style="background:#ffc000;"| 0

【最终版】证明通过直接建立两个参数的完全可计算函数不可能是所需要的函数h来进行。在这个概念的概略中，给定任何一个完全可计算的二元函数f，下面的部分函数g也可以被某个程序e计算:

[math]\displaystyle{ g(i) = \lt math \gt g (i) = |- style="font-size:9pt; text-align:center; vertical-align:bottom;" \begin{cases} 开始{ cases } | style="height:12px;"| 0 & \text{if } f(i,i) = 0,\\ 0 & text { if } f (i，i) = 0, | style="background:#99ff8b;"| ''g''(''i'') \text{undefined} & \text{otherwise.} 文本{ undefined } & text { otherwise. } | style="background:#99ff8b;"| U \end{cases} }[/math]

结束{ cases } </math >

| style="background:#99ff8b;"| 0

| style="background:#99ff8b;"| 0

The verification that g is computable relies on the following constructs (or their equivalents):

G 是可计算的验证依赖于以下构造(或者它们的等价物) :

| style="background:#99ff8b;"| U

| style="background:#99ff8b;"| U

| style="background:#99ff8b;"| 0

|}

【最终版】结束{ cases } </math >

| style="background:#99ff8b;"| 0

| style="background:#99ff8b;"| 0

g是可计算的验证依赖于以下结构(或它们的等价结构):

Possible values for a total computable function f arranged in a 2D array. The orange cells are the diagonal. The values of f(i,i) and g(i) are shown at the bottom; U indicates that the function g is undefined for a particular input value.

The following pseudocode illustrates a straightforward way to compute g:

下面的伪代码展示了一种简单的计算 g 的方法:

【最终版】下面的伪代码演示了一种计算g的简单方法:

The proof proceeds by directly establishing that no total computable function with two arguments can be the required function h. As in the sketch of the concept, given any total computable binary function f, the following partial function g is also computable by some program e:

[math]\displaystyle{ g(i) = \lt div style="width: 50%;"\gt \lt div style = " width: 50% ; " \gt \begin{cases} \lt !-- the following code is not Pascal, but that option makes the highlighting work correctly --\gt \lt ! -- 下面的代码不是 pascal，但是这个选项可以使高亮显示正确工作 -- \gt 0 & \text{if } f(i,i) = 0,\\ \lt syntaxhighlight lang="pascal"\gt “ syntaxhighlight lang = " pascal" \text{undefined} & \text{otherwise.} procedure compute_g(i): 过程计算 _ g (i) : \end{cases} }[/math]

   if f(i, i) == 0 then

如果 f (i，i) = 0

       return 0

返回0

The verification that g is computable relies on the following constructs (or their equivalents):

   else

别的

• computable subprograms (the program that computes f is a subprogram in program e),

       loop forever

永远循环

• duplication of values (program e computes the inputs i,i for f from the input i for g),

</syntaxhighlight>

</syntaxhighlight >

• conditional branching (program e selects between two results depending on the value it computes for f(i,i)),

• not producing a defined result (for example, by looping forever),

• returning a value of 0.

Because g is partial computable, there must be a program e that computes g, by the assumption that the model of computation is Turing-complete. This program is one of all the programs on which the halting function h is defined. The next step of the proof shows that h(e,e) will not have the same value as f(e,e).

因为 g 是部分可计算的，所以假设计算模型是图灵完全的，那么一定有一个程序可以计算 g。这个程序是所有用来定义停止函数 h 的程序之一。证明的下一步显示 h (e，e)的值不会与 f (e，e)的值相同。

【最终版】因为g是部分可计算的，所以在假设计算模型是图灵完备的情况下，必须有一个程序e来计算g。这个程序是所有定义了停止函数h的程序之一。证明的下一步表明h(e,e)不会和f(e,e)有相同的值。

The following pseudocode illustrates a straightforward way to compute g:

It follows from the definition of g that exactly one of the following two cases must hold:

根据 g 的定义，下列两种情况之一必须成立:

【最终版】下面的伪代码演示了一种计算g的简单方法:

由g的定义可以得出以下两种情况中的一种必须成立:

In either case, f cannot be the same function as h. Because f was an arbitrary total computable function with two arguments, all such functions must differ from h.

在这两种情况下，f 都不可能是 h 的同一个函数，因为 f 是一个任意的总可计算函数，有两个参数，所有这些函数都必须与 h 不同。

【最终版】在任何一种情况下，f都不能和h是同一个函数。因为f是一个任意的具有两个参数的完全可计算函数，所以所有这些函数都必须不同于h。

procedure compute_g(i):

This proof is analogous to Cantor's diagonal argument. One may visualize a two-dimensional array with one column and one row for each natural number, as indicated in the table above. The value of f(i,j) is placed at column i, row j. Because f is assumed to be a total computable function, any element of the array can be calculated using f. The construction of the function g can be visualized using the main diagonal of this array.  If the array has a 0 at position (i,i), then g(i) is 0. Otherwise, g(i) is undefined. The contradiction comes from the fact that there is some column e of the array corresponding to g itself. Now assume f was the halting function h, if g(e) is defined (g(e) = 0 in this case), g(e) halts so f(e,e) = 1.  But g(e) = 0 only when f(e,e) = 0, contradicting f(e,e) = 1. Similarly, if g(e) is not defined, then halting function f(e,e) = 0, which leads to g(e) = 0 under gs construction. This contradicts the assumption of g(e) not being defined. In both cases contradiction arises. Therefore any arbitrary computable function f cannot be the halting function h.

这个证明类似于康托尔的对角线论证。人们可以想象一个二维数组，每个自然数有一列和一行，如上表所示。F (i，j)的值放在第 i 列 j 行。因为假设 f 是总可计算函数，所以可以使用 f 计算数组的任何元素。函数 g 的构造可以用这个数组的主对角线可视化。如果数组的位置(i，i)是0，那么 g (i)是0。否则，g (i)是未定义的。这个矛盾来自于这样一个事实: 数组中有一些 e 列对应于 g 本身。现在假设 f 是停止函数 h，如果定义了 g (e)(g (e) = 0) ，g (e)停止，那么 f (e，e) = 1。但是只有当 f (e，e) = 0时，g (e) = 0，与 f (e，e) = 1相矛盾。类似地，如果没有定义 g (e) ，那么停止函数 f (e，e) = 0，这导致 g (e) = 0在 gs 构造下。这与 g (e)没有被定义的假设相矛盾。在这两种情况下都会产生矛盾。因此，任意的可计算函数 f 都不能是停机函数 h。

    if f(i, i) == 0 then

        return 0

    else

        loop forever

The typical method of proving a problem to be undecidable is with the technique of reduction. To do this, it is sufficient to show that if a solution to the new problem were found, it could be used to decide an undecidable problem by transforming instances of the undecidable problem into instances of the new problem. Since we already know that no method can decide the old problem, no method can decide the new problem either. Often the new problem is reduced to solving the halting problem. (The same technique is used to demonstrate that a problem is NP complete, only in this case, rather than demonstrating that there is no solution, it demonstrates there is no polynomial time solution, assuming P ≠ NP.)

证明一个问题不可判定的典型方法是用归约技巧。要做到这一点，只要证明如果找到了新问题的解决方案，就可以用它来决定一个不可解问题，将不可解问题的实例转换为新问题的实例。既然我们已经知道没有方法可以决定旧的问题，那么也没有方法可以决定新的问题。通常，新问题被简化为停机问题的求解。(同样的技巧被用来证明一个问题是 NP 完全的，只是在这种情况下，不是证明没有解，而是证明假设 p ≠ NP，没有多项式时间解。)

【最终版】证明问题为不可定的典型方法是用约简技术。要做到这一点，只要证明如果找到了新问题的解决方案，就可以用它来决定一个不可决定的问题，方法是将不可决定问题的实例转换为新问题的实例。既然我们已经知道没有一种方法可以决定老问题，那么也没有一种方法可以决定新问题。通常新问题被简化为解决停机问题。(同样的技巧被用来证明一个问题是NP完备的，只是在这种情况下，它不是证明没有解，而是证明没有多项式时间解，假设P≠NP。)

For example, one such consequence of the halting problem's undecidability is that there cannot be a general algorithm that decides whether a given statement about natural numbers is true or false. The reason for this is that the proposition stating that a certain program will halt given a certain input can be converted into an equivalent statement about natural numbers. If we had an algorithm that could find the truth value of every statement about natural numbers, it could certainly find the truth value of this one; but that would determine whether the original program halts, which is impossible, since the halting problem is undecidable.

例如，停机问题的不可判定性的一个这样的结果是，不可能有一个一般的算法来决定一个给定的关于自然数的陈述是真还是假。其原因在于，某个程序在给定某个输入时会停止的命题可以转换成关于自然数的等价命题。如果我们有一个算法，可以找到关于自然数的每个语句的真值，它肯定可以找到这个语句的真值; 但这将决定原始程序是否停止，这是不可能的，因为停止问题是不可判定的。

【最终版】例如，停止问题的不可判定性的一个这样的结果是，不可能有一个通用的算法来决定一个给定的自然数的陈述是真还是假。这样做的原因是，某个程序在给定特定输入后会停止的命题，可以转换成关于自然数的等价命题。如果我们有一个算法可以找到每个自然数命题的真值，它肯定可以找到这个命题的真值;但这将决定最初的程序是否停止，这是不可能的，因为停止问题是不可决定的。

Because g is partial computable, there must be a program e that computes g, by the assumption that the model of computation is Turing-complete. This program is one of all the programs on which the halting function h is defined. The next step of the proof shows that h(e,e) will not have the same value as f(e,e).

Rice's theorem generalizes the theorem that the halting problem is unsolvable. It states that for any non-trivial property, there is no general decision procedure that, for all programs, decides whether the partial function implemented by the input program has that property. (A partial function is a function which may not always produce a result, and so is used to model programs, which can either produce results or fail to halt.) For example, the property "halt for the input 0" is undecidable. Here, "non-trivial" means that the set of partial functions that satisfy the property is neither the empty set nor the set of all partial functions. For example, "halts or fails to halt on input 0" is clearly true of all partial functions, so it is a trivial property, and can be decided by an algorithm that simply reports "true." Also, this theorem holds only for properties of the partial function implemented by the program; Rice's Theorem does not apply to properties of the program itself. For example, "halt on input 0 within 100 steps" is not a property of the partial function that is implemented by the program—it is a property of the program implementing the partial function and is very much decidable.

赖斯定理推广了停机问题不可解的定理。它指出，对于任何非平凡属性，没有一般的决策过程，对于所有程序，决定输入程序实现的部分函数是否具有该属性。(部分函数是一个可能不总是产生结果的函数，因此用于为程序建模，它可以产生结果，也可以不停止。)例如，属性“输入0的暂停”是不可判定的。在这里，“非平凡”意味着满足该属性的部分函数集既不是空集，也不是所有部分函数的集。例如，“ halt or fails to halt on input 0”显然适用于所有部分函数，因此它是一个平凡的属性，可以由简单报告“ true”的算法来决定此外，这个定理仅适用于由程序实现的部分函数的性质; 赖斯定理不适用于程序本身的性质。例如，“输入0在100步内停止”不是由程序实现的部分函数的性质ーー它是实现部分函数的程序的性质，是非常可判定的。

【最终版】赖斯定理推广了停机问题不可解的定理。它指出，对于任何重要的属性，没有一个通用的决策过程来决定输入程序实现的部分函数是否具有该属性。(部分函数是一种不一定总是产生结果的函数，因此用于对程序进行建模，程序既可以产生结果，也可以停止。)例如，属性“halt For the input 0”是不可判定的。这里，“非平凡”是指满足这个性质的部分函数集既不是空集，也不是所有部分函数的集合。例如，“在输入0时停止或停止失败”显然对所有部分函数都是正确的，所以这是一个微不足道的属性，可以通过一个简单地报告“true”的算法来决定。而且，这个定理只适用于由程序实现的部分函数的性质;赖斯定理并不适用于程序本身的性质。例如，“在100步内暂停输入0”并不是由程序实现的部分函数的属性——它是实现部分函数的程序的属性，而且非常具有可判定性。

It follows from the definition of g that exactly one of the following two cases must hold:

• f(e,e) = 0 and so g(e) = 0. In this case h(e,e) = 1, because program e halts on input e.

Gregory Chaitin has defined a halting probability, represented by the symbol Ω, a type of real number that informally is said to represent the probability that a randomly produced program halts. These numbers have the same Turing degree as the halting problem. It is a normal and transcendental number which can be defined but cannot be completely computed. This means one can prove that there is no algorithm which produces the digits of Ω, although its first few digits can be calculated in simple cases.

定义了一个柴廷常数，用符号 ω 表示，这是一种实数，非正式的说法是用来表示一个随机产生的程序停止运行的概率。这些数字与停机问题具有相同的图灵度。它是一个正常的超越数，可以定义，但不能完全计算。这意味着人们可以证明，没有算法产生的数字 ω，虽然它的前几位数字可以计算在简单的情况下。

【最终版】由g的定义可以得出以下两种情况中的一种必须成立:

F (e,e) = 0 g(e) = 0。在这种情况下，h(e,e) = 1，因为程序e在输入e时停止。

Gregory Chaitin定义了一个停止概率，用符号Ω表示，这是一种实数，非正式地说，它表示随机产生的程序停止的概率。这些数字与停机问题的图灵度相同。它是一个可以定义但不能完全计算的正规的超越数。这意味着可以证明没有生成Ω的数字的算法，尽管它的前几个数字可以在简单的情况下计算出来。

• f(e,e) ≠ 0 and so g(e) is undefined. In this case h(e,e) = 0, because program e does not halt on input e.

In either case, f cannot be the same function as h. Because f was an arbitrary total computable function with two arguments, all such functions must differ from h.

While Turing's proof shows that there can be no general method or algorithm to determine whether algorithms halt, individual instances of that problem may very well be susceptible to attack. Given a specific algorithm, one can often show that it must halt for any input, and in fact computer scientists often do just that as part of a correctness proof. But each proof has to be developed specifically for the algorithm at hand; there is no mechanical, general way to determine whether algorithms on a Turing machine halt. However, there are some heuristics that can be used in an automated fashion to attempt to construct a proof, which succeed frequently on typical programs. This field of research is known as automated termination analysis.

虽然图灵的证明表明，不可能有一般的方法或算法来确定算法是否停止，该问题的个别实例可能很容易受到攻击。给定一个特定的算法，人们经常可以证明它必须停止任何输入，事实上计算机科学家经常这样做，作为正确性证明的一部分。但是每个证明都必须针对手头的算法进行专门的开发; 没有机械的、通用的方法来确定图灵机上的算法是否停止。然而，有一些启发法可以用于自动构造证明，这在典型的程序中经常成功。这个研究领域被称为自动终止分析。

【最终版】在任何一种情况下，f都不能和h是同一个函数。因为f是一个任意的具有两个参数的完全可计算函数，所以所有这些函数都必须不同于h。

虽然图灵的证明表明，不存在确定算法是否停止的通用方法或算法，但这个问题的个别实例可能很容易受到攻击。给定一个特定的算法，我们通常可以证明它必须为任何输入而停止，事实上，计算机科学家经常这样做，作为正确性证明的一部分。但每个证明都必须针对手头的算法进行;没有一个机械的，通用的方法来确定图灵机上的算法是否停止。然而，有一些启发式方法可以用自动化的方式来尝试构造一个证明，通常在典型的程序上成功。这一研究领域被称为自动终止分析。

This proof is analogous to Cantor's diagonal argument. One may visualize a two-dimensional array with one column and one row for each natural number, as indicated in the table above. The value of f(i,j) is placed at column i, row j. Because f is assumed to be a total computable function, any element of the array can be calculated using f. The construction of the function g can be visualized using the main diagonal of this array. If the array has a 0 at position (i,i), then g(i) is 0. Otherwise, g(i) is undefined. The contradiction comes from the fact that there is some column e of the array corresponding to g itself. Now assume f was the halting function h, if g(e) is defined (g(e) = 0 in this case), g(e) halts so f(e,e) = 1. But g(e) = 0 only when f(e,e) = 0, contradicting f(e,e) = 1. Similarly, if g(e) is not defined, then halting function f(e,e) = 0, which leads to g(e) = 0 under g's construction. This contradicts the assumption of g(e) not being defined. In both cases contradiction arises. Therefore any arbitrary computable function f cannot be the halting function h.

Since the negative answer to the halting problem shows that there are problems that cannot be solved by a Turing machine, the Church–Turing thesis limits what can be accomplished by any machine that implements effective methods. However, not all machines conceivable to human imagination are subject to the Church–Turing thesis (e.g. oracle machines). It is an open question whether there can be actual deterministic physical processes that, in the long run, elude simulation by a Turing machine, and in particular whether any such hypothetical process could usefully be harnessed in the form of a calculating machine (a hypercomputer) that could solve the halting problem for a Turing machine amongst other things. It is also an open question whether any such unknown physical processes are involved in the working of the human brain, and whether humans can solve the halting problem (Copeland 2004, p. 15).

由于对停机问题的否定回答表明，有些问题是图灵机无法解决的，因此丘奇-图灵理论限制了任何实现有效方法的机器所能完成的工作。然而，并非所有人类想象得到的机器都受制于 Church-Turing 论点(例如:。甲骨文机器)。这是一个开放的问题，是否有实际的确定性物理过程，从长远来看，逃避了图灵机的模拟，特别是是否有任何这样的假设过程可以有效地利用的形式，一个机械式计算器，可以解决停机问题的图灵机除了其他事情。这也是一个开放的问题，是否有任何这种未知的物理过程参与了人类大脑的工作，以及人类是否能够解决停机问题(Copeland 2004，第15页)。

【最终版】由于停止问题的否定答案表明存在图灵机无法解决的问题，Church-Turing论文限制了任何实现有效方法的机器所能完成的工作。然而，并不是所有人类想象的机器都符合丘奇-图灵理论(如oracle机器)。从长远来看，是否存在能够逃避图灵机模拟的实际确定性物理过程，这是一个有待解决的问题，特别是，这种假设的过程是否可以有效地用于一台计算机(超级计算机)，从而解决图灵机的停机问题。这些未知的物理过程是否参与到人类大脑的工作中，以及人类是否能够解决停止问题，也是一个有待解决的问题(Copeland 2004, p. 15)。

Computability theory可计算性理论

Main article: Computability theory

The typical method of proving a problem to be undecidable is with the technique of reduction. To do this, it is sufficient to show that if a solution to the new problem were found, it could be used to decide an undecidable problem by transforming instances of the undecidable problem into instances of the new problem. Since we already know that no method can decide the old problem, no method can decide the new problem either. Often the new problem is reduced to solving the halting problem. (The same technique is used to demonstrate that a problem is NP complete, only in this case, rather than demonstrating that there is no solution, it demonstrates there is no polynomial time solution, assuming P ≠ NP.)

For example, one such consequence of the halting problem's undecidability is that there cannot be a general algorithm that decides whether a given statement about natural numbers is true or false. The reason for this is that the proposition stating that a certain program will halt given a certain input can be converted into an equivalent statement about natural numbers. If we had an algorithm that could find the truth value of every statement about natural numbers, it could certainly find the truth value of this one; but that would determine whether the original program halts, which is impossible, since the halting problem is undecidable.

Many variants of the halting problem can be found in computability textbooks (e.g., Sipser 2006, Davis 1958, Minsky 1967, Hopcroft and Ullman 1979, Börger 1989). Typically their undecidability follows by reduction from the standard halting problem. However, some of them have a higher degree of unsolvability. The next two examples are typical.

停顿问题的许多变体可以在可计算性教科书中找到(例如，Sipser 2006，Davis 1958，Minsky 1967，hoplcroft and Ullman 1979，Börger 1989)。通常，它们的不可判定性随着标准停机问题的减少而减少。但是，有些问题具有较高的不可解性。接下来的两个例子是典型的。

【最终版】证明问题为不可定的典型方法是用约简技术。要做到这一点，只要证明如果找到了新问题的解决方案，就可以用它来决定一个不可决定的问题，方法是将不可决定问题的实例转换为新问题的实例。既然我们已经知道没有一种方法可以决定老问题，那么也没有一种方法可以决定新问题。通常新问题被简化为解决停机问题。(同样的技巧被用来证明一个问题是NP完备的，只是在这种情况下，它不是证明没有解，而是证明没有多项式时间解，假设P≠NP。)

例如，停止问题的不可判定性的一个这样的结果是，不可能有一个通用的算法来决定一个给定的自然数的陈述是真还是假。这样做的原因是，某个程序在给定特定输入后会停止的命题，可以转换成关于自然数的等价命题。如果我们有一个算法可以找到每个自然数命题的真值，它肯定可以找到这个命题的真值;但这将决定最初的程序是否停止，这是不可能的，因为停止问题是不可决定的。

停机问题的许多变种可以在可计算性教科书中找到(例如，Sipser 2006, Davis 1958, Minsky 1967, Hopcroft和Ullman 1979, Börger 1989)。一般来说，它们的不可判定性是通过减少标准的停止问题来实现的。然而，其中一些具有较高程度的不可解性。下面两个例子很典型。

Rice's theorem generalizes the theorem that the halting problem is unsolvable. It states that for any non-trivial property, there is no general decision procedure that, for all programs, decides whether the partial function implemented by the input program has that property. (A partial function is a function which may not always produce a result, and so is used to model programs, which can either produce results or fail to halt.) For example, the property "halt for the input 0" is undecidable. Here, "non-trivial" means that the set of partial functions that satisfy the property is neither the empty set nor the set of all partial functions. For example, "halts or fails to halt on input 0" is clearly true of all partial functions, so it is a trivial property, and can be decided by an algorithm that simply reports "true." Also, this theorem holds only for properties of the partial function implemented by the program; Rice's Theorem does not apply to properties of the program itself. For example, "halt on input 0 within 100 steps" is not a property of the partial function that is implemented by the program—it is a property of the program implementing the partial function and is very much decidable.

Gregory Chaitin has defined a halting probability, represented by the symbol Ω, a type of real number that informally is said to represent the probability that a randomly produced program halts. These numbers have the same Turing degree as the halting problem. It is a normal and transcendental number which can be defined but cannot be completely computed. This means one can prove that there is no algorithm which produces the digits of Ω, although its first few digits can be calculated in simple cases.

The universal halting problem, also known (in recursion theory) as totality, is the problem of determining, whether a given computer program will halt for every input (the name totality comes from the equivalent question of whether the computed function is total).

普遍停机问题，也被称为可计算性理论问题，是确定一个给定的计算机程序是否会对每个输入停机的问题(名称的全部来自于计算函数是否为全部的等价问题)。

【最终版】赖斯定理推广了停机问题不可解的定理。它指出，对于任何重要的属性，没有一个通用的决策过程来决定输入程序实现的部分函数是否具有该属性。(部分函数是一种不一定总是产生结果的函数，因此用于对程序进行建模，程序既可以产生结果，也可以停止。)例如，属性“halt For the input 0”是不可判定的。这里，“非平凡”是指满足这个性质的部分函数集既不是空集，也不是所有部分函数的集合。例如，“在输入0时停止或停止失败”显然对所有部分函数都是正确的，所以这是一个微不足道的属性，可以通过一个简单地报告“true”的算法来决定。而且，这个定理只适用于由程序实现的部分函数的性质;赖斯定理并不适用于程序本身的性质。例如，“在100步内暂停输入0”并不是由程序实现的部分函数的属性——它是实现部分函数的程序的属性，而且非常具有可判定性。

Gregory Chaitin定义了一个停止概率，用符号Ω表示，这是一种实数，非正式地说，它表示随机产生的程序停止的概率。这些数字与停机问题的图灵度相同。它是一个可以定义但不能完全计算的正规的超越数。这意味着可以证明没有生成Ω的数字的算法，尽管它的前几个数字可以在简单的情况下计算出来。

通用停止问题(在递归理论中)也称为总体问题(totaltal)，是确定给定的计算机程序是否会在每次输入时停止的问题(totaltal这个名字来自于计算出的函数是否为总体的等价问题)。

This problem is not only undecidable, as the halting problem, but highly undecidable. In terms of the arithmetical hierarchy, it is [math]\displaystyle{ \Pi^0_2 }[/math]-complete (Börger 1989, p. 121).

这个问题不仅是不可判定的问题，而且是高度不可判定的问题。就算数阶层而言，它是 < math > Pi ^ 0 _ 2 </math >-complete (Börger 1989，p. 121)。

【最终版】这个问题不仅像停机问题那样是不可判定的，而且是高度不可判定的。在算术层次结构方面，它是[math]\displaystyle{\Pi^0_2}[/math]-complete (Börger 1989, p. 121)。

While Turing's proof shows that there can be no general method or algorithm to determine whether algorithms halt, individual instances of that problem may very well be susceptible to attack. Given a specific algorithm, one can often show that it must halt for any input, and in fact computer scientists often do just that as part of a correctness proof. But each proof has to be developed specifically for the algorithm at hand; there is no mechanical, general way to determine whether algorithms on a Turing machine halt. However, there are some heuristics that can be used in an automated fashion to attempt to construct a proof, which succeed frequently on typical programs. This field of research is known as automated termination analysis.

This means, in particular, that it cannot be decided even with an oracle for the halting problem.

这尤其意味着，即使对于停机问题有一个预言，也无法做出决定。

【最终版】虽然图灵的证明表明，不存在确定算法是否停止的通用方法或算法，但这个问题的个别实例可能很容易受到攻击。给定一个特定的算法，我们通常可以证明它必须为任何输入而停止，事实上，计算机科学家经常这样做，作为正确性证明的一部分。但每个证明都必须针对手头的算法进行;没有一个机械的，通用的方法来确定图灵机上的算法是否停止。然而，有一些启发式方法可以用自动化的方式来尝试构造一个证明，通常在典型的程序上成功。这一研究领域被称为自动终止分析。

这意味着，特别是，它不能决定，即使是一个暂停问题的预言。

Since the negative answer to the halting problem shows that there are problems that cannot be solved by a Turing machine, the Church–Turing thesis limits what can be accomplished by any machine that implements effective methods. However, not all machines conceivable to human imagination are subject to the Church–Turing thesis (e.g. oracle machines). It is an open question whether there can be actual deterministic physical processes that, in the long run, elude simulation by a Turing machine, and in particular whether any such hypothetical process could usefully be harnessed in the form of a calculating machine (a hypercomputer) that could solve the halting problem for a Turing machine amongst other things. It is also an open question whether any such unknown physical processes are involved in the working of the human brain, and whether humans can solve the halting problem (Copeland 2004, p. 15).

【最终版】由于停止问题的否定答案表明存在图灵机无法解决的问题，Church-Turing论文限制了任何实现有效方法的机器所能完成的工作。然而，并不是所有人类想象的机器都符合丘奇-图灵理论(如oracle机器)。从长远来看，是否存在能够逃避图灵机模拟的实际确定性物理过程，这是一个有待解决的问题，特别是，这种假设的过程是否可以有效地用于一台计算机(超级计算机)，从而解决图灵机的停机问题。这些未知的物理过程是否参与到人类大脑的工作中，以及人类是否能够解决停止问题，也是一个有待解决的问题(Copeland 2004, p. 15)。

Gödel's incompleteness theorems哥德尔不完备定理

{{#lsth:Undecidable problem|Relationship with Gödel's incompleteness theorem}}

There are many programs that, for some inputs, return a correct answer to the halting problem, while for other inputs they do not return an answer at all.

有许多程序，对于某些输入，返回停机问题的正确答案，而对于其他输入，它们根本不返回答案。

【最终版】有很多程序，对于某些输入，会返回停机问题的正确答案，而对于其他输入，它们根本不返回答案。

However the problem "given program p, is it a partial halting solver" (in the sense described) is at least as hard as the halting problem.

然而，“给定程序 p，它是否是一个部分停止求解器”(在所描述的意义上)的问题至少和停止问题一样困难。

【最终版】然而，“给定程序p，它是一个部分停机求解器吗”(在描述的意义上)的问题至少和停机问题一样难。

Generalization泛化

To see this, assume that there is an algorithm PHSR ("partial halting solver recognizer") to do that. Then it can be used to solve the halting problem,

为了看到这一点，假设有一个算法 PHSR (“部分停止求解器识别器”)来做到这一点。然后可以用它来解决停机问题,

【最终版】要了解这一点，假设有一个算法PHSR(“部分停止求解器识别器”)来实现这一点。可用于解决停机问题；

as follows:

详情如下:

Many variants of the halting problem can be found in computability textbooks (e.g., Sipser 2006, Davis 1958, Minsky 1967, Hopcroft and Ullman 1979, Börger 1989). Typically their undecidability follows by reduction from the standard halting problem. However, some of them have a higher degree of unsolvability. The next two examples are typical.

To test whether input program x halts on y, construct a program p that on input (x,y) reports true and diverges on all other inputs.

为了测试输入程序 x 在 y 上是否停止，构造一个程序 p，该程序在输入(x，y)上报告 true，并在所有其他输入上偏离。

Then test p with PHSR.

然后用 PHSR 测试 p。

【最终版】如下:

停机问题的许多变种可以在可计算性教科书中找到(例如，Sipser 2006, Davis 1958, Minsky 1967, Hopcroft和Ullman 1979, Börger 1989)。一般来说，它们的不可判定性是通过减少标准的停止问题来实现的。然而，其中一些具有较高程度的不可解性。下面两个例子很典型。

为了测试输入程序x是否在y上停止，构造一个程序p，它在输入(x,y)上报告为真，并且在所有其他输入上发散。

Halting on all inputs停止所有输入

The above argument is a reduction of the halting problem to PHS recognition, and in the same manner,

以上的论点是一个减少停机问题到 PHS 识别，并以同样的方式,

【最终版】上述论证是将停机问题减少到小灵通识别，同样，

The universal halting problem, also known (in recursion theory) as totality, is the problem of determining, whether a given computer program will halt for every input (the name totality comes from the equivalent question of whether the computed function is total).

harder problems such as halting on all inputs can also be reduced, implying that PHS recognition is not only undecidable, but higher in the arithmetical hierarchy, specifically [math]\displaystyle{ \Pi^0_2 }[/math]-complete.

难度较大的问题，比如所有输入的停顿，也可以减少，这意味着 PHS 识别不仅是无法判定的，而且在算数阶层中更高，特别是 Pi ^ 02 </math >-complete。

【最终版】通用停止问题(在递归理论中)也称为总体问题(totaltal)，是确定给定的计算机程序是否会在每次输入时停止的问题(totaltal这个名字来自于计算出的函数是否为总体的等价问题)。

更困难的问题，如暂停所有输入也可以减少，这意味着PHS识别不仅是不可判断的，而且在更高的算术层次，特别是[math]\displaystyle{\Pi^0_2}[/math]-完整。

This problem is not only undecidable, as the halting problem, but highly undecidable. In terms of the arithmetical hierarchy, it is [math]\displaystyle{ \Pi^0_2 }[/math]-complete (Börger 1989, p. 121).

This means, in particular, that it cannot be decided even with an oracle for the halting problem.

A lossy Turing machine is a Turing machine in which part of the tape may non-deterministically disappear. The Halting problem is decidable for lossy Turing machine but nonprimitive recursive.

损耗图灵机是一种图灵机，其中的一部分磁带可能不确定地消失。有损图灵机的停机问题是可判定的，但它是非本原递归的。

【最终版】这个问题不仅像停机问题那样是不可判定的，而且是高度不可判定的。在算术层次结构方面，它是[math]\displaystyle{\Pi^0_2}[/math]-complete (Börger 1989, p. 121)。

这意味着，特别是，它不能决定，即使是一个暂停问题的预言。

有损耗的图灵机是一种图灵机，其中部分磁带可能会不确定地消失。对于有损耗的图灵机，停机问题是非原语递归的。

Recognizing partial solutions识别部分的解决方案

There are many programs that, for some inputs, return a correct answer to the halting problem, while for other inputs they do not return an answer at all.

A machine with an oracle for the halting problem can determine whether particular Turing machines will halt on particular inputs, but they cannot determine, in general, if machines equivalent to themselves will halt.

一台拥有停机问题预言的机器可以确定特定的图灵机是否会在特定的输入上停机，但是一般来说，它们不能确定等价于它们自己的机器是否会停机。

【最终版】有很多程序，对于某些输入，会返回停机问题的正确答案，而对于其他输入，它们根本不返回答案。

对于停机问题，一个具有oracle的机器可以确定特定的图灵机是否会在特定的输入时停止，但一般来说，它们无法确定等效于自己的机器是否会停止。

However the problem "given program p, is it a partial halting solver" (in the sense described) is at least as hard as the halting problem.

To see this, assume that there is an algorithm PHSR ("partial halting solver recognizer") to do that. Then it can be used to solve the halting problem,

as follows:

To test whether input program x halts on y, construct a program p that on input (x,y) reports true and diverges on all other inputs.

Then test p with PHSR.

The above argument is a reduction of the halting problem to PHS recognition, and in the same manner,

harder problems such as halting on all inputs can also be reduced, implying that PHS recognition is not only undecidable, but higher in the arithmetical hierarchy, specifically [math]\displaystyle{ \Pi^0_2 }[/math]-complete.

【最终版】然而，“给定程序p，它是一个部分停机求解器吗”(在描述的意义上)的问题至少和停机问题一样难。

要了解这一点，假设有一个算法PHSR(“部分停止求解器识别器”)来实现这一点。然后它可以用来解决停机问题，

如下:

为了测试输入程序x是否在y上停止，构造一个程序p，它在输入(x,y)上报告为真，并且在所有其他输入上发散。

然后用PHSR测试p。

Lossy computation损耗计算

A lossy Turing machine is a Turing machine in which part of the tape may non-deterministically disappear. The Halting problem is decidable for lossy Turing machine but nonprimitive recursive.

【最终版】有损耗的图灵机是一种图灵机，其中部分磁带可能会不确定地消失。停机问题对于有损图灵机但非原语递归是可判定的。

See also扩展阅读

• Busy beaver

• Gödel's incompleteness theorem

• Brouwer-Hilbert controversy

• Kolmogorov complexity

• P versus NP problem

• Termination analysis

• Worst-case execution time

忙碌的海狸

哥德尔不完备定理

Brouwer-Hilbert争议

Kolmogorov复杂度

P与NP问题

终止分析

最坏执行时间

References参考文献

• Alan Turing, On computable numbers, with an application to the Entscheidungsproblem, Proceedings of the London Mathematical Society, Series 2, Volume 42 (1937), pp 230–265, doi:10.1112/plms/s2-42.1.230. — Alan Turing, On Computable Numbers, with an Application to the Entscheidungsproblem. A Correction, Proceedings of the London Mathematical Society, Series 2, Volume 43 (1938), pp 544–546, doi:10.1112/plms/s2-43.6.544 . Free online version of both parts This is the epochal paper where Turing defines Turing machines, formulates the halting problem, and shows that it (as well as the Entscheidungsproblem) is unsolvable.

• Sipser, Michael (2006). "Section 4.2: The Halting Problem". Introduction to the Theory of Computation (Second ed.). PWS Publishing. pp. 173–182. ISBN 0-534-94728-X. https://archive.org/details/introductiontoth00sips/page/173. 

• c2:HaltingProblem

• Church, Alonzo (1936). "An Unsolvable Problem of Elementary Number Theory". American Journal of Mathematics. 58 (2): 345–363. doi:10.2307/2371045. JSTOR 2371045.

• B. Jack Copeland ed. (2004), The Essential Turing: Seminal Writings in Computing, Logic, Philosophy, Artificial Intelligence, and Artificial Life plus The Secrets of Enigma, Clarendon Press (Oxford University Press), Oxford UK,
  .
  • Davis, Martin (1965). The Undecidable, Basic Papers on Undecidable Propositions, Unsolvable Problems And Computable Functions. New York: Raven Press. https://archive.org/details/undecidablebasic0000davi. . Turing's paper is #3 in this volume. Papers include those by Godel, Church, Rosser, Kleene, and Post.
  • Davis, Martin (1958). Computability and Unsolvability. New York: McGraw-Hill. .
  • Alfred North Whitehead and Bertrand Russell, Principia Mathematica to *56, Cambridge at the University Press, 1962. Re: the problem of paradoxes, the authors discuss the problem of a set not be an object in any of its "determining functions", in particular "Introduction, Chap. 1 p. 24 "...difficulties which arise in formal logic", and Chap. 2.I. "The Vicious-Circle Principle" p. 37ff, and Chap. 2.VIII. "The Contradictions" p. 60ff.
  • Martin Davis, "What is a computation", in Mathematics Today, Lynn Arthur Steen, Vintage Books (Random House), 1980. A wonderful little paper, perhaps the best ever written about Turing Machines for the non-specialist. Davis reduces the Turing Machine to a far-simpler model based on Post's model of a computation. Discusses Chaitin proof. Includes little biographies of Emil Post, Julia Robinson.
  • Marvin Minsky, Computation: Finite and Infinite Machines, Prentice-Hall, Inc., N.J., 1967. See chapter 8, Section 8.2 "Unsolvability of the Halting Problem."
  • Roger Penrose, The Emperor's New Mind: Concerning computers, Minds and the Laws of Physics, Oxford University Press, Oxford England, 1990 (with corrections). Cf. Chapter 2, "Algorithms and Turing Machines". An over-complicated presentation (see Davis's paper for a better model), but a thorough presentation of Turing machines and the halting problem, and Church's Lambda Calculus.
  • John Hopcroft and Jeffrey Ullman, Introduction to Automata Theory, Languages and Computation, Addison-Wesley, Reading Mass, 1979. See Chapter 7 "Turing Machines." A book centered around the machine-interpretation of "languages", NP-Completeness, etc.
  • Andrew Hodges, Alan Turing: The Enigma, Simon and Schuster, New York. Cf. Chapter "The Spirit of Truth" for a history leading to, and a discussion of, his proof.
  • Constance Reid, Hilbert, Copernicus: Springer-Verlag, New York, 1996 (first published 1970). Fascinating history of German mathematics and physics from 1880s through 1930s. Hundreds of names familiar to mathematicians, physicists and engineers appear in its pages. Perhaps marred by no overt references and few footnotes: Reid states her sources were numerous interviews with those who personally knew Hilbert, and Hilbert's letters and papers.
  • Edward Beltrami, What is Random? Chance and order in mathematics and life, Copernicus: Springer-Verlag, New York, 1999. Nice, gentle read for the mathematically inclined non-specialist, puts tougher stuff at the end. Has a Turing-machine model in it. Discusses the Chaitin contributions.
  • Moore, Cristopher; Mertens, Stephan (2011), The Nature of Computation, Oxford University Press, ISBN 9780191620805
  • Ernest Nagel and James R. Newman, Godel’s Proof, New York University Press, 1958. Wonderful writing about a very difficult subject. For the mathematically inclined non-specialist. Discusses Gentzen's proof on pages 96–97 and footnotes. Appendices discuss the Peano Axioms briefly, gently introduce readers to formal logic.
  • Taylor Booth, Sequential Machines and Automata Theory, Wiley, New York, 1967. Cf. Chapter 9, Turing Machines. Difficult book, meant for electrical engineers and technical specialists. Discusses recursion, partial-recursion with reference to Turing Machines, halting problem. Has a Turing Machine model in it. References at end of Chapter 9 catch most of the older books (i.e. 1952 until 1967 including authors Martin Davis, F. C. Hennie, H. Hermes, S. C. Kleene, M. Minsky, T. Rado) and various technical papers. See note under Busy-Beaver Programs.
  • Busy Beaver Programs are described in Scientific American, August 1984, also March 1985 p. 23. A reference in Booth attributes them to Rado, T.(1962), On non-computable functions, Bell Systems Tech. J. 41. Booth also defines Rado's Busy Beaver Problem in problems 3, 4, 5, 6 of Chapter 9, p. 396.

  Category:Theory of computation

  类别: 计算理论

  • David Bolter, Turing’s Man: Western Culture in the Computer Age, The University of North Carolina Press, Chapel Hill, 1984. For the general reader. May be dated. Has yet another (very simple) Turing Machine model in it.

  Category:Computability theory

  类别: 可计算性理论

  • Egon Börger. "Computability, Complexity, Logic". North-Holland, 1989.

  Category:Mathematical problems

  类别: 数学问题

  • Stephen Kleene, Introduction to Metamathematics, North-Holland, 1952. Chapter XIII ("Computable Functions") includes a discussion of the unsolvability of the halting problem for Turing machines. In a departure from Turing's terminology of circle-free nonhalting machines, Kleene refers instead to machines that "stop", i.e. halt.

  Category:Undecidable problems

  类别: 无法判定的问题

  • Sven Köhler, Christian Schindelhauer, Martin Ziegler, On approximating real-world halting problems, pp.454-466 (2005)
    Springer Lecture Notes in Computer Science volume 3623: Undecidability of the Halting Problem means that not all instances can be answered correctly; but maybe "some", "many" or "most" can? On the one hand the constant answer "yes" will be correct infinitely often, and wrong also infinitely often. To make the question reasonable, consider the density of the instances that can be solved. This turns out to depend significantly on the Programming System under consideration.

    Category:1936 introductions

    类别: 1936年引言

    
    

    This page was moved from wikipedia:en:Halting problem. Its edit history can be viewed at 图灵停机问题/edithistory