另一個 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) 做了正確的事（根據歸納假設），所以我們的程式是正確的。