Lambda初级简介 - 逻辑运算

如果说计算机的血液是零与一，那么逻辑运算是她的心脏。

同样，真假与或非也是不存在的。

​ 邱奇数的定义想必十分精妙，如果能理解邱奇数，那么理解逻辑运算只不过是手到擒来的事情罢了。前文说过，λ演算强大到可以进行逻辑推演；那么同样，我们需要用函数来定义的逻辑运算。

​ 前文的简介长达2800字，真的是简介了。相信这次我能把字数压缩到800字左右，毕竟东西不多。

​ 和邱奇数一样，λ演算里的逻辑运算所使用的真假定义也叫“邱奇布尔值”。其定义比邱奇数更加简单。为：

TRUE := λx y.x
FALSE := λx y.y

​ 这两个值实际上并不直观，不过如果联想，在机器编程里TRUE的功能是当TRUE时执行第一个语句块抛弃第二个语句块，FALSE的功能是执行第一个抛弃第二个的情况，事情就变得直观许多。事实上，λ演算内布尔值的定义有许多，其归根结底是根据逻辑运算的定义而定义的。之所以邱奇布尔值的定义如上，那是因为逻辑运算所需要这样的特性。

​ 逻辑运算总共分为三种：和(AND)、或(OR)、非(NOT)，其在λ演算内，基于邱奇布尔值的通常定义如下：

AND := λp q . p q FALSE
OR  := λp q . p TRUE q
NOT := λp   . p FALSE TRUE

​ 若与邱奇布尔值结合来看，其实是十分简单易懂的(现代魔法)。求和在于两者皆真结果真，所以当AND的参数p、q两者接受到假的时候都会返回假：当p为假，根据定义返回第二个参数，即FALSE。当p为真，根据定义返回第一个参数，q为真则返回真，为假则假。OR和NOT同理。下面我们来推导一下：

AND TRUE FALSE
(λp q . p q FALSE) TRUE FALSE	# 代换AND定义
TRUE FALSE FALSE				# β-归约, 展开
(λx y.x) FALSE FALSE			# 代换TRUE定义
FALSE							# β-归约, 展开

​ 如果你刚刚看完邱奇数那篇，那么你可能注意到了，FALSE的定义在α-转换后和zero的定义是一样的，即FALSE等价于zero，这和许多机器编程以及人的直感是相符的。根据这个，我们很容易就可以判定一个数字是否为零。一般来说，判断一个数字是否为零的函数“ISZERO”的定义是：

ISZERO := λn.n(λx.FALSE) TRUE

​ 同样也是十分容易理解的，当n不等于零的时候肯定存在最外层的后继函数，所以要让后继函数恒返回FALSE。当n等于零的时候只有零点函数存在，所以返回TRUE。

​ 当然，我们也可以写出if语句来：

IF := λp x y. p x y

​ 归功于邱奇布尔值十分简单，我们也能用这样简单的方法来实现if。二元组及其相关操作也可以通过这些来实现。二元组就是两个有顺序的数据存在一起的组合，又称为有序对，其和我们所说的链表是一样的，当有序对的第一个数据为链表的元素，第二个数据为另一个有序对时，这就构成了一个链表，比如：(a (b (c d))。其有关操作定义为：

CONS := λx y.λp IF p x y
CAR  := λx.x TRUE
CDR  := λx.x FALSE

​ 定义简明无需多言。何况不试着用JavaScript实现这一切呢？

​ 现在，我们有了逻辑运算，有了if语句，有了数字，有了基础运算，我们就可以打拼一片属于λ的天下了！可能你已经迫不及待的想写一写实际的算法来大展身手。可能你想用大家熟知的阶乘运算来证明λ的实力，很简单，你写出了以下代码：

FACT := λn.IF (ISZERO n) 1 (mul n (FACT (pre n)))

​ 然后兴致冲冲的宣布你在λ里实现了阶乘！

​ 等一下……

​ 这里的FACT是什么？

​ λ演算里真的有FACT存在吗？

​ 调用自身的话，就一定要使用函数名吗？

​ 可是，λ演算存在的仅仅只有匿名函数啊？