Church 编码（和 Lambda 演算）

引入

Church 编码是一种“抽象方法”，它将“数字”、“运算”等概念全数“抽象”成 λ- 演算（别急着跑，会介绍什么是 λ- 演算的），来让程序实现更好的抽象性。换句话说，它将物件（布尔值、自然数、列表、etc）抽象为函数，并通过将公理的基本元素作为参数应用于其上来获得（依基本元素不同而不同的）值。

前置知识：布尔代数，基础 Python，小学数学

• 这篇文章讲的东西，对 OI 有什么用吗？
  • 抱歉，几乎没有。如果您不想在 λ- 演算等抽象废话上浪费时间，现在就可以关闭本页面。
• 你讲的真烂/你个初学者还写这种博客班门弄斧。
  • 请告诉我如何改进，或者自己写一篇吊打我。
• 我学过 λ- 演算和 Haskell，想看更直接的介绍。
  • 可以到这里看这篇文章的原始版本。不过真的有人会了这些还不会 Church encoding 吗...

前置知识：λ- 演算

λ- 演算可以算作最原始的编程语言。我们来通过几个例子了解一下它，每个例子都有对应的 Python 代码（不用 C++ 是因为 C++ 弄这种东西非常困难，不用 Haskell 是因为很多人看不懂）。注意，所有 Python 函数都用 lambda 表达式，这是为了更好地对应，不会的可以学一下。

p1. λ- 演算的函数声明

所有 λ- 演算中的函数都接受且只接受一个参数。来看一个基本的函数：把参数加一。

\lambda x . x + 1

各个部分的意义：

lambda 符号，相当于“函数声明关键字”	参数名	分隔符	函数体
\lambda	x	.	x + 1

Python 里就是

lambda x : x + 1

p2. λ- 演算的函数调用

函数调用没有括号。

f = \lambda x . x + 1 a := 3 b := fa = 4.

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. λ- 演算的高阶函数

有些人可能有高阶函数的概念。高阶函数是“接受函数作为参数的函数”或者“返回函数的函数”。看一个例子。

g = lambda x : lambda y: x + y
g(1)(2) # 1 + 2 => 3

这种函数一次只接受一个参数，返回等待接受下一个参数的函数，这个函数又返回接受下下个参数的函数...,这种函数叫做“柯里化函数”。

• 它可以被更容易地“部分应用”。部分应用就是说只给它传一部分参数：

  add1 = g(1)
  add1(3) # 1 + 3 => 4

• λ- 演算的所有函数，事实上都是柯里化函数，也就是说它们只接受一个参数。

在 λ- 演算中也可以直接调用函数表达式

(\lambda x. \lambda y. x + y) ab = (\lambda y. a + y) b = a + b.

(lambda x : lambda y : x + y)(a)(b) # => a + b

函数接受的参数也可以是函数，比如

(\lambda x. \lambda y. xy) ab = ab

(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.

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.

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.

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.

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.

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.

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.

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.

cmul = lambda x. lambda y. lambda s. x(y(s))

幂

（这一部分用 Python 实在难讲，就用 Haskell 了，能看的凑合看看吧）

自然数幂及证明略。

回顾一下，Church Number 的类型是：

   type Cnum a = (a -> a)   -> a    -> a
--               Successor  -> Zero -> Number

(->) 是右结合的，加对括号也无妨：

   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.

cexp :: Cnum a -> (Cnum a -> Cnum a) -> Cnum a
cexp x e = e x

第一眼看上去很难懂，我们回到刚才的话题：

Church Number 可以看作接受一个函数，并返回该函数的若干次幂的高阶函数。

再看一下那个指数的类型：

            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)
• Church Numbers - Add, Multiply, Exponents (3 kyu)