math - 电感规范 : Top-down vs Bottom-up vs Rules of Inference?

Question

请多多包涵。我将首先描述书中的一个例子，然后在最后提出我的问题。

根据编程语言范式的文本:

Inductive specification is a powerful method of specifying a set of values. To illustrate this method, we use it to describe a certain subset S of the natural numbers N = {0, 1, 2, . . .}.

自顶向下定义:

一个自然数 n 在 S 中当且仅当

n = 0，或

n −3 ∈ S。

我们知道 0 ∈ S。因此 3 ∈ S，因为 (3 − 3) = 0 并且
0 ∈ S。类似地 6 ∈ S，因为 (6−3) = 3 且 3 ∈ S。继续这样，我们
可以得出结论，所有 3 的倍数都在 S 中。

其他自然数呢？ 1∈S吗？我们知道 1 != 0，所以
第一个条件不满足。此外，(1−3) = −2，这不是自然的
number 并且因此不是 S 的成员。因此第二个条件
不满意。

自底向上定义:

定义集合 S 为包含在 N 中且满足的最小集合
以下两个属性:

0 ∈ S，且

如果 n ∈ S，则 n +3 ∈ S。

“最小集合”是满足性质 1 和 2 的集合，它是一个
满足性质 1 和 2 的任何其他集合的子集。很容易看出
只能有一个这样的集合:如果 S1 和 S2 都满足性质 1 和
2，且两者都最小，则 S1 ⊆ S2(因为 S1 最小)，且 S2 ⊆ S1
(因为 S2 最小)，因此 S1 = S2。我们需要这个额外的条件，因为
否则有很多集合满足剩下的两个条件

推理规则:

_____
0 ∈ S

n ∈ S
---------
(n+3) ∈ S

这只是之前版本定义的简写符号。
每个条目都称为推理规则，或者只是规则；水平的
行读作“if-then”。线以上的部分称为假设
或前因；线以下的部分称为结论或结果。
当列出两个或多个假设时，它们之间的联系是
隐含的“和”

现在问题来了。

可能最重要的问题是为什么我需要知道这些归纳定义，以及它们在现实世界中的用途？

为什么 Google 在 Inductive Definition 上几乎没有返回任何结果？

如果自顶向下、自底向上和推理规则本质上显示相同的东西，为什么我们需要 3 种方式来编写相同的东西？

为什么我很难找到比书中例子更复杂的问题的归纳定义，如下所示。

我想找到以下 2 个问题的自上而下、自下而上和推理的定义。您不必给我答案，但我确实想知道如何推导出归纳定义。我从哪里开始？是否有解决此类问题的系统方法(食谱)？

1. {2n+3m +1 | n,m ∈ N}
2. {(n, 2n+1) | n ∈ N}

Answer 1

你在这里问了很多问题，所以希望这个答复能回答所有问题。如果有什么你想澄清的，请告诉我。

你的第一个问题 - 为什么我们需要归纳定义？ - 最容易回答。在计算机科学中，大量的结构被归纳定义。例如，您的简单链表具有归纳定义

空列表是一个链表。

单个节点后跟一个链表是一个链表

或者二叉树:

空树是二叉树。

具有两个二叉树子节点的节点是二叉树。

或者正则表达式:

∅ 是一个正则表达式。

ε 是正则表达式。

a 是每个字符 a

的正则表达式

如果 R1 和 R2 是正则表达式，则 R1 | R2 是一个正则表达式。

如果 R1 和 R2 是正则表达式，则 R1 R2 是正则表达式。

如果 R 是正则表达式，则 R* 是正则表达式。

如果 R 是正则表达式，则 (R) 是正则表达式。

这些定义有许多很好的特性。首先，它们适合递归算法。如果要访问二叉树中的每个节点，我们可以使用二叉树的归纳定义来构建一个简单的访问算法:

要访问空树，什么都不做。

要访问由一个节点和两个子树组成的树:

访问节点

访问左子树

访问右子树

类似地，如果我们想操纵正则表达式的结构——例如，可能为它构建一个匹配的自动机——那么归纳定义让我们可以从正则表达式中分段构建自动机。

归纳定义也可用于形式化证明结构的性质。例如，这里有一个 AVL 树的正式定义:

单个节点是 0 阶 AVL 树

具有一个或两个子节点的 0 阶 AVL 树的节点是 1 阶 AVL 树。

具有两个子节点的节点是 n - 1 阶 AVL 树，或者一个节点是 n - 1 阶 AVL 树，另一个节点是 n - 3 阶 AVL 树，是 n 阶 AVL 树。

使用这个定义，可以正式证明 AVL 树是平衡的。

我们可以类似地使用这些类型的定义来证明有关编程语言的属性。大多数语言都有某种归纳定义，因此通过证明程序的每个部分都保留了一些信息，我们可以从头开始构建正确性证明。

你的第二个问题 - 为什么谷歌不提供归纳定义的任何例子？ - 我认为是因为它将它解释为“定义归纳”，而不是一个术语本身。如果您查找递归定义，那么您会发现很多归纳定义的示例，因为归纳定义和递归定义彼此非常相似。

你的第三个问题——为什么我们需要多种方式来表达同一件事？ ——也很简单。如果你想证明一个系统的某些东西，归纳定义非常好。如果你证明它适用于基本元素，然后证明较大的元素保留了这个属性，你就可以证明它总是正确的。递归定义有利于编写程序，因为递归函数倾向于向后运行归纳。推理规则与逻辑证明系统相关联，并为使用经典逻辑证明系统属性提供了起点。

你的第四个问题 - 为什么你找不到任何例子？ - 可以通过花一分钟时间查看您所知道的经典数据结构和算法来轻松修复。你可以归纳地定义多少数据结构？尝试查看链表、二叉树、红黑树、AVL 树等以获取灵感。你会如何定义图形？ DAG？同样，尝试查看句法结构。例如，您将如何归纳定义平衡括号的字符串？ C中的函数原型(prototype)怎么样？

您的最后一个问题 - 是否有解决这些问题的系统方法？ - 有一个否定的答案。您可以定义等效于在输入上模拟任意图灵机的循环，并且由于停机问题是不可判定的，因此没有解决此类问题的通用程序。但是，确实存在许多方法。尝试查看 Graham、Knuth 和 Patashnik 的“具体数学”，以获取有关如何处理重复的灵感。

希望这可以帮助!