更改

自20世纪70年代以来，计算机的交互式使用变得更加普遍。原则上，可以通过让外部代理与图灵机同时从纸带中读出并写入纸带的方式进行建模，但这很少与交互的实际发生方式相吻合；因此，在描述交互性时，通常首选I/O自动机等替代程序。

自20世纪70年代以来，计算机的交互式使用变得更加普遍。原则上，可以通过让外部代理与图灵机同时从纸带中读出并写入纸带的方式进行建模，但这很少与交互的实际发生方式相吻合；因此，在描述交互性时，通常首选I/O自动机等替代程序。

==History==

==历史==

They were described in 1936 by Alan Turing.

[[Robin Gandy]] (1919–1995)—a student of Alan Turing (1912–1954), and his lifelong friend—traces the lineage of the notion of "calculating machine" back to [[Charles Babbage]] (circa 1834) and actually proposes "Babbage's Thesis":

===Historical background: computational machinery===

罗宾•甘迪（Robin Gandy，1919-1995)是图灵(1912-1954)的学生，也是他一生的朋友，他将“计算机器”这一概念的渊源追溯到查尔斯•巴贝奇（Charles Babbage） (大约1834年) ，并提出了“ 巴贝奇论” :

[[Robin Gandy]] (1919–1995)—a student of Alan Turing (1912–1954), and his lifelong friend—traces the lineage of the notion of "calculating machine" back to [[Charles Babbage]] (circa 1834) and actually proposes "Babbage's Thesis":

{{quote|整个发展和分析的操作现在都可以由机器来执行.|(italics in Babbage as cited by Gandy, p.54)}}

Gandy's analysis of Babbage's [[Analytical Engine]] describes the following five operations (cf. p. 52–53):

Gandy's analysis of Babbage's [[Analytical Engine]] describes the following five operations (cf. p. 52–53):

甘迪对巴贝奇分析机的分析描述了以下五种操作(参见。第52-53页) :

甘迪对巴贝奇分析机的分析描述了以下五种操作:

# The arithmetic functions +, −, ×, where − indicates "proper" subtraction {{nowrap|''x'' − ''y'' {{=}} 0}} if {{nowrap|''y'' ≥ ''x''}}.

# The arithmetic functions +, −, ×, where − indicates "proper" subtraction {{nowrap|''x'' − ''y'' {{=}} 0}} if {{nowrap|''y'' ≥ ''x''}}.

The arithmetic functions +, −, ×, where − indicates "proper" subtraction  0}} if  {{nowrap|''y'' ≥ ''x''}}.

The arithmetic functions +, −, ×, where − indicates "proper" subtraction  0}} if  {{nowrap|''y'' ≥ ''x''}}.

算术函数 + ,-，× ，其中-表示“适当的”减法x-y=0,如果y ≥x。

# 算术函数 +, -，×，其中“-”表示“适当的”减法，即满足某种条件，比如y≥x，x-y=0。

# Any sequence of operations is an operation.

# Any sequence of operations is an operation.

任何运算序列都是一个运算。

# 任何运算序列都是一个运算。

# Iteration of an operation (repeating n times an operation P).

# Iteration of an operation (repeating n times an operation P).

# 操作的迭代(重复n次操作p)。

 

操作的迭代(重复 n 次操作 p)。

# Conditional iteration (repeating n times an operation P conditional on the "success" of test T).

# Conditional iteration (repeating n times an operation P conditional on the "success" of test T).

条件迭代(以测试 t 的“成功”为条件重复 n 次操作 p)。

# 条件迭代(以测试t的“成功”为条件重复n次操作p)。

# Conditional transfer (i.e., conditional "[[goto]]").

# Conditional transfer (i.e., conditional "[[goto]]").

# 条件转移(即有条件的“goto”)。

 

条件转移(即有条件的“ goto”)。

Gandy states that "the functions which can be calculated by (1), (2), and (4) are precisely those which are [[Turing computable]]." (p. 53). He cites other proposals for "universal calculating machines" including those of [[Percy Ludgate]] (1909), [[Leonardo Torres y Quevedo]] (1914), [[Maurice d'Ocagne]] (1922), [[Louis Couffignal]] (1933), [[Vannevar Bush]] (1936), [[Howard Aiken]] (1937). However:

Gandy states that "the functions which can be calculated by (1), (2), and (4) are precisely those which are [[Turing computable]]." (p. 53). He cites other proposals for "universal calculating machines" including those of [[Percy Ludgate]] (1909), [[Leonardo Torres y Quevedo]] (1914), [[Maurice d'Ocagne]] (1922), [[Louis Couffignal]] (1933), [[Vannevar Bush]] (1936), [[Howard Aiken]] (1937). However:

Gandy指出: “可由(1)、(2)和(4)计算出来的函数恰恰是那些图灵可计算的函数。”(p. 53).他引用了其他关于“通用计算机”的提议，包括珀西 · 卢德盖特Percy Ludgate (1909年)、莱昂纳多 · 托雷斯 · 奎维多Leonardo Torres y Quevedo(1914年)、莫里斯 · d’奥卡涅Maurice d'Ocagne (1922年)、路易斯 · 库夫尼纳尔Louis Couffignal(1933年)、万尼瓦尔 · 布什Vannevar Bush (1936年)、霍华德 · 艾肯Howard Aiken(1937年)。然而:

Gandy指出: “可由(1)、(2)和(4)计算出来的函数恰恰是那些图灵可计算的函数。”(p. 53).他引用了其他关于“通用计算机”的理论，包括珀西·卢德盖特（Percy Ludgate， 1909年)、莱昂纳多 · 托雷斯 · 奎维多（Leonardo Torres y Quevedo，1914年)、莫里斯 · d’奥卡涅（Maurice d'Ocagne，1922年)、路易斯 · 库夫尼纳尔（Louis Couffignal，1933年)、万尼瓦尔 · 布什V（annevar Bush，1936年)、霍华德 · 艾肯（Howard Aiken，1937年)。然而:

{{quote|… the emphasis is on programming a fixed iterable sequence of arithmetical operations. The fundamental importance of conditional iteration and conditional transfer for a general theory of calculating machines is not recognized…|Gandy p. 55}}

{{quote|… the emphasis is on programming a fixed iterable sequence of arithmetical operations. The fundamental importance of conditional iteration and conditional transfer for a general theory of calculating machines is not recognized…|Gandy p. 55}}

...强调的是一个固定的可迭代的算术运算序列的编程。没有认识到条件迭代和条件转移对一般计算机理论的根本重要性......。

{{quote|...重点是对一个固定的可迭代的算术运算序列进行编程。条件性迭代和条件性转移对于计算机的一般理论的根本重要性没有得到承认...

With regard to [[Hilbert's problems]] posed by the famous mathematician [[David Hilbert]] in 1900, an aspect of problem #10 had been floating about for almost 30 years before it was framed precisely. Hilbert's original expression for #10 is as follows:

With regard to [[Hilbert's problems]] posed by the famous mathematician [[David Hilbert]] in 1900, an aspect of problem #10 had been floating about for almost 30 years before it was framed precisely. Hilbert's original expression for #10 is as follows:

{{quote|'''10. Determination of the solvability of a Diophantine equation'''. Given a [[Diophantine equation]] with any number of unknown quantities and with rational integral coefficients: To devise a process according to which it can be determined in a finite number of operations whether the equation is solvable in rational integers.

当我们知道一个程序，允许任何给定的逻辑表达式通过有限的多次操作来决定其有效性或可满足性时，决策问题（一阶逻辑的决定问题）就解决了......决策问题必须被认为是数理逻辑的主要问题。--2008年，德尔肖维茨（Dershowitz）和古列维奇（Gurevich）引用了此译文和德文原文}}

By 1922, this notion of "[[Entscheidungsproblem]]" had developed a bit, and [[Heinrich Behmann|H. Behmann]] stated that

By 1922, this notion of "[[Entscheidungsproblem]]" had developed a bit, and [[Heinrich Behmann|H. Behmann]] stated that

{{quote|... most general form of the Entscheidungsproblem [is] as follows:

{{quote|...决策问题的一般形式如下:

 

 

 

 

需要一个相当明确的、普遍适用的处方，它将允许人们在有限的步骤中决定一个给定的纯逻辑论断的真假... ..

需要一个相当明确的、普遍适用的处方，它将允许人们在有限的步骤中决定一个给定的纯逻辑论断的真假... ..

—Gandy，第57页，引用Behmann的话。

—Gandy，第57页，引用Behmann的话。}}

{{quote|Behmann remarks that ... the general problem is equivalent to the problem of deciding which mathematical propositions are true.|''ibid.''}}

{{quote|Behmann remarks that ... the general problem is equivalent to the problem of deciding which mathematical propositions are true.|''ibid.''}}

Behmann指出，......一般问题相当于决定哪些数学命题是真的问题。

Behmann指出......一般问题相当于决定哪些数学命题是真的问题。

 

{{quote|If one were able to solve the Entscheidungsproblem then one would have a "procedure for solving many (or even all) mathematical problems".|''ibid.'', p. 92}}

{{quote|If one were able to solve the Entscheidungsproblem then one would have a "procedure for solving many (or even all) mathematical problems".|''ibid.'', p. 92}}

如果一能够解决判定问题，那么人们就会有一个 "解决许多（甚至所有）数学问题的程序"。

如果能够解决决策问题，那么人们就会有一个"解决许多（甚至所有）数学问题的程序"。

By the 1928 international congress of mathematicians, Hilbert "made his questions quite precise. First, was mathematics ''[[Completeness (logic)|complete]]'' ... Second, was mathematics ''[[Consistency proof|consistent]]'' ... And thirdly, was mathematics ''[[Decidability (logic)|decidable]]''?" (Hodges p. 91, Hawking p. 1121). The first two questions were answered in 1930 by [[Kurt Gödel]] at the very same meeting where Hilbert delivered his retirement speech (much to the chagrin of Hilbert); the third—the Entscheidungsproblem—had to wait until the mid-1930s.

By the 1928 international congress of mathematicians, Hilbert "made his questions quite precise. First, was mathematics ''[[Completeness (logic)|complete]]'' ... Second, was mathematics ''[[Consistency proof|consistent]]'' ... And thirdly, was mathematics ''[[Decidability (logic)|decidable]]''?" (Hodges p. 91, Hawking p. 1121). The first two questions were answered in 1930 by [[Kurt Gödel]] at the very same meeting where Hilbert delivered his retirement speech (much to the chagrin of Hilbert); the third—the Entscheidungsproblem—had to wait until the mid-1930s.

1928年的国际数学家大会，希尔伯特把他的问题描述的非常的细致。第一，数学是完整的吗? 第二，数学是一致的吗? 第三，数学是可判定的吗? ”1930年，在希尔伯特发表退休演讲的同一次会议上，库尔特 · 哥德尔(Kurt Gödel)回答了前两个问题; 而第三个问题（决策问题）不得不等到上世纪30年代中期。

 

到了1928年的国际数学家大会，Hilbert把他的问题说得非常精确。第一，数学是完整的吗? 第二，数学是一致的吗? 第三，数学是可判定的吗? ”(Hodges p. 91，Hawking p. 1121)。1930年，在Hilbert发表退休演讲的同一次会议上，库尔特 · 哥德尔(Kurt Gödel)回答了前两个问题(这让Hilbert颇为懊恼) ; 而第三个问题（判定问题）不得不等到上世纪30年代中期。

The problem was that an answer first required a precise definition of "''definite general applicable prescription''", which Princeton professor [[Alonzo Church]] would come to call "[[effective calculability]]", and in 1928 no such definition existed. But over the next 6–7 years [[Emil Post]] developed his definition of a worker moving from room to room writing and erasing marks per a list of instructions (Post 1936), as did Church and his two students [[Stephen Kleene]] and [[J. B. Rosser]] by use of Church's [[lambda-calculus]] and Gödel's [[recursion theory]] (1934). Church's paper (published 15 April 1936) showed that the Entscheidungsproblem was indeed "undecidable" and beat Turing to the punch by almost a year (Turing's paper submitted 28 May 1936, published January 1937). In the meantime, Emil Post submitted a brief paper in the fall of 1936, so Turing at least had priority over Post. While Church refereed Turing's paper, Turing had time to study Church's paper and add an Appendix where he sketched a proof that Church's lambda-calculus and his machines would compute the same functions.

The problem was that an answer first required a precise definition of "''definite general applicable prescription''", which Princeton professor [[Alonzo Church]] would come to call "[[effective calculability]]", and in 1928 no such definition existed. But over the next 6–7 years [[Emil Post]] developed his definition of a worker moving from room to room writing and erasing marks per a list of instructions (Post 1936), as did Church and his two students [[Stephen Kleene]] and [[J. B. Rosser]] by use of Church's [[lambda-calculus]] and Gödel's [[recursion theory]] (1934). Church's paper (published 15 April 1936) showed that the Entscheidungsproblem was indeed "undecidable" and beat Turing to the punch by almost a year (Turing's paper submitted 28 May 1936, published January 1937). In the meantime, Emil Post submitted a brief paper in the fall of 1936, so Turing at least had priority over Post. While Church refereed Turing's paper, Turing had time to study Church's paper and add an Appendix where he sketched a proof that Church's lambda-calculus and his machines would compute the same functions.

The problem was that an answer first required a precise definition of "definite general applicable prescription", which Princeton professor Alonzo Church would come to call "effective calculability", and in 1928 no such definition existed. But over the next 6–7 years Emil Post developed his definition of a worker moving from room to room writing and erasing marks per a list of instructions (Post 1936), as did Church and his two students Stephen Kleene and J. B. Rosser by use of Church's lambda-calculus and Gödel's recursion theory (1934). Church's paper (published 15 April 1936) showed that the Entscheidungsproblem was indeed "undecidable" and beat Turing to the punch by almost a year (Turing's paper submitted 28 May 1936, published January 1937). In the meantime, Emil Post submitted a brief paper in the fall of 1936, so Turing at least had priority over Post. While Church refereed Turing's paper, Turing had time to study Church's paper and add an Appendix where he sketched a proof that Church's lambda-calculus and his machines would compute the same functions.

The problem was that an answer first required a precise definition of "definite general applicable prescription", which Princeton professor Alonzo Church would come to call "effective calculability", and in 1928 no such definition existed. But over the next 6–7 years Emil Post developed his definition of a worker moving from room to room writing and erasing marks per a list of instructions (Post 1936), as did Church and his two students Stephen Kleene and J. B. Rosser by use of Church's lambda-calculus and Gödel's recursion theory (1934). Church's paper (published 15 April 1936) showed that the Entscheidungsproblem was indeed "undecidable" and beat Turing to the punch by almost a year (Turing's paper submitted 28 May 1936, published January 1937). In the meantime, Emil Post submitted a brief paper in the fall of 1936, so Turing at least had priority over Post. While Church refereed Turing's paper, Turing had time to study Church's paper and add an Appendix where he sketched a proof that Church's lambda-calculus and his machines would compute the same functions.

问题在于，要回答这个问题，首先需要对“明确的通用规则”下一个精确定义。后来，普林斯顿大学的教授阿朗佐•丘奇Alonzo Church将其称为“有效可计算性”，而在1928年并不存在这样的定义。但在接下来的6-7年里，埃米尔•波斯特Emil Post 发展了他的定义，即一个工人按照一张指令表从一个房间移动到另一个房间书写和擦除标记（1936），Church和他的两个学生斯蒂芬•克莱恩Stephen Kleene和 j.B. Rosser也是如此， 利用 Church 的 λ微积分和哥德尔的递归理论。Church的论文(发表于1936年4月15日)表明，判定问题确实是“无法判定的” ，比Turing早了将近一年(Turing的论文1936年5月28日提交，1937年1月发表)。与此同时，Emil Post 在1936年秋天提交了一篇简短的论文，所以图灵至少比波斯特更有优先权。当丘奇评审图灵的论文时，图灵有时间研究丘奇的论文，并在附录中添加了一个草图，证明Church的λ 微积分和他的机器可以计算同样的函数。

问题在于，要回答这个问题，首先需要对“明确的通用规则”下一个精确定义。普林斯顿大学的教授阿朗佐•丘奇（Alonzo Church）将其称为“有效可计算性”，而在1928年并不存在这样的定义。但在接下来的6-7年里，埃米尔•波斯特（Emil Post）拓展了他的定义，即一个工人按照一张指令表从一个房间移动到另一个房间书写和擦除标记（1936），邱奇和他的两个学生斯蒂芬•克莱恩（Stephen Kleene）和（j.B. Rosser）利用邱奇的λ微积分和哥德尔的递归理论也是如此。丘奇的论文(发表于1936年4月15日)表明，决策问题确实是“无法决策的” ，比图灵早了将近一年(图灵的论文1936年5月28日提交，1937年1月发表)。与此同时，波斯特在1936年秋天提交了一篇短文，所以图灵至少比波斯特更有优先权。当丘奇评审图灵的论文时，图灵有时间研究丘奇的论文，并在附录中添加了一个草图，证明邱奇的λ微积分和他的机器可以计算同样的函数。

{{quote|But what Church had done was something rather different, and in a certain sense weaker. ... the Turing construction was more direct, and provided an argument from first principles, closing the gap in Church's demonstration.|Hodges p. 112}}

{{quote|But what Church had done was something rather different, and in a certain sense weaker. ... the Turing construction was more direct, and provided an argument from first principles, closing the gap in Church's demonstration.|Hodges p. 112}}

但Church所做的是完全不同的事情，而且在某种意义上是较弱的。......Turing的构造更直接，并提供了最初原则的论据，从而弥补了 Church证明中的空白。

{{quote|但邱奇所做的是完全不同的事情，而且在某种意义上是较差的。......图灵的构造更直接，并提供了最初原则的论据，从而弥补了邱奇证明中的空白。

—Hodges，第112页

—Hodges，第112页}}

And Post had only proposed a definition of [[Church–Turing thesis|calculability]] and criticized Church's "definition", but had proved nothing.

And Post had only proposed a definition of [[Church–Turing thesis|calculability]] and criticized Church's "definition", but had proved nothing.

Post只是提出了一个可计算性的定义，并批评了Church的“定义” ，但没有证明任何事情。

波斯特只是提出了一个可计算性的定义，并批评了邱奇的“定义” ，但没有证明任何事情。

===Alan Turing's a-machine===

===阿兰图灵的机器===

In the spring of 1935, Turing as a young Master's student at [[King's College Cambridge]], [[UK]], took on the challenge; he had been stimulated by the lectures of the logician [[M. H. A. Newman]] "and learned from them of Gödel's work and the Entscheidungsproblem ... Newman used the word 'mechanical' ... In his obituary of Turing 1955 Newman writes:

In the spring of 1935, Turing as a young Master's student at [[King's College Cambridge]], [[UK]], took on the challenge; he had been stimulated by the lectures of the logician [[M. H. A. Newman]] "and learned from them of Gödel's work and the Entscheidungsproblem ... Newman used the word 'mechanical' ... In his obituary of Turing 1955 Newman writes:

Gandy states that:

Gandy states that:

甘迪表示:

Gandy表示:

{{quote|I suppose, but do not know, that Turing, right from the start of his work, had as his goal a proof of the undecidability of the Entscheidungsproblem. He told me that the 'main idea' of the paper came to him when he was lying in Grantchester meadows in the summer of 1935. The 'main idea' might have either been his analysis of computation or his realization that there was a universal machine, and so a [[Cantor's diagonal argument|diagonal argument]] to prove unsolvability.|''ibid.'', p. 76}}

{{quote|I suppose, but do not know, that Turing, right from the start of his work, had as his goal a proof of the undecidability of the Entscheidungsproblem. He told me that the 'main idea' of the paper came to him when he was lying in Grantchester meadows in the summer of 1935. The 'main idea' might have either been his analysis of computation or his realization that there was a universal machine, and so a [[Cantor's diagonal argument|diagonal argument]] to prove unsolvability.|''ibid.'', p. 76}}

我想，但我不知道，图灵，从他的工作开始，就把证明判定问题的不可判定性作为他的目标。他告诉我，1935年夏天，当他躺在格兰切斯特草地的时候，他想到了这篇论文的'主要想法'。这个 "主要想法 "可能是他对计算的分析，也可能是他意识到有一个普遍的机器，因此有一个对角线论证来证明不可解性。

{{quote|我想，但我不知道，图灵从他工作的一开始，就把证明决策问题的不可解性作为他的目标。1935年夏天，他告诉我，当他躺在格兰切斯特草地的时候，他完成了这篇论文的构想。这个 "构想"可能是他对计算的分析，也可能是他意识到有一个普遍的机器，因此有一个对角线论证来证明不可解性。

- 同上，第76页

- 同上，第76页 }}

While Gandy believed that Newman's statement above is "misleading", this opinion is not shared by all. Turing had a lifelong interest in machines: "Alan had dreamt of inventing typewriters as a boy; [his mother] Mrs. Turing had a typewriter; and he could well have begun by asking himself what was meant by calling a typewriter 'mechanical'" (Hodges p. 96). While at Princeton pursuing his PhD, Turing built a Boolean-logic multiplier (see below). His PhD thesis, titled "[[Systems of Logic Based on Ordinals]]", contains the following definition of "a computable function":

While Gandy believed that Newman's statement above is "misleading", this opinion is not shared by all. Turing had a lifelong interest in machines: "Alan had dreamt of inventing typewriters as a boy; [his mother] Mrs. Turing had a typewriter; and he could well have begun by asking himself what was meant by calling a typewriter 'mechanical'" (Hodges p. 96). While at Princeton pursuing his PhD, Turing built a Boolean-logic multiplier (see below). His PhD thesis, titled "[[Systems of Logic Based on Ordinals]]", contains the following definition of "a computable function":

虽然Gandy认为Newman的上述言论有“误导性” ，但并非所有人都赞同这一观点。Turing一生都对机器有着浓厚的兴趣: “Alan从小就梦想发明打字机; (他的母亲)图灵夫人有一台打字机; 他很可能一开始就问自己，把打字机称为'机械的'是什么意思"（Hodges p.96）。在普林斯顿攻读博士学位时，图灵制造了一个布尔逻辑乘法器（见下文）。他的博士论文题为 "基于序数的逻辑系统"，包含了 "可计算函数 "的如下定义。

尽管Gandy认为Newman的上述言论有“误导性” ，但这一观点并不为所有人所认同。图灵一生都对机器有着浓厚的兴趣: “阿兰（图灵）从小就梦想发明打字机; (他的母亲)图灵夫人有一台打字机; 他很可能一开始就问自己，把打字机称为'机械的'是什么意思"（Hodges p.96）。在普林斯顿攻读博士学位时，图灵制造了一个布尔逻辑乘法器（见下文）。他的博士论文题为 "基于序数的逻辑系统"，包含了 "可计算函数 "的定义:

{{quote|It was stated above that 'a function is effectively calculable if its values can be found by some purely mechanical process'. We may take this statement literally, understanding by a purely mechanical process one which could be carried out by a machine. It is possible to give a mathematical description, in a certain normal form, of the structures of these machines. The development of these ideas leads to the author's definition of a computable function, and to an identification of computability with effective calculability. It is not difficult, though somewhat laborious, to prove that these three definitions [the 3rd is the λ-calculus] are equivalent.|Turing (1939) in ''The Undecidable'', p. 160}}

{{quote|It was stated above that 'a function is effectively calculable if its values can be found by some purely mechanical process'. We may take this statement literally, understanding by a purely mechanical process one which could be carried out by a machine. It is possible to give a mathematical description, in a certain normal form, of the structures of these machines. The development of these ideas leads to the author's definition of a computable function, and to an identification of computability with effective calculability. It is not difficult, though somewhat laborious, to prove that these three definitions [the 3rd is the λ-calculus] are equivalent.|Turing (1939) in ''The Undecidable'', p. 160}}

上面说过，"如果一个函数的值可以通过某种纯粹的机械过程找到，那么这个函数就是有效的可计算函数"。我们可以从字面上理解这句话，将纯机械过程理解为可以由机器完成的过程。可以用一定的正常形式对这些机器的结构进行数学描述。这些思想的发展导致了作者对可计算函数的定义，以及对具有有效可计算性的计算认同。要证明这三个定义第3个是λ可计算性是等价的并不困难，虽然有些费力。

{{quote|上面说过，"如果一个函数的值可以通过某种纯粹的机械过程找到，那么它就是有效的可计算的"。我们可以从字面上理解这句话，用纯粹的机械过程来理解可以由机器来完成的过程。我们有可能以某种正常形式对这些机器的结构进行数学描述。这些想法的发展导致了作者对可计算函数的定义，以及对可计算性与有效可计算性的认同。要证明这三个定义（第三个是λ-微积分）是等价的并不困难，虽然有些麻烦。

- 图灵(1939)在The Undecidable一书中，第160页。

- 图灵(1939)在The Undecidable一书中，第160页。}}

When Turing returned to the UK he ultimately became jointly responsible for breaking the German secret codes created by encryption machines called "The Enigma"; he also became involved in the design of the ACE ([[Automatic Computing Engine]]), "[Turing's] ACE proposal was effectively self-contained, and its roots lay not in the [[EDVAC]] [the USA's initiative], but in his own universal machine" (Hodges p. 318). Arguments still continue concerning the origin and nature of what has been named by Kleene (1952) [[Turing's Thesis]]. But what Turing ''did prove'' with his computational-machine model appears in his paper "[[On Computable Numbers, with an Application to the Entscheidungsproblem]]" (1937):

When Turing returned to the UK he ultimately became jointly responsible for breaking the German secret codes created by encryption machines called "The Enigma"; he also became involved in the design of the ACE ([[Automatic Computing Engine]]), "[Turing's] ACE proposal was effectively self-contained, and its roots lay not in the [[EDVAC]] [the USA's initiative], but in his own universal machine" (Hodges p. 318). Arguments still continue concerning the origin and nature of what has been named by Kleene (1952) [[Turing's Thesis]]. But what Turing ''did prove'' with his computational-machine model appears in his paper "[[On Computable Numbers, with an Application to the Entscheidungsproblem]]" (1937):

When Turing returned to the UK he ultimately became jointly responsible for breaking the German secret codes created by encryption machines called "The Enigma"; he also became involved in the design of the ACE (Automatic Computing Engine), "[Turing's] ACE proposal was effectively self-contained, and its roots lay not in the EDVAC [the USA's initiative], but in his own universal machine" (Hodges p. 318). Arguments still continue concerning the origin and nature of what has been named by Kleene (1952) Turing's Thesis. But what Turing did prove with his computational-machine model appears in his paper "On Computable Numbers, with an Application to the Entscheidungsproblem" (1937):

当图灵回到英国后，他负责破解名为“英格玛”的加密机创造的德国密码；他还参与了ACE（自动计算引擎）的设计。“图灵的ACE建议实际上是自成一体的，其根源不在于EDVAC（美国的倡议），而在于他自己的通用机器"（Hodges p.318）。关于被Kleene（1952年）命名为 "图灵论文 "的起源和性质的争论仍在继续。但是，图灵用他的计算机模型所证明的东西出现在他的论文中"On Computable Numbers, with an Application to the Entscheidungsproblem"。

{{quote|[that] the Hilbert Entscheidungsproblem can have no solution ... I propose, therefore to show that there can be no general process for determining whether a given formula U of the functional calculus K is provable, i.e. that there can be no machine which, supplied with any one U of these formulae, will eventually say whether U is provable.|from Turing's paper as reprinted in ''The Undecidable'', p. 145}}

{{quote|[that] the Hilbert Entscheidungsproblem can have no solution ... I propose, therefore to show that there can be no general process for determining whether a given formula U of the functional calculus K is provable, i.e. that there can be no machine which, supplied with any one U of these formulae, will eventually say whether U is provable.|from Turing's paper as reprinted in ''The Undecidable'', p. 145}}

希尔伯特-判定问题不可能有解......。因此我建议，不可能有一个一般的过程来确定函数微积分K的一个给定公式U是否可证明，也就是说，不可能有一台机器在提供任何一个公式U的情况下，最终会说出U是否可证明。

{{quote|希尔伯特-决策问题不可能有解......。因此我建议，不可能有一个一般的过程来确定函数微积分K的一个给定公式U是否可证明，也就是说，不可能有一台机器在提供任何一个公式U的情况下，最终会说出U是否可证明。

- 摘自Turing的论文，详见The Undecidable，第145页。

- 摘自图灵的论文，详见The Undecidable，第145页。}}

Turing's example (his second proof): If one is to ask for a general procedure to tell us: "Does this machine ever print 0", the question is "undecidable".

Turing's example (his second proof): If one is to ask for a general procedure to tell us: "Does this machine ever print 0", the question is "undecidable".

Turing的例子(他的第二个证明):如果有人要求用一般程序来告诉我们:“这台机器是否曾经打印过0”，这个问题就是“无法确定的”。

图灵的例子(他的第二个证明):如果有人要求用一般程序来告诉我们:“这台机器是否曾经打印过0”，这个问题就是“无法确定的”。

===1937–1970: The "digital computer", the birth of "computer science"==

===1937–1970: The "digital computer", the birth of "computer science"==