Articles

Affichage des articles du avril, 2023

停机问题(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...

停机问题(1)- 术语溯源

“ 停机 问题 ” ( the Halting Problem ) 【 1 】 是 计算机理论中流行的一个最基本术语,现在学术界一致认为图灵在 1936 年 论文 “ 论可计算数及其在判定问题上的应用( On Computability Numbers, with an Application to the Entscheidungsproblem ) ” 中 处理的 “ 判定 问题 ” ( Entscheidungsproblem )就是 “ 停机 问题 ” ,然而 图灵在他的论文中从来没有用过 “ 停机 问题 ” 这个术语,那么此术语从何而来? 已知最早使用 “ 停机 问题 ” 一 词是在 Martin Davis 的一个 证明中 【 3 】 ( p.70-71 ):  "Theorem 2.2 There exists a Turing machine whose halting problem is recursively unsolvable. 但是 Davis 在他的 证明没有给出 “ 停机 问题 ” 术语 的出处,所以人们推断这是他的原创。 “The Essential Turing” 一 书的作者 Jack Copeland 这样说【 4 】( p.40) : - The halting problem was so named (and, it appears, first stated) by Martin Davis. The proposition that the halting problem cannot be solved by computing machine is known as the ‘halting theorem’. (It is often said that Turing stated and proved the halting theorem in ‘On Computable Numbers’, but strictly this is not true.) 所以,我 们的问题是: - 为什么要用 “ 停机 问题 ” 替代 图灵 1936 年 论文中的 “ 判定 问题 ” ? - “ 停机 问题 ” 与 图灵 1936 年 论文中的 “ 判定 问题 ” 等价 吗? ...