5.1 歸納型別與模式匹配#

本章導讀#

本章是第 5 章的入口，目標是把第 4 章的自然數經驗推廣成通用工具。你已經見過自然數 \(Nat\) 由 \(zero\) 與 \(succ\) 生成，本章把這個模式用到一切資料。學完本章，你能用 \(inductive\) 定義新資料型別，並用 \(match\) 做分類討論。下一節 5.2 會在這些型別上寫遞迴函數並做結構歸納證明。建議先複習 04.2 節的歸納直覺，再讀本章會事半功倍。

淺顯說明#

所謂歸納型別，就是把一個型別的所有成員一次說清楚的定義方式。例如一週只上三天課，你可以直接宣告日子只有三種 Monday Friday Sunday 。這種列舉就是構造子，每個構造子都是一種合法的生成方式。自然數 \(Nat\) 也是同樣的把戲，只是有無窮多個成員而已。串列 \(List\) 則是兩種情形，空串列 \(nil\) 或在串列前加一個元素 \(cons\) 。二元樹 \(Tree\) 類似，空樹 \(empty\) 或把左右子樹掛在節點下 \(node\) 。而 \(match\) 表達式就是使用這些資料的方法，按構造子逐一處理。它的精神是分類討論，每一種構造子對應一個分支，不可遺漏。 Lean 會幫你做窮盡性檢查，少寫一個分支就會報錯提醒，這正是函數式程式設計的核心手感。掌握它之後，證明中的分類討論 \(cases\) 也會變得自然。

正規理論#

歸納型別由三部分構成，型別形成規則，構造子引入規則，消去規則。形成規則宣告新成員集合，引入規則給出生成方式，消去規則即模式匹配。以自然數為例，其語法骨架可用獨立公式表示如下。

\[ Nat::=zero\mid succ(Nat) \]

一般歸納型別的消去子是依賴的模式匹配，其型別形如以下骨架。

\[ match:I(a)\to motive(a)\to branches\to motive(a) \]

其中 \(motive\) 是隨被匹配對象變化的目標族， \(branches\) 是逐構造子給出的處理。下表整理本章五個典型歸納型別及其構造子。

型別 \(T\)	構造子	直觀讀法
\(Day\)	\(monday\) ， \(friday\) ， \(sunday\)	有限列舉三天
\(Bool\)	\(true\) ， \(false\)	真假兩種取值
\(Nat\)	\(zero\) ， \(succ\)	零與後繼數
\(List\)	\(nil\) ， \(cons\)	空串列與接上元素
\(Tree\)	\(empty\) ， \(node\)	空樹與左右子樹成節點

下表整理構造子與消去子的對應關係，幫助記憶證明 tactics 的來源。

概念	型別層含義	邏輯層含義
\(inductive\)	定義新資料型別	定義新命題族
構造子	資料的生成方式	命題的引入規則
\(match\)	按構造子計算	按引入規則做分類

窮盡性檢查的規則很簡單，分支集合必須覆蓋構造子集合。若構造子集合是 \(C\) 而分支集合是 \(B\) ，則檢查條件為以下公式。

\[ B\supseteq C \]

少寫分支等於分類不完全， Lean 會以警告或錯誤指出缺少的構造子，初學階段建議把每個分支都寫出來。

簡易範例#

下面程式一次示範五個歸納型別，全部放在命名空間 \(Toy\) 之中。這樣做是為了避免與核心函式庫的同名型別衝突，請特別留意。接著定義星期判斷，串列長度 \(length\) 與映射 \(map\) 兩個經典函數。

namespace Toy

inductive Day where
  | monday : Day
  | friday : Day
  | sunday : Day

inductive Bool where
  | true : Bool
  | false : Bool

inductive Nat where
  | zero : Nat
  | succ : Nat → Nat

inductive List (α : Type) where
  | nil : List α
  | cons : α → List α → List α

inductive Tree (α : Type) where
  | empty : Tree α
  | node : α → Tree α → Tree α → Tree α

def isClassDay : Day → Bool
  | .monday => .true
  | .friday => .true
  | .sunday => .false
def length : List α → Nat
  | .nil => .zero
  | .cons _ xs => .succ (length xs)
def map (f : α → β) : List α → List β
  | .nil => .nil
  | .cons x xs => .cons (f x) (map f xs)

end Toy

請注意 \(length\) 與 \(map\) 都是對子結構做遞迴呼叫，前者計數，後者以函數 \(f\) 代換每個元素。若刪掉 \(isClassDay\) 的任一分支， Lean 會報告缺少 \(Day\) 的某個構造子。這正是窮盡性檢查在保護你，讓分類討論不會悄悄缺角，下一節會把它變成終止性論證。

歷史典故#

構造子的想法最早可追溯到 Church 簡單型別理論，以有限規則生成無窮良型項。而構造子即引入規則的觀點，則在 Howard 公式即型別中開花結果。 Howard 把自然數的零與後繼看成存在證據的兩種構造方式。自動證明一側， Boyer-Moore 證明器把歸納資料型別變成機器可用的公理，其現代形式最終在 CoC 與 CIC 中定型。讀本章時，不妨把構造子想成探案卷宗中的物證清單，每多一個構造子就多一種結案路徑。

習題#

為本節的 \(Day\) 新增一個構造子 \(holiday\) ，並補上 \(isClassDay\) 的對應分支，使程式重新通過窮盡性檢查。
仿照 \(length\) 的寫法，為 \(Tree\) 寫一個計算節點個數的函數 \(count\) ，要求對 \(empty\) 與 \(node\) 分別處理。
故意刪去 \(map\) 的 \(nil\) 分支，觀察 Lean 的錯誤訊息，並用一句話說明窮盡性檢查的意義。