Lemma. 规约使大小严格下降

Glomzzz
2026-10-10
About

采用大小与深度的大小函数与一步规约的十条规则．若 $𝑡 ⟶ 𝑡^{'}$ ，则 $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 ．测试实现时不能预先假定它恰好实现了规则，仍应检查每个返回后继是否更小．这条引理不说明链的终点是值还是受阻的项；那个问题由类型安全回答．

Lemma. 规约使大小严格下降

References

Backlinks