专栏文章

Church 编码（和 Lambda 演算）

ddove
科技·工程参与者 46已保存评论 52

文章操作

快速查看文章及其快照的属性，并进行相关操作。

当前评论
52 条
当前快照
1 份
快照标识符
@mhz5rz1p
此快照首次捕获于
2025/11/15 01:55
4 个月前
此快照最后确认于
2025/11/29 05:24
3 个月前
查看原文

引入

Church 编码是一种“抽象方法”，它将“数字”、“运算”等概念全数“抽象”成 λ- 演算（别急着跑，会介绍什么是 λ- 演算的），来让程序实现更好的抽象性。换句话说，它将物件（布尔值、自然数、列表、etc）抽象为函数，并通过将公理的基本元素作为参数应用于其上来获得（依基本元素不同而不同的）值。
前置知识：布尔代数，基础 Python，小学数学
  • 这篇文章讲的东西，对 OI 有什么用吗？
    • 抱歉，几乎没有。如果您不想在 λ- 演算等抽象废话上浪费时间，现在就可以关闭本页面。
  • 你讲的真烂/你个初学者还写这种博客班门弄斧。
    • 请告诉我如何改进，或者自己写一篇吊打我。
  • 我学过 λ- 演算和 Haskell，想看更直接的介绍。

前置知识：λ- 演算

λ- 演算可以算作最原始的编程语言。我们来通过几个例子了解一下它，每个例子都有对应的 Python 代码（不用 C++ 是因为 C++ 弄这种东西非常困难，不用 Haskell 是因为很多人看不懂）。注意，所有 Python 函数都用 lambda 表达式，这是为了更好地对应，不会的可以学一下。
p1. λ- 演算的函数声明
所有 λ- 演算中的函数都接受且只接受一个参数。来看一个基本的函数：把参数加一。
λx.x+1\lambda x . x + 1
各个部分的意义：
lambda 符号，相当于“函数声明关键字”参数名分隔符函数体
λ\lambdaxx..x+1x + 1
Python 里就是
PYTHON
lambda x : x + 1
p2. λ- 演算的函数调用
函数调用没有括号。
f=λx.x+1f = \lambda x . x + 1 a:=3a := 3 b:=fa=4.b := fa = 4.
PYTHON
f = lambda x : x + 1
a = 3
b = f(a) # => 4.
λ- 演算的执行只有三条公理
  • α\alpha- 等价：λx.fx=λy.fy\lambda x. fx = \lambda y. fy。
  • β\beta- 归约：(λx.fx)y=fy(\lambda x. fx)y = fy。
  • η\eta- 归约：(λx.fx)=f(\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
  • λ- 演算的所有函数，事实上都是柯里化函数，也就是说它们只接受一个参数。
在 λ- 演算中也可以直接调用函数表达式
(λx.λy.x+y)ab=(λy.a+y)b=a+b.(\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
函数接受的参数也可以是函数，比如
(λx.λy.xy)ab=ab(\lambda x. \lambda y. xy) ab = ab
PYTHON
(lambda x : lambda y : x(y))(a)(b) # => a(b)
这里的 aa 只能是个函数。
有时候会见到 λxy.\lambda xy.这样的参数列表，它只是 λx.λy.\lambda x. \lambda y. 的简写。

Church 布尔代数

Church 布尔代数通过 Church 编码抽象了标准布尔代数，我们可以通过它来理解 Church 编码。

布尔值

考虑布尔代数的基本元素，即布尔值：
公理 a1. 布尔值的集合 B={F,T}\mathbb{B} = \{ F, T \}
其中 TT 为逻辑真，FF 为逻辑假。
在 Church 布尔代数中，它们将会如此表示：
定义 a1. Church 布尔代数中的布尔值 true⁡=λtf.t\operatorname{true} = \lambda tf.t false⁡=λtf.f\operatorname{false} = \lambda tf.f
可以认为 tt 与 ff 分别代表了抽象的逻辑真与逻辑假。
令 t:=T,f:=Ft := T , f := F，即将标准布尔代数的基本单位应用于 Church 布尔值后，其归约为（我们所想得到的）标准布尔代数值 - 这展示了标准布尔值和 Church 布尔值之间的关系：
true⁡TF=T\operatorname{true} T F = T false⁡TF=F\operatorname{false} T F = F
代码 a1.
PYTHON
true = lambda t : lambda f : t
false = lambda t : lambda f : f

取反

接下来考虑在标准布尔代数中的逻辑取反：
公理 a2. 布尔值的取反 ¬T=F\neg T = F ¬F=T\neg F = T
不难想到，在 Church 布尔代数中，逻辑取反的定义：
定义 a2. Church 布尔代数中的取反 neg⁡=λx.λtf.xft\operatorname{neg} = \lambda x. \lambda tf. xft
我们颠倒了逻辑真与逻辑假，这就令原值归约为相反的值。
代码 a2.
PYTHON
cnot = lambda x: lambda t: lambda f: x(f)(t)

逻辑与

公理（定理）a3. 布尔代数中的逻辑与 T∧T=TT \land T = T T∧F=FT \land F = F F∧T=FF \land T = F F∧F=FF \land F = F
定义 a3. Church 布尔代数中的逻辑与 有两种理解方式：
and⁡=λxy.xyx\operatorname{and} = \lambda xy. xyx 如果第一个值为假，那就直接得到结果，否则再判断第二个值是否为假。
and⁡=λxy.λtf.x(ytf)f\operatorname{and} = \lambda xy. \lambda tf. x(ytf)f 将其中一个值（xx）作为另一个值（yy）的真值，若xx为假，则yy即使为真，最后仍归约为假。
代码 a3.
PYTHON
cand = lambda x: lambda y: x(y)(x)

逻辑或

公理（定理）a4. 布尔代数中的逻辑或 T∨T=TT \lor T = T T∨F=TT \lor F = T F∨T=TF \lor T = T F∨F=FF \lor F = F
定义 a4. Church 布尔代数中的逻辑或 有两种理解方式：
or⁡=λxy.xxy\operatorname{or} = \lambda xy. xxy 如果第一个值为真，那就直接得到结果，否则再判断第二个值是否为真。
or⁡=λxy.λtf.xt(ytf) \operatorname{or} = \lambda xy. \lambda tf. xt(ytf) 将其中一个值（xx）作为另一个值（yy）的假值，若xx为真，则yy即使为假，最后仍归约为真。
代码 a4.
PYTHON
cor = lambda x: lambda y: x(x)(y)

逻辑异或

公理（定理）a5. 布尔代数中的逻辑异或 T⊕T=FT \oplus T = F T⊕F=TT \oplus F = T F⊕T=TF \oplus T = T F⊕F=FF \oplus F = F
定义 a5. Church 布尔代数中的逻辑异或 有两种理解方式：
xor⁡=λxy.x(not⁡y)y=λxy.x(λtf.yft)y\operatorname{xor} = \lambda xy. x(\operatorname{not} y)y = \lambda xy. x(\lambda tf. yft)y 如果 xx 那么判断是否 ¬y\neg y，如果 ¬x\neg x 那么判断是否 yy。
xor⁡=λxy.and⁡(not⁡(and⁡xy))(or⁡xy)=λxy.xyx(λtf.xyxft)(xxy)\operatorname{xor} = \lambda xy. \operatorname{and}(\operatorname{not}(\operatorname{and} xy))(\operatorname{or} xy) = \lambda xy. xyx(\lambda tf. xyxft)(xxy) 如果并非 x∧yx \land y 且存在 x∨yx \lor y，那么存在 xx 异或 yy。
代码 a5.
PYTHON
cxor = lambda x: lambda y: x(cnot(y))(y)

Church Number

Church Number 编码了自然数及它的运算。

Peano 公理

Peano 公理定义了自然数。其他自然数之上的运算与关系都可由其推出。
公理 b1. Peano 公理
2- 元组 (N,x+)(\mathbb{N}, x^+) 是一个 Dedekind-Peano 结构，仅当其满足如下条件： ∀n∈N,n+∈N;(1) \forall n \in \mathbb{N}, n^+ \in \mathbb{N}; (1) ∀m,n∈N,m+=n+→m=n;(2) \forall m, n \in \mathbb{N}, m^+ = n^+ \to m = n; (2) ∃e∈N,∀n∈N,n+≠e;(3)\exists e \in \mathbb{N}, \forall n \in \mathbb{N}, n^+ \neq e; (3) ∀S⊆N,e∈S∧(∀s∈S→s+∈S)→S=N.(4)\forall S \subseteq \mathbb{N}, e \in S \land (\forall s \in S \to s^+ \in S) \to S = \mathbb{N}. (4) 并且我们称 N\mathbb{N} 为自然数集，x+x^+ 为后继关系，e=0,e+=1,(e+)+=2,...e = 0, e^+ = 1, (e^+)^+ = 2, ...

将自然数编码

可以看到，自然数定义中的基本元素是自然数 ee（即 00） 与后继运算 x+x^+。
定义 b2. 自然数集元素的 Church Number
很容易得到 00 的 Church Number： zero⁡=λsz.z\operatorname{zero} = \lambda sz.z
可以认为 zz 是 00，ss 是后继运算。
同样地，1,2,...1, 2, ... 的 Church Number 是： one⁡=λsz.sz\operatorname{one} = \lambda sz.sz two⁡=λsz.s(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 的加法
add⁡=λxy.λsz.xs(ysz)\operatorname{add} = \lambda xy. \lambda sz. xs(ysz) 这里，xx 的 “00” 是 yy，即 xx 内部所应用的后继关系并非对于 00 而是对于 yy，最后结果就是 x+yx + y 而非 x+0x + 0。
代码 b3.
PYTHON
cadd = lambda x. lambda y. lambda s. lambda z. x(s)(y(s)(z))

乘法

自然数乘法及证明略。
定义 b4. Church Number 的乘法
mul⁡=λxy.λsz.x(λn.ysn)z=λxy.λs.x(ys)\operatorname{mul} = \lambda xy. \lambda sz. x(\lambda n. ysn)z = \lambda xy. \lambda s. x(ys) 这里，xx 的“后继关系”从“加 11”变为了“加 yy”，应用了 xx 遍，结果是 y⋅xy \cdot x 而非 1⋅x1 \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 的幂
exp⁡=λxe.ex\operatorname{exp} = \lambda xe. ex 其中 xx 为底数，ee 为指数。
可以想见，此函数的类型需要是这样才能工作：
代码 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 的幂。举一个例子，23=2⋅2⋅22^3 = 2 \cdot 2 \cdot 2 在 Church Number 中就变为了将一个 Church Number，也是一个函数，组合 3 次：
C2∘C2∘C2C_2 \circ C_2 \circ C_2
其中 C2C_2 为 22 的 Church Number。这也就是说，那个“高阶 Church Number”其实就是 C3C_3，33 的 Church Number。
归约一下看看，就会发现我们的思路是正确的：
C2C3(λz.z+)0C_2 ^ {C_3} (\lambda z. z^+)0 =C3C2(λz.z+)0= C_3 C_2 (\lambda z. z^+)0 =(C2∘C2∘C2)(λz.z+)0= (C_2 \circ C_2 \circ C_2)(\lambda z. z^+)0 =(C2(C2(C2(λz.z+))))0= (C_2(C_2(C_2(\lambda z. z^+))))0 =(C2(C2(λz.z++)))0= (C_2(C_2(\lambda z. z^{++})))0 =(C2(λz.z++++)))0= (C_2(\lambda z. z^{++++}) ))0 =(λz.z++++++++)0= (\lambda z.z^{++++++++})0 =8.= 8.

可以做的 Codewars 题

评论

共 52 条评论，欢迎与作者交流。

正在加载评论...