有人可以向我解释如何使用替换来获得数字“零”或其他自然数吗？
例如值：“零”
λf.λx.x
如果我将此表达式应用于另一个表达式：
"(λf.(λx.x)) a"
然后使用替换：
:=[a/f](λx.x)
:=(λx.x)
我错过了什么？我应该如何解释这些数字表达式？
【问题讨论】：
λf.λx.x是零。
标签： lambda-calculus church-encoding
教堂数字n 是一个函数，它接受另一个函数f 并返回一个将f 应用于其参数n 次的函数。所以0 a（如你所说，0 是λf.λx.x
）返回λx.x，因为这适用于a 到x 0 次。
1 a 给你λx. a x，2 a 给你λx. a (a x) 等等。
以下是基于paper by Erhan Bagdemir 在answer by sepp2k 的评论中的解释。
要掌握的要点：
f — 是“后继”函数（即接受教会数字并返回下一个教会数字的函数，基本上是递增）；x — 是一个（教会数字）值，表示“零”（计数起点）。牢记这一点：
λf . λx . x
如果我们将传递适当的 f，则将等于 0（在这种特殊情况下，将作为 f 传递的函数并不重要，因为它从未应用）和x：
λf . λx . ZERO
以下：
λf . λx . fx
将被评估为 1：
λf . λx . INCREMENT ZERO
还有这个：
λf . λx . f f x
将等于 2：
λf . λx . INCREMENT(INCREMENT ZERO)
等等，对于所有连续的数字。
将我的(broader) answer 与另一个（但密切相关的）question 联系。
【讨论】：
一个教堂数字 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 关于教堂编码的一个很好的解释
【讨论】：