停机问题(英语:halting problem)是逻辑数学中可计算性理论的一个问题。通俗地说,停机问题就是判断任意一个程序是否能在有限的时间之内结束运行的问题。该问题等价于如下的判定问题:是否存在一个程序P,对于任意输入的程序w,能够判断w会在有限时间内结束或者死循环。
艾伦·图灵在1936年用对角论证法证明了,不存在解决停机问题的通用算法。这个证明的关键在于对计算机和程序的数学定义,这被称为图灵机。停机问题在图灵机上是不可判定问题。这是最早提出的决定性问题之一。
用数学语言描述,则其本质问题为: 给定一个图灵机T,和一个任意语言集合S,是否T会最终停机于每一个
。其意义相同于可确定语言。显然任意有限 S 是可判定性的,可数的(countable)S 也是可停机的。停机问题包含了自我指涉,本质是一阶逻辑的不完备性,类似的命题有理发师悖论、全能悖论等。
假设停机问题有解,即:存在过程H(P, I)可以判断对于程序P在输入I的情况下是否可停机。假设P在输入I时可停机,H输出“停机”,反之输出“死循环”,即可导出矛盾:
显然,程序本身也是一种数据,因此它可以作为输入(例如Pascal的编译器本身就可以用Pascal所写成,所以程序在自己身上运行自己也是合理的),故H应该可以判定当将P作为P的输入时,P是否会停机。然后我们定义一个过程U(P),其流程如下:
伪代码及其注释表示如下:
int H(procedure,Input); // 这里的H函数有两种返回值,死循环(1) 或 停机(0)int U(P){ if (H(P,P) == 1){ // 如果H死循环 return 0; // 此时会停机 }else{ // 否則 while(1){} // 此时会死循环,而這是個空迴圈 }}