10.2有子定型的简单类型化入演算 O<:t 从Sb中的断言，用公理和推理规则可以证明子 定型断言σ<：x 引理对任何基调Σ，如果∑ o<:,那么o匹配x 对入的子定型的语义解释 子定型可以解释为转换或者包含 转换解释有助于澄清子定型为什么是前序而不是 偏序 前序解释：可能同时有p<:和x<:p,但p≠ 可相互转换的值集并不一定有同样表示
10.2 有子定型的简单类型化演算 • <: – 从Sub中的断言，用公理和推理规则可以证明子 定型断言 <: – 引理 对任何基调，如果 <:，那么 匹配 • 对<:的子定型的语义解释 – 子定型可以解释为转换或者包含 – 转换解释有助于澄清子定型为什么是前序而不是 偏序 – 前序解释：可能同时有 <:和 <:，但 可相互转换的值集并不一定有同样表示 →
10.2有子定型的简单类型化演算 2、项 入之项的定型规则 包括)→项的所有定型规则：(cst)、(vMr) (→Intro)、(→Elim)、(add var) 新增包容规则 TM:o,Σ (subsumption) M:t
10.2 有子定型的简单类型化演算 2、项 • <:项的定型规则 – 包括→项的所有定型规则：(cst)、(var)、 (→Intro)、(→ Elim)、(add var) – 新增包容规则 (subsumption) M : , <: M : →
10.2有子定型的简单类型化入演算 例10.1 假定基调中有int<:real、2:int、2.0:real和 div:real-→real-→real - 令M是项x:real.(diwx2.0):real-→real -确定M2的类型 -方式l:利用real→real<:int→real的事实 方式2：利用int<:real,使得2：real
10.2 有子定型的简单类型化演算 • 例10.1 – 假定基调中有int <: real、2: int、2.0: real和 div: real→real→real – 令M是项x: real.(div x 2.0): real → real – 确定M 2的类型 – 方式1: 利用real → real <: int → real的事实 – 方式2: 利用int <: real，使得2: real
10.2有子定型的简单类型化入演算 3、等式规则 入等式证明系统和入→的正好包含同样的公理 和推理规则 等价关系： (re)、(gym)和(tras) 加变量到类型指派：(add var 入抽象和应用： ()、(β和( 一同余关系： ()和() 通常，只有在TM:o和T N:σ都可推导时 才把等式r M=N:o看成是良形的
10.2 有子定型的简单类型化演算 3、等式规则 • <:等式证明系统和→的正好包含同样的公理 和推理规则 – 等价关系: (ref)、(sym)和(trans) – 加变量到类型指派: (add var) – 抽象和应用: ()、()和() – 同余关系: ()和() – 通常，只有在 M 和 N 都可推导时， 才把等式 M = N 看成是良形的 →
10.2有子定型的简单类型化入演算 有了子定型后会引起一些定型上的混淆 - 外延公理() T入x:x.(Mx)=M x在M中不是自由的 会导致相等的项有不同的类型 适当地定义M(入y:t.N且x<:t)会出现： x:石.(Mx):T→P T M:→P 其中x<: -由于x'→p<:→p是可推导的，因此 T 入x:x(Mc)=M:T→p可以使用
10.2 有子定型的简单类型化演算 • 有了子定型后会引起一些定型上的混淆 – 外延公理() x:. (Mx) = M x在M中不是自由的 会导致相等的项有不同的类型 适当地定义M（ y:.N且 <: ）会出现: x:. (Mx) : → M : → 其中 <: – 由于→ <: →是可推导的，因此 x:. (Mx) = M : →可以使用