布尔类型的定义

实际上，[[2025-12-20-Lambda - 1 基本定理#多参数输入 / 柯里化 Currying|柯里化]]中我们给到的式子就是TRUE的表达形式，我们这里再写一遍 \(\displaylines{ \lambda a b.a \equiv TRUE\ (1)\\ \lambda ab.b \equiv FALSE\ (2) }\) 可以实验一下，如果给 $(1)$ 传入 $V_1\ V_2$，则会返回 $V_1$ 其实不该说布尔“类型”，而是一个布尔函数，它本质上是一个选择器

if-else定义

[!attention] 再次明确 所有东西都是函数！包括输入和输出！

上文提到了$TRUE$和$FALSE$本质上是一个选择器

  • 如果是$TRUE$，他会选择输入的两个值的前者
  • 如果是$FALSE$，他会选择输入的两个值的后者

由此，我们可以很轻易的用它来表示一个if-else函数 \(\lambda X.(X\ A\ B)X\) 这里的 $X$ 应当为 $TRUE$ 或者 $FALSE$，而 $A$ 和 $B$ 在 $X$ 输入后作为其两个参数输入，从而实现对 $A$ 或者 $B$ 的选择。其实现的功能伪代码如下

if X == TRUE:
	select A
if X == FALSE:
	select B

逻辑门定义

[!tip] $TRUE$ 和 $FALSE$ 的表达式我们上面已经知道了，之后就用英文字符串来代替了

非门实际上是最好想的，只需要把上文提到的 $A$ 和 $B$ 替换为 $FALSE$ 和 $TRUE$ 就行了 \(\lambda X.(X\ FALSE\ TRUE)X\)

与门需要两个参数的输入，只有两个都为 $TRUE$ 才返回 $TRUE$，这里我们不妨一级一级去判定。 假设输入的是 $xy$ ，我们先来判定 $x$ ，如果 $x$ 是 $FALSE$，那么返回 $FALSE$，如果 $x$ 不是，则再去判断 $y$，后面不做赘述。 其实不难发现，这是一个if-else的嵌套，所以也可以很容易的写出 \(\displaylines{ (\lambda{xy}.(x\ (y\ TRUE\ FALSE)\ FALSE)\ x\ y)\\ 注意到y\Leftrightarrow(y\ TRUE\ FALSE)，原式可化简为：\\ (\lambda{xy}.(x\ y\ FALSE)\ x\ y) }\)

或门同理可得 \((\lambda{xy}.(x\ TRUE\ y)\ x\ y)\)

比较符定义

零判断符 $isZero$

$0$有一个性质，那就是其相当于$FALSE$，对于输入的两个函数，它会将前者执行于后者$0$次，也就是说，他会返回后者本身 \(\lambda n.(n\ (\lambda x.FALSE)\ TRUE)\) 这样以来，若$n=0$,则返回$TRUE$，否则$(λx.FALSE)$至少一次的应用于$TRUE$，即最终返回$FALSE$ 进一步解释一下，若$n\neq0$，这里$x$输入的实际上$TRUE$，但是由于这个函数不管$x$什么事，只返回$FALSE$，所以逻辑是自洽的。

小于等于 $leq$

[!attention] 这需要[[2025-12-20-Lambda - 3 自然数定义#前驱类运算的定义 / 减法的定义|减法]]作为前提 另外需要注意的是，在执行$(-\ m\ n)$时，若$m<n$，那么其返回值依旧是$0$

很好理解，两个数相减，若其差为$0$，则必满足$m\leq n$ \(leq=\lambda{mn}.(isZero\ (-\ m\ n))\)

等于 eq

当且仅当$m\leq n$和$n\leq m$同时成立，满足$m=n$ \(eq=\lambda mn.((AND\ (leq\ m\ n)\ (leq\ n\ m))\ TRUE\ FALSE)\)

小于 lt

即小于等于成立且等于不成立的情况 \(lt=\lambda mn.(AND\ (leq\ m\ n)\ (not\ (eq\ m\ n)))\)

大于等于 geq

\(geq=\lambda mn.(not\ (lt\ m\ n))\)

大于 gt

\(gt = \lambda mn.(not\ (leq\ m\ n))\)

[[2025-12-20-Lambda - 3 自然数定义]]