又一个 Haskell 教程/递归

递归和归纳

非正式地说，如果一个函数的定义依赖于自身，那么该函数就是递归函数。典型的例子是阶乘，其定义为

$fact(n)={\begin{cases}1&n=0\\n*fact(n-1)&n>0\\\end{cases}}$

在这里，我们可以看到，为了计算 $fact(5)$，我们需要计算 $fact(4)$，但为了计算 $fact(4)$，我们需要计算 $fact(3)$，等等。

递归函数定义总是包含一定数量的非递归基本情况和一定数量的递归情况。在阶乘的情况下，我们每个都有一个。基本情况是当 $n=0$，递归情况是当 $n>0$。

实际上，可以将自然数本身视为递归的（事实上，如果你问集合论者这个问题，他们会说这就是事实）。也就是说，有一个零元素，然后对于每个元素，它都有一个后继元素。即 1=succ(0), 2=succ(1), ..., 573=succ(572), ...，依此类推，永远持续下去。我们实际上可以在 Haskell 中实现这个自然数系统

data Nat = Zero | Succ Nat

这是一个递归类型定义。在这里，我们将 1 表示为 Succ Zero，将 3 表示为 Succ (Succ (Succ Zero))。我们可能想要做的一件事是能够在 Nat 和 Int 之间进行转换。显然，我们可以写一个基本情况为

natToInt Zero = 0

为了写递归情况，我们意识到我们将得到 Succ n 形式的东西。我们可以假设我们能够取 n 并生成一个 Int。假设我们可以做到这一点，我们所需要做的就是将 1 加到这个结果中。这产生了我们的递归情况

natToInt (Succ n) = natToInt n + 1

递归和数学归纳之间存在密切的联系。归纳是一种证明技术，它通常将问题分解为基本情况和“归纳”情况，这与我们对递归的分析非常类似。

假设我们要证明对于所有$n\geq 0$，语句 $n!\geq n$ 成立。首先，我们制定一个基本情况：即，我们希望在 $n=0$ 时证明该语句。当 $n=0$ 时，根据定义，$n!=1$。由于 $n!=1>0=n$，我们得到 $0!\geq 0$ 如所期望的那样。

现在，假设 $n>0$。那么，对于某个值 $k$，有 $n=k+1$。现在我们使用归纳假设，并断言该命题对于 $n=k$ 成立。也就是说，我们假设 $k!\geq k$。现在，我们使用 $k$ 来构建我们 $n$ 值的命题。也就是说，$n!\geq n$ 当且仅当 $(k+1)!\geq (k+1)$。现在我们应用阶乘的定义，得到 $(k+1)!=(k+1)*k!$。现在，我们知道 $k!\geq k$，所以 $(k+1)*k!\geq k+1$ 当且仅当 $k+1\geq 1$。但我们知道 $k\geq 0$，这意味着 $k+1\geq 1$。因此，命题得证。

在证明一个断言对于 $n$ 为真时，假设该断言对于 $k$ 为真可能看起来有点违反直觉。你可以这样理解：我们已经证明了当 $n=0$ 时断言成立。现在，我们知道它对于 $n=0$ 为真，因此利用这一点，我们可以使用归纳论证来证明它对于 $n=1$ 也为真。现在，我们知道它对于 $n=1$ 为真，所以我们可以再次使用归纳论证来证明它对于 $n=2$ 也为真。我们可以不断重复这个论证，最终发现它对于所有 $n$ 都成立。

这就像推倒多米诺骨牌一样。你知道，当你推倒第一个骨牌时，它会推倒第二个。然后，第二个会推倒第三个，以此类推。基本情况就像推倒第一个骨牌，而归纳步骤就像证明推倒第 $k$ 个骨牌会使第 $k+1$ 个骨牌倒下。

事实上，我们可以使用归纳法来证明我们的 natToInt 函数执行了正确操作。首先，我们证明基本情况：natToInt Zero 是否等于 $0$？是的，很明显它等于。现在，我们可以假设 natToInt n 计算出正确的值（这是归纳假设），并询问 natToInt (Succ n) 是否产生正确的值。同样，通过查看定义，很明显它也是正确的。

让我们考虑一个更复杂的例子：Nat 的加法。我们可以简洁地将其写成

addNat Zero m = m
addNat (Succ n) m = addNat n (Succ m)

现在，让我们证明它执行了正确操作。首先，作为基本情况，假设第一个参数是 Zero。我们知道无论 $m$ 是什么，$0+m=m$ 都成立；因此，在基本情况中，算法执行了正确操作。现在，假设 addNat n m 对于所有 m 都执行了正确操作，我们要证明 addNat (Succ n) m 也执行了正确操作。我们知道 $(n+1)+m=n+(m+1)$，因此，由于 addNat n (Succ m) 执行了正确操作（根据归纳假设），所以我们的程序是正确的。