5.2 結構歸納與遞迴函數#

本章導讀#

上一節你學會用 \(inductive\) 定義資料，用 \(match\) 做分類討論。本章要回答下一個自然問題，遞迴函數為什麼一定會停下來。學完本章，你能寫出結構遞減的遞迴，並在需要時補上度量證明。主線例子是串列的反轉 \(reverse\) 與拼接 \(append\) ，外加一個引理骨架。下一章 6.1 會把歸納證明接到命題即型別的理論上。閱讀時請把終止性與歸納假設看成同一件事的兩面。

淺顯說明#

遞迴函數像下樓梯，每一步都要比上一步更接近地面。結構遞減的意思就是，每次遞迴呼叫都只處理更小的子結構。例如串列的 \(cons\) 分支只對尾部 \(xs\) 遞迴，絕不碰原串列本身。因為子結構層層剝開終究見底，所以函數一定會停。 Lean 內建的終止檢查器會自動辨認這種模式，多數定義不用操心。遇到自動檢查失敗時，就用 termination_by 親自指定度量。度量是一個隨遞迴嚴格變小的數值，例如串列長度或自然數本身。證明側的孿生兄弟就是歸納法，歸納假設只能用在更小的子結構上。對 \(nil\) 證明基本情形，對 \(cons\) 用尾部的假設推導全體結論。這種證明形狀常被稱為瀑布，基本情形在前，歸納步驟層層推進。記住口訣，遞迴用在子結構，假設也只用在子結構。

正規理論#

結構遞迴的合法性來自歸納型別的良基性，子結構關係沒有無窮下降鏈。設子結構關係為 \(sub\) ，其關鍵性質是以下公式所表達的良基性。

\[ Wf(sub):=\forall P,step\to\forall a,P(a) \]

其中 \(step\) 表示由子結構的性質推出全體的性質，即歸納步驟。終止度量的一般形狀是映射到自然數的函數 \(m\) ，滿足以下不等式。

\[ m(call)<m(input) \]

每次遞迴呼叫的度量都嚴格小於輸入的度量，故遞迴不可能無限進行。下表整理常見終止判據與對應的寫法。

判據	適用情形	Lean 寫法
結構遞減	遞迴參數是構造子的直接子結構	直接寫等式，自動通過
度量遞減	參數重組但某數值變小	補上度量註記
詞典序遞減	多參數輪流變小	補上多元組度量

歸納假設的使用時機可以用下表記憶，核心是只能用在子結構上。

證明分支	可用假設	典型動作
\(nil\) 分支	無歸納假設	化簡加 \(rfl\) 結案
\(cons\) 分支	尾部 \(xs\) 的假設 \(ih\)	重寫 \(ih\) 再化簡
非子結構實例	不可使用假設	另找引理或換歸納對象

基本原則可以寫成一句蘊涵，子結構關係蘊涵假設可用性。

\[ sub(b,a)\to usable(IH(b)) \]

這也是瀑布式證明的邏輯骨架，先處理基本情形，再逐層使用假設。度量註記 termination_by 的本質，就是親手提供這個 \(m\) 並證明遞減。

簡易範例#

下面先定義串列反轉 \(reverse\) ，其中符號 ++ 即拼接 \(append\) 。接著用費氏數列示範度量註記，最後給出反轉分配律的引理骨架。

def reverse : List α → List α
  | [] => []
  | x :: xs => reverse xs ++ [x]

def fib : Nat → Nat
  | 0 => 0
  | 1 => 1
  | n + 2 => fib n + fib (n + 1)
termination_by n => n

theorem reverse_append (xs ys : List α) :
    reverse (xs ++ ys) = reverse ys ++ reverse xs := by
  induction xs with
  | nil => simp [reverse]
  | cons x xs ih =>
    simp [reverse, ih]
    sorry -- 待補結合律引理後結案

請注意 \(reverse\) 的遞迴呼叫只吃尾部 \(xs\) ，故屬於結構遞減。 \(nil\) 分支不需要歸納假設，化簡 \(reverse\) 定義即可結案。 \(cons\) 分支則先化簡 \(reverse\) ，再用假設 \(ih\) 改寫尾部。最後一個等式需要串列拼接的結合律，留作習題補上。而 \(fib\) 的遞迴參數經過重組，需用度量註記宣告以 \(n\) 遞減。這正是上表第二列的情形，自動檢查失敗時的手動逃生門。

歷史典故#

把歸納證明交給機器正是 Boyer-Moore 證明器的創舉。該卷宗記載如何讓證明器自動挑選歸納變數並生成瀑布式證明。而結構遞減的理論身分，要到 CoC 與 CIC 才完全確立。歸納族的消去子在演算層保證了遞迴一定終止。稍後的 Coq 誕生則把這套機制變成可互動的證明環境。你在 Lean 中寫的每一個 induction ，都是這條歷史長河的下游。下次被終止檢查器退件時，不妨想成 Boyer 與 Moore 在提醒你補度量。

習題#

證明輔助引理 reverse_singleton ，即反轉單元素串列等於自身，只需對 \(nil\) 與 \(cons\) 分類化簡。
補完 \(reverse\) 分配律骨架中留下的 sorry ，提示是先證明拼接結合律再用它改寫目標。
為串列拼接 \(append\) 寫一個關於長度的引理骨架，說明在哪個分支需要使用假設 \(ih\) ，在哪個分支不需要。