【发布时间】：2009-09-26 19:17:57
【问题描述】：
我正在学习 lambda 演算，但我似乎无法理解数字 0 的编码。
“函数接受一个函数和第二个值并将函数应用于参数零次”如何为零？还有其他方法可以编码零吗？有人可以帮我编码 0 吗？
【问题讨论】：
标签： lambda theory lambda-calculus
【发布时间】：2009-09-26 19:17:57
【问题描述】：
“接受一个函数和第二个值并在参数上应用该函数零次的函数”当然不是零。这是一个零的编码。当您处理简单的 lambda 演算时，您必须以某种方式对数字（以及其他原始类型）进行编码，并且对每种类型都有一些要求。例如，自然数的一个要求是能够将 1 加到给定的数字上，另一个要求是能够区分零和更大的数字（如果您想了解更多，请查找“Peano Arithmetic”）。 Dario 引用的流行编码为您提供了这两件事，它还通过一个函数表示整数 N（编码为 f 参数）N 次——这是一种使用 naturals 的自然方式.
还有其他可能的编码——例如，一旦您可以表示列表，您就可以将 N 表示为包含 N 个项目的列表。这些编码各有优劣，但以上一种是迄今为止最流行的一种。
【讨论】：
-
这是我在 google 群组中提出的一个相关问题：假设我有一个函数 f。我如何证明这可以转换为自然数 0？为了推断我的函数 f 的行为类似于 0，我还需要哪些其他函数？
-
如果你想证明一个函数
f在通常的编码下为零，你需要证明对于所有g(f g x) == x。除了这些，你不需要知道任何事情。
0 ≡ λf.λx. x
1 ≡ λf.λx. f x
2 ≡ λf.λx. f (f x)
3 ≡ λf.λx. f (f (f x))
...
n ≡ λf.λx. fn x
【讨论】：
-
它没有回答问题，它只是重复了 OP 已经清楚知道的编码。他只是不明白 0 ≡ λf.λx 的方式或原因。 x（我也没有，这就是我在这里的原因哈哈）
如果你学过 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。
【讨论】：