函数式编程

#00 | 初识Lambda演算
#01 | Lambda演算中的自然数
#02 | Lambda演算中的循环与递归

Lambda演算 #01

在定义了布尔值并且实现了“布尔运算”之后，我们要迈入下一步探索：自然数在Lambda演算中应该如何定义？

自然数的定义

我们依然采用Alonzo Church的方案来构造所谓的邱奇数（Church numerals），这个方案也满足皮亚诺公理，可以形成一个皮亚诺算术系统。

介绍这一方案前，我想定义一下函数的复合的表示形式，以便后文使用：

$f^{\circ n}=\underbrace {f\circ f\circ \cdots \circ f} _{n{\text{ times}}}$

而这一表示方案即利用函数复合的次数来表示对应的自然数，同时 $0$ 以不应用函数来表示，写作定义的形式即：

$\begin{align*} 0 &:= \lambda \ f \ x. x\\\\ 1 &:= \lambda \ f \ x. f \ x\\\\ 2 &:= \lambda \ f \ x. f \ (f \ x)\\\\ &\dots\\\\ N &:= \lambda \ f \ x. f^{\circ n} \ x \end{align*}$

为避免歧义，我们定义的自然数用 $N$ 表示，而其对应的数字意义的 $N$ 用小写字母 $n$ 表示。

可以发现，我们的 $0$ 和 $F$ 是 $\alpha$ 等价的，这对于学过编程——尤其是C语言——的同学似乎是理所当然的：
毕竟计算机里确实就是用0去表示False。

后继算子的构造

根据皮亚诺公理，现在需要得到一个后继算子 $succ$ 来实现自然数的递增，即我们希望有 $succ \ 0 = 1$ ， $succ \ 1 = 2$ ， $succ \ 2 = 3$ 以此类推。将其展开，即：

$\begin{align*} succ \ (\lambda \ f \ x. {\color{red}x}) &= \lambda \ f \ x. f \ {\color{red}x}\\\\ succ \ (\lambda \ f \ x. {\color{red}f \ x}) &= \lambda \ f \ x. f \ ({\color{red}f \ x})\\\\ succ \ (\lambda \ f \ x. {\color{red}f \ ( f \ x)}) &= \lambda \ f \ x. f \ ({\color{red}f \ ( f \ x)})\\\\ &\dots \end{align*}$

这意味着 $succ$ 算子将接收一个“自然数n”作为参数并且返回“自然数n+1”，但注意，这里的“自然数”的本质亦是一个函数。

由上篇文章关于柯里化的讨论，我们可以认为 $succ$ 算子应该是一个“三元函数”，它的第一个参数是一个“自然数”，而第二、第三个参数则是“自然数”本身应该具有的两个参数，如此，当我们给定一个“自然数n”时，它的值便成为了我们所需要的“自然数”的样子。

在这样的思路下， $succ$ 的作用就很显而易见了：

$succ \ N \ f \ x = f \ (N \ f \ x)$

于是，很显然得：

$succ := \lambda \ N \ f \ x. f \ (N \ f \ x)$

后继之上——加法，乘法与指数

有了后继算子，我们可以思考如何构造加法和乘法算子了。

由于我们定义了“自然数”的Lambda项是函数的复合，那么对于函数复合的一些基本的运算律我们就可以拿来使用并借此进行算子的构造。

首先，是加法算子，函数复合 $n+m$ 次的意义其实可以理解为：函数复合 $n$ 次，而后复合 $m$ 次。即：

$f^{\circ (n+m)}(x)=f^{\circ n}(f^{\circ m}(x))$

于是，利用构造后继算子的经验，加法算子 $plus$ 理应是一个“四元函数”，且返回值是两个“自然数”的“复合”：

$plus := \lambda \ N \ M \ f \ x. M \ f \ (N \ f \ x)$

其次，轮到了乘法算子，函数复合 $n\times m$ 次的意义其实可以理解为：函数复合 $n$ 次后作为一个新的函数，而后让这个新的函数复合 $m$ 次。即：

$f^{\circ (n\times m)}(x)=(f^{\circ n})^{\circ m}(x)$

和加法算子极其类似，不过在乘法算子中我们需要注意的是 $f$ 需要变为 $(N \ f)$ ，而不变的是 $x$ ：

$mult := \lambda \ N \ M \ f \ x. M \ (N \ f) \ x$

对于指数算子的构造，我们需要先从指数到底做了什么这件事情入手。一个函数复合 $n^m$ 次可以理解为：函数复合 $n$ 次后作为一个新的函数继续复合 $n$ 次，将这个过程持续进行 $m$ 遍。即：

$f^{\circ (n^m)}(x) = \underbrace{((f^{\circ n})^{\circ n}\dots )^{\circ n}}_{m \ times}(x)$

这会可能有点不好办了，但别急，我们看一下“自然数”的定义： $(N \ f)$ 可以做到将 $f$ 复合 $n$ 次得到 $f^{\circ n}$ ，而“自然数” $N$ 又可以理解为一个复合函数的函数——但它依旧是个函数——虽然它会接受两个参数。

于是，我们产生了一个想法：是否可以将 $N$ 复合呢？如果 $N \rightarrow M$ ， $f \rightarrow N$ 是不是就能实现将 $N$ 复合 $M$ 次了呢？我们尝试着计算一下如下的Lambda项：

$\begin{align*} M \ N \ f \ x &= \underbrace {N \ (N \dots N \ (N \ (N}\_{m \ times} \ f)))x\\\\ &= \underbrace {N \ (N \dots N \ (N}\_{m-1 \ times} \ (f^{\circ n}\ ))) x\\\\ &= \underbrace {N \ (N \dots N}\_{m-2 \ times} \ (f^{\circ (n^2\ )}\ )) x\\\\ & \dots\\\\ &= \underbrace {N \ (N \dots}\_{m-k \ times} \ (f^{\circ (n ^ k\ )}\ )) x\\\\ &= (f^{\circ (n ^ m\ )\ }) \ x \end{align*}$

而这也就是我们所期望得到的指数算子了，它看上去十分简单：

$exp := \lambda \ N \ M . M \ N$

前驱和减法

为了定义减法算子，我们需要先定义一个前驱算子。而定义前驱算子是个比较困难的过程，为了实现它有两个方法，这里我选择较为简单的一条，另一条你可以在Church encoding - Wikipedia中找到较为详细的描述。

首先，我们先定义一个数对算子 $pair$ ，将两个数组成一对来用：

$pair := \lambda \ M \ N \ x. x \ M \ N$

为了方便，我们将他记作： $[a, b] := pair \ a \ b = \lambda x. x \ a \ b$ ，利用之前定义的布尔值的选择能力，我们可以用它来选择其中的某一项：

$\begin{align*} [a, b] \ T &= pair \ a \ b \ T = T \ a \ b = a\\\\ [a, b] \ F &= pair \ a \ b \ F = F \ a \ b = b \end{align*}$

然后，我们再为 $pair$ 定义一个迭代算子 $phi$ ，它的作用是将数对 $[n, m]$ 忽略 $m$ 的值，并迭代到 $[n + 1, n]$ ，即在自增的同时能将自己的前驱保存在后一位：

$phi := \lambda \ p . [succ \ (p \ T), p \ T]$

比如：

$\begin{align*} phi \ [0, 0] &= [succ \ 0, 0] = [1, 0]\\\\ phi \ [5, 4] &= [succ \ 5, 4] = [6, 5] \end{align*}$

于是，我们可以借助”自然数“的复合迭代能力让数对在”加上来“的同时给了我们得到其前驱的机会，即定义 $pred$ 算子的机会：

$pred := \lambda N. N \ phi \ [0, 0] \ F$

其意义就是让 $pair[0,0]$ 进行 $N$ 次 $phi$ 而后选取其后一位输出。
用3作为例子试一下：

$\begin{align*} pred \ 3 &= 3 \ phi \ [0,0] \ F \\\\ &= 2 \ phi \ [1,0] \ F \\\\ &= phi \ [2,1] \ F\\\\ &= [3,2] \ F\\\\ &= 2 \end{align*}$

而对于”自然数“0，依照皮亚诺公理，它没有前趋，而这里则用稍微变通一点的方式，不妨设定0的前趋就是0本身。在这种情况下，我们的 $pred$ 算子依然可用，检验一下：

$\begin{align*} pred \ 0 &= 0 \ phi \ [0,0] \ F \\\\ &= [1,0] \ F \\\\ &= 0\\\\ \end{align*}$

完美符合预期。而有了前驱算子 $pred$ 之后，定义减法算子 $minus$ 就显得很简单了：如果要计算 $n - m$ 则只需要让 $n$ 连续求 $m$ 次前驱即可：

$minus := \lambda \ N \ M. M \ pred \ N$

而注意到我们定义的运算是在自然数的范围内讨论，所以对于算子 $minus$ ，当 $m > n$ 时， $minus \ N \ M = 0$

而对于仅剩的除法运算，由于它较为复杂，暂时先不作讨论，你可以在Division找到相关内容。

关系运算

在定义完基础的算数运算和布尔运算之后，我们的脚步可以迈入关系运算的领域了。

首先，我们考虑应该算子： $IsZero$ ，当输入为 $0$ 输出为 $T$ ，当输入为其他自然数时，输出为 $F$ 。

$IsZero := \lambda \ N. N \ F \ not \ F$

这里需要用到上篇文章中关于 $F$ 的一个特殊用处： $F\ x = \lambda \ x. x = I$

这个算子的核心在于 $(N \ F \ not)。$ 当 $N$ 为 $0$ 时，相当于 $F\ F\ not = not$ 。

$IsZero\ 0 = not \ F = T$

当 $N$ 是大于0的自然数时，相当于：

$\begin{align*} IsZero \ N &= N \ F \ not \ F \\\\ &= \underbrace {F (F \dots F(F}\_{n > 0 \ times} \ not))\ F\\\\ &= \underbrace {F (F \dots F}\_{n - 1 \ times} \ I))\ F\\\\ &= I \ F = F \end{align*}$

于是我们可以更加轻松得使用之前的准备去构建相等算子 $EQ$ ，小于或等于算子 $LEQ$ ，大于算子 $GT$ ，不等算子 $NEQ$ 等等了。利用一些很简单的运算律：

$\begin{align*} m \le n &\Leftrightarrow m - n = 0\\\\ m = n &\Leftrightarrow (m \le n)\wedge (n \le m) \end{align*}$

我们可以得到：

$\begin{align*} LEQ &= \lambda \ M \ N. IsZero\ (minus \ M \ N)\\\\ EQ &= \lambda \ M \ N. and\ (LEQ \ N \ M) \ (LEQ \ N \ M)\\\\ GT &= \lambda \ M \ N. not\ (LEQ \ N \ M) \end{align*}$

不妨试试构造更多的关系算子吧！

未完待续… 下一篇：#02 | Lambda演算中的循环与递归

函数式编程 | #01 | Lambda演算中的自然数