递归定义与结构归纳
Recursive Definitions & Structural Induction递归数据类型的定义只有两部分：基例（base case）——一些已知元素直接入伙；构造规则（constructor case）——从已有元素造新元素。以字符串为例（定义 7.1.1）：基例：空串 λ ∈ A*；构造：a ∈ A 且 s ∈ A*，则 (a, s) ∈ A*。串 1011 在这套定义下是嵌套对 ⟨1, ⟨0, ⟨1, ⟨1, λ⟩⟩⟩⟩——Scheme 的 cons、Python 的 list 正是这么活的。
函数也能照搬同一套 cases 递归定义：|λ| ::= 0，|(a,s)| ::= 1 + |s|；连接 λ·t ::= t，(a,s)·t ::= (a, s·t)。而结构归纳（structural induction）就是"按构造证明"：基例元素有性质 P；每个构造规则保持 P；⇒ 全体元素都有 P。书里的例题：s·λ = s（λ 是右单位元）与 |s·t| = |s| + |t|，两证都是教科书级的结构归纳。
匹配括号串
Strings of Matched Brackets编译器解析表达式 x + y∗z² ÷ y + 7 时要决定括号怎么加——这正是当年 Floyd 得图灵奖的工作之一。匹配括号串有个优雅的递归定义（RecMatch）：基例 λ ∈ RecMatch；构造：若 s, t ∈ RecMatch，则 [ s ] t ∈ RecMatch（一对括号包住 s，再拼上 t）。
用这个定义能结构归纳地证明：RecMatch 里每个串的左右括号数量相等（#₁ = #₂）。更妙的是反过来也成立：RecMatch 恰好就是"matched"的括号串全体。来，用构造规则亲手造一个：
病态递归定义展览馆
Ill-formed Function Definitions递归定义要"跟着数据类型的构造走"，否则就会生病。原书收集了四种病：无基例（f₁(n) ::= 2 + f₁(n−1)，加个常数还成立，定义不唯一）、不终止（f₂(n) ::= f₂(n+1)，越递归越远）、不一致（f₃(6) 同时要求 =0 与 =1）、以及最著名的悬而未决——Collatz 猜想。逐一参观：
算术表达式
Arithmetic Expressions3x² + 2x + 1 在编译器眼里其实是 [ [3∗[x∗x]] + [[2∗x]+1] ]——一个 Aexp（全括号、无指数的算术表达式递归类型）。求值函数 eval 与替换函数 subst 都是按构造逐 case 递归定义的。而它们的组合揭示了一个编译器日常：替换模型（先代入再求值）与环境模型（先求值再代入）殊途同归——定理 7.4.4 用结构归纳证明 eval(subst(f,e), n) = eval(e, eval(f,n))。两种模型的乘法次数却不同！亲手数：
结构归纳实战：树叶 = 节点 + 1
Ordered Binary Trees · Problem 7.1有序二叉树 OBT：基例 ⟨leaf⟩ 是树；构造：若 R、S 是树，⟨node, R, S⟩ 也是。习题 7.1 要证 lᴛ = nᴛ + 1（叶数 = 节点数 + 1）——结构归纳两步走：
基例 ⟨leaf⟩：l = 1，n = 0 ⇒ l = n + 1 ✓
构造 ⟨node, R, S⟩：由归纳假设 l_R = n_R + 1、l_S = n_S + 1。整树 l = l_R + l_S = (n_R + 1) + (n_S + 1) = (n_R + n_S + 1) + 1 = n + 1 ✓ ■
习题实战：串归纳与 cons 嵌套
7.3.2 & 7.1, Playable7.3.2 的串归纳实例 + 7.1 的 cons 嵌套翻译器。
终局自测
Final Check六题，覆盖全章。
彩蛋与课后挑战
Easter Eggs & Problems表达式解析：从手工活到消失的技术（原书 7.2 文框）
1950-60 年代，编译器最头疼的问题之一就是给 x + y∗z² ÷ y + 7 加上正确的括号——Floyd 因此发现括号插入的简单流程（后来因此拿图灵奖）。70-80 年代这套技术被打包进编译器编译器（parser generators），90 年代时解析已从 CS 课程基本消失：一门技术成功的最高境界，是让人忘记它存在。
Ackermann 函数与 Union-Find（原书 7.3.2 末尾）
A(m,n) 的定义"反直觉"地用更大的参数定义自己——证明它良定义需要点巧思。它的逆函数增长慢过 log n、log log n、log log log n…但仍无界；Union-Find 算法的运行时间系数就约等于这个逆 Ackermann——理论上不是线性的算法，实践中比线性还快。病态与神器，一线之隔。
课后挑战（均出自原书习题）
- 7.1 OBT 的 lᴛ = nᴛ + 1 完整结构归纳证明（本页已给出骨架，补全细节）。
- 7.2 / 7.3 证明连接的结合律 (r·s)·t = r·(s·t)，以及 rev(s·t) = rev(t)·rev(s)。
- 7.4 初等 18.01 函数（F18）：基例 id、常函数、sin；构造 +、×、fg^g、取逆、复合。证明 F18 对求导封闭——微积分的结构归纳化！
- 7.7 回文串的递归定义 RecPal（λ、单字符、asa）与 rev 定义的一致性证明。
- 7.19 证明 AmbRecMatch = RecMatch——歧义定义与无歧义定义可以定义同一个集合。