zoukankan      html  css  js  c++  java
  • Church 整数前驱的推导

    Church 整数前驱的推导比其后继复杂得多,wiki中一个前驱的定义据王垠的博客里说,是他一个数学系的同学花一星期时间推导出来的,

    其定义确实比其它介绍lambda的文章中用pair来实现(据说是图灵的学长花了3个月时间才想出来的)的方式简单许多,本文记录自己学习这

    个定义的分析过程,Church 整数的详细介绍

    见:http://zh.wikipedia.org/wiki/%E9%82%B1%E5%A5%87%E6%95%B0

    pred = λnfx.((n (λgh. h (g f)) (λu. x)) (λu. u))
     
     pred 0 = λnfx.((n (λgh.h (g f)) (λu.x)) (λu.u)) λfx.x
    = λfx.((λfx.x (λgh.h (g f)) (λu.x)) (λu.u))
            = λfx.(((λx.x) (λu.x)) (λu.u))
            = λfx.((λu.x) (λu.u))
            = λfx.x
            = 0
     
     分析关键部分:((n (λgh.h (g f)) (λu.x)) (λu.u))
     对n=1,2,3...分别有
       (((λgh.h (g f)) (λu.x)) (λu.u))
     = ((λh.h ((λu.x) f)) (λu.u))
     = ((λh.h x) (λu.u))
     = ((λu.u) x)
     = x
     
      ((λgh.h (g f) ((λgh.h (g f)) (λu.x))) (λu.u))
     =(((λgh.h (g f)) (λh.h x)) (λu.u))=((λh.h ((λh.h x) f)) (λu.u))
     =((λh.h (f x)) (λu.u))
     =((λu.u) (f x))
     =(f x)
     
     可见((n (λgh.h (g f)) (λu.x))对于大于0的情况分别等于
     (λh.h x), ((λh.h (f x)), ((λh.h (f (f x))) ....
     
     (λu.u)的作用就是将第二个项 x, (f x), (f (f x)) ........提取出来:
     
     整个pred的核心就在((n (λgh.h (g f)) (λu.x))
     
     这里,为了理解方便,将0临时编码为(λh.h x),也就是第一次应用(λgh.h (g f)) (λu.x)
     后得到0,然后用(λgh.h (g f))作为后继函数作用在0上得到了1,(λh.h (f x)),
     再次应用得到2,(λh.h (f (f x)))...
     
     这就说明了为什么pred能获得n-1,n的丘奇编码中总共有n个f,总共产生n个(λgh.h (g f)),
     其中最右边一个应用到(λu.x)上得到0,剩下的n-1个相当于从0开始应用succ(在这里succ是(λgh.h (g f)) )
     n-1次,所以得到了n-1.
  • 相关阅读:
    hdu 4710 Balls Rearrangement()
    hdu 4707 Pet(DFS水过)
    hdu 4706 Children's Day(模拟)
    hdu 4712 Hamming Distance(随机函数暴力)
    csu 1305 Substring (后缀数组)
    csu 1306 Manor(优先队列)
    csu 1312 榜单(模拟题)
    csu 1303 Decimal (数论题)
    网络爬虫
    Python处理微信利器——itchat
  • 原文地址:https://www.cnblogs.com/sniperHW/p/3147382.html
Copyright © 2011-2022 走看看