Corollary. 检查器接受的程序不会受阻

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

Proof.

𝑡 : 𝑇

，再由类型安全即得．

∎

References