图灵机(TM)是否覆写自身输入的不可判定性证明与思路

核心直觉逻辑 #

• 这个问题的不可判定性本质来自和停机问题的绑定：要判断一台图灵机是否会在未来某个时刻覆写输入，本质上需要先知道这台图灵机会不会运行到能执行覆写操作的阶段，而不存在通用方法能提前判定任意图灵机的运行最终会进入哪个分支、会不会停机。
• 我们可以很容易把这个问题和已知不可判定的停机问题挂钩：只要构造一个特殊图灵机，它只有在目标图灵机停机后才会执行覆写输入的操作，那能不能判定前者会不会覆写，就等价于能不能判定后者会不会停机。

严谨证明过程 #

我们采用归约法证明，核心思路是将已知不可判定的停机问题归约到当前问题，若当前问题可判定则停机问题可判定，从而导出矛盾，证明当前问题不可判定。

前提定义 #

• 待证命题：不存在通用判定器OverwriteChecker，对于任意输入的图灵机编码<M>和输入字符串x，OverwriteChecker总能在有限步内输出：M在输入x上运行时，是否会覆写初始输入带中x对应位置的任意字符。
• 已知结论：停机问题不可判定，即不存在通用判定器HaltChecker，对于任意<M>和w，总能在有限步内判定M在输入w上是否会停机。

归约构造 #

假设OverwriteChecker存在，我们可以用它构造出停机问题的判定器HaltChecker，步骤如下：

1. 对于任意停机问题的输入<M>, w，构造新的图灵机M'，其运行逻辑为：
   • 初始输入为w，运行时首先将读写头移动到输入区域右侧的空白带位置，所有模拟M运行所需的状态、临时存储全部放在该空白区域，全程不触碰初始输入w对应的带位置。
   • 若模拟M在w上运行的过程中，M触发停机逻辑，则立刻将读写头移回初始输入的第一个字符位置，将该字符修改为和初始值不同的内容，随后停机。
   • 若M在w上永不停机，则M'会永远停留在模拟阶段，永远不会触碰初始输入区域的任何字符。
2. 调用OverwriteChecker(<M'>, w)得到结果：
   • 若返回True：说明M'会覆写输入，即M在w上会停机，因此HaltChecker(<M>, w)返回True。
   • 若返回False：说明M'永远不会覆写输入，即M在w上永不停机，因此HaltChecker(<M>, w)返回False。

矛盾导出 #

上述构造得到的HaltChecker是停机问题的通用判定器，和停机问题不可判定的已知结论矛盾，因此初始假设不成立，即OverwriteChecker不存在，判定任意图灵机是否会覆写自身输入的问题不可判定。

内容的提问来源于stack exchange，提问作者InfiniteLoop