use*_*246 17 lambda-calculus reduction
我对lambda演算中的前身函数的维基百科描述感到困惑.
维基百科所说的如下:
PRED:=λnfx.n(λgh.h(gf))(λu.x)(λu.u)
有人可以一步一步地解释减少过程吗？
谢谢.
C. *_*ann 25
好吧,所以教会数字的想法是用函数编码"数据",对吧？可行的方法是通过您使用它执行的某些通用操作来表示值.因此,我们也可以走向另一个方向,这有时可以使事情变得更加清晰.
教会数字是自然数字的一元表示.所以,让我们Z用来表示零,并Sn代表继承者n.现在,我们可以算这样的:Z,SZ,SSZ,SSSZ...等效教会数字有两个参数-第一个对应S,二来Z--then使用它们来构建上面的图案.因此,给定的参数f和x,我们可以算这样的:x,f x,f (f x),f (f (f x))...
让我们来看看PRED的作用.
首先,它创建了一个带有三个参数的lambda-- n是教会数字,我们想要的前任,当然,这意味着f并且x是结果数字的参数,这意味着该lambda的主体将被f应用于x一次少于n.
接下来,它适用n于三个参数.这是棘手的部分.
Z与之前对应的第二个参数是 - ?u.x一个忽略一个参数并返回的常量函数x.
S与之前相对应的第一个参数是?gh.h (g f).我们可以重写这一点,?g. (?h.h (g f))以反映只有最外面的lambda被应用的事实n.这个函数的作用是将累积的结果带到目前为止g并返回一个带有一个参数的新函数,该函数将该参数g应用于f.当然,这绝对令人困惑.
那么......这里发生了什么？考虑用S和直接替换Z.在非零数字中Sn,n对应于绑定的参数g.所以,记住,f并x在外部范围的约束,我们可以算这样的:?u.x,?h. h ((?u.x) f),?h'. h' ((?h. h ((?u.x) f)) f)...表演明显下降,我们得到:?u.x,?h. h x,?h'. h' (f x)...这里的模式是一个功能被传递"向内"一层,一个S将应用它,而一个Z将忽略它.所以我们除了最外层之外f每个应用程序都有一个应用程序.S
第三个参数只是身份函数,它由最外面的人尽职尽责地应用S,返回最终结果 - f应用的次数少于S层数n对应的次数.
麦肯的答案很好地解释了它.让我们来看看Pred 3 = 2的一个具体例子:
考虑表达式:n(λgh.h(gf))(λu.x).设K =(λgh.h(gf))
对于n = 0,我们进行编码0 = ?fx.x,因此当我们应用beta减少时,(?fx.x)(?gh.h(gf))均值(?gh.h(gf))被替换为0次.进一步降低beta后,我们得到:
?fx.(?u.x)(?u.u)
减少到
?fx.x
在哪里?fx.x = 0,如预期.
对于n = 1,我们应用K 1次:
(?gh.h (g f)) (?u.x)
=> ?h. h((?u.x) f)
=> ?h. h x
对于n = 2,我们应用K 2次:
(?gh.h (g f)) (?h. h x)
=> ?h. h ((?h. h x) f)
=> ?h. h (f x)
对于n = 3,我们应用K 3次:
(?gh.h (g f)) (?h. h (f x))
=> ?h.h ((?h. h (f x)) f)
=> ?h.h (f (f x))
最后,我们得到了这个结果并对它应用了一个id函数
?h.h (f (f x)) (?u.u)
=> (?u.u)(f (f x))
=> f (f x)
这是2号的定义.
基于列表的实现可能更容易理解,但需要许多中间步骤.所以它不如教会最初的实施IMO那么好.