. 确定性：从规则归纳到求值器

Glomzzz
2026-10-10
About

用规则归纳法证明一步规约的确定性，并证明 Rust 求值函数与规约规则一致．

$⟶$ 是对规则封闭的最小关系，因此具有规则归纳法．它与结构归纳原理的依据相同：每个可推导的 $𝑡 ⟶ 𝑡^{'}$ 都来自有限次规则应用；只要待证性质在无前提的规则上成立，并能由每条规则的前提传到结论，就对所有可推导的转移成立．

Theorem 1 规则归纳法 [induction-on-derivations]

2026-10-10
Glomzzz

设 $𝑃 (𝑡, 𝑡^{'})$ 是关于一对词项的性质．若对一步规约的每条规则实例，假定前提中的各个转移都满足 $𝑃$ 后，能够证明结论中的转移也满足 $𝑃$ ，则 $𝑃$ 对所有可推导的 $𝑡 ⟶ 𝑡^{'}$ 成立．

无前提的规则是基准情况，须直接验证其结论满足 $𝑃$ ；有前提的规则是归纳情况，可对前提的子推导使用归纳假设．这就是规则归纳法，也可理解为对有限推导树作结构归纳，其归纳对象是整条可推导的转移判断 $𝑡 ⟶ 𝑡^{'}$ ．

Proof.

令

𝑅 = {(𝑡, 𝑡^{'}) | 𝑡 ⟶ 𝑡^{'} 且 𝑃 (𝑡, 𝑡^{'})}

．假设恰好说明

𝑅

对十条规则封闭．

⟶

是对规则封闭的最小关系，所以

⟶ \subseteq 𝑅

．

∎

直观地说，规则归纳就是对推导树的结构或高度归纳，请对照一棵推导理解．公理对应没有前提的叶子，是基准情况，没有归纳假设可用； E-If 这类带前提的规则对应归纳情况，可以对前提的子推导使用归纳假设，再证明当前结论的性质．

这里需要对推导归纳（单对项作结构归纳不够用），因为已知条件是一棵 $𝑡 ⟶ 𝑡^{'}$ 的推导，要跟踪的性质同时涉及左右两项；按最后用的规则拆解，就能得到前提里的子推导以及左右两边怎样拼成结论．确定性和保型都会用到它．若只试了几条规约链，或只处理无前提的基本规约规则而漏掉 E-If 等结构规则，就不能覆盖嵌套项：例如内层规约保持类型，并不替你证明外层 $succ$ 拼回去以后也保持类型．规则归纳正是把这个“拼回去”的步骤逐条核实．

在证明确定性之前，要先确认“已经算完的值”确实不能再走一步．这既给求值器提供了可靠的停止条件，也用来排除基本规约规则和结构规则同时适用．若另加 $0 ⟶ 0$ 这样的规则， $0$ 虽仍是语法上指定的值，按“不能再走”判断停止的求值器却会永远循环；后面的确定性证明也不能再用“值不能规约”排除重叠．

Lemma 2 值不可规约 [values-do-not-reduce]

2026-10-10
Glomzzz

采用值与数值的值定义与一步规约的十条求值规则．若 $𝑣$ 是值，则不存在 $𝑡^{'}$ 使 $𝑣 ⟶ 𝑡^{'}$ ．

Proof.

对值与数值的值作结构归纳．常量

true

、

false

、

0

作为基准情况：逐条检查十条规则的结论左边，没有一条是这三个常量之一．对于

succ nv

：结论左边形如

succ \dots

的规则只有 E-Succ，它的前提要求

nv ⟶ t'_(1)

；而

nv

是更小的值，由归纳假设不可能规约．

∎

接下来证明一步规约的确定性，为后面的求值函数铺路：我们准备实现的 step step 每次只返回单个后继项；它要完整实现一步规约关系，就必须证明关系不会给同一输入两个不同后继，否则 match match 的分支顺序可能偷偷选掉另一条合法路线． E-PredSucc 的数值限制会给出放宽一条规则就失去这一保证的具体反例；多路线不必然是语言设计错误，但必须说明是否用策略限制它（求值策略、规约策略与合流性）．

Theorem 3 确定性 [determinism]

2026-10-10
Glomzzz

对一步规约定义的关系 $⟶$ ，若 $𝑡 ⟶ 𝑡^{'}$ 且 $𝑡 ⟶ 𝑡^{″}$ ，则 $𝑡^{'} = 𝑡^{″}$ ．

Proof.

证明采用分类讨论（也称分情形讨论）：穷尽所有可能情形并逐一论证．由于 $⟶$ 是最小关系，任何推导的最后一步只能出自那十条规则，因此只需按这十条规则分类即可穷尽所有情况，无需枚举无穷多个词项．下面覆盖这十种情形，对称或重复的论证合并说明；每个情形里，再按结论左边的形状排除不匹配的规则，检查第二个推导剩下的候选规则．

具体地，对 $𝑡 ⟶ 𝑡^{'}$ 作规则归纳（规则归纳法），要证的性质是“对任意 $𝑡^{″}$ ， $𝑡 ⟶ 𝑡^{″}$ 蕴涵 $𝑡^{'} = 𝑡^{″}$ ”． “任意 $𝑡^{″}$ ”必须写进性质里，否则归纳假设只能用于某个固定的 $𝑡^{″}$ ，在 E-If 情形就不够用．每个情形里，再看 $𝑡 ⟶ 𝑡^{″}$ 的推导最后一步可能是哪条规则：它的结论左边必须和 $𝑡$ 形状相同．

对 E-IfTrue， $𝑡 = if true then 𝑡_{2} else 𝑡_{3}$ ， $𝑡^{'} = 𝑡_{2}$ ．第二个推导若是 E-IfTrue，则 $𝑡^{″} = 𝑡_{2}$ ；条件为 $true$ ，排除了要求条件为 $false$ 的 E-IfFalse；值不可规约又排除了要求 $true ⟶ \dots$ 的 E-If． E-IfFalse 与上一条对称．对 E-If，前提为 $𝑡_{1} ⟶ 𝑡_{1}^{'}$ ；由于 $𝑡_{1}$ 能规约，由值不可规约知它不可能等于 $true$ 或 $false$ ，从而排除 E-IfTrue 与 E-IfFalse，第二个推导只能是 E-If（前提 $𝑡_{1} ⟶ 𝑡_{1}^{″}$ ），由归纳假设得 $𝑡_{1}^{'} = 𝑡_{1}^{″}$ ，于是 $𝑡^{'} = 𝑡^{″}$ ．

对 E-Succ，左边形如 $succ \dots$ 的规则只有 E-Succ，由归纳假设即得．对 E-PredZero， $𝑡 = pred 0$ ；E-PredSucc 要求 $pred$ 后面是 $succ \dots$ ，不适用；E-Pred 要求 $0$ 能规约，与值不可规约矛盾，所以只能是 E-PredZero， $𝑡^{″} = 0 = 𝑡^{'}$ ．对 E-PredSucc， $t = pred (succ nv)$ ；E-PredZero 不适用，E-Pred 要求值 $succ nv$ 能规约而矛盾，所以只能是 E-PredSucc，结果相同．对 E-Pred，前提为 $𝑡_{1} ⟶ 𝑡_{1}^{'}$ ；由值不可规约知 $𝑡_{1}$ 不属于值，而 E-PredZero 与 E-PredSucc 分别要求 $𝑡_{1}$ 为值 $0$ 或 $succ nv$ ，故都不适用，剩下 E-Pred，用归纳假设． E-IsZeroZero、E-IsZeroSucc、E-IsZero 与 $pred$ 的三条一一对应，论证相同．

∎

这个证明没什么巧思，功夫全花在排除情形上．这正是形式化的用处，下面的附注给出具体例子．

Note 4 E-PredSucc 的数值限制 [numeric-value-restriction-in-predecessor-reduction]

2026-10-10
Glomzzz

打开独立页面 →

5 从关系到函数

确定性表明：对每个词项 $𝑡$ ，至多有一个一步后继 $𝑡^{'}$ ．因此 $⟶$ 对应偏函数：有后继时返回唯一后继，没有后继时无定义．用 Rust 实现时，可以把返回类型写成 Option<Term> Option<Term> ，以 None None 显式表示没有后继．这样能把数学上的偏函数扩充为词项到可选结果的全函数，前提是它对每个输入都终止；仅有这个返回类型并不保证终止．下面的 step step 及 is_nv is_nv 都沿直接子项递归，克隆也只处理有限子树，所以在算术语言形式化的未展开前提的资源与基础操作假设下会正常返回．若一步关系有多个后继，函数仍然可以选择其中一个，但必须写明选择的策略；否则它只实现了关系的一部分，却误说成实现了整个关系．

Note 5.1 求值策略、规约策略与合流性 [evaluation-strategies-reduction-strategies-and-confluence]

2026-10-10
Glomzzz

打开独立页面 →

先把前面的 Term Term 定义重新贴在这里，方便对照：

#[derive(Clone, Debug, PartialEq, Eq, Hash)]
pub enum Term {
    True, False,
    If(Box<Term>, Box<Term>, Box<Term>),  // if t1 then t2 else t3
    Zero,
    Succ(Box<Term>), Pred(Box<Term>), IsZero(Box<Term>),
}

#[derive(Clone, Debug, PartialEq, Eq, Hash)]
pub enum Term {
    True, False,
    If(Box<Term>, Box<Term>, Box<Term>),  // if t1 then t2 else t3
    Zero,
    Succ(Box<Term>), Pred(Box<Term>), IsZero(Box<Term>),
}

Term Term 没有派生 Copy Copy ． Copy Copy 的意思是“按位复制一份就是合法的副本”，而 Box Box 独占堆上的子树；按位复制会得到两个指向同一块内存、都以为自己负责释放它的指针，所以 Rust 不允许含 Box Box 的类型实现 Copy Copy ．下面代码里的 (**a).clone() (**a).clone() 、 a.clone() a.clone() 是在显式地深拷贝子树： a a 的类型是 &Box<Term> &Box<Term> ， *a *a 是 Box<Term> Box<Term> ， **a **a 是 Term Term ．

/// nv ::= 0 | succ nv
pub fn is_nv(t: &Term) -> bool {
    match t { Term::Zero => true, Term::Succ(t) => is_nv(t), _ => false }
}

/// v ::= true | false | nv
pub fn is_value(t: &Term) -> bool {
    matches!(t, Term::True | Term::False) || is_nv(t)
}

/// t ⟶ t'．返回 None 表示不存在 t'：t 是值，或者受阻了．
pub fn step(t: &Term) -> Option<Term> {
    use Term::*;
    match t {
        If(c, a, b) => match &**c {
            True => Some((**a).clone()),                          // E-IfTrue
            False => Some((**b).clone()),                         // E-IfFalse
            c => Some(If(Box::new(step(c)?), a.clone(), b.clone())), // E-If
        },
        Succ(t1) => Some(Succ(Box::new(step(t1)?))),              // E-Succ
        Pred(t1) => match &**t1 {
            Zero => Some(Zero),                                   // E-PredZero
            Succ(n) if is_nv(n) => Some((**n).clone()),           // E-PredSucc
            t1 => Some(Pred(Box::new(step(t1)?))),                // E-Pred
        },
        IsZero(t1) => match &**t1 {
            Zero => Some(True),                                 // E-IsZeroZero
            Succ(n) if is_nv(n) => Some(False),                 // E-IsZeroSucc
            t1 => Some(IsZero(Box::new(step(t1)?))),            // E-IsZero
        },
        True | False | Zero => None,                              // 值不可规约
    }
}

/// nv ::= 0 | succ nv
pub fn is_nv(t: &Term) -> bool {
    match t { Term::Zero => true, Term::Succ(t) => is_nv(t), _ => false }
}

/// v ::= true | false | nv
pub fn is_value(t: &Term) -> bool {
    matches!(t, Term::True | Term::False) || is_nv(t)
}

/// t ⟶ t'．返回 None 表示不存在 t'：t 是值，或者受阻了．
pub fn step(t: &Term) -> Option<Term> {
    use Term::*;
    match t {
        If(c, a, b) => match &**c {
            True => Some((**a).clone()),                          // E-IfTrue
            False => Some((**b).clone()),                         // E-IfFalse
            c => Some(If(Box::new(step(c)?), a.clone(), b.clone())), // E-If
        },
        Succ(t1) => Some(Succ(Box::new(step(t1)?))),              // E-Succ
        Pred(t1) => match &**t1 {
            Zero => Some(Zero),                                   // E-PredZero
            Succ(n) if is_nv(n) => Some((**n).clone()),           // E-PredSucc
            t1 => Some(Pred(Box::new(step(t1)?))),                // E-Pred
        },
        IsZero(t1) => match &**t1 {
            Zero => Some(True),                                 // E-IsZeroZero
            Succ(n) if is_nv(n) => Some(False),                 // E-IsZeroSucc
            t1 => Some(IsZero(Box::new(step(t1)?))),            // E-IsZero
        },
        True | False | Zero => None,                              // 值不可规约
    }
}

每个分支旁边标了它实现的规则．结构规则对应的分支都用到了 ? ? ，它的作用见下面的附注．

Note 5.2 Rust 的 ? ? 运算符 [rust-question-mark-operator]

2026-10-10
Glomzzz

打开独立页面 →

确定性说明关系至多有一个后继，但还没有说明 step step 返回的就是这个后继．下面的定理把两者接上：函数返回的每个后继都能由规则推出，规则允许的每个后继函数也都能返回．

Theorem 5.3 求值器与一步规约一致 [evaluator-faithfulness]

2026-10-10
Glomzzz

取 Rust 求值器 step step ，规约关系采用一步规约，实现论证采用算术语言形式化的未展开前提的资源与基础操作假设．对任意项 $𝑡$ 与 $𝑢$ ： step(t) = Some(u) step(t) = Some(u) 当且仅当 $𝑡 ⟶ 𝑢$ ．

两个方向各有分工． “仅当”方向（ step step 蕴涵规则）说明函数返回的每个后继都能由规则推出，函数不会凭空造出规则不允许的一步． “若”方向（规则蕴涵 step step ）说明规则允许的每个后继函数都能返回，函数没有漏掉任何合法路线．

“若”方向要用值不可规约排除“别的分支抢先匹配”的情形，这与确定性证明里的排除论证同源．反过来看也成立： step step 是函数，所以只要这条定理成立，若 $𝑡 ⟶ 𝑢$ 且 $𝑡 ⟶ 𝑢^{'}$ ，则 step(t) step(t) 同时等于 Some(u) Some(u) 与 Some(u') Some(u') ，于是 $𝑢 = 𝑢^{'}$ ．因此对这十条规则，这条定理蕴涵确定性，给出了确定性的另一条证明路线．若把 E-PredSucc 放宽成任意项，“若”方向会在这一情形失败，见 E-PredSucc 的数值限制．

Proof.

（仅当： step(t) = Some(u) step(t) = Some(u) 蕴涵 $𝑡 ⟶ 𝑢$ ） 对 $𝑡$ 结构归纳，按 step step 实际走到的分支分情形．常量 $true$ 、 $false$ 、 $0$ 上 step step 返回 None None ，前提不成立．当 $𝑡 = if 𝑡_{1} then 𝑡_{2} else 𝑡_{3}$ 时，若 $𝑡_{1}$ 是 $true$ 则返回 $𝑡_{2}$ （对应 E-IfTrue），若是 $false$ 则返回 $𝑡_{3}$ （对应 E-IfFalse）；否则 step(t1) = Some(t1') step(t1) = Some(t1') 且 $𝑢 = if 𝑡_{1}^{'} then 𝑡_{2} else 𝑡_{3}$ ，由归纳假设得 $𝑡_{1} ⟶ 𝑡_{1}^{'}$ ，再用 E-If 即得．当 $𝑡 = succ 𝑡_{1}$ 时， step(t1) = Some(t1') step(t1) = Some(t1') 且 $𝑢 = succ 𝑡_{1}^{'}$ ，由归纳假设与 E-Succ 即得．当 $𝑡 = pred 𝑡_{1}$ 时，若 $𝑡_{1}$ 是 $0$ 则返回 $0$ （E-PredZero），若 $t_(1) = succ nv$ （ is_nv is_nv 为真）则返回 $nv$ （E-PredSucc），其余情形 step(t1) = Some(t1') step(t1) = Some(t1') ，由归纳假设与 E-Pred 即得． $iszero 𝑡_{1}$ 与 $pred$ 的三个分支一一对应，分别用 E-IsZeroZero、E-IsZeroSucc、E-IsZero．

（若： $𝑡 ⟶ 𝑢$ 蕴涵 step(t) = Some(u) step(t) = Some(u) ） 对 $𝑡 ⟶ 𝑢$ 作规则归纳（规则归纳法），按最后一步的规则分情形．对 E-IfTrue、E-IfFalse，条件分别是 $true$ 、 $false$ ， step step 的前两个分支直接返回 $𝑡_{2}$ 、 $𝑡_{3}$ ．对 E-If，前提为 $𝑡_{1} ⟶ 𝑡_{1}^{'}$ ；由值不可规约知 $𝑡_{1}$ 不属于值，不可能匹配 $true$ 或 $false$ ，所以 step step 走第三个分支，再由归纳假设得 step(t1) = Some(t1') step(t1) = Some(t1') ，返回 $if 𝑡_{1}^{'} then 𝑡_{2} else 𝑡_{3}$ ．对 E-Succ，由归纳假设直接得到．对 E-PredZero、E-PredSucc， step step 的前两个分支返回规则的结论，其中 E-PredSucc 的条件 is_nv is_nv 正是规则对 $nv$ 的限制．对 E-Pred，前提为 $𝑡_{1} ⟶ 𝑡_{1}^{'}$ ；由值不可规约知 $𝑡_{1}$ 不属于值，不可能匹配 $0$ 或数值 $succ nv$ ， step step 走第三个分支，由归纳假设得 step(t1) = Some(t1') step(t1) = Some(t1') ． E-IsZeroZero、E-IsZeroSucc、E-IsZero 与 $pred$ 的三条一一对应，论证相同．

∎

这条定理接上的是“规则”与“Rust 函数”之间那道缝，与算法可靠性和算法完备性对类型检查器做的事相呼应．它是对这段 Rust 代码的纸面论证，未经机器检查；对代码里没有写出的细节（例如 clone clone 的行为）仍然依赖对 Rust 语义的默认理解．配套工程 code/plt-arith code/plt-arith 里的 determinism determinism 测试把 step step 与逐条照抄规则的枚举器在有限样本上对照，作为对定理的经验检验．

Note 5.4 分支顺序里藏着证明 [proofs-behind-pattern-matching-order]

2026-10-10
Glomzzz

打开独立页面 →

. 确定性：从规则归纳到求值器

References

Backlinks