博客
关于我
强烈建议你试试无所不能的chatGPT,快点击我
Church 整数前驱的推导
阅读量:6693 次
发布时间:2019-06-25

本文共 1218 字,大约阅读时间需要 4 分钟。

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

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

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

见:

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.

 

转载于:https://www.cnblogs.com/sniperHW/p/3147382.html

你可能感兴趣的文章
iView3.x Anchor(锚点)组件 导航锚点
查看>>
Network --- Tcp Protocol
查看>>
sqlite效率探测
查看>>
React生命周期
查看>>
数据库 -- mysql表操作
查看>>
shutil 高级文件操作
查看>>
Itellij Idea全局搜索
查看>>
Android系统简介
查看>>
配置证书
查看>>
Oracle VM VirtualBox技巧
查看>>
uvm_svcmd_dpi——DPI在UVM中的实现(二)
查看>>
Crimm Imageshop 2.3。
查看>>
SQL AND和OR求值顺序
查看>>
买房必知的五大法律常识 助你安心顺利选房
查看>>
leetcode563
查看>>
剑指Offer 40 最小的k个数
查看>>
winform创建树形菜单的无限级分类
查看>>
面试问题总结
查看>>
HTML特殊转义字符列表
查看>>
2、NIO--缓冲区(Buffer)
查看>>