成功函数的定义

Posted 2023-03-15

【中文标题】成功函数的定义

【英文标题】：Definition of success function

【发布时间】：2021-08-10 23:58:49

【问题描述】：

在教堂数字中，如果我们有：

# (define zero (lambda (f) (lambda (x) x)))
zero = lambda f: lambda x: x

那么后继函数可以定义为：

# (define succ (lambda (n) (lambda (f) (lambda (x) (f ((n f) x))))))
succ = lambda n: lambda f: lambda x: f(n(f)(x))

也许这是一个愚蠢的问题，但如果继任者实质上在前面的等式中添加了一个包装器f(...)，为什么不能将其定义为f(n)？这更多是为了定义的一致性，还是为什么不能使用更短的形式？

（注意：这里使用 python 定义以及方案，因为它使我测试起来更简单。）

【参考方案1】：

数字n被定义为n函数f对某个参数x的应用。

因此，

0 = λf.λx.x
1 = λf.λx.f x
2 = λf.λx.f (f x)
3 = λf.λx.f (f (f (x))
...

请注意，1 与λf.λx.f 0 不同，所以succ 0 也不相同。 （其他数字也一样。）

你的定义，λn.λf.λx.(f n) 会给出

succ 0 = (λn.λf.λx.(f n)) (λg.λy.y)
       = λf.λx.f (λg.λy.y)

和1不一样，但是

 (λn.λf.λx.f (n f x)) (λg.λy.y)
= λf.λx.f ((λg.λy.y) f x)
= λf.λx.f ((λy.y) x)
= λf.λx.f x
= 1