recursion - 递归和归纳证明有什么关系？

Question

递归和归纳证明有什么关系？

比方说fn(n)，

递归是fn(n)调用自身直到 meet base condition；

归纳是当base condition是满足，试图证明(base case + 1)也是正确的。

似乎递归和归纳是不同的方向。一个从nto开始，一个从tobase case开始。base caseinfinite

有人可以详细解释这个想法吗？

Answer 1

递归和归纳是一回事！如果您使用具有依赖类型的编程语言（例如 Agda），这一点会变得很明显，但在某种程度上也可以在没有它们的情况下进行演示。

请记住，由于Curry-Howard 对应关系，类型是命题，程序是证明。当您编写一个类型函数时Nat -> Nat（我将使用 Haskell 表示法），您试图证明给定一个自然数，您的程序将终止并产生另一个自然数。现在我们可能有这样的定义：

f 0 = 1
f (1 + n) = n * f n

这既是其终止的递归定义，f又是其终止的归纳证明！

您可以通过以下方式将其作为证明阅读：

让我们证明 fx 对于任何 x 都终止。

• 基本情况：f 0根据定义，我们有常量，因此它终止。
• 归纳案例：如果我们假设f ntermiates，f (1 + n)也终止（因为它调用的所有函数都终止）。

请注意，由于递归不仅限于递减其计数器的函数，因此归纳也不限于自然数。还有结构归纳，对应结构递归，两者在数学/编程中都很流行。这些将在尝试在更复杂的数据结构（列表/树/等）上证明事物/定义函数时使用。

现在，解决您对递归/归纳的“方向”的担忧。在这里考虑“需求方向”和“供应方向”是有帮助的，它们是相反的。

当您定义递归函数时，需求（方法调用）从较大的值流向基本情况。另一方面，供应（返回值）从基本情况流向较大的参数值。“定义性”是另一种思考供应的方式。它从基本情况开始并通过递归情况传播到无穷大。

现在，当您进行归纳证明时，定理是您的供应，而目标是您的需求。您可以从基本情况得出一个定理 T 0 ，然后使用归纳情况改进到您喜欢的任何大的 T n ：您的供应从 0 流向无穷大。现在，如果您有一个目标 G n，您可以使用归纳步骤从中制作一个较小的目标 G (nk)，直到您达到零。这样你的需求就会从 n 变为 0。

如您所见，在这两种情况下，供应方向都是“无穷大”，而需求方向在这两种情况下都是“趋于零”。

您还可以在不改变其含义的情况下颠倒归纳和递归描述中的明显顺序：

归纳是当证明 P n 成立时，您需要首先通过重复应用归纳案例将目标减少到 P 0，然后使用基本案例证明最终目标。

类似地，递归是您首先定义一个基本情况，然后根据之前的值定义进一步的值。看，方向很容易互换！