[定理] 保型

采用 [定义] 类型与类型判断的类型关系和 [定义] 一步归约的归约关系。若 $𝑡 : 𝑇$ 且 $𝑡 ⟶ 𝑡^{'}$ ，则 $𝑡^{'} : 𝑇$ 。

证明

对 $𝑡 ⟶ 𝑡^{'}$ 的推导归纳（ [定理] 对推导归纳），对 $𝑇$ 一般化。每个情形先对 $𝑡 : 𝑇$ 使用 [引理] 反演。

E-IfTrue： $𝑡 = if true then 𝑡_{2} else 𝑡_{3}$ ， $𝑡^{'} = 𝑡_{2}$ 。反演得 $𝑡_{2} : 𝑇$ 。
E-IfFalse：对称，反演得 $𝑡_{3} : 𝑇$ 。
E-If： $𝑡^{'} = if 𝑡_{1^{'}} then 𝑡_{2} else 𝑡_{3}$ ，前提 $𝑡_{1} ⟶ 𝑡_{1^{'}}$ 。反演得 $𝑡_{1} : Bool$ ， $𝑡_{2} : 𝑇$ ， $𝑡_{3} : 𝑇$ 。对前提用归纳假设（取类型为 $Bool$ ）得 $𝑡_{1^{'}} : Bool$ ，再用 T-If。
E-Succ：反演得 $𝑇 = Nat$ ， $𝑡_{1} : Nat$ 。归纳假设给出 $𝑡_{1^{'}} : Nat$ ，用 T-Succ。
E-PredZero： $𝑡^{'} = 0$ 。反演得 $𝑇 = Nat$ ，用 T-Zero。
E-PredSucc：，。反演两次：先得 $𝑇 = Nat$ 且，再得。
E-Pred：同 E-Succ，最后用 T-Pred。
E-IsZeroZero、E-IsZeroSucc： $𝑡^{'}$ 是 $true$ 或 $false$ 。反演得 $𝑇 = Bool$ ，用 T-True 或 T-False。
E-IsZero：反演得 $𝑇 = Bool$ ， $𝑡_{1} : Nat$ 。归纳假设给出 $𝑡_{1^{'}} : Nat$ ，用 T-IsZero。

∎

References