Lambda初级简介 - 邱奇数

发表于 | 更新于 | 分类于

鹅鹅鹅，曲项向天歌，白毛浮绿水，红掌拨清波。

毫无疑问，在只有函数的λ演算里，数字是……不存在的…………。

​ 先前就已经讲过无类型的λ表达式当中，只有函数存在。那么，我们先前在λ演算里用的数字和加减乘除难道都是假的吗？是的，是假的。数字在λ演算里并非是必要之物，也是实际上不存在的。λ演算里存在的，只有函数。那么问题来了，数理逻辑是数学的分支，没有数字听起来是荒谬的。八十二年以前，那个男人自然不会没有想到这点。他就是λ演算的发明者，邱奇大神。

​ 用纯粹的函数可以做到和数字一样的效果，这是毋庸置疑的。归根结底，数字也是可以用函数定义的。自然数的运算，归根结底也就是那么几种。而可计算数又大抵是自然数，所以用于解决可计算问题的λ只要能完成这些运算就足够实现没有数字的数字了。

邱奇数 For λ表达式

​ 首先展现三个定义，在这里，我们用:=表示赋值，要记住，赋值只是一个方便使用的小把戏，函数名是不必要的(下篇文章会详细展开)。

1
2
3
zero := λs z . z
one  := λs z . s z
two  := λs z . s (s z)

​ 从现在起，我们不光使用λ表达式，我们也使用支持匿名函数的JavaScript来直观的演示我们学到的一切。

​ 聪明的你一定发现了，邱奇数对数字的定义其实很简单：任何邱奇数接受参数s和z，返回一个参数。邱奇数0，是直接返回z。而邱奇数1，则是返回z应用在s上的结果。邱奇数2，就是z应用在s上的的结果再次应用在s上。这里的参数s，意味着“后继函数(successor)“，而z，意味着”零点函数(zero)“。而邱奇数，就是把数字的前驱数作为参数应用在后继函数上的函数。比如说0没有前驱，则只是返回零点。1的前驱是0，所以返回s z，2的前驱是1，所以返回s (s z)。很简单，不是吗？

​ 现在我们有了数字，让我们看一看数字的运算。首先自然是最简单也是最基础的加法运算。

​ 我们知道，一个数字归根结底就是以零点为基准的后继函数调用链。那么，加法显而易见，就是把被加数的零点从原来的零点改为加数。想想看是不是这样？零点顾名思义是后继的基本点，后继函数就相当于从零点向后数，有一个后继函数就数一个数字。

​ 根据这个，我们很容易就能写出加法的λ表达式：add := λx y s z . x s (y s z)。很直观的结果！不过空口无凭，何况不套用一下我们刚刚学会的转换和归约，来实际计算一下邱奇数的加法呢？

​ 对于表达式：add one two s z，我们可以用如下步骤展开：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
add := λx y . (λs z . x s (y s z))	# 柯里化add函数, 因为其返回一个邱奇数所以add函数是接受x,y并返回一个接受s,z的函数.

add one two s z
add (λs z . s z) (λs z . s (s z)) s z	#代换one和two的定义
add (λs1 z1 . s1 z1) (λs2 z2 . s2 (s2 z2)) s' z'	#α-转换重命名消除歧义
(λx y . (λs z . x s (y s z))) (λs1 z1 . s1 z1) (λs2 z2 . s2 (s2 z2)) s' z'	#代换add的柯里化后的定义

#因为s'和z'是传递给新的邱奇数的参数, 所以舍去.
(λx y . (λs z . x s (y s z))) (λs1 z1 . s1 z1) (λs2 z2 . s2 (s2 z2))

(λs z . (λs1 z1 . s1 z1) s ((λs2 z2 . s2 (s2 z2)) s z)))	#应用β-归约 - 第一次
(λs z . (λs1 z1 . s1 z1) s (s (s z)) ))						#应用β-归约 - 第二次
(λs z . s (s (s z)) )										#应用β-归约 - 第三次
(λs z . s (s (s z)))	#最终结果!
three := (λs z . s (s (s z)))

​ 可以看到，运用加法函数，我们可以进行邱奇数的运算，而结果显而易见和直接定义是一样的！

​ 同理，我们可以定义其他的一些基础函数来进行邱奇数的运算：

1
2
3
4
5
6
suc := λx s z . s (x s z)		# 求x的后继数
mul := λx y s z . x (y s) z	# 求x*y
exp := λx y s z . (y x) s z	# 求x^y
pre := λx s z . x (λg.λh.h (g s)) (λu.z) (λu.u) # 求x的前驱数
sub := λx y . y pre x	# 求x-y
add := λx y . y suc x	# 同理, 求x+y

​ 我们注意到，这些函数无一例外都是运用了邱奇数会将后继函数执行n次的性质进行设计的。比如说x乘以y就是用执行y次的s当做x的后继函数，同时返回一个执行了x次该后继函数的邱奇数，显而易见就是x*y。x的y次方则是执行y次x，也就是y个x相乘，是幂运算的定义。前驱数是比其他基础运算复杂一些的运算(同理还有除法，本系列文章不介绍除法)，但是万变不离其宗。我们用一个实例来说明前驱数是如何实现的：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
pre := λx s z . x (λg.λh.h (g s)) (λu.z) (λu.u)
three := (λs z . s (s (s z)))	# 我们用邱奇数三做演示
pre three
λx s z . x (λg.λh.h (g s)) (λu.z) (λu.u) (λs z . s (s (s z)))	# 展开
λs z . (λs z . s (s (s z))) (λg.λh.h (g s)) (λu.z) (λu.u)		# 应用β-归约(以下简称归约)

# 让我们单独看这部分: (λs z . s (s (s z))) (λg.λh.h (g s))
(λs z . s (s (s z))) (λg.λh.h (g s))
# 可以看出邱奇数就是将其后继函数连续嵌套应用n次的函数, 所以应用归约显而易见可得: (中括号=括号)
λz.(λg.λh.h (g s))[ (λg.λh.h (g s))[ (λg.λh.h (g s))z ] ]
# 继续应用归约
λz.λh.h ( [ (λg.λh.h (g s))[ (λg.λh.h (g s))z ] ]  s)
# 继续应用
λz.λh.h ( [ λh.h ([ (λg.λh.h (g s))z ] s) ]  s)
# 继续
λz.λh.h ( [ λh.h ( (λh.h (z s)) s) ]  s)
# 继
λz.λh.h ( [ λh.h ( s (z s)) ]  s)
# 
λz.λh.h(s(s(z s)))
# 我们不难发现, 展开之后生成了n-1个s嵌套的函数链, 如果我们想要获得前驱数字, 只需要消除h并把z s替换为z.
# 这就是后半部分的作用, 回到原式并用连续应用归约得到的表达式代换
λs z . (λz.λh.h(s(s(z s))) ) (λu.z) (λu.u)
# 显然h和z分别出现在函数嵌套的最内层和最外层, 所以,h的函数作用就是返回其参数, z的函数作用就是返回z.
# 也就是说, z=λu.z, h=λu.u, 和后半部分相符, 展开, 则有:
λs z . (λu.u)(s(s((λu.z) s)))
# 继续应用归约
λs z . s(s(z))
# 则有pre three = λs z . s(s(z)) = two.  (o゜▽゜)o☆[BINGO!]

​ 剩余的函数的展开和推导十分简单，请读者自行完成。以上，就是邱奇数的主要部分，关于邱奇数，实际上有更加精妙的部分，感兴趣的读者可以自行查阅其他文章和资料。

邱奇数 For JavaScript

​ λ表达式固然精妙简洁，也存在着许多解释器、自动展开的程序。不过用JavaScript的匿名函数配合es6的箭头语法也是一个不错的，实现λ演算的方法，可以让我们更有实感的感受λ演算的魅力所在。

​ 本篇博客的载体就是网页，使用Chrome或其他派生浏览器的读者可以打开浏览器的debug页，利用其console实验本段给出的JavaScript代码。不过注意的是，由于使用了es6标准的箭头语法，所以部分浏览器可能不支持。

​ 首先参见上段给出的数字和基础操作的定义，我们不难写出他们在JS的表达式：

1
2
3
4
5
6
7
8
9
10
11
zero = s => z => z;
one = s => z => s(z);
two = s => z => s(s(z));

add = (x, y) => s => z => x(s)(y(s)(z));
suc = x => s => z => s(x(s)(z));
pre = x => s => z => x((g => h => h(g(s)))) ((u => z)) ((u => u));
add = (x, y) => y(suc)(x);
sub = (x, y) => y(pre)(x);
mul = (x, y) => s => z => x(y(s))(z);
exp = (x, y) => s => z => y(x)(s)(z);

​ 注意的是，由于λ表达式是左结合而且皆为单参数函数，所以利用JS转写λ表达式的时候要注意，每个函数接受一个参数并返回另一个函数，所以切记不要写成双参数的函数！本段代码内有部分二元运算使用了双参数，是在不影响定义的情况下进行的简写，调用者被规定一次必须使用一对参数。若把zero = s => z => z;简写成zero = (s,z) => z;就是错误的了。

​ 你可能十分迅速的就把这些代码复制到console里执行了，而且试图调用了一些加减法运算。不过发现并没有什么直观的效果出现。那是因为我们所有操作都返回一个邱奇数，而邱奇数本质是一个函数。我们要给定一个合理的后继函数和零点函数才能直观的感受邱奇数的魅力。

​ 后继函数和零点函数多种多样，JS和其他编程语言一样，都是依赖于机器数字进行运算，所以我们使用的后继函数和零点函数的效果就应该把邱奇数转换为机器数字。就像上文所说的一样，邱奇数的实质就是一套n次嵌套的后继函数调用链。那么如果我们每层都接受一个返回机器数字的函数并调用它得到机器数字，然后返回一个函数，这个函数返回得到的机器数字+1的值。那我们就可以实现将邱奇数转换为机器数了！

​ 所以，为了更方便、直观地试验邱奇数，我写了以下两个函数：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
Apply2param = (x, y, f) => {
	s = z => () => z() + 1;
	z = () => 0;

	console.log(x.name + ': ' + x.toString());
	console.log(y.name + ': ' + y.toString());
	console.log(f.name + ': ' + f.toString());
	return_value = f(x, y)(s)(z)();
	console.log(f.name + '( ' + x.name + ', ' + y.name + ' ) = ', return_value);
	console.log('');
	return return_value;
}

Apply1param = (x, f) => {
	s = z => () => z() + 1;
	z = () => 0;

	console.log(x.name + ': ' + x.toString());
	console.log(f.name + ': ' + f.toString());
	return_value = f(x)(s)(z)();
	console.log(f.name + '( ' + x.name + ' ) = ', return_value);
	console.log('');
	return return_value;
}

​ 现在，直接调用Apply2param(one, two, add)就可以直观地观察到1+2的邱奇数运算了！

​ 请读者自行写出生成任意邱奇数的函数。