另一个 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

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

natToInt Zero = 0

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

natToInt (Succ n) = natToInt n + 1

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

假设我们要证明语句 $n!\geq n$ 对所有 $n\geq 0$ 成立。首先我们构造一个基本情况：我们要证明当 $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。我们知道$0+m=m$ 不管$m$ 是什么；因此，在基本情况下，算法执行了正确的事。现在，假设 addNat n m 对于所有 m 都做了正确的事，我们想要证明 addNat (Succ n) m 做了正确的事。我们知道$(n+1)+m=n+(m+1)$，因此由于 addNat n (Succ m) 做了正确的事（根据归纳假设），所以我们的程序是正确的。