16.2 可判定性与不可判定性
可计算性理论按照算法所能做出的保证来对各类数学问题进行分类。判定问题(decision problem)对编码后的输入提出 是/否(yes/no)的问题,因此在数学上可等同为一种语言(language):即所有让答案为“是”的输入编码集合。例如:“这个记号流(token stream)是否由语法 G(grammar)生成?”“这个控制流图(control-flow graph)是否有环?”“图灵机 M 是否接受(accept)输入 w?”
若存在一个判定器(decider)对每一个可能的输入都保证最终停机并正确回答属于或不属于该集合,则该语言/问题是可判定的(decidable)。若存在一个识别器(recognizer)能保证接受每一个属于该集合的成员(member),但对非成员(nonmember)可以拒绝或永远无限运行下去,则该语言是可识别的(recognizable / recursively enumerable)。每一个 decidable 的语言都必然是 recognizable 的,但反过来,有些可识别的语言却在数学上被证明是不可判定的。
停机行为区分判定器与识别器
对于可识别的语言,可以通过穷举模拟来枚举所有的候选计算步骤;当接受凭证(accepting witness)确实存在时,只要模拟足够长的时间,最终总能找到它。然而,即便已经模拟运行了一百万步仍没找到,并不能在数学上证明该成员确实不属于此集合。这也完美解释了为什么现代编译器的底层搜索过程(search procedure)通常会有三种可用的运行输出(operational outcomes):已证明(proved)、已证伪(disproved)以及不确定/超时(unknown/timeout),尽管它们的具体内部逻辑比抽象的图灵机模型复杂得多。
若一个问题语言 L 与其补集 ¬L 都是 recognizable 的,那么 L 就是 decidable 的。我们可以采用交错执行(dovetailing)的精妙工程策略同时运行两个识别器:交替各模拟一步,如此循环。由于数理确定性,最终有且仅有一方会接受,我们便可由此彻底停机并得出答案。如果选择先把第一个识别器跑完再启动第二个,则不具有可行性,因为第一个识别器可能会陷入无限死循环从而永远无法将执行权交给第二个。
诸如有限状态问题(Finite-state problem)、固定上下文无关语法(context-free grammar)的语法分析(parsing)、被刻意设计为完全可判定的强类型系统、图可达性分析以及有界模型检测(bounded model checking)在数学上都是完全可判定的,尽管它们的计算复杂度可能依然很高:“可判定(decidable)”并不直接等同于“执行快速”。相反,不可判定性(undecidability)是比计算困难性更深一层的理论壁垒:即表明在原则上根本不存在任何能够对每一个输入都保证停机并输出 是/否 正确答案的算法。
归约(Reduction)可以转移不可能性
为了证明一个新遇到的问题 B 是不可判定(undecidable)的,我们通常会将一个已知的不可判定问题 A 归约(reduce)到它。多一归约(Many-one reduction)通过构造一个全停机且可计算的转换函数 f,使其满足:
x ∈ A 当且仅当 f(x) ∈ B若问题 B 的 decider 确实存在,我们就可以对任意输入 x 快速计算出 f(x),然后再调用 B 的判定器来终极决定 A 属于与否,这便直接与“A 是不可判定的”这一已知结论相矛盾。在这里,归约的方向非常重要:表示为 A ≤ B,意味着“B 至少和 A 一样难”。错误地将一个新目标归约到已知的困难问题上,并不能证明这个目标本身也是困难的。
一个严谨的可计算归约证明必须:对每一个源输入都清晰定义一种转换逻辑;严格说明该转换必定能在有限步骤内终止且完全是可计算的;并分别证明在“是”方向与“否”方向下的等价属于关系。仅仅“两个问题的逻辑形式看起来相似”并不能构成合法的 reduction 证明。若归约的目标是其补集,还必须在变换时严谨地反转其成员等价性。
限制问题可以恢复可判定性
即便一个核心的通用问题在数学上是不可判定的(undecidable),这并不妨碍我们在工业界使用各种实用的可判定子集与片段(decidable fragments)。例如,有限状态程序(Finite-state program)的终止性(termination)是完全可判定的,因为一旦出现相同的运行状态(configuration)重复,就能直接暴露存在控制流无限死循环(loop);结构化递归语言(structurally recursive language)中,若其递归参数被类型检查器(type checker)强制要求严格递减,其终止性也可能是完全可判定的;确定性有限自动机(DFA)的等价性(equivalence)是可判定(decidable)的,但在图灵完备语言下的任意程序等价性(arbitrary program equivalence)则是彻底不可判定的。
这是极具实战指导意义的语言设计(language-design)杠杆。宏系统(Macro system)可以严令禁止无界递归,以保证宏展开(expansion)必定能在有限步骤内安全终止;查询语言(query language)可以强硬限制循环迭代(iteration)的深度;定理证明助理(proof assistant)可强制要求用户必须编写全函数(total function)或显式提供终止性证明凭证;编译器的常量求值器(compiler constant evaluator)可主动设置执行步数与内存上限(limit),在超限时优雅地返回“该表达式不是一个合法的编译期常量(compile-time constant)”,而不是不切实际地向用户承诺去判定任意图灵完备代码的执行。
在论证这类问题时,我们必须极其精确地说明输入的定义域(input domain)。“分析器(Analyzer)对于最多仅包含 20 个布尔变量(Boolean variables)且内部循环(loops)有界的特定程序必定能够终止”,该论断与“无限制下的通用终止性问题在数学上不可判定”在本质上并不冲突。一个静态分析算法在面对绝大多数主流程序时回答正确、在少数复杂非结构化代码上偶尔选择返回不确定(unknown),这在工业界实践中也完全不冲突。不可判定性所严厉禁止的,是妄图在图灵完备的领域(Turing-complete domain)上实现全停机(total)且全局绝对正确的通用判定过程(decision procedure)。
所以在阅读任何声称的可计算性结论(computability claim)时,我们应当首先严谨地自问四个问题:究竟是在对什么格式的输入进行编码?算法是否必须对所有毫无限制的输入保证停机?“是”与“否”两种答案是否都必须绝对正确?是否在允许保留“不确定(unknown)”这一诚实且安全的出口?这些关键的设计细节能帮我们在工程中精准地区分:判定器、识别器、半判定过程(semi-decision procedure)、有界校验器以及启发式算法(heuristic),也能巧妙地避免将死板的理论边界生套到定理(theorem)根本未曾覆盖的广阔工程沃土上。