Corollary. 类型安全

由词项的集合、一步规约与类型与类型判断规定的布尔值与自然数语言满足类型安全：若 $𝑡 : 𝑇$ 且 $𝑡 ⟶^{*} 𝑡^{'}$ ，则 $𝑡^{'}$ 没有受阻．

Proof.

对 $𝑡 ⟶^{*} 𝑡^{'}$ 的步数归纳（多步规约的两条规则）．零步时 $𝑡^{'} = 𝑡$ ，直接有 $𝑡^{'} : 𝑇$ ；至少一步时 $𝑡 ⟶ 𝑡_{1}$ 且 $𝑡_{1} ⟶^{*} 𝑡^{'}$ ，由保型得 $𝑡_{1} : 𝑇$ ，再对 $𝑡_{1}$ 用归纳假设即可．

归纳给出的其实是更强的结论： $𝑡^{'} : 𝑇$ ．最后对 $𝑡^{'}$ 用进展：它是值或还能规约，总之不受阻．

∎

References