8. 丘奇数与丘奇布尔值¶
8.1. 丘奇布尔值（Church Booleans）¶
要把 \(\lambda\) 演算变成一门"真正的"编程语言，我们需要能够处理：
布尔常量（true、false）
逻辑运算符（and、or、not）
条件表达式（if）
整数（0、1、2、3 等）
算术运算符（\(+\)、\(-\) 等）
数学函数（阶乘等）
\(\lambda\) 演算的创造者阿隆佐·丘奇（Alonzo Church）认识到了这一点，并由此着手制作了一系列 \(\lambda\) 表达式的编码，旨在满足我们对上面列表中的各项所期望的性质。我们首先考察 丘奇布尔值 常量与操作的一些编码。
TRUE = \(\lambda x. \lambda y.x\)
FALSE = \(\lambda x. \lambda y.y\)
AND = \(\lambda p. \lambda q.((p \; q) \; FALSE)\)
注意，AND 是双变量 p 和 q 的柯里化函数。下面的幻灯片演示了 TRUE AND FALSE——在柯里化形式中即 ((AND TRUE) FALSE)——是如何进行 \(\beta\)-归约的。
正如人们对布尔运算所预期的那样，TRUE AND FALSE 归约为 FALSE。建议你也尝试对 FALSE AND TRUE、FALSE AND FALSE、TRUE AND TRUE 做类似的归约，以使你自己确信：对于全部四种情况，我们的 AND 定义都精确地做了它该做的事。
8.2. 编码 If-Then-Else¶
下面的问题讨论三元 IF/THEN/ELSE 运算符的一种可能表示。
8.3. 编码 OR¶
下面的问题讨论二元 OR 运算符的一种可能表示。
8.4. 丘奇数（Church Numerals）¶
为了编码非负整数，丘奇使用了下面的编码：
ZERO = \(\lambda f. \lambda\ x.x\)
后继函数 SUCC = \(\lambda n. \lambda f. \lambda x.(f \; ((n \; f) \; x))\)
ONE = (SUCC ZERO) = \(\lambda f. \lambda\ x.(f \; x)\)
TWO = (SUCC ONE) = \(\lambda f. \lambda\ x.(f \; (f \; x))\)
THREE = (SUCC TWO) = \(\lambda f. \lambda\ x.(f \; (f \; (f \; x)))\)
FOUR = (SUCC THREE) = ???
FIVE = (SUCC FOUR) = ???
SIX = (SUCC FIVE) = ???
SEVEN = (SUCC SIX) = ???
EIGHT = (SUCC SEVEN) = ???
NINE = (SUCC EIGHT) = ???
TEN = (SUCC NINE) = ???
为了帮助你理解后继函数的工作原理，请看下面这个演示 THREE 的后继如何归约为 FOUR 的幻灯片。
加法和乘法可以编码为柯里化函数：
PLUS = \(\lambda m. \lambda n. \lambda f. \lambda x.((n \;f) \; ((m \; f) \; x))\)
MULT = \(\lambda m. \lambda n. \lambda f.(m \; (n \; f))\)
要了解乘法函数的工作原理，请看下面这个演示 (MULT TWO THREE) 如何归约为 SIX 的幻灯片。
我们再添加一个丘奇编码，用于计算丘奇数 n 的前驱：
PRED = \(\lambda n. \lambda f. \lambda x.(((n \; \lambda g. \lambda h.(h \; (g \; f)))\; \lambda u.x) \; \lambda u.u)\)
最后，我们添加一个测试是否为 0 的操作，它可以用于你在前面的练习题中（见上文）识别出的 if-then-else 。
ISZERO = \(\lambda n.((n \; \lambda x.FALSE) \; TRUE)\)
就像我们在前面的幻灯片中所做的那样，你应该使用这些已定义的操作做一些 \(\beta\)-归约，以使你自己确信它们按预期工作。
8.5. 丘奇数与加法和乘法¶
下面的问题帮助你认识和运用丘奇数以及相应加法与乘法运算符的表示。要获得这个随机题目的学分，你必须连续三次答对。
