𝜆 演算 (Lambda Calculus)

0. 背景

函数

函数在数学中的含义:

函数为两集合间的一种对应关系：输入值集合中的每项元素皆能对应唯一一项输出值集合中的元素。

例如，我们假设一个函数 f 定义了这样一种关系:

f(1) = A
f(2) = B
f(3) = C

输入集合是 {1, 2, 3}，输出集合是 {A, B, C}。如果输入 1，函数总是返回 A。

相反，这样不是一个合法函数：

f(1) = X
f(1) = Y
f(2) = Z

这不满足函数的定义中唯一一项的要求。

这样是合法函数吗：

f(1) = A
f(2) = A
f(3) = A

是合法的。不同的输入可以返回相同的输出。

我们知道，在函数式编程中有个概念叫 纯函数。是说，

此函数在相同的输入值时，需产生相同的输出。函数的输出和输入值以外的其他隐藏信息或状态无关，也和由I/O设备产生的外部输入无关。

该函数不能有语义上可观察的函数副作用，诸如输出到I/O设备，或更改输出值以外可变对象的内容等。

第一点和数学上函数的定义是一致的。带副作用的函数中，输出可能依赖于全局变量或函数外的变量，或者从I/O获取数据，都有可能导致同样的输入返回不同的输出。这不满足数学上函数的定义。

图灵完备 (Turing completeness)

世界上存在各种各样的编程语言，有各种各样的特性。很多语言特性的存在其实只是为了方便 (语法糖)：

多参数函数
```
foo(a, b, c)
```
解决办法：科里化 (Currying) 或元组 (Tuple)
循环
```
while (a < b) ...
```
解决办法：递归 (Recursion)

那么，什么样的语言特性是真正需要的？换句话说，没有这个特性，这个语言就不叫语言呢？

我们用过很多语言，比如汇编，C, Objective-C, Java, Swift, Kotlin, PHP, HTML/CSS 等。有两个比较流行的观点：

一个问题，如果可以用 Java 解决，那么用 C，Swift，甚至汇编都能解决，只是哪个语言更方便的区别。
有些 Java 能解决的问题，HTML/CSS 不能解决。Java 和 HTML/CSS 的区别在哪里？

上个世纪30年代艾伦·图灵思考，能不能造一个机器，模拟计算人类所能进行的任何计算过程？这就是 图灵机 。然后图灵又提出了 通用图灵机 的概念，即接受任意一个图灵机的编码，然后模拟其运作。现代电子计算机 (冯·诺伊曼结构) 其实就是这样一种通用图灵机，它能接受一段描述其他图灵机的程序，并运行程序实现该程序所描述的算法。

图灵完备：一个可以计算所有图灵机可计算的计算系统被称为图灵完备的。换句话说就是一个可以模拟通用图灵机的系统。

汇编，C，Java 等编程语言都是 图灵完备 的。而他们之间也是 图灵等价 的，即他们之间可以相互模拟，他们的计算能力与通用图灵机的计算能力相同。

能不能有一个语言，特性越少越好，但仍满足图灵完备？换句话说，可以模拟通用图灵机，亦可以模拟所有的图灵完备的编程语言？

𝜆演算就是这样一种语言。

1. 𝜆演算简介

𝜆 演算（英语：lambda calculus，𝜆-calculus）是一套用于研究函数定义、函数应用和递归的形式系统。它由阿隆佐·邱奇 (Alonzo Church) 和他的学生斯蒂芬·科尔·克莱尼 (Stephen Cole Kleene) 在20世纪30年代引入。邱奇运用𝜆演算在1936年给出判定性问题（Entscheidungsproblem）的一个否定的答案。这种演算可以用来清晰地定义什么是一个可计算函数。关于两个 𝜆 演算表达式是否等价的命题无法通过一个“通用的算法”来解决，这是不可判定性能够证明的头一个问题，甚至还在停机问题之先。𝜆 演算对函数式编程语言有巨大的影响，比如 Lisp 语言、ML 语言和 Haskell 语言。 𝜆 演算可以被称为最小的通用程序设计语言。它包括一条变换规则（变量替换）和一条函数定义方式，𝜆 演算之通用在于，任何一个可计算函数都能用这种形式来表达和求值。因而，它是等价于图灵机的。尽管如此，𝜆 演算强调的是变换规则的运用，而非实现它们的具体机器。可以认为这是一种更接近软件而非硬件的方式。

2. 𝜆 演算的定义

𝜆 演算只有三种基本成员，或称为 项 (terms): 表达式 (expressions)，变量 (variables)，抽象 (abstraction)。

表达式是这三个东西的超集：一个表达式可以是一个变量名字，可以是一个抽象，也可以是这些东西的组合。表达式的定义：

e ::= x           // variable
  | 𝜆x.e          // abstraction
  | e e′          // abstraction application

变量仅仅是一个名字，用来指代抽象可能的输入。
抽象是纯函数，也是数学定义上的函数。以下我们都把抽象称为函数。函数包括一个头部 (head) 和一个体 (body)，如：

𝜆 x . x
^─┬─^
  └────── 函数头部

𝜆 x . x

  ^────── 函数参数，与函数体中每一个同样名字的变量绑定。

𝜆 x . x

      ^── 函数体，当函数被应用时就会返回这个表达式。这里 `x` 是绑定变量 (bound variable)。

头部中的变量为函数的参数 (parameter)，与函数体中相同的变量绑定。意思是：当我们应用 (apply) 函数到一个参数上去，函数体中每一个变量的值都为这个参数的值。

总结起来，𝜆 演算中所有东西都是函数。函数的应用 e e′ 中，e 是被应用的函数，参数 e′ 也是函数。变量 x 不过是函数中的变量。

自由变量 (Free variables)

𝜆x.e 这个句法构造 (syntactic construct) 把变量 x 绑定 (binds) 在了表达式 e。𝜆 表达式中的变量，如果不是自由的 (free) 那么它就是被约束的 (bound)。

如果一个变量属于如下递归定义的 FV(e) 集合，那么它就是自由的：

FV(e) = FV(e1) union FV(e2)  if e = e1 e2
FV(e) = FV(e1) \ {x}  if e = 𝜆x.e1
FV(e) = {x}  if e = x

举例：

FV(x)={x}
FV((x (y x)))={x,y}
FV((𝜆x.(x y))={y}

β-规约 (Beta reduction)

𝜆 演算最纯粹的形式中，不存在内置的常量和操作，包括数字，算术运算，条件，记录，循环，I/O等。当我们谈论“计算”时我们在谈论应用函数到参数上 (参数也是函数)。计算中的每一步都是这样的，左边是一个函数，右边是参数，把左边函数体中的绑定变量替换 (substitute) 为右边的参数，然后去掉头部。这个过程叫 β-规约。

比如有函数：

𝜆𝑥.𝑥

我们使用数字来做β-规约 (通常的数字概念，在 𝜆 演算中是不存在的。但是后面我们会找到一种方法来推导出数字的概念)。我们应用这个函数到数字 2，即把函数体中每一个绑定变量都替换为 2，然后去掉函数头：

(𝜆𝑥.𝑥) 2
2

这个函数叫 恒等函数 (identity function)。

我们也可以应用我们的恒等函数到另一个函数：

(𝜆𝑥.𝑥)(𝜆𝑦.𝑦)

这里我们引入一个新的语法，[𝑥 ∶= 𝑧]，来表示所有的 x 会被替换为 z。(在这里，z 为函数 (𝜆𝑦.𝑦))。做β-规约如下：

(𝜆𝑥.𝑥)(𝜆𝑦.𝑦)
[𝑥 ∶= (𝜆𝑦.𝑦)]
𝜆𝑦.𝑦

(𝜆x. e’) e 这种形式的项是 可规约表达式 (reducible expression，丘齐称其为 redex)。我们可以对其做β-规约。

一个项如果不能再被β-规约，我们称它为 规范型 (normal form)。而有一些项永远都不能被求值为规范型，被称为 发散的 (diverge)。

静态作用域和α-转换 (Static scoping & Alpha Conversion)

𝜆演算使用静态作用域。

而采用静态作用域的语言中，基本都是最内嵌套作用域规则：由一个声明引进的标识符在这个声明所在的作用域里可见，而且在其内部嵌套的每个作用域里也可见，除非它被嵌套于内部的对同名标识符的另一个声明所掩盖。为了找到某个给定的标识符所引用的对象，应该在当前最内层作用域里查找。如果找到了一个声明，也就可以找到该标识符所引用的对象。否则我们就到直接的外层作用域里去查找，并继续向外顺序地检查外层作用域，直到到达程序的最外嵌套层次，也就是全局对象声明所在的作用域。如果在所有层次上都没有找到有关声明，那么这个程序就有错误。

我们考虑这样一个表达式：

(𝜆x.x (𝜆x.x)) z → ?

第二个 x 是第一个绑定，最右边的 x 是第二个绑定。第一个绑定中的 x 被第二个绑定给 遮蔽 (shadow) 了。

对函数 𝜆𝑥.𝑥 来说，变量 x 没有语义上的意义。项之间存在一种等价形式叫 α-等价 (Alpha equivalence)，如：

𝜆𝑥.𝑥
𝜆𝑑.𝑑
𝜆𝑧.𝑧

都是相同的函数。称他们是α-等价的。

把一个𝜆项转换成另一种α-等价的项，叫做 α-转换。如把 𝜆𝑥.𝑥 α-转换成 𝜆𝑑.𝑑，写作 [𝑥/𝑑]。

又如:

𝜆y.𝜆x.y [y/z] = 𝜆z.𝜆x.z

α-转换的本质是对处于同一个绑定内的相同名字的变量做集体换名。如：

(𝜆y.y (𝜆y.y)) [y/z] = 𝜆z.z (𝜆y.y)

替换 (Substitution)

β-规约的核心是替换，我们递归定义替换过程：

1. x[x:=e] = e
2. y[x:=e] = y
3. (e1 e2)[x:=e] = (e1[x:=e]) (e2[x:=e])
4. (𝜆x.e’)[x:=e] = 𝜆x.e’
5. (𝜆y.e’)[x:=e] = ?

解释一下第 4 点，在 𝜆x.e’ 中，x 是参数，根据静态作用域的概念，这是一个 局部变量 (local variable)，和其外层的函数中的 x 是不一样的。举例：

(𝜆x.x (𝜆x.e’)) e
(x (𝜆x.e’)) [x:=e]
(x[x:=e] (𝜆x.e’)[x:=e])
(e (𝜆x.e’))

问题：第 5 点是 𝜆y.(e’[x:=e]) 吗？不是。

变量捕捉 (Variable capture)

(𝜆x.𝜆y.x y) y → ?

当我们把 y 替换进去时，我们不想让它被内层的 y 的绑定捕捉 (captured)，这样破坏了静态作用域。如：

(𝜆x.𝜆y.x y) y ≠ 𝜆y.y y

解决办法：使用α-转换重命名内层的绑定。

(𝜆x.𝜆y.x y) y
(𝜆x.𝜆y.x y)[y/z] y
(𝜆x.𝜆z.x z) y
𝜆z.y z

完成替换的定义

重回替换定义的第 5 点：

(𝜆y.e’)[x:=e]

我们想避免把 e 中的自由出现 (free occurrences) 的 y 被绑定。

解决方法就是α-转换：

把 y 替换为变量 w，w 既没有出现在 e’ 中，也没有出现在 e 中。 w 被称为新鲜的 (free)。
把 e’ 中所有的 y 都替换为 w。
把 e’ 中所有的 x 替换为 e。

形式化地描述：

(𝜆y.e’)[x:=e] = 𝜆w.((e’[y:=w]) [x:=e]) (w is fresh)

求值策略

𝜆演算有多种求值策略，策略定义了项中哪一个 redex 可以在下一步被规约。我们列举几个：

完全规约 (full reduction)

任意 redex 可以在任意时间被规约。在任意一步我们都可以选取任意 redux 来规约。举例，有这样的项

(𝜆x.x) ((𝜆x.x) (𝜆z. (𝜆x.x) z))

或者我们可以写的更具可读性 id (id (𝜆z. id z))。这个项包含3个redex：

id (id (𝜆z. id z))
------------------

id (id (𝜆z. id z))
   ---------------

id (id (𝜆z. id z))
            ----

我们可以按任意顺序规约，比如先最里面的redex，然后是中间的，最后是最外层的：

  id (id (𝜆z. id z))
            ----
→ id (id (𝜆z. z))
     ------------
→ id (𝜆z. z)
  ----------
→ 𝜆z. z

规范序规约(normal order reduction)

最左边的，最外层的redex总是最先被规约。按照这种顺序，上面的例子：

  id (id (𝜆z. id z))
  ------------------
→ id (𝜆z. id z)
  -------------
→ 𝜆z. id z
      ----
→ 𝜆z. z

传名调用(call by name)

传名调用比上面两个更受限，不允许在函数内部做规约。如：

  id (id (𝜆z. id z))
  ------------------
→ id (𝜆z. id z)
  -------------
→ 𝜆z. id z

这里把 𝜆z. id z 当做一个规范型 (即不能再被规约)。

传名调用有很多种变体，而 Haskell 使用了一种更优化的变体叫 传需求调用(call by need)，即不用每次都去对参数求值，而是把参数第一次求值时的值记下来，然后以后的调用都直接替换为这个值。

传值调用(call by value)

这是大多数语言采用的求值策略，是只有最外侧的redex会被规约，一个redex要被规约前，他右边的值必须已经被规约到一个值(value) (值无法再继续被规约，在𝜆演算中即规范型的项，而在其他语言中，可能是数字，布尔值，字符串，元组，字典，列表等)。举例：

  id (id (𝜆z. id z))
     ---------------
→ id (𝜆z. id z)
  -------------
→ 𝜆z. id z

我们称传值调用是 严格的(strict)，意味着函数的参数总是被求值，不管是否会不会被函数体用到。相反，传名调用和传需求调用是 非严格的(non-strict)，也称作 惰性的(lazy)，只有在参数被用到时才会去求值。

多参数 (Multiple arguments)

每一个 lambda 函数只能绑定一个参数，也只能接受一个参数。如果要实现多参数呢？可以用多个嵌套的函数头来实现。当应用多参数函数时，首先第一个 (最左边) 函数头被去掉，然后是第二个函数头，依次下去。这个方法最早是Moses Schönﬁnkel(俄罗斯的逻辑学家和数学家，在哥廷根大学做研究，发明了组合逻辑) 和戈特洛布·弗雷格 (Gottlob Frege，德国的逻辑学家，数学家和哲学家，数理分析和分析哲学的奠基人) 于 20 世纪 20 年代发现的，然后被哈斯凯尔·科里 (Haskell Curry) 重新发现。通常称为 科里化 (Currying)。

举例：

𝜆𝑥𝑦.𝑥𝑦

是两个嵌套的函数的简写：

𝜆𝑥.(𝜆𝑦.𝑥 𝑦)

当应用第一个参数时会绑定 x，然后消除外层的函数，得到 𝜆𝑦.𝑥𝑦，其中 x 为外层函数参数绑定的值。

3. 邱奇编码 ([Church encoding])

𝜆 演算是图灵完备的，意味着，我们可以用 𝜆 演算来编码任意计算，包括：

布尔值 (Booleans)
序对 (Pairs)
自然数及算术 (Natural numbers & arithmetic)
循环 (Looping)

布尔值

对基本的布尔值我们可以编码成：

true = 𝜆x.𝜆y.x
false = 𝜆x.𝜆y.y

即 true 是一个接受两个参数的函数，返回第一个参数，false 也是一个接受两个参数的函数，返回第二个参数。

那么我们想编码条件判断 if 表达式，可以这样

if a then b else c = a b c

例如：

if true then b else c
(𝜆x.𝜆y.x) b c
(𝜆y.b) c
b

习题：

if false then b else c = ?

对于取反操作 not 我们可以编码成：

not = 𝜆x.x false true

可以解释为：

not x = if x then false else true

举例：

not true
(𝜆x.x false true) true
true false true
false

对于与操作 and 我们可以编码成：

and = 𝜆x.𝜆y.x y false

可以解释为：

and x y = if x then y else false

对于或操作 or 我们可以编码成：

or = 𝜆x.𝜆y.x true y

可以解释为：

or x y = if x then true else y

序对

我们可以把序对 a, b 编码成：

(a, b) = 𝜆x.if x then a else b
fst = 𝜆f.f true
snd = 𝜆f.f false

例子：

fst (a, b)
(𝜆f.f true) (𝜆x.if x then a else b)
(𝜆x.if x then a else b) true
if true then a else b
a

习题：

snd (a, b) = ???

自然数 (Natural Numbers, 或称丘奇数 Church Numerals)

我们可以把非负数编码如下:

0 = 𝜆s.𝜆z.z
1 = 𝜆s.𝜆z.s z
2 = 𝜆s.𝜆z.s (s z)
3 = 𝜆s.𝜆z.s (s (s z))
...
n = 𝜆s.𝜆z.<apply s n times to z>
n + 1 = 𝜆s.𝜆z.s (n s z)

有的丘奇数都是带有两个参数的函数，对于任何数 n，它的丘奇数是将其第一个参数应用到第二个参数上 n 次的函数。

一个很好的理解办法是将 z 作为是对于零值的命名，而 s 作为后继函数的名称。因此，0 是一个仅返回零值的函数，1 是将后继函数运用到零值 1 次的函数；2 则是将后继函数应用到零值的后继上的函数，以此类推。

后继 (Successor)

succ = 𝜆n.𝜆s.𝜆z.s (n s z)

n 为丘齐数，我们可以把 s 和 z 作为参数传给 n，然后显式地对结果再应用 1 次 s，最终得到一个函数，函数中 s 应用到 z 的次数比 n 多 1 次，这正是丘齐数 n+1，即 n 的后继。

举例求 0 的后继：

succ 0 =
(𝜆n.𝜆s.𝜆z.s (n s z)) (𝜆s.𝜆z.z)
𝜆s.𝜆z.s ((𝜆s.𝜆z.z) s z)
𝜆s.𝜆z.s ((𝜆z.z) z)
𝜆s.𝜆z.s z
= 1

IsZero?

iszero = 𝜆z.z (𝜆y.false) true

iszero 0 =
(𝜆z.z (𝜆y.false) true) (𝜆s.𝜆z.z)
(𝜆s.𝜆z.z) (𝜆y.false) true
(𝜆z.z) true
true

加法 (Addition)

M + N = 𝜆s.𝜆z.M s (N s z)

写成 4 个参数的形式:

+ = 𝜆M.𝜆N.𝜆s.𝜆z.M s (N s z)

加法是接受两个丘齐数 M 和 N，返回另一个丘齐数，这个丘齐数是这样一个函数，接受参数 s 和 z，把 s 应用到 z n

举例：

1 + 1 =
𝜆s.𝜆z.(1 s) ((1 s) z)
𝜆s.𝜆z.((𝜆s.𝜆z.s z) s) ((1 s) z)
𝜆s.𝜆z.(𝜆z.s z) ((1 s) z)
𝜆s.𝜆z.s ((1 s) z)
𝜆s.𝜆z.s (((𝜆s.𝜆z.s z) s) z)
𝜆s.𝜆z.s ((𝜆z.s z) z)
𝜆s.𝜆z.s (s z)
= 2

乘法 (Multiplication)

乘法的定义为，加法的连续运算，即同一数的若干次连加，所以可以利用我们定义好的 + 来定义乘法：

M * N = M (+ N) 0

写成函数的形式:

* = 𝜆M.𝜆N.M (+ N) 0

这里用科里化的思想比较好理解。因为函数 + 可以看做接受两个参数然后返回其和的函数，那么传入一个参数 N 后会自然地得到另一个函数 + N，这个函数接受一个参数，返回结果是对这个参数加上 N。所以把函数 + N 作为 M 的第一个参数，0 作为第二个参数，意思是 “重复应用这个对参数加 N 的函数 M 次到 0 上”，即 “对 N 连加 M 次”。

也可以不用 + 的定义，写作：

* = 𝜆M.𝜆N.𝜆s.𝜆z.M (N s) z

列表 (List)

我们可以用𝜆演算的函数 fold (或 reduce) 来表示列表。如 [x, y, z]，可以表示为一个函数，这个函数接受两个参数 c 和 n，返回 c x (c y (c z n)))。

我们定义函数 cons，接受一个元素 h 和一个列表 t (即一个 fold 函数)，返回一个和 t 类似的列表，只是把 h 加在了 t 的最前面：

cons = 𝜆h.𝜆t.𝜆c.𝜆n.c h (c t n)

我们回顾 true 和 false 的定义：

true = 𝜆x.𝜆y.x
false = 𝜆x.𝜆y.y

我们定义空列表 nil：

nil = false

定义函数 isnil，接受一个参数为列表，判断列表是否为空：

isnil = 𝜆l.l (𝜆x.𝜆y.false) true

定义函数 head，接受一个参数为列表，取列表的第 1 项，如果列表为空则返回 nil：

head = 𝜆l.l true false

举例，有列表 l = cons 1 (cons 2 nil)：

isnil l =
(𝜆l.l (𝜆x.𝜆y.false) true) (𝜆c.𝜆n.c 1 (c (cons 2 nil) n))
(𝜆c.𝜆n.c 1 (c (cons 2 nil) n)) (𝜆x.𝜆y.false) true
(𝜆n.(𝜆x.𝜆y.false) 1 ((𝜆x.𝜆y.false) (cons 2 nil) n)) true
(𝜆x.𝜆y.false) 1 ((𝜆x.𝜆y.false) (cons 2 nil) true)
false

isnil nil =
(𝜆l.l (𝜆x.𝜆y.false) true) false
false (𝜆x.𝜆y.false) true
(𝜆x.𝜆y.y) (𝜆x.𝜆y.false) true
true

稍微总结

个人觉得丘齐编码最酷的地方在于，只用函数这一个东西就能定义出各种计算的对象，如序对，布尔值，自然数。或者进一步说，这些对象其实就是计算。如布尔值 true 的定义为函数 𝜆x.𝜆y.x，解释出来就是，一个接受 2 个参数返回第 1 个参数的函数。相应地，布尔值 false 的定义是一个接受 2 个参数返回第 2 个参数的函数。由于布尔值是函数，而函数可以被应用，那么可以直接应用函数 true 和 false 来实现常用的条件计算，即 if ... then ... else ...。类似序对，自然数及其上的运算都是类似的实现。

循环和递归 (Looping & Recursion)

如果一个 lambda 项中没有自由变量，我们说这个项是封闭的 (closed)。一个封闭的项也称为 组合子。如恒等函数 𝜆x.x。

我们之前提过，有一些项永远都不能被求值为规范型，即会一直求值下去，被称为发散的，比如我们定义组合子 D = 𝜆x. x x:

D D =
(𝜆x. x x) (𝜆x. x x)
(𝜆x. x x) (𝜆x. x x)
...
= D D

D D 是一个无限循环。

对于一个图灵完备的语言来说，循环必不可少。在函数式语言中一般用递归来实现循环。如阶乘函数的定义：

factorial(n) = 1 if n = 0
factorial(n) = n * factorial(n-1) if n > 0

但是在𝜆演算中，我们只有匿名函数。我们没有办法通过引用一个函数的名字来递归调用它。那么怎么办呢？

不动点组合子 (The Fixpoint Combinator)

不动点组合子也叫 Y 组合子，定义如下：

Y = 𝜆f.(𝜆x.f (x x)) (𝜆x.f (x x))

有：

Y F =
(𝜆f.(𝜆x.f (x x)) (𝜆x.f (x x))) F
(𝜆x.F (x x)) (𝜆x.F (x x))
F ((𝜆x.F (x x)) (𝜆x.F (x x)))
= F (Y F)

可以看出不动点组合子是发散的。

Y F 叫做 F 的不动点 (fixed point)。

因此有

Y F = F (Y F) = F (F (Y F)) = ...

我们可以用不动点组合子实现递归调用。

例如阶乘函数定义：

fact = 𝜆f.𝜆n.if n = 0 then 1 else n * (f (n-1))

fact 的第二个参数是整数，第一个参数是在函数体中调用的函数。

那么有：

(Y fact) 1 = (fact (Y fact)) 1
→ if 1 = 0 then 1 else 1 * ((Y fact) 0)
→ 1 * ((Y fact) 0)
→ 1 * (fact (Y fact) 0)
→ 1 * (if 0 = 0 then 1 else 0 * ((Y fact) (-1))
→ 1 * 1
→ 1