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

Glomzzz
2026-10-10
About

1 语法树

1.1 [约定] 抽象语法 [abstract-syntax]

2026-10-10
Glomzzz

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

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

2 BNF

描述语法树长什么样，最常用的写法是 BNF，全称巴科斯–诺尔范式（Backus–Naur Form，参见维基百科）。它得名于巴科斯（John Backus）和诺尔（Peter Naur）：1960 年的 ALGOL 60 报告第一次用这种写法给一门程序语言写出了完整的语法，此后几乎所有语言的规格都沿用了它的某种变体。

BNF 的一行叫一条产生式（production），形如

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

$⩴$ 读作“定义为”或“可以是”；
$|$ 读作“或者”，把几种选项隔开；
每个选项是一串符号，其中有些是写死的关键字（如 $if$ 、 $succ$ ），有些是名字本身，表示“这里放一个同类的东西”。

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

$𝑛 ⩴ 0 | succ 𝑛$

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

3 项

对象语言的程序称为项（term），用字母 $𝑡$ 表示。项的写法用一行 BNF 给出：

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

竖线读作“或者”。 $succ 𝑡$ 是“ $𝑡$ 的后继”（successor），可以理解为加一； $pred 𝑡$ 是“前驱”（predecessor），可以理解为减一； $iszero 𝑡$ 问 $𝑡$ 是不是零。例如 $if (iszero (pred (succ 0))) then 0 else succ 0$ 是一个项，它对应的语法树如下：

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

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

2026-10-10
Glomzzz

对 [定义] 项的集合中的项，采用 [定义] 树的基本术语的树术语。根节点的每个孩子所对应的整棵子树，称为它的直接子项（immediate subterm）。具体地：

$true$ 、 $false$ 、 $0$ 没有直接子项；
$succ 𝑡_{1}$ 、 $pred 𝑡_{1}$ 、 $iszero 𝑡_{1}$ 的唯一直接子项是 $𝑡_{1}$ ；
$if 𝑡_{1} then 𝑡_{2} else 𝑡_{3}$ 的三个直接子项按顺序是 $𝑡_{1}$ 、 $𝑡_{2}$ 、 $𝑡_{3}$ 。

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

这一行 BNF 看起来是在描述“项长什么样”，但严格来说它是在定义一个集合。

3.2 [定义] 项的集合 [set-of-terms]

2026-10-10
Glomzzz

把项视为 [约定] 抽象语法中的有限语法树，常量 $true$ 、 $false$ 、 $0$ 是叶子， $succ$ 、 $pred$ 、 $iszero$ 是一元构造， $if$ 有条件、then 分支和 else 分支三个有序子项。

项的集合是满足下面三条封闭条件（closure conditions）的最小（least）集合：

，，；
若，则 $succ 𝑡_{1}$ 、 $pred 𝑡_{1}$ 、 $iszero 𝑡_{1}$ 都属于；
若，则。
“最小”的意思是：如果另一个集合 $𝑆$ 也满足这三条，那么。

注：这个符号是字母T的花体, 可以读作 script T script T 。

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

为什么还要加“最小”？因为满足封闭条件的集合有很多。比如允许额外的叶子 null null ，并且把所有包含这个新叶子的 $succ$ 、 $if$ 等树也一起加进来，得到的更大集合仍然满足封闭条件。但 null null 不是本文的项，因为三条生成条件没有给出它。注意只加 null null 而不加 $succ null$ 等树，反而会破坏封闭性。

取最小的那个，就是在说：项只有用上面三条规则、在有限步内搭出来的东西，别的一概不算。

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

2026-10-10
Glomzzz

[定义] 项的集合有一个存在性前提：满足那三条封闭条件的集合中真的有一个最小的。先固定一个背景集合 $𝑈$ ，包含节点标签取自 $true$ 、 $false$ 、 $0$ 、 $succ$ 、 $pred$ 、 $iszero$ 、 $if$ 的所有有限有序树（暂不限制每个标签的孩子数量）。 $𝑈$ 本身满足三条封闭条件，所以满足条件的 $𝑈$ 的子集至少有一个，取交集不是在对空的一族集合操作。

把所有满足封闭条件的 $𝑈$ 的子集取交集，记为 $𝐼$ ：

每个集合都含 $true$ 、 $false$ 、 $0$ ，所以 $𝐼$ 也含这三个常量；
若 $𝑡_{1} \in 𝐼$ ，则 $𝑡_{1}$ 在每个集合里。每个集合都对三个一元构造封闭，所以 $succ 𝑡_{1}$ 、 $pred 𝑡_{1}$ 、 $iszero 𝑡_{1}$ 也在每个集合里，因而在 $𝐼$ 里；
若 $𝑡_{1}, 𝑡_{2}, 𝑡_{3} \in 𝐼$ ，它们在每个集合里。每个集合都对 $if$ 构造封闭，所以 $if 𝑡_{1} then 𝑡_{2} else 𝑡_{3}$ 也在交集里。

因此 $𝐼$ 满足全部封闭条件，而且按交集的定义，它包含在每个满足条件的集合里。这就是所需的最小集合，不是从一堆集合里凭直觉挑一个。

由此可以得到两件事。第一，每个项都是一棵有限的树：叶子是 $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 的指针，并且独占它指向的那块内存。为什么不直接写 Succ(Term) Succ(Term) ？因为 Rust 要在编译时知道每个类型占多少字节。如果 Succ Succ 里直接装一个 Term Term ，那个 Term Term 里又可能装一个 Term Term ……大小就成了无穷大，编译器会报错（“recursive type has infinite size”）。换成 Box Box 以后， Succ Succ 里装的只是一个固定大小的指针，真正的子树放在堆上。

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

4 结构归纳

“最小”不只是为了排除例外，它还直接送给我们一条证明方法。我们常常想证明“所有项都有某个性质 $𝑃$ ”。项有无穷多个，不能一个个检查；但项的集合是用三条规则“搭”出来的，所以只要性质能跟着这三条规则一起“搭”上去就行。

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

2026-10-10
Glomzzz

“归纳”（induction）这个词在不同领域里意思不一样，先分清楚。

在经验科学和日常推理里，归纳推理是从有限个观察得出普遍结论：见过的天鹅都是白的，于是“所有天鹅都是白的”。与它对立的是演绎推理（deduction）：从前提出发，按逻辑规则推出结论，前提为真则结论必真。归纳推理的结论可能出错（澳大利亚有黑天鹅），休谟（Hume）在 18 世纪指出，归纳推理没有逻辑上的保证，这就是归纳问题。
数学里的数学归纳法名字里虽然有“归纳”，却是一种演绎：证明 $𝑃 (0)$ ，再证明“ $𝑃 (𝑛)$ 蕴涵 $𝑃 (𝑛 + 1)$ ”，就能断定所有自然数都满足 $𝑃$ ，没有任何“可能出错”的余地。 [定理] 结构归纳原理（structural induction）与 [定理] 对推导归纳使用的也是这种演绎证明方法。

数学归纳法的历史很长。古希腊的欧几里得（Euclid）证明素数有无穷多个时，已经有了它的影子；16 世纪的莫罗利科（Maurolico）、17 世纪的帕斯卡（Pascal）在讨论二项式系数时比较明确地用了它；“数学归纳法”这个名字是 19 世纪德摩根（De Morgan）起的。19 世纪末，戴德金（Dedekind）和皮亚诺（Peano）把它写成了自然数的公理之一，并指出它其实来自“自然数是包含 $0$ 、对后继封闭的最小集合”。 [定理] 结构归纳原理（structural induction）把这个想法从自然数推广到由规则搭起来的有限树。

在程序语言理论里，和归纳对立的是余归纳（coinduction）。归纳对应“最小”的集合，处理有限的、搭得完的对象；余归纳对应“最大”的集合，处理可以无限展开的对象，比如永不停机的程序、无穷长的数据流。 [定义] 项的集合的有限项与 [定义] 一步归约的有限推导都属于归纳定义的对象。

先让我们来想想“最小”为什么能推出归纳。

设 $𝑆$ 是所有满足 $𝑃$ 的项组成的集合。

如果 $𝑃$ 能“跟着规则搭上去”，意思就是： $𝑆$ 也满足那三条封闭条件，它也是一个“规则搭不出去”的集合。

而是这样的集合里最小的那个，即是每一个这样的集合的子集。

所以当然也是 $𝑆$ 的子集，于是的每个项都在 $𝑆$ 里，都满足 $𝑃$ 。

如果没有“最小”，里可能混进 null null 这样的例外，它不是任何上面那三条规则搭出来的，规则对这种例外什么也没说， $𝑃$ 对它成不成立也就无从谈起。

所以“最小”保证了里只有规则搭出来的东西，所以“对每条规则检查一遍”就等于“对每个项检查一遍”。

下面把这段话写成定理。

4.2 [定理] 结构归纳原理（structural induction） [structural-induction]

2026-10-10
Glomzzz

设 $𝑃$ 是关于 [定义] 项的集合中有限项的一个性质。如果下面三条都成立：

$𝑃 (true)$ 、 $𝑃 (false)$ 、 $𝑃 (0)$ ；
对任意项 $𝑡_{1}$ ，由 $𝑃 (𝑡_{1})$ 能推出 $𝑃 (succ 𝑡_{1})$ 、 $𝑃 (pred 𝑡_{1})$ 、 $𝑃 (iszero 𝑡_{1})$ ；
对任意项 $𝑡_{1}, 𝑡_{2}, 𝑡_{3}$ ，由 $𝑃 (𝑡_{1})$ 、 $𝑃 (𝑡_{2})$ 、 $𝑃 (𝑡_{3})$ 能推出 $𝑃 (if 𝑡_{1} then 𝑡_{2} else 𝑡_{3})$ ，

那么对所有项 $𝑡$ ， $𝑃 (𝑡)$ 成立。

证明

令

，即满足

𝑃

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

𝑆

满足 [定义] 项的集合的三条封闭条件。由于

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

。也就是说每个项都在

𝑆

里，都满足

𝑃

。

∎

在这里，结构归纳不是额外请来的对象语言公理：在元语言的集合论背景下，它由“最小”这两个字推出。这里不是说一切数学基础都不需要公理，而是说定义了这个最小集合以后，不必再另加一条关于它的归纳公理。

4.3 [定义] 归纳假设 [induction-hypothesis]

2026-10-10
Glomzzz

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

在 [定理] 结构归纳原理（structural induction）的第 2 条中，归纳假设是 $𝑃 (𝑡_{1})$ ；第 3 条中是 $𝑃 (𝑡_{1})$ 、 $𝑃 (𝑡_{2})$ 、 $𝑃 (𝑡_{3})$ 。这些对象恰好是 [定义] 直接子项与真子项中列出的直接子项。常量没有子项，所以基础情形没有归纳假设，必须直接证明。

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

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

2026-10-10
Glomzzz

取 [定义] 项的集合中的有限项，树的术语见 [定义] 树的基本术语，归纳方法采用 [定理] 结构归纳原理（structural induction）。

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

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

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

4.5 [附注] 归纳假设不只限于直接子项 [scope-of-induction-hypotheses]

2026-10-10
Glomzzz

“只能对直接子项使用”是 [定理] 结构归纳原理（structural induction）的直接表述，不是一切归纳法的限制。若改用强归纳，先证明某个自然数度量严格下降，就可以对度量更小的任意对象使用归纳假设；对真子项的归纳也可以成立。一般的要求叫良基性（well-foundedness）：不存在无限地向更小对象下降的链。

[定义] 直接子项与真子项的直接子项关系在 [定义] 项的集合的有限树上是良基的，但“归约后的项”并不因此自动是直接子项。例如按 [定义] 一步归约， $succ (pred 0)$ 一次计算变成 $succ 0$ ，后者不是前者的直接子项。要在证明中对归约结果使用归纳假设，必须另证合适的度量下降，或选择相应的归纳原理。用在一个不被当前归纳原理许可的对象上，证明就是缺了一步；若这个缺口依赖当前结论来填，就构成循环论证。

下图是一个例子。要证 $𝑃$ 对整棵树成立，只需要：叶子处直接验证（第 1 条），每个内部节点处假定以它的各个孩子为根的子项都满足 $𝑃$ ，再推出以当前节点为根的项满足 $𝑃$ （第 2、3 条）。这里 $𝑃$ 是项的性质，不是单个节点标签的性质。箭头表示“由孩子所在的子树推出父节点所在的子树”，信息自下而上流动：

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

2026-10-10
Glomzzz

“先把东西定义成满足某些规则的最小对象，再沿着这些规则归纳”，这个方法在许多理论里反复出现：

自然数：戴德金 1888 年的《数是什么，应该是什么？》把自然数定义为包含 $1$ 、对后继封闭的所有集合的交（他称为“链”），由此证明了数学归纳法，而不是把它当作公理。皮亚诺 1889 年的公理系统则把同一件事写成了第五条公理。
递归函数论：克莱尼（Kleene）等人在 1930 年代把“可计算函数”定义为包含基本函数、对复合和递归封闭的最小函数类。
不动点定理：克纳斯特–塔斯基定理（1928 / 1955）说，完备格上的单调函数有最小不动点。 [定义] 项的集合的“最小集合”正是“由封闭条件确定的函数”的最小不动点，这是归纳定义最一般的数学基础。
形式语言：BNF 定义的语言，就是满足产生式的最小字符串集合。
类型论：马丁-洛夫（Martin-Löf）的直觉主义类型论（1970 年代）把“归纳类型”作为基本构造：一个类型由它的构造子给出，并自动附带一个归纳原理。Coq、Lean、Agda 里的 Inductive Inductive / inductive inductive / data data 就是这个想法的直接实现，Rust 的 enum enum 也是它的一个简化版。
程序语义：普洛特金（Plotkin）1981 年的结构化操作语义讲义，把“程序怎么运行”写成推导规则定义的最小关系， [定义] 一步归约使用的就是这种做法。

这些理论研究的对象虽然各不相同，用的方法是同一个。

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

2026-10-10
Glomzzz

写“对 $𝑡$ 结构归纳”时，意思是套用 [定理] 结构归纳原理（structural induction）：按项的形状逐个情形讨论，每个情形里可以对 [定义] 直接子项与真子项所列的直接子项使用 [定义] 归纳假设中说明的假设。采用 [定理] 对推导归纳对推导归纳时，更小对象则是规则前提对应的子推导，不是任意一个看起来有关的项。

先拿一个简单的性质练手。下面两个函数分别数一棵树有多少个节点、有多深：

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$ ：大小把三个分支都算进去，深度只取最长的那条路。

这里又有一个隐含前提：按项的形状逐个情形写等式，真的定义出了一个函数吗？答案是肯定的，因为每个项恰好属于一种形状（ [约定] 抽象语法已经保证没有歧义），而右边只用到直接子项的函数值，子项又更小，一路往下总会落到常量上。这种定义方式称为结构递归（structural recursion），它和结构归纳是同一枚硬币的两面：结构归纳沿着项的构造过程证明性质，结构递归则沿着同样的结构定义函数。（熟悉 Haskell 的读者应该能认出，这正是许多基于代数数据类型（algebraic data type）和模式匹配（pattern matching）的递归函数所采用的方式；当然Haskell也允许非结构递归甚至利用惰性求值定义的无限结构，这属于共递归（corecursion）的典型形式，而不是通常意义上对有限归纳数据的结构递归。）

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

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

2026-10-10
Glomzzz

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

证明

按 [定理] 结构归纳原理（structural induction）对 $𝑡$ 进行结构归纳。

$𝑡$ 是常量： $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$ 。

∎

形式化证明大致就是这个样子：按定义的情形逐个过，每个情形里只用定义和归纳假设。

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

2026-10-10
Glomzzz

亚里士多德（Aristotle）区分过两种无穷：潜无穷（potential infinity）是一个可以无限进行下去的过程，比如数数总能再数一个；实无穷（actual infinity）是一个已经完成的无穷整体。项的集合两种读法都可以：按 [定义] 项的集合的写法，它是一个现成的无穷集合（实无穷）；按“用规则在有限步内搭出来”的读法，每个项都是一个有限过程的产物（潜无穷）。

[定理] 结构归纳原理（structural induction）的巧妙之处在于，它让我们对一个无穷集合下结论，却只需检查有限多条规则。这也是数学基础里构造主义者（constructivist）认可归纳定义的原因：每个对象都有一个有限的构造历史。

5 练习：语法

本节练习（5题）

练习2.1：把项还原成树

画出

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

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

0

是否是整项的直接子项？依据 [定义] 树的基本术语、 [定义] 直接子项与真子项与 [定义] 大小与深度作答。

提示

根是

if

；三个直接子项要按条件、then、else 的顺序列出。大小数节点，深度数最长路径上的边。

参考答案

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$ 是整项的真子项，但不是直接子项。不能因为三个叶子的标签相同，就把它们合并成同一个位置。

练习2.2：语法合法，不等于有意义

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

succ false

、

if 0 then true else 0

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

提示

这里仅使用 [定义] 项的集合的生成条件，不提前使用后面的求值或类型规则。

参考答案

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

单独的 pred pred 不是项，因为这个构造必须带一个子项。字面记号 1 1 也不在这套抽象语法里；后面会用 $succ 0$ 表示自然数一，但不能未经约定就把 1 1 当成已有的构造。前两个项的语法合法，并不保证运算能正常进行。

练习2.3：封闭与最小各负责什么？

设

，只比原项集合多一个新叶子。

𝑆

是否满足原来的三条封闭条件？若不满足，应当怎样扩充才封闭？扩充后的集合为什么仍不是 [定义] 项的集合定义的集合？

提示

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

succ

会提出什么要求？

参考答案

不封闭： $null \in 𝑆$ ，但 $succ null \notin 𝑆$ 。它既不是原语言的项，也不是单独补进去的 null null 。

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

练习2.4：证明边数比节点数少一

令

𝐸 (𝑡)

表示项

𝑡

的语法树中的边数。写出

𝐸

的完整结构递归定义，并用 [定理] 结构归纳原理（structural induction）证明

𝐸 (𝑡) = size (𝑡) - 1

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

提示

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

if

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

参考答案

完整的结构递归定义为：

$\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}$

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

练习2.5：两种不同的错误“归纳证明”

令

𝑃 (𝑡)

为“

size (𝑡) \leq 3

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

𝑃 (succ 𝑡_{1})

，所以

𝑃 (succ 𝑡_{1})

”；“假定

𝑃 (𝑡_{1})

，大小加一仍不超过

3

，所以

𝑃 (succ 𝑡_{1})

”。它们各错在哪里？给出具体反例，并说明为什么第二段不能简单称为“假设用错对象”。

提示

第一段用了哪个对象上的假设？第二段虽然取了子项，还要检查不等式是否真的能传给父项。

参考答案

第一段是循环论证：它假定的是当前待证的 $𝑃 (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$ 的反例。

References

[] 求值：用推导规则定义运行 [evaluation]

[定义] 树的基本术语 [tree-terminology]

[] 形式化入门：从 BNF 到类型安全 [index]

[] 为什么形式化：自然语言与元语言 [natural-and-formal]

Backlinks

[] 为什么形式化：自然语言与元语言 [natural-and-formal]

[] 求值：用推导规则定义运行 [evaluation]

Based on Typsite