lambda-calculus - 为什么要定义Church's Numerals

Question

我想明白，为什么丘奇定义了这样的数字:

0 = λ f . λ x . x
1 = λ f . λ x . f x
2 = λ f . λ x . f f x
3 = λ f . λ x . f f f x
4 = λ f . λ x . f f f f x

背后的逻辑是什么？

为什么 0 表示如下:

0 = λ f . λ x . x

Answer 1

Church 并没有试图变得实际。他试图证明有关 lambda 演算表达能力的结果——原则上任何可能的计算都可以在 lambda 演算中完成，因此 lambda 演算可以作为研究可计算性的理论基础。为了做到这一点，有必要将数字编码为 lambda 表达式，以便像后继函数这样的东西很容易定义。这是证明 lambda 演算与 Gödel's recursive function theory 等价的关键步骤(这是关于自然数的可计算函数)。教会数字基本上是一种方便的数字编码，尽管不是很易读。从某种意义上说，它没有任何很深的逻辑。声明并不是 1 的本质是 λ f . λ x . f x ，但后者是前者的有用编码。

这并不意味着它是任意编码。它有一个明确的逻辑。最自然的数字编码方式 n是由涉及 n 的事情引起的.教堂数字使用 n功能应用。自然数n由应用函数 n 的高阶函数表示次输入。 1由一次应用的函数编码，2通过应用两次的函数，依此类推。这是一种非常自然的编码，尤其是在 lambda 演算的上下文中。此外，很容易在它们上定义算术这一事实简化了 lambda 演算等同于递归函数的证明。

要在实践中看到这一点，您可以运行以下 Python3 脚本:

#some Church numerals:

ZERO = lambda f: lambda x: x
ONE = lambda f: lambda x: f(x)
TWO = lambda f: lambda x: f(f(x))
THREE = lambda f: lambda x: f(f(f(x)))

#function to apply these numerals to:

def square(x): return x**2

#so ZERO(square), ONE(square), etc. are functions
#apply these to 2 and print the results:

print(ZERO(square)(2), ONE(square)(2), TWO(square)(2),THREE(square)(2))

输出:

2 4 16 256

请注意，这些数字是通过将两个数字分别平方 0 次、1 次、2 次和 3 次而获得的。