10.2有子定型的简单类型化入演算 两个项在一种类型下相等而在另一种类型下 不相等 在入→中，等式的形式写成 M=N:t, 以直接 表示这两个项的公共定型 λx:real.lLx]≠λx:real.x:real-→real -x:real.x=λx:real.x:int→real 通常，如果A<:B, 在类型A上有不同值的表达式 在类型B上却相等是可能的
10.2 有子定型的简单类型化演算 • 两个项在一种类型下相等而在另一种类型下 不相等 – 在→中，等式的形式写成 M = N:，以直接 表示这两个项的公共定型 – x: real.x x: real. x: real → real – x: real.x = x: real. x: int → real – 通常，如果A <: B，在类型A上有不同值的表达式 在类型B上却相等是可能的
10.2有子定型的简单类型化演算 子定型和等式的一般原则由下面推理规则给 出 M=N:,Σ t<:D M=N:P (subsumption eq) 该规则是一条导出规则
M = N :, <: M = N : 10.2 有子定型的简单类型化演算 • 子定型和等式的一般原则由下面推理规则给 出 该规则是一条导出规则 (subsumption eq)
10.2有子定型的简单类型化入演算 例10.3对任何入.项工 入x:G.M:g→x,并且 p<:o,可以证明等式 入x:c.M=xp.M:p-→t 证明的最后两步： xp.(x:o.Mx=入xp.M:p→T使用(B 入x:p.入：c.M0x=入x:G.M:p→t/使用(7 此例说明，在入<项上，B和归约没有合流性 可以由加一条归约规则来补救 x:o.M→x:p.M:p→t若Σ D<:O (type label)
10.2 有子定型的简单类型化演算 • 例10.3 对任何<:项 x:. M: →，并且 <:,可以证明等式 x:. M = x:. M : → 证明的最后两步： x:. (x:.M) x = x:.M: → //使用 () x:. (x:.M) x = x:.M: → //使用 ( ) 此例说明，在<:项上， 和归约没有合流性 – 可以由加一条归约规则来补救 x:.M → x:. M: → 若 <: (type label) → →