如何用 Church 编码实现布尔值？

[!quote] 关于λ表达式…… 详见λ表达式 ⚠ 本文导出自Obsidian，可能存在格式偏差（例如链接、Callout等） 本文地址：https://www.cnblogs.com/oberon-zjt0806/p/18710283 目录λ演算与λ代数Church 编码Church-Boolean 逻辑编码条件选择函数真与假 | True | False逻辑运算 | AND | OR | NOT合取 | 且 | AND析取 | 或 | OR反转 | 非 | NOT λ演算与λ代数 上一整节我们利用λ符号体系构建了一套表达式系统，从这里开始，我们将正式开始利用这套系统进行代数应用，在进行演算之前，需要先利用符号体系构建一个代数运算系统。 [!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必须发生η归约。