logic - 为什么 lambda 演算中的变量集通常定义为可数无穷大？

Question

在阅读 lambda 演算的正式描述时，变量集似乎总是被定义为可数无穷大。为什么这个集合不能是有限的似乎很清楚；将变量集定义为有限会以不可接受的方式限制术语构造。但是，为什么不允许集合是不可数无限的呢？

目前，我收到的对这个问题的最明智的回答是，选择可数无限的变量集意味着我们可以枚举变量，从而自然地描述如何选择新变量，比如 alpha 重写。

我正在寻找这个问题的明确答案。

Answer 1

数学和逻辑中的大多数定义和构造仅包括实现所需目标所需的最小设备。正如您所注意到的，可能需要超过有限数量的变量。但是既然只需要一个可数的无穷大，为什么要允许更多呢？

Answer 2

有一个可数的变量，以及它们和 ℕ 之间的可计算双射，让我们在 Λ 和 ℕ 之间创建一个双射：

1. #v = ⟨0, f(v)⟩，其中 f 是和ℕ（因为可数而存在）和⟨m之间的可计算双射，n⟩是ℕ<sup>2和ℕ之间的可计算双射。
2. #(LM) = ⟨1, ⟨#L, #M⟩⟩
3. #(λv.L) = ⟨2, ⟨#v, #L⟩⟩

符号⌜L⌝代表c_{#L}，教会数字代表L的编码。对于所有集合S，#S代表集合{#L | L ∈ S}。

---

这使我们能够证明 lambda 演算是不可判定的：

令 A 是在 α 和 β 等式下封闭的非平凡（不是 ∅ 或 Λ）集（如果 L ∈ A 且 L β= M, M ∈ A）。令 B 为集合 {L | L⌜L⌝ ∈ A}。假设集合 #A 是递归的。那么 f，对于其中 f(x) = 1 如果 x ∈ A 和 0 如果 x ∉ A，必须是一个μ 递归函数。所有 μ 递归函数都是 λ 可定义的*，因此必须有一个 F 满足：

F⌜L⌝ = c_1 ⇔ ⌜L⌝ ∈ A
F⌜L⌝ = c_0 ⇔ ⌜L⌝ ∉ A

通过让 G ≡ λn。iszero (F ⟨1, ⟨n, #n⟩⟩) M_0 M_1，其中 M_0 是 B 中的任何 λ-项，M_1 是不在 B 中的任何 λ-项。请注意，#n 是可计算的，因此是可定义的。

现在只要问“G⌜G⌝在B中吗？”这个问题。如果是，那么 G⌜G⌝ = M_1 ∉ B，所以 G⌜G⌝ 不可能在 B 中（记住 B 在 β= 下是闭的）。如果不是，则 G⌜G⌝ = M_0 ∈ B，所以它一定在 B 中。

这是一个矛盾，所以 A 不可能是递归的，因此没有封闭的β=非平凡集合是递归的。

注意 {L | L β= true} 在 β= 下是封闭的并且是非平凡的，因此它不是递归的。这意味着 lambda 演算是不可判定的。

---

* 证明所有可计算函数都是 λ 可定义的（我们可以有一个 λ 项 F 使得 F c_{n1} c_{n2} ... = c_{f(n1, n2, ...)}），以及此答案中的证明，可以在Henk Barendregt 的“Lambda Calculi With Types”中找到（第 2.2 节）。

Answer 3

Uncountable collections of things seem to usually have uncomputable elements. I'm not sure that all uncountable collections have this property, but I strongly suspect they do.

As a result, you could never even write out the name of those elements in any reasonable way. For example, unlike a number like pi, you cannot have a program that writes out the digits Chaitin's constant past a certain finite number of digits. The set of computable real numbers is countably infinite, so the "additional" reals you get are uncomputable.

I also don't believe you gain anything from the set being uncountably infinite. So you would introduce uncomputable names without benefit (as far as I can see).

Answer 4

要求这个集合是可数的原因很简单。想象一下，你有一个装满变量的袋子。除非集合是可数的，否则无法计算此包中的变量数。

请注意，袋子与麻袋同构。