递归和归纳证明有什么关系？
假设fn(n)，
递归是fn(n)调用自己直到遇到base condition；
归纳是当base condition满足时，尝试证明(base case + 1)也是正确的。
似乎递归和归纳的方向不同。一个从n 到base case，另一个从base case 到infinite。
有人能详细解释一下这个想法吗？
【问题讨论】：
标签： recursion type-theory induction
递归和归纳是一回事！如果您使用具有依赖类型的编程语言（例如 Agda），这一点会变得很明显，但在某种程度上也可以在没有依赖类型的情况下进行演示。
请记住，由于Curry-Howard correspondence，类型是命题，程序是证明。当您编写Nat -> Nat 类型的函数时（我将使用Haskell 表示法），您试图证明给定一个自然数，您的程序将终止并产生另一个自然数。现在我们可能有这样的定义：
f 0 = 1
f (1 + n) = n * f n
这既是f 的递归定义，同时也是其终止的归纳证明！
您可以通过以下方式将其作为证明阅读：
让我们证明 f x 终止于任何 x。
f 0 常量定义，所以它终止。 f n 终止，f (1 + n) 也终止（因为它调用的所有函数都终止）。请注意，由于递归不仅限于递减其计数器的函数，因此归纳也不限于自然数。还有结构归纳，对应结构递归，两者在数学/编程中都很流行。这些将在尝试在更复杂的数据结构（列表/树/等）上证明事物/定义函数时使用。
现在，解决您对递归/归纳的“方向”的担忧。在这里考虑“需求方向”和“供应方向”是有帮助的，它们是相反的。
当您定义递归函数时，需求（方法调用）会从较大的值流向基本情况。另一方面，供应（返回值）从基本情况流向较大的参数值。 “定义性”是另一种思考供应的方式。它从基本情况开始，通过递归情况传播到无穷大。
现在，当您进行归纳证明时，定理是您的供应，而目标是您的需求。您可以从基本情况得出一个定理 T 0 ，然后使用归纳情况改进到您喜欢的任何大的 T n ：您的供应从 0 流向无穷大。现在，如果您有一个目标 G n，您可以使用归纳步骤从中制作一个较小的目标 G (n-k)，直到您达到零。这样你的需求就会从 n 变为 0。
如您所见，在这两种情况下，供应方向都是“无穷大”，而需求方向在这两种情况下都是“趋于零”。
你也可以颠倒归纳和递归描述中的明显顺序而不改变它们的含义：
归纳是当证明 P n 成立时，您需要首先通过重复应用归纳案例将目标减少到 P 0，然后使用基本案例证明最终目标。
同样，递归是您首先定义一个基本情况，然后根据之前的值定义进一步的值。看，方向很容易互换！
【讨论】：