Lambda Calculus 学习笔记

· · 科技·工程

UPDATE on 2025 年 11 月 6 日：修复了 null? 的 bug。

前言

今天突然想起了 CodeWars，想在里面试试 Scheme，结果看到有个语言叫“Lambda Calculus” 就尝试了用这个做题。

然后就被创飞了。

所以我要好好复习一下 Lambda Calculus，于是我就要写这篇文章。

Lambda Calculus 的语法

金将军说过：编程语言一定要有语法。所以 Lambda Calculus 有语法，Lambda Calculus 中有三种元素如下：

::cute-table{tuack}

内容 变量 函数 应用
形式 <变量名> λ <参数> . <函数体> <函数> <参数>
解释 就是变量名 就是函数，返回 <函数体> 的值 以 <参数> 为参数调用 <函数>，是左结合的
例子 a λ x y . x (λ x y . x) a b
解释 一个叫 a 的变量 一个有两个参数的函数，函数的值是第一个参数 调用刚才的函数，以 a b 为参数

没看懂？很正常，我们来看一些例子：

  1. (λ x y . x) a b

a 的值。

  1. (λ x y . y) a b

b 的值。

  1. (λ u t f . u t f) (λ x y . x) a b

这个比较复杂，但我们可以进行代换，把它变成 (λ x y . x) a b，那原式的值就是 a。

第三个例子告诉我们：函数也可以是参数，应用也可以是函数体，当然函数也可以是函数体，这点我们稍后再说。

然后原生的 Lambda Calculus 的语法就只有这么多了，但某些常见的版本还有以下两种元素：

::cute-table{tuack}

内容 数字 定义
形式 <数字> <名称>=<值>
解释 就是数字 用于把复杂的值绑定到一个名称上，方便后续使用
例子 114514 true = (λ x y . x)
解释 略 略

语法规则太少了！什么东西都没有！这种语言真的可以用吗？你可能这么想，但不管是原版 Lambda Calculus 还是扩展版，都是图灵完备的，下一节我们就来开始研究怎么做到这点。

实现布尔型

（下文中我们使用扩展版 Lambda Calculus，注意上下文中的函数的引用）

（并且用 ; 表示单行注释）

这很简单，我们只要定义出下面的这些东西就行了：

true = λ x y . x
false = λ x y . y

if = λ u t f . u t f

and = λ x y . if x y false
or = λ x y . if x true y
not = λ x . if x false true

你可能第一眼看到这些东西后一头雾水，并质疑它的可用性，所以我们还是举几个例子吧。

  1. if true a b

我们要求这个式子的值，实际上就是求 (λ u t f . u t f) (λ x y . x) a b，把参数带入后前面那一坨就直接没了，所以转化成求 (λ x y . x) a b，再把 a b 带进去变成 a，这就是最终结果（其实就是上一节的第三个例子）。

在 C++ 里可以这么写：(true ? a : b)，也许你就理解了。

  1. and true false

还是一样的步骤（每行都是等价的）：

and true false
(λ x y . if x y false) (λ x y . x) (λ x y . y)
if (λ x y . x) (λ x y . y) (λ x y . y)
(λ u t f . u t f) (λ x y . x) (λ x y . y) (λ x y . y)
(λ x y . x) (λ x y . y) (λ x y . y)
(λ x y . y)

也就是 false。

然后其它的函数你可以自己试试。

于是我们就可以发现了：Lambda Calculus 中根本没有“变量”，只有函数，连布尔值都是函数（你也许可以猜出下一节的内容了）。

很奇怪，很猎奇，但是这是可行的一种解决方案。

数字（只有非负整数）

在构造数字前，让我们先拜谢阿隆佐·邱奇大佬，他是图灵的老师，发明了 Lambda Calculus，并用这个证明了停机问题的不可计算性。%%%orz

然后我们考虑使用邱奇编码来表示函数，也就是说我们可以认定：

n=\lambda f x.\overbrace{f(f(\cdots f(f}^{n个}(x))))

也就是一个函数，参数为 f x，返回 f 在 x 上应用 n 次的结果。

例如：

0 = λ f x . x
1 = λ f x . f x
2 = λ f x . f(f x)

虽然这很低效，但是我们已经没有更好的办法了。

如果这还不够让你如雷灌顶的话，请看：

succ = λ n . λ f x . f(n f x)

这个函数有什么用？它可以返回 n+1。

试试看！

succ 3
succ (λ f x . f(f(f x)))
(λ n . λ f x . f(n f x)) (λ f x . f(f(f x)))
λ f x . f((λ f x . f(f(f x))) f x)
λ f x . f(f(f(f x))) ; 就是 4

我们很自然地想到用 succ 去定义加法，然而这是可行的，如下：

add = λ a b . a succ b

也就是把 a 的 f 和 x 换成 succ 和 b。

试着展开一下（不太好用纯文本描述所以换成了 \TeX）：

a\ \text{succ}\ b \\ \lambda f x.\overbrace{f(f(\cdots f(f}^{n个}(x))))\ \text{succ}\ \lambda f x.\overbrace{f(f(\cdots f(f}^{m个}(x)))) \\ \overbrace{\text{succ}(\text{succ}(\cdots \text{succ}(\text{succ}}^{n个}(\lambda f x.\overbrace{f(f(\cdots f(f}^{m个}(x)))))))) \\ m+n

但这样比较复杂，于是有另一种加法的定义方式（实际上没有太大区别）：

add = λ a b . λ f x . a f (b f x)

并且丘奇指出了这两个式子：

mul = λ a b . λ c . a (b c) ; 乘法
pow = λ a b . b a ; 乘方

你可以试着证明一下这两个式子的正确性。

（你可以在这里测试你的代码）

另外我们还可以判断一个数是否为零（感谢 @litjohn 大佬）：

zero? = λ n . n (λ x . false) true

然后我们还要实现减法，但现在还做不到，请看下一节。

元组

目前我们已有的数据结构都太简单了，而且它们之间的关系是离散的，于是我们就想到要有个东西能把它们聚合起来，这样我们就可以有更复杂的程序，最天真的想法就是把两个数据“黏”在一起，这是尝试的结果：

cons = λ x y . λ p . if p x y ; 把两个元素黏在一起的函数
car = λ p . p true ; 把第一个元素取出来
cdr = λ p . p false ; 把第二个元素取出来

当然还有别的实现方式，但这种算是比较简洁的了。

元组最简单的应用就是实现减法。

设想有一个函数 f，给它一个二元组 (a, b)，它会返回一个二元组 (b, b+1)，那如果对 (0, 0) 应用 n 次 f，就可以得到 (n-1, n)，于是我们可以写出一个可以求出 n-1 的函数（对于 0，它返回 0）：

pred = λ n . car (n
  (λ a . cons (cdr a) (succ (cdr a)))
  (cons 0 0))
; 我们可以把函数拆成多行写

你可以自己去验证这个函数的正确性，然后我们可以写出减法和一系列谓词：

sub = λ a b . b pred a
le = λ a b . zero? (sub a b) ; 小于等于
ge = λ a b . le b a ; 大于等于
eq = λ a b . and (le a b) (ge a b) ; 等于
neq = λ a b . not (eq a b) ; 不等于
lt = λ a b . and (le a b) (neq a b) ; 小于
gt = λ a b . and (ge a b) (neq a b) ; 大于

测试你的代码

然后因为元组的元素还可以是元组，所以就可以构造出列表、树之类的东西。

但在这之前，我们要先实现递归。

递归

我们要来实现递归，也就是一个函数不断调用自身来进行循环的操作。举个例子，如何实现一个函数，返回第 x 个斐波那契数？

我会！

fib = λ x . if (lt x 2)
  1
  (add (fib (sub x 1)) (fib (sub x 2)))

然而这样是不行的，这样的代码没法按传统的方式（是什么呢，好难猜啊）运行。

那我们可以把目光移向参数，这是个存储数据的好地方：

fib- = λ f x . if (lt x 2)
  1
  (add (f f (sub x 1)) (f f (sub x 2)))

f = λ x . fib- fib- x

这种做法和上面的做法看上去一样实际上是不一样的，我们把代码里的 if、lt、add 之类的东西展开再把代码变成原生的 Lambda Calculus 版本后就会发现：第一个版本因为调用了自己导致无法被展开，而第二个版本就可以正确地展开。

我们把这一技术称为自应用技术（有时也被戏称为“穷人的 Y 组合子”）。

但这么做是很烦的，所以我们来尝试一个更简单的例子：

sum = λ s . λ x . if (eq x 0) 0 (add x (s (sub x 1)))

那我们只要找到一个合适的 s 就可以了，且这个 s 要满足 sum s = s。

那我们假设有一个函数 Y，使得对于所有类似于 sum 的函数 f 和类似于 s 的 g（即 f g = g），都有 Y f = g。

为了得出 s，我们再设一个函数 G 使得 G G = s。又 s = sum s，所以 G G = sum (G G)。观察这个等式，可以找到 G 的定义：

G = λ x . sum (x x)

那 s 和 Y 也就有了：

s = G G
Y = λ f . (λ x . f (x x)) (λ x . f (x x)) ; 这就是 Y 组合子

但这要求我们的语言是惰性求值的，因为一旦执行 Y，语言内核就会试图不断展开 (x x)，从而应发无线循环。所以为了使 Y 组合子能在一般的语言环境中运行，我们要将 (x x) 封装在一个函数内部来进行延迟求值，我们把这种方法称为 Z 组合子：

Z = λ f . (λ x . f (λ y . (x x) y)) (λ x . f (λ y . (x x) y))

我们的 Lambda Calculus 语言已经可以支持更复杂的运算了，现在它距离完全被证实图灵完备只有一步之遥，那就是更复杂的数据结构。

列表

我们已经做了很多，但是还没有开始接触列表。列表是一些元素，经过 cons 的“黏合”组成的，比如由数字 1 到 5 组成的列表是这样构造的：

onetofive = cons 1 (cons 2 (cons 3 (cons 4 (cons 5 nil)))) ; 注意最后的 nil

这里的 nil 是指一个空表，它的定义如下（这和 0 很像，不是吗？）：

nil = λ f . true

当然为了方便，我们还要实现一个函数 null? 来判断一个列表是否是空表（这和 zero? 很像，不是吗？）：

null? = λ x . x (λ a b . false)

因为和列表相关的操作通常是需要递归的，所以我们现在终于可以开始了。

length- = λ len . λ a . if (null? a)
  0
  (add 1 (len (cdr a)))

length = Z length- ; 使用前面的 Z 组合子来实现递归
append- = λ app . λ a b . if (null? a)
  b
  (cons (car a)
        (app (cdr a) b))

append = Z append-
max- = λ m . λ a . if (null? a)
  0
  ((λ x y . if (gt x y) x y) (car a) (m (cdr a)))

max = Z max-

像这样的例子我们还能举出很多。同时，因为列表的元素还可以是列表，所以我们可以用 Lambda Calculus 写出的代码的复杂度也就可以进一步提升。

参考文献/完结撒花

Harold Abelson, Gerald Jay Sussman and Juile Sussman. 计算机程序的构造与解释（原书第 2 版）[M]. 北京：机械工业出版社，2019.

Daniel P. Friedman, Matthias Felleisen. The Little Schemer: 递归与函数式的奥妙[M]. 北京：电子工业出版社，2017.

Roger Penrose. 皇帝新脑[M]. 长沙：湖南科学技术出版社，2007.

Let's build our mathematics by using lambda calculus && church encoding! - 洛谷专栏

Learn Lambda Calculus in Y Minutes

λ演算-简单介绍lambda演算的基本定义以及操作 - 知乎

初涉 λ 演算 (lambda calculus) - greyishsong

Y组合子的一个启发式推导 - 知乎

其实我还留了一个坑，那就是 Lambda Calculus 的运行方式，比如 β 规约、η 变换、柯里化之类的，但考虑到这篇文章的写作目的是学会使用 Lambda Calculus，就都略过了。

下次一定。