lambda-calculus

lambda-calculus

(lambda)演算(lambda-calculus)，是最小的通用程序设计语言。

三条基本语法规则

1. 函数为第一类对象，即所有(lambda)表达式构成(Lambda)空间，而所有的(lambda)表达式都是从(Lambda)空间到(Lambda)空间的一个映射。可以理解为所有的(lambda)表达式都是以(lambda)表达式为参数，返回值为(lambda)表达式的函数。

2. 函数的抽象原则，对于一个(lambda)表达式，不妨称为P，可以用一个字母代表哑元，不妨称为x，使用抽象原则，可以构造出另一个(lambda)表达式，如

x -> P

表示构造了一个函数，以一个(lambda)表达式为输入，返回一个(lambda)表达式，即将P中的所有x用输入替换（不太严谨），例如，若P为

x y z
y (x -> x)

那么对应的构造出来的(lambda)表达式分别为

x -> x y z
x -> y (x -> x)

如果代入一个值a，那么得到的结果分别为

a y z
y (x -> x)

3. 函数应用(Function application)，即给函数一个参数，得到一个结果。函数和参数之间用空格隔开即可，函数的结合是左结合的。

定义Bool

Bool类型是由两个值True,False构造成的，那么我们先来定义True和False:

True  = x y -> x
False = x y -> y

其中,x y -> x <==> x (y -> x)。

这样定义True和False后，我们就可以定义And,Or,Not了。

And = x y -> x y True
Or  = x y -> x True y
Not = x -> x False True

有了这三个操作，我们的Bool类型就算是定义完成了。

定义自然数

得到自然数

首先给出定义：

0 = f x -> x
1 = f x -> f x
2 = f x -> f (f x)
...
N = f x -> f^n x

要完整定义自然数，还要有后继数函数inc，大概要完成下面的事情。

inc N = N + 1

然而我们还没有加法，那么考虑N是一个接受两个参数的(lambda)表达式，接受了f,x，并将f作用到x上n次，我们再作用一次就能得到N+1了。于是有了如下定义：

inc = N -> (f x -> f (N f x))
    = N f x -> f (N f x)

有了inc的定义，我们就能定义出自然数了。

加减乘的定义

类比上面可得加法和乘法的定义：

add = N M -> (f x -> N f (M f x))
    = N M f x -> N f (M f x)
mul = N M -> (f x -> N (y -> M f y) x)
    = N M f x -> N (f M) x

定义了乘法，我们还可以定义指数：

pow = N M -> N (mul M) 1

此外还有一个更妙的定义：

pow = a b -> b a

然后定义前驱数dec。首先定义数对：

Pair = M N x -> x M N
[a,b] = Pair a b

可以用定义过的True和False来取其中的元素：

[a,b] True  = Pair a b True  = True a b  = a
[a,b] False = Pair a b False = False a b = a

为它定义一个迭代算子Phi，将数对[N,M]迭代到[N+1,N]:

Phi = p -> [inc (p True), p True]

现在就能定义dec：

dec = N -> N Phi [0,0] F

这里的意思是让Phi作用到[0,0]上n次，然后取第二个元素。

这样，我们也可以定义减法：

sub = N M -> M dec N

即将dec作用到N上M次。若M大于N，得到的值是0而非负数。

自然数的关系运算

首先定义一个判断是否为零的函数：

isZero = N -> N (and False) True

然后可以定义关系运算

leq = N M -> isZero (sub N M)
geq = N M -> isZero (sub M N)
le  = Not geq
re  = Not leq
eq  = N M -> And (leq N M) (req N M)
neq = Not eq

不动点

所谓不动点即为一个函数f(x)满足(exist x, f(x)=x)。

先看这样的函数：

f = x -> x x

那么，有

f f = (x -> x x) = f f

来看不动点的构造：

Y = f -> (x -> f (x x) ) (x -> f (x x) )
Y g = (x -> g (x x) ) (x -> g (x x) )
    = g (x -> g (x x) ) (x -> g (x x) )
    = g (Y g)

即Y g为g的一个不动点。

此外，还有一些不动点：

X = f -> (x -> x x) (x -> f(x x) )
0 = (x y -> y (x x y) ) (x y -> y (x x y) )

递归函数

有了不动点函数，我们就可以定义递归函数了。

比如，我们有一个关于自然数的递归定义：(N(n)={n}cup N(n+1))

我们想用lambda calculus来定义。

首先考虑不动点函数：

Y f = f Y f

定义一个辅助函数：

g = f N -> [N, f (inc N) ]

那么自然数可定义为：

naturalNumber = Y g 0

Y g 0 = g Y g 0
      = [0, Y g 1]
      = [0, g Y g 1]
      = [0, [1, Y g 2]]
      = [0, [1, g Y g 2]]
      = [0, [1, [2, Y g 3]]]
      = ...

这样，我们就用递归函数完成了自然数的定义。

例如，我们要定义一个阶乘函数，那么可以这样定义：

g = f N -> isZero N 1 (mul N (f (dec N)))

fact = Y g

Y g 3 = g Y g 3
      = mul 3 (Y g 2)
      = mul 3 (g Y g 2)
      = mul 3 (mul 2 (Y g 1))
      = mul 3 (mul 2 (g Y g 1))
      = mul 3 (mul 2 (mul 1 (Y g 0)))
      = mul 3 (mul 2 (mul 1 (g Y g 0)))
      = mul 3 (mul 2 (mul 1 1))
      = 6

定义斐波那契数列：

g = f N -> leq N 1 1 (add (f (dec N)) (f (dec(dec N))))

fib = Y g

Y g 4 = add (Y g 3) (Y g 2)
      = add (add (Y g 2) (Y g 1)) (add (Y g 1) (Y g 0))
      = add (add (add (Y g 1) (Y g 0)) (Y g 1)) (add (Y g 1) (Y g 0))
      = add (add (add 1 1) 1) (add 1 1)
      = 5