lambda - lambda 演算中的算术定义

Question

作为lambda calculus wiki说:

There are several possible ways to define the natural numbers in lambda calculus, but by far the most common are the Church numerals, which can be defined as follows:

0 := λf.λx.x
1 := λf.λx.f x
2 := λf.λx.f (f x)
3 := λf.λx.f (f (f x))

我只知道0定义中的λx.x部分是恒等函数，数字与f重复多少次有关(in 0 f repeated 0 time)，但为什么要这样定义，如何用容易理解的句子解释λf.λx.x(0) 和λf.λx.f (f x)(2)(尤其是什么f 代表)。

---

补充:这个定义有什么值得解释的地方吗？

Answer 1

因为一切都是 lambda 项，在 lambda 演算中你只能定义 lambda 项(函数)对其他 lambda 项(唯一允许的“值”，用λ 表示法)。

因此，如果我们想从理论上证明 lambda 演算允许人们编写任何可计算的函数，我们需要找到合适的表示(编码，在技术术语中) 的自然数，在其上定义可计算函数(请注意，使用 Church 编码，您通过 lambda 项表示 numbers ，而不是 numerals !)。

将数字编码为 lambda 项后，可以在“数字”上定义所有常用函数。例如，后继函数可以定义为:

SUCC := λn.λf.λx.f (n f x)

它接受一个“数字”(即，对数字进行编码的 lambda 项)并返回其后继(即，对该数字的后继进行编码的 lambda 项)。因此，例如，((SUCC) 0) β-减少到 1(即 ((λn.λf.λx.f (n f x)) λf.λx.x) 等价于 λf.λx.f x), 等等。以此为起点，可以定义“数”的所有其他函数，如求和、乘法、求幂等。

这样的编码有什么用呢？当然，给出一种实用的编程语言来执行两个数字的求和是没有用的。但它允许在 computability theory 领域研究这种形式主义，例如，提供一种表达 Church-Turing 论点的方式，该论点断言任何可计算运算符(及其操作数)都可以表示在 Church 编码下。