可计算性理论
计算理论中的可计算性理论用于研究在某个计算模型(常常是图灵机)中的某个问题是否存在某个算法解决该问题. 定义上的算法需要是具有有穷步骤的, 也就是在无论任何输入下都必须能够停机. 执行无穷步骤的过程一般不叫算法. 然而, 在某些情况下一个无穷执行下去的过程并在过程中不断产生结果的机器是有讨论意义的. 这种机器被称为枚举机(Enumerator).
问题是否可计算, 是判断解决算法是否存在的根本分野. 而讨论解决一个问题的算法是否高效, 那就是计算复杂度理论的内容了.
问题与语言
问题与语言其实可以看成是同一个东西. 所谓"问题", 可以被形式化为全体输入的某个子集$S$. 当我们在问"一个问题是否有解"时, 就是在问是否存在一个解法, 使得对任意一个输入$x$, 都能判断$x$是否在这个集合$S$中. 也就是判断 $x \overset{?}\in S$ 的算法是否存在; 从计算模型的角度上来说, 其实是在问"这个问题所对应的语言是否是可判定的". 更直接点说, 是在问"是否存在这么一个图灵机, 它接受任意输入并总能够在有限步骤内停机, 同时它准确地接受所有这个问题所对应的语言, 拒绝所有不是这个问题所对应的语言". 这样一个总能够停机的图灵机就是解决该问题的算法. 我们得到了解决问题的算法, 问题就得到了它的解法. 我们常常不关心某个问题的具体答案是什么, 而是关心这个问题是否存在解决方案——一种一劳永逸的解决方案, 能够源源不断地告诉我们所有具体答案的解决方案.
上面的有限步骤非常重要. 一个问题可判定, 不只是说它能够在输入是正确的情况下能够停机, 而是说在任意输入———使是错误的输入上———能够停机. 这样的问题对应的语言被称为递归语言(Recursive Language, RL), 或可判定语言(Decidable Language).
为什么要强调这一点? 因为存在一些语言, 它所对应的图灵机最多只能在所有正确的输入上停机, 而在错误的输入上, 它可能停机, 也可能不停机. 这意味着如果你想找到一个问题的答案, 你把输入告诉图灵机, 图灵机一直运行, 却可能永远都不能告诉你答案. 在运行时的任意时刻, 你都不知道是因为解决问题的步骤太长, 所以它还没运行结束; 还是因为输入根本就是错的, 图灵机陷入了永不停机的死循环中. 这样的语言是递归可枚举语言(Recursively Enumerable Language, REL) 但不是 递归语言.
递归可枚举语言又是什么? 它跟之前提到的枚举机有关, 如果一个图灵机可以在运行期间不断地输出一个语言对应的串, 对于每个该语言的串, 图灵机都能在有限步骤内输出, 这样的图灵机就是这个语言的枚举机. 如果语言无穷, 很显然这个图灵机会永远运行下去, 不断输出这个语言的每个串. 如果存在这么一个枚举该语言串的图灵机, 那么该语言就是递归可枚举的. 这样我们可以知道递归可枚举语言类覆盖了所有递归语言类, 并且还多出了一些非递归的语言——想象一下你给这个枚举机略动一些改造, 它得到一个输入串, 然后不断枚举这个语言的串, 并和输入串比较. 如果在某时刻比较相等, 那么输入串确实就属于这个语言. 而如果这个输入串不属于这个语言呢? 很显然这个机器会永远枚举下去, 跑冒烟了都找不到一个相等的比较. 这样一个半截子的图灵机不能被我们认可为一个合格的算法(如果你能让图灵机在有限时间内执行无穷次步骤, 那么我们也许就能接受这个算法😅——恭喜, 你发明了芝诺机, 这种机器以有穷肘赢无穷, Turing OUT!).
总结一下, 递归可枚举语言就是所有图灵机所能枚举的语言的集合. 其中一部分称作递归语言的子集, 不但可被枚举, 还可被判定. 而剩下的一部分语言就是我们所说的"半截子"语言.
是否存在连递归可枚举都不是的语言呢? 有的兄弟, 有的. 存在一些语言, 它甚至不能被图灵机一个个地把所有这个语言的串枚举出来. 它们被简单称为非递归可枚举语言(Non-Recursively Enumerabele Language). 也就是说你也许可以找到一个非递归可枚举语言的一个串, 但是你不可能制造一个图灵机/过程, 使得图灵机能够枚举出所有这个语言的串——哪怕你给它无穷的时间也做不到.
规约(Reduction)
措辞 问题A可归约到问题B: 意为问题A可以转化为问题B的一个情形/特例. 亦即问题B的强度高于或等于问题A. 那么若知道B如何解, 则可知道A如何解.
例:
若 $\text{HALT}_{TM}$ 可以归约到 $\text{PC}$, 那么如果 $\text{PC}$ 可判定, 则可给出判定 $\text{HALT}_{TM}$ 的方法. 但是已知问题 $\text{HALT}_{TM}$ 不可判定, 因此 $\text{PC}$ 也不可判定.
这是在说, 如果我们找到了一个规约方式, 把图灵机停机问题( $\text{HALT}_{TM}$ )归约到皮亚诺算数公理完备性问题( $\text{PC}$ ), 那么我们就知道了完备性问题至少不比停机问题简单. 我们如果解决了完备性问题, 那么就一定能解决停机问题, 这是因为停机问题可以转化为完备性问题的一个特例.
然而很可惜, 已经证明停机问题是不可解决的. 也就是简单的特例无法解决, 更强的问题——完备性问题就更没法解决了.
简单总结一下就是: 弱问题规约到强问题. 如果强问题可解, 那么弱问题也可解; 反过来, 如果弱问题不可解, 那么强问题也不可解.
映射可规约(Mapping Reducible)
为了准确刻画规约是什么东西, 定义了映射可归约.
映射可归约: 一个语言$A$ 映射可归约到 语言$B$, 记作$A \leq_m B$, 若:
$$ \exists Computable\ Function\ f : \Sigma^* \rightarrow \Sigma^*, s.t:\\ \forall w \in \Sigma^*,\ w \in A \Leftrightarrow f(w) \in B. $$解释:
可计算函数(Computable Function): 可以理解为所有可被图灵机实现的函数. 它接收一个输入, 图灵机计算之后在带子上留下计算结果, 这个图灵机需要在函数定义域上的所有值都计算停机;
字母表($\Sigma$): 我们讨论中所有串可能出现的字母的集合;
串集合/串空间($\Sigma^*$): 就是字母表派生出的所有有穷串的集合, 字母表$\Sigma$右上加$*$表示对集合取Kleene闭包.
如果存在一个串空间($\Sigma^*$)到串空间上的可计算函数$f$, 使得对于任意的串$w$, 要么$w$和$f(w)$都分别在他们的语言($A$和$B$)上, 要么都分别不在他们的语言上, 那么$A$就映射可规约到$B$上.
这样, 我们实际上就构造了一个从$A$到$B$的同态映射, 把小语言$A$整个嵌入到大语言$B$中.
我们还需要深入解释一下. 从定义上看, 似乎$A$和$B$的地位是平等的, 看不出来有什么$A$小于$B$的说法. 当然, $A$完全可以等于$B$或者同构于$B$, 记号$\leq_m$中用了小于等于号就是这个意思. 然而, 如果按照一般情况来说, A是一个弱(小)问题, B是一个强(大)问题, 映射可归约性定义中体现强弱的是那个映射函数$f$. 我们找的函数$f$完全可以不是满射也不是单射. 只有当$f$既满又单时, 也就是$f$是一个双射时, 才能存在一个$f^{-1}$把$B$完整地映射回$A$, 这时$A$和$B$就是同构的, $f$就是$A$到$B$的同构映射.
- 思考一下, 如果$f$不是满射会怎么样? $B$中会有一些串不能被$f$映射到, 也就是不存在这些串的原像. 你可以回顾一下映射可规约的定义, 发现这些串永远都不会是$f(w)$, 也就不在定义的讨论范围内. 这些串可以理解为强问题中除去弱问题的其他问题, 这些问题正是为什么强问题比弱问题"强"的原因——强问题所覆盖范围更广, 要解决的东西更多.
- 如果$f$不是单射会怎么样? 这意味着$A$中存在多个串通过$f$映射到$B$的同一个串中, 相当于$A$通过映射把自己"蜷缩"在了$B$里. $A$可能只是看着困难, 其实不会比$B$困难, $A$中的有些问题本质上其实只是重复或相似的问题罢了.
规约与判定性
TODO…
回顾一下规约那一节的说明, 你可以发现映射可规约的定义确实就是我们想要的直觉上规约的形式化版本.
这样, 我们现在就可以简单捋一下规约和可判定性问题的关系.
- $if A \leq_m B \wedge B\ \text{decidable, then } A \text{ is also decidable.}$
- $if A \leq_m B \wedge A\ \text{undecidable,then } B \text{ is also undecidable.}$
可以看到, 上面两段基本上就是规约一节例子最后一句总结的形式化表述. 规约是一种强有力的工具, 可以用来解决许多可计算性问题. 如果你能在两个看似风马牛不相及的问题上找到一个鬼斧神工的规约, 那就相当于找到了一个桥梁, 从一头的已知可解或不可解, 通向另一头的未知. 具体点说, 如果你觉得某个问题应该是可判定的, 那么你应该尽可能找到一个规约, 把这个问题归约到另一个已知可判定的问题上; 反过来, 如果你想证明某个问题不可判定, 那么你应该把某个已知不可判定的问题归约到你想证明的问题上.
图灵-丘奇论题
为了后面简化讨论, 我们需要给出上面这个论题. 它大概是在说: 一切我们直觉意义上的算法/计算过程, 都可以由图灵机模拟——你也许会觉得这不是废话吗? 事实上, 大家都承认这个论题. 然而, 想想我们自身的思考行为. 人脑有点像计算机, 可是人的思考就真的只是一个个机械的计算过程吗? 那些灵感迸发的火花, 也是机械计算吗? 很可惜, 现在的科学尚未能给出一个明确的答复. 无论你相信还是不相信, 你总得拿出证据来证明. 除此之外, 你真的相信宇宙中就没有什么更强大的东西, 可以以某种神秘, 超脱我们理解范围的的方式运作, 然后告诉我们关于某个问题的答案吗? 我们也不知道. 正是因为这些不知道, 我们意识到了从图灵机所代表的抽象的计算过程, 到现实中的计算, 可能隐藏着一个未知的鸿沟, 我们必须澄清这一点, 而这就是这个论题的意义所在. 其实, 相信这个论题, 也代表着你相信图灵机的计算能力就是物理宇宙中的计算能力上限.
扯得有点远, 无论你相信还是不相信这个论题, 有一个比较弱的版本是毫无疑问的. 那就是图灵机的计算能力和许多计算机编程语言(C++, Python, 汇编等等)的计算能力完全等价. 这意味着, 你可以编码图灵机, 使得其运行计算机程序, 得到与计算机程序的输出等价的输出; 反过来, 你也可以轻易地编写一个C++程序, 使得其模拟一个图灵机运作. 在这里, 我们不考虑现实世界中关于运行速度, 内存限制等等无关紧要的问题, 我们想做的是仅仅把编程语言视作一个纯粹的数学模型, 然后将它与同是数学模型的图灵机相比较. 在你相信这一点后, 我们就可以把之后关于图灵机的讨论, 无损替换成任意你所熟悉的任意编程语言, 乃至抽象简洁的算法的讨论, 而不必拘泥于图灵机编码的细枝末节. 而如果你更进一步, 相信图灵-丘奇论题, 那你大可以发挥你大脑的聪明才智, 使用"瞪眼瞧"“显然是"和"俺寻思"这类你的直觉来解决一个问题——不过你的寻思至少得让大多数人信服.
莱斯定理(Rice’s Theorem)
图灵停机问题不可判定已经耳熟能详, 简单点说, 就是无法找到一个算法/图灵机, 判断任意一台图灵机是否会停机. 你也许会感到很失望, 图灵机这么弱, 无法判断任意一个图灵机的一个看似简单的行为; 然而图灵机又那么强, 强到捉摸不定, 休想让别人预测它的未来. 能打败自己的只有自己. 事实上, 停机问题只是图灵机古怪脾气的冰山一角. 我们早已知道大量关于图灵机的问题都是不可判定的: 想要判断图灵机是否永远拒绝(接受空集问题)? 做不到; 想要判断图灵机永远接受(接受全集问题)? 也做不到; 想要判断任意两个图灵机是否接受相同的语言? 别想了. 诸如此类, 一概不可判定.
乍一看, 你可能会觉得太离谱了, 这怎么可能呢? 在我们接受上一节的基础上, 可以将上面比较抽象的问题改编成下面这个具体又类似的问题: 判断任意一个C++函数是否永远只返回0. 这些的问题都有一个重点: 判断任意的图灵机/函数怎么怎么样, 而不是个别一些图灵机或者程序什么的. 也就是说, 我们要找的是一个完全的, 毫无遗漏的解决方案. 这意味着一些一拍脑门的方法是行不通的: 欸☝🤓我直接扫一眼C++函数的源代码, 看它后面是不是只有return 0;不就行了嘛? Naive! 函数出现分支怎么办? 出现循环怎么办? 出现递归怎么办…万一函数中出现了一大堆复杂又诡异的计算, 然后最后却又神奇地从不返回其他值而只返回0, 你会不会破防? 你会发现越想越复杂, 然后发现这个破问题实在没有乍一看上去这么简单. 然后你又会发现, 如果这些问题任意一个都能找到答案, 抛开算法复杂度不谈, 那么理论上对于任意一个数学问题, 我们都能有一个机械的解决方案, 于是数学家们全都将原地转型成定理民工.
所有这些类似的问题, 已经说过都有一个统一的答案——不可判定. 事实上, 我们有一个解决停机问题, 或者上面所说的问题一个统一的定理, 那就是莱斯定理.
莱斯定理: 有关于图灵机所接受语言的一切非平凡性质, 一概不可判定.
这个定理乍听起来很唬人又很有一股霸总的味道. 我们首先需要做一番解释, 比如什么是性质, 什么是非平凡, 它们噼里啪啦地组合起来又是什么意思. 不过在此之前, 我需要给出足够阐释这个定理的符号解释, 然后再给出这个定理的形式化版本.
编码
首先需要承认一件事, 那就是图灵机是可编码的. 这个编码跟上面提到的编码不同. 上面的编码是说对图灵机进行"编程”, 让它按照某个特定的方式运行. 而本节所说的编码, 是说可以对所有的图灵机都进行编号. 存在一种方式, 使得每个图灵机都得到一个唯一的编号. 所谓编号, 也就是1, 2, 3, 4…这类正整数集, 然后把每个数字指派给唯一的某个图灵机. 事实上, 有无数种编码方式把图灵机进行编码, 数码也不一定是从1开始, 也可能是从某个很大的整数开始. 要是你喜欢, 你也可以用负数给图灵机编码. 这个道理对我来说至少看上去是挺显然的, 尽管如果要进行严谨的证明, 需要进行一些繁杂的技术性工作. 如果你不相信, 你可以想象一下一个C++源代码文件的二进制编码, 把这个二进制编码看作一个巨大的正整数, 然后把这个正整数指派给这个C++源代码的程序. 这是完全可行的, 只不过看起来简单粗暴了一点罢了. 例如如下C++程序:
|
|
这个程序啥也不干, 运行后立即返回0并终止. 为了减小例子中编码的大小, 我尽量精简了源代码. 我们采用最简单的ASCII码集编码文本, 那么其文本的十六进制编码为:
| ascii character: | i | n | t | m | a | i | n | ( | ) | { | } | |
|---|---|---|---|---|---|---|---|---|---|---|---|---|
| hex code: | 69 | 6e | 74 | 20 | 6d | 61 | 69 | 6e | 28 | 29 | 7b | 7d |
那么最终的的编码就是文本编码简单地首尾相接, 用十六进制就表示为: 696e74206d61696e28297b7d, 转换成十进制就是32629456264088361407586335613.
是的, 我们把一个简单得也许不能再简单的合法C++程序映射到了一个巨大无比的整数中, 而且编码的大小将以程序长度的指数级增长. 不过我们确实实现了我们的目的, 这样做, 我们可以把任意程序(无论是正确的还是连编译都编译不了的程序)都指派到一个唯一的整数, 甚至还能把编码轻松还原为源程序文本.
既然可以编码C++程序, 那么根据图灵-丘奇论题那一章, 我们就没有理由不相信可以对图灵机编码, 只是编码方式可能略有不同罢了.
给图灵机编码, 我们是想干什么呢? 本质上, 我们是建立了一个图灵机集合到正整数集(或其子集)的一个映射, 这说明全体图灵机集合虽然无穷大, 但至少是可列的. 但更重要的目的是, 我们说明了可以把任意图灵机本身作为数据, 来传递给另一个图灵机作为输入.
在下文中, 我将以$\langle M \rangle$表示一个图灵机$M$的编码(表示), 具体的编码方式其实无关紧要, 只要前后的编码方式一致即可. 另外, 我们还将用$S$表示全体图灵机描述的集合, 并简称为全体图灵机的集合(因为这两个集合没有什么本质上的不同):
$$ S := \{\langle M \rangle\ |\ \text{M is a Turing Machine} \} $$性质/属性(Property)
所谓图灵机的性质或属性$P$, 其实就是全体图灵机集合上$S$的一个等价关系, 它把$S$划分成两个部分——一个部分就是拥有该属性的图灵机集合, 剩下一部分就是没有该属性的图灵机集合. 为了简化讨论, 我们也直接把属性指代这个等价关系所诱导的其中一个集合——拥有该属性的集合, 即: $P \subseteq S$.
平凡性质
所谓平凡性质, 就是指这个性质要么所有图灵机都有, 要么所有图灵机都没有, 这就叫平凡. 反过来, 非平凡性质就是这个属性不能是图灵机全集本身, 也不能是空集, 即: $ P \subset S \wedge P \neq \emptyset $
关于图灵机所接受语言的非平凡性质
这是在说, 这个非平凡性质$P$是与图灵机所接受的语言相关的——如果两个描述(编码)不同的图灵机接受相同的语言, 那么这两个图灵机应当要么都在$P$中, 要么都不在$P$中. 形式化描述, 即为$P$关于下述命题成立:
解释
现在, 我们就能好好解释一下这整个定理是什么意思了. 它是在说, 对于任意一个满足上面所述要求的性质$P$, $P$本身可以看作一个语言, 那么这个语言是不可判定的. 更直白点说, 是不存在一个算法/图灵机, 使得其能够判断任意的$\langle M \rangle$是否属于$P$.
在尝试证明这个定理之前, 我想先给出一些关于这个定理的例子.
事实上, 我们之前所说的许多不可判定问题, 都是这个定理的一个例子.
例如接受空集问题, 有关于这个问题的性质定义如下:
接受全集问题:
停机问题:
你可以验证一下, 这些性质都是非平凡的(性质非空且非全集), 且都满足上面有关于图灵机所接受语言的命题(元素是否属于一个性质, 只与其所接受的语言有关).
形象点说, 只要你切图灵机全集这块大蛋糕的一刀切刀法满足一些特定的要求, 那么你总是没法把蛋糕上的任意一块面芯子在哪一边给全都分清的.
证明
经过上面的铺垫, 我们终于可以开始着手证明这个定理了. 我们将使用到之前所说的一个强有力工具——规约. 同时, 这个证明也是熟悉规约技巧的一个很好的例子.
由于我们希望证明的是一个命题不可判定, 那么我们应当把这个命题本身规约到一个(也许?)更强的已知不可判定命题上, 在这里, 我选择的所谓"更强"命题是$A_{TM}$, 具体一点, 这个命题是指这么一个语言:
这个语言是一个所有图灵机及其所接受语言对的一个集合. $\langle M,w \rangle$是指将$M$和它所接受的串$w$编码在一起, 可以理解为一个$M$和$w$所组成的一个二元组的编码. 如果这个命题是可判定的, 那么就意味着存在一个图灵机$M_{A_{TM}}$, 它接受任意一个图灵机$M$的描述以及一个串$w$, 然后能够告诉我们这个串$w$是否能够被$M$接受, 也就是能够判定$\langle M,w \rangle$是否在$A_{TM}$这个集合里.
引理: ATM不可判定
这个引理的证明是简单的. 但是需要注意一下, 为了避免循环论证, 我们不能直接套用莱斯定理本身去证明这个引理. 尽管证明确实是可行的——这意味着莱斯定理和这个引理其实等价.
我们使用反证法, 假设就存在判定$A_{TM}$的这么一个图灵机$M_{A_{TM}}$. 于是仿照停机问题不可判定的证明那样, 我们在$M_{A_{TM}}$的基础上, 构造一个唱反调的另一台图灵机$M'$, 构造$M_{A_{TM}}$的矛盾. 这个设计构造如下.
|
|
$M'$的输入是一个图灵机的描述$\langle M \rangle$, 然后改写成$\langle M, \langle M \rangle \rangle$并传给我们的$M_{A_{TM}}$. 如果$M_{A_{TM}}$的结果是接受, 那么$M'$的结果就是拒绝; 反之若$M_{A_{TM}}$的结果是拒绝, 那么$M'$的结果就是接受.
可以知道, 我们构造的这个$M'$判定任意一个图灵机$M$是否不接受自身的描述$\langle M \rangle$. 为了导出矛盾, 我们询问: $M'$在输入为$\langle M' \rangle$, 亦即输入为其自身的描述时会发生什么? 你可以思考一下. 但在此之前, 我需要明确一下构造的合法性. 可能有些人对这些图灵机自指的做法感到担忧, 这里的每一步是否都是可以实现的呢?
可以捋一下我们构造这个$M'$的过程. 在得到$M'$得到它的输入$\langle M' \rangle$后, 改写成$\langle M, \langle M \rangle \rangle$的这一步实际上不过是把输入又复制了一份. 一份作为$M_{A_{TM}}$需要判定的图灵机输入$\langle M \rangle$, 另一份作为需要判定是否被这个图灵机接受的串$w = \langle M \rangle$. 这显然可以实现. 不要被嵌套的尖括号记号给迷惑了.
在$M'$构造完成后, 它本身的描述$\langle M' \rangle$当然是可以得到的了, 然后我们把它的描述喂给它自身, 一切就都大功告成了. 需要注意, $M'$的构造事实上并没有使用到关于它自身的什么信息. 因此构造本身也并没触及自指之类令人可疑的方法. 于是整个构造可行. 这个图灵机$M'$所接受的语言也能够表示出来:
现在我们来看一看$M'$的输入为$\langle M' \rangle$时, 会发生什么.
输入为$\langle M' \rangle$, 亦即我们在询问是否$\langle M' \rangle \overset{?}\in L(M')$.
- 如果$\langle M' \rangle \in L(M')$, 那么根据$L(M')$的定义, 立即有 $\langle M' \rangle \notin L(M')$, 矛盾;
- 如果$\langle M' \rangle \notin L(M')$, 那么根据$L(M')$的定义, 立即有 $\langle M' \rangle \in L(M')$, 矛盾;
通过这一整个合法的证明过程, 我们推导出了左右为难的矛盾. 于是就只能有一个地方不对了, 那就是$M'$根本不能存在, 于是$M_{A_{TM}}$也就不能存在. 这样, 我们就证明了$A_{TM}$不可判定.
从ATM到P的规约
现在回顾一下我们的目标, 我们需要证明莱斯定理中任意满足条件的性质$P$都不可判定, 于是我们考虑把$A_{TM}$规约到$P$上. 这样一旦规约构造完成, 我们就立即证明了$P$也是不可判定的.
不失一般性, 我们设$\langle T_\emptyset \rangle \notin P$, 其中$L(T_\emptyset) = \emptyset$, 即空接受的图灵机不满足性质$P$. 这是合法的, 因为如果$\langle T_\emptyset \rangle \in P$, 我们就可以使用$P$的补集$\bar{P}$代替它来继续证明, 而$P$和$\bar{P}$没有什么本质上的区别——$P$是非平凡且仅与图灵机所接受语言有关的, $\bar{P}$也是如此.
考虑到$P$的非平凡性, 我们知道至少存在一个图灵机具有性质$P$, 我们设这个图灵机为$T$, 于是$\langle T \rangle \in P$.
这样, 我们找到了两个图灵机, 一个具有性质$P$, 而另一个反之. 于是, 我们就能够简单粗暴地写出我们需要的映射函数$f$的定义.
可以验证, $f$就是我们要找的从$A_{TM}$到$P$的一个同态映射, 它满足$\langle M,w \rangle \in A_{TM} \leftrightarrow f(\langle M,w \rangle) \in P$. 然而, 这个函数却并不符合上文映射规约一节中提及的对$f$的要求, 因为这个函数是所对应的图灵机是可能不停机的, 换句话说, 函数可能是不可计算的. 这是因为$w \overset{?}\in L(M)$这个命题可能不可判定. 这样, 我们就没法得出$A_{TM} \leq_m P$. 不过暂且别急, 我们可以先明确构造出函数所对应的图灵机$M_f$.
|
|
$M_f$的设计是这样的: 它接收一个输入$\langle M,w \rangle$, 然后$M_f$从输入$\langle M \rangle$(也就是$M$的描述)构造$M$, 并把$w$传输给构造出来的$M$.
如果$M$接受$w$, 那么输出$\langle T \rangle$, 否则若停机并拒绝$w$, 则输出$\langle T_\emptyset \rangle$. $M$还有一种结果, 那就是不停机. 为了解决这个问题, 我们需要把$M_f$和整个规约的图灵机耦合在一起, 构造一个图灵机$M'$.
|
|
$M'$的构造与$M_f$有些类似, 它接收$\langle M,w \rangle$构造$M$, 将$w$传入$M$.
- 若$M$接受, 那么再接收另一个输入$x$并模拟$T$;
- 若$M$拒绝, 那么接收$x$并模拟$T_\emptyset$. (技术上, 由于$T_\emptyset$接受的语言为空, 因此$x$实际上没有必要传入$T_\emptyset$, 因为它在任意输入$x$上都拒绝.)
如果$M'$不停机, 那么可能是$M$在输入$w$上不停机, 或者在$M$接受以后, $T$在输入$x$上不停机. 但是这都没关系, 只要$M'$不停机, 就实际上同样模拟了$T_\emptyset$, 因为串$x$在一个语言中当且仅当这个语言对应的图灵机停机并接受$x$, 其余情况都是拒绝.
于是现在有:
如果$P$可判定, 那么$A_{TM}$也将可判定, 但是这与事实不符. 于是$P$不可判定, 定理证毕.
注解
在本定理的证明中, 我们构造了一个从已知不可判定命题$A_{TM}$到任意满足条件的性质$P$的规约. 需要注意的是, 由于这个规约中映射函数$f$的可计算性依赖于具体参数$M$的可判定性, 因此这个规约并不能称为映射规约, 不过这个证明巧妙地把$M$不停机的情况对应到了$T_\emptyset$, 使得$A_{TM}$和$P$的对应关系依旧可以成立.
TO BE CONTINUED…