49
个编辑
更改
跳到导航
跳到搜索
第38行：
第38行： − + − == 背景 == 第110行：
第109行： − + − − === 编程的后果 === 第239行：
第236行： − + − − === 常见的陷阱 === 第290行：
第285行： − + − − == 历史 == − + − − === 时间轴 === 第386行：
第377行： − + − − == 形式化 == 第403行：
第392行： − + − − === 表示为一个集合 === 第471行：
第458行： − + − − === 证据的概念 === 第1,297行：
第1,282行： − + − − == 可计算性理论 == 第1,358行：
第1,341行： − + − − === 哥德尔不完备定理 === 第1,375行：
第1,356行： − + − − == 泛化 == 第1,406行：
第1,385行： − + − − === 停止所有输入 === 第1,441行：
第1,418行： − + − − === 识别部分的解决方案 === 第1,480行：
第1,455行： − + − − === 损耗计算 === 第1,517行：
第1,490行： + + + + + + + + + + + +
无编辑摘要
【最终版】停机问题是在一个固定的图灵完备计算模型上，即用某种给定的程序语言编写的所有程序的性质的决策问题，该语言的通用性足以与图灵机相当。问题是，给定一个程序和一个程序的输入，当运行该输入时，程序是否最终会停止。在这个抽象的框架中，对于程序执行所需的内存或时间没有资源限制;在停止之前，它可以花费任意长的时间和使用任意数量的存储空间。问题很简单，给定的程序是否会在特定的输入时停止。
【最终版】停机问题是在一个固定的图灵完备计算模型上，即用某种给定的程序语言编写的所有程序的性质的决策问题，该语言的通用性足以与图灵机相当。问题是，给定一个程序和一个程序的输入，当运行该输入时，程序是否最终会停止。在这个抽象的框架中，对于程序执行所需的内存或时间没有资源限制;在停止之前，它可以花费任意长的时间和使用任意数量的存储空间。问题很简单，给定的程序是否会在特定的输入时停止。
== Background ==
== Background背景 ==
For example, in pseudocode, the program
For example, in pseudocode, the program
【最终版】然而，大多数子程序的目的是完成(停止)。
【最终版】然而，大多数子程序的目的是完成(停止)。
=== Programming consequence ===
=== Programming consequence编程的后果 ===
In particular, in hard real-time computing,
In particular, in hard real-time computing,
.．.所涉及的量应该使人怀疑，主要基于状态图的有限性的定理和论证可能没有太大的意义。
.．.所涉及的量应该使人怀疑，主要基于状态图的有限性的定理和论证可能没有太大的意义。
=== Common pitfalls ===
=== 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.
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 ==
== History历史 ==
The halting problem is historically important because it was one of the first problems to be proved [[undecidable problem|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.
The halting problem is historically important because it was one of the first problems to be proved [[undecidable problem|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]。)随后，又叙述了许多其他无法决定的问题。
【最终版】停机问题在历史上很重要，因为它是第一个被证明是不可决定的问题之一。(图灵的证明在1936年5月付印，而Alonzo Church对lambda微积分中一个问题的不可判定性的证明已经在1936年4月发表[Church, 1936]。)随后，又叙述了许多其他无法决定的问题。
===Timeline===
===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)
* 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)
这个集合是递归可枚举的，这意味着有一个可计算的函数列出了它包含的所有对(i, x)。然而，这个集合的补集不是递归可枚举的。
这个集合是递归可枚举的，这意味着有一个可计算的函数列出了它包含的所有对(i, x)。然而，这个集合的补集不是递归可枚举的。
== Formalization ==
== 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:
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:
【最终版】重要的是，形式化允许将算法直接映射到算法可以操作的某些数据类型。例如,如果形式允许算法定义函数在字符串(如图灵机),那么应该有一个映射这些算法的字符串,如果形式允许算法定义函数在自然数(如可计算函数),那么应该有一个自然数的映射算法。到字符串的映射通常是最直接的，但是包含n个字符的字母表上的字符串也可以通过将它们解释为n-ary数字系统中的数字来映射为数字。
【最终版】重要的是，形式化允许将算法直接映射到算法可以操作的某些数据类型。例如,如果形式允许算法定义函数在字符串(如图灵机),那么应该有一个映射这些算法的字符串,如果形式允许算法定义函数在自然数(如可计算函数),那么应该有一个自然数的映射算法。到字符串的映射通常是最直接的，但是包含n个字符的字母表上的字符串也可以通过将它们解释为n-ary数字系统中的数字来映射为数字。
=== Representation as a set ===
=== 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:
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:
【最终版】{i |有一个输入x，使得程序i在运行输入x时最终停止运行}。
【最终版】{i |有一个输入x，使得程序i在运行输入x时最终停止运行}。
=== Proof concept ===
=== 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):
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):
【最终版】由于停止问题的否定答案表明存在图灵机无法解决的问题，Church-Turing论文限制了任何实现有效方法的机器所能完成的工作。然而，并不是所有人类想象的机器都符合丘奇-图灵理论(如oracle机器)。从长远来看，是否存在能够逃避图灵机模拟的实际确定性物理过程，这是一个有待解决的问题，特别是，这种假设的过程是否可以有效地用于一台计算机(超级计算机)，从而解决图灵机的停机问题。这些未知的物理过程是否参与到人类大脑的工作中，以及人类是否能够解决停止问题，也是一个有待解决的问题(Copeland 2004, p. 15)。
【最终版】由于停止问题的否定答案表明存在图灵机无法解决的问题，Church-Turing论文限制了任何实现有效方法的机器所能完成的工作。然而，并不是所有人类想象的机器都符合丘奇-图灵理论(如oracle机器)。从长远来看，是否存在能够逃避图灵机模拟的实际确定性物理过程，这是一个有待解决的问题，特别是，这种假设的过程是否可以有效地用于一台计算机(超级计算机)，从而解决图灵机的停机问题。这些未知的物理过程是否参与到人类大脑的工作中，以及人类是否能够解决停止问题，也是一个有待解决的问题(Copeland 2004, p. 15)。
==Computability theory==
==Computability theory可计算性理论==
{{main|Computability theory}}
{{main|Computability theory}}
【最终版】由于停止问题的否定答案表明存在图灵机无法解决的问题，Church-Turing论文限制了任何实现有效方法的机器所能完成的工作。然而，并不是所有人类想象的机器都符合丘奇-图灵理论(如oracle机器)。从长远来看，是否存在能够逃避图灵机模拟的实际确定性物理过程，这是一个有待解决的问题，特别是，这种假设的过程是否可以有效地用于一台计算机(超级计算机)，从而解决图灵机的停机问题。这些未知的物理过程是否参与到人类大脑的工作中，以及人类是否能够解决停止问题，也是一个有待解决的问题(Copeland 2004, p. 15)。
【最终版】由于停止问题的否定答案表明存在图灵机无法解决的问题，Church-Turing论文限制了任何实现有效方法的机器所能完成的工作。然而，并不是所有人类想象的机器都符合丘奇-图灵理论(如oracle机器)。从长远来看，是否存在能够逃避图灵机模拟的实际确定性物理过程，这是一个有待解决的问题，特别是，这种假设的过程是否可以有效地用于一台计算机(超级计算机)，从而解决图灵机的停机问题。这些未知的物理过程是否参与到人类大脑的工作中，以及人类是否能够解决停止问题，也是一个有待解决的问题(Copeland 2004, p. 15)。
=== Gödel's incompleteness theorems ===
=== Gödel's incompleteness theorems哥德尔不完备定理 ===
{{trim|{{#lsth:Undecidable problem|Relationship with Gödel's incompleteness theorem}}}}
{{trim|{{#lsth:Undecidable problem|Relationship with Gödel's incompleteness theorem}}}}
【最终版】然而，“给定程序p，它是一个部分停机求解器吗”(在描述的意义上)的问题至少和停机问题一样难。
【最终版】然而，“给定程序p，它是一个部分停机求解器吗”(在描述的意义上)的问题至少和停机问题一样难。
== Generalization ==
== 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,
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,
为了测试输入程序x是否在y上停止，构造一个程序p，它在输入(x,y)上报告为真，并且在所有其他输入上发散。
为了测试输入程序x是否在y上停止，构造一个程序p，它在输入(x,y)上报告为真，并且在所有其他输入上发散。
=== Halting on all inputs ===
=== Halting on all inputs停止所有输入 ===
The above argument is a reduction of the halting problem to PHS recognition, and in the same manner,
The above argument is a reduction of the halting problem to PHS recognition, and in the same manner,
有损耗的图灵机是一种图灵机，其中部分磁带可能会不确定地消失。对于有损耗的图灵机，停机问题是非原语递归的。
有损耗的图灵机是一种图灵机，其中部分磁带可能会不确定地消失。对于有损耗的图灵机，停机问题是非原语递归的。
=== Recognizing partial solutions ===
=== 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.
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.
然后用PHSR测试p。
然后用PHSR测试p。
=== Lossy computation ===
=== 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 non[[primitive recursive]].<ref name="Undecidable over unreliable channels">{{cite journal |last1=Abdulla |first1=Parosh Aziz|last2=Jonsson|first2=Bengt |title=Verifying Programs with Unreliable Channels|journal = Information and Computation |date= 1996 |volume=127 |issue=2 |pages=91–101 |doi=10.1006/inco.1996.0053}}</ref>{{rp|92}}
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 non[[primitive recursive]].<ref name="Undecidable over unreliable channels">{{cite journal |last1=Abdulla |first1=Parosh Aziz|last2=Jonsson|first2=Bengt |title=Verifying Programs with Unreliable Channels|journal = Information and Computation |date= 1996 |volume=127 |issue=2 |pages=91–101 |doi=10.1006/inco.1996.0053}}</ref>{{rp|92}}
* [[Worst-case execution time]]
* [[Worst-case execution time]]
忙碌的海狸
哥德尔不完备定理
Brouwer-Hilbert争议
Kolmogorov复杂度
P与NP问题
终止分析
最坏执行时间
== Notes == <!-- This section should have *explanatory* notes. References use parenthetical citations. -->
== Notes == <!-- This section should have *explanatory* notes. References use parenthetical citations. -->