这篇是我读《the little scheme》之后想记下来一些东西,这本书初看是在介绍简单的scheme的语法,写一些例子,但是在最后几章分别介绍了图灵停机问题和Y combinator,我才发现作者的心思。

\(\lambda\)-Calculus的语法与规约

语法以及自由变量

先给出lambda演算的BNF 然后给出一些例子:

简单的解释一下的话,对于单一的x,就是指一个变量x,而对于(x y)这种形式,意义是将x应用在y上,以scheme(scheme本身就可以看做一个\(\lambda\)-Calculus的扩展)的代码为例(+ 1 2),就是将第一个符号+应用到12上。

对于\(\lambda\)这个符号就是定义一个匿名函数,即lambda函数,如\((\lambda x.x)\)就是定义了一个以x为参数,返回x的函数,如果要调用这个函数,就用括号的语法\(((\lambda x.x) a)\),就相当于将a当做参数传给函数。当然正如经常所说的函数是第一类成员,函数的定义可以出现在任何地方,比如在调用参数\(((\lambda x.x) (\lambda x.x))\)、在返回值上\((\lambda y.(\lambda x.x))\)等。

然后,使用\(\mathcal{FV}\)代表free variables,其实就是没有被绑定的变量,它有以下的关系:

即变量的集合中的元素都是自由变量。但是在函数中,除参数(他们的值应该在调用时被确定)意外,其他的变量也应该是自由变量。在一个语句中的自由变量应该是所有符号自由变量的并集。 下面有一些例子: \[\mathcal{FV}(x) = \{x\}\] \[\mathcal{FV}((x\space (y\space x))) = \{x,y\}\] \[\mathcal{FV}((\lambda x.(x \space y)) = \{y\}\] \[\mathcal{FV}(z\space (\lambda z.z)) = \{z\}\]

规约

在我们定义lambda演算表达式的规约之前,还需要定义变量替换的一些关系。定义关系\(\_[\_ \leftarrow \_]\)将一个将源表达式映射到目标表达式。这只是一个简单地替换,但是它__只替换自由变量__。 具体语法

一些例子

然后定义三种简单的规约关系\(\alpha,\beta,\eta\)

  • \(\alpha\)关系对参数进行重命名。意义是对于\((\lambda X_1.M)\)等价于将参数换成\(X_2\),然后将M中的\(X_1\)换成\(X_2\),当然前提是\(X_2 \notin \mathcal{FV}(M)\)。这表明了诸如\((\lambda x.x)\)这种函数和\((\lambda y.y)\)是等价的。所以,有时候也叫\(\alpha\)替换。
  • \(\beta\)关系是主要的规约原则,主要处理函数的规约。其实就是对于一个函数调用,就是将其函数体部分的替换成参数。有时候,直接叫\(\beta\)规约。
  • \(\eta\)关系体现了一个事实,当一个函数做的事是接受一个参数,然后马上将这个参数传给另一个函数,等价于直接调用另一个函数。

三种规约的并集,我们称general reduction relation为__n__。

下面是一个规约的例子:

标示符中有很多的括号会导致阅读的困难,为了简化,有时会采用如下简写:

  • \(M_1 \space M_2 \space M_3\)等价于\((M_1 \space M_2 \space M_3)\)
  • \(\lambda X.M_1 \space M_2\)等价于\((\lambda X.(M_1 \space M_2))\)
  • \(\lambda X Y Z.M\)等价于\((\lambda X.(\lambda Y.(\lambda Z.M)))\)

实现基本元素

定义Boolean

Boolean值是我们编程语言必须的,一般我们常见的方法就是预先定义两个常量truefalse。但是在lambda演算中采用不同的办法,这里定义

为什么这么定义呢? 我们展开试一下 首先,其实对于if我们期望它应该满足两个功能

1
2
(if # t M N) ;应该返回M
(if # f M N) ;应该返回N

我们展开这两个式子

显然,这种方式定义的if,true,false都是可以满足需求的。

定义pairs

除了Boolean以外,还需要一些数据结构,这里就定义pair以及相关的操作。显然应该有 \[fst \space (mkpair \space M \space N) =_n M\] \[snd \space (mkpair \space M \space N) =_n N\]

所以我们利用之前定义的boolean内容来定义 \[<M, N> \doteq \lambda s.if \space s \space M \space N\] \[fs \doteq \lambda p.p \space true\] \[snd \doteq \lambda p.p \space false\]

这几个定义都比较容易理解。

定义数字

除了Boolean和pair以外,还有一个非atom的特例,就是数字。在lambda演算中有很多方法定义数字,其中最著名的还是Church numerals(邱奇数)。

这里f看成函数,x是函数参数,数字的大小其实就是对应了f函数的调用次数。 对于数字应该还有加减等操作。 定义加1这个操作为: \[add1 \doteq \lambda n.\lambda f.\lambda x \space f \space(n \space f \space x)\] 有了这个加一的操作以后,就可以定义add了,n加m其实就是将n+1这个操作做m次,正好我们这里对数字的定义就是f在以x为参数执行的次数,所以,我们可以直接定义 \[add \doteq \lambda n.\lambda m.m \space add1 \space n\] 相似的可以定义函数iszero \[iszero \doteq \lambda n.n\space (\lambda x . false)\space true\]

之前已经成功的定义了一系列的函数,但是在定义sub1上,明显有一些困难,add1只要在数字外面再包一层对于f的调用就好,但是sub1却不是这么简单,我们想要一种回滚这种函数的方法。 这里采用一种巧妙的方式实现,将sub1的实现分成两部分:

  • 生成一个包含对于给定的参数x和true的pair,true代表函数f应该被跳过。
  • 包裹给定的函数f,依次获取pair,只有当pair包含false时,才执行f,同时永远返回包含false的pair,这样f在接下来会被使用。

\[wrap \doteq \lambda f.\lambda p.<false, if\ (fst\ p)\ (snd\ p)\ (f\ (snd\ p))>\]

然后定义sub1,它接受一个数字n,然后返回一个以f和x为参数的函数,但是他会把f用上面定义的wrap函数包裹着,由于同时给了参数是,所以,在第一层调用f(注意这个时候其实调用的是用wrap包裹的f),会因为(fst p)是true而直接返回第二个值。

\[sub1 \doteq \lambda n.\lambda f.\lambda x.snd\ (n \ (wrap\ f)\ <true,x>)\]

为了形象的理解这个问题,下面我们计算一下2 - 1 \[(sub1\ \ \lambda f.\lambda x . f\ (f\ x))\]sub1展开 \[((\lambda n.\lambda f.\lambda x. snd\ (n\ (wrap\ f)\ <true,x>))\ \ \lambda f.\lambda x . f\ (f\ x))\] 展开n部分 \[(\lambda f.\lambda x.snd\ \ ((\lambda f.\lambda x . f\ (f\ x)) \ \ (wrap\ f)\ <true,x>))\] 展开后面 \[(\lambda f.\lambda x.snd\ \ ((wrap\ f)\ \ ((wrap\ f)\ <true,x>)))\] 后一个\(((wrap\ f)\ <true,x>)\)的结果显然是\(<false,x>\) \[(\lambda f.\lambda x.snd\ \ ((wrap\ f)\ <false,x>))\] 现在\(((wrap\ f)\ <false,x>)\)的结果是\(<false, (f\ x)>\) 最后结果就变成 \[(\lambda f.\lambda x.f \ x)\]

这里也是证明了函数是有效的。 这里再提一点,在之前的所有例子中,所有的lambda函数都是只有一个参数的,有时候可能会见到有直接写多个参数的写法,其实是一样。

1
2
3
(lambda (x)
(lambda (y)
x+y))

1
2
(lambda (x y)
x+y)

这两种写法后一种可以看作第一种写法的一个语法糖而已。

至此,也是大致了解了\(\lambda\)-Calculus的能力与算法。接下来,让我们回到scheme,来看一下图灵停机问题。

图灵停机

停机其实是一个描述起来很简单的问题:是否存在一个函数对于任意函数它都能计算该函数在给定的输入是否会停止?

先让我们尝试写一下这个函数,首该先参数应该是个函数,

1
2
3
(define will-stop?
(lambda (f)
...))

我们希望will-stop?这个函数能在参数为可以停止的函数时返回true,否则返回true,这个好像很难写,我们先找几个例子试一下。于是我们写下来一个函数

1
2
3
4
(define eternity
(lambda (x)
(eternity x)
))

显然这个函数会无穷递归下去,显然我们希望

1
(will-stop? eternity)

的结果应该是false。 然后我们再定义一个函数

1
2
3
4
(define next-try
(lambda (x)
(and (will-stop? next-try)
(eternity x))))

在试一试这个函数,如果调用

1
(will-stop? next-try)

结果会怎么样呢?这个好像有点复杂,我们先猜一下,假设返回值是false。这样,语句

1
(and (will-stop? next-try) (eternity x))

会因为and的短路效果,只执行第一句,就意味着next-try这个函数会停止。等等,好像不太对,返回值是false不是意味着这个函数不会停止嘛?看样子,我们只能假设会返回true了,但是这样上面那条语句又会因为and,去执行后面那个停止不了的函数,从而导致next-try这个函数不会听着。两条路都走不通。 这就说明,will-stop?这个函数就不存在。 魔鬼存在于递归(自指)之中。

Y-combinator

最后终于到了今天的重点Y-combinator了,不过在得到Y-combinator之前,还有一些概念。

一些概念

首先定义不动点,所谓的不动点fixed-point就是指函数映射到自身的一个点。比如对于一个函数\(f(x) = x^2 -x + 1\)就有\(f(1) = 1\)这就可以称为函数f的一个不动点。粗看好像并不是所有的函数都有不动点,比如像\(f(x)= x+ 1\)这种函数就明显没有不动点。不动点的存在其实有着很深的含义,比如我们在求解方程的时候可以利用不断地迭代x、f(x)、f(f(x))来接近解。

先看一个常见的概念高阶函数(higher-order function),这个名字在编程时肯定比较常见,所谓的高阶函数就是至少满足下面一个条件: - 接受一个或多个函数作为输入 - 输出一个函数 其实很多函数式编程语言的map、filter等函数都是高阶函数的例子。高阶函数也叫做算子。在无类型的lambda演算中,所有的函数都是高阶的;而在函数式编程中返回另一个函数的高阶函数称为curry化函数。

我们把fixed-pointhigher-order function就来到了fixed-point combinator。如果一个以函数为参数f的不动点就是有一个函数g满足f(g)=g。如果一个函数fix满足对于所有的函数g都有g(fix)=fix即g(fix(g)) = fix(g),我们称为fixed-point combinator。而在我们之前见到的无类型lambda演算中的最简单的fixed-point combinator就称为Y-combinator

接近Y-combinator

从之前的lambda演算的过程可以发现,由于lambda的不存在命名,所以没有办法像写代码一样实现递归。这里就需要之前的fixed-point combinator出场了。如果我们能找到一个fixed-point的话,问题就解决了。看个例子,比如定义 Y为我们找到的fixed-point combinator,则

1
(Y g) = (g (Y g)) = (g (g (Y g)))

这样就可以利用Y combinator达到递归的能力了。

从递归的例子开始

让我们从一个例子开始,让我们写一个乘法

1
2
3
4
5
6
7
(define mult
(lambda (n)
(lambda (m)
(cond
((zero? n) 0)
(else
(+ m ((mult (sub1 n)) m)))))))

等价于lambda验算的 \[mult \doteq \lambda n.\lambda m.if\ (zero? \ n)\ 0 \ (add\ m\ (mult\ (sub1 \ n)\ m))\] 但是这种写法是不能直接按照那三个原则展开的。 既然没有办法直接写出来这个函数,就想办法写出来一个生成乘法的函数,然后慢慢改对。

1
2
3
4
5
6
7
8
(define mkmult0
(lambda (t)
(lambda (n)
(lambda (m)
(cond
((zero? n) 0)
(else
(+ m ((t (sub1 n)) m))))))))

函数mkmult0接受接受一个函数t(先不管接受的是什么函数),然后返回一个正常计算得到一个数一个数乘以0的值的函数。好,这里迈出了第一步。我们这试着用这种方法写出来一个满足乘以1的情况。怎么写呢?我们已经有一个满足0的情况了,当n为1的时候,在(sub1 n)之后得到的不就是0的情况了嘛!那我们就把mkmult0里面的t变成一个mkmult0接受任意一个参数返回之后的值就行了。

1
2
3
4
5
6
7
8
(define mkmult1
(lambda (t)
(lambda (n)
(lambda (m)
(cond
((zero? n) 0)
(else
(+ m (((mkmult0 t) (sub1 n)) m))))))))

好了,这样我们又得到了一个可以生成计算0、1的函数的函数了。再来一发,写个可以计算2的

1
2
3
4
5
6
7
8
(define mkmult2
(lambda (t)
(lambda (n)
(lambda (m)
(cond
((zero? n) 0)
(else
(+ m (((mkmult1 t) (sub1 n)) m))))))))

只要按照这个方法,我们只要写无穷次就能写出计算所有结果的函数了,可惜我们写不出无穷个。。。 不过观察一下这个函数,这几个函数都是很相似,唯一不懂的就是

1
(+ m (((mkmult* t) (sub1 n)) m))))))))

这里的mkmult*不太一样,而且不论是哪一个mkmult*都是在外面包了一层遇到0的情况而已,我们只要保证每次都能生成一个那样的函数同时能保证下次的展开就行了,这个形式直接写成

1
(+ m (((t t) (sub1 n)) m))))))))

就行了啊。

于是就有了,

1
2
3
4
5
6
7
8
9
(define mkmult-f
(lambda (t)
(lambda (n)
(lambda (m)
(cond
((zero? n) 0)
(else
(+ m
(((t t) (sub1 n)) m)))))))

然后,我们的乘法就是

1
2
(define mult
(mkmult-f mkmult-f))

终于,我们写完了这个乘法函数。

获取Y-combinator

有了这个例子,我们类比一下之前的想法,想得到一个对于函数mult的递归调用,我们在外面嵌入了(mkmult mkmult)的调用,那这个mk*函数又有什么可以抽象出来的呢? 回到这个乘法,我们把mkmult-f替换到进去,把整个展开

1
2
3
4
5
6
7
8
9
10
11
12
13
((lambda (f)
(f f))
(lambda (t)
(lambda (n)
(lambda (m)
(cond
((zero? n) 0)
(else
(+ m
(((lambda (x)
(lambda (y)
(((t t) x) y)))
(sub1 n)) m))))))))

为了把统一的部分区分开,这里把之前的(t t)写成了

1
2
(lambda (x)
((t t) x))

这个根据\(\eta\)替换应该是一样的。 然后我们进一步,把这个写在函数里面的调用当做参数,写到这个函数外面。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
((lambda (f)
(f f))
(lambda (t)
((lambda (multi)
(lambda (n)
(lambda (m)
(cond
((zero? n) 0)
(else
(+ m
((multi (sub1 n)) m)))))))
(lambda (x)
(lambda (y)
(((t t) x) y))))))

中间以multi为参数的又可以拿出来

1
2
3
4
5
6
7
8
9
10
11
12
13
14
((lambda (multi)
((lambda (mk-multi)
(mk-multi mk-multi))
(lambda (mk-multi)
(multi
(lambda (x)
(lambda (y)
(((mk-multi mk-multi) x) y)))))))
(lambda (multi)
(lambda (n)
(lambda (m)
(cond
((zero? n) 0)
(else (+ m ((multi (sub1 n)) m))))))))

仔细观察一下最下面,那不是我们想要的一般的递归的乘法的写法嘛!而前面的这部分,可以单独提出来称为一个函数,给他个名字Y

1
2
3
4
5
(define Y
(lambda (le)
((lambda (f) (f f))
(lambda (f)
(le (lambda (x) ((f f) x)))))))

这个就是我们想要的Y-combinator。 用lambda演算表示的话 \[Y \doteq \lambda f.(\lambda x.f\ (x \ x))\ (\lambda x.f\ (x \ x))\] 很容易可以计算出(Y g) = (g (Y g)),证明了这个是个fixed-point combinator

(Y g)
= (λf.(λx.(f (x x)) λx.(f (x x))) g)
= (λx.(g (x x)) λx.(g (x x)))(λf的β-归约 - 应用主函数于g)
= (λy.(g (y y)) λx.(g (x x)))(α-转换 - 重命名约束变量)
= (g (λx.(g (x x)) λx.(g (x x))))(λy的β-归约 - 应用左侧函数于右侧函数)
= (g (Y g))(Y的定义)

至此,终于得到了Y-combinator

参考引用:

  1. 《Programming Languages and Lambda Calculi》

  2. 《the little scheme》

  3. wiki上关于lambda演算的介绍




X