为什么定义丘奇数词

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次的平方得到的。

Answer 2

根据Peano axioms，一个自然数要么是0，要么是S(n)另一个自然数n:

0 = 0
1 = S(0)
2 = S(S(0))
...

您可以将教会数字视为皮亚诺数字的概括，您可以在其中提供自己的 0 和 S:

0 = λs.λz. z
1 = λs.λz. s(z)
2 = λs.λz. s(s(z))
...

由于这是一个编程论坛，让我们在 EcmaScript 6 中创建一些教堂数字：

const ZERO = s => z => z;
const ONE  = s => z => s(z);
const TWO  = s => z => s(s(z));
...

您可以通过提供适当的零和后续数字将这些教会数字转换为 JavaScript 数字：

function toInt(n) {
    return n(i => i + 1)(0);
}

然后：

> toInt(TWO)
2

您可以使用教会数字来做一些实际的事情：

function shout(text) {
    return text + "!";
}

> shout("hi")
"hi!"
> NINE(shout)("hi")
"hi!!!!!!!!!"

您可以在这里尝试：https://es6console.com/iyoim5y8/

Answer 3

下面的paper by Robert (Corky) Cartwright对我来说很好分解。

一开始要掌握的要点：

所有丘奇数都是带两个参数的函数；
在任何数字的教会表示中，都暗示：
- f — 是 'successor' 函数（即接受一个教会数字和 returns 教会数字的函数， 它基本上是和增量);
- x — 是一个（教会数字）值，表示 'zero'（计数起点）。

记住这一点：

λf . λx . x

将等于零，如果我们将传递适当的 f （'successor' — 增量函数）和 x （'zero' — 计数起点）。 在这种特殊情况下，什么函数将作为 f 传递并不重要，因为它从未应用过:

λf . λx . ZERO

这个：

λf . λx .  fx

将计算为 1:

λf . λx . INCREMENT ZERO

以及以下内容：

λf . λx . f f x

等于 2:

λf . λx . INCREMENT(INCREMENT ZERO)

依此类推，对于所有连续的数字。

奖金（教会数字的加法、乘法和求幂）：

这是一个 Python 代码片段来说明（并扩展）上面所说的：

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)))

SUCC = lambda x: x + 1

ADD = lambda f: lambda x: lambda n: lambda m: n(f)(m(f)(x))
MULT = lambda f: lambda x: lambda n: lambda m: n(m(f))(x)
EXPON = lambda m: lambda n: n(m)

ADD 利用了这样一个事实，即任何教会数字都接受 'zero' 计数起点，因为它是参数——它只从 m 开始计数到 n。所以，ADD(SUCC)(0)(THREE)(TWO) 只会数到 3，但从 2 开始，因此我们得到 2 + 1 + 1 + 1 = 5.

MULT 利用了一个事实，即 'successor' 函数只是一个 Church 数字的参数，因此可以被替换。因此 MULT(SUCC)(0)(TWO)(THREE) 将 return 3 两次，这与 2 * 3 = 6.

相同

EXPON 有点棘手（至少对我自己来说是这样），这里的关键 点是要跟踪 return 被什么[编辑的内容] =86=]。它基本上所做的是使用 Church 数字表示的内在机制（特别是 f 应用程序的递归）。下面举几个例子来说明：

3⁰

EXPON(THREE)(ZERO)(SUCC)(0) ↓ lambda n: n(THREE)(ZERO)(SUCC)(0) ↓ ZERO(THREE)(SUCC)(0) ↓ lambda x: (SUCC)(0) ↓ SUCC(0) ↓ 1

3¹

EXPON(THREE)(ONE)(SUCC)(0) ↓ lambda n: n(THREE)(ONE)(SUCC)(0) ↓ ONE(THREE)(SUCC)(0) ↓ lambda x: THREE(x)(SUCC)(0) ↓ THREE(SUCC)(0) ↓ 3

1³

EXPON(ONE)(THREE)(SUCC)(0) ↓ lambda n: n(ONE)(THREE)(SUCC)(0) ↓ THREE(ONE)(SUCC)(0) ↓ lambda x: ONE(ONE(ONE(x)))(SUCC)(0) ↓ ONE(ONE(ONE(SUCC)))(0) ↓ ONE(ONE(lambda x: SUCC(x)))(0) ↓ lambda x:(lambda x: (lambda x: SUCC(x)) (x))(x)(0) ↓ SUCC(0) ↓ 1

为什么定义丘奇数词

Why the definition of Church's Numerals

lambda-calculus