. 正规形式、受阻与多步规约

Glomzzz
2026-10-10
About

区分作为合法终点的值与作为运行时错误的受阻项，并定义多步规约关系．

Definition 1 正规形式与受阻 [normal-forms-and-stuck-terms]

2026-10-10
Glomzzz

采用一步规约的关系 $⟶$ ．若不存在词项 $𝑡^{'}$ 使 $𝑡 ⟶ 𝑡^{'}$ ，称 $𝑡$ 是正规形式．按值与数值判断，不属于值的正规形式称为受阻词项．正规形式与受阻都相对于给定的转移规则定义； “正规形式”只表示不能继续规约，不代表正常结果，也不保证每个词项都能到达唯一正规形式．

正规形式是相对于给定规约关系没有后继的词项，好比 $(1 + 2) \times 3$ 化简到 $9$ 后不能再算．这里的定义只看能否继续规约，不保证结果合法、存在或唯一，也与 BNF 中的 Form 无关．在本文的关系下，正规形式分成值与受阻的项两类．值表示已经算完且合法的结果；由值不可规约，值都是正规形式，例如 $true$ 、 $succ 0$ ．受阻的项则是不能再规约的非值，计算停在了规则无法继续处理的地方：比如 $succ true$ ，唯一候选规则 E-Succ 要求 $true$ 能规约而无法满足，同时 $true$ 又不属于数值，整项不算值；又如 $if 0 then true else false$ ，E-IfTrue、E-IfFalse 要求条件是 $true$ 或 $false$ ，E-If 要求 $0$ 能规约，三条都用不上；再如 $iszero false$ ，E-IsZeroZero、E-IsZeroSucc 要求参数是数值，E-IsZero 要求 $false$ 能规约，同样无一成立．

Note 2 “受阻”的译名 [translation-of-stuck]

2026-10-10
Glomzzz

打开独立页面 →

本文用受阻建模一类运行时错误：例如词项要求把布尔值加一，但没有转移规则处理这一操作．受阻只刻画这类“非值且无后继”的状态，显式抛异常与无限循环仍须另外区分．下一节的类型系统会在不按求值规则运行程序的前提下拒绝一些项；我们要证明，类型系统接受的项不会走到受阻状态．检查器拒绝某项可以报为编译期错误，但遭拒绝不意味着实际求值一定受阻．这套规则的保守性见类型系统是保守的．

3 多步规约

一步规约只描述“一次改写”．程序真正运行时要连续改写很多次，所以需要把若干步串起来．

Definition 3.1 多步规约 [multi-step-reduction]

2026-10-10
Glomzzz

以一步规约的关系 $⟶$ 为基础， $𝑡 ⟶^{*} 𝑡^{'}$ 读作“ $𝑡$ 多步规约到 $𝑡^{'}$ ”，表示从 $𝑡$ 出发经过零步或有限多步一步规约到达 $𝑡^{'}$ ．精确地说，它是对下面两条规则封闭的最小关系：

M-Refl：前提无；结论 t ⟶^(∗) t M-Step：前提 t ⟶ t'；t' ⟶^(∗) t''；结论 t ⟶^(∗) t''

M-Refl 给出零步规约，即自反性；M-Step 把一步接到有限多步之前．由于取的是最小关系， $𝑡 ⟶^{*} 𝑡^{'}$ 成立当且仅当存在一条有限链 $𝑡 = 𝑡_{0} ⟶ 𝑡_{1} ⟶ \dots ⟶ 𝑡_{𝑛} = 𝑡^{'}$ （ $𝑛 \geq 0$ ）．上角的星号表示重复零次或多次，与 Kleene 星号的惯例一致； $⟶^{*}$ 称为 $⟶$ 的自反传递闭包．

Example 3.2 多步规约到值 [multi-step-reduction-to-a-value]

2026-10-10
Glomzzz

采用一步规约的十条规则， $⟶^{*}$ 表示多步规约的零步或有限多步规约；终点是否为值按值与数值判断．

$\begin{matrix} if (iszero (pred (succ 0))) then succ 0 else 0 \\ ⟶ & if (iszero 0) then succ 0 else 0 & E-If + E-IsZero + E-PredSucc \\ ⟶ & if true then succ 0 else 0 & E-If + E-IsZeroZero \\ ⟶ & succ 0 & E-IfTrue \end{matrix}$

每行右边列出了这一步推导用到的规则，从外层的结构规则写到最里层的基本规约规则．三步之后到达值 $succ 0$ ，所以

$if (iszero (pred (succ 0))) then succ 0 else 0 ⟶^{*} succ 0$

由确定性，每一步都别无选择，所以这条链是唯一的． $⟶^{*}$ 也包括中间每一站：这个项也多步规约到第二行、第三行的项，以及它自己（零步）．

Example 3.3 规约到受阻 [reduction-to-a-stuck-term]

2026-10-10
Glomzzz

按一步规约的规则，取 $𝑡 = succ (if true then false else 0)$ ．是否为值采用值与数值，是否受阻采用正规形式与受阻．

第一步， $𝑡$ 的最外层是 $succ$ ．结论左边形如 $succ \dots$ 的规则只有 E-Succ，它要求里面的 $if true then false else 0$ 能规约．这个 $if$ 的条件是 $true$ ，E-IfTrue 适用，得到 $false$ ．于是推导是：

E-Succ：前提 [E-IfTrue：前提 [无]；结论 if true then false else 0 ⟶ false]；结论 succ (if true then false else 0) ⟶ succ false

第二步，现在的项是 $succ false$ ．仍然只有 E-Succ 可能适用，它要求 $false ⟶ 𝑡_{1}^{'}$ 对某个 $𝑡_{1}^{'}$ 成立．但 $false$ 是值，由值不可规约不能规约，于是 E-Succ 的前提搭不上，没有任何规则可用： $succ false$ 是正规形式．由于 $succ$ 后面必须是数值， $succ false$ 不属于值，因此受阻了．

第一步完全合法，问题出在第二步：词项当前能规约，并不保证后续步步都能正常推进．

对这门小语言，规约链不会无限延续下去．

Lemma 3.4 规约使大小严格下降 [reduction-decreases-size]

2026-10-10
Glomzzz

采用大小与深度的大小函数与一步规约的十条规则．若 $𝑡 ⟶ 𝑡^{'}$ ，则 $size (𝑡^{'}) < size (𝑡)$ ．因此，从 $𝑡$ 出发的任何规约链至多有 $size (𝑡) - 1$ 步，不存在无限规约链．

Proof.

对 $𝑡 ⟶ 𝑡^{'}$ 作规则归纳（规则归纳法），按最后一步的规则分情形．对 E-IfTrue 与 E-IfFalse，整项的大小是 $1 + size (𝑡_{1}) + size (𝑡_{2}) + size (𝑡_{3})$ ，结果只留下选中的一个分支，严格更小．对 E-PredZero 与 E-IsZeroZero， $size (pred 0) = size (iszero 0) = 2$ ，结果 $0$ 或 $true$ 的大小为 $1$ ．对 E-PredSucc， $size(pred (succ nv)) = size(nv) + 2$ ，结果是 $nv$ ．对 E-IsZeroSucc， $size(iszero (succ nv)) = size(nv) + 2 \geq 3$ ，结果 $false$ 的大小为 $1$ ．对 E-Succ、E-Pred、E-IsZero，前提为 $𝑡_{1} ⟶ 𝑡_{1}^{'}$ ，由归纳假设得 $size (𝑡_{1}^{'}) < size (𝑡_{1})$ ；两边都只多包一层同一个一元节点，严格不等式仍成立．对 E-If，前提为 $𝑡_{1} ⟶ 𝑡_{1}^{'}$ ，由归纳假设条件部分变小，另两个分支与根节点不变，整项严格变小．

对步数：设 $𝑡 = 𝑡_{0} ⟶ 𝑡_{1} ⟶ \dots ⟶ 𝑡_{𝑛}$ ．每一步大小至少减 $1$ ，所以 $size (𝑡_{𝑛}) \leq size (𝑡) - 𝑛$ ．大小至少为 $1$ ，故 $𝑛 \leq size (𝑡) - 1$ ．

∎

这条引理说明规约链有限．结合求值器与一步规约一致，在算术语言形式化的未展开前提的资源与基础操作假设下，反复调用 Rust 求值器 step step 会在有限次返回后得到 None None ．测试实现时不能预先假定它恰好实现了规则，仍应检查每个返回后继是否更小．这条引理不说明链的终点是值还是受阻的项；那个问题由类型安全回答．

多步规约仍属于小步语义：它把执行步骤串起来，右端 $𝑡^{'}$ 可以是任意中间状态，不必是值． 大步操作语义（也称自然语义）则通常直接定义词项与最终值之间的求值关系，常记为 $𝑡 ⇓ 𝑣$ ．不能只因 $⟶^{*}$ 描述了多次改写，就把它当作大步语义；两种定义是否给出相同的求值结果，需要针对具体规则证明．

同样，实现成函数也不直接等同于指称语义．指称语义通过值化函数把词项映射到语义域，并要求复合词项的意义由子项的意义组合而成，即满足组合性．操作语义同样可以实现成函数；两者的分野在于所定义的是执行关系，还是词项在语义域中的意义．

4 练习：求值

Exercises (5)

Exercise 3.1. 值、正规形式与受阻别混在一起

对下面五个项分别判断是否为值、是否为正规形式、是否受阻；能够规约的，还要给出下一项和规则名：

succ (succ 0)

、

pred (succ 0)

、

succ true

、

if true then 0 else (succ true)

、

if 0 then 0 else 0

．

Hint

先用值与数值判断值，再问是否存在一步规约； “正规形式”与“受阻”按正规形式与受阻判断．

Solution

$succ (succ 0)$ 是数值，同时也是值和正规形式，不受阻． $pred (succ 0)$ 不属于值，且 E-PredSucc 给出后继 $0$ ，因此也不属于正规形式，当前不受阻． $succ true$ 不属于值，唯一候选 E-Succ 的前提无法成立，属于受阻的正规形式． $if true then 0 else (succ true)$ 不属于值，但 E-IfTrue 直接给出 $0$ （未选中的坏分支不参与求值），因此不属于正规形式，也不受阻． $if 0 then 0 else 0$ 不属于值，条件既非布尔值又不能规约，属于受阻的正规形式．

可见“非值”未必“受阻”，“含有坏的子项”也未必“当前受阻”．

Exercise 3.2. 一条链与第一步的推导树

写出

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

到正规形式的完整规约链，标明每一步用到的规则，并画出第一步的推导树．使用一步规约，不要把两次计算并成一步．

Hint

第一步经由三条同余规则进入条件中的

pred 0

，尚不能直接消去最外层

pred

．

Solution

$\begin{matrix} pred (if (iszero (pred 0)) then succ (succ 0) else 0) \\ ⟶ & pred (if (iszero 0) then succ (succ 0) else 0) \\ ⟶ & pred (if true then succ (succ 0) else 0) \\ ⟶ & pred (succ (succ 0)) \\ ⟶ & succ 0 \end{matrix}$

四步所用的规则依次是 E-Pred + E-If + E-IsZero + E-PredZero， E-Pred + E-If + E-IsZeroZero，E-Pred + E-IfTrue，E-PredSucc．第一步的完整推导是：

E-Pred：前提 [E-If：前提 [E-IsZero：前提 [E-PredZero：前提 [无]；结论 pred 0 ⟶ 0]；结论 iszero (pred 0) ⟶ iszero 0]；结论 if (iszero (pred 0)) then succ (succ 0) else 0 ⟶ if (iszero 0) then succ (succ 0) else 0]；结论 pred (if (iszero (pred 0)) then succ (succ 0) else 0) ⟶ pred (if (iszero 0) then succ (succ 0) else 0)

最后 $succ 0$ 是值，没有后继．注意多步规约关系除了连接起点与最终值，也包含起点自身以及链上的每个中间项．

Exercise 3.3. 扩展：函数选一条路，不等于关系只有一条路

只把 E-PredSucc 的

nv

放宽为任意项，其余规则不变．为

pred (succ (iszero 0))

找出两个不同的一步后继，并分别继续规约．说明这个例子证明了什么、没有证明什么，并判断在 step step 用 match match 只返回其中一个后继时，能否据此声称扩展关系仍确定．

Hint

使用 E-PredSucc 的数值限制的放宽规则时，可以消去外层，也可以先在

iszero 0

里计算．

Solution

把 E-PredSucc 改成允许任意 $𝑡$ 的 $pred (succ 𝑡) ⟶ 𝑡$ 后，取 $𝑠 = pred (succ (iszero 0))$ ．直接消去外层得到 $𝑠 ⟶ iszero 0$ ；先用同余规则进入内部，得到 $𝑠 ⟶ pred (succ true)$ ．

两个后继不同，所以一步关系不确定．第一条路线再用 E-IsZeroZero 到 $true$ ，第二条路线再用放宽的 E-PredSucc 到 $true$ ；因此这个分叉可以汇合．但一个可汇合的例子不证明整套扩展关系合流．

Rust 函数即使按分支优先级选出唯一返回值，也没有消除关系的另一条合法路线．要么实现“所有后继”的接口，要么明确说这个单后继函数实现的是选定策略限制后的关系．注意扩展规则下 $pred (succ true)$ 能规约，不能照搬它在原语言中受阻的判断．

Exercise 3.4. 换一个相等三角形

对 "" "" 、 0 0 、 "0" "0" 两两计算 == == 与 === === 的结果，画出另一个相等三角形．再按“新值与任何已保留值满足 == == 就丢弃”的算法，分别去重 ["", 0, "0"] ["", 0, "0"] 与 [0, "", "0"] [0, "", "0"] ，并解释两者的保留数量为何不同．

Hint

比较空字符串 "" "" 、数字 0 0 和字符串 "0" "0" ．同类字符串的 == == 不会再把两边都转成数字．

Solution

"" == 0 "" == 0 和 0 == "0" 0 == "0" 为 true true ， "" == "0" "" == "0" 为 false false ；三组 === === 都为 false false ．前两次把字符串转为数字，第三次只比较两个不同的字符串．

使用相等关系的“地狱”给语言设计什么教训的自定义 == == 去重算法，输入 ["", 0, "0"] ["", 0, "0"] 留下 ["", "0"] ["", "0"] ，输入 [0, "", "0"] [0, "", "0"] 只留下 [0] [0] ．规则明确仍可能失去算法所依赖的传递性；改用 === === 后这三种输入彼此不同，在这个例子中不会合并，但仍要留意对象身份和 NaN NaN 的特殊处理．

Exercise 3.5. 扩展：错误只沿实际求值的位置传播

比较原语言与显式错误扩展对

if true then 0 else (succ true)

和

pred (succ false)

的处理，写出每一步，并区分

wrong

、Kotlin 的异常对象与底类型

⊥

．

Hint

使用显式错误规则与 Kotlin 的底类型的错误扩展；不要把未选中的分支当作正在求值的操作数．

Solution

对 $if true then 0 else (succ true)$ ，原语言与错误扩展都用 E-IfTrue 直接得到 $0$ ，不计算 $else$ 分支．

原语言中的 $pred (succ false)$ 没有后继，是受阻的正规形式．错误扩展先在内部用 E-OpBool，并由 E-Pred 提升到整项，得到 $pred wrong$ ；再用 E-OpWrong 到 $wrong$ （这是专设的异常终点，与普通数值分开）．

$wrong$ 是错误项， IllegalArgumentException IllegalArgumentException 是异常对象， $⊥$ 是底类型． Kotlin 的抛异常表达式可以具有 Nothing Nothing 类型，不意味着异常对象是底类型的值，也不意味着未选中的异常分支必须先执行．

. 正规形式、受阻与多步规约

References

Backlinks