函数式编程的数学基础（三）邱奇数的比较，分支逻辑-五八三

我们已经有了邱奇数的加、减和乘法。

但是现在lambda定义的邱奇数看上去无法互相比较，我们这里就考虑一下如何实现邱奇数的比较。

TRUE和FALSE

要想实现比较运算，我们首先要再lambda体系中定义TRUE和FALSE。

因为lambda演算中只有函数，所以我们思考一下，TRUE和FALSE应该是什么样的函数？

考虑到，我们一般使用布尔类型都是用于分支逻辑，所以我们把TRUE和FALSE设计成类似if和else的结构。

我们让TRUE和FALSE以柯里化的形式接受两个值，然后TRUE返回第一个值，FALSE返回第二个值：

TRUE = \lambda x.\lambda y.x \\ FALSE = \lambda x.\lambda y.y

这样我们就可以直接把这种布尔类型的函数当作if使用。我们调用某一布尔型函数：

(b\ x\ y)

这里等价于

if(b)
    return x;
else
    return y;

从数学的角度，这个形式完全没有问题，但是如果我们真正要落到可执行的程序代码，有时我们希望x或y不要进行计算，这时我们就还要稍微做一些处理，我们留待后文讨论。

有了TRUE和FALSE，我们来考虑如何实现邱奇数的比较，首先我们来考虑一个基本的问题，判断一个邱奇数是否为0。

我们先来复习一下邱奇数：

ZERO = \lambda f.\lambda x.x \\ ONE = \lambda f.\lambda x.(f\ x) \\ TWO = \lambda f.\lambda x.(f\ (f\ x)) \\ ……

我们看到，除了0以外，其它邱奇数生成的lambda函数都至少会调用一次函数f。

于是我们可以构造一个把任何值变成FALSE的f，和一个值为TRUE的x。

isZero = \lambda n.(n\ (\lambda a.FALSE)\ TRUE)

这样我们就有了第一个比较运算。

这里我们要用到上一篇中的减法。我们来考虑一下，当我们用一个较小的数减掉一个较大的数，会发生什么。

根据 $pred$ 的实现方案，我们发现，这样的减法并不会产生负数，而是会固定得到0。

结合我们上一小节实现的 isZero，我们就可以得到大于等于和小于等于

lessOrEqual = \lambda m.\lambda n.(isZero\ (minus\ m\ n))\\ greaterOrEqual = \lambda m.\lambda n.(isZero\ (minus\ n\ m))

目前为止，我们仅仅得到了判断0、大于等于和小于等于两种比较运算。很容易想到，如果我们的布尔类型能进行布尔运算，我们就能够实现其它比较运算了。

我们先考虑与运算。其大致形态应该是：

and = \lambda x.\lambda y.\ …

我们看下and运算的真值表：

不难发现，当x为TRUE时，其结果与y一致，当x为FALSE时，其结果必然为FALSE。

所以我们可以根据这个规律写出and

and = \lambda x.\lambda y.(x\ y\ FALSE)

同理我们可以写出or

or = \lambda x.\lambda y.(x\ TRUE\ y)

非运算则非常简单：

not = \lambda x.(x FALSE\ TRUE)

有了逻辑运算，我们可以从大于等于和小于等于得到等于

equal = \lambda m.\lambda n.(and\ (lessOrEqual\ m\ n)\ (greaterOrEqual\ m\ n))

结合非运算，可以得到不等于：

notEqual = \lambda m.\lambda n.(not\ (equal\ m\ n))

有了不等于，再从大于等于和小于等于中得到大于和小于：

less = \lambda m.\lambda n.(and\ (lessOrEqual\ m\ n)\ (notEqual\ m\ n))\\ greater = \lambda m.\lambda n.(and\ (greaterOrEqual\ m\ n)\ (notEqual\ m\ n))

到此，我们实现了邱奇数的比较运算，还获得了分支逻辑的能力，分支是达成图灵完备的重要条件之一，接下来我们只需要再获得循环的能力，就可以论证邱奇数的图灵完备性（注：事实上，历史中邱奇数的图灵完备性论证比结构化程序设计提出要早，所以它使用的是另外的方法）。

文章版权归作者所有，未经允许请勿转载，侵权请联系 admin@trc20.tw 删除。

THE END