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