关于图灵停机问题不可判定性证明

什么是图灵停机问题

概念：图灵停机问题（Halting Problem）是否可判定，形式化而言：

停机

不停机

对角线证明

对角线，实际上逻辑系统中的符号完备问题也是通过该法构造解答的

由于所有的图灵机都可以由

序列编码，所以图灵机是可数的，我们可以枚举出所有的图灵机

。假设存在某个函数

，能判定任何图灵机

对 任何输入

是否停机，那么我们可以构造一个图灵机

，使得

，显然这个图灵机和枚举的所有图灵机都不相同，而且这个图灵机可以经由函数

构造出来（该函数本身也是一个图灵机）。这与列举了所有的图灵机相悖，所以我们可以得出不存在这样的

，即图灵停机问题不可判定。

使用对角线对图灵机的证法说明了可数的无限中包含了不可数无限的性质，即后者表现在前者中，但是前者所在的系统无法表达这种性质，即斯寇伦佯谬（Skolem's paradox）。

构造法证明

思路与证明：通常使用反证法与构造法。那么，首先假设存在

，接下来构造矛盾（问题是矛盾应当体现在何处，它的根源是什么），从而得出假设为错。考虑引入中间过程

。一般而言，

应当体现出 递归 或者 否定 的性质，才能体现出矛盾。然而若是一般的递归，则由于

永远需要一个输入

。这显然会导致函数参数的不一致。譬如，此处考虑

停机

不停机

具体而言，其中的停机可由直接返回表示，不停机由死循环表示。那么，如果使用

来判断其是否停机，则函数变成

，显然与题设不符（虽然可以直观地将后二者压缩成一个参数，但是这对

内部的判断条件并不友好）。所以此处的问题是如何防止参数长度的变化，或者说，如何消去参数呢？答案是，将参数实例化为已有的特征，换句话说，将图灵机本身作为参数，因为它既是「机器」又是「语言」，此处即为 自我递归 或者 自我指涉。那么显然地，我们有：

停机

不停机

显然该图灵机矛盾，故而证否。

该证明中利用的矛盾是自我指涉，该自我指涉的根源是图灵机的二义性，即上文所提：它既是「机器」又是「语言」。其体现在图灵机既作为「执行机构」又作为「输入内容」。

构造法证明之我见

除此之外，我们还可以用假设做什么？上文将参数固化，此处直接获取参数。设

while (i in I && H(m, i) == 1);return i; 用于获取使

不停机的的输入。则显然可知，要么

，要么

。此法也可以避免参数长度不一致的问题。于是可以构建：

不停机

停机

可以看出判断中并没有出现

的参数

，这给了我们操作的余地。若

，则说明

不存在令其不停机的输入，然而此处它却停机，故而矛盾；若

，则说明

存在令其不停机的输入

，此处令其为

输入，即

，则此时它应该不停机，然而根据定义它却停机，故而矛盾。故而证否。

该证明为本人在思考如何去除参数，而保证参数长度一致性时想出，既然通过传参的方式行不通，那么就直接在内部生成，也可以看出，这种方法保证了

参数的任意性。在构造的过程中发现，该生成函数也是一个不知何时停机的图灵机，那么可以基于假设构造矛盾，基本思想仍然是自我指涉，但是和上一证明存在本质的不同。此处，矛盾的根源是纯粹语义上的循环递归性，其体现在

外部的输入和

内部函数输入构造的对应性。其次需要说明的是

的内部使用了

本身，这是否可以。当然可以，因为里面的M是「语言」。