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.
但图灵的模型更加直接地弥补了丘奇的缺陷。