Church 编码（和 Lambda 演算）
dove
2020-02-01 12:38:52
## 引入
Church 编码是一种“抽象方法”，它将“数字”、“运算”等概念全数“抽象”成 λ- 演算（别急着跑，会介绍什么是 λ- 演算的），来让程序实现更好的抽象性。换句话说，它将物件（布尔值、自然数、列表、etc）抽象为函数，并通过将公理的基本元素作为参数应用于其上来获得（依基本元素不同而不同的）值。
> **前置知识：[布尔代数](https://en.wikipedia.org/wiki/Boolean_algebra)，基础 Python，小学数学**
>
> - 这篇文章讲的东西，对 OI 有什么用吗？
> - 抱歉，几乎没有。如果您不想在 λ- 演算等抽象废话上浪费时间，现在就可以关闭本页面。
> - 你讲的真烂/你个初学者还写这种博客班门弄斧。
> - 请告诉我如何改进，或者自己写一篇吊打我。
> - 我学过 λ- 演算和 Haskell，想看更直接的介绍。
> - 可以[到这里看这篇文章的原始版本](https://t532.github.io/2020/01/21/church-encoding/)。不过真的有人会了这些还不会 Church encoding 吗...
## 前置知识：λ- 演算
λ- 演算可以算作最原始的编程语言。我们来通过几个例子了解一下它，每个例子都有对应的 Python 代码（不用 C++ 是因为 C++ 弄这种东西非常困难，不用 Haskell 是因为很多人看不懂）。注意，所有 Python 函数都用 `lambda` 表达式，这是为了更好地对应，[不会的可以学一下](https://www.liaoxuefeng.com/wiki/1016959663602400/1017451447842528)。
**p1. λ- 演算的函数声明**
所有 λ- 演算中的函数都接受且只接受一个参数。来看一个基本的函数：把参数加一。
$$ \lambda x . x + 1 $$
各个部分的意义：
|lambda 符号，相当于“函数声明关键字”|参数名|分隔符|函数体|
|-|-|-|-|
|$\lambda$|$x$|$.$|$x + 1$|
Python 里就是
```python
lambda x : x + 1
```
**p2. λ- 演算的函数调用**
函数调用没有括号。
$$ f = \lambda x . x + 1 $$
$$ a := 3 $$
$$ b := fa = 4. $$
```python
f = lambda x : x + 1
a = 3
b = f(a) # => 4.
```
λ- 演算的执行只有三条公理
- **$\alpha$- 等价**：$\lambda x. fx = \lambda y. fy$。
- **$\beta$- 归约**：$(\lambda x. fx)y = fy$。
- **$\eta$- 归约**：$(\lambda x. fx) = f$。
**p3. λ- 演算的高阶函数**
有些人可能有高阶函数的概念。高阶函数是“接受函数作为参数的函数”或者“返回函数的函数”。看一个例子。
```python
g = lambda x : lambda y: x + y
g(1)(2) # 1 + 2 => 3
```
这种函数一次只接受一个参数，返回等待接受下一个参数的函数，这个函数又返回接受下下个参数的函数...,这种函数叫做“柯里化函数”。
- 它可以被更容易地“部分应用”。部分应用就是说只给它传一部分参数：
```python
add1 = g(1)
add1(3) # 1 + 3 => 4
```
- λ- 演算的所有函数，事实上都是柯里化函数，也就是说它们只接受一个参数。
在 λ- 演算中也可以直接调用函数表达式
$$ (\lambda x. \lambda y. x + y) ab = (\lambda y. a + y) b = a + b. $$
```python
(lambda x : lambda y : x + y)(a)(b) # => a + b
```
函数接受的参数也可以是函数，比如
$$ (\lambda x. \lambda y. xy) ab = ab $$
```python
(lambda x : lambda y : x(y))(a)(b) # => a(b)
```
这里的 $a$ 只能是个函数。
> 有时候会见到 $\lambda xy.$这样的参数列表，它只是 $\lambda x. \lambda y.$ 的简写。
## Church 布尔代数
Church 布尔代数通过 Church 编码抽象了标准布尔代数，我们可以通过它来理解 Church 编码。
### 布尔值
考虑布尔代数的基本元素，即布尔值：
**公理 a1. 布尔值的集合**
$$ \mathbb{B} = \{ F, T \} $$
其中 $T$ 为逻辑真，$F$ 为逻辑假。
在 Church 布尔代数中，它们将会如此表示：
**定义 a1. Church 布尔代数中的布尔值**
$$ \operatorname{true} = \lambda tf.t $$
$$ \operatorname{false} = \lambda tf.f $$
可以认为 $t$ 与 $f$ 分别代表了抽象的逻辑真与逻辑假。
令 $t := T , f := F$，即将标准布尔代数的基本单位应用于 Church 布尔值后，其归约为（我们所想得到的）标准布尔代数值 - 这展示了标准布尔值和 Church 布尔值之间的关系：
$$ \operatorname{true} T F = T $$
$$ \operatorname{false} T F = F $$
**代码 a1.**
```python
true = lambda t : lambda f : t
false = lambda t : lambda f : f
```
### 取反
接下来考虑在标准布尔代数中的逻辑取反：
**公理 a2. 布尔值的取反**
$$ \neg T = F $$
$$ \neg F = T $$
不难想到，在 Church 布尔代数中，逻辑取反的定义：
**定义 a2. Church 布尔代数中的取反**
$$ \operatorname{neg} = \lambda x. \lambda tf. xft $$
我们颠倒了逻辑真与逻辑假，这就令原值归约为相反的值。
**代码 a2.**
```python
cnot = lambda x: lambda t: lambda f: x(f)(t)
```
### 逻辑与
**公理（定理）a3. 布尔代数中的逻辑与**
$$ T \land T = T $$
$$ T \land F = F $$
$$ F \land T = F $$
$$ F \land F = F $$
**定义 a3. Church 布尔代数中的逻辑与**
有两种理解方式：
$$ \operatorname{and} = \lambda xy. xyx $$
如果第一个值为假，那就直接得到结果，否则再判断第二个值是否为假。
$$ \operatorname{and} = \lambda xy. \lambda tf. x(ytf)f $$
将其中一个值（$x$）作为另一个值（$y$）的真值，若$x$为假，则$y$即使为真，最后仍归约为假。
**代码 a3.**
```python
cand = lambda x: lambda y: x(y)(x)
```
### 逻辑或
**公理（定理）a4. 布尔代数中的逻辑或**
$$ T \lor T = T $$
$$ T \lor F = T $$
$$ F \lor T = T $$
$$ F \lor F = F $$
**定义 a4. Church 布尔代数中的逻辑或**
有两种理解方式：
$$ \operatorname{or} = \lambda xy. xxy $$
如果第一个值为真，那就直接得到结果，否则再判断第二个值是否为真。
$$ \operatorname{or} = \lambda xy. \lambda tf. xt(ytf)$$
将其中一个值（$x$）作为另一个值（$y$）的假值，若$x$为真，则$y$即使为假，最后仍归约为真。
**代码 a4.**
```python
cor = lambda x: lambda y: x(x)(y)
```
### 逻辑异或
**公理（定理）a5. 布尔代数中的逻辑异或**
$$ T \oplus T = F $$
$$ T \oplus F = T $$
$$ F \oplus T = T $$
$$ F \oplus F = F $$
**定义 a5. Church 布尔代数中的逻辑异或**
有两种理解方式：
$$\operatorname{xor} = \lambda xy. x(\operatorname{not} y)y = \lambda xy. x(\lambda tf. yft)y $$
如果 $x$ 那么判断是否 $\neg y$，如果 $\neg x$ 那么判断是否 $y$。
$$\operatorname{xor} = \lambda xy. \operatorname{and}(\operatorname{not}(\operatorname{and} xy))(\operatorname{or} xy) = \lambda xy. xyx(\lambda tf. xyxft)(xxy) $$
如果并非 $x \land y$ 且存在 $x \lor y$，那么存在 $x$ 异或 $y$。
**代码 a5.**
```python
cxor = lambda x: lambda y: x(cnot(y))(y)
```
## Church Number
Church Number 编码了自然数及它的运算。
### Peano 公理
Peano 公理定义了自然数。其他自然数之上的运算与关系都可由其推出。
**公理 b1. Peano 公理**
2- 元组 $(\mathbb{N}, x^+)$ 是一个 Dedekind-Peano 结构，仅当其满足如下条件：
$$ \forall n \in \mathbb{N}, n^+ \in \mathbb{N}; (1)$$
$$ \forall m, n \in \mathbb{N}, m^+ = n^+ \to m = n; (2)$$
$$ \exists e \in \mathbb{N}, \forall n \in \mathbb{N}, n^+ \neq e; (3) $$
$$ \forall S \subseteq \mathbb{N}, e \in S \land (\forall s \in S \to s^+ \in S) \to S = \mathbb{N}. (4) $$
并且我们称 $\mathbb{N}$ 为自然数集，$x^+$ 为后继关系，$e = 0, e^+ = 1, (e^+)^+ = 2, ...$
### 将自然数编码
可以看到，自然数定义中的基本元素是自然数 $e$（即 $0$） 与后继运算 $x^+$。
**定义 b2. 自然数集元素的 Church Number**
很容易得到 $0$ 的 Church Number：
$$ \operatorname{zero} = \lambda sz.z $$
可以认为 $z$ 是 $0$，$s$ 是后继运算。
同样地，$1, 2, ...$ 的 Church Number 是：
$$ \operatorname{one} = \lambda sz.sz $$
$$ \operatorname{two} = \lambda sz.s(sz) $$
$$ ... $$
**代码 b2.**
```python
zero = lambda s: lambda z: z
one = lambda s: lambda z: s(z)
two = lambda s: lambda z: s(s(z))
-- ...
```
### 加法
自然数加法及证明略。
**定义 b3. Church Number 的加法**
$$ \operatorname{add} = \lambda xy. \lambda sz. xs(ysz) $$
这里，$x$ 的 “$0$” 是 $y$，即 $x$ 内部所应用的后继关系并非对于 $0$ 而是对于 $y$，最后结果就是 $x + y$ 而非 $x + 0$。
**代码 b3.**
```python
cadd = lambda x. lambda y. lambda s. lambda z. x(s)(y(s)(z))
```
### 乘法
自然数乘法及证明略。
**定义 b4. Church Number 的乘法**
$$ \operatorname{mul} = \lambda xy. \lambda sz. x(\lambda n. ysn)z = \lambda xy. \lambda s. x(ys) $$
这里，$x$ 的“后继关系”从“加 $1$”变为了“加 $y$”，应用了 $x$ 遍，结果是 $y \cdot x$ 而非 $1 \cdot x$。
**代码 b4.**
```python
cmul = lambda x. lambda y. lambda s. x(y(s))
```
### 幂
（这一部分用 Python 实在难讲，就用 Haskell 了，能看的凑合看看吧）
自然数幂及证明略。
回顾一下，Church Number 的类型是：
```haskell
type Cnum a = (a -> a) -> a -> a
-- Successor -> Zero -> Number
```
`(->)` 是右结合的，加对括号也无妨：
```haskell
type Cnum a = (a -> a) -> (a -> a)
```
这说明了，Church Number 可以看作“接受一个函数，并返回该函数的若干次幂的高阶函数”。这里“幂”的“乘法”是 function compose，即 Haskell 中的 `(.)`，范畴论中的 $\circ$。
Church Number 的幂是这样的：
**定义 b5. Church Number 的幂**
$$ \operatorname{exp} = \lambda xe. ex $$
其中 $x$ 为底数，$e$ 为指数。
可以想见，此函数的类型需要是这样才能工作：
**代码 b5.**
```haskell
cexp :: Cnum a -> (Cnum a -> Cnum a) -> Cnum a
cexp x e = e x
```
第一眼看上去很难懂，我们回到刚才的话题：
> Church Number 可以看作接受一个函数，并返回该函数的若干次幂的高阶函数。
再看一下那个指数的类型：
```haskell
e :: Cnum a -> Cnum a
{- 展开为 -} e :: ((a -> a) -> (a -> a)) -> ((a -> a) -> (a -> a))
{- 也就是 -} e :: Cnum (a -> a)
```
也就是说，这个指数是一个“高阶 Church Number”，也是一个“函数的 Church Number”。
理解了这个概念，我们再回来看 Church Number 的幂。举一个例子，$2^3 = 2 \cdot 2 \cdot 2$ 在 Church Number 中就变为了将一个 Church Number，也是一个函数，组合 3 次：
$$ C_2 \circ C_2 \circ C_2 $$
其中 $C_2$ 为 $2$ 的 Church Number。这也就是说，那个“高阶 Church Number”其实就是 $C_3$，$3$ 的 Church Number。
归约一下看看，就会发现我们的思路是正确的：
$$ C_2 ^ {C_3} (\lambda z. z^+)0 $$
$$ = C_3 C_2 (\lambda z. z^+)0 $$
$$ = (C_2 \circ C_2 \circ C_2)(\lambda z. z^+)0 $$
$$ = (C_2(C_2(C_2(\lambda z. z^+))))0 $$
$$ = (C_2(C_2(\lambda z. z^{++})))0 $$
$$ = (C_2(\lambda z. z^{++++}) ))0 $$
$$ = (\lambda z.z^{++++++++})0 $$
$$ = 8. $$
## 可以做的 Codewars 题
- [Church Booleans (5 kyu)](https://www.codewars.com/kata/5ac739ed3fdf73d3f0000048)
- [Church Numbers - Add, Multiply, Exponents (3 kyu)](https://www.codewars.com/kata/55c0c452de0056d7d800004d)