lambda-calculus - 教会数字：我应该如何解释表达式中的数字？

Question

有人可以使用替换向我解释我们如何得到一个数字“零”或其余的自然数吗？

例如值：“零”

λf.λx.x

如果我将此表达式应用于另一个表达式：

"(λf.(λx.x)) a"

然后使用替换：

:=[a/f](λx.x)
:=(λx.x)

我错过了什么？我应该如何解释这些数字表达式？

Answer 1

教堂数字n是一个函数，它接受另一个函数f并返回一个适用f于其参数n时间的函数。所以0 a（0正如你所说，在哪里λf.λx.x ）返回λx.x，因为这适用a于x0 次。

1 a给你λx. a x，2 a给你λx. a (a x)等等。

Answer 2

以下是基于Erhan Bagdemir在sepp2k回答的评论中的论文的解释。

要掌握的要点：

• 所有 Church 数字都是两个参数的函数；
• 对于教堂数字，暗示：
  • f— 是“后继”函数（即接受一个教会数字并返回下一个教会数字的函数，它基本上是和 increment）；
  • x— 是一个（教会数字）值，表示“零”（计数起点）。

牢记这一点：

λf . λx . x

将等于零，如果我们将传递适当的f（在这种特殊情况下，将传递什么函数并不重要f，因为它从未应用过）并且x：

λf . λx . ZERO

下列的：

λf . λx .  fx

将被评估为 1：

λf . λx . INCREMENT ZERO

和这个：

λf . λx . f f x

将等于 2：

λf . λx . INCREMENT(INCREMENT ZERO)

依此类推，对于所有连续的数字。

请参阅我对另一个（但密切相关的）问题的（更广泛的）回答。

Answer 3

一个教堂数字 n，（比如 2，）表示对任何给定参数应用任何给定函数 n 次（这里是两次）的“动作”。

根据定义，教堂数字是一个带有两个参数的函数，即
1) 一个函数
2) 一个参数或表达式或值，所提供的函数应用于该参数或表达式或值。

当提供的函数是后继函数，并且提供的第二个参数是 Zero 时，您会得到数字。（2，在上面的例子中）

教会数字 2 的定义是，

λf . λx . f( f( x)) 

,这显然是一个带两个参数的函数。

在传递后继函数时，即 f(x)=x+1 作为第一个参数，零作为函数的第二个参数，我们得到...

f(f(0))  
=f(1) 
=2

这个解释有点简化，因为在 lambda 演算中，后继函数的定义和零没有显示出来。

参考：http ://www.cse.unt.edu/~tarau/teaching/GPL/docs/Church%20encoding.pdf 关于教堂编码的一个很好的解释