cgnail's weblog | A quantum of academic

为什么是Y?

| categories academic 
tags 翻译  lambda演算  function programming 

Good Math, Bad Math Lambda演算系列之四

在前面的几个帖子里,我已经建立了如何把lambda演算变成一个有用的系统的点点滴滴。 我们已经有了数字,布尔值和选择运算符。我们唯一欠缺的是重复。

这个有点棘手。lambda演算使用递归实现循环(递归的解释可以看这里)。 但是,由于在lambda演算里函数没有名字,我们得采取一些非常手段。这就是所谓的Y组合子,又名lambda不动点运算符。

让我们先来看看lambda演算之外的一个简单的递归函数。阶乘函数,这是标准的例子:

factorial(n) = 1 if n = 0 
factorial(n) = n * factorial(n-1) if n > 0 

如果我们要用lambda演算来写的话,我们需要几个工具……我们需要一个测试是否为零的函数,一个乘法函数,以及一个减1的函数。

为了检查是否为零,我们将使用一个命名函数IsZero,它有三个参数:一个数字,两个值。如果数字为0,则返回第一个值;如果它不为0,则返回第二个值。

对于乘法——我们在制定出递归之前写不出乘法。但我们可以假设目前有一个乘法函数 Mult x y

最后,减1函数,我们用Pred x表示x的前驱——即x - 1

所以——第一版的阶乘,如果我们把递归调用留做空白的话,将是:

lambda n . IsZero n 1 (Mult n ( something (Pred n))) 

现在的问题是,我们怎么填上“something”,使其递归?

答案是一些所谓的组合子。一个组合子是一种特殊的高阶函数,它们只引用函数应用。(一个高阶函数是一个函数,它接受函数作为参数,并且返回的结果也是函数)。Y组合子非常特殊,它有近乎神奇的功能使得递归成为可能。它的样子如下:

let Y = lambda y . (lambda x . y (x x)) (lambda x . y (x x)) 

看了公式,你就就明白为什么叫它Y了,因为它的“形状”像一个Y。为了让这一点更清晰,有时我们把它写成树的形式。下面是Y组合子的树:

y-combinator

Y组合子的特别之处在于它应用自身来创造本身,也就是说 (Y Y) = Y (Y Y)。让我们从(Y Y)开始看看它如何工作:

  • Y Y
  • 展开第一个Y(lambda y . (lambda x . y (x x)) (lambda x . y (x x))) Y
  • 现在,beta规约:(lambda x . Y (x x)) (lambda x . Y (x x))
  • alpha[x/z]变换第二个lambda:(lambda x . Y (x x)) (lambda z. Y (z z))
  • beta规约:Y ((lambda z. Y (z z)) (lambda z. Y (z z)))
  • 展开前面的Y,并alpha[y/a][x/b]变换:(lambda a . (lambda b . a (b b)) (lambda b . a (b b))) ((lambda z . Y (z z)) ( lambda z . Y (z z)))
  • beta规约:(lambda b . ((lambda z. Y (z z)) (lambda z. Y (z z))) (b b)) (lambda b . ((lambda * z. Y (z z)) (lambda z. Y (z z))) (b b))

现在,仔细看该表达式。这是(Y (Y Y)) [记得前面的(Y Y) = (lambda x . Y (x x)) (lambda x . Y (x x))吧]。所以, Y Y = Y (Y Y),这是Y的魔力:它再造了本身。(Y Y) = Y (Y Y) = Y (Y (Y Y)),子子孙孙无穷匮也。

那么,我们如何使用这个疯狂的玩意?

好吧,让我们拿我们的第一次尝试做一下修改。给它取个名字,并尝试使用该名字重写:

let fact = lambda n . IsZero n 1 (Mult n (fact (Pred n))) 

现在的问题是,“fact”不是“fact”中定义的标识符。我们如何让“fact”引用“fact”呢?好了,我们可以做一个lambda抽象,让“fact”函数作为参数传过去;于是,如果我们能找到一种方法来写“fact”,使得我们可以把它作为一个参数传给它自己,事情就搞定了。我们称之为metafact。

let metafact = lambda fact . (lambda n . IsZero n 1 (Mult n (fact (Pred n)))) 

现在,如果我们可以应用metafact到本身,我们就得到了我们的阶乘函数。也就是说,

fact n = (metafact metafact) n 。
        <= (lambda f1 . lambda t1 .  t1 ? 1 : t1 * f1 (P(t1))) (lambda f2 . lambda t2 .  t2 ? 1 : t2 * f2 (P(t2))) n  
        <= (lambda t1 .  t1 ? 1 : t1 * (lambda f2 . lambda t2 .  t2 ? 1 : t2 * f2 (P(t2))) (P(t1))) n
        <= lambda n .  n ? 1 : n * (lambda f2 . lambda t2 .  t2 ? 1 : t2 * f2 (P(t2))) (P(n))
        <= lambda n .  n ? 1 : n * (lambda f2 .  P(n) ? 1 : P(n) * f2 (P(P(n))) ) 
        <= lambda n .  n ? 1 : n * (lambda f .  (P(n) ? 1 : P(n) * f (P(P(n))) )
        <= lambda n . n ? 1 : n * (lambda f . f (P(n)))
        <= lambda f . lambda n . n ? 1 : n * f (P(n))
        <= f (n)

这正是Y的用武之地。它让我们可以创建一个古怪的结构,每次需要递归的时候都可以复制函数过来。metafact (Y metafact)将得到我们想要的。展开之,这就是:

(lambda fact . (lambda n . IsZero n 1 (Mult n (fact (Pred n))))) (Y (lambda fact . (lambda n . IsZero n 1 (Mult n (fact (Pred n)))))) 

(Y metafact)实际上是第一个lambda中参数fact的值;当我们对它做beta规约的时候,如果n为零,那么它只是返回1,如果它不为零,那么它调用fact (Pred n)。 然后再将factbeta规约为Y metafact, 这个变换疯狂地复制,得到输出metafact (Y metafact) (Pred n)

瞧,递归(metafact (Y metafact) = metafact (Y metafact) (Pred n))。极度扭曲的递归。

我第一次了解了Y组合子是在本科,1989左右,至今我仍然觉得它很神秘。我虽然也明白它是怎么来的,但我无法想象地球上怎么会有人把它给想出来!

如果你对此很长感兴趣,那么我极力推荐「The Little Schemer」这本书。这是本非常棒的小书 —— 写得象一本儿童读物。书里要么每一页正面是一个问题,背面就是答案,要么一页分成两栏,一栏问题一栏答案。书的风格轻松幽默,不仅教你Scheme编程,更教人怎么思考。

一个重要的提示:实际上有几个不同的版本的Y组合子。也有几种不同的lambda演算的计算方式:给定以下表达式:

(lambda x y . x * y) 3 ((lambda z . z * z) 4) 

我们可以按不同的顺序来计算:我们可以首先对(lambda x y . x * y)做beta规约,于是有:

3 * ((lambda z . z * z) 4) 

或者,我们可以先beta规约((lambda z . z * z) 4)

(lambda x y . x * y) 3 (4 * 4) 

在这种情况下,两种方式得到相同的结果;但事实并非总是如此。

第一种顺序就是我们所说的「惰性求值」(Lazy evaluation):我们不计算函数的参数,直到我们需要使用它们。第二种叫「急切求值」(eager evaluation):我们总是在把参数传递给函数之前进行计算。(在实际的编程语言中,Lisp语言,Scheme,和ML使用急切求值计算lambda演算,Haskell和Miranda则使用惰性值计算lambda演算。)我上面描述的Y组合子是惰性求值。如果我们用急切求值,那么上述Y组合子是导不出来的——事实上,它会永远地复制Y。

一点个人解释

Y在定义递归函数中的作用

首先,在lambda演算中,函数名不是不可缺少的,没有函数名的函数称为「匿名函数」。lambda符号的引入就是为了去掉函数名这个冗余,使定义匿名函数成为可能。但是当需要定义的函数含有递归时,比如阶乘factorial,也就是函数的定义部分需要引用函数自身的时候,没有函数名意味着用lambda演算无法直接引用函数自身。怎么办呢?

一种办法是设计另一个函数G,它接受一个函数作为参数,返回值也是一个函数(这种参数是函数的函数称为高阶函数)。然后,我们把factorial当做参数传给G,如果G返回的函数也是factorial的话,就圆满了。也就是说,这个G需要满足两个特征:

  1. G的定义中不会出现factorial,但是它可以接受factorial作为参数。回想一下一阶函数f(x) = x * x,它的定义里没有出现数字「1」,但是「1」可以传给它进行计算。而在构造G时,factorial就相当于数字「1」。
  2. 方程G(f)=f的解是factorial。这样我们就不用直接定义factorial,求解这个关于G的方程就可以得到factorial的定义了。

于是,我们需要干两件事:找到G,和找到求解G(f)=f的办法。寻找G很简单,既然我们想让G(factorial)=factorial,那么把factorial定义中关于factorial的引用参数化就可以了,即:

let G = lambda f . lambda n . IsZero n 1 (Mult n ( f (Pred n))) 

这就是上面的metafact函数。这种构造方法可以用于构造任意递归函数的「G」。

然后我们需要找到求解方程G(f)=f的办法。满足f(x)=x的x称为函数f的不动点,f是高阶函数时也不例外。Y组合子的作用就是计算函数的不动点,它对所有的函数f都满足f(Y(f)) = Y(f),推理如下:

Y (f) = (lambda y . (lambda x . y (x x)) (lambda x . y (x x))) f
    = (lambda x . f (x x)) (lambda x . f (x x)) 
    = (lambda x . f (x x)) (lambda a . f (a a))
    = f ((lambda a . f (a a)) (lambda a . f (a a)))
    = f ((lambda x . f (x x)) (lambda x . f (x x)))
    = f (Y(f))

于是,factorial的定义就可以写成:

factorial n = (Y metafact) n 
            = {[lambda y . (lambda t . y (t t)) (lambda t . y (t t))]
               [lambda f . lambda n . IsZero n 1 (Mult n ( f (Pred n)))]} n

这下不用引用自身了。

Y怎么来的

现在回到第一版的阶乘。我们虽然不能直接引用自身,但可以把它作为参数传进来,也就是说:

let fact2 = lambda f. lambda n . IsZero n 1 (Mult n ( f (Pred n))) 

这样,在计算5的阶乘时,我们只需要计算fact2(fact2, 5)就可以了。定义并没有引用自身,只是在使用的时候把自己当参数传过去。是不是很简单?

但是,这个计算式是错误的:fact2的定义要求它接受两个参数,其中参数f是只接受一个参数的函数,于是计算式中第二个的fact2在参数数量上是无法和定义中的f匹配的。那怎么办?

不要紧,我们可以修改一下f的形式,让它接受两个参数。即:

let fact3 = lambda f. lambda n . IsZero n 1 (Mult n ( f [f, (Pred n)])) 

这下计算fact3(fact3, 5)就不会出错了。除了这个定义有点丑……

如果对fact3做下化简又如何呢?首先是对拥有两个参数的f进行柯里化变换:

let fact3 = lambda h . lambda n . IsZero n 1 (Mult n ( h h (Pred n))) 
          = lambda h . lambda n . IsZero n 1 (Mult n ( (h h) (Pred n)))

这样计算阶乘的方式也相应变成了(fact3 fact3) 5。接着把(h h)用函数q代替,则有

let fact3 = lambda h . lambda n . [lambda q . IsZero n 1 (Mult n ( q (Pred n)))] (h h)
          = lambda h . [lambda n . lambda q . IsZero n 1 (Mult n ( q (Pred n)))] (h h)

仔细观察中括号部分,参数h对于这部分是完全自由的,于是我们可以用另一个函数定义替换之:

let f0 = lambda n . lambda q . IsZero n 1 (Mult n ( q (Pred n)))
let fact3 = lambda h . f0 (h h)

是不是觉得f0眼熟?没错,这就是metafact!不过我们先把f0放一边,看看如何使用这个定义计算n的阶乘。

factorail n = (fact3 fact3) n 
            = (lambda h . f0 (h h)) (lambda h . f0 (h h)) n

把上面的式子写成 function_name x的形式:

factorial n = {[lambda f . (lambda h . f (h h)) (lambda h . f (h h))] f0} n

注意大括号中的部分,是不是更眼熟了?这就是Y的定义。真是怎么绕都扰不过去的Y啊……

factorial n = {[lambda f . (lambda h . f (h h)) (lambda h . f (h h))] f0} n
            = {Y f0} n
            = (Y metafact) n
If you liked this post, you can share it with your followers !