停机问题

定义

停机问题询问：是否存在一个通用算法，能够对任意给定的程序及其输入，判断该程序运行后是会停机还是会无限循环下去。这是计算理论中第一个被严格证明为不可判定的问题。

原理

图灵用反证法证明停机问题无解。假设存在判定程序能正确回答任意程序是否停机，便可构造一个自相矛盾的程序：它先询问自己是否停机，若回答停机就故意进入死循环，若回答不停机就立即停机。这个程序的行为与判定程序的预测永远相反，从而推出矛盾，说明这样的判定程序不可能存在。

意义

停机问题的不可判定性是可计算性理论的里程碑，它确立了算法能力存在客观上限。许多其他问题可通过归约到停机问题来证明同样不可判定，例如判断两个程序是否等价、程序是否会抛出某种错误。这一结论也解释了为何无法编写出能完美检测所有死循环或所有漏洞的工具，对软件验证领域有深远影响。