先划出“已经算完”的项．

数值就是 $0$、$\text{succ }0$、$\text{succ }\left(\text{succ }0\right)$……，分别代表 $0,1,2,\dots$． 例如 $\text{true}$、$0$、$\text{succ }\left(\text{succ }0\right)$ 都是值； $\text{succ }\text{ true}$ 虽然是项，但由于 $\text{succ}$ 后面要求数值而 $\text{true}$ 不属于数值，它算不上值； $\text{pred }0$ 也不属于值（值的定义里根本没有 $\text{pred}$，直观上它还能再算）．

规约是依据规则把词项改写为另一词项， 例如把 $\left(1+2\right)\times 3$ 改写为 $3\times 3$，再改写为 $9$． 一次改写称为一步规约，连续零次或有限多次改写称为多步规约． 规约不天然保证词项更小或更接近终点；本文的终止性要由大小严格下降另行证明．

在本模型中，$⟶$ 同时是词项之间的转移关系： $𝑡⟶{𝑡}^{\prime }$ 描述从状态 $𝑡$ 到状态 ${𝑡}^{\prime }$ 的一次转移． 程序执行就是依次作这样的转移．

数学上，$⟶$ 是二元关系： 它是由若干 $\left(𝑡,{𝑡}^{\prime }\right)$ 对组成的集合，$𝑡⟶{𝑡}^{\prime }$ 是 $\left(𝑡,{𝑡}^{\prime }\right)\in ⟶$ 的简写． 我们用推导规则定义它．一条规则形如

$$\frac{{\text{前提 }}_1\cdots {\text{ 前提}}_{𝑛}}{\text{结论}}$$

读作：如果横线上的前提全都成立，那么横线下的结论成立． 没有前提的规则称为公理；它是推导规则的特例，不需要先证明其他判断就能使用．

横线右边可以标上规则的名字，方便引用．

元变量的取值范围也是规则的一部分． 例如 nv 只能表示数值，不能用任意词项代换． 文献还常把额外限制显式写成附加条件，放在横线旁或前提中； 它们必须满足，才能应用规则，不能靠读者自行补全．

这里的“最小”和 词项的集合 里的“最小”含义相同： $𝑡⟶{𝑡}^{\prime }$ 成立，当且仅当能用这十条规则的实例搭出一棵以它为根的有限树． 这棵树称为推导树，也称推导． 推导规则是通用的规则模式， 推导则是把规则实例组合起来、证明具体判断的有限结构．

规则没有提到的情形，例如 $\text{succ }\text{ true}$ 该规约到哪里，就是没有定义． “没有定义”在这里有精确的含义： 十条规则里没有一条的结论能匹配 $\text{succ }\text{ true }⟶\dots$ （E-Succ 的结论形状对得上，但它的前提要求 $\text{true}$ 能规约，而没有规则能做到）， 所以不存在任何 ${𝑡}^{\prime }$ 使 $\text{succ }\text{ true }⟶{𝑡}^{\prime }$．

遇到没有定义的情形时，形式化将其直接视为明确的状态，常见处理方式有三种： 可以直接承认它是错误状态，把“不属于值、却又不能规约”的项单独命名（下文 正规形式与受阻 的“受阻”），再用类型系统证明良类型的程序永远到不了这种状态，本文采用这种做法； 也可以显式加上错误规则，扩充语法、增加终止计算的错误项 $\text{wrong}$，把原来受阻的运算规定为产生错误并向外传播，Python 对 1 + "a" 1 + "a" 抛出 TypeError TypeError 属于类似的运行时处理，Kotlin 的例子以及它与底类型的关系见 显式错误规则与 Kotlin 的底类型 ； 还可以补上约定的结果，例如规定布尔值先转成数，$\text{true}$ 对应 $1$、$\text{false}$ 对应 $0$，于是 $\text{succ }\text{ true }⟶\text{ succ }\left(\text{succ }0\right)$，JavaScript 的 true + 1 === 2 true + 1 === 2 就是这种做法（这只给该类运算规定了普通结果，不代表所有程序都会正常返回，隐式转换也可能掩盖本想发现的错误，见 JavaScript 隐式转换与相等三角图 ）．

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

无论选哪种，关键是写下来． C 语言标准里的未定义行为是典型的反面教材： 标准明确说某些情形没有定义，却没有要求实现报错， 于是编译器可以假设它们永远不会发生，并据此做出让程序员意外的优化．

这十条规则分成两类：一类规定基本运算怎样执行，另一类规定基本步骤可发生在哪些位置．

规约规则（也称计算规则或收缩规则）直接规定基本运算的结果： E-IfTrue、E-IfFalse、E-PredZero、E-PredSucc、E-IsZeroZero、E-IsZeroSucc． 能直接匹配这类规则的词项，称为可规约表达式，简称可规约项． 这里的六条基本规约规则没有关于 $⟶$ 的前提（其他语言的规约规则未必都如此）． 例如，取 ${𝑡}_2=\text{ succ }0$、${𝑡}_3=0$，由 E-IfTrue 可得 $\text{if }\text{ true }\text{ then }\text{ succ }0\text{ else }0⟶\text{ succ }0$； 取 nv = succ 0，由 E-PredSucc 可得 $\text{pred }\left(\text{succ }\left(\text{succ }0\right)\right)⟶\text{ succ }0$； 取 nv = 0，由 E-IsZeroSucc 可得 $\text{iszero }\left(\text{succ }0\right)⟶\text{ false}$．

结构规则（也称同余规则）把子项的规约提升到指定的求值位置： E-If 允许规约条件，E-Succ、E-Pred、E-IsZero 允许规约各自的参数．

这里的“同余”强调规约与特定构造相容，不表示一步规约是同余等价关系： $⟶$ 有方向，而且只对规则许可的位置封闭． 把许可位置另写成带一个空位的求值语境，再规定怎样在空位处执行基本规约， 就得到语境语义（也称规约语义）的写法． 参见 Hutton 译文第 6 节，以及 Harper §1.3.1．

这套小步语义中，每棵一步推导都由零次或多次结构规则与顶端的一次基本规约规则组成． 从结论向上读，结构规则定位正在求值的子项，基本规约规则执行其中的运算． 一棵推导 就是两次结构规则（E-Pred、E-If） 加一次基本规约（E-IsZeroZero）．

上图中 pred pred 和 if if 节点是结构规则经过的路径， iszero 0 iszero 0 是基本规约发生的位置； 虚线连接的分支不参与这一步．

规则的细节里藏着两项设计决定： E-If 只允许在条件里规约，没有规则允许在分支里规约， 因此总是先求条件、再选择分支，不会提前计算未选中的分支 （下文 求值策略、规约策略与合流性 会把这样的顺序规定称为求值策略，并与一般的规约策略区分）； 同时，基本规约规则要求正在检查的操作数已经是合适的值，但不要求未选中的分支是值． 例如 E-PredSucc 的左边是 pred (succ nv)， 只有 $\text{succ}$ 里面已经是数值时才能用；否则只能先用结构规则把里面算完． 这保证了“先算里面，再算外面”的顺序， 其作用见下文 E-PredSucc 的数值限制 ．