万物皆为 lambda

定义

lambda 的语法和规约定义中都没有定义数字类型。

这是为了保持 lambda 的简洁性。数字类型的定义不是必须的，可以用特定的 lambda 表示。

根据皮亚诺公理，算数系统由一个起点（1 或者 0），和一个后继函数构成。

0，1，2，3，4，5，6……只是一种符号，一种自然数的编码。自然数的编码不是唯一的。

如果你愿意你也可以使用零一二三四五六来编码。

邱奇数是一种 lambda 形式的自然数编码。

定义起点为 $ 0 = \lambda f . \lambda x . x$

后继函数为 $succ = \lambda n . \lambda f. \lambda x. f (n f x)$

根据定义 $0$ 的后继为 $1$ 。所以将 $0$ 带入后记函数 $succ$ 中得到

$ (\lambda n . \lambda f . \lambda x. f(n f x) 0)$

将 $0$ 代入得到。

$(\lambda n. \lambda f. \lambda x. f(n f x) (\lambda f . \lambda x . x))$

为了避免混淆，对 $0$ 使用 $\alpha$ 变换。

$(\lambda n. \lambda f. \lambda x .f(n f x) (\lambda a . \lambda b . b))$

应用 $n = \lambda a . \lambda b . b$

$\lambda f. \lambda x. f((\lambda a . \lambda b . b) (f x))$

继续规约 $ a = f $

$\lambda f . \lambda x. f((\lambda b. b)x)$

继续规约 $ b = x $

$\lambda f . \lambda x .f x$

类似的方法可以得到 1 到 n 的定义

$0 = \lambda f . \lambda x . x $

$1 = \lambda f . \lambda x . f x$

$2 = \lambda f . \lambda x . f (f x)$

$3 = \lambda f . \lambda x . f (f (f x))$

$4 = \lambda f . \lambda x . f (f (f (f x)))$

$5 = \lambda f . \lambda x . f (f (f (f (f x))))$

$6 = \lambda f . \lambda x . f (f (f (f (f (f x)))))$

$7 = \lambda f . \lambda x . f (f (f (f (f (f (f x))))))$

$8 = \lambda f . \lambda x . f (f (f (f (f (f (f (f x)))))))$

$9 = \lambda f . \lambda x . f (f (f (f (f (f (f (f (f x))))))))$

$n = \lambda f . \lambda x . f^n x$

邱奇数的编码是将自然数 n 转化为 n 的次方，也就是 n 次函数复合。

运算

自然数运算最常见的是加减乘除。

先来定义最简单的加法。

$plus(m,n) = m + n$

因为邱奇数的编码是次方，所以 $f^{m+n}(x) = f^m(x) + f^n (x)$ 。

因此定义加法为

$ plus = \lambda m . \lambda n. \lambda f. \lambda x . m f (n f x)$

类似的乘法定义为

$mult = \lambda m . \lambda n . \lambda f . n (m f)$

因为减法和除法会产生出界的情况，这里就不展开定义了。有兴趣的烦请移步维基百科