[定义] 类型与类型判断 定义的是一个关系：哪些 $\left(𝑡,𝑇\right)$ 有推导。它没有告诉我们怎么找推导。真正写出来的类型检查器是一个函数：

#[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 ，大多数手写测试照样能过。要把“一样”说清楚，得拆成两个方向。

可靠说算法不乱接受，完备说算法不乱拒绝。两者合起来，算法恰好判定了这个关系。

先确认一个隐含前提： type_of type_of 对每个输入都会返回，不会无限递归。它是结构递归（每次递归调用的参数都是 [定义] 直接子项与真子项 中的直接子项），由 [定义] 大小与深度 后面那段讨论，这样的函数总会终止。

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

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

两个证明各自只有几行，但方向不同、归纳的对象也不同：可靠性跟着算法走（对项归纳，因为算法按项递归），完备性跟着推导走（对推导归纳，因为前提给的是推导）。

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

这一条就是 [附注] 两个“可靠” 说的那条完整的链。完备性没有出现在这里：因为完备性保证的是检查器“不冤枉好程序”，而非“安全”。

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