. 语法：BNF、最小集合与结构归纳

Glomzzz
2026-10-10
About

用 BNF 与最小封闭集合定义算术语言的词项，并由最小性导出结构归纳原理．

1 语法树

Convention 1.1 抽象语法 [abstract-syntax]

2026-10-10
Glomzzz

抽象语法把程序视为语法树，即节点标签表示程序构造的树（树的术语见树的基本术语），隐去字符排列和括号等表面细节．从字符串到树的那一步叫解析．采用这条约定时，假定解析已经完成，且已消除了结构歧义那样的歧义；解析器本身留在这条约定的研究范围之外．书写时为了能在一行里写下一棵树，会用括号表示分组： $pred (succ 0)$ 表示根标着 $pred$ ，它的唯一孩子标着 $succ$ ；这个孩子及其后代构成表示 $succ 0$ 的子树．

这条约定是第一个“隐含前提”：本文所有的定理都是关于树的．至于怎样把字符串可靠地变成树，那是另一个话题．这种只关心树形结构、不关心字符怎么排的语法，叫抽象语法．

2 BNF

文法用产生规则描述允许的语法构造；语法则是关于程序结构的更一般的概念．本文用文法直接描述抽象语法树，省略字符层面的解析．

常用的文法记号是 BNF，即 Backus–Naur 表示法 （参见维基百科）．它得名于 John Backus 与 Peter Naur，与 ALGOL 60 的语法描述密切相关．英文名里的 Form 指一种表示形式，注意与后文规约理论中的“正规形式”区分．

BNF 用产生式描述各个语法类别，形如

$名字 ⩴ {选项}_{1} | {选项}_{2} | \dots$

其中 $⩴$ 读作“定义为”或“可以是”， $|$ 读作“或者”，用来隔开几种选项．右侧的符号分为终结符号与非终结符号：终结符号是直接给出的符号（如关键字 $if$ 、 $succ$ ），非终结符号表示还可由产生式展开的语法类别．

名字出现在自己的右边，就形成了递归．例如

$𝑛 ⩴ 0 | succ 𝑛$

说的是： $𝑛$ 可以是 $0$ ，也可以是 $succ$ 后面跟着另一个 $𝑛$ ．于是 $0$ 、 $succ 0$ 、 $succ (succ 0)$ 都是 $𝑛$ ． BNF 本身只是一种记号，它的准确含义要靠下面的“最小集合”来说清楚．

3 词项

对象语言中的程序称为词项（简称“项”），用元变量 $𝑡$ 表示．这门语言只有表达式，没有单独的语句类别；词项的抽象语法用两行 BNF 给出：

$\begin{matrix} 𝑡 ⩴ & true | false | if 𝑡 then 𝑡 else 𝑡 \\ | 0 | succ 𝑡 | pred 𝑡 | iszero 𝑡 \end{matrix}$

竖线读作“或者”． $succ 𝑡$ 是 $𝑡$ 的后继，可以理解为加一； $pred 𝑡$ 是前驱，可以理解为减一； $iszero 𝑡$ 判断 $𝑡$ 是否为零．例如 $if (iszero (pred (succ 0))) then 0 else succ 0$ 是词项，它对应的语法树见下图：

图中的 $if$ 是根，有三个孩子； $iszero$ 、 $pred$ 、 $succ$ 是只有一个孩子的内部节点；三个标着 $0$ 的节点是不同位置上的叶子．

Definition 3.1 直接子项与真子项 [immediate-and-proper-subterms]

2026-10-10
Glomzzz

对词项的集合中的项，采用树的基本术语的树术语．根节点的每个孩子所对应的整棵子树，称为它的直接子项．常量 $true$ 、 $false$ 、 $0$ 没有直接子项；一元构造 $succ 𝑡_{1}$ 、 $pred 𝑡_{1}$ 、 $iszero 𝑡_{1}$ 的唯一直接子项是 $𝑡_{1}$ ；条件构造 $if 𝑡_{1} then 𝑡_{2} else 𝑡_{3}$ 的三个直接子项依次是 $𝑡_{1}$ 、 $𝑡_{2}$ 、 $𝑡_{3}$ ．

沿着“取直接子项”走一步或多步得到的项，称为真子项．例如 $pred (succ 0)$ 的直接子项只有 $succ 0$ ； $0$ 属于真子项，但隔了一层 $succ$ ，故不属直接子项；整项本身也不算自己的真子项．同一文本可以出现在树的不同位置，谈子项时还要看它所在的位置．

这段 BNF 描述了词项的构造方式，严格的集合含义由归纳定义给出．

Definition 3.2 词项的集合 [set-of-terms]

2026-10-10
Glomzzz

把词项（简称“项”）视为抽象语法中的有限语法树：常量 $true$ 、 $false$ 、 $0$ 是叶子， $succ$ 、 $pred$ 、 $iszero$ 是一元构造， $if$ 有条件、 $then$ 分支和 $else$ 分支三个有序子项．

词项的集合 $花体(T)$ 是同时满足三条封闭条件的最小集合：常量 $true$ 、 $false$ 、 $0$ 都属于 $花体(T)$ ；若 $t_(1) \in 花体(T)$ ，则 $succ 𝑡_{1}$ 、 $pred 𝑡_{1}$ 、 $iszero 𝑡_{1}$ 都属于 $花体(T)$ ；若 $t_(1), t_(2), t_(3) \in 花体(T)$ ，则 $if t_(1) then t_(2) else t_(3) \in 花体(T)$ ．

“最小”的意思是：如果另一个集合 $𝑆$ 也满足这三条，那么 $花体(T) \subseteq S$ ．因此 $花体(T)$ 只含有限次应用生成规则所能得到的词项，没有其他元素；这一限制称为最小性子句．

记号 $花体(T)$ 是花体字母 T，可读作 script T script T ；它表示词项集合，与后文表示类型的元变量 $𝑇$ 不同．

“封闭”说的是：集合里有了 $𝑡_{1}$ ，就必须也有 $succ 𝑡_{1}$ 等等，用这几条规则造不出集合外的东西．

只要求“封闭”还不够，因为满足封闭条件的集合有很多．例如允许额外的叶子 null null ，并且把所有包含这个新叶子的 $succ$ 、 $if$ 等树也一起加进来，得到的更大集合仍然满足封闭条件．但三条生成条件并未给出 null null ，它不属于本文的项（若只加 null null ，漏掉 $succ null$ 等树，则会直接破坏封闭性）．

取最小集合，就是说：词项只有用上面三条规则在有限步内构造出来的对象，没有其他元素．这一限制称为最小性子句；它排除了规则没有生成的额外对象．

Note 3.3 最小集合确实存在 [existence-of-the-least-set]

2026-10-10
Glomzzz

打开独立页面 →

由此可以看出两件事：每个项都是一棵有限的树，叶子是 $true$ 、 $false$ 、 $0$ ，内部节点是 $succ$ 、 $pred$ 、 $iszero$ （各有一个孩子）或 $if$ （有三个孩子）；同时，语法只规定形状，不保证项满足类型规则． $succ true$ 和 $if 0 then 0 else true$ 都是合法的项；它们是否良类型，要由后面的类型规则判断．操作语义则单独规定项能怎样规约，不良类型的项也在它的讨论范围内，甚至可能正常求值．

在 Rust 里，这个集合可以表示为枚举． enum enum 的值只能由这几个构造子有限次地组合出来，“最小”由语言本身保证：

// 对象语言的项（定义“词项的集合”）
#[derive(Clone, Debug, PartialEq, Eq, Hash)]
pub enum Term {
    True, False,
    If(Box<Term>, Box<Term>, Box<Term>),  // if t1 then t2 else t3
    Zero,
    Succ(Box<Term>), Pred(Box<Term>), IsZero(Box<Term>),
}

// 对象语言的项（定义“词项的集合”）
#[derive(Clone, Debug, PartialEq, Eq, Hash)]
pub enum Term {
    True, False,
    If(Box<Term>, Box<Term>, Box<Term>),  // if t1 then t2 else t3
    Zero,
    Succ(Box<Term>), Pred(Box<Term>), IsZero(Box<Term>),
}

Box<Term> Box<Term> 是指向堆上 Term Term 的指针，并且独占它指向的那块内存． Rust 需要在编译时确定每个类型占多少字节：若直接写成 Succ(Term) Succ(Term) ，里面嵌套的 Term Term 又可能装一个 Term Term ，大小就会变成无穷大，编译器会报错 recursive type has infinite size recursive type has infinite size ．换成 Box Box 以后， Succ Succ 里装的只是一个固定大小的指针，真正的子树放在堆上．

从树的角度看， Box Box 正好对应语法树里的一条边：父节点通过它“拥有”自己的子树，子树不和别的节点共享．也正因为独占， Box Box 不能按位复制；复制一个项要用 .clone() .clone() 把整棵子树深拷贝一遍，后面的代码里会看到这一点．

4 结构归纳

最小性在排除额外元素的同时，还给出了结构归纳法．要证明“所有词项都满足性质 $𝑃$ ”，不必逐一检查无穷多个词项：只需验证常量的基准情况，再验证各个构造子的归纳情况，也就是证明当直接子项满足 $𝑃$ 时，由它们构成的词项也满足 $𝑃$ ．

Note 4.1 什么是归纳 [meaning-of-induction]

2026-10-10
Glomzzz

打开独立页面 →

先看“最小”怎样推出归纳．设 $𝑆$ 是所有满足 $𝑃$ 的项组成的集合．如果 $𝑃$ 能“跟着规则搭上去”，意思就是 $𝑆$ 也满足那三条封闭条件，用这三条规则同样搭不出 $𝑆$ 之外的对象．而 $花体(T)$ 是这类集合里最小的，即每个这类集合的子集．因此 $花体(T) \subset S$ ， $花体(T)$ 的每个项都在 $𝑆$ 里，都满足 $𝑃$ ．

要是去掉“最小”， $花体(T)$ 里就可能混进 null null 这样的例外：三条规则搭不出它，对它也无话可说， $𝑃$ 在它身上成不成立也就无从谈起． “最小”保证了 $花体(T)$ 里只有规则搭出来的东西，所以“对每条规则检查一遍”就等于“对每个项检查一遍”．下面把这段论证写成定理．

Theorem 4.2 结构归纳原理 [structural-induction]

2026-10-10
Glomzzz

设 $𝑃$ 是关于词项的集合中有限项的性质．若第 1 条 $𝑃 (true)$ 、 $𝑃 (false)$ 、 $𝑃 (0)$ 成立，第 2 条对任意项 $𝑡_{1}$ 由 $𝑃 (𝑡_{1})$ 能推出 $𝑃 (succ 𝑡_{1})$ 、 $𝑃 (pred 𝑡_{1})$ 、 $𝑃 (iszero 𝑡_{1})$ ，且第 3 条对任意项 $𝑡_{1}, 𝑡_{2}, 𝑡_{3}$ 由 $𝑃 (𝑡_{1})$ 、 $𝑃 (𝑡_{2})$ 、 $𝑃 (𝑡_{3})$ 能推出 $𝑃 (if 𝑡_{1} then 𝑡_{2} else 𝑡_{3})$ ，那么对所有项 $𝑡$ ， $𝑃 (𝑡)$ 成立．

Proof.

令

S = {t \in 花体(T) | P(t)}

，即满足

𝑃

的项组成的集合．三条假设恰好说明

𝑆

满足词项的集合的三条封闭条件．由于

花体(T)

是满足封闭条件的最小集合，

花体(T) \subseteq S

，因此每个项都在

𝑆

里，都满足

𝑃

．

∎

在元语言的集合论背景下，结构归纳直接由“最小”这两个字推出，无需作为对象语言的额外公理引入（当然，元语言自身的数学基础仍有其公理，这里只是说定义了这个最小集合后不必再单独追加一条归纳公理）．

Definition 4.3 归纳假设 [induction-hypothesis]

2026-10-10
Glomzzz

归纳假设是在归纳步骤中，对归纳原理许可的更小对象暂时假定的性质．它是用来证明“如果这些更小对象满足 $𝑃$ ，那么当前对象也满足 $𝑃$ ”的前提；这里不能把“所有对象都满足 $𝑃$ ”或当前待证结论预先当真．

在结构归纳原理的第 2 条中，归纳假设是 $𝑃 (𝑡_{1})$ ；第 3 条中是 $𝑃 (𝑡_{1})$ 、 $𝑃 (𝑡_{2})$ 、 $𝑃 (𝑡_{3})$ ．这些对象恰好是直接子项与真子项给出的直接子项．常量没有子项，所以基准情况没有归纳假设，必须直接证明．

这种暂时假定之所以合法，是因为我们首先证明的是条件命题．每个实际词项都由有限次构造得到，从已经验证的叶子出发，逐层应用这个条件命题，就能把性质传到根．假设只沿着更小的结构使用，不会绕回当前待证结论．

Example 4.4 合法的归纳假设与循环论证 [induction-hypotheses-and-circular-reasoning]

2026-10-10
Glomzzz

取词项的集合中的有限项，树的术语见树的基本术语，归纳方法采用结构归纳原理．

取 $𝑃 (𝑡)$ 为“ $𝑡$ 至少含有一个叶子”．常量本身就是叶子，基准情况成立．证明 $𝑃 (pred 𝑡_{1})$ 时，归纳假设 $𝑃 (𝑡_{1})$ 给出 $𝑡_{1}$ 中有一个叶子；加上 $pred$ 根以后，那个叶子仍然存在．证明 $𝑃 (if 𝑡_{1} then 𝑡_{2} else 𝑡_{3})$ 时，任取某个孩子中的叶子即可．对于 $pred (succ 0)$ ，先验证 $𝑃 (0)$ ，再推出 $𝑃 (succ 0)$ ，最后推出整项的性质，没有一步用到尚未证明的结论．

反过来，试图证明错误命题 $𝑄 (𝑡)$ ：“ $𝑡$ 不含 $pred$ ”，然后在 $pred 𝑡_{1}$ 的情形里说“假定 $𝑄 (pred 𝑡_{1})$ ，所以它不含 $pred$ ”，就是循环论证：用待证结论本身支持待证结论．它至多证明了 $𝑄 (pred 𝑡_{1}) ⟹ 𝑄 (pred 𝑡_{1})$ ，没有证明归纳步骤要求的 $𝑄 (𝑡_{1}) ⟹ 𝑄 (pred 𝑡_{1})$ ．实际取 $𝑡_{1} = 0$ ，前者 $𝑄 (0)$ 为真，后者 $𝑄 (pred 0)$ 为假，反例立刻出现．

循环也可以藏在两步里： “为了证明父项满足 $𝑃$ ，先用父项满足 $𝑃$ 来证明子项满足 $𝑃$ ，再由子项推出父项”．两句话合起来仍然没有独立的起点．

Note 4.5 归纳假设的适用范围 [scope-of-induction-hypotheses]

2026-10-10
Glomzzz

打开独立页面 →

再看一棵具体语法树上的归纳方向．要证 $𝑃$ 对整棵树成立，只需在叶子处直接验证（第 1 条），并在每个内部节点处假定以各个孩子为根的子项都满足 $𝑃$ ，再推出以当前节点为根的项满足 $𝑃$ （第 2、3 条）．这里 $𝑃$ 描述的是以该节点为根的整棵子项，与单个节点的标签区分开．箭头表示“由孩子所在的子树推出父节点所在的子树”，信息自下而上流动：

Remark 4.6 “最小 + 归纳”的历史 [history-of-least-sets-and-induction]

2026-10-10
Glomzzz

打开独立页面 →

Convention 4.7 归纳证明的写法 [writing-inductive-proofs]

2026-10-10
Glomzzz

写“对 $𝑡$ 结构归纳”时，意思是应用结构归纳原理：按项的形状逐个情形讨论，每个情形里可以对直接子项与真子项给出的直接子项使用归纳假设．采用规则归纳法作规则归纳时，归纳假设只能用于规则前提对应的子推导，不能随便套在任意相关的项上．

先用两个函数练手，它们分别计算一棵语法树有多少个节点、有多深：

Definition 4.8 大小与深度 [size-and-depth]

2026-10-10
Glomzzz

对词项的集合的有限语法树，大小 $size (𝑡)$ 数节点，深度 $depth (𝑡)$ 数从根到最远叶子的路径上的边．两个函数按直接子项与真子项的直接子项递归定义：

$\begin{matrix} size (true) = size (false) = size (0) = 1 \\ size (succ 𝑡_{1}) = size (pred 𝑡_{1}) = size (iszero 𝑡_{1}) = size (𝑡_{1}) + 1 \\ size (if 𝑡_{1} then 𝑡_{2} else 𝑡_{3}) = size (𝑡_{1}) + size (𝑡_{2}) + size (𝑡_{3}) + 1 \end{matrix}$

深度数的是从根到最远叶子的路径上的边数（区别于节点数），完整定义为：

$\begin{matrix} depth (true) = depth (false) = depth (0) = 0 \\ depth (succ 𝑡_{1}) = depth (pred 𝑡_{1}) = depth (iszero 𝑡_{1}) = depth (𝑡_{1}) + 1 \\ depth (if 𝑡_{1} then 𝑡_{2} else 𝑡_{3}) = \max (depth (𝑡_{1}), depth (𝑡_{2}), depth (𝑡_{3})) + 1 \end{matrix}$

例如 $pred (succ 0)$ 有三个节点、两条边，所以大小是 $3$ ，深度是 $2$ ． $if true then 0 else (succ 0)$ 的大小是 $5$ ，深度也是 $2$ ：大小把三个分支都算进去，深度只取最长的那条路径．

按项的形状逐个情形写等式，之所以能定义出函数，是因为每个项恰好属于一种形状（抽象语法已经保证没有歧义），而右边只用到直接子项的函数值，子项又更小，一路往下总会落到常量上．这种定义方式称为结构递归，它和结构归纳相伴而生：结构归纳沿着项的构造过程证明性质，结构递归则沿着同样的结构定义函数．熟悉 Haskell 的读者会认出，这正是许多基于归纳类型（也称代数数据类型）和模式匹配的递归函数所采用的方式． Haskell 也允许非结构递归，但不能把它们一概称为共递归；利用惰性求值逐步产生无限列表是共递归的常见例子，还须检查它能否持续给出可观察部分（什么是归纳）．

接下来这条引理检查“大小”和“深度”两个定义是否协调：最长路径用到的节点不会超过整棵树的节点数．它也给递归的资源估计一个上界，例如遍历语法树时，递归栈深度不超过节点总数．没有这个证明，这只是直觉；如果误把 $if$ 的深度写成三个分支深度之和加一，就不再是在数最长路径了．例如三个分支各有深度 $1$ 时，这种错误写法给出 $4$ ，但实际最长路径只有 $2$ 条边．要证明递归终止，还需另查每次调用的参数是否严格变小，不能只引用一个数值上界．

Lemma 4.9 深度小于大小 [depth-is-less-than-size]

2026-10-10
Glomzzz

对词项的集合中的所有有限项 $𝑡$ ，采用大小与深度的函数定义，有 $depth (𝑡) < size (𝑡)$ ．

Proof.

按结构归纳原理对 $𝑡$ 作结构归纳．若 $𝑡$ 是常量，则 $depth (𝑡) = 0 < 1 = size (𝑡)$ ．若 $𝑡 = succ 𝑡_{1}$ （ $pred$ 、 $iszero$ 完全相同），归纳假设是 $depth (𝑡_{1}) < size (𝑡_{1})$ ，两边加一即得 $depth (𝑡) < size (𝑡)$ ．若 $𝑡 = if 𝑡_{1} then 𝑡_{2} else 𝑡_{3}$ ，设 $𝑡_{𝑖}$ 是三个子项中深度最大的，由归纳假设得

$depth (𝑡) = depth (𝑡_{𝑖}) + 1 < size (𝑡_{𝑖}) + 1 \leq size (𝑡_{1}) + size (𝑡_{2}) + size (𝑡_{3}) + 1 = size (𝑡)$

其中

\leq

用到了每个子项的大小都至少为

1

．

∎

这就是结构归纳证明的基本思路：虽然项有无穷多个，但构造它们的规则只有有限几条。我们只需按这些规则逐一讨论：基础情形直接验证，递归情形则借助对子项的归纳假设，一步步推出结论．

Remark 4.10 潜无穷与实无穷 [potential-and-actual-infinity]

2026-10-10
Glomzzz

打开独立页面 →

5 练习：语法

Exercises (5)

Exercise 2.1. 把项还原成树

画出

if (iszero (pred 0)) then (succ (succ 0)) else (pred (succ 0))

的树，标出根、叶子与内部节点，列出直接子项，计算大小和深度，并判断

0

是否属于整项的直接子项．依据树的基本术语、直接子项与真子项与大小与深度作答．

Hint

根是

if

；三个直接子项要按条件、

then

分支、

else

分支的顺序列出．大小数节点，深度数最长路径上的边．

Solution

if
├── iszero
│   └── pred
│       └── 0
├── succ
│   └── succ
│       └── 0
└── pred
    └── succ
        └── 0

if
├── iszero
│   └── pred
│       └── 0
├── succ
│   └── succ
│       └── 0
└── pred
    └── succ
        └── 0

三个直接子项依次是 $iszero (pred 0)$ 、 $succ (succ 0)$ 、 $pred (succ 0)$ ，大小都为 $3$ ，深度都为 $2$ ．所以整项大小为 $1 + 3 + 3 + 3 = 10$ ，深度为 $1 + \max (2, 2, 2) = 3$ ．

三个标着 $0$ 的节点都没有孩子，都是叶子；根 $if$ 和其余六个一元节点都是内部节点． $0$ 属于整项的真子项，但隔着中间节点，不算整项的直接子项．不能因为三个叶子的标签相同，就把它们合并成同一个位置．

Exercise 2.2. 语法合法，不等于满足类型规则

判断下面四种写法是否描述本文的项；构成项的写出构造过程，不构成项的说明生成条件缺了什么：

succ false

、

if 0 then true else 0

、单独的 pred pred 、字面记号 1 1 ．不要用“它运行时会出错”作为不属于项集合的理由．

Hint

这里仅使用词项的集合的生成条件，不提前使用后面的求值或类型规则．

Solution

$succ false$ 是项：先由第一条生成 $false$ ，再由第二条包上 $succ$ ． $if 0 then true else 0$ 也是项：三个常量都由第一条生成，再用第三条组合．

单独的 pred pred 缺少子项，不构成词项．字面记号 1 1 也不在这套抽象语法里；后面会用 $succ 0$ 表示自然数一，但不能未经约定就把 1 1 当成已有的构造．前两个项都满足语法的生成条件；这既不保证它们有类型，也不保证求值能到达值．是否有类型、怎样规约，要分别对照后面各自的规则，不能混成一个“有没有意义”的判断．

Exercise 2.3. 封闭与最小的分工

设

S = 花体(T) \cup {null}

，只比原项集合多一个新叶子．判断

𝑆

是否满足原来的三条封闭条件；若不满足，说明怎样扩充才封闭，并指出扩充后的集合与词项的集合定义的集合差在哪个条件上．

Hint

考虑集合里一旦有 null null ，封闭条件对

succ

所提出的要求．

Solution

$S = 花体(T) \cup {null}$ 不封闭： $null \in 𝑆$ ，但 $succ null \notin 𝑆$ ； $succ null$ 既不在原语言的项集合 $花体(T)$ 中，也不等于新添的叶子 null null ．

要得到含 null null 的封闭集合，必须同时加入所有由原构造子和这个额外叶子在有限步内搭出的树，包括 $succ null$ 、 $if null then 0 else true$ 等．这个集合满足原来的封闭条件，却严格大于 $花体(T)$ ． “封闭”要求构造后不能跑到集合外，“最小”则排除规则没有生成的额外东西．

Exercise 2.4. 证明边数比节点数少一

令

𝐸 (𝑡)

表示项

𝑡

的语法树中的边数．写出

𝐸

的完整结构递归定义，并用结构归纳原理证明

𝐸 (𝑡) = size (𝑡) - 1

．每个归纳步骤都要写清归纳假设用在哪个子项上．

Hint

常量有零条边；一元构造增加一条边；

if

根连向三个孩子，增加三条边．

Solution

完整的结构递归定义为：

$\begin{matrix} 𝐸 (true) = 𝐸 (false) = 𝐸 (0) = 0 \\ 𝐸 (succ 𝑡_{1}) = 𝐸 (pred 𝑡_{1}) = 𝐸 (iszero 𝑡_{1}) = 𝐸 (𝑡_{1}) + 1 \\ 𝐸 (if 𝑡_{1} then 𝑡_{2} else 𝑡_{3}) = 𝐸 (𝑡_{1}) + 𝐸 (𝑡_{2}) + 𝐸 (𝑡_{3}) + 3 \end{matrix}$

对 $𝑡$ 结构归纳．常量有 $𝐸 (𝑡) = 0 = 1 - 1$ ．一元情形由子项上的归纳假设得

$𝐸 (succ 𝑡_{1}) = 𝐸 (𝑡_{1}) + 1 = size (𝑡_{1}) = size (succ 𝑡_{1}) - 1$

$pred$ 、 $iszero$ 的等式相同．

对 $if 𝑡_{1} then 𝑡_{2} else 𝑡_{3}$ ，三个子项上的归纳假设分别是 $𝐸 (𝑡_{𝑖}) = size (𝑡_{𝑖}) - 1$ ．三棵子树的边加上根的三条边，得到

$\begin{matrix} 𝐸 (𝑡) & = 𝐸 (𝑡_{1}) + 𝐸 (𝑡_{2}) + 𝐸 (𝑡_{3}) + 3 \\ = (size (𝑡_{1}) - 1) + (size (𝑡_{2}) - 1) + (size (𝑡_{3}) - 1) + 3 \\ = size (𝑡_{1}) + size (𝑡_{2}) + size (𝑡_{3}) \\ = size (𝑡) - 1 \end{matrix}$

全部构造情形都覆盖了，因此结论对所有项成立．∎

Exercise 2.5. 两种不同的错误“归纳证明”

令

𝑃 (𝑡)

为“

size (𝑡) \leq 3

”．有人分别写出两段归纳步骤： “假定

𝑃 (succ 𝑡_{1})

，所以

𝑃 (succ 𝑡_{1})

”； “假定

𝑃 (𝑡_{1})

，大小加一仍不超过

3

，所以

𝑃 (succ 𝑡_{1})

”．指出两段论证各自的错误，给出具体反例，并区分“假设用错对象”与“由归纳假设推不出结论”．

Hint

先核对第一段使用的假设对象，再检查第二段的不等式能否从子项传给父项．

Solution

第一段是循环论证：它直接把当前待证的 $𝑃 (succ 𝑡_{1})$ 当作假设，没有使用结构归纳许可的子项性质 $𝑃 (𝑡_{1})$ ，只相当于说了“结论蕴涵自身”．

第二段使用子项上的假设本身合法，但推理错误： $size (𝑡_{1}) \leq 3$ 只能给出 $size (succ 𝑡_{1}) \leq 4$ ，不能给出 $\leq 3$ ．取 $𝑡_{1} = succ (succ 0)$ ，子项大小为 $3$ ，包上一层后为 $4$ ．可见 $𝑃$ 本身就是假命题，光修改措辞也无法把它证出来． $if true then 0 else 0$ 也是大小为 $4$ 的反例．

. 语法：BNF、最小集合与结构归纳

References

Backlinks