Lambda演算之Y-Combinator的推导

上一节中,我们讲到了如何使用λ演算来描述自然数,可以看出λ演算的表现力确实非常强大,然而遗憾的是,由于lambda演算中使用的都是匿名函数,所以它无法很直观地表述递归。 如果缺少了递归,λ演算的能力无疑会大打折扣。

所有基于λ演算的语言中,其实都是支持对过程进行命名的,那为什么这里我们还需要探讨匿名函数的递归呢?

  1. 为了保持纯洁性,我们希望仅仅通过λ演算的规则本身来解决递归的问题。
  2. 部分语言对过程的命名必须等到该过程定义完成后才可以进行,这个时候我们必须找到一种方式使其能够很容易地获得递归的能力。

下面我们就是用factorial函数为原型,来看看如何使用lambda演算基本的规则,为其增加递归的能力。

传统定义方式,不过这个方式不符合我们的需求,因为它使用到了函数自身fact。

(defn fact [n] (if (<= n 0) 1 (* n (fact (dec n)))))
(assert (= (fact 5) 120))

几乎所有的问题解决过程都可以通过分层来解决,既然它不允许我们直接使用fact,那我们是不是可以直接把fact作为函数传入呢?

(defn fact2 [self n] (if (<= n 0) 1 (* n (self self (dec n)))))
(assert (= (fact2 fact2 5) 120))

为了后续处理方便,我们先对该函数进行currying。

(defn fact3 [self] (fn [n] (if (<= n 0) 1 (* n ((self self) (dec n))))))
(assert (= ((fact3 fact3) 5) 120))

((self self) (dec n)) 是不是有点丑陋,我们知道λ演算是数学家们搞出来的,他们对构造形式是有很严重的洁癖的。既然我们就是函数本身,为什么还需要(self, self)这样多此一举呢。 如果我们的定义能变成下面这样就比较完美了。

(defn fact3 [self] (fn [n] (if (<= n 0) 1 (* n (self (dec n))))))

或者换成二元形式

(defn fact3 [f, n] (if (<= n 0) 1 (* n (f (dec n)))))

这样也许更符合数学家们的口味,但是该函数是无法被直接执行的,这个使我们暂时假定的factorial的理想函数形式。为了构造这个理想函数形式,我们不妨把它变成(f (dec n)),下面我们试着把(self self)拎出来,用作参数f传入。

(defn fact4 [self]
  (fn [n] (letfn [(fac-gen [f] (if (<= n 0) 1 (* n (f (dec n)))))]
            (fac-gen (self self)))))
(assert (= ((fact4 fact4) 5) 120))

我们来看fac-gen的形式,其等价于

(defn fac-gen [f] (if (<= n 0) 1 (* n (f (dec n)))))

是不是和我们理想中的fact形式已经很接近了,当然其中有一个自由变量n,没关系,我们给他加个帽子。

(defn fact5 [self]
  (fn [n]
    (letfn [(fac-gen [f]
              (fn [n] (if (<= n 0) 1 (* n (f (dec n))))))]
      ((fac-gen (self self)) n))))
(assert (= ((fact5 fact5) 5) 120))

这次的fac-gen和我们的理想函数形式非常像了,换成二元就是

(defn fac-gen [f, n] (if (<= n 0) 1 (* n (f (dec n)))))

这正是我们找寻的理想形式。

(defn fact6 [self]
  (letfn [(fac-gen [f]
            (fn [n] (if (<= n 0) 1 (* n (f (dec n))))))]
    (fn [n] ((fac-gen (self self)) n))))
(assert (= ((fact6 fact6) 5) 120))

让我们把fac-gen抽出来,作为一个单独的函数,它刚好就是我们要构造的factorial函数的理想形式,并给出fact7函数的定义。

(defn fac-gen [f] (fn [n] (if (<= n 0) 1 (* n (f (dec n))))))
(defn fact7 [self]
  (fn [n] ((fac-gen (self self)) n)))
(assert (= ((fact7 fact7) 5) 120))

其实这个时候,fact7和factorial的计算过程已经没有什么关系了,换而言之,其实它可以更通用一些。

(defn fact8 [gen]
  (fn [self]
    (fn [n] ((gen (self self)) n))))
;; (fact8 fac-gen) = fact7
(assert (= (((fact8 fac-gen) (fact8 fac-gen)) 5) 120))

fact8其实和factorial的计算过程没有任何关系,所以我们不妨给它换个名字

(defn y [gen]
  (fn [self]
    (fn [n] ((gen (self self)) n))))
(assert (= (((y fac-gen) (y fac-gen)) 5) 120))

事实确是如此,该函数有一种神奇的能力,它不仅使可以计算factorial,它事实上可以计算所有形如factorial理想形式的函数递归。

(defn fib-gen [f] (fn [n] (if (<= n 2) 1 (+ (f (dec n)) (f (- n 2))))))
(assert (= (((y fib-gen) (y fib-gen)) 1) 1))
(assert (= (((y fib-gen) (y fib-gen)) 2) 1))
(assert (= (((y fib-gen) (y fib-gen)) 3) 2))
(assert (= (((y fib-gen) (y fib-gen)) 4) 3))
(assert (= (((y fib-gen) (y fib-gen)) 5) 5))
(assert (= (((y fib-gen) (y fib-gen)) 6) 8))

(defn range-gen [f] (fn [n] (if (<= n 0) () (conj (f (dec n)) n))))
(assert (= (((y range-gen) (y range-gen)) 5) (list 5 4 3 2 1)))

我们看下我们的调用,都是形如:(((y *-gen) (y *-gen)) n)的形式,还是相当丑陋的,我们不如精简下,简化其调用过程。

(defn y1 [gen]
  (letfn [(g [self] (fn [n] ((gen (self self)) n)))]
    (g g)))
(assert (= ((y1 range-gen) 5) (list 5 4 3 2 1)))
(assert (= ((y1 fib-gen) 6) 8))
(assert (= ((y1 fac-gen) 5) 120))

去除letfn,把self使用f替换。

(defn Y [gen]
  ((fn [g] (g g))
    (fn [f]
      (fn [n] ((gen (f f)) n)))))
(assert (= ((Y range-gen) 5) (list 5 4 3 2 1)))
(assert (= ((Y fib-gen) 6) 8))
(assert (= ((Y fac-gen) 5) 120))

说了这么多,这个东西和Y Combinator又有什么关系?其实,我们最终得出的Y函数,其实就是我们所要苦苦找寻的Y Combinator函数,它具有性质Y(F) = F(Y(F)) = F(F(Y(F)))。

(assert (= ((fac-gen (Y fac-gen)) 5) 120))
(assert (= ((fac-gen (fac-gen (Y fac-gen))) 5) 120))

不动点组合子(Y Combinator)

函数f的不动点是一个值x使得f(x) = x。例如,0和1是函数f(x) = x**2的不动点,因为0**2 = 0而1**2 = 1。鉴于一阶函数(在简单值比如整数上的函数)的不动点 是个一阶值,高阶函数f的不动点是另一个函数g使得f(g) = g。那么,不动点算子是任何函数fix使得对于任何函数f都有 f(fix(f)) = fix(f).

在无类型lambda演算中众所周知的(可能是最简单的)不动点组合子叫做Y组合子。它是Haskell B. Curry发现的,定义为Y = λf.(λx.f (x x)) (λx.f (x x))用一个例子函数g来展开它,我们可以看到上面这个函数是怎么成为一个不动点组合子的:

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的定义)

根据定义得出的函数如下,但是它毫无用武之地,当把参数应用到它之上时,它将会进入无穷递归。

(defn y [f]
  ((fn [x] (f (x x)))
    (fn [x] (f (x x)))))

当该函数应用到f上时,当有

((fn [x] (f (x x))) (fn [x] (f (x x)))))

let g = (fn x) 当有如下的执行过程

(f (g g)) = (f ((fn [x] (f (x x))) g))
          = (f (f (g g)))
          ...
          = (f ... (f (g g)))

由于此处总是eager load,故此函数会进入无穷递归。

有没有办法让(f (x x))不展开呢? 可以,只需要加个lambda就可以使其变成lazy load。

(defn y1 [f]
  ((fn [x]
     #(f (x x)))
    (fn [x]
      #(f (x x)))))

由于新增的lambda没有参数,故在clojure中我们调用的函数也不能有参数,但是已经可以实现递归了,下面的例子会进入无穷递归。

((y1 (fn [f] (println :hello) (f))))

让我们给他加入参数,以便做支持更多的调用场景。

(defn y [f]
  ((fn [x] (fn [n] ((f (x x)) n)))
    (fn [x] (fn [n] ((f (x x)) n)))))
(assert (= ((y fac-gen) 5) 120))

上面的代码实现有明显重复的地方,根据DRY原则,我们稍稍对源代码进行下改造。

(defn Y [f]
  ((fn [g] (g g))
    (fn [x] (fn [args] ((f (x x)) args)))))
(assert (= ((Y fac-gen) 5) 120))

我们根据Y Combinator也同时得出了Y函数的定义,和我们之前根据factorial推演得出的结果一模一样。

让我们来证明下,我们的Y确实是一个通用的不动点组合子。

Y = λf.(λx.λn.f (x x) n) (λx.λn.f (x x) n)
Y g n  = (λf.(λx.λn.f (x x) n) (λx.λn.f (x x) n)) g n
       = (λx.λn.g (x x) n) (λx.λn.g (x x) n) n
       = (λy.λm.g (y y) m) (λx.λn.g (x x) n) n
       = (λm.g ((λx.λn.g (x x) n) (λx.λn.g (x x) n)) m) n
       = (λm.g (Y g) m) n
       = g (Y g) n

参考

  1. Lambda演算之自然数
  2. y-combinator演算示例代码
时间: 2016-04-12

Lambda演算之Y-Combinator的推导的相关文章

Lambda演算之Y-Combinator的推导(JS描述)

上一节中,我们讲到了如何使用λ演算来描述自然数,可以看出λ演算的表现力确实非常强大,然而遗憾的是,由于lambda演算中使用的都是匿名函数,所以它无法很直观地表述递归. 如果缺少了递归,λ演算的能力无疑会大打折扣. 所有基于λ演算的语言中,其实都是支持对过程进行命名的,那为什么这里我们还需要探讨匿名函数的递归呢? 1. 为了保持纯洁性,我们希望仅仅通过λ演算的规则本身来解决递归的问题. 2. 部分语言对过程的命名必须等到该过程定义完成后才可以进行,这个时候我们必须找到一种方式使其能够很容易地获得

基于文本替换的解释器及lambda演算

最近比较闲,打算整理一下之前学习的关于程序语言的知识.主要的内容其实就是一边设计程序语言一边写解释器实现它.这些知识基本上来自Programming Languages and Lambda Calculi和Essentials of Programming Languages这两本书. 我还记得高中奥数竞赛培训时的老师这样说过:"解题时一定要抓住定义." 编程和解题一样,也要抓住定义. 所以在写解释器前,得先定义好这门要解释的程序语言. 这门程序语言基于Lambda演算. 从\(\l

Y Combinator

由于匿名函数(通常成为lambda函数但是跟lambda calculus不同)在递归时无法获得函数名,从而导致一些问题,而Y Combinator能很好地解决这个问题.利用不动点的原理,可以利用一般的函数来辅助得到匿名函数的递归形式,从而间接调用无法表达的真正的匿名函数.下面以一个阶乘的递归来说明. #Python版本,后面会加上C++版本 #F(f) = f def F(f,n): return 1 if n==0 else n*f(n-1) #或者用lambda #F = lambda f

基于文本替换的解释器:递归定义与lambda演算的一些额外说明

这一篇接在第一篇lambda演算的后面.讲讲一些数学知识. 经常有些看似很容易理解的东西,一旦要描述得准确无误,就会变得极为麻烦. 软件工程里也有类似情况:20%的代码实现了核心功能,剩下80%的代码处理边界情况. 于是,所谓的准确描述里的大部分文字都在说明边界情况,核心概念只有寥寥几字--好比一件打满补丁的衣服,完全看不出原来的样子. 出现这种现象要么是人类的大脑有缺陷,难以严谨而又准确的理解概念,也就是说人类太笨: 要么就是语言系统有问题,难以简洁地表达概念,而发明不出新的语言系统的人类还是

对现有城市环境不满 孵化器Y Combinator打算自己建座城

美国科技创业公司孵化器Y Combinator合伙人阿多拉·常(Adora Cheung)周一表示,由于现有的城市无法提供获得成功所需的机会和居住环境,因此该公司将效仿其他科技公司的做法,自建一座城市. 包括Zappos和亚马逊在内的科技公司都公布了自建城市的计划,谷歌母公司Alphabet似乎也准备部署相似的计划. 阿多拉·常还着重强调自建城市试图解决的住房和交通问题.但该公司对改造其目前所在的加州山景城并无兴趣,而是希望在现行法律许可的情况下,从头建设一座最好的城市.不过,Y Combina

Y Combinator成功秘诀:“校友网络”异常强大

加速器正在成为创业生态系统中愈发重要的一部分. 它们在各地涌现,但没有哪家的名气能比得上位于硅谷的Y Combinator(以下简称"YC"). YC成立于2005年,迄今已在1,500位企业创始人身上投资了800万美元,在超过30个市场打造了400多家企业. 这些投资正在得到回报.去年,<福布斯>将YC评选为最有价值的孵化器,其地位领先于其他著名企业,如大卫·科恩(David Cohen)的TechStars和戴夫·麦克鲁尔(Dave McClure)的500 Start

硅谷梦旅人:Y Combinator的创业孵化经

新浪科技 郑峻 发自美国硅谷 青春是一场无悔的梦,创业就是追梦的旅程.无数的年轻人来到硅谷,在这个梦想的天堂挥洒自己的青春.追梦的旅程艰辛却并不孤单,因为硅谷有着全球最好的创业环境,帮助年轻人实现创业梦想.创业孵化器Y Combinator(以下简称YC)就是其中最为知名的梦旅人. YC的七年之旅 2005年3月,保罗·格拉汗姆(Paul Graham)对自己说:"我该为年轻人做点什么".当时他刚结束在哈佛大学的创业演讲,并将演讲内容编撰成书<如何开始创业>(How to

Y Combinator创始人预警:硅谷融资将面临艰难

中介交易 SEO诊断 淘宝客 云主机 技术大厅 Y Combinator联合创始人保罗·格雷厄姆(Paul Graham) 新浪科技讯 北京时间6月5日晚间消息,硅谷知名创业孵化器Y Combinator联合创始人保罗·格雷厄姆(Paul Graham)表示,硅谷融资的艰难时刻即将到来. 格雷厄姆在发送给其所投资公司的电子邮件中称:"Facebook IPO(首次公开招股)的糟糕表现将加大硅谷科技创业公司融资的难度,其影响有多大目前尚无法预测,可能很小,但也很可能很大." 格雷厄姆表示

Y Combinator创始人首次加入初创公司董事会

据国外媒体报道,对于他曾经帮助过的多家初创公司而言,Y Combinator创始人保罗•格雷厄姆(Paul Graham)可谓是一个教父级人物,但格雷厄姆从未进入其中任何一家公司的董事会.不过,格雷厄姆今日宣布,其已经同意加入医保众筹平台Watsi的董事会.Watsi筹集人们捐赠的资金,向那些缺乏医保的人提供帮助.Y Combinator此前决定资助Watsi,这是Y Combinator资助的首个非盈利性项目.具体来讲,Watsi帮助的对象是那些缺乏医保但又无力承担的人群.在Watsi的网站上