在1983年或是1984年，阿隆佐•邱奇大概80岁时，他被邀请到斯坦福大学的语言和信息研究中心做报告，并参观了中心的Xerox Dandelion计算机。计算机运行的是LISP语言，这是由约翰•麦卡锡（1927—2011）发明的一种编程语言。邱奇被告知，LISP是基于他50多年前发明的λ演算发展而来的。
邱奇坦言他对计算机一无所知，但他的一个学生了解计算机。1当然，那时所有人都已经知道阿兰•图灵是谁了。
1 Maria Manzano，“Alonzo Church: His Life，His Work and Some of His Miracles”，History and Philosophy of Logic，Vol. 18（1997），212。
λ演算是阿隆佐•邱奇在20世纪30年代早期为证明一阶谓词逻辑没有通用判定过程而发明的。图灵在发表关于可计算数和判定性问题的论文之前就对此有所了解了。为此，他在论文中增加了一个附录，用来说明他的方法与邱奇的方法在本质上是等价的，这一附录就是本章的主题。
如果说对λ演算的理念觉得很熟悉，那是因为它们对编程语言的发展影响深远。相当早的时候，人们就发现λ演算与划分为过程式或命令式的编程语言之间存在着结构关系，例如早期的编程语言ALGOL2，基于这个语言发展出了Pascal和C，同样在C基础上发展出了 C++、Java和C#。用过程式语言编写的程序，其结构围绕着将数据传递给过程（也称为子程序或方法）的理念来组织，过程以各种各样的方式对数据进行处理。
2 P. J. Landin，“A Correspondence Between ALGOL 60 and Church's Lambda-Notation”，Communications of the ACM，Vol. 8，No.2（Feb 1965），89-101，Vol. 8，No. 3（Mar 1965），158-165。
λ演算对LISP、APL、Haskell、Scheme和F#等函数式编程语言有着更直接的影响。在函数式语言中，函数的排列方式更像是链条，后一个函数从前一个函数获得输出。函数式语言通常允许像过程式语言操作数据那样来操作函数。尽管函数式语言没有像过程式语言那样受到主流群体的欢迎，但是最近它们也展露了一些复兴的气息。
阿隆佐•邱奇1903年出生于华盛顿，他职业生涯的大部分时间是在普林斯顿大学度过的。他本科就读于普林斯顿，24岁时获得数学博士学位。在作为国家研究院院士工作两年后，他回到普林斯顿教学，从1929年一直到1967年退休。邱奇后来又在UCLA工作了一段时间，直到1990年。
邱奇是一个勤奋且一丝不苟的人，说话严谨，经常工作到深夜。他的课程经常开始于精心设计的仪式般的擦黑板，有时候还会借助一桶水。在处理数学问题时，他通常会用不同颜色的墨水。当需要更多颜色的时候，他就会按照不同比例混合那些标准颜色的墨水；当完成了一页并要保存起来时，他会用Duco涂满表面。Duco是一种漆，邱奇发现它非常适合保护纸张，因为它不会把纸弄皱。3
3 Herbert B. Enderton，“Alonzo Church: Life and Work”，introduction to Collected Works of Alonzo Church（MIT Press，forthcoming）引言，http://www.math.ucla.edu/~hbe/church.pdf。
邱奇指导过31篇博士论文，论文来自于斯蒂芬•克莱尼（1931）、约翰•巴克利•罗瑟（1934）、莱昂•亨金（1947）、马丁•戴维斯（1950）、哈特利•罗杰斯（1952）、雷蒙德•斯穆里安（1959）以及阿兰•图灵（1938）。4
4 Herbert B. Enderton, “In Memoriam: Alonzo Church, 1903–1995,” The Bulletin of Symbolic Logic, Vol. 1, No. 4 (1995), 486–488。
通常认为，邱奇建立了符号逻辑协会，因为他是《符号逻辑杂志》的第一位编辑。实际上，他并没有建立这个组织，而是指导杂志取得了辉煌的成功，最突出的是他编纂了重要的逻辑文献书目。
邱奇是在1927年至1929年作为国家研究院院士时开始λ演算的工作的。在那时，数学家们希望理解有效可计算性这个模糊的概念。为了知道数值计算的局限及能力，有必要用形式系统化的方式来定义函数，也就是说用符号、字符串和确定性规则来定义。最好的方法是什么呢？这种方法能否表明这些函数能够充分概括有效可计算性？
邱奇就这一方面的第一篇论文在1931年10月5日被《数学年鉴》收录，并在下一年的4月发表。5在这篇文章中，邱奇用了一个小写的 lambda（λ）来表示函数。
5 阿隆佐·邱奇，“A Set of Postulates for the Foundation of Logic”，The Annals of Mathematics，2nd Series，Vol. 33，No. 2（Apr.1932），346-366。
邱奇引入新记号的一个动机来自于传统函数表示的特定二义性。看看下面的表达式：
x2 + 5x + 7
就表达式本身而言，它在语法上是正确的，但我们仍不知道该对这个表达式做些什么，下面这个就清晰点了：
f (x) = x2 + 5 x + 7
这是传统的函数标记法，其中x是约束变量（或自变量）。我们可以按照自己的意愿任意改变约束变量，只要与函数表达式中的其他部分不冲突就行：
f (y) = y2 + 5 y + 7
我们可以使用表达式f(4)来表示函数的一个值，用4代替自变量x，并计算函数的值
f (4) = (4)2 + 5· (4) +7 = 43
当你意识到这一点时可能会吃惊，那就是没有标准的形式可以将函数表达式（也就是y 2+ 5 y + 7）与y的具体值一起表示出来。一旦我们用4替换了y，就丢失了自变量信息。如果你需要修复这样的缺点，并发展出一套表示取某个值的函数的方式，可能会想到这样的东西：
[ y2 + 5 y + 7] (4)
这其实不算太差，但是如果表达式中含有多个自变量呢？下面的表示就会让人不明就理：
[ y2 + 5 y +18 x - 2 xy + 7] (4)
即使你写成：
[ y2 + 5 y +18 x - 2 xy + 7] (4,5)
你假设对x和y按照特定顺序赋值。
在《数学原理》中，怀特海和罗素使用了抑扬符号来表示符合特定函数的类：ŷ。邱奇想把这个抑扬符号移到变量的前面，像^ y一样，但因为书写的原因，这个符号后来改成了lambda6：λy。
6 J. Barkley Rosser，“Highlights of the History of Lambda-Calculus”，Annals of the History of Computing，Vol. 6，No. 4（Oct.1984），337-349。
多年来，邱奇的表示法已经有了发展。在下面的讨论中，我使用图灵在其论文附录中使用的表示法。一元变量的函数用下面这个通用形式表示：
λx[ M]
其中M是包含自变量x的表达式。对于之前的例子，我们可以表示为：
λx[ x2 + 5 x + 7]
一个包含特定自变量值的函数可以写成这个通用形式：
{F}(A)
F是函数，如果F含有一个自变量，那么公式代表了函数，其中A代表函数中的自变量。例如，如果函数中的自变量为x，则通用形式为：
{λx[ M]}(A)
将M替换为之前的函数，就变成了：
{λx[ x2 + 5 x + 7]}(A)
若x的值为4，则可以将其写为：
{λx[ x2 + 5 x + 7]}(4)
现在，我们已经成功地将函数和某个自变量的值表示在一起了。
含有两个自变量的函数有如下一般形式：
{{F}(A)}(B)
为了方便且可读性强，它可以简写为：
{F}(A, B)
如果将F替换为一个真正的函数，它看起来会是：
{λx λy[ y2 + 5 y +18 x - 2 x y + 7]}(A, B)
我们现在知道A将替代x， B将替代y，它们以前面λ的排列顺序为准。
也可以再简写。如果没有歧义，可以去掉花括号，那么
{F}(A, B)
变成
F (A, B)
这看起来很像常规的函数表示法，但F表达式实际上包含了一些λ：
λx λy[ M] (A, B)
邱奇还允许将方括号替换为一个点，紧跟在λ串的后面：
λx λy. M( A, B)
这个形式会在接下来的大多数lambda表达式中出现。
邱奇在建立了基本的lambda表示法后，引入了常用逻辑算子的表达式和用于转换为等价公式的替换规则。邱奇以形式化方式定义了这些变换的规则，也可归结为：
Ⅰ. 如果新的自变量不与公式中的其他部分冲突，可以改变某个自变量（例如，x换为y）；
Ⅱ. 在公式{λx. M}(N)中，如果N中不包含x的任何东西，那么可以将N替换到M中任何x出现的位置，这样公式就变成了用N替换原始的x所形成的M；
Ⅲ.Ⅱ的相反情况仍成立。
在第一篇lambda函数的论文发表一年半后，邱奇发表了第二篇论文7。他修正了其给出的假设，并强调：“整个系统的形式字符，使得从符号的本身意义进行抽象，以及将（形式逻辑的）定理证明看做是可以根据一套特定规则在纸上进行推导的游戏成为可能。”8这个理念很大程度上符合形式主义的传统。
7 邱奇，“A Set of Postulates for the Foundation of Logic（Second Paper）”，The Annals of Mathematics，2nd Series，Vol. 34，No. 4（Oct. 1933），839-864。
8 邱奇，842。
邱奇也引入了缩写conv来表示“通过转换”，指出利用规则Ⅰ、Ⅱ、Ⅲ可以将一个公式转换为等价形式，例如
λx [x2 + 5 x + 7] (A)conv A2 + 5 A + 7
邱奇第二篇论文的最后是对正整数的研究。他使用了lambda表示法来定义符号1、后继、加运算、乘运算以及5个皮亚诺公理，并且声明道：“我们的纲领是要在之前所描述内容的基础上建立一套关于正整数的理论，然后，通过已知的方法或是进行适当的改变，将该理论推广到有理数以及实数领域。”9
9 邱奇，864。
邱奇的学生斯蒂芬•科尔•克莱尼在约翰•巴克利•罗瑟（1907—1989）的帮助下继续下一步的研究。1934年，克莱尼所做的基础工作体现在“形式逻辑的例证”10一文中，并简化了多重lambda表示法。之前使用的
10 S. C. 克莱尼，“Proof by Cases in Formal Logic”，The Annals of Mathematics，2nd Series，Vol. 35，No. 3（July 1934），529-544。
λx λyM
现在可以使用
λxyM
来表示。
克莱尼于1935年改写并发表了他的博士论文“形式逻辑的正整数理论”，11该论文分为两部分。阅读这篇论文之前要先看邱奇的两篇论文以及克莱尼之前的论文，其第二部分也提及了即将发表的邱奇和罗瑟合作的论文。12
11 S. C. 克莱尼，“A Theory of Positive Integers in Formal Logic，Part I”，American Journal of Mathematics，Vol. 57，No. 1（Jan. 1935），153-173；Vol. 57，No. 2（Apr. 1935），219-244。
12 邱奇和罗瑟，“Some Properties of Conversion”，Transactions of the American Mathematical Society，Vol. 39，No. 3（May 1936），472-482。
尽管由邱奇、克莱尼、罗瑟一起发明的λ演算相当全面，既涉及逻辑又涉及算术，但是这里我只想集中探讨一些基本的算术，这样你就可以看到，如何通过单纯的字符运算来实现加法和乘法了。
定义自然数时，我们总是需要从0或1开始。邱奇和克莱尼是以1开始的，下面就是其符号：13
13 我将采用克莱尼的“A Theory of Positive Integers in Formal Logic, Part I”中前10页出现的定义。
1 → λfx.f (x)
这里箭头的意思是“代表”或“全称是”。这个公式看起来似乎有点怪，实际上可能看起来是非常怪，但这仅仅是一个定义，所以现在还没必要追究其意义。更冗长的版本是
1 → {λfx [f (x)]}/p>
因此，1实际上是一个含有两个自变量f和x的函数，非常唐突，定义一个数字居然需要额外多出的两个变量。
下面的是后继函数：
S → λρfx.f( ρ( f, x))
还是很奇怪吧，我也这么认为。尽管我们希望后继函数中包括自变量，但不希望其中包含3个自变量。
幸运的是，符号2可以定义成你期望的形式：
2 → S(1)
如果我们事实上想对1应用后继函数，就必须保证所有的自变量都是唯一的，因此要使用下面1的等价表达式：
1 → λab.a( b)
当使用λ表达式时，函数和变量经常互换角色。在下面变换后的公式的推导过程中，我选择性地使用花括号来标记将要在那一步被替换的包含一个自变量的函数。
函数S(1)也可以写为{S}1或者：
{λρfx.f( ρ( f, x))}(λab.a( b))
后继函数的第一个自变量为ρ，因此用1的表达式将函数中的ρ替换掉，λ后的ρ就消失了：
λfx.f(λab.a( b)(f, x))
现在这个公式包含另一个函数，该函数中含有两个参数：
λfx.f({λab.a( b)}(f, x))
用f替换a， x替换b：
λfx.f( f( x))
这样就完成了。
尽管1最初定义为：
1 → λfx.f( x)
数字2定义为：
2 → S(1)convλfx.f( f( x))
比较转换后的2和1的表达式，你会发觉在点的右侧多出一个f和一对括号。现在使用不同的变量λab.a( a( b))来表示2，并尝试确定下一个后继数{S}(2):
{λρfx.f( ρ( f, x))}(λab.a( a( b)))
同样，用2来替代ρ：
λfx.f({λab.a( a( b))}(f, x))
用f替换a， x替换b：
λfx.f( f( f( x)))
这是3的λ表达式。我猜你开始明白这个模式了，我们最想从正整数的抽象表达式中得到的是某种后继性。下面这个记号表明了这一后继性：每一个后继整数都会增加对第一个自变量的嵌套。
克莱尼定义“加”运算为：
+ → λρσfx.ρ( f, σ( f, x))
有点怀疑了吧？我们试着将2和3相加。首先我们需要使所有的自变量不同。我将使用λab.a( a( b))代表2，λcd.c( c( c( d)))代表3，因此{+}(2,3)就是：
{λρσfx.ρ( f, σ( f, x))}(λab.a( a( b)),λcd.c( c( c( d))))
在+函数中，用2的公式替换ρ，用3的公式替换σ：
λfx.λab.a( a( b))(f,{λcd.c( c( c( d)))}(f, x))
替换后的3是一个函数，其中用f替换c， x替换d：
λfx.{λab.a( a( b))}(f, f( f( f( x))))
现在替换后的2是一个用f替代a，用f( f( f( x)))替代b的函数：
λfx.f( f( f( f( f( x)))))
到这里，我们就完成了运算。答案与S( S( S( S(1))))一致，也就是5。
有意思的是，乘法函数比加法函数还要简单：
× → λρσx.ρ( σ( x))
我们来计算2和3的乘法，可以将{×}(2,3)写成：
{λρσx.ρ( σ( x))}(λab.a( a( b)),λcd.c( c( c( d))))
用2的公式替换ρ，3的公式替换σ：
λxλ ab.a( a( b))({λcd.c( c( c( d)))}(x))
现在3变成一个用x替代c的函数：
λx.{λab.a( a( b))}(λd.x( x( x( d))))
现在2变成一个函数，用右侧的表达式替换a：
λx.λb.λd.x( x( x( d)))({λd.x( x( x( d)))}(b))
在右侧的函数，用b替换d
λx.λb.{λd.x( x( x( d)))}(x( x( x( b))))
最后替换d：
λxb.x( x( x( x( x( x( b))))))
这就是6，当然也是2与3相乘的结果。
这些数字的函数定义可以让你做一些比较奇怪的事情，例如
{2}(3)
即：
{λab.a( a( b))}(λcd.c( c( c( d))))
在你完成了所有费力的替换后，最后会得到：
λbd.b( b( b( b( b( b( b( b( b( d)))))))))
也就是9，毫无意外，这就是3的二次方。这也就是为什么m的n次方定义为：
λmn.nm
在这个系统中，乘比加看起来要简单，指数形式是其中最简单的。当邱奇、克莱尼和罗瑟使用λ演算做实验时，他们发现λ表示法可以表示任何他们能想到的东西，这是后来称为λ可定义性的性质。“邱奇一直在推断，并最后明确地提出，λ可定义函数是所有的有效可计算函数。”14
14 克莱尼，“Origins of Recursive Function Theory”，Annals of the History of Computing，Vol. 3，No. 1（Jan 1981），59。
库尔特•哥德尔在1933年来到高级研究院。1934年春，他在普林斯顿讲授他的不完备性定理及递归函数，递归函数是从基本原始函数发展出来的。15让哥德尔对递归函数感兴趣的是雅克•赫尔布兰德（1908—1931）在1931年写给他的信，这位年轻聪明的法国数学家在攀登阿尔卑斯山时意外身亡了。
15 根据克莱尼和罗瑟的笔录，哥德尔的讲义早已在内部流传，但直到1965年才正式出版在马丁·戴维斯，ed.，The Undecidable（Raven Press，1965），41-71中。接着它们又被出版在库尔特·哥德尔，Selected Works: Volume I, Publications 1929-1936（Oxford University Press，1986），346-371。
尽管如此，哥德尔在那时仍然坚信，λ函数和递归函数都不足以包含所有我们认为的非正式有效可计算性。
1936年，邱奇发表了“初等数论的不可解问题”16，在这篇文章中首次出现了“λ可定义”一词。（之前，克莱尼在使用lambda记号表示逻辑和算术运算时仅仅使用了“可定义”或者“形式可定义”。）邱奇引用了自己之前的论文、克莱尼的两篇论文，以及克莱尼即将发表的探讨递归函数和λ可定义函数之间关系的论文。17与哥德尔构造了一个不可判定的命题一样，邱奇使用哥德尔的记数法同样构造了一个不可解的问题。
16 邱奇，“An Unsolvable Problem of Elementary Number Theory”，American Journal of Mathematics，Vol. 58，No.2（Apr. 1936），345-363。
17 克莱尼，“General Recursive Functions of Natural Numbers”，Mathematische Annalen，Vol. 112，No.1（Dec.1936），727-742，重印于马丁·戴维斯，ed.，The Undecidable（Raven Press，1965），237-252。S. C. 克莱尼，“λ-Definability and Recursiveness”，Duke Mathematical Journal，Volume 2，Number 2（1936），340-353。
在此基础上，邱奇在《符号逻辑期刊》（他自己也是该期刊的编辑）的首版上发表了两页的“判定性问题的笔记”，他在结论中写道：“判定性问题的通用情况是不可解的。”18这篇文章是在1936年4月15日被杂志接收的，比图灵在1936年5月28日提交到伦敦数学学会的文章早了6周。
18 邱奇，“A Note on the Entscheidungsproblem”，The Journal of Symbolic Logic，Vol. 1，No. 1（Mar. 1936），40-41。也可参见邱奇，“Correction to a Note on the Entscheidungsproblem”，The Journal of Symbolic Logic，Vol. 1，No. 3（Sep. 1936），101-102。
1936年夏，图灵可能花了大部分时间阅读我之前提到的邱奇和克莱尼的文章，学习λ演算，并验证它如何与自己的计算机器相关联。据显示，图灵的三页附录在8月28日被伦敦数学学会接收。图灵在最后写上了：“美国新泽西州普林斯顿大学研究生院。”他很期待自己的新家。直到9月23日，他才离开英国前往美国，在29日到达纽约。19
19 安德鲁·霍奇斯，Alan Turing: The Enigma（Simon & Schuster，1983），116。
1936年8月28日新增
附录
可计算性和有效可计算性
所有的有效可计算（λ可定义）序列都是可计算的，反之也成立。这个定理的证明将在下面简略给出。
在这里，“简略”的意思是证明中会跳过一些步骤。
假设人们已经理解了邱奇和克莱尼所使用的“合式公式”（W.F.F.）和“转换”这些术语。在第二个证明中，我们假定了一些公式已经存在，不再证明。这些公式可以参考克莱尼的论文“形式逻辑的正整数理论”[发表在《美国数学杂志》57（1935），153-173，219-244]直接构造。
图灵这里说的“第二个证明”是指上述定理的逆命题：每一个可计算序列同样也是λ可定义的。
表示一个整数n的W.F.F.将记为Nn。
我们开始使用克莱尼对1和后继数字的定义，但要使这些自变量与图灵后面使用的保持一致，N1是λxy.x( y)，N2是λxy.x( x( y))，Nn是λxy.x( x( x( x...(y)...)))。
如果1+φγ(u)是n的 λ可定义函数，我们就称第n个数字为φγ(n)的序列γ是 λ可定义的或者是有效可计算的。
φr两次出现时的参数都应该是n，而不是u，因此表达式应该是1+φγ(n)。可计算序列γ的第n位是0或者1，但邱奇和克莱尼定义的λ演算只考虑了正整数，并不包括0。φγ(n)并不是λ可定义的，因为0不是λ可定义的。所以，数字都加上1变成1和2。
如果存在W.F.F. Mγ，使得对于所有的整数n，
{Mγ}(Nn)conv Nφγ(n)+1
即根据λ的第n位数是1还是0，{Mγ}(Nn)可以转换为λxy.x( x( y))或者λxy.x( y)。
最后一行的λ其实是错的，应该是“γ的第n位数”。根据对应的数字是1还是0，值Nn（指序列中的数字位）处的函数Mγ可转换为λxy.x( x( y))（也就是2）或者λxy.x( y)（也就是1）。
例如，如果γ的第5位是1，那么φγ(5)是1，并且
{Mγ}(N5)conv Nφγ(5)+1
也就是说
{Mγ}(N5)conv N2
为了证明每一个λ可定义序列γ都是可计算的，我们必须首先构造一个可以计算γ的机器。使用机器，可以方便地在演算转换中进行简单的修改，这些修改包括使用x， x'，x''，...作为变量，而不是使用a， b， c，...。
图灵至今还未使用任何以a、 b或 c命名的变量，但他使用了x和 y。他希望所有的变量都具有统一的形式，因为接下来需要进行比较和匹配。这与第8节的要求很相似（本书第205页）：一阶谓词逻辑在被机器处理前需要“系统化”。
我们现在构造一台机器
，在提供了公式Mγ时可以写下序列γ。
在某种程度上很相似，
在图灵论文的第252页有5个脚注，图灵引用的是第二个（本书第205页）。在那里，他讨论了可以证明所有一阶逻辑的可证明公式的机器。考虑到λ表达式转换的系统化方式，这台机器看起来与之相似，很可能更加简单。
λx[λx'[{x}({x}(x'))]]，即N2，
及λx[λx'[{x}(x')]]，即N1。
这就是数字2和1的冗长的表达式。为了实现一个可以转换λ表达式的机器，你必须在表示法中保持一致，而不包含语法捷径的方法实际上是最简单的。
如果与第一个完全一样，那么机器打印1，第n部分完成。如果与第二个相同，那么打印0，这部分也结束了。如果与这两个都不一样，那么
在开始更加复杂的变换证明之前，图灵空了一行：如何设计一个能包括特定机器运转情况的λ表达式。
为了证明每一个可计算序列γ都是λ可定义的，我们必须先说明如何找到一个公式Mγ，对于所有的整数n，
{Mγ}(Nn)conv N1+φγ(n)
这个公式正好和之前那个一样，只是最后那个N的下标被重排了。现在，要做的不是描述一个操作λ函数的机器，而是定义一个模拟机器的λ函数。
假设
是一台计算γ的机器，我们来用数字描述一下
在下面的讨论中，我将会引用到“格局数”，这其实就是简单的连续整数0, 1, 2, 3等，这个数字随机器运转而递增。对于任何一个特定的机器，对每个格局数，存在一个与完全格局对应的描述数。这些是非常大的数字，包括了描述纸带上已打印数字及下一个m-格局的代码。
令ξ( n)为
图灵在这里使用的n是我所指的格局数，而ξ( n)是一个描述数。
从
ξ( n+1) = ργ(ξ( n))
其中ργ是一个严格受限的函数，尽管通常不是很简单：其形式由
ργ函数将一个描述数转换为下一个描述数。一般来讲，输入是一个长的数字，输出是另一个长的数字。这个函数基本上必须在这个长输入数中，寻找一组对应于m-格局和扫描符的特定模式的数字，并基于格局表构造下一个完全格局，有可能包含一个新的打印符号，并改变m-格局和下一个扫描符。
图灵对于这个函数的“通常不是很简单”的描述切中目标。这个函数需要将描述数拆分为单个数位并验证它们。因为描述数是十进制数，所以这个函数可以通过先将数字除以10的幂，忽略分数部分，再除以另一个10的幂，保留余数，来抽取其中任意长度的部分。尽管ργ函数毫无疑问是很复杂的，但它肯定是能被想到的。
ργ是λ可定义的（我略去了这部分的证明），即存在一个合式公式Aγ，对于所有的整数n：
{Aγ}(Nξ( n))conv Nξ( n+1)
Aγ本质上是与ργ一样的函数，只不过是用λ演算的语言表示的。它用来进行描述数间的转换。
令U表示
λu[{{u}(Aγ)}(Nr)]，
其中r= ξ(0)
这句开头的大写U应该有一个下标γ，因为它是基于一个特定可计算序列的。Nr是机器开始时的完全格局的描述数——数字313。这个数字对应于标准描述DAD，意思是m-格局q1（DA）和扫描一个空格（D）。变量u是格局数，随着机器运行依次是0、1、2等。包含u的是个花括号，通常意味着是个函数，虽然看起来似乎没什么意义，但很快你就将看到它很有效。
那么，对于所有的整数n，
{Uγ}(Nn)conv Nξ( n)
Uγ函数的参数是格局数（0，1，2等）。图灵认为，这个函数可以转换为那个格局的描述数。我们使用描述数4来验证一下，其中需要涉及转换表达式{Uγ}(N4)，即：
{λu[{{u}(Aγ)}(Nξ(0))]}(λxy.x( x( x( x( y)))))
在Uγ函数中，我使用了Nξ(0)而不是Nr，正因如此，我们不会忘记下标代表了描述数。用4的表达式替换函数中的u：
{{λxy.x( x( x( x( y))))}(Aγ)}(Nξ(0))
现在将x替换为Aγ：
{λy.Aγ( Aγ( Aγ( Aγ( y))))}(Nξ(0))
最后我们用Nξ(0)替换y：
Aγ(Aγ(Aγ(Aγ(Nξ(0)))))
Aγ在Nξ(0)上第一个应用的结果是Nξ(1)，下一次得到Nξ(2)，等等，因此最后的结果就是Nξ(4)，这和图灵预想的一样。现在，你就可以看出为什么将u定义为Uγ中的函数是有意义的了：它可以在根本上将出现在Aγ函数中的u混合嵌套。
可以证明，对于公式V，有
函数V基本上分析了连续两个完全格局的描述数，并确定打印0或者1，或者什么都不打印，这又是一个复杂但可以想到的函数。
令Wγ表示
λu[{{V}({Aγ}({Uγ}(u)))}({Uγ}(u))]，
因此，对于任意一个整数n，
{{V}(Nξ( n+1))}(Nξ( n))conv{Wγ}(Nn)，
这个命题左侧的公式可以转换为N1、N2或 N3中的一个。描述这种变换比较容易，可以先描述转换后的结果：
{Wγ}(Nn)
将Wγ替换为图灵刚刚给出的那个表达式
{λu[{V}({Aγ}({Uγ}(u)))}({Uγ}(u)]}(Nn)
用Nn代替u：
{{V}({Aγ}({Uγ}(Nn)))}({Uγ}(Nn))
表达式{Uγ}(Nn)可以转换为Nξ( n)，因此：
{{V}({Aγ}(Nξ( n)))}(Nξ( n))
表达式{Aγ}(Nξ( n))可以转换为Nξ( n+1)，这正是我们所求的：
{{V}({Nξ( n+1))}(Nξ( n))
通过这个简短的证明，我们可以知道{Wγ}(Nn)可以转换为N1、N2或 N3，这取决于第n个完全格局转换为第n+1个时打印的是0还是1，或是什么都不打印。
令Q是一个公式，使得
{{Q}(Wγ)}(Ns)conv Nr( z)，
其中r( s)是第s个整数q，其中{Wγ}(Nq)转换为N1或N2。
在上面的公式中，最后一个N的下标明显应该是r( s)而不是r( z)。只有一部分的完全格局才会打印0或者1，函数r( s)就是用来揭示这些完全格局的。例如，如果在1、4、6、7等完全格局中打印了0或者1，那么r(1)返回1，r(2)返回4，r(3)返回6，r(4)返回7，等等。
如果Mγ表示
λw[{Wγ}({{Q}(Wγ)}(w))]，
那么它将具备所需要的性质。†
† 在可计算序列的λ可定义性的完整证明中，最好改变这个方法，用我们的机器能够很好处理的描述代替完全格局的数字描述。我们选择某些整数来代表这些符号和机器的m-格局。假设在特定的完全格局中，那些代表纸带上后续符号的数字是S1S2...Sn，其中第m个符号被扫描到，m-格局的标号为t，那么我们可以用下面的公式表示这个完全格局
[[NS1,NS2,...NSm-1],[Nt,NSm],[NSm+1,...,NSn]]，
其中
[a, b]代表λu[{{u}(a)}(b)]
[a, b, c]代表λu[{{{u}(a)}(b)}(c)]，
等等。
在图灵证明的第二部分，他开始自己寻找公式Mγ，使得对于所有n，
{Mγ}(Nn)conv N1+φγ(n)
这个公式告诉我们序列的第n位是0还是1。我们先来分析：
{Mγ}(Nn)
用图灵刚刚为Mγ推导出的公式代替之：
{λw[{Wγ}({{Q}(Wγ))}(w))]}(Nn)
用Nn替代w：
{Wγ}({{Q}(Wγ))}(Nn))
括号中的表达式可以转换为Nr( n)，因此
{Wγ}(Nr( n))
已经表明，这个公式可以转换为N1、N2或N3，这主要取决于完全格局r( n)打印的是0或1或其他。然而，r( n)定义了只有在完全格局打印了0和1的情况下才返回。
上面的脚注表明，完全格局在纸带上被分为了下一个扫描符之前部分及下一个扫描符之后部分。图灵所建议的用来表示纸带这些部分的λ表达式可以是非常长，并且大小会随着完全格局的增长而增长。
下面是论文的结尾。
研究生院，
普林斯顿大学，
美国新泽西州。
对于更加严格的证明，图灵并没有遵循他在这里概述的证明逆命题的思路。论文“可计算性和λ可定义性”于1937年9月11日被《符号逻辑杂志》收录，这时距他抵达普林斯顿还不到一年的时间。20文章开始写道：
我们已经给出了许多定义用来表述与“有效计算性”的直观思路相对应的确切含义，并将其应用到了正整数函数中。这篇论文的意图是为了表明作者所介绍的可计算函数与邱奇发明的λ可定义的函数，以及与由赫尔布兰德和哥德尔引入并由克莱尼发展的一般递归函数是一致的。（在本论文中）已表明，任意的λ可定义函数都是可计算的，并且每一个可计算函数是一般递归函数。
20 阿兰·图灵，“Computability and λ-Definability”，The Journal of Symbolic Logic，Vol. 2，No. 4（Dec. 1937），pp.153-163。
图灵首先通过给出一台图灵机来证明λ可定义函数是可计算的。这台图灵机可能比图灵的通用机更复杂，它可以解析和转换λ函数。
证明的第二部分展示了可计算函数是递归的。图灵并不需要证明可计算函数是λ可定义的，因为斯蒂芬•克莱尼已经证明了递归函数是λ可定义的（在“λ可定义性和递归”一文中）。这样，有效计算性的三个定义被等价地联系起来了。
图灵后来经常提到他1935年夏躺在格兰切斯特庄园草地上时构想出来的这些神奇的虚拟机器，但是在他后续发表的论文中并没有给出机器的实际格局表。当他在邱奇的指导下写博士论文时，21论文内容已经完全与递归函数和λ函数相关了。
21 阿兰·图灵，“Systems of Logic Based on Ordinals”，Proceedings of the London Mathematical Society，2nd Series，Vol. 45，No.1（1939），161-228。