柳渝
哥德尔论图灵的可计算性(译文) - Oron Shagrir
2022-12-6 01:30
阅读:1866

这是Oron Shagrir的文章Gödel on Turing on Computability”的第三节Gödel on Turing’s Analysis of Computability”译文:


***

第三节 哥德尔论图灵的可计算性分析


众所周知,在哥德尔的1934年普林斯顿演讲的印刷版中出现了一个似乎很像丘奇-图灵论题的声明。在论文的正文中,哥德尔提出了通常被认为是丘奇-图灵论题的简单部分:

 [原始]递归函数有一个重要的特性,即对于每个给定的参数值集合,函数的值可以通过一个有限的程序计算出来 [348]。


在这一声明的脚注中,哥德尔指出,如果除了[原始]递归[……],其他形式的递归(例如,同时涉及两个变量)也被接受[即一般递归],则反之似乎是真的。这不能被证明,因为有限计算的概念没有被定义,但它可以作为一个启发式的原则” [348页,注3]


然而,在给马丁-戴维斯的信(1965215)中,哥德尔否认1934年的论文预见了丘奇-图灵论题:

- 说脚注3是丘奇论题的陈述是不正确的。那里所说的猜想只是指 "有限(计算)程序 " "递归程序 "的等价性。'有限(计算)程序''递归程序'的等同性。然而,在这些讲座的时候,我根本不相信我的递归概念包括所有可能的递归;事实上,我的定义与Kleene[1936]之间的等价性 Kleene[1936]之间的等价关系并不十分简单。[Davis 1982, p. 8]


事实上,与哥德尔会面的丘奇--显然是在1934年初在写给Kleene的信中对这次会面进行了评论[日期为19351129]:

- 关于哥德尔以及递归性和有效可计算性的概念,其历史如下。在与他[原文如此]讨论lambda-definability的概念时,发现有效可计算性并没有一个好的定义。我提出的将λ-definability作为它的定义的建议,他认为是完全不满意的。


但没过多久,哥德尔的态度发生了变化。在一篇未发表的可能是1938年的论文中,他写道: 

- 当我第一次发表我的关于不可判定命题的论文时,这个结果无法在这种普遍性中被宣布出来。因为对于机械程序和形式系统的概念,当时还没有一个令人满意的数学定义,这个空白后来被赫布兰德,丘奇和图灵填补了 [193?, p. 166]


因此,在拒绝丘奇的提议仅仅四年之后,哥德尔就接受了丘奇的提议,把可计算性的 "数学上令人满意的定义归功于赫布兰德、丘奇和图灵。为什么哥德尔会改变主意?很难肯定地说,但显然,图灵的工作是一个重要因素。最初,他将图灵与赫布兰德和丘奇放在一起提及,但在几年之后,哥德尔将图灵的工作称为证明了数学定义的正确性,“这确实是机械可计算性的正确定义,是由图灵毫无疑问地确立的” [168]。更具体地说:

[图灵]已经表明,以这种方式定义的可计算函数正是那些可以用有限数量的部件构造一台机器,而这台机器将做以下事情。如果你在一张纸条上写下任何数字n1,…,nr,并把纸条放进机器,然后转动曲柄,那么,在转动有限的次数之后,机器就会停止,参数n1,...,nr的函数值将被打印在纸上[168]


从这一点上说,哥德尔把图灵的工作称为建立了机械可计算性的正确定义。在他的吉布斯讲座中,例如,他宣称: 

- 最大的改进是通过对有限程序概念的精确定义来实现的,它在这些结果中起着决定性的作用。有几种不同的方法可以得出这样的定义,但是,它们都导致了完全相同的概念。在我看来,最令人满意的方式是将有限程序的概念简化为具有有限部件数量的机器的概念,正如英国数学家图灵所做的那样[Gödel 1951,第304-305]


而在他1964年对1934年文章的后记中,哥德尔重申了这一点:

- 由于后来的进展,特别是由于图灵的工作,对形式系统的一般概念有了一个精确的、毫无疑问的充分定义,现在,对于每一个包含一定数量的有限数论的一致形式系统,都可以严格地证明不可判定的算术命题的存在和同一系统的一致性的不可证明性。图灵的工作给出了对机械程序(别名'算法''计算程序''有限组合程序')概念的分析。这一概念被证明与图灵机的概念是等同的[369-370]


一般来说,无论我们使用图灵对可计算性的精确定义还是其他定义,例如一般递归性,从哥德尔的角度来看都是不相关的。然而,哥德尔一直呼吁的是图灵的分析,以说明这些可计算性的等价定义的正确性。这是很重要的一点,图灵的论证直到最近才被充分认识。图灵同时代的人提到了这个分析,以及其他熟悉的论证,例如不同概念的汇合、准经验证据以及丘奇的逐步论证,但并没有赋予它任何特殊的优点。有鉴于此,哥德尔对图灵的分析作为可计算性定义的判定性论证的赞扬是值得注意的。


尽管如此,由于哥德尔并没有解释到底是什么让图灵的概念分析如此令人信服,让我首先澄清一下。首先,哥德尔倾向于概念分析而非其他论证。他认为定义可计算性的问题是一个很好的例子[......],这个概念对我们来说并不尖锐,但经过仔细的思考之后就变得尖锐了”[Wang 1974, p. 84]。他还说,图灵的工作对'机械程序'的概念进行了分析。[......]这个概念被证明与图灵机的概念是等价的(我的强调)而且,任何理解这个问题并知道图灵定义的人绝对不可能决定使用一个不同的概念”[Wang 1974, p. 84]。第二,图灵的分析是基于公理的方法,约束被表述为基本公理。这是哥德尔在1934年与丘奇的谈话中推荐的方法,他在谈话中拒绝了丘奇的提议,认为其 "完全不能令人满意"。哥德尔向丘奇建议,就作为未定义概念的有效可计算性而言,也许可以陈述一套公理,它将体现这一概念的普遍接受的属性,并在此基础上做一些事情”[Davis 1982, p. 9]


第三,图灵的定义强调了哥德尔所认为的形式系统的判定性属性:被一个有限和机械的程序所支配。让我详细说明一下。图灵与哥德尔在援引可计算性定义的语境中存在着重要的差异。图灵在Entscheidungsproblem的语境中定义可计算性,而哥德尔则认为图灵的定义的意义是在不完全性理论的普遍性背景下的正如他所说,不完全性结果无法在这种普遍性中被宣布直到这个 "空白" 赫布兰德、丘奇和图灵填补。但究竟是如何填补了这个空白?


当哥德尔讨论形式系统时,甚至在1936年之前,他就援引了两个基本属性。1934年,哥德尔在讲话中以形式化数学系统”[346]的特征开篇,强调了有限的属性:

- 我们要求推理规则以及有意义的公式和公理的定义是构造性的;也就是说,对于每一条推理规则,都应该有一个有限的程序来确定一个给定的公式B是否是给定的公式A1...An的直接结果,并且应该有一个有限的程序来确定一个给定的公式A是否是一个有意义的公式或一个公理。[p. 346]


哥德尔[1933b]在美国数学协会的讲话(数学基础的现状)中阐述了机械的属性。他在讲话中首先对形式系统进行了粗略的描述,指出推理规则的突出特点是它们是纯形式的,即只指公式的外在结构,而不是它们的意义,因此它们可以被一个对数学一无所知的人应用,或者被一台机器应用”[45] 。从哥德尔的角度来看,图灵在用具有有限部件数的机器”(强调是后加的),即用图灵机来定义可计算性时,提供了一个明确满足这两种约束的程序的精确数学特征。因此,图灵提供了形式系统一般概念的精确和毫无疑问的充分定义,因此不完全性结果对于每一个包含一定数量的有限数论的一致的形式系统都是真的。


然而,需要注意的是,尽管哥德尔在提到形式系统时,在机械程序有限程序这两个术语之间摇摆不定,但他明确指出,它们不是同义词。此外,虽然哥德尔认为在形式系统的背景下,有限和机械约束是并存的,即程序必须满足这两种约束,但他并不认为它们在其他背景下是一致的。特别是,他坚持认为存在非机械的有限程序:是否存在与任何算法不等价的有限非机械程序的问题,与'形式系统''机械程序'的定义是否充分没有任何关系” [Gödel 1964, p. 370]。在一个脚注中,他提到了他1958年的文章,在那里他提出了可以被理解为满足有限性要求的程序,因为它们是构造性的,但又是非机械性的,因为它们涉及在其意义基础上使用抽象术语”[同上,注36]


原文:


https://openscholar.huji.ac.il/sites/default/files/oronshagrir/files/godel_on_turing_book_version_0.pdf


Oron ShagrirDepartments of Philosophy and Cognitive Science, The Hebrew University of Jerusalem.


3. Gödel  on Turing’s Analysis of Computability


It is well known that a statement that seems to be much like the Church–Turing thesis appears in the printed version of Gödel ’s 1934 Princeton lectures. In the body of the paper, Gödel  formulates what is generally taken to be the “easy” part of the Church–Turing thesis:


“[primitive] recursive functions have the important property that, for each given set of values of the arguments, the value of the function can be computed by a finite procedure” [p. 348]. 


In a footnote to this statement, Gödel  remarks that “the converse seems to be true if, besides [primitive] recursions [...] recursions of other forms (e.g., with respect to two variables simultaneously) are admitted [i.e., general recursions]. This cannot be proved, since the notion of finite computation is not defined, but it serves as a heuristic principle” [p. 348, note 3]. 


However, in a letter to Martin Davis (February 15, 1965), G¨odel denies that the 1934 paper anticipated the Church–Turing thesis:


It is not true that footnote 3 is a statement of Church’s Thesis. The conjecture stated there only refers to the equivalence of ‘finite (computation) procedure’ and ‘recursive procedure.’ However, I was, at the time of these lectures, not at all convinced that my concept of recursion comprises all possible recursions; and in fact the equivalence between my definition and Kleene [1936] is not quite trivial. [Davis 1982, p. 8]


Indeed, Church, who met with G¨odel—apparently, early in 1934 — commented on the encounter in a letter to Kleene [dated November

29, 1935]:


In regard to Gödel  and the notions of recursiveness and effective calculability, the history is the following. In discussion with him [sic] the notion of lambda-definability, it developed that there was no good definition of effective calculability. My proposal that lambda-definability be taken as a definition of it he regarded as thoroughly unsatisfactory.


But before too long, Gödel ’s attitude changed. In an unpublished paper, probably from 1938, he writes:


When I first published my paper about undecidable propositions the result could not be pronounced in this generality, because for the notions of mechanical procedure and of formal system no mathematically satisfactory definition had been given at that time. This gap has since been filled by Herbrand, Church and Turing [193?, p. 166].


Thus just four years after having rejected it, G¨odel embraces Church’s proposal, attributing the “mathematically satisfactory definition” of computability to Herbrand, Church and Turing. Why did G¨odel change his mind? It is difficult to say with certainty, but clearly, Turing’s work was a significant factor. Initially, he mentions Turing together with Herbrand and Church, but a few pages later Gödel  refers to Turing’s work as having demonstrated the correctness of the mathematical definition(s): “that this really is the correct definition of mechanical computability was established beyond any doubt by Turing” [p. 168]. More specifically:


[Turing] has shown that the computable functions defined in this way are exactly those for which you can construct a machine with a finite number of parts which will do the following thing. If you write down any number n1,...,nr on a slip of paper and put the slip into the machine and turn the crank, then after a finite number of turns the machine will stop and the value of the function for the argument n1,...,nr will be printed on the paper [p. 168].


From this point on, Gödel  refers to Turing’s work as establishing the “correct definition” of mechanical computability. In his Gibbs Lecture, for instance, he declares:


The greatest improvement was made possible through the precise definition of the concept of finite procedure, which plays a decisive role in these results. There are several different ways of arriving at such a definition, which, however, all lead to exactly the same concept. The most satisfactory way, in my opinion, is that of reducing the concept of finite procedure to that of a machine with a finite number of parts, as has been done by the British mathematician Turing [Gödel  1951, pp. 304–305].


And in his 1964 postscript to the 1934 article, Gödel  reaffirms:


In consequence of later advances, in particular of the fact that, due to A.M. Turing’s work, a precise and unquestionably adequate definition of the general concept of formal system can now be given, the existence of undecidable arithmetical propositions and the non-demonstrability of the consistency of a system in the same system can now be proved rigorously for every consistent formal system containing a certain amount of finitary number theory. Turing’s work gives an analysis of the concept of ‘mechanical procedure’ (alias ‘algorithm’ or ‘computation procedure’ or ‘finite combinatorial procedure’). This concept is shown to be equivalent with that of a ‘Turing machine’ [pp. 369–370].


Generally speaking, whether we use Turing’s precise definition of computability or other definitions, e.g., general recursiveness, is irrelevant from G¨odel’s perspective.16 After all, they have been proven to be extensionally equivalent. Yet it is Turing’s analysis that G¨odel consistently appeals to as accounting for the correctness of these equivalent definitions of computability. This is a significant point. Turing’s argument has been fully appreciated only recently.17 Turing’s contemporaries mention the analysis, along other familiar arguments, e.g., the confluence of different notions, quasi-empirical evidence, and Church’s step-by step argument, but do not ascribe it any special merit.18 Logic and computer science textbooks from the decades following the pioneering work of the 1930s ignore it altogether.19 In light of this, Gödel ’s praise of Turing’s analysis as the decisive argument for the definition of computability is noteworthy.


Nevertheless, as Gödel  does not explain just what it is that makes Turing’s conceptual analysis so convincing, let me begin by clarifying this. First, Gödel  favors conceptual analyses over other arguments. He sees the problem of defining computability as “an excellent example [...] of a concept which did not appear sharp to us but has become so as a result of a careful reflection” [Wang 1974, p. 84]. He also says that “Turing’s work gives an analysis of the concept of ‘mechanical procedure.’ [...] This concept is shown to be equivalent with that of a Turing machine” (my emphasis),21 and, that it is “absolutely impossible that anybody who understands the question and knows Turing’s definition should decide for a different concept” [Wang 1974, p. 84]. Second, Turing’s analysis is based on an axiomatic approach, the constraints being formulated as basic axioms. This is the approach Gödel  recommends in his 1934 conversation with Church, in which he rejects Church’s proposal as “thoroughly unsatisfactory.” Gödel suggests to Church that “it might be possible, in terms of an effective calculability as an undefined notion, to state a set of axioms which would embody the generally accepted properties of this notion, and to do something on that basis” [Davis 1982, p. 9].


Third, Turing’s definition highlights what Gödel takes to be the defining properties of a formal system: being governed by a procedure that is finite and mechanical. Let me elaborate. There is an important difference in the contexts in which Turing and Gödel invoke the definition of computability. While Turing defines computability in the context of the Entscheidungsproblem, Gödel sees the significance of Turing’s definition in the context of the generality of the incompleteness theorems.23 As he says, the incompleteness results “could not be pronounced in this generality,”24 until the “gap” was “filled by Herbrand, Church and Turing.” But how exactly has the gap been filled?


When Gödel discusses formal systems, even before 1936, he invokes two essential properties. The property of being finite is stressed in 1934, where Gödel opens his address with a characterization of a “formal mathematical system” [p. 346]:


We require that the rules of inference, and the definitions of meaningful formulas and axioms, be constructive; that is, for each rule of inference there shall be a finite procedure for determining whether a given formula B is an immediate consequence (by that rule) of given formulas A1,..., An, and there shall be a finite procedure for determining whether a given formula A is a meaningful formula or an axiom. [p. 346]


The property of being mechanical is spelled out in Gödel’s [1933b] address to the Mathematical Association of America (“The Present Situation in the Foundations of Mathematics”). He opens the address with a rough characterization of formal systems, pointing out that the “outstanding feature of the rules of inference being that they are purely formal, i.e., refer only to the outward structure of the formulas, not to their meaning, so that they could be applied by someone who knew nothing about mathematics, or by a machine” [p. 45]. From Gödel’s perspective, Turing, in defining computability in terms of “a machine with a finite number of parts” (emphasis added), i.e., in terms of a Turing machine, provides a precise mathematical characterization of a procedure that explicitly satisfies both constraints. As such, Turing provides “a precise and unquestionably adequate definition of the general concept of formal system,” hence the incompleteness results are true for “every consistent formal system containing a certain amount of finitary number theory.”


It is important to note, however, that although Gödel vacillates between the terms ‘mechanical procedure’ and ‘finite procedure’ when referring to formal systems,26 he makes clear that they are not synonymous. Moreover, while G¨odel takes the finite and mechanical constraints to go hand in hand in the context of a formal system, in the sense that the procedure must satisfy both constraints, he does not maintain that they coincide in other contexts. In particular, he insists that there are finite procedures that are non-mechanical: “the question of whether there exist finite non-mechanical procedures, not equivalent with any algorithm, has nothing whatsoever to do with the adequacy of the definition of ‘formal system’ and of ‘mechanical procedure’” [Gödel 1964, p. 370]. In a footnote he refers to his 1958 article, where he posits procedures that can be construed as fulfilling the finiteness requirement, in that they are constructive, yet are non-mechanical in that they “involve the use of abstract terms on the basis of their meaning” [ibid., note 36].28 As we will now see, these procedures play an important role in Gödel’s critique of Turing.


转载本文请联系原作者获取授权,同时请注明本文来自柳渝科学网博客。

链接地址:https://wap.sciencenet.cn/blog-2322490-1366697.html?mobile=1

收藏

分享到:

当前推荐数:1
推荐人:
推荐到博客首页
网友评论2 条评论
确定删除指定的回复吗?
确定删除本博文吗?