教堂数字：如何在 lambda 演算中编码零？
我正在学习 lambda 演算，但我似乎无法理解数字 0 的编码。
“接受一个函数和第二个值并对参数应用函数零次的函数”是如何为零的？还有其他方法可以对零进行编码吗？这里有人能帮我编码0吗？
I am learning lambda calculus but I cant seem to understand the encoding for the number 0.
how is "function that takes in a function and a second value and applies the function zero times on the argument" a zero? Is there any other way to encode zero? Could anyone here help me encode 0?
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（4）
当然，“接受一个函数和第二个值并对参数应用该函数零次的函数”不是零。它的编码为零。当您处理普通 lambda 演算时，您必须以某种方式对数字（以及其他基本类型）进行编码，并且每种类型都规定了一些要求。例如，自然数的一个要求是能够将给定数字加 1，另一个要求是能够区分零和更大的数字（如果您想了解更多信息，请查找“皮亚诺算术”）。 Dario 引用的流行编码为您提供了这两件事，并且它还通过执行某件事（编码为
f参数）N 次的函数来表示整数 N - 这是一种使用自然的自然方式。还有其他可能的编码 - 例如，一旦您可以表示列表，您就可以将 N 表示为包含 N 个项目的列表。这些编码各有优缺点，但上面的编码是迄今为止最流行的一种。
A "function that takes in a function and a second value and applies the function zero times on the argument" is, of course, not zero. It's an encoding of zero. When you deal with plain lambda calculus, you have to encode numbers (as well as other primitive types) in some way, and there are a few requirements dictated for each of these types. For example, one requirement for natural numbers is to be able to add 1 to a given number, and another is to be able to distinguish zero from bigger numbers (if you want to know more, look for "Peano Arithmetic"). The popular encoding that Dario quoted gives you these two things, and it is also representing an integer N by a function that does something (encoded as the
fargument) N times -- which is a kind of a natural way to use naturals.There are other encodings that are possible -- for example, once you can represent lists, you can represent N as a list of N items. These encodings have their pros and cons, but the one above is by far the most popular one.
请参阅维基百科：
See wikipedia:
如果您学习 Lambda 演算，您可能已经知道 λxy.y arg1 *arg2* 将减少为 arg2，因为 x 没有被替换，余数 (λy .y) 是恒等函数。
您可以用许多其他方式写零（即提出不同的约定），但使用 λxy.y 有充分的理由。例如，您希望零成为第一个自然数，因此如果您对其应用后继函数，您将得到 1、2、3 等。使用函数 λabc.b(abc)，您将得到 λxy.x(y ), λxy.x(x(y)), λxy.x(x(x(y))) 等，换句话说，你得到了一个完整的数字系统。
此外，您希望零成为加法的中性元素。通过后继函数 S := λabc.b(abc)，我们可以将 n+*m* 定义为 n S m，即n 次将后继函数应用到 m。我们的零 λxy.y 满足这一点，0 S m 和 m S 0 都减少到 m。
If you learn Lambda Calculus, you probably already know that λxy.y arg1 *arg2* will reduce to arg2, since the x is replaced by nothing, and the remainder (λy.y) is the identity function.
You could write zero in many other ways (i.e. come up with a different convention), but there are good reasons for using λxy.y. For instance, you want zero to be the first natural number, so that if you apply the successor function to it, you get 1, 2, 3 etc. With the function λabc.b(abc), you get λxy.x(y), λxy.x(x(y)), λxy.x(x(x(y))) etc., in other words, you get a whole number system.
Furthermore, you want zero to be the neutral element with respect to addition. With our successor function S := λabc.b(abc), we can define n+*m* as n S m, i.e., n times the application of the successor function to m. Our zero λxy.y satisfies this, both 0 S m and m S 0 reduce to m.
在通常的命令式编程语言中，我们有类似的 for 循环表示法
，其中我们将函数 foo 应用于当前状态，并通过这样做将当前状态修改为下一个状态。 （例如，递增变量）
您可以将教会表示法中的数字视为具有给定初始状态
z的 for 循环，以及应用于先前调用返回的每个状态的函数s。表示数字的 lambda 应该将这些作为参数。例如(λsz.sz)用于在初始状态上应用一个for 循环。使用这个逻辑，我们可以构造 0 的 λsz.z，因为我们知道该函数在初始状态上应用了零次，因此该数字代表 0。In usual imperative programming languages we have similar notation of for loops
where we apply function foo on the current state and by doing that, we modify the current state to the next state. (e.g. increment a variable)
You can think of numbers in church notation as for loops with its given initial state
zand a functionsapplied to each state returned by previous calls. The lambda representing a number should then take these as arguments. e.g.(λsz.s z)for applying one for loop cycle on the initial state. Using this logic we can construct λsz.z for 0 because we know that the function is applied zero times on the initial state, therefore the number represents 0.