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.
  • 相关阅读:
    还记得吗
    PAT A 1065. A+B and C (64bit) (20)
    畅通project(杭电1863)
    cocos2d-x 3.0游戏实例学习笔记《卡牌塔防》第七步---英雄要升级&属性--解析csv配置文件
    热烈祝贺Polymer中文组织站点上线
    具体解释HTML中的window对象和document对象
    oc15--文档安装
    oc14--匿名对象
    oc13--pragma mark
    oc12--对象作为参数
  • 原文地址:https://www.cnblogs.com/sniperHW/p/3147382.html
Copyright © 2011-2022 走看看