函数——是横跨数学、逻辑和计算的最基础概念，也是从逻辑走向计算的基本工具。想象一下，如果一个逻辑系统不再以命题、谓词、量词、变量为基本单位而把函数作为唯一的原生元素会是什么样？——其结果就是组合子逻辑和λ演算。

组合子逻辑和λ演算属于数理逻辑中的形式系统，本质上是以函数为基本元素的高阶逻辑。

在这个意义上，如果要想真正搞懂它们的基本思想而不仅仅是编程等实用目的，就必须从一阶逻辑开始，而要真正透彻理解如何从一阶逻辑走到组合子逻辑、λ演算，就需要了解这两门学科产生的背景和动机，来龙去脉和前世今生。

1 组合子逻辑简介

组合子逻辑（Combinatory Logic）又称作组合子理论（Theory of Combinator）学界简称为CL，是一个以函数为基本元素、以【应用】（application）作为基本运算连接函数和函数参数。在组合子逻辑中，所有的元素，包括基本元素和复合元素通通称作【项】(term），项与项之间的连接规则，就是【应用】。而“应用”的规则，则是以两个原生定义的“运算符”：S和K，这就像传统一阶逻辑定义的∧、∨、~、→、⇋5大运算符一样。那S和K表示什么意思，为什么要用两个大写字母表示运算符呢？这里面当然有很大的任意性，没有什么非这样做的理性理由。我们知道现在所有科技论文的标准语言是英语，而原因想必大家都知道，这里不再探讨。而在二战之前，基于同样的理由，特别是在数学、逻辑、哲学方面的论文，除了美国，大部分都是德语的，因此数学、逻辑中的许多符号都和德语有关。例如表示整数集合的Z，就来自德语Zahl（对我来说更像是来自汉语：zhengshu的Z嘛）。而组合子逻辑的原创来自一个乌克兰裔的俄国人，但论文的写作毫无例外的是德语。S来自于德语“组合函数”（Verschmelzungsfunktion），而K则来自于德语“常量函数”（Konstanzfunktion）。在组合子逻辑中，S和K作为逻辑运算符替代符号，其本身也是函数，只不过，它们不是一般的函数，而称作高阶函数。这样我们可以想象在组合子逻辑中的函数都是高阶函数。那么什么是【高阶函数】？简单武断地说就是：以函数作为参数的函数就是高阶函数。而详细探讨“高阶”、“低阶”等关于【阶】概念的学问就是“类型论”，因此对组合子逻辑、λ演算的研究，就必然和类型论放在一起。而类型论本身，又是对逻辑推理的论证模式——证明论的形式化，因此，组合子逻辑、λ演算、类型论、证明论通常纠缠在一起，你中有我我中有你，著名的“命题即类型”（proposition as type）就是所谓的“Curry-Howard同构”，延伸到计算，又称作“证明即程序”（proof as program），形成了“逻辑-数学-计算-逻辑-……”这样一个生态圈。

2 λ演算简介

λ演算(λ calculus)知道的人可能多一些，它是出于同一目的——用逻辑方法解决数学基础问题、由美国数学家、逻辑学家Alonzo Church提出的类似组合子逻辑的方案。

λ演算的基本思想和组合子逻辑相同，只是实现的技术细节不同。例如，λ演算中，函数也是最基本元素，也包含“应用”的概念，而且和组合子逻辑基本相同，但是对如何从已知函数定义或者派生出新的函数，方法上却完全不同。上面讲到，在组合子逻辑中，已经没有变量的概念，所有新函数的生成，都是靠S和K这两个基本“运算符”（高阶函数）的组合完成，而λ演算，则将函数的定义看做是原生的操作之一，看做是“公理”，具体的技术实现就是“函数抽象”；函数抽象就是，函数的建立过程是独立的，不会再从更基本的公理、定理出发，而只根据函数本身的变量和值定义，换句话说，是根据函数的外延性定义。定义公式就是：λx.y，表示ƒ(x) = y。如果你是第一次看见这个符号，千万不要把前面那个希腊字母看做是和ƒ一样的“函数符号”，它不是！那λ表示什么呢？如果硬要牵强地比喻，这个λ更像是谓词逻辑中的量词符号∀或∃。因为逻辑符号从来就不是统一的，即使到了今天仍然如此。弗雷格曾经使用ἑ表示量词，在罗素、怀特海时代x̂常被用来表示约束变量，当时由于排版的原因，往往被写成了∧x，而在视觉上，逻辑符号∧和大写希腊字母Λ经常混淆，所以Church最终决定用希腊小写字母λ表示函数的变量抽象。因此λx.y的正确解读应当是表达式y中变量x的抽取——抽象化，表示变量x与表达式y内某一变量的互动关系。

除了“应用”、“抽象”这样的基本操作外，λ演算另一个重要操作就是“求值”（evaluation），这个过程很有意思，在不同的学科有不同的“解读”：在算术中就是代入求值，x+2=5，x=3，代入3+2=5；在计算机程序中就是“运行”，在函数定义、函数调用之后，最终运行这个函数得到返回值；而在逻辑学中，称作语义解释。

可以看出，从两个形式系统的句法来看，组合子逻辑要比λ演算更加简单，预设的未定义概念、命题更少，在我看来更富有智慧，但是由于历史的原因，λ演算比组合子逻辑更为人所知，例如现在非常流行的计算机程序设计语言Haskell本质上就是λ演算的一种实现。

我们这里的介绍，包括用Haskell和Lisp语言表述逻辑推理，其根本目的在于介绍逻辑和计算的关系，如何从现代符号逻辑的角度更深刻地理解计算问题。

3. 历史背景和产生动机

现代形式科学的所有的故事都来自于莱布尼茨的两大梦想：第一、建立一套严格精密的人工语言，这种语言没有人类语言的歧义多结构，可以精确地描述任何哲学、逻辑和数学问题；第二、找到一种方法，利用这套“普遍语言”，解决任何科学、哲学和数学的问题。

莱布尼茨的梦想，在20世纪先后成真：集合论和符号逻辑、计算科学。而这一切的一切都源自19世纪末20世纪初发生的第三次数学危机。这场危机的结果使得数学、逻辑学和哲学发生了脱胎换骨的变化，数学的公理化、逻辑学的数学化、哲学的逻辑化是这个伟大变革中最显著的特点。

不过很遗憾，这里没有空间详细讲故事，只有三个关键词：数学公理化，数学逻辑化和公理集合论。如果对这段历史不太了解可以参考《数学悖论与三次数学危机》第3、4、5章以及《逻辑的引擎》这两本书。

数学公理化运动，是德国数学家希尔伯特领导的一场彻底重构数学的运动，1899年希尔伯特发表了《几何基础》(Grundlagen der Geometrie)，重新用公理化方法诠释了欧氏几何公理系统。以此为契机，希尔伯特企图将所有的数学理论都嵌入到严格的公理系统中。

而弗雷格的一阶谓词逻辑，则第一次明确地确立了逻辑是数学的基础的立场，亦即，对数学命题的严格描述，只能借助精密严格的人工语言——一阶谓词逻辑才可以完成，这也是当年弗雷格的先辈——莱布尼兹的宏大构想之一。弗雷格企图借助最基础的逻辑概念，建立一个一阶逻辑的形式系统，包括一套人工语言和一套推理规则来定义数学的基本概念；

与此同时发生的就是康托尔的集合论的产生，这使得数学、逻辑和哲学有了一套共同的语言重新定义、解释和表达本学科的概念和命题。因此，当有关集合的悖论被发现后，就不仅仅是数学的危机，同时也是逻辑学和哲学的危机。为了解决数学危机，人类可以说耗费了空前的精力、历经几代人（至少三代）才算达到了对危机的管控；这期间，有多少人皓首穷经、付出毕生精力和心血追求对这个问题的答案。在这个过程中，最大的成果有两个，第一个就是上世纪初怀特海和罗素的鸿篇巨著《Principia Mathematica》，这部著作被后世看做是数理逻辑的圣经，我们现在所熟知的许多数学逻辑学大师都是在这部著作的感召之下走上了逻辑研究之路。第二个就是哥德尔的不完整性定理，亦即，在一个描述自然数算术的逻辑公理化系统内无法使得所有的命题都为真；任何逻辑系统也无法证明自身是无矛盾的。这意味着，所有企图用公理化的方法、逻辑形式系统的框架建立无矛盾的完备的数学公理化系统在逻辑上是不能成立的。哥德尔定理一出，一掷乾坤，使得逻辑学在相当长的一段时间内再没有关于数学基础的活跃研究出现，由于ZF公理集合论的出现，暂时解决了因罗素悖论产生的集合论的心腹大患，使得集合论真正成为所有形式科学的基础语言。

我们讨论的组合子逻辑和λ演算就是在这个大背景下诞生的。为了方便，组合子逻辑我们将用其简称CL，而λ演算则简称为λ。

4 CL的故事

CL的第一创始人Moses Ilyich Schönfinkel（我自己的中文译名：尚芬克尔）是乌克兰裔的俄国数学家和逻辑学家，其俄语名是：Моисей Исаевич Шейнфинкель。Schönfinkel1889年出生于乌克兰，后在敖德萨大学学习数学。从1914年到1924年，Schönfinkel来到德国，加入到希尔伯特领导的哥廷根学派，从事研究。正是在这个期间Schönfinkel专注于数理逻辑的研究，重点是如何简化逻辑学的原始概念，力图用最小数量的原始概念派生所有逻辑运算。在这方面，Schönfinkel的前辈，包括弗雷格、罗素、怀特海已经做了大量工作，在《Principia Mathematica》（数学原理）中，已经将定义前的逻辑运算符从五个减少到两个：否定和析取，或者，否定和合取、析取、蕴含中的任何一个；在此基础上，波兰犹太裔的美国逻辑学家Henry Sheffer提出了一个最激进的简化方案，单一逻辑运算符，写作：nand（学过逻辑电路的可能比较熟悉，称作“非与”门），逻辑符号用竖线表示：“|”，所以又称作“Sheffer竖线”（Sheffer Stroke），其意义相当于合取运算的否定，~(𝑝 ∧ 𝑞)，作为单一运算符，这样，所有其它运算符都可以从它派生。例如：

否定：~𝑝 = 𝑝 | 𝑝 = ~(𝑝 ∧ 𝑝)

析取：𝑝 ∨ 𝑞 = (𝑝 | 𝑝) | (𝑞 | 𝑞) = ~(~p ∧ ~𝑞)

而蕴含可以从否定和析取派生，亦即从上面两个派生式派生，因此这里就不给出了，有兴趣的朋友可以自己试试。

总之，利用“非与”，这一单一运算，就可以派生所有的逻辑运算。而Schönfinkel的研究则是在此基础上更进一步，不但命题逻辑的逻辑连接符可以精简，就连谓词逻辑的变量也可以取消。要做到这一点，就必须对表达逻辑系统的符号概念进行全面更新。Schönfinkel的做法就是：取消所有命题逻辑中的命题字母的概念，不管是有真值的命题常项p、q、r，还是表示量化的变量x、y、z，一律取消。取消的基本理由就是，这些符号没有任何逻辑学上的意义，真正起作用的是逻辑连接符和真值。因此，无论命题逻辑还是谓词逻辑，一律用表达谓词逻辑的真值函数的形式——P(x)表示。有人会说，这里不是还是有变量x吗？是啊！不过这个x是我加上的，作为我们学习的过渡，我们以后会看到变量的出现越来越少，直到踪迹全无。然后，将真值函数的概念一般化，传统一阶逻辑中的所有命题、命题函数一律用函数的形式表示，这就是我们在《通往逻辑、数学和编程的Haskell之路》系列的最后两篇所介绍的内容。这样，无论命题逻辑、谓词逻辑，逻辑系统中的基本元素不再是命题、谓词，而是函数。这是Schönfinkel建立CL朝着简化逻辑系统走出的第一步。

第二步就是简化多参数运算。懂OO编程的都知道方法重载的概念，一个函数，名称、功能都一样，但是所需的参数个数不同，例如加法函数，add(a, b)，add(a,b,c)，可以无限定义，如果我们没有统一的方法论来解决这个问题，可以说这个问题没有最终解决方案。想想看，你如何定义无穷多个参数的加法函数？在数学中，我们可以用归纳法解决问题，Schönfinkel使用的方法本质上，在我看来，仍然是归纳法。懂编程的可能会说，我哪能那么傻一个个定义，我会用数组、对象或任何封装手段将参数打包作为一个参数传递。思路好是好，就是仍然没有解决无限的问题。Schönfinkel用的方法，现在称作“柯里化”（currying），就是将多参数的函数看做是多个单参数函数的叠加，也就说，我不再应对任何多参数的函数问题，只解决单参数函数的问题，一旦单参数的函数没有问题，就可将单参数函数的值重新作为函数应对下一个参数，这个思想，实际上是归纳法的应用。

仍以加法函数举例：add(a, b), 如果重新定义为((add(a))(b)，也就是

add(a, b) 等价于

[add(a)](b)

换句话说就是，我们将add看做是a的函数，而将add(a)看做是b的函数

那么如何得到函数值呢？

add(a) = a + b

设a=2

add(2) = 2 + b

设b=3

[add(2)](3) = 2 + 3

这样我们就得到了函数结果。

再举一例：

<(a, b) = a < b

a = 2

<(2) = 2 < b

b = 3

[<(2)](3) = 2 < 3

从以上结果我们可以看出，用括号表示参数不是必要的，Schönfinkel的写法是

addab

<ab

函数的通用写法是Fxy = (Fx)y

有了对单参数函数的定义，和迭代方法，我们就可以应对任意多参数的函数了

Fx1x2…xn = ((Fx1)x2)…)xn

为什么说是归纳法的应用呢？

1) 我可以得到单参数函数的值：fx1

2）如果可以得到k个参数的函数值，((fx1)x2)..xk)

3）那么我实际就可以得到k+1个参数的值：((fx1)x2)..xk)xk+1

CL的技术细节我们会在后面讨论。现在回到Schönfinkel本人的学术生涯。Schönfinkel在1920年12月7日在哥廷根大学举行的数学学术会议上首次做了关于CL的基本框架和技术细节的口头发表，而作为书面论文，因种种原因直到1924年才以《关于数理逻辑的基本构件》为标题发表（über die Bausteine der mathematischen Logik）。

令人遗憾的是，Schönfinkel此后再未发表过关于组合逻辑方面的论文，最后一篇论文发表于1928年，是和别人联合署名并作为第二作者，内容是关于可判定性问题的，即本篇开始提到的莱布尼茨第二问题。而且令人不解的是，这两篇论文都是在同事“帮助”下发表的，当然这些同事也是著名的数理逻辑学家，Behmann和Bernays，后者后来又和Curry合作研究CL。据说Schönfinkel在1927年左右患上了心理病患，一直在疗养院生活，因此发表论文可能有些技术上的困难，因此这仅有的两篇论文是在同事的帮助下才完成发表。Schönfinkel后来的生活主要是在莫斯科度过，生活拮据、陷入贫困，经济上一直接受朋友的帮助。在长期患病之后于1942年与世长辞。令人匪夷所思的是，他逝世后其手稿竟然被邻居在战争中当做“燃料”给烧了。

在Schönfinkel远离学界之后，他的组合逻辑的思想，却被许多有见识的学者视为珍宝。据史料记载，当年冯诺依曼的博士论文，虽然研究对象是公理集合论，但是其赖以为基础的形式系统却不是基于集合论，而是基于函数的，其中有些公理的设定明显就是Schönfinkel式的组合子运算。据提供史料的作者说，我们不知道是否冯诺依曼的思路是否来自Schönfinkel，但确实知道冯诺依曼在1925年之前访问过哥廷根大学并与其逻辑小组搞过合作研究，所以很难想象他不知道Schönfinkel的研究。冯诺依曼论文中的组合子概念已经经过修改，和Schönfinkel本人的不完全一样，不过冯诺依曼并没有在论文中提及Schönfinkel。

（注：这一段文字，很有些“黑”冯诺依曼的味道，不过在西方学术界不算新鲜事。例如现在“黑”乔姆斯基的也很多，最致命的，要属英国语言学家Pullum提出的《句法结构》中关于句法重写规则系统完全是美国数理逻辑学家Post产生式系统的翻版，这也引起了我对Post学说的兴趣）。

冯诺依曼的组合子理论，在经过几番修改之后，不仅可以在基于函数的形式化系统也可以在基于集合论的系统中适用，现在已经发展成为“Neumann-Bernays-Gödel”系统，简称NBG系统，成为在ZF公理集合论之外另一个重要形式系统。

对Schönfinkel理论感兴趣的不仅仅是冯诺依曼，更是来自大西洋彼岸的美国数学家Haskell Curry。现代人提起CL，首先想到的不是Schönfinkel，而是Curry（中文：柯里）。

Curry对逻辑问题的研究，一生都致力于关于替换性操作问题的研究，这个在外行人看来“很简单”问题，其实包含许多复杂的逻辑基础问题，而这些问题当时还是无人问津的领域，特别是是在《Principia Mathematica》中这个问题就根本没有视作问题讨论。在研究这个问题时，Curry提出了类似Schönfinkel组合子的概念，1927年，当他读了Schönfinkel的论文之后，大喜过望，认为Schönfinkel的论文中所表达思想和自己一致，而且表达的更清楚，见识上更远远超出自己的视野。在事业心的驱使下，Curry放弃了在普林斯顿的教职和正在哈佛攻读的学位，远赴德国哥廷根大学，加入到Schönfinkel曾经工作的小组。由于Schönfinkel是希尔伯特的学生，Curry决定也在希尔伯特的指导下重新开始攻读学位。Schönfinkel那时已经不在哥廷根大学了，Curry只好与曾经和Schönfinkel合作过、对Schönfinkel研究十分了解、并给予其很多帮助的Bernays合作，全力研究Schönfinkel的理论，希望以此为契机，解决替换性操作的问题。

Curry的对CL理论的研究成果，最终归结为和自己学生合著的两卷著作《组合逻辑卷I·卷2》，其后CL成为绝响。

对数理逻辑、特别是对哥德尔以后的数理逻辑新的觉醒，起于1960年代，彼时有几个重大事件可以作为参考。计算机科学开始有了长足进步，在经历的第一门高级程序设计语言Fortran和人工智能语言Lisp之后，由于乔姆斯基的语言学理论所产生的形式语言理论开始普及，特别是对上下文无关语法的研究，使得学者第一次在明确理论的指导下设计程序语言，其结果就是当时非常著名的算法语言Algol语言。与此同时，乔氏对自然语言的形式化研究促进许多形式科学的研究，尤为瞩目的就是蒙太古的形式语义学研究。与此同时，在理论计算机科学界，开始对图灵机以外的计算模型给予更大的关注，使得对类型论、特别是基于构造式数学和直觉主义逻辑的再发现产生了基于直觉主义的类型论。而在逻辑方面，Kripte提出了可能世界的概念，从而将模态逻辑研究引入了可公理化的方向。最重要的，就是对CL和λ的再发现和发展，这一研究又刺激了语言学形式化研究另一分支：范畴语法的发展。这多学科互相影响重新觉醒的趋势一直延续到1980年代，这20多年是一个收获成果的时代。我们现在所有享受到的科技成果（以机器学习为核心的人工智能）、学术理论（类型论、证明论和范畴论）、实用技术（函数式编程）等，其基础都是在1960年代-1980年代学术界的新的复兴运动中建立的。但自1960年代以来的许多理论，都不是新理论，而是在1920-1930年代早已做足了技术储备的基础上发展起来的，这也包括了我们正在学习的CL和λ.

5. λ的故事

λ的创建人是Alonzo Church(中文：丘奇)。Church1903年生于美国华盛顿特区，后在普林斯顿大学学习数学，专攻数理逻辑。在获得博士学位后，曾短暂在芝加哥大学教学，并先后在哈佛大学、德国哥廷根大学和荷兰阿姆斯特丹大学做访问学者。其后一直在普林斯顿大学教学直到1967年退休。

和当时大多数数学家和逻辑学家一样，Church一开始也将自己的研究重点放在了数学基础的逻辑问题上。Church形成λ思想是在1928年，1932年开始向外公布自己的思想。Church最初的目标是建立一个逻辑公理系统，以此作为形式化数学理论的基础。Church认为，怀特海和罗素的《数学原理》(Principia Mathematica)对作为数学基础的许多逻辑问题虽然提出了解决方案，但最大问题是，虽然原始概念、公理设定、推理体系形成了一个科学体系，但是实现这个体系所使用的规则、或者称算法过于复杂。对于数学基础问题的研究当时基本上有两条路线，一条是基于集合论，特别是Zermelo的公理集合论在试图解决悖论方面虽然取得了成就，但仍然留下了问题。而另一条路线就是基于函数，这条路线从弗雷格开始，经皮亚诺、罗素，但是始终没有实质性的进展。美国数理逻辑学家Sheffer提出了简化基本逻辑运算符的方案，为用函数方法解决逻辑问题提供了新的动力。在此基础上，在希尔伯特指导下学习的Schönfinkel和美国数学家逻辑学家Curry进一步提出了系统的基于函数、而不是基于命题变量的逻辑系统。而Church也属于这个阵营。由于Church和Curry、冯诺依曼等人一样，都在哥廷根大学学习过，自然都对Schönfinkel的基于函数的组合子研究了解。因此后来他们各自提出的逻辑系统或多或少都有Schönfinkel的影响存在。

Church的λ思想和组合子方案不同的地方是，后者设立了两个原生的函数常项：S和K，而Church的方案则是将函数看做是一个建构过程，这个过程由函数的框架——函数抽象、和函数与其它对象的互动——函数应用两个部分组成。函数抽象的基本格式就是λx[M]，而函数应用的表示则是{F}(X)，这些表达方式到了现代分别成为：λx . M，(F X)。

而λ符号的使用，Church在1964年明确解释过，其原意是x̂，作为束缚变量，是《数学原理》中的标准用法，也是当时非常流行的表示法，就和现在的全称量词的表示法一样。而Church为了简化将其改为∧x，不久为了区别希腊大写字母，索性改成了小写字母λ。由此可知并λ没有什么特殊的意义仅仅是符号标记，表示束缚的抽象变量而已。

而函数抽象的概念，并不是Church的发明，早在他之前的弗雷格和皮亚诺都曾经提出过相似的概念，Church的创新是，他第一次以函数抽象和函数应用作为逻辑系统的原生概念，以此作为推理其它概念和定理的基础。不过当时由于学术交流不像现在这么方便，Church在制定自己的逻辑系统时，并不知道弗雷格和皮亚诺已经提出并使用类似的概念，因此可以认为对Church来说仍然是一种创造。

遗憾的是，Church的理论生不逢时，1930年代初，哥德尔定理发表，从理论上证明希尔伯特的公理化计划以及《数学原理》的目标在形式上是无法达成的。不过，当时的学界，懂得哥德尔定理的人并不多，况且哥德尔发表论文是在当时世界的学术中心欧洲，而Church作为美国学者，未必对欧洲同行的所有工作都了如指掌。因此Church仍然雄心勃勃地从事自己的数学基础理论的研究。到了1933年底，Church发表了自己的研究成果，继皮亚诺算术公理和《数学原理》之后，Church给出了自己以λ为基础的自然数定义系统。

Church的定义后被称作Church数 (Church numeral)。

Church在普林斯顿教学期间曾经指导了两名出色的研究生：Kleene (中文：克里尼)和Rosser（中文：罗瑟尔），这两个学生在1931年至1934年期间一直和自己的导师共同研究。Church学术成果的相当一部分来自于他们，特别是上面提到的1933年的论文。Church的逻辑体系分为两大部分，第一部分是基础部分，纯λ演算，而不涉及应用这个形式系统到数学其它部分。而另一部分则是λ演算的应用，就像上面将λ演算用于定义自然数。

终于有一天，哥德尔定理对希尔伯特计划的宣判降临到了Church身上，不过这个宣判并不是哥德尔，而正是Church的两个学生，Kleene和Rosser，他们发现了Church逻辑体系中存在着类似于Richard悖论的矛盾性，这个证明现在叫做Kleene-Rosser悖论。而Richard悖论则是法国数学家提出的有关自然语言表述数学对象时产生的语义悖论[1]。

由于纯λ演算不牵涉对算术系统的推理，因而不存在矛盾性问题。而且Kleene发现纯λ演算虽然在Church系统中只作为基础，看似很简单，但是从这些基本的函数抽象和应用中，特别是后来发展出来的β-归约，其实和组合子逻辑的中心问题——替换问题其实是同一问题。在这一思想的指导下，Church和他的学生Rosser证明了一个关于λ项和λ演算的一条定理：当把归约规则施用于λ项和λ演算时，所选择的归约顺序将不会影响最终的结果。这个定理的意义我们以后会谈到，现在能说的就是，如果归约顺序无碍于结果，那么对一些比较复杂的λ演算就可以大大简化。

Church在后来的研究中发现如果一个可以用λ演算定义的关于计算基数的函数，其实可以形成一个更大的类，而这类函数后来证明等价于当时已知的关于递归函数和可计算函数的两个理论：Herbrand-Gödel递归函数论和图灵的可计算函数理论，这样使得过去关于“有效计算性”这种不严格的术语就可以在λ可定义性的概念下得到精确的定义。最令人印象深刻的就是，图灵的可计算函数是以图灵机——一种想象的无限长的纸带上的读写过程可以等价于λ可定义的函数类，它们的共同点就是现代计算机科学对计算有效性的描述：对某类问题的解决，其过程必须是有限长的步骤，过程最后总能够结束，过程结束后总可以产生正确结果。如果达到这样的有效计算，就可以称作λ可定义，而在图灵的术语中则称作可计算函数。所以这个结果后来被称为Church-Turing Thesis (中文：丘奇-图灵论题)。在这里λ演算从最早的逻辑形式系统的基本要素转化成为研究递归函数进而研究有效计算最后为此建立了形式化理论——λ可定义——等价于Herbrand-Gödel递归函数和图灵的可计算函数，这就是λ演算脱胎于逻辑，在数学基础研究遭遇失败后，成功转型成为早期理论计算科学基础的过程。

正像上篇所述，上世纪1960年代，随着计算机科学的进步，CL和λ重新受到青睐，不过不是逻辑学家而是一个新领域的学者——计算机科学家。在这方面，英国学者Peter Landin可以说是先行者。他在构建新型的程序设计语言Algol60的时候第一次提出以λ-项作为语言的基本结构，并首次提出以λ演算为基础的抽象机概念，这个理论后来成为函数式编程语言编译器设计的基本理论——SECD抽象机；S：栈，E：环境，C：控制，D：转储。介绍SECD不是这篇文章的目的，因为回头看，我们已经离开逻辑的领域很远了，再往前走就是计算机科学的地界了，只好先打住。

关于Richard悖论有兴趣的可参考百度百科

本篇笔记主要参考了以下文献：

《History of Lambda-calculus and Combinatory Logic》

《Type Theory and Formal Proof》

《Combinators, λ-Terms and Proof Theory》

<Wikipedia> Church-Turing Theis>

<Wikipedia> SECD machine>