. 规则与算法：可靠性与完备性

Glomzzz
2026-10-10
About

将语法导向的类型规则实现为 Rust 类型推理函数，并证明它相对类型规则可靠且完备．

1 从规则到程序

类型与类型判断用逻辑规则定义类型关系：哪些 $(𝑡, 𝑇)$ 可以推出类型判断．它并没有直接给出搜索推导的程序，更没有仅凭符号形式就保证类型检查可判定．同一个关系，还可以按给定的是词项还是类型，提出不同的问题：

Note 1.1 类型检查、类型推理与类型居留性 [type-what-so-many]

2026-10-12
Glomzzz

可以把判断看作算法规范，分析其中的信息流：这里 $𝑡$ 是输入， $𝑇$ 是待求的输出．对本文的语法导向规则，每种词项构造都对应一个递归分支，因此可以写出 Rust 函数 type_of type_of ．它接收词项、返回类型，严格说是类型推理接口；我们也沿用“类型检查器”这个广义称呼．若调用者同时给出期望类型 $𝑇$ ，再判断 $𝑡 : 𝑇$ 是否成立，那才是狭义的类型检查．

#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub enum Type { Bool, Nat }

/// 类型推理接口：返回 Some(T) 表示“t 的类型是 T”，None 表示拒绝．
pub fn type_of(t: &Term) -> Option<Type> {
    use Term::*;
    match t {
        True | False => Some(Type::Bool),                  // T-True / T-False
        Zero => Some(Type::Nat),                           // T-Zero
        Succ(t1) | Pred(t1) => {                           // T-Succ / T-Pred
            (type_of(t1)? == Type::Nat).then_some(Type::Nat)
        }
        IsZero(t1) => {                                    // T-IsZero
            (type_of(t1)? == Type::Nat).then_some(Type::Bool)
        }
        If(c, a, b) => {                                   // T-If
            let ta = type_of(a)?;
            (type_of(c)? == Type::Bool && type_of(b)? == ta).then_some(ta)
        }
    }
}

#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub enum Type { Bool, Nat }

/// 类型推理接口：返回 Some(T) 表示“t 的类型是 T”，None 表示拒绝．
pub fn type_of(t: &Term) -> Option<Type> {
    use Term::*;
    match t {
        True | False => Some(Type::Bool),                  // T-True / T-False
        Zero => Some(Type::Nat),                           // T-Zero
        Succ(t1) | Pred(t1) => {                           // T-Succ / T-Pred
            (type_of(t1)? == Type::Nat).then_some(Type::Nat)
        }
        IsZero(t1) => {                                    // T-IsZero
            (type_of(t1)? == Type::Nat).then_some(Type::Bool)
        }
        If(c, a, b) => {                                   // T-If
            let ta = type_of(a)?;
            (type_of(c)? == Type::Bool && type_of(b)? == ta).then_some(ta)
        }
    }
}

x.then_some(y) x.then_some(y) 的意思是“条件 x x 成立就返回 Some(y) Some(y) ，否则返回 None None ”．

这个函数和规则之间隔着一道缝．写代码的人会觉得“显然一样”，可这正是不完整的规格之后一直在提防的词．比如有人把 If If 分支写成只检查 a a 、不检查 b b ，大多数手写测试照样能过．要把“一样”说清楚，得拆成两个方向．

Definition 1.2 可靠与完备 [soundness-and-completeness]

2026-10-10
Glomzzz

以类型与类型判断的关系 $𝑡 : 𝑇$ 为规格，以 Rust 类型检查算法 type_of type_of 为实现．在算术语言形式化的未展开前提的实现假设下，正常返回 Some(T) Some(T) 表示算法报告类型 $𝑇$ ， None None 表示拒绝； Rust 的 Bool Bool 、 Nat Nat 分别对应对象语言的 $Bool$ 、 $Nat$ ．

若 type_of(t) = Some(T) type_of(t) = Some(T) 蕴涵 $𝑡 : 𝑇$ ，则称算法相对规则可靠；若 $𝑡 : 𝑇$ 蕴涵 type_of(t) = Some(T) type_of(t) = Some(T) ，则称算法相对规则完备．

算法可靠性保证报告的类型判断都能由规则推出， 完备性保证规则认可的类型判断不会遗漏．两者针对的是算法与类型规则的对应；再加上对所有输入的终止性，算法才恰好判定这个关系．下节先检查这项终止性前提．

Note 1.3 类型健全性与算法可靠性 [type-soundness-and-algorithm-soundness]

2026-10-10
Glomzzz

打开独立页面 →

2 证明

先确认一条隐含前提：把 type_of type_of 看作有限项上的数学算法时，它会终止．每次递归调用的参数都是直接子项与真子项中的直接子项，所以由大小与深度后面关于结构递归的讨论，不会出现无限递归．对实际 Rust 实现，这个论证采用算术语言形式化的未展开前提的资源与基础操作假设；它没有保证任意深的输入都不耗尽机器的栈或内存．

首先证明可靠性，因为类型安全定理的前提是“规则能推出类型的项”，某个函数返回 Some Some 并不能自动代替这一前提．若检查器在 If If 分支里忽略 $else$ 分支，就可能接受 $succ (if false then 0 else true)$ ；程序下一步变成受阻的 $succ true$ ．类型规则本身没有错，错在算法冒称规则已接受它．下面的定理防止这种“假阳性”．

Theorem 2.1 算法可靠性 [type-checking-algorithm-soundness]

2026-10-10
Glomzzz

取 Rust 类型检查算法 type_of type_of ，类型关系采用类型与类型判断．实现论证采用算术语言形式化的未展开前提的资源与基础操作假设； Rust 的 Bool Bool 、 Nat Nat 分别对应 $Bool$ 、 $Nat$ ．对任意项 $𝑡$ 和类型 $𝑇$ ：若 type_of(t) = Some(T) type_of(t) = Some(T) ，则 $𝑡 : 𝑇$ ．

Proof.

对 $𝑡$ 结构归纳（归纳证明的写法）． type_of type_of 本身按项的形状分支，所以每个情形对应一个分支．

若 $𝑡$ 是常量， True True 、 False False 分支返回 Bool Bool ， Zero Zero 分支返回 Nat Nat ，分别是 T-True、T-False、T-Zero 的结论．若 $𝑡 = succ 𝑡_{1}$ ，返回 Some(Nat) Some(Nat) 意味着 type_of(t1) = Some(Nat) type_of(t1) = Some(Nat) ，由归纳假设得 $𝑡_{1} : Nat$ ，再用 T-Succ 即得 $succ 𝑡_{1} : Nat$ ； $pred$ 、 $iszero$ 同理，分别用 T-Pred、T-IsZero．若 $𝑡 = if 𝑡_{1} then 𝑡_{2} else 𝑡_{3}$ ，返回 Some(ta) Some(ta) 说明 type_of(c) = Some(Bool) type_of(c) = Some(Bool) 、 type_of(a) = Some(ta) type_of(a) = Some(ta) 、 type_of(b) = Some(ta) type_of(b) = Some(ta) ；三次使用归纳假设分别给出 $𝑡_{1} : Bool$ 、 $𝑡_{2} : 𝑇$ 、 $𝑡_{3} : 𝑇$ （ $𝑇$ 即 ta ta ），恰好满足 T-If 的三个前提．

∎

可靠性还不够保证“算法与规则一致”：对所有输入都返回 None None 的检查器也是可靠的，却连 $0$ 都不接受．完备性排除这种“假阴性”，保证实现不会漏掉规则认可的程序．例如把 T-Pred 对应的代码分支误写成直接返回 None None ，不会放进坏程序，却会拒绝 $pred 0$ 这样的合法程序；下面这条定理能发现它．

Theorem 2.2 算法完备性 [type-checking-algorithm-completeness]

2026-10-10
Glomzzz

取 Rust 类型检查算法 type_of type_of ，类型关系采用类型与类型判断．实现论证采用算术语言形式化的未展开前提的资源与基础操作假设； Rust 的 Bool Bool 、 Nat Nat 分别对应 $Bool$ 、 $Nat$ ．对任意项 $𝑡$ 和类型 $𝑇$ ：若 $𝑡 : 𝑇$ ，则 type_of(t) = Some(T) type_of(t) = Some(T) ．

Proof.

对

𝑡 : 𝑇

作规则归纳，按最后一步的规则分情形．对公理 T-True、T-False、T-Zero，直接计算 type_of type_of 即得．对 T-Succ，前提

𝑡_{1} : Nat

由归纳假设给出 type_of(t1) = Some(Nat) type_of(t1) = Some(Nat) ，于是 Succ Succ 分支返回 Some(Nat) Some(Nat) ；T-Pred、T-IsZero 同理．对 T-If，三个前提由归纳假设给出 type_of type_of 在三个子项上分别返回 Bool Bool 、 T T 、 T T ；代入 If If 分支后 ta = T ta = T ，两个比较都成立，返回 Some(T) Some(T) ．

∎

两个证明的方向不同，归纳对象也不同：可靠性跟着算法走，对输入词项作结构归纳；完备性跟着类型推导走，对规则作归纳．前者利用递归调用的结构，后者利用判断可推导时最后应用的规则．

最后要把两个不同的保证接起来：算法符合类型规则，类型规则又与运行规则协调．少了第一段，错误检查器可能乱接受；少了第二段，类型系统可能认可运行时受阻的项．这个端到端结论才是使用者真正需要的“检查通过以后能相信什么”，也说明只证明某个局部函数正确不足以替整条链作保证．

Corollary 2.3 检查器接受的程序不会受阻 [accepted-programs-do-not-get-stuck]

2026-10-10
Glomzzz

取 Rust 类型检查算法 type_of type_of ，以及多步规约的关系 $⟶^{*}$ ．若 type_of(t) = Some(T) type_of(t) = Some(T) 且 $𝑡 ⟶^{*} 𝑡^{'}$ ，则 $𝑡^{'}$ 不会处于正规形式与受阻定义的受阻状态．

Proof.

由算法可靠性得

𝑡 : 𝑇

，再由类型安全即得．

∎

这一条就是类型健全性与算法可靠性说的完整链条．完备性没有出现在这里，因为完备性负责的是检查器“不漏掉好程序”，与“运行安全”分工不同．

3 转化顺利的条件

这一节的证明顺利，靠的是反演依赖的那个性质：规则是语法导向的，而且每条规则前提里出现的类型，都能从子项算出来． T-If 里的 $𝑇$ 由 $𝑡_{2}$ 算出，然后拿来比较 $𝑡_{3}$ ，没有哪一步需要凭空猜一个类型．

Note 3.1 从规则到算法的条件 [turning-rules-into-algorithms]

2026-10-10
Glomzzz

打开独立页面 →

更大的系统也可能显式划分信息流． 双向类型检查把通常的类型判断分成检查判断 $Γ ⊢ 𝑡 \Leftarrow 𝑇$ 与推导判断 $Γ ⊢ 𝑡 \Rightarrow 𝑇$ ：检查时 $𝑇$ 是输入，推导时 $𝑇$ 是输出； $Γ$ 是共同的输入语境（这里的箭头标记类型信息的流向，注意与词项的执行步骤区分）．本文的 type_of type_of 与练习中的 check check 展示了两种接口，但尚未定义一套双向类型规则，不能只因同时有这两个函数就称它为双向类型系统．

Remark 3.2 语法与语义，证明与真 [syntax-semantics-proof-and-truth]

2026-10-10
Glomzzz

打开独立页面 →

4 练习：规则与算法

Exercises (4)

Exercise 6.1. 可靠与完备守的是不同方向

三个终止的检查器分别这样实现： A 总返回 None None ；B 总返回 Some(Nat) Some(Nat) ； C 只接受

true

、

false

、

0

并返回正确类型，其余返回 None None ．判断每个检查器相对原类型规则是否可靠、完备；凡不成立的方向，都给出反例．

Hint

按照可靠与完备对具体的返回类型作判断，不要把“返回了某个类型”混同于“返回了规则给出的类型”．

Solution

对所有输入返回 None None 的 A 是可靠的：可靠性的前提从不成立；但它不完备，因为 $0 : Nat$ 遭到拒绝．

对所有输入返回 Some(Nat) Some(Nat) 的 B 既不可靠也不完备．它为 $true$ 报告 $Nat$ ，规则只能给出 $Bool$ ，所以不可靠； $true : Bool$ 成立却没有返回 Some(Bool) Some(Bool) ，所以也不完备．它还会接受根本没有类型的 $succ true$ ．

C 只接受三个常量并返回它们正确的类型，其余返回 None None ．它可靠，但不完备： $pred 0 : Nat$ 就是漏掉的合法项．可靠性允许少接受，完备性不允许漏掉规则认可的判断．

Exercise 6.2. 漏掉条件种类的检查

若 type_of type_of 的 If If 分支写成下面这样，其余分支不变，找出一个错误接受的项，指出漏了 T-If 的哪个前提，修复代码，并判断这个修改是否也破坏完备性．

If(c, a, b) => {
    let ta = type_of(a)?;
    type_of(c)?;
    (type_of(b)? == ta).then_some(ta)
}

If(c, a, b) => {
    let ta = type_of(a)?;
    type_of(c)?;
    (type_of(b)? == ta).then_some(ta)
}

Hint

让两个分支都是

0

，却把条件也写成

0

；再区分放进坏项与漏掉好项．

Solution

错误检查器会给 $if 0 then 0 else 0$ 返回 Some(Nat) Some(Nat) ：两个分支相同，条件也能得到某个类型，所以三个调用都成功．但 T-If 要求条件为 $Bool$ ， $0$ 只能为 $Nat$ ，因此这个项没有类型，算法可靠性失效；运行时它也受阻．

修复是恢复条件种类的比较：

If(c, a, b) => {
    let ta = type_of(a)?;
    (type_of(c)? == Type::Bool && type_of(b)? == ta).then_some(ta)
}

If(c, a, b) => {
    let ta = type_of(a)?;
    (type_of(c)? == Type::Bool && type_of(b)? == ta).then_some(ta)
}

这处遗漏本身不会破坏完备性：对原规则认可的项，条件确实为 Bool Bool ，修改前后的检查都会通过；对子项的类型推导使用规则归纳，仍得到正确的输出类型．但“好项仍能通过”不抵消“坏项也得以通过”．

Exercise 6.3. 检查顺序与求值顺序

本文 type_of type_of 在 If If 分支先检查 a a （即

then

分支）．判断能否改成先检查条件 c c ，同时保持接受的项与输出类型不变；给出代码并论证，再说明这样的改动是否会让对象语言先运行

then

分支．

Hint

本文的 type_of type_of 没有副作用，总会终止，失败只返回 None None ；注意区分检查器的调用顺序与对象语言的求值顺序．

Solution

可以在保持全部条件检查的前提下，先检查条件，再检查两个分支．例如：

If(c, a, b) => {
    if type_of(c)? != Type::Bool { return None; }
    let ta = type_of(a)?;
    (type_of(b)? == ta).then_some(ta)
}

If(c, a, b) => {
    if type_of(c)? != Type::Bool { return None; }
    let ta = type_of(a)?;
    (type_of(b)? == ta).then_some(ta)
}

原版与此版恰好都要求：条件为 Bool Bool 、两个分支都有类型且相等．每次调用都终止且没有副作用，所以最终 Some(T) Some(T) 或 None None 相同．条件不合适时，此版只是更早返回 None None ．

这不会改变 step step 的顺序：检查器在元语言中分析整个项，求值器则按对象语言的规约规则运行．若检查器改成返回详细错误，检查顺序可能改变首先报告哪个错误，但那属于诊断接口的附加行为，不影响本文 Option<Type> Option<Type> 的结果．

Exercise 6.4. 实现一个带期望类型的检查接口

按类型检查、类型推理与类型居留性的区分，把推理接口 type_of type_of 包装成检查接口 check(t, expected) -> bool check(t, expected) -> bool ，使它当且仅当原规则能推出

𝑡 : 𝑇

时返回真，其中 expected expected 对应

𝑇

．证明两个方向及终止性，给出成功、期望类型不符和项本身不良类型三个例子．

Hint

不必新增类型规则；比较 type_of type_of 的结果与 Some(expected) Some(expected) ，然后分别使用算法可靠与完备．

Solution

pub fn check(t: &Term, expected: Type) -> bool {
    type_of(t) == Some(expected)
}

pub fn check(t: &Term, expected: Type) -> bool {
    type_of(t) == Some(expected)
}

若 check(t, T) check(t, T) 为真， type_of(t) type_of(t) 等于 Some(T) Some(T) ，由算法可靠性得 $𝑡 : 𝑇$ ．若 $𝑡 : 𝑇$ ，由算法完备性得 type_of(t) = Some(T) type_of(t) = Some(T) ，比较为真．两方向合起来就是 check(t, T) = true check(t, T) = true 当且仅当 $𝑡 : 𝑇$ ．∎

type_of type_of 结构递归并终止，最后一次类型比较也终止，所以 check check 终止． check(true, Bool) check(true, Bool) 为真， check(true, Nat) check(true, Nat) 为假， check(pred 0, Nat) check(pred 0, Nat) 为真；没有类型的 $succ true$ 对两个期望类型都返回假．这只是原算法的接口包装，没有增加一种对象语言的判断或求值策略．

. 规则与算法：可靠性与完备性

References

Backlinks