1936年，丘奇在《美国数学杂志》(American Journal of Mathematics）上发表了题为“初等数论中的不可解问题”（An unsolvable problem of elementary number theory）的论文，否定性回答了Hilbert的判定问题（Entscheidungsproblem）：不存在通用算法判定给定的λ表达式的可定义性。

图灵很快就证明了图灵机的可计算性的概念与λ表达式的可定义性是等价的，并将此证明题为“可计算性和能行可计算性”，作为附录放在他1936年的论文“论可计算数及其在判定问题上的应用”（On Computability Numbers, with an Application to the Entscheidungsproblem）中。

***

附录

可计算性和能行可计算性 - 图灵

所有能行可计算（λ可定义）序列都是可计算的定理及其逆定理在下面简要证明。假设人们已经了解丘奇（Church）和克莱尼（Kleene）使用的术语“合式公式”（W.F.F.）和“转换（conv）”。在第二个证明中，假设存在几个公式，无需证明，这些公式可以参考克莱尼在“形式逻辑的正整数理论”中的结果直接构造（《美国数学杂志》，57（1935），153-173，219-244）。

表示整数 n 的 W.F.F. 将用 Nn 表示。我们说，第n位数字是φγ(n) 的序列γ是λ可定义的或能行可计算的，如果 1+ φγ(u)是n的 λ可定义函数，即如果存在 W.F.F. Mγ，使得对于所有整数 n，

{Mγ}(Nn) conv Nφγ(n)+1

即根据 λ 的第n位数字是 1 或 0, {Mγ} (Nn)可以转换为 λxy.x(x(y)) 或 λxy.x(y)。

为了证明每个 λ 可定义序列 γ 都是可计算的，我们必须说明如何构造一台机器来计算 γ。为了便于使用机器，只需对转换演算进行简单的修改即可。这种修改包括使用 x、x'、x" ... 作为变量，而不使用 a、b、c、...。我们现在构造一个机器 L，当提供公式 Mγ 时，它可以写下序列 γ。L 的构造与机器 K 的构造有些相似，后者可以证明函数演算的所有可证明公式。我们首先构造一个选择机器 L1，如果为其提供 W.F.F.，比如M，并对其进行适当操作，它就会获得任何M可以转换的公式。然后可以修改 L1 以产生一个自动机器 L2，它依次获得 M 可以转换到的所有公式（参见第 252 页）。机器 L包括L2作为一部分。当提供公式 Mγ 时，机器 L 的运动被分为几个部分，其中第n部分用于查找 γ 的第n位数字。这第n部分的第一阶段是 {Mγ} {Nn) 的形成。然后，该公式被提供给机器 L2，它将其依次转换为各种其他公式。每一个可转换的公式都会最终出现，并与下列公式进行比较：

λx[λx’[{x}({x}(x’))]], i.e. N2

和

λx[λx’[{x}(x’)]], i.e. N1

如果与第一个相同，则机器打印数字 1，第n部分完成。如果与第二个相同，则打印 0，该部分完成。如果与两者不同，则恢复 L2 的工作。根据假设，{My}(Nn) 可转换为公式 N2或 N1之一；因此，第n部分最终将完成，即γ的第n位数字最终将被写下来。

为了证明每个可计算序列γ都是 λ 可定义的，我们必须展示如何找到一个公式Mγ，使得对于所有整数 n，

{Mγ}(Nn) conv N1+φγ(n)

令 M 是一台计算 γ 的机器，我们用数字来描述M的完全格局，例如，我们可以取 §6 中描述的完全格局的描述数（D.N）。令 ξ(n) 是M第n个完全格局的描述数。机器M的表格给出了ξ(n+1)和ξ(n)之间的关系如下：

ξ(n+1) = ργ(ξ(n)),

其中 ργ 是一个形式严格受限的函数，尽管通常不是很简单：它由 M的表格确定，py 是λ可定义的（我省略了对此的证明），即存在一个 W.F.F. Aγ 使得对于所有整数 n，

{Aγ}(Nξ(n)) conv Nξ(n+1)

令U 代表

λu[{{u}(Aγ)}(Nr)], 

其中 r=ξ(0)；然后，对于所有整数 n，

{Uγ}(Nn) conv Nξ(n).

可以证明，存在一个公式 V，使得

{{V}(Nξ(n+1))}Nξ(n)

- conv N1，如果从第 n 个到第 (n+1) 个完全格局，打印的是数字 0。

- conv N2，如果打印的是数字 1。

- conv N3，否则。

令 Wγ 代表

λu[{V}({Aγ}({Uγ}(u)))}({Uγ}(u))], 

因此，对于每个整数 n，

{{V}(Nξ(n+1))} (Nξ(n) conv {Wγ}(Nn),

令 Q 为公式，

{{Q}(Wγ)}(Ns) conv Nr(s),

其中 r(s) 是第 s 个整数 q，对于该整数，{Wγ} (Nq) 可以转换为 N1 或 N2。然后，如果 Mγ 代表

λw[{Wγ}({Q}({Wγ}}(w))],

它将具有所需的属性。

原文：

https://www.cs.virginia.edu/~robins/Turing_Paper_1936.pdf

Computability and effective calculability

The theorem that all effectively calculable (λ-definable) sequences are computable and its converse are proved below in outline. It is assumed, that the terms "well-formed formula " (W.F.F.) and "conversion " as used by Church and Kleene are understood. In the second of these proofs the existence of several formulae is assumed without proof; these formulae may be constructed straightforwardly with the help of, e.g., the results of Kleene in "A theory of positive integers in formal logic'", American Journal of Math., 57 (1935), 153-173, 219-244.

The W.F.F. representing an integer n will be denoted by Nn. We shall say that a sequence γ whose n-th figure is φγ(n) is λ-definable or effectively calculable if 1+ φγ(u) is a λ-definable function of n, i.e. if there is a W.F.F. Mγ such that, for all integers n,

{Mγ}(Nu) conv N φγ(n)+1

i.e. {Mγ} (Nn) is convertible into λxy.x(x(y)) or into λxy.x(y) according as the n-th figure of λ is 1or 0.

λxy.x(x(y)) or λxy.x(y)。

To show that every λ-definable sequence γ is computable, we have to show how to construct a machine to compute γ. For use with machines it is convenient to make a trivial modification in the calculus of conversion. This alteration consists in using x, x', x", ... as variables instead of a, b, c, .... We now construct a machine L which, when supplied with the formula Mγ, writes down the sequence γ. The construction of L is somewhat similar to that of the machine K which proves all provable formulae of the functional calculus. We first construct a choice machine L1 which, if supplied with a W.F.F., M say, and suitably manipulated, obtains any formula into which M is convertible. L1 can then be modified so as to yield an automatic machine L2 which obtains successively all the formulae into which M is convertible (cf. foot-note p. 252). The machine L includes L2 as a part. The motion of the machine L when supplied with the formula Mγ is divided into sections of which the n-th. is devoted to finding the n-th figure of γ. The first stage in this n-th. section is the formation of {Mγ} {Nn). This formula is then supplied to the machine L2, which converts it successively into various other formulae. Each formula into which it is convertible eventually appears, and each, as it is found, is compared with

λx[λx’[{x}({x}(x’))]], i.e. N2

And with

λx[λx’[{x}(x’)]], i.e. N1

If it is identical with the first of these, then the machine prints the figure 1 and the n-th section is finished. If it is identical with the second, then 0 is printed and the section is finished. If it is different from both, then the work of L2 is resumed. By hypothesis, {Mγ}(Nn) is convertible into one of the formulae N2 or N1; consequently the n-th section will eventually be finished, i.e. the n-th. figure of γ will eventually be written down.

To prove that every computable sequence γ is λ-definable, we must show how to find a formula M such that, for all integers n,

{Mγ}(Nn) conv N1+φγ(n).

Let M be a machine which computes γ and let us take some description of the complete configurations of M by means of numbers, e.g. we may take the D.N of the complete configuration as described in §6. Let ξ(n) be the D.N of the n-th complete configuration of M. The table for the machine M gives us a relation between ξ(n+1) and ξ(n) of the form

ξ(n+1) = ργ(ξ(n)),

where ργ is a function of very restricted, although not usually very simple, form : it is determined by the table for M, py is λ-defmable (I omit the proof of this), i.e. there is a W.F.F. Aγ such that, for all integers n,

{Aγ}(Nξ(n)) conv Nξ(n+1)

Let U stand for

λu[{{u}(Aγ)}(Nr)], 

where r=ξ(0); then, for all integers n,

{Uγ}(Nn) conv Nξ(n).

It may be proved that there is a formula V such that

{{V}(Nξ(n+1))}Nξ(n)

- conv N1, if, in going from the n-th to the (n+1)-th complete configuration, the figure 0 is printed.

- conv N2, if the figure 1 is printed.

- conv N3, otherwise

Let Wγ stand for

λu[{V}({Aγ}({Uγ}(u)))}({Uγ}(u))], 

so that, for each integer n,

{{V}(Nξ(n+1))} (Nξ(n)) conv {Wγ}(Nn),

and let Q be a formula such that

{{Q}(Wγ)}(Ns) conv Nr(s),

where r(s) is the s-th integer q for which {Wγ} (Nq) is convertible into either N1 or N2. Then, if Mγ stands for

λw[{Wγ}({Q}({Wγ}}(w))],

it will have the required property.