λ演算

news/2025/2/11 18:19:44/文章来源:https://www.cnblogs.com/oberon-zjt0806/p/18710283

[!quote] 关于λ表达式……
详见[[λ表达式]]

λ演算与λ代数

上一整节我们利用λ符号体系构建了一套表达式系统，从这里开始，我们将正式开始利用这套系统进行代数应用，在进行演算之前，需要先利用符号体系构建一个代数运算系统。

[!note] 命名终究只是命名
虽然我们之前使用了很多诸如(+ x 1)等等这样的形式，但它们只是我们定义的命名，所以无论是x还是+和1，都只是一个记号而已，尽管我们根据以往的经验为这些符号赋予了某些我们所熟知的含义，但在当前的λ演算语境下，这些东西都还没定义过。

Church 编码

为了使λ演算能够具体应用到计算机和程序上，那么就意味着λ代数系统必须能够表示如下两种东西——

数值（逻辑值、整数……）
运算（算符、函数、操作……）

也就是说，这些东西要在λ演算中映射为λ表达式（使用表达式来表示）。

[!tip]
粗暴地说，Church编码就是一种把数值和运算编码为λ表达式的过程。

但注意！Church编码并非唯一的编码方式，还有其他的编码方式，如Scott编码等。

Church编码的特点在于以数值表示为起点进行编码，并在基础上构建其他编码。

Church-Boolean 逻辑编码

[!abstract] Church-Boolean 编码汇总
为了方便查阅，这里将本节所有的编码定义列出来，正文是比较冗长的推导过程
DEF T = λx.λy.x
DEF F = λx.λy.y
DEF AND = λP.λQ.(P Q P)
DEF OR = λP.λQ.(P P Q)
DEF NOT = λP.λQ.(P F T)

首先我们需要通过Church编码构建出布尔运算系统。之所以先选择布尔代数，是因为布尔代数的结构简单，性质清晰，比较容易构建。

布尔代数（Boolean Algebra）包含的内容非常简单——

布尔域$\mathbb B$中只包含两个元素$\mathrm T$和$\mathrm F$
支持三种基本运算$\wedge$ 、$\vee$、$\neg$ 。
运算对域封闭，且对于$\wedge$和$\vee$都在$\mathbb B$上分别存在上界和下界

条件选择函数

在介绍Church-Boolean中的真假值前，我们先来考察条件选择函数，所谓条件选择函数就是下面这样的一个三元函数——

\[\operatorname{COND} (c,x,y) = \begin{cases} x, &c=\mathrm{T} \\ y, &c=\mathrm{F} \end{cases} \]

其中$c$是条件值，条件选择函数根据$c$的值就在$x$和$y$中做出选择。可以发现，实际上，这个条件选择函数就对应了大多数编程语言中的三元运算符c ? x : y。

我们将这个运算表示为IF-THEN-ELSE形式，可以表示为——

IF c THEN x ELSE y

可以发现这里分为3个子部——

IF c ：判断c的条件；
THEN x：当c == true被满足时，选择x；
ELSE y：上述条件不成立时，选择y；

至此，我们可以把这三个部分抽象为三个λ表达式。

DEF cond = λc.λx.λy.(c x y)

由于真假值承载于c中，因此我们就利用c来对真假值进行编码。

真与假 | True | False

基于上面的想法，我们就能够通过Church编码定义出逻辑的真值T和假值F。讨论c的情况，根据定义，cond函数应当满足——

cond T x y => λc.λx.λy.(c x y) T x y => λx.λy.(T x y) x y => T x y => x
COND F x y => λc.λx.λy.(c x y) T x y => λx.λy.(F x y) x y => F x y => y

观察倒数两步归约，我们发现

欲使T x y => x，那么就要求(T x) y必须发生η归约。
- 也就是说(T x)中约束不生效，可以构建自由表达式(T x) == λb.x
  - 再脱去对x的运用，解开约束对，意味着我们需要引入一个新的约束变量
  - 于是我们就可以得到T == λa.λb.a。
欲使F x y => y，那么就要求(F x) y必须发生β归约。
- 而且更进一步地，(F x) == identity == λb.b
  - 类似地，再脱去对x的运用，解开约束对，引入另外的约束变量 λa
  - 于是F == λa.λb.b

[!tip] 反归约技巧
我们知道对于运用(f x)进行归约时，会将f中受约束的变量替换为参数x，例如(λa.a x) => x
那么，反过来对于已知的某一表达式x如果想要引入约束，或者把x作为参数提出来，那么就需要引入新的不冲突的约束命名，x => (λy.y x)。
利用这种性质在已知(f x)的情况下可以展开f == λa.(f a)

^9b9507

经过α转换，将a更名为x，b更名为y，我们就可以得出T和F的定义

DEF T = λx.λy.x
DEF F = λx.λy.y

这种定义下的T和F被映射为λ函数，因此可以作为一种条件选择函数来运用。

可以将上述定义代入表达式(c x y)通过[[λ表达式#归约消解|归约]]来证明这个编码的正确性——

[!warning] 注意
归约化简时，不要忘记变量约束的[[λ表达式#^{3bba62|右结合律]]**和**函数运用的[[λ表达式#}887c32|左结合律]]

(T T F) => (λx.λy.x λx.λy.x λx.λy.y)β|=> (λx.λy.(λx.λy.x) λx.λy.y) α|=> (λy.(λa.λb.a) λx.λy.y)η|=> (λa.λb.a)α|=> (λx.λy.x) => T(F T F) => (λx.λy.y λx.λy.x λx.λy.y)η|=> (λy.y λx.λy.y) β|=> (λx.λy.y) => F // alternatively, ==> identity F => F

逻辑运算 | AND | OR | NOT

接下来要对逻辑运算进行Church编码，这里先给出三种基本逻辑运算的真值表——

A	B	A AND B	A OR B	NOT A
F	F	F	F	T
F	T	F	T	T
T	F	F	T	F
T	T	T	T	F

XOR、NAND之类的都可以在这三种基本运算的基础上组合出来。所以我们姑且只定义上面三个基本运算即可。

在正式开始之前，我们先考察一个东西——既然T和F都被映射为函数，那么意味着他们可以相互作为函数和参数构成约束对进行运用，那么约束对能否归约，以及归约后的结果是什么，这里给出两个基本函数相互运用的归约结果——

T T => (λx.λy.x) (λx.λy.x) β|=> λy.(λx.λy.x) α|=> λy.(λa.λb.a) => λy.T
T F => (λx.λy.x) (λx.λy.y) β|=> λy.(λx.λy.y) α|=> λy.(λa.λb.b) => λy.F
[i.e.]  T P => λy.PT P Q => P
F T => (λx.λy.y) (λx.λy.x) η|=> λy.y => identity
F F => (λx.λy.y) (λx.λy.y) η|=> λy.y => identity
[i.e.]  F P => λy.y => identityF P Q => Q

^6686a8

需要注意的是，归约结果中的T和F中的x和y和外层约束的y没有任何关系，而是出现了命名冲突（如果要展开那么需要进行一次α转换），所以实际上这里的T是自由表达式。在上面的归约过程中，我们可以归纳出如下性质——

如果以T作为函数运用(T P)（其中P,Q in {T, F}），那么会通过β归约将x替换为P从而得到一个新的函子λy.P，且Q不受y的约束。
- 把这个结果λy.P再作为函数并传入参数Q构成约束对，那么下一步将发生η归约，消去λy约束，最终只会剩下P（T P Q => λy.Q Q => Q）
如果以F作为函数，那么由于F的λx并没有进行约束，所以先进行η归约，消去λx约束，最终总会留下λy.y，好巧不巧地，这正好是恒等函数identity
- 那接下来就很清晰了，如果再传入参数Q，由于identity的性质，或者直接通过β归约替换，则会只留下后面的这个参数P（F P Q => identity Q => λy.y Q => Q）

![Church T F.svg]]

完成上面的工作有助于我们通过Church编码来定义逻辑运算。

合取 | 且 | AND

首先来看一下合取运算，合取的要求是只有当两个输入均为T，才可以被归约为T，其他情形全部为F——

AND T Q => QAND T => (F P)
AND F Q => FAND F => (T P)

观察上面的形式，对于AND P Q ，我们可以做出如下归纳

当P==T时，AND P Q => AND T Q => Q
- 这种情况对应[[#^6686a8|上面]]的(F P)，于是AND T Q => F P Q
当P==F时，AND P Q => AND F Q => F
- 这种情况对应[[#^6686a8|上面]]的(T P)，于是AND F Q => T P Q

[!question] 麻烦了
目前我们归纳出的结论是AND P == (NOT P) P，然而问题在于我们还没有定义过NOT，这怎么办呢？

[!tip] 还好
AND满足交换律，也就是说应当有AND P Q == AND Q P

通过交换律将AND P Q换成AND Q P，不影响先前的结论，除了讨论对象此时从AND P变成了AND Q。

AND Q P[P:=T] => QAND Q => (T Q)
AND Q P[P:=F] => AND Q F => FAND Q => (F Q)
AND Q => (P Q)

终于我们可以得出AND的Church编码——

DEF AND = λP.λQ.(P Q P)

析取 | 或 | OR

与合取类似，析取也具有交换律，并且我们也可以效仿刚才的过程完成OR的定义，首先考察

OR T Q => TOR T => (T P)
OR F Q => QOR F => (F P)

这次无需交换律了，直接替换就能够得到OR的定义——

DEF OR = λP.λQ.(P P Q)

反转 | 非 | NOT

NOT比较特别，因为NOT是一个一元运算，需要单独讨论。

NOT T == NOT λx.λy.x => F == λx.λy.y
NOT F == NOT λx.λy.y => T == λx.λy.x

简单来说，输入的参数是选择其中一个，那么NOT的输出总是选择另外一个。考虑到真假值T和F均是通过cond定义的，那么，如果直接反转cond的定义是不是就能够得到相反的输出？

cond == λc.λx.λy.(c x y)
ncond == λc.λx.λy.(c y x)

于是我们得到了一种NOT的定义形式

DEF NOT1 = λP.λx.λy.(P y x)

这个形式看起来比较底层，我们能不能利用已有的逻辑值来定义呢？

再次考察 cond P ——

cond P => λP.λx.λy.(P x y) P => λx.λy.(P x y)

如果考虑将x替换为F，y替换为T，也能达成同样的效果，于是我们进一步提供参数——

cond P F T => λx.λy.(P x y) F T => P F T

于是我们得到了另一种NOT的定义——

DEF NOT2 = λP.(P F T)

通过归约可证明，NOT1 <=> NOT2

至此，两个逻辑值和三个基本逻辑运算被定义完毕，Church-Boolean编码完成，可以使用λ表达式进行逻辑演算了。

[!question] 思考
不妨试试用类似的方式定义出更多的逻辑运算，例如异或XOR、与非NAND等……

Church-N 自然数编码

自然数域的情况就要比布尔域的情况复杂得多了，自然数的特点是——

具有无限多可枚举的元素
- 具有下界0，但没有上界
具有更多的运算形式，且计算更为复杂

不过，即便情况更为复杂，在已经定义了Church-Boolean编码后，我们也同样可以借鉴相关的思路，甚至是在其基础上继续构建。

Peano 公理

先介绍一下自然数的Peano公理——

[!info] Peano 公理
自然数集合 $\mathbb{N}$ 可以用如下5条公理来描述

$0$是自然数 $$0 \in \mathbb{N}$$

对任一自然数$n$，总存在其后继$n^+=n+1$，且后继$n'$亦是自然数$$\forall n\in \mathbb{N}, \exists n^+=n+1,n+ \in \mathbb{N}$$

$0$不是任何自然数的后继 $$\forall \kappa \in \mathbb{N}, \kappa^+ \ne 0$$

任意两个自然数$a$和$b$具有相同的后继，当且仅当$a=b$（后继运算是单射/每个自然数具有各自唯一的后继）$$\forall a,b \in \mathbb{N}, a^+=b+ \iff a=b$$

归纳公理：对集合$N \subseteq \mathbb{N}$，若$N$满足如下两个条件，则$N=\mathbb{N}$

$0 \in N$

$\forall n \in N, n^+\in N$

\[N \subseteq \mathbb{N},0\in N, (\forall n \in N, n^+\in N) \implies N = \mathbb{N} \]

根据Peano公理，我们了解到，自然数集合$\mathbb N$，其下界 $\inf \mathbb{N} = 0$ 。由于自然数集合可枚举且良序，因此我们可以定义一个“后继”运算SUCC来获得下一个更大的元素。

0
1 == SUCC 0
2 == SUCC 1 == SUCC SUCC 0
3 == SUCC 2 == SUCC SUCC SUCC 0
...

此时我们发现，自然数可以用SUCC的复合次数来表示。但问题在于如何定义0和succ。最重要的是，将复合的次数通过λ表达式体现出来。

Church 数

我们先将后继运算抽象为f放在一边，先考虑0，0没有经过任何f运算，也就是复合层数为0，如果对于一个参数x而言，没有复合意味着输入不经过函数处理而保持原样输出。符合这个条件的函数显而易见——恒等函数identity == λx.x。

identity x => λx.x x => x

但是直接用identity并不能体现0次的f运用，因为那个复合层数为0的函数f在identity中并没有得到抽象，于是需要引入额外的约束λf。

DEF 0 = λf.λx.x

现在的0被定义为对x的0次f运用，如果我们需要前进到1，那么我们就应该对x运用1次f，即——

DEF 1 = λf.λx.(f x)
DEF 2 = λf.λx.(f (f x))
DEF 3 = λf.λx.(f (f (f x)))
...

后继 | SUCC

观察上面的Church编码，如果我们想要表示100那恐怕是一件麻烦的事情——

DEF 100 = λf.λx.(f f f f ...? x) // 100 f's??

根据Peano公理，我们知道100 == SUCC 99，类似地3 == SUCC 2、2 == SUCC 1、1 == SUCC 0。而这些数都已经被编码为λ函数。

那么我们能否通过N来定义出SUCC N，答案是肯定的，首先考察对0中的两个约束进行参数绑定——

0 => λf.λx.x
0 f => λf. f η|=> λx.x

可以发现，0 f经过η归约就是恒等函数，下面我们以同样的方式对1作处理，这里我们可以使用前面提到的 [[#^9b9507|反归约技巧]]，将(f x)变形

1 => λf.λx.(f x) <== λf.λx.(λa.(f a) x)
1 f => λf.λx.(f x) f => λx.(f x) α|=> λa.(f a)

虽然我们没有把0和1关联起来，但此时我们发现一个惊人的结论，我们可以使用1 f来表示1——实际上，我们对0也可以做同样的操作，结论同样成立，可以用0 f来表示0，于是我们可以把自然数抽象出来，形成一个新的λ表达式——

1 == λf.λx.(λa.(f a) x) == λf.λx.(1 f x)
0 == λf.λx.(λa.a x) == λf.λx.(0 f x)
N == λf.λx.(N f x)
DEF num = λn.λf.λx.(n f x)

可以证明，将上述定义的自然数绑定num时，num相当于恒等函数，当然，num N也可以视为自然数的递归编码——

num N => λn.λf.λx.(n f x) λf.λx.(N f x) => λf.λx.(λf.λx.(N f x) f x) => λf.λx.(N f x) == N

截止目前为止，还是在用0来表示0罢了，但是我们得到了N f x与N的关系，下面就结合自然数Church编码定义来考察N f x

0 f x => λf.λx.x f x => x
1 f x => λf.λx.(f x) f x => f x => f (0 f x)
2 f x => λf.λx.(f (f x)) f x => (f (f x)) => f (1 f x)
...
SUCC N f x == f (N f x)

这样，我们总算把N和它的后继SUCC N关联起来了，于是我们可以定义出SUCC运算了