我正在查看Sipser的计算理论简介中的停止问题的证明，我主要关心的是以下证明：
如果 TM M 不知道它何时循环（它不能接受或拒绝，这就是为什么 TM 对所有字符串都是图灵可识别的），那么决策者 H 将如何确定 M 是否可能处于循环中？当 TM D 进行处理时，同样的问题将继续存在。
问问题
18143 次
3 回答
28
在阅读了这篇文章并尝试将证明可视化后，我想出了这段代码，这是对相关问题的回答中代码的简化版本：
function halts(func) {
// Insert code here that returns "true" if "func" halts and "false" otherwise.
}
function deceiver() {
if(halts(deceiver))
while(true) { }
}
如果halts(deceiver)返回true，deceiver将永远运行，如果返回false，deceiver将停止，这与 的定义相矛盾halts。因此，该功能halts是不可能的。
于 2013-11-27T01:50:49.737 回答
19
这是一种“反证法”，一种归谬法。（拉丁短语在理论课上总是很好……当然，只要它们有意义。）
这个程序H只是一个有两个输入的程序：一个代表某个机器的程序的字符串和一个输入。为了证明的目的，您只需假设程序 H 是正确的：如果 M 接受w ，它将停止并接受。您无需考虑它会如何做到这一点；事实上，我们即将证明它不能，没有这样的程序H可以存在，......
因为
如果存在这样的程序，我们可以立即构造另一个H无法决定的程序H' 。但是，根据假设，不存在这样的程序：H可以决定一切。所以，我们不得不得出结论，没有任何程序定义为我们定义的H是可能的。
顺便说一句，考虑到它的使用频率，尤其是在计算机科学中，证明的归约方法比你想象的更具争议性。你不应该因为发现它有点奇怪而感到尴尬。神奇的术语是“非建设性的”，如果你真的很有野心，可以向你的一位教授询问 Errett Bishop 对非建设性数学的批评。
于 2011-12-06T02:16:18.627 回答
-2
以下是基于Sipser证明
我花了两年时间创建（完全可操作的）x86utm 操作系统，以使用用 C 编写的暂停决策器具体解决暂停问题。这个部分暂停决策器调用 x86 仿真器以调试步骤模式执行其输入。输入是转换为 32 位无符号整数的 x86 函数的机器地址。
在模拟每条 x86 指令后，它会立即检查此输入的完整执行跟踪。一旦部分停止决策器识别出非终止行为模式，它就会中止模拟并报告未停止。
#define u32 uint32_t
int D(u32 P) // P is a machine address
{
if ( H(P, P) )
return 0 // reject when H accepts
return 1; // accept when H rejects
}
int main()
{
H((u32)D, (u32)D );
}
当 H 是一个模拟停止决策器时，H(D,D) 基于 H(D,D) 指定对 H 的无限嵌套模拟而拒绝其输入作为停止计算，除非 H 中止其对 D(D) 的模拟。
_D()
[00000cd0](01) 55 push ebp
[00000cd1](02) 8bec mov ebp,esp
[00000cd3](03) 8b4508 mov eax,[ebp+08]
[00000cd6](01) 50 push eax
[00000cd7](03) 8b4d08 mov ecx,[ebp+08]
[00000cda](01) 51 push ecx
[00000cdb](05) e800feffff call 00000ae0
[00000ce0](03) 83c408 add esp,+08
[00000ce3](02) 85c0 test eax,eax
[00000ce5](02) 7404 jz 00000ceb
[00000ce7](02) 33c0 xor eax,eax
[00000ce9](02) eb05 jmp 00000cf0
[00000ceb](05) b801000000 mov eax,00000001
[00000cf0](01) 5d pop ebp
[00000cf1](01) c3 ret
Size in bytes:(0034) [00000cf1]
_main()
[00000d00](01) 55 push ebp
[00000d01](02) 8bec mov ebp,esp
[00000d03](05) 68d00c0000 push 00000cd0
[00000d08](05) 68d00c0000 push 00000cd0
[00000d0d](05) e8cefdffff call 00000ae0
[00000d12](03) 83c408 add esp,+08
[00000d15](02) 33c0 xor eax,eax
[00000d17](01) 5d pop ebp
[00000d18](01) c3 ret
Size in bytes:(0025) [00000d18]
===============================
...[00000d00][00101730][00000000](01) 55 push ebp
...[00000d01][00101730][00000000](02) 8bec mov ebp,esp
...[00000d03][0010172c][00000cd0](05) 68d00c0000 push 00000cd0
...[00000d08][00101728][00000cd0](05) 68d00c0000 push 00000cd0
...[00000d0d][00101724][00000d12](05) e8cefdffff call 00000ae0
Begin Local Halt Decider Simulation at Machine Address:cd0
...[00000cd0][002117d0][002117d4](01) 55 push ebp
...[00000cd1][002117d0][002117d4](02) 8bec mov ebp,esp
...[00000cd3][002117d0][002117d4](03) 8b4508 mov eax,[ebp+08]
...[00000cd6][002117cc][00000cd0](01) 50 push eax
...[00000cd7][002117cc][00000cd0](03) 8b4d08 mov ecx,[ebp+08]
...[00000cda][002117c8][00000cd0](01) 51 push ecx
...[00000cdb][002117c4][00000ce0](05) e800feffff call 00000ae0
...[00000cd0][0025c1f8][0025c1fc](01) 55 push ebp
...[00000cd1][0025c1f8][0025c1fc](02) 8bec mov ebp,esp
...[00000cd3][0025c1f8][0025c1fc](03) 8b4508 mov eax,[ebp+08]
...[00000cd6][0025c1f4][00000cd0](01) 50 push eax
...[00000cd7][0025c1f4][00000cd0](03) 8b4d08 mov ecx,[ebp+08]
...[00000cda][0025c1f0][00000cd0](01) 51 push ecx
...[00000cdb][0025c1ec][00000ce0](05) e800feffff call 00000ae0
Local Halt Decider: Infinite Recursion Detected Simulation Stopped
...[00000d12][00101730][00000000](03) 83c408 add esp,+08
...[00000d15][00101730][00000000](02) 33c0 xor eax,eax
...[00000d17][00101734][00100000](01) 5d pop ebp
...[00000d18][00101738][00000058](01) c3 ret
Number_of_User_Instructions(23)
Number of Instructions Executed(23826)
于 2021-05-29T05:13:24.757 回答