无类型 λ 演算与重写系统

本文讨论 Alonzo Church 发明的无类型 λ 演算（λ-calculus）。这是一个类型论与计算理论的基础模型。

本站提供了一个在线演绎器，其中使用 @eval 命令仅会使用 β-归约按正则次序进行求值，使用 @simp 会额外尝试使用 η-等价进行简化。输出使用 de Brujin 无名表示（#i 表示从里到外第 $i$ 层函数声明对应的参数）。想要自行编写解释器的读者可参考其仓库 Rratic/my-lam.

语法

一个 λ-表达式被递归定义为有限次使用以下规则得到的表达式：

• 变量名是 λ-表达式，如 $x$
• 函数声明是 λ-表达式，写作 $\lambda x.\ E$，其中 $x$ 是变量名，表示参数；$E$ 是 λ-表达式，表示函数体，理解为创建了一个匿名的函数，满足 $f(x) = E$
• 函数应用是 λ-表达式，写作 $E_1\ E_2$，其中 $E_1, E_2$ 都是 λ-表达式，理解为把 $E_1$ 作用于 $E_2$，即一般语境所说的 $E_1(E_2)$

写成形式文法即：

E = x           // variables
  | λx. E       // function creation (abstraction)
  | E1 E2       // function application

一些简单的例子：

• 恒等函数 $\lambda x.\ x$
• 返回恒等函数的函数 $\lambda y.\ (\lambda x.\ x)$ 这里的 $y$ 参数被忽略了，引入参数而不使用它是被允许的
• 表示复合的函数 $\circ = \lambda g.\ \lambda f.\ \lambda x.\ g\ (f\ x)$

在书写时，常常省略括号。对此的惯例是：

• 函数声明时，函数体尽可能向右扩展
• 函数应用时，从左到右结合（即“左结合”）

例如，$\lambda x.\ x\ \lambda y.\ x\ y\ z$ 应被理解为 $\lambda x.\ (x\ \lambda y.\ ((x\ y)\ z))$.

Currying

尽管在定义中，函数有且仅有一个参数，多个参数的函数仍然可以通过 currying 技术间接地表示。即，一般语境所说的 $f(x, y) = x + y$ 应被表达为：

$$f = \lambda x.\ (\lambda y.\ x + y)$$

对上述 $f$，你可以传入少于全部参数个数的参数。例如代入 $g = f\ 1$ 将得到 $g = \lambda y.\ 1 + y$，这也是一个可用的函数。

求值

替换

在 $\lambda x.\ M$ 中，$\lambda x$ 称为约束器，$M$ 是它的辖域。函数体 $M$ 中由这一层 $\lambda x$ 约束的 $x$ 称为约束出现；不受任何约束器约束的变量出现称为自由出现。例如在 $\lambda x.\ x\ y$ 中，$x$ 是约束出现的，而 $y$ 是自由出现的。

若变量 $x$ 在表达式 $M$ 中有自由出现，则称 $x$ 是 $M$ 的自由变量；若 $x$ 由 $M$ 中的某个函数声明引入，则称 $x$ 是 $M$ 的约束/哑变量（bound/dummy variable）。分别记二者的集合为 $\mathrm{FV}(M)$ 与 $\mathrm{BV}(M)$，递归地定义：

$$ \begin{aligned} \mathrm{FV}(x) &= \set{x}, \cr \mathrm{FV}(M\ N) &= \mathrm{FV}(M) \cup \mathrm{FV}(N), \cr \mathrm{FV}(\lambda x.\ M) &= \mathrm{FV}(M) \setminus \set{x}, \cr \mathrm{BV}(x) &= \varnothing, \cr \mathrm{BV}(M\ N) &= \mathrm{BV}(M) \cup \mathrm{BV}(N), \cr \mathrm{BV}(\lambda x.\ M) &= \mathrm{BV}(M) \cup \set{x}. \end{aligned} $$

记 $M[N/x]$ 为在 $M$ 中用 $N$ 替换 $x$ 的所有自由出现的结果。替换沿表达式的结构递归进行：

$$ \begin{aligned} x[N/x] &= N, \cr y[N/x] &= y && (y \neq x), \cr (M\ P)[N/x] &= M[N/x]\ P[N/x], \cr (\lambda x.\ M)[N/x] &= \lambda x.\ M, \cr (\lambda y.\ M)[N/x] &= \lambda y.\ M[N/x] && (y \neq x,\ y \notin \operatorname{FV}(N)). \end{aligned} $$

最后一种情形中，若 $y \in \mathrm{FV}(N)$，直接替换会使 $N$ 中自由出现的 $y$ 被 $\lambda y$ 捕获（capture）。此时先取一个在 $M, N$ 中均未出现且不同于 $x$ 的变量 $z$，将约束变量 $y$ 重命名为 $z$，再进行替换：

$$(\lambda y.\ M)[N/x] = \lambda z.\ M[z/y][N/x]$$

例如，若直接计算 $(\lambda y.\ x)[y/x]$，会错误地得到 $\lambda y.\ y$；正确做法是先重命名约束变量，从而得到 $(\lambda z.\ x)[y/x] = \lambda z.\ y$。这种不改变自由变量约束关系的替换称为捕获规避替换（capture-avoiding substitution）。

求值规则

求值规则包括：

• $\alpha$-重命名，在避免变量捕获的前提下改变约束变量名。例如 $\lambda x.\ x\ (\lambda x.\ x)$ 可重命名为 $\lambda x.\ x\ (\lambda y.\ y)$；一般地，若 $y \notin \operatorname{FV}(M)$，则 $\lambda x.\ M$ 与 $\lambda y.\ M[y/x]$ 是 $\alpha$-等价的
• $\beta$-归约（reduction），在应用时将实参代入函数体，即 $(\lambda x.\ M)\ N \to_\beta M[N/x]$，例如 $(\lambda x.\ x)\ (\lambda y.\ y)\to_\beta\lambda y.\ y$
• $\eta$-归约，若 $x \notin \operatorname{FV}(M)$，则 $\lambda x.\ M\ x \to_\eta M$；两者对任意参数具有相同的作用，因而也称 $\eta$-等价

这三者均可称为转换（conversion）。

组合子

类似于 λ-演算但有所不同，组合子希望不使用变量来描述函数：

  S K K
= λz. K z (K z)
= λz. z
= I

使用这些组合子可以一般地表达 Lambda 表达式，因为：

• $\lambda x.\ x$ 可写为 $I$
• $\lambda x.\ A$ 其中 $A$ 不含有 $x$ 可写为 $K\ A$
• $\lambda x.\ A\ B$ 可写为 $S\ (\lambda x.\ A)\ (\lambda x.\ B)$

求值顺序

考虑函数应用 $(\lambda y.\ (\lambda x.\ x)\ y)\ E$，它有两种计算方法：

• 先求内层，得到 $(\lambda y.\ y)\ E$，然后得到 $E$
• 先求外层，得到 $(\lambda x.\ x)\ E$，然后得到 $E$

一般来说，有如下几种常用的不同计算方式：

一种是在函数应用前先计算函数参数的值，称为应用次序（Applicative Order），在实际语言中对应 call-by-value / eager evaluation；另一种是不预先计算实参，代入函数体后在需要时求值，通常称为 call-by-name；加上共享可实现 call-by-need / lazy evaluation.

每次归约最左最外的归约式的策略称为正则/标准次序（Normal Order）。如果表达式可以被归约到正规形式，那么标准次序总是能成功归约¹，使用应用次序则可能陷入无限递归。

不动点

不动点组合子

事实上，对一般的函数 $f$，我们都可以找到不动点，此不动点与该函数的结构无关。

可以参阅此文章的启发式推导。大意如下：

我们希望有一个一般的方法找到 $p$ 使得 $p = f\ p$，让 $p = Y\ f$，即 $Y\ f = f\ (Y\ f)$.

可以看出 $p = Y\ f$ 展开后为形如无穷列 $f\ f\ f\ f\cdots$，不妨将该无穷列看成两段 $G\ G$，有 $G\ G = f\ (G\ G)$，可以看出一个构造 $G = \lambda x.\ f\ (x\ x)$.

从而我们找到了如下 Y 组合子：

$$Y = \lambda f.\ (\lambda x.\ f\ (x\ x))\ (\lambda x.\ f\ (x\ x))$$

不难验证：

  Y f
= (λx. f (x x)) (λx. f (x x))
= f ((λx. f (x x)) (λx. f (x x)))
= f (Y f)

递归

Y 组合子可以用于实现递归。

如果我们希望定义一个递归函数，伪代码： $$f = \lambda \mathrm{fact}.\ \lambda n.\ \begin{cases} 1 & n < 2 \cr n\times \mathrm{fact}(n-1) & \text{otherwise} \end{cases}$$

那么，若使用正则次序，可得到正确的结果。

  Y f 2
= f (Y f) 2
= 2 × (Y f 1)
= 2 × (f (Y f) 1)
= 2 × 1

但使用应用次序，则会造成无限递归。

  Y f 2
= f (Y f) 2
= f (f (Y f)) 2
= f (f (f (Y f))) 2
= ...

此时需改用 Z 组合子，将参数改造成延迟求值的。

$$Z = \lambda f.\ (\lambda x.\ f\ (\lambda y.\ (x\ x)\ y))\ (\lambda x.\ f\ (\lambda y.\ (x\ x)\ y))$$

这是因为在应用次序中有：

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

从而：

  Z f 2
= f (λy. (Z f) y) 2
= 2 × (λy. (Z f) y 1)
= 2 × (Z f 1)
= 2 × (f (λy. (Z f) y) 1)
= 2 × 1

类型模拟

无类型 λ 演算中只有函数而没有纯粹的、实践中关心的数据类型，不过我们可以用函数来间接地表达它们。

布尔值

布尔值支持二元逻辑运算，但其最重要的意义是实现条件判断。

我们可以简单地定义 true 为 $\lambda x.\ \lambda y.\ x$，false 为 $\lambda x.\ \lambda y.\ y$. 这样，if e then u else v 就可被重写为 $e\ u\ v$.

自然数

自然数可以被 Peano 公理所描述。其核心是，存在起点 0，并且每个自然数都有其后继。

在 Lambda 演算中，我们可以这样定义：

$$\mathrm{iszero}\ n = n\ (\lambda b.\ \mathrm{false})\ \mathrm{true}$$ $$0 = \lambda f.\ \lambda s.\ s$$ $$1 = \lambda f.\ \lambda s.\ f\ s$$ $$2 = \lambda f.\ \lambda s.\ f\ (f\ s)$$

……诸如此类。自然数的信息被表现在 $f$ 的层叠数目上，对其计算只需用 $s$ 给出的接口添加层叠数即可。

$$\mathrm{succ}\ n = \lambda f.\ \lambda s.\ f\ (n\ f\ s)$$ $$\mathrm{add}\ n_1\ n_2 = n_1\ \mathrm{succ}\ n_2$$ $$\mathrm{mult}\ n_1\ n_2 = n_1\ (\mathrm{add}\ n_2)\ 0$$

举个例子：

  add 0
= (λn₁. λn₂. n₁ succ n₂) 0
= λn₂. 0 succ n₂
= λn₂. n₂
= λx. x

又如：

  add 1 1
= 1 succ 1
= succ 1
= λf. λs. f (f s)
= 2

Church 进一步构造了判定自然数是否相等的函数，从而能够编码 Diophantus 方程。²

列表

构造基于这一思想：将“如何遍历列表”的问题放到使用列表时。

let nil = λc. λn. n // 空列表

// h 表示在开头添加的元素
// t 是之后的列表部分
let cons = λh. λt. λc. λn. c h (t c n)

cons 1 (cons 2 (cons 3 nil)) // 构造列表示例
// = λc. λn. c 1 (λc. λn. c 2 (λc. λn. c 3 (λc. λn. n)))

重写系统

术语

重写是将表达式的一部分替换为其它表达式的过程，可以看作一种关系或者一组规则，在这里，规则包括 $\alpha, \beta, \eta$ 三种归约。

在此之上，重写系统是由一个表达式的集合和表达式到表达式之间的重写关系组成的结构，类似于有向图。我们记表达式的集合 $E$，重写关系 $(\to) \subset E\times E$.

用 $\stackrel \ast \to$ 表示将 $\to$ 应用任意自然数次的版本。用双向箭头 $\stackrel \ast \leftrightarrow$ 表示两边都可的版本。

正规性

对于重写系统 $E$ 和 $a \in E$，如果不存在 $b$ 使 $a \to b$，那么 $a$ 是一个正规形式/既约形式。因此 Ω 组合子虽然满足 $\Omega \stackrel{\ast}{\to} \psi \iff \psi = \Omega$，却不是正规形式。

若重写系统中任意表达式都能通过某个特定的顺序重写为正规形式，那么该重写系统是弱正规/弱停机的。

若重写系统中任意表达式都能通过任意顺序重写为正规形式，那么该重写系统是强正规/强停机的。

合流性

若对于重写系统 $E$ 和任意 $a, b, c \in E$，一旦成立 $b \stackrel \ast \gets a \stackrel \ast \to c$，就存在 $d$ 使得 $b \stackrel \ast \to d \stackrel \ast \gets c$，那么 $E$ 是合流的。

$$ \begin{CD} a @>\ast>> b \cr @V\ast VV @VV\ast V \cr c @>>\ast> d \end{CD} $$

参考了文献 D. Kozen/Church–Rosser Made Easy³ 列举的其它证明方式。其本身的证明包含了过多未声明含义的术语，且包含了今天看来不必要的步骤，例如，使用了包含序列的集合来定义树⁴，并混用术语。此外，你可以在此找到一个使用 Coq 形式化验证的证明。

以下将对证明思路进行摘要。

首先，α-等价关系的刻画是易完成的。只需考虑 β-归约，全体的合法 Lambda 表达式记作 $\omega = \omega^{\ast}/\sim _\alpha$.

一步 β-归约是之前定义的 $(\lambda x.\ a)\ b\to a[b/x]$。多步归约就是之前定义的 $\stackrel{\ast}{\to}$，我们重新记作 $\twoheadrightarrow$，它也可看作一步 β-归约的自反传递闭包。

证明中最大的难题是归约时，内部的可归约式结构可能被破坏。

为此，我们定义并行归约（parallel reduction），使用符号 $\Longrightarrow$ 标记，满足：

• $x\Longrightarrow x$
• 若 $M\Longrightarrow M'$ 则 $\lambda x.\ M\Longrightarrow \lambda x.\ M'$
• 若 $M\Longrightarrow M'$ 且 $N\Longrightarrow N'$ 则 $M\ N\Longrightarrow M'\ N'$
• 若 $M\Longrightarrow M'$ 且 $N\Longrightarrow N'$ 则 $(\lambda x.\ M)\ N\Longrightarrow M'[N'/x]$

容易证明并行归约是合流的。

而后，存在包含关系 $(\to)\subset(\Longrightarrow)\subset(\twoheadrightarrow)=(\stackrel{\ast}{\Longrightarrow})$ 其中最后一点可以分别说明两边的包含关系。

由此，λ 演算具有合流性。