[定理] 算法完备性

取 Rust 类型检查算法 type_of type_of ，类型关系采用 [定义] 类型与类型判断。Rust 的 Bool Bool 、 Nat Nat 分别对应 $Bool$ 、 $Nat$ 。对任意项 $𝑡$ 和类型 $𝑇$ ：若 $𝑡 : 𝑇$ ，则 type_of(t) = Some(T) type_of(t) = Some(T) 。

证明

对 $𝑡 : 𝑇$ 的推导归纳，按最后一步的规则分情形。

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) 。

∎

References