雙語暢銷書《艾倫圖靈傳》第4章:彼岸新星(3)
Then Church's paper arrived from across the Atlantic.
It pre-empted the result, and threw into jeopardy the publication of Alan's work, scientific papers not being allowed to repeat or copy one another.
它先發制人，給艾倫的成果帶來了危險，因爲學術論文是不允許重複的。But what Church had done was something rather different, and in a certain sense weaker.
不過，丘奇的成果有些不同，某種程度上說，他不如艾倫。
He had developed a formalism called the 'lambda-calculus' and, with the logician Stephen Kleene, had discovered that this formalism could be used to translate all the formulae of arithmetic into a standard form.
丘奇提出了一個叫作"λ算子"的模型注，邏輯學斯蒂芬·克林發現，這個模型可以將所有的算術公式變形爲標準形式。In this form, proving theorems was a matter of converting one string of symbols of the lambda-calculus into another string, according to certain rather simple rules.
在這個模型中，"證明"就是按照某個基本的規則，把一個λ表達式轉化成另一個。Church had then been able to show that the problem of deciding whether one string could be converted into another string was unsolvable, in the sense that there existed no formula of the lambda-calculus which could do it.
然後丘奇能夠證明，不存在一個λ算子，能夠判斷一個表達式是否能夠轉化成另一個。Having found one such unsolvable problem, it had become possible to show that the exact question that Hilbert had posed must also be unsolvable.
找到這麼一個無法解決的問題，就能證明，希爾伯特提出的判定性問題一定是無解的。But it was not obvious that 'a formula of the lambda-calculus' corresponded to the notion of a 'definite method'.
但是，"λ算子"並不是顯著的"機械的過程"。Church gave verbal arguments for the assertion that any 'effective' method of calculation could be represented by a formula of the lambda-calculus.
丘奇給出了一個說明，任何有效的計算過程都可以用λ算子表示。But the Turing construction was more direct, and provided an argument from first principles, closing the gap in Church's demonstration.
但圖靈的模型更加直接地彌補了丘奇的缺陷。
