• 对象语言（object language）：被研究的那门语言。
• 元语言（metalanguage）：用来谈论对象语言的语言。

例如， [定义] 项的集合 、 [定义] 一步归约 与 [定义] 类型与类型判断 规定的布尔值／自然数语言是对象语言；用来写这些定义和证明的自然语言与数学符号属于元语言。用 Rust 实现这门小语言时，Rust 也充当元语言，见 [附注] Rust 也是元语言 。

用 Rust 实现 [定义] 项的集合 的项和 [定义] 一步归约 的运行规则时，Rust 充当 [定义] 对象语言与元语言 中的元语言：Rust 的 enum Term enum Term 描述对象语言的项，Rust 的函数描述对象语言的运行。不要把 Rust 自己的类型（ bool bool 、 Option Option ）和 [定义] 类型与类型判断 中的对象语言类型（$\text{Bool}$、$\text{Nat}$）混为一谈，它们分属两层。实现示例见 Rust 求值器 与 Rust 类型检查器 。

“对象语言 / 元语言”这对术语来自逻辑学家塔斯基（Tarski）。1930 年代他研究“真”这个概念时发现，像说谎者悖论（liar paradox，“这句话是假的”）这样的困境，根源在于一门语言试图谈论自身句子的真假。他的方案是分层：关于对象语言 $𝐿$ 的句子是否为真，只能在更高一层的元语言里说。

程序语言理论中的 [定义] 对象语言与元语言 采用同样的区分：被研究的语言和研究它的语言分属两个层次。后来者在这基础上发展出了更精细的做法（比如允许一门语言有限度地谈论自身的“反射”（reflection）），但出发点都是先把层次分清。

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

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

• $\text{true}$、$\text{false}$、$0$ 没有直接子项；
• $\text{succ }{𝑡}_1$、$\text{pred }{𝑡}_1$、$\text{iszero }{𝑡}_1$ 的唯一直接子项是 ${𝑡}_1$；
• $\text{if }{𝑡}_1\text{ then }{𝑡}_2\text{ else }{𝑡}_3$ 的三个直接子项按顺序是 ${𝑡}_1$、${𝑡}_2$、${𝑡}_3$。

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

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

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

1. ，，；
2. 若 ，则 $\text{succ }{𝑡}_1$、$\text{pred }{𝑡}_1$、$\text{iszero }{𝑡}_1$ 都属于 ；

3. 若 ，则 。

   “最小”的意思是：如果另一个集合 $𝑆$ 也满足这三条，那么 。

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

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

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

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

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

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

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

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

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

1. $𝑃\left(\text{true}\right)$、$𝑃\left(\text{false}\right)$、$𝑃\left(0\right)$；
2. 对任意项 ${𝑡}_1$，由 $𝑃\left({𝑡}_1\right)$ 能推出 $𝑃\left(\text{succ }{𝑡}_1\right)$、$𝑃\left(\text{pred }{𝑡}_1\right)$、$𝑃\left(\text{iszero }{𝑡}_1\right)$；
3. 对任意项 ${𝑡}_1,{𝑡}_2,{𝑡}_3$，由 $𝑃\left({𝑡}_1\right)$、$𝑃\left({𝑡}_2\right)$、$𝑃\left({𝑡}_3\right)$ 能推出 $𝑃\left(\text{if }{𝑡}_1\text{ then }{𝑡}_2\text{ else }{𝑡}_3\right)$，

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

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

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

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

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

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

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

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

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

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

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

• 自然数：戴德金 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 年的结构化操作语义讲义，把“程序怎么运行”写成推导规则定义的最小关系， [定义] 一步归约 使用的就是这种做法。

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

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

对 [定义] 项的集合 的有限语法树，大小 $\mathrm{size}\left(𝑡\right)$ 数节点，深度 $\mathrm{depth}\left(𝑡\right)$ 数从根到最远叶子的路径上的边。函数按 [定义] 直接子项与真子项 的直接子项递归定义。

$$\begin{array}{c}\mathrm{size}\left(\text{true }\right)=\mathrm{size}\left(\text{false }\right)=\mathrm{size}\left(0\right)=1\\ \mathrm{size}\left(\text{succ }{𝑡}_1\right)=\mathrm{size}\left(\text{pred }{𝑡}_1\right)=\mathrm{size}\left(\text{iszero }{𝑡}_1\right)=\mathrm{size}\left({𝑡}_1\right)+1\\ \mathrm{size}\left(\text{if }{𝑡}_1\text{ then }{𝑡}_2\text{ else }{𝑡}_3\right)=\mathrm{size}\left({𝑡}_1\right)+\mathrm{size}\left({𝑡}_2\right)+\mathrm{size}\left({𝑡}_3\right)+1\end{array}$$

深度数的是从根到最远叶子的路径上的边数，不是节点数。完整定义为：

$$\begin{array}{c}\mathrm{depth}\left(\text{true }\right)=\mathrm{depth}\left(\text{false }\right)=\mathrm{depth}\left(0\right)=0\\ \mathrm{depth}\left(\text{succ }{𝑡}_1\right)=\mathrm{depth}\left(\text{pred }{𝑡}_1\right)=\mathrm{depth}\left(\text{iszero }{𝑡}_1\right)=\mathrm{depth}\left({𝑡}_1\right)+1\\ \mathrm{depth}\left(\text{if }{𝑡}_1\text{ then }{𝑡}_2\text{ else }{𝑡}_3\right)=\max \left(\mathrm{depth}\left({𝑡}_1\right),\mathrm{depth}\left({𝑡}_2\right),\mathrm{depth}\left({𝑡}_3\right)\right)+1\end{array}$$

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

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

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

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

在 [定义] 项的集合 的项中，用以下 BNF 划出值。$⩴$ 读作“定义为”，$|$ 读作“或者”； 是数值的元变量，不是对象语言的关键字。

形如 $𝑣$ 的项称为值（value），形如 的项称为数值（numeric value）。和 [定义] 项的集合 一样，这两行 BNF 定义的是满足相应封闭条件的最小集合。

以下读法使用 [定义] 项的集合 中的项，以及 [定义] 一步归约 定义的关系 $⟶$。

• $𝑡⟶{𝑡}^{\prime }$ 读作“$𝑡$ 一步归约到 ${𝑡}^{\prime }$”，英文常读作 “$𝑡$ steps to ${𝑡}^{\prime }$” 或 “$𝑡$ reduces to ${𝑡}^{\prime }$”。
• 它是一个命题，可以成立也可以不成立，就像 $1<2$ 成立、$2<1$ 不成立一样。例如 $\text{pred }0⟶0$ 成立；$0⟶\text{ pred }0$ 不成立。
• 箭头是有方向的：左边是归约前的项，右边是归约后的项。
• 它不是函数调用，也不是赋值。$𝑡⟶{𝑡}^{\prime }$ 不会“改变” $𝑡$，它只是断言 $𝑡$ 与 ${𝑡}^{\prime }$ 之间有这样一种关系。
• 写 $𝑡⟶{𝑡}^{\prime }$ 的时候没有说 ${𝑡}^{\prime }$ 是唯一的；唯一性是要证明的（ [定理] 确定性 ）。
• ${⟶}^{\ast }$ 读作“多步归约到”，其含义由 [定义] 多步归约 给出。

在 [定义] 一步归约 与 [定义] 类型与类型判断 的规则里，${𝑡}_1,{𝑡}_2,{𝑡}_{1^{\prime }}$ 等字母是元变量（metavariable）：它们是元语言里的变量，可以代换成 [定义] 项的集合 中的任意项； 只能代换成 [定义] 值与数值 中的数值。同一条规则里同一个字母必须代换成同一个东西。一条规则因此代表无穷多条实例（instance）。

设 $𝑡$、${𝑡}^{\prime }$ 属于 [定义] 项的集合 的项集合， 只取 [定义] 值与数值 中的数值。关系 $𝑡⟶{𝑡}^{\prime }$ 是对下列十条规则封闭的最小关系。

每条横线之上的判断是前提，横线之下的是结论；前提全部成立，结论才成立。没有前提的规则可以直接使用。同一条规则中相同的元变量必须替换成同一个项，见 [约定] 元变量 。

以 [定义] 项的集合 的语法和 [定义] 一步归约 的十条求值规则为基础，可以另行加入错误项 $\text{wrong}$，并规定错误传播。以下讨论的是这门扩展语言，不把新增规则当作未扩展语言的规则。只写 $\text{succ }\text{ true }⟶\text{ wrong}$ 还不完整：还要处理 $\text{succ }\text{ false}$、$\text{pred }\text{ true}$、非布尔条件，以及嵌套位置里的错误。

记 $𝑏$ 为 $\text{true}$ 或 $\text{false}$， 为 [定义] 值与数值 中的数值。可以补上这些错误规则，其中 $\text{op}$ 分别取 $\text{succ}$、$\text{pred}$、$\text{iszero}$：

原同余规则继续向正在求值的子项走。于是 $\text{succ }\left(\text{if }\text{ true }\text{ then }\text{ false }\text{ else }0\right)$ 先归约到 $\text{succ }\text{ false}$，再归约到 $\text{wrong}$；$\text{pred }\left(\text{succ }\text{ true}\right)$ 先变成 $\text{pred }\text{ wrong}$，再向外传播成 $\text{wrong}$。$\text{wrong}$ 本身不再归约，应被识别为一种异常终点，而非原来定义的普通值。未选中的分支仍不会求值，例如 $\text{if }\text{ true }\text{ then }0\text{ else }\text{ wrong}$ 得到 $0$，不能不分位置地把整项都传播成错误。

Kotlin 可以显式写出这种异常控制流：

fun succ(x: Any): Int = when (x) {
    is Int -> x + 1
    else -> throw IllegalArgumentException("succ expects an Int")
}

fun fail(message: String): Nothing =
    throw IllegalArgumentException(message)

fun requireNat(n: Int): Int =
    if (n >= 0) n else fail("negative number")

// succ(true) 会抛出异常；requireNat(-1) 也会抛出异常。
// 这里借用 Kotlin 的 Int 演示错误处理，不把机器整数当作无界自然数。

fun succ(x: Any): Int = when (x) {
    is Int -> x + 1
    else -> throw IllegalArgumentException("succ expects an Int")
}

fun fail(message: String): Nothing =
    throw IllegalArgumentException(message)

fun requireNat(n: Int): Int =
    if (n >= 0) n else fail("negative number")

// succ(true) 会抛出异常；requireNat(-1) 也会抛出异常。
// 这里借用 Kotlin 的 Int 演示错误处理，不把机器整数当作无界自然数。

requireNat requireNat 的 else 分支为什么能放在需要 Int Int 的位置？ fail(...) fail(...) 的类型是 Nothing Nothing ，表示它不会正常返回一个值。Kotlin 的 类型系统规格把 Nothing Nothing 定义成底类型（bottom type），通常写作 $\perp$、读作 bottom。它是任何类型的子类型（subtype），即 $\perp <:𝑇$ 对任意 $𝑇$ 成立。这里 $𝑆<:𝑇$ 的意思是：$𝑆$ 类型的表达式可以放进要求 $𝑇$ 类型的上下文。因此不返回的失败分支可以和返回 Int Int 的成功分支放在同一个 if if 里。

必须区分三个对象：$\text{wrong}$ 是对象语言里的错误项， IllegalArgumentException IllegalArgumentException 是 Kotlin 的异常对象，$\perp$ 是描述表达式不会正常产出值的类型。异常对象本身不是 Nothing Nothing ； Nothing Nothing 没有正常的值，也不是 null null （ Nothing? Nothing? 是另一回事）。抛异常的表达式可以具有底类型，永远循环的表达式也可以不返回，所以不能把“错误”与 $\perp$ 当作同义词。

仅仅补上运行时错误规则，不会自动得到这样的子类型系统。若把显式异常加入 [定义] 类型与类型判断 的定型系统，也必须写明异常如何定型，并相应重述 [定理] 进展 与 [定理] 保型 ；不能直接套用未扩展语言的证明就声称“良类型程序永不抛异常”。 [推论] 类型安全 采用的则是未扩展语言：不加入错误项，让类型规则排除受阻。

JavaScript 没有把 true + 1 true + 1 留作未定义，而是明确规定转换后得到 2 2 。同样，宽松相等（loose equality） == == 规定了按两边种类进行转换的规则；严格相等（strict equality） === === 则不做这种转换，不同种类的操作数直接判为不相等。把两种比较放在一起看：

true + 1;    // 2：true 转换为 1

[] == 0;     // true
[] === 0;    // false
0 == "0";    // true
0 === "0";   // false
[] == "0";   // false
[] === "0";  // false

true + 1;    // 2：true 转换为 1

[] == 0;     // true
[] === 0;    // false
0 == "0";    // true
0 === "0";   // false
[] == "0";   // false
[] === "0";  // false

图中每条边同时列出 == == 和 === === 的结果，不是归约箭头。绿色实线表示 == == 为真，红色虚线表示 == == 为假；第二行单独记录 === === ，这里三条边都为假。

[] == 0 [] == 0 会先把空数组转换成空字符串 "" "" ，再因另一边是数字而把 "" "" 转成 0 0 ； 0 == "0" 0 == "0" 会把字符串 "0" "0" 转成数字 0 0 ，所以这两条边都为真。但 [] == "0" [] == "0" 把数组转成 "" "" 后，两边已经都是字符串，只比较 "" "" 与 "0" "0" ，结果为假。具体转换规则见 MDN 的 == == 文档。

传递性（transitivity）要求：$𝑎$ 与 $𝑏$ 相等、$𝑏$ 与 $𝑐$ 相等，就能推出 $𝑎$ 与 $𝑐$ 相等。这个三角图正好展示 == == 不满足传递性，不能像数学等号那样用于替换或推理。 === === 不会做上述转换：数组、数字、字符串种类不同，所以这三个比较都为假。它回答的是另一个问题，而不是“同一套转换做得更严格”。

但 === === 也不等于完整的数学等价关系。自反性（reflexivity）要求每个值都与自身相等，而 NaN === NaN NaN === NaN 为 false false 。对对象， === === 比较的是是否为同一个对象，不是内容是否相同： const a = []; a === a const a = []; a === a 为 true true ， [] === [] [] === [] 却为 false false ，因为后者创建了两个不同的数组。严格相等的完整规则见 MDN 的 === === 文档。

[例] JavaScript 隐式转换与相等三角图 展示了 [] == 0 [] == 0 与 0 == "0" 0 == "0" 为真、 [] == "0" [] == "0" 为假的三角关系。它让人觉得“地狱”，不是因为结果随机：每一条比较都能按规格算出来。难受之处在于，名字叫“相等”，却不能沿用相等最基本的推理。我们原本希望“$𝑎$ 等于 $𝑏$、$𝑏$ 等于 $𝑐$”能让第三次比较省下来，现在却必须重新跑一遍转换规则。定义得精确与设计得容易理解，是两件事；形式化能让问题无处藏身，却不会自动把一个糟糕的约定变成好约定。

隐式转换确实能少写一些代码，例如让输入得到的字符串 "0" "0" 直接和数字 0 0 比较。但 == == 并不是先把每个值各自转换成某个统一表示，再比较这个表示：一个值怎样参与比较，还取决于另一边是什么种类。三角图里，同一个 [] [] 遇到数字时走到 0 0 ，遇到字符串时却停在 "" "" 。这份便利的代价，是读者不能只看一个值就知道比较会怎样进行，必须同时记住另一边以及两者触发的规则。

这会变成实际的算法问题。假如自己写一个去重函数：按输入顺序扫描，只要新值与某个已保留的值满足 == == ，就把新值丢掉。输入 [[], 0, "0"] [[], 0, "0"] 时，先保留 [] [] ，丢掉与它“相等”的 0 0 ，再保留与它“不相等”的 "0" "0" ，结果留下两个值；换成 [0, [], "0"] [0, [], "0"] ，后两个值都与 0 0 “相等”，结果只留一个值。普通去重也可能因顺序不同保留不同的代表，但若依据的真是等价关系，不应连分成几类都随顺序改变。这里说的是这个自定义的 == == 算法，不是 JavaScript 的 Set Set ； Set Set 使用的是另一套比较规则。

一种更容易推理的设计，是把“验证输入”“转换表示”和“比较”分开：在需要数字的边界先检查哪些输入可接受，再显式转成数字，最后使用不做隐式转换的比较。仅仅把 == == 换成 Number(a) === Number(b) Number(a) === Number(b) 也不够， Number("") Number("") 与 Number([]) Number([]) 都是 0 0 ；如果空输入或数组本来就是错误，仍应拒绝它们，而不是转换后假装正常。相等操作也要讲清楚是在比较对象身份、结构内容，还是领域中的某个键，并且检查算法需要的自反性、对称性与传递性。不同任务可以有不同规则，但不能只靠一个“相等”的名字暗示它们全都成立。

对新语言，这意味着不要只问“这个常见例子能不能少写一次转换”，还要问“加了这条便利规则以后，原有的推理性质是否还在，和其他规则组合会怎样”。这不等于所有隐式转换都不可取；需要判断的是转换保留了什么信息，以及它是否会掩盖应当暴露的错误。对已经部署的语言，直接改掉旧规则又可能破坏依赖它的代码，因而常常需要显式提供更清楚的操作，并用工具约束旧操作的使用。少写一个转换的局部便利，可能变成整个语言长期承担的理解与兼容成本。

所以“补上约定结果”不是“随便猜一个结果”：必须完整规定转换顺序，并检查这些约定保留了哪些性质、放弃了哪些性质。这也是 [附注] 显式错误规则与 Kotlin 的底类型 中显式报错方案与隐式转换方案的真正取舍：有时拒绝一次操作，比给它一个出乎意料却合法的结果更有帮助。

使用 [定义] 一步归约 的规则，推导树的每条横线都是一条规则的实例：横线上方的子推导满足前提，下方给出结论。以下三层合起来只证明整项的一步归约，不是三步运行。