停机问题(2)- 证明溯源
一个流行的关于“停机 问题”不可判定的证明是基于自指的反证法,即基于悖论的证明 【1】。 该证明过程如下: 假 设存在一个可计算的全函数 halts(f) 判定函数 f 是否停机,如果 f 停机, 则返回 true ,否 则返回 false 。 现在考虑下面这个函数 g : def g(): if halts(g): loop_forever() 如果 halts(g) 返回 true ,即 g 停机,那么 g 将 调用 loop_forever 而 g 不停机,矛盾。如果 halts(g) 返回 false ,即 g 不停机,因 为 g 不 调用 loop_forever 而停机,也矛盾。因此,关于存在 halts 是一个可 计算的全函数的最初假设不成立。 函数 g 是一个典型的 “ 判断性 质的自指函数 ” ,本 质上与 “ 说谎者悖论 ” 相同。据文献 记载,这个证明最初出现在英国计算机学者 Christopher Strachey ( 1916-1975 )在 1965 年写 给 The Computer Journal 杂志的一封信中【 2 】。 *** To the Editor, The Computer Journal An impossible program Sir, A well-known piece of folk-lore among programmers holds that is impossible to write a program which can examine any other program and tell, in every case, if it will terminate or get into a closed loop when it is run. I have never actually seen a proof of this in print, and though Alan Turing once gave me a verbal proof (in a railway carriage on the way to a Conference at the...