|
|
如果说当今哲学界有一个被严重低估的概念，那就是计算。它为何如此重要？因为计算主义是当代的新机械论。几千年来，哲学家们想要论证或质疑宇宙能否以机械的方式被解释，却始终举步维艰——因为很难界定什么是机器、什么不是机器。而“计算”这个概念恰好解决了这个问题：它精准定义了机器能做什么、不能做什么。如果宇宙/心灵/大脑/兔子/上帝可以用机械方式解释，那它就是一台计算机，反之亦然。
遗憾的是，编程和计算机科学领域之外的大多数人，都不清楚“计算”到底是什么含义。很多人可能听说过图灵机，但这类概念往往弊大于利：它们会让人强烈联想到转动的齿轮和纸带，却掩盖了其本质——对计算核心本质的具象化呈现。
λ演算也完全能实现同样的效果，却不会用齿轮这类具象意象干扰你的认知。乍看之下它的数学感强得吓人（毕竟名字里还带了个希腊字母！），所以计算机学术圈之外几乎没人愿意深入了解它，但它其实简单到超乎想象。一旦你弄懂它，就能对“计算”形成深刻得多的直观认知。
λ演算由阿隆佐·邱奇在20世纪30年代中期提出，几乎和图灵机诞生于同一时期。别被“演算”这个词吓到！它根本没有复杂的公式或运算规则，全程只做一件事：拿一串字符（符号），对它执行简单的剪切粘贴操作。你很快就能看到，λ演算仅凭这套极简的剪切粘贴规则，就能完成所有可计算的任务。
一串符号就叫做一个表达式，比如这个例子：(λx.xy) (ab)
我们用到的符号只有三类：
- 单个字母（比如a、b、c、d……）：被称为变量。一个表达式可以是单个字母，也可以是多个字母连写。更宽泛地说，任意两个或多个表达式拼接在一起，就能得到一个新的表达式。
- 括号：( )：用来标注表达式里需要绑定为整体的部分，就像句子里用括号把内容归为一组。没有括号的地方，我们就从左到右依次解读表达式。
- 希腊字母λ（读音为“拉姆达”）和点号.：用λ和点号就能写出函数。函数的固定格式是：以λ开头，后跟一个变量，接一个点号，最后跟上一个表达式。λ本身没有复杂含义，它只用来标记“这里开始定义一个函数”。函数里λ-变量-.的部分叫做函数头，后面剩下的表达式部分叫做函数体。
问：变量的值或含义是什么？
答：什么都不是。变量不指代任何实体，它们只是空的名称，甚至连名称本身都不重要。唯一的规则是：两个变量同名，它们就是同一个变量。你可以随意重命名变量，完全不会改变表达式的含义。
问：函数在计算什么？
答：实际上什么都不算。它只是一类带有函数头和函数体的表达式，就只是静态存在的符号串。我们能对它做的唯一操作，就是对它做归约处理。
问：为什么符号是“λ”？
答：这或许只是个意外。最初阿隆佐·邱奇只是画了个小屋顶符号来标记头部变量，写成(ŷ xy) ab。在录入打字稿时，他把这个屋顶符号放到了头部变量前面，变成了(⋀y.xy) ab。排版工人最终把它排成了视觉上足够接近的(λy.xy) ab，λ符号就这么沿用了下来。
更严谨一点来说：所有变量都是λ项，也就是λ演算中的合法表达式。如果x和y都是λ项，那么(x y)是λ项，(λx.y)也是λ项。凭借这三条规则，我们就能构造出所有合法的表达式。如果我们约定所有λ表达式都从左到右解读，还可以省略部分括号：(λy.xy) ab就是(((λy.(x y)) a) b)的简化写法。
剪切与粘贴
如果函数后面紧跟着另一个表达式，就可以对这个函数做归约操作。归约的规则是：取出函数头里标注的变量，把函数体里该变量的所有出现位置，全部替换成函数后面的那个表达式。我们把函数后面的表达式剪切下来，粘贴到函数体里所有由函数头指定的位置。完成替换后，就可以丢弃函数头了——它的作用已经达成，也就是告诉我们要替换哪一个变量。
函数归约是λ演算中我们唯一能执行的操作。一旦我们消去了所有λ符号，或是剩余函数的后面再也没有可用于替换的表达式，就再也没法做任何替换操作了，整个归约过程就可以结束了。
问：函数可以嵌套其他函数吗？
答：完全可以。函数本身就是表达式，而表达式可以包含其他表达式，所以函数可以成为其他函数函数体的一部分，也可以作为替换用的表达式的一部分。实际上，像λx.λy.xzy这类表达式出现频率极高，我们通常会把它简写为λxy.xzy。这代表我们会依次用函数体后的第一个表达式替换函数头里的第一个变量x，用紧随其后的下一个表达式替换第二个变量y，以此类推完成所有替换。
函数头里标注出来、指定要被替换的变量，就叫做约束变量。没有被函数头提及的变量，就是自由变量。由于函数可以嵌套在其他函数内部，同一个表达式里的某个变量，可能同时兼具约束和自由两种属性。
问：我觉得这有点让人摸不着头脑。
答：你可以这么理解：想象你在编辑一份风格极简的八卦小报，这份报纸里所有内容全是人名——没有冠词、动词、代词，只有名字。当事人不想在报道里被认出来，你就把所有真名都替换成了随机的化名。这些化名本身没有任何实际含义，但只要同一段文本里出现了两个相同的化名，它们指代的就是同一个人。
报纸里的所有内容都按文本块排布。一个文本块最终完全由名字构成，它可以有标题，也可以没有。标题用粗体印刷，且仅由一个名字组成。在该标题对应的正文范围内，这个名字的所有出现位置都是“特指”的，也就是指代标题里的这个人。所有没出现在标题里的名字都是普通泛指的名字。文本块可以嵌套其他文本块，连带它们的标题一起——这些嵌套标题就相当于子标题、二级子标题，以此类推。因此，同一个名字在某个子文本块里是普通泛指的，在另一个子文本块里，就可能被该子块的标题指定为特指对象。
这和λ演算的逻辑完全一致：名字就是变量，文本块就是表达式，标题就是函数头——只不过函数头不用粗体印刷，而是用λ和点号包裹起来，让我们能明确它的起止边界。
归约操作就是一次简单的查找替换：我们找到带标题的文本块里所有约束名的出现位置，把每一处都替换成紧跟在它后面的那个文本块。（当然要说明的是，在现实报纸里，用一整段内容替换单个名字的操作几乎没有实际意义。）
顺便提一句：如果用来替换的文本里，包含了我们要合并进去的原文本中已有的同名名字，就会遇到一个小问题。所有名字都是匿名化名，但不同文本里可能用了同一个化名指代不同的人。现在把这些文本合并到一起时，我们必须确保不同的人用不同的化名指代，所以可能需要给部分化名重新命名。
另一种方案是，我们可以约定任意两个文本块都不使用相同的名字。换句话说：要么在互不相关的表达式里使用不同的变量，要么在替换操作过程中，根据需要及时给变量重命名，避免冲突。
问：如果一个变量在函数头里被约束了，但函数体里完全没有出现它，会发生什么？
答：这个变量当然还是处于被约束的状态。但在执行替换操作时，用来替换的表达式会直接消失——因为函数体里根本没有可以插入它的位置。这完全是合理的，它反而能简化最终结果，没有任何问题。
数字
搞定所有技术细节之后（太棒了！这部分很简单，对吧？），我们来看看能用λ演算实现哪些有趣的功能。你可能会说计算总得能处理数字，那我们就来构造数字。数学家通常会从自然数起步，再通过定义各类运算推导出其他数的类型。
一次性定义所有自然数的最简单方法，是先定义第一个数（也就是0），再定义一个后继运算。对任意自然数执行后继运算，就能得到一个更大的自然数，这样我们就可以通过递推计数推导出全部自然数。
我们把0表示为：
0 :⇔ λ sz.z
（记住：这是λs.λz.z的简写，它和λab.b、λqx.x的含义完全相同。）
这个表达式有个很有意思的特性：执行归约时，它会直接丢弃紧跟在它后面的第一个表达式，完整保留第二个表达式。约束变量s不会被任何内容替换——因为它根本没在函数体里出现，而变量z最终会保留自身。
译注：
((λs. λz. z) A) B
→ (λz. z) B （A 被丢弃，因为 s 不在函数体里）
→ B （z 被替换成 B）
同理，我们可以这样定义：
1 = λ sz.s(z)
2 = λ sz.s(s(z))
3 = λ sz.s(s(s(z)))
4 = λ sz.s(s(s(s(z))))
……
换句话说，这套数字表示法的规则是：在z的外层嵌套s(...)的次数，就等于这个数字本身的数值。这也意味着，当我们对数字n做归约时，它会把紧跟其后的表达式重复复制n次。我们也可以表述为：把s作用在z上，一共执行n次。
一个简洁的后继函数定义如下：
S :⇔ λ abc.b(abc)
我们来用它计算0的后继：
S0 = (λ abc.b(abc)) (λ sz.z)
= λ bc.b((λ sz.z) bc)
= λ bc.b((λ z.z) c)
= λ bc.b(c)
最后得到的这个表达式已经无法再化简了——函数体后面已经没有可用于替换的表达式了。你会惊喜地发现：
λ bc.b(c) = λ sz.s(z) = 1
也就是说，把后继函数作用在我们定义的0上，就能得到1的表达式。我们可以再试一次：
S1 = (λ abc.b(abc)) (λ sz.s(z))
= λ bc.b((λ sz.s(z)) bc)
= λ bc.b((λ z.b(z)) c)
= λ bc.b(b(c))
你看，结果正好是：
λ bc.b(b(c)) = λ sz.s(s(z)) = 2
我们能看到，这个后继函数完全实现了预期功能：从0出发，它可以生成任意自然数。它的实现逻辑，就是在输入的任意自然数的函数体外层，再多嵌套一层s(...)结构。这就是剪切粘贴操作的神奇魔力！
问：这种写数字的方式也太奇怪了……
答：实际上从数学角度来看，这套表示法和用阿拉伯数字1、2、3……，罗马数字I、II、III……，中文数字一、二、三……，或是二进制1、10、11……相比，并没有更怪异。数字的书写不存在唯一的“正确方式”，只有不同的约定规则而已，自然数本身根本不会在意我们用什么形式来表示它。
加法
数字加法可以理解为对后继函数的自动化封装。如果要给数字3加上5，就相当于对3连续执行5次后继运算（反过来也成立，因为3+5=5+3）。
幸运的是，我们这套数字表示法本身就内置了这种自动化能力。前面我们提到过，对数字n求值，就意味着把它后面的表达式重复执行n次。如果紧跟在数字后的表达式是后继函数，归约后就会自动把后继函数作用在它后面的数字上，连续执行n次。
3+5 = 3S5 = (λ sz.s(s(s(z)))) (λ abc.b(abc)) (λ xy.x(x(x(x(x(y))))))
如果你想动手验证，可以试着一步步归约，最终会得到8的表达式：λ xy.x(x(x(x(x(x(x(x(y)))))))。
乘法
一个同样设计巧妙的函数可以实现乘法运算：
MULTIPLY :⇔ λ abc.a(bc)
这个函数接收两个参数，比如计算2×3的过程如下：
2 × 3 = MULTIPLY 2 3 :⇔ (λ abc.a(bc)) (λ sz.s(s(z))) (λ xy.x(x(x(y))))
= λ c.(λ sz.s(s(z)))((λ xy.x(x(x(y))))c)
= λ cz.((λ xy.x(x(x(y))))c)(((λ xy.x(x(x(y))))c)(z))
= λ cz.(λ y.c(c(c(y)))) (c(c(c(z))))
= λ cz.c(c(c(c(c(c(z)))))) = 6
它的运行原理是什么？仔细观察就能发现，乘法函数接收2和3两个参数后，会按这样的逻辑排布：
MULTIPLY 2 3 = (λ abc.a(bc)) 2 3 = λ c.2(3c)
对这个表达式归约后得到λ cz.(3c)(3c(z))，相当于先把第二个c作用在z上3次，得到c(c(c(z)))，再把第一个c作用在这个结果上3次，得到c(c(c(c(c(c(z)))))。再加上函数头λ cz，最终就得到了6——也就是把第一个参数对应的操作，在第二个参数的基础上重复执行6次。
想要彻底消除疑惑，最好的办法就是拿纸笔自己动手试几次乘法运算，很快你就能完全掌握这套规则了。
反向计数
到目前为止，我们只实现了从小数往大数的递增运算。要做减法，我们还需要一个前驱运算，这样就能实现反向计数。我们该怎么构造它呢？
根据之前的定义，除了0被直接定义为λ sz.z之外，所有自然数都是另一个数的后继。我们可以基于这个定义，把前驱描述为：对它执行后继运算，就能得到原本给定的那个数。
用常规的数学语言表述就是：y = P(x) ⇔ x = S(y) —— 当且仅当x是y的后继时，y就是x的前驱。可惜这只是一个功能说明，并不是可执行的计算过程。说明只定义了前驱函数需要满足的条件，却没有给出它的具体运行逻辑。而λ演算只能执行明确的计算，我们必须把从x得到y的每一步操作都完整、精确地定义出来。
一种可行的实现思路是：从0开始，把后继函数连续执行x次：
x S 0 = x (λ abc.b(abc)) (λ sz.z)
得到的表达式就是x对应的数值。如果我们能在第x-1次执行后继操作（也就是最后一次嵌套s(...)之前），把当时的表达式状态记录下来，就能得到x的前驱对应的表达式。
我们可以用一对数来实现这个目标：不用单独的x，改用数对(y, y-1)。然后定义一个新的后继函数，能从这个数对推导出(y+1, y)。我们从y=0的初始状态开始，把这个后继函数重复执行x次，最终得到的数对就会是(x, x-1)。最后取出数对的第二个元素，就得到了x的前驱。具体实现如下：我们把数对(a, b)表示为λp.pab。最小的初始数对是λp.p00，展开后就是λp.p (λ sz.z) (λuv.v)。我们可以取出数对的第一个元素a，构造出新的数对(a+1, a)，这就是数对版本的后继操作。
数对λp.pab的第一个元素，可以通过把它作用在λxy.x上得到：
(λp.p a b) (λxy.x)
= (λxy.x) a b
= (λy.a) b
= a
可以看到，λxy.x会保留紧跟在它后面的第一个表达式，直接丢弃第二个。同理，要取出数对的第二个元素，用λxy.y就可以实现。
新数对(a+1, a)的构造方式是：用后继函数S = λ abc.b(abc)作用在a上，再把得到的S a和a打包成新数对。
NEXT-PAIR pair :⇔ (λ pair z.z S (pair λxy.x) pair λxy.x) = (a+1, a)
别被λ pair的写法搞晕，它只是表示要把数对(a, a-1)代入这个λ函数的函数体里。
现在我们把这个函数从初始数对(0, 0)开始，重复执行n次，最后取出数对的第二个元素，就能得到最终结果。你可能已经发现这里做了一点简化：初始数对(0, 0)并不是严格意义上的(a, a-1)，也就是(0, -1)。但我们目前还没有定义负数，而且这个辅助函数NEXT-PAIR本来就会忽略数对的第二个元素，所以完全不影响运算。对(0, 0)反复执行NEXT-PAIR，就会依次得到(1, 0)、(2, 1)、(3, 2)、(4, 3)……
前驱函数P的完整定义就是：
P n :⇔ (λn.n NEXT-PAIR(0, 0)) λxy.y
借助这个前驱函数P，我们就可以在自然数范围内实现反向计数。注意当数值降到0之后，继续执行前驱运算结果会保持为0，这是很合理的特性。我把负数、除法、幂运算、虚数的定义留给你当作练习。说实在的，我们完全可以花大量篇幅在λ演算里复现集合论和数论的全部标准内容，但这对理解核心机制不会有太多额外帮助。
问：我明白我们可以通过多次执行前驱运算来实现减法，但每次要做一次前驱操作，都得从0开始用后继运算生成所有中间数，这难道不是效率极低吗？
答：谁在乎啊！λ演算只承诺能有效计算所有可计算的内容，从来没保证过要高效完成计算。而且它本身就是一个数学概念，在抽象的数学世界里，它完全可以以无限快的速度运行。
逻辑运算
λ演算并不局限于数值计算，它同样可以轻松处理逻辑表达式。还记得之前用来选取数对元素的两个小函数吗？我们可以直接用它们定义布尔值的真和假：
TRUE :⇔ λ xy.x
FALSE :⇔ λ xy.y
布尔逻辑里有AND、OR、NOT这类运算符来判定逻辑表达式的结果，这些在λ演算里也都能实现。比如我们可以用下面这个定义，把TRUE取反得到FALSE，把FALSE取反得到TRUE：
NOT :⇔ λ a.a (λ bc.c) (λ de.d)
它的运行逻辑是怎样的？比如我们计算NOT TRUE（展开后是(λ a.a (λ bc.c) (λ de.d)) λ xy.x），开头的λ a.a会把TRUE代入，作用在后面的(λ bc.c) (λ de.d)上，也就是FALSE TRUE。而TRUE本身就是我们之前用来选取数对第一个元素的函数，所以TRUE FALSE TRUE等价于：从数对(FALSE, TRUE)里选出第一个元素，最终得到FALSE，正好完成取反。
下面是AND和OR的定义，感兴趣的话你可以自行推导它们的运行原理：
AND :⇔ λ ab.ab (λ xy.y)
OR :⇔ λ ab.a (λ xy.x) b
条件判断
我们不只能从逻辑值计算出新的逻辑值，下面这个函数可以判断给定数值是否等于0：等于0时返回TRUE，否则返回FALSE，这类判断在编程中非常实用。
IS-ZERO :⇔ λ a.a FALSE NOT FALSE
把IS-ZERO作用在任意非零数n上，得到：
IS-ZERO n = n FALSE NOT FALSE
这会把函数FALSE连续n次作用在NOT上，最终再作用在末尾的FALSE上。每一次运算，第一个FALSE（即λ xy.y）都会直接抹掉紧跟在它后面的表达式，经过n次运算后，最终会到达NOT FALSE的位置，抹掉NOT后返回FALSE，因此IS-ZERO作用在任意非零数上结果都是FALSE。如果觉得抽象，可以代入具体数值试算验证。
唯一的例外是n=0的情况：把0作用在FALSE NOT FALSE上，它会直接跳过第一个表达式，最终只剩下NOT FALSE = TRUE：
IS-ZERO 0
= (λ sz.z) FALSE NOT FALSE
= NOT FALSE
= TRUE
掌握了判断数值是否为0的能力后，我们就可以定义“大于等于(≥)”运算：
GREATER-OR-EQUAL n m :⇔ λ n m. IS-ZERO(n P m)
它的逻辑是：对m连续执行n次前驱运算。如果n和m相等，最终结果是0；如果n大于m，结果也会停在0；只有当m大于n时，最终结果才是非零值。
借助≥运算，我们就能进一步定义相等判断：当n≥m且m≥n时，n和m相等，对应的λ演算表达式为：
EQUAL n m :⇔ λ n m. AND (GREATER-OR-EQUAL(n m) GREATER-OR-EQUAL(m n))
= λ n m. AND (IS-ZERO(n P m) IS-ZERO(m P n))
延伸拓展
如你所见，λ演算本身就是一种极简的编程语言。这是必然的，因为所有能写出的计算机程序，最终都可以被映射为某个λ函数。实际上，经典且强大的编程语言Lisp就是直接基于λ演算的思想构建的，只是对语法做了实用化调整，规范了函数宏的创建方式，还补充了少量实用的数据类型。
我们这篇入门内容，大体参考了劳尔·罗哈斯的优秀教程《λ演算入门指南》，那篇教程面向计算机专业学生，还覆盖了递归相关内容，整体技术深度会稍高一些。现在你已经掌握了基础概念，完全可以去挑战更进阶的入门资料，比如维基百科上的相关词条。
所有可计算的内容
λ演算并不能覆盖全部数学领域：很多数学问题没有解，还有大量数学公式是不可计算的，这两者并不是一回事。那么图灵机和λ演算谁的能力更强呢？
实际上，我们完全可以把图灵机纸带上的所有内容，映射为一个λ表达式（其中还包含读写头的状态和位置信息），再构造出对应的λ函数，让它修改这个表达式的结果和对应图灵机的运行结果完全一致。
反过来，我们也可以把任意λ表达式写到纸带上，构造出一台图灵机，完成所有需要的查找、替换操作。由此可以证明，λ演算和图灵机的计算能力完全对等。
同理可以证明，我们能造出的所有计算机，计算能力都是等价的，包括个人电脑、超级计算机、量子计算机甚至iPhone。它们之间的区别只在于实际实现的内存大小，以及得到结果所需的运算步数。这个“所有计算机的底层计算能力本质上完全对等”的结论，就是著名的“丘奇-图灵论题”。
λ演算还可以以任意精度完成神经网络的计算：把神经元之间的连接权重、神经元的激活值都表示为丘奇数，再以极小的时间步长计算激活值在网络中的传播过程。从技术层面来说，所有能处理信息的可实现系统都是可计算的，而所有能表达λ演算（或其他可以等价表达λ演算的体系）的可计算系统，都可以被定义为一台计算机。
原文链接
|
|
发表于 
发表于