在 [定义] 项的集合 的项中，用以下 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 的底类型 中显式报错方案与隐式转换方案的真正取舍：有时拒绝一次操作，比给它一个出乎意料却合法的结果更有帮助。

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

从下往上读：要说明最下面那一步成立，用 E-Pred，它要求里面的 $\text{if}$ 能一步归约；这又用 E-If，它要求条件 $\text{iszero }0$ 能一步归约；最后 E-IsZeroZero 是公理，无条件成立。

[定义] 一步归约 不用自然语言的直觉解释来决定 $\text{succ}$ “是什么”，而是规定它在计算里怎样被使用。后期维特根斯坦（Wittgenstein）在《哲学研究》里提出，一个词的意义在很多情况下就是它在语言中的用法；逻辑学里的推理主义（inferentialism，根岑（Gentzen）、普拉维茨（Prawitz）、达米特（Dummett）、布兰顿（Brandom）一脉）更进一步，主张逻辑联结词的意义由它的推理规则给出。

操作语义正是这种立场的工程版本：一个构造的意义，就是关于它的规则的全体。这种立场有一个好处，它把“意义”变成了可以逐条核对的东西。