lambda - 教堂数字：如何在 lambda 演算中编码零？

Question

我正在学习 lambda 演算，但我似乎无法理解数字 0 的编码。

“接受一个函数和第二个值并在参数上应用函数零次的函数”如何为零？还有其他方法可以编码零吗？这里有人可以帮我编码0吗？

Answer 1

参见维基百科：

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

Answer 2

“接受一个函数和第二个值并在参数上应用该函数零次的函数”当然不是零。这是一个零编码。当您处理普通的 lambda 演算时，您必须以某种方式对数字（以及其他原始类型）进行编码，并且对每种类型都有一些要求。例如，对自然数的一个要求是能够将 1 加到给定的数字上，另一个要求是能够区分零和更大的数字（如果您想了解更多，请查找“Peano Arithmetic”）。Dario 引用的流行编码为您提供了这两件事，它还通过一个函数表示整数 N，该函数执行fN 次（编码为参数） - 这是一种使用 naturals 的自然方式。

还有其他可能的编码 - 例如，一旦您可以表示列表，您就可以将 N 表示为 N 个项目的列表。这些编码各有利弊，但上面的一种是迄今为止最受欢迎的一种。

Answer 3

如果您学习 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。