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.
上一篇:System.Dynamic.ExpandoObject 类型的简单使用


下一篇:iOS 设置系统音量和监听系统音量变化