停机问题（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 NPL in 1953), I unfortunately and promptly forgot the details. This left me with an uneasy feeling that the proof must be long or complicated, but in fact it is so short ans simple that it may be of interest to casual readers. The version below uses CPL, but not in any essential way.

在程序员中，有一个著名的民间传说，认为不可能写出一个可以检查任何其他程序的程序，并且在每一种情况下都能知道它在运行时是否会终止或进入一个死循环。虽然艾伦-图灵曾经给过我一个口头证明（1953年在去NPL开会的火车上），但不幸的是，我很快就忘记了细节。这给我留下了一种不安的感觉，认为这个证明一定很冗长或复杂，但事实上，它是如此的简短和简单，以至于它可能会引起普通读者的兴趣。下面的版本使用了CPL，但不是以任何基本方式。


Suppose T[R] is a Boolean function taking a routine (or program) R with no formal or free variables as its argument and that for all R, T[R]=True if R terminates if run and that T[R]=False if R does not terminate.

假设T[R]是一个布尔函数，以一个没有形式变量或自由变量的例程（或程序）R为参数，对于所有的R，如果R运行终止，T[R]=True，如果R不终止，T[R]=False。


Consider the routine P defined as follows

考虑例行程序P，定义如下


rec routine P

       $L: if T[P] go to L

            return $


If T[P]=True the routine P will loop, and it will only terminate if T[P]=False. In each case T[P]= has exactly the wrong value, and this contradiction shows that the function T cannot exist.

如果T[P]=True，例程P将循环，只有当T[P]=False时才会终止。在每种情况下，T[P]=的值都是错误的，这个矛盾表明函数T不可能存在。


Churchill College,

Cambridge                                

                                          Your faithfully,

                C. Strachey.


参考文献：

【1】https://en.wikipedia.org/wiki/Halting_problem

【2】https://academic.oup.com/comjnl/article/7/4/313/354243


Commentaires

Enregistrer un commentaire

Posts les plus consultés de ce blog

令人不安的哥德尔证明 - 倡议重读哥德尔1931年论文

美国最大出版社诺顿公司在介绍 2021 年出版的哥德尔传记 “ 理性的边缘之旅 - 库尔特 - 哥德尔的一生 ” （ Stephen Budiansky ）时说  [1]  ： 这是第一本为普通读者撰写的关于这位逻辑学家和数学家的重要传记，他的不完备性定理帮助发起了一场现代科学革命。库尔特 - 哥德尔（ Kurt Gödel ）的著名证明，即每个数学系统都必须包含 “ 为真但不可证明的命题 ”—— 在发表后的近一百年里，继续令数学、哲学和计算机科学感到不安。 此说并不夸张，那么哥德尔不完备性定理中到底有什么令人至今不安？如果我们仔细观察，就会发现这种不安并不是 因为哥德尔给出的 形式系统不完备性的 结论，也不是因为 哥德尔在证明中运用了 “ 说谎者悖论 ”，而是 哥德尔 将”自己说自己是不可证明的“ 说谎者悖论 命题当作 形式系统中正常的 “ 不可判定命题 ”了，由此 得出 形式系统中存在如 说谎者悖论 的命题是常态 ！ [2]  哥德尔的证明自发表以来一直受到挑战， 道森（ John W. Dawson Jr. ） 在文章 “ 哥德尔不完备性定理的接受情况（ The reception of Gödel's Incompleteness Theorems）” 中对此进行了梳理  [3]  （ p.74-95 ）： 策梅洛（Ernst Zermelo） 在 1931 年写给哥德尔的信中说，哥德尔对不可判定命题存在性的证明存在一个 “essential gap” ； 逻辑学家佩雷曼（ Chaïm Perelman） 断言，哥德尔发现的实际上是一个二律背反（Antinomy）； 维特根斯坦（Ludwig Wittgenstein）对哥德尔的证明发表了备受争议的评论（ Remarks on the Foundations of Mathematics ， 1938) ； 罗素（Bertrand Russell）在给 亨金（Leon Henkin）的信中表达了他的深刻困惑：我当然意识到哥德尔的工作具有根本的重要性，但我对它感到困惑。 [……] 如果一个给定的公理集导致矛盾，很明显，至少有一个公理必须是错误的。 。。。 还有 埃尔布朗（ Jacques Herbrand）在 1931 年写给哥德尔的信中指出  [4]...
Lire la suite

图灵谁如何定义“可计算性”的？

  I. How did Turing define the computability? Turing's 1936 paper, as its title suggests:  On Computable Numbers, with an Application to the Entscheidungsproblem , aimed to solve the  Entscheidungsproblem  proposed by Hilbert based on c omputable numbers .   Turing answered the Entscheidungsproblem negatively, Turing said: I propose, therefore, to show that there can be no general process for determining whether a given formula A of the functional calculus K is provable (Note: K refers to the first-order predicate), i.e. that there can be no machine which, supplied with any one A of these formulae, will eventually say whether A is provable. Therefore, Turing gave a definition of  decision problem  such that «  there is a general process for determining . . . ».   1. Decision problem     Turing said ([ 1], Section 8) : The expression ''there is a general process for determining . . .'' has been used throughout this section ...
Lire la suite

停机问题（3）- 证明溯源

  There are two versions of the popular proof of the "haling problem": one based on the liar's paradox and the other based on the Cantor’s diagonisation. The academic claims that the halting problem and its proofs are originated from Turing's 1936 paper, which is highly questionable, … Roger Penrose gave an accessible presentation of the proof of the halting problem based on the Cantor’s diagonisation in  The Emperor's New Mind , and I excerpt the relevant content as follows (p.59-64) : A natural question arises: how are we to decide whether or not any particular Turing machine (when fed with some specific input) will ever stop?  … So, is there some algorithmic procedure for answering the general question - the halting problem - completely automatically?  Turing showed that indeed there is not. His argument was essentially the following.  We first suppose that, on the contrary, there is such an algorithm. Then there must be some Turing machine H which 'decides...
Lire la suite