中国科学技术大学：《程序设计语言理论》课程教学资源（PPT课件讲稿）第7章 多态性

7.2直谓式多态演算 ·良形上下文的公理和推理规则 T,x:A context (var) T,x:A x A T A:B T,x:C context (add var T,x:C A:B 这两条规则可用于多个类型系统 第二条规则可用于推导x:A,y:B x:A这样的断 言

7.2 直谓式多态演算 • 良形上下文的公理和推理规则 (var) (add var) 这两条规则可用于多个类型系统 第二条规则可用于推导x:A, y:B x:A这样的断 言 , x : A context , x : A x : A  A : B , x : C context , x : C A : B

7.2直谓式多态演算 ·U和U,类型表达式的语法规则 一V,的类型表达式由三个公理和推理规则给出 ☑ b:U1 (cst U I,x:A context (限制到U,的变量)(var) T,x:A x A TT:U,Tt:U (→U) T →：U1

7.2 直谓式多态演算 • U1和U2类型表达式的语法规则 – U1的类型表达式由三个公理和推理规则给出  b: U1 (cst U1 ) （限制到U1的变量） (var) (→ U1 )   : U1 ,   : U1   →  : U1 , x : A context , x : A x : A

7.2直谓式多态演算 第二个全域U,包含类型U和多态函数类型 t:U (U∈U2) T t:Uz T,t:U 6:U ΠU2) T Πt:Uo):U2 虽然有属于U,的类型表达式，但是没有U,的变量 如果加了变量和，抽象到U,上，它就会导致形式 是亚：Uo的类型，它将属于第三个全域U3

7.2 直谓式多态演算 – 第二个全域U2包含类型U1和多态函数类型 (U1U2 ) (U2 ) – 虽然有属于U2的类型表达式，但是没有U2的变量 – 如果加了变量和抽象到U2上，它就会导致形式 是t:U2 .的类型，它将属于第三个全域U3 , t : U1  : U2  ( t : U1 . ) : U2   : U1   : U2

7.2直谓式多态演算 例 证明Π：U.t→是属于U,的良形的类型表达式 ☑ context 由(empty context) t:U context 由(U,context) t.U t:U (var) t:U t→t:U (-→U1) t.U t→t:U2 (U1sU2〉 ☑ (ΠUt-→t):U2 U2)

7.2 直谓式多态演算 • 例 证明t: U1 .t → t是属于U2的良形的类型表达式  context 由(empty context) t: U1 context 由(U1 context) t: U1 t: U1 (var) t: U1 t → t: U1 (→U1 ) t: U1 t → t: U2 (U1U2 )  ( t: U1 .t → t) : U2 (U2 )

7.2直谓式多态演算 项的语法（先给入，Ⅱ预备项的文法)》 M:=b|xl入x:.M|MM|入t:UM|Mz 定型规则用来判断项是否为良类型的 T,x:4 context (var) T,x:A x:A T A:B T,x:C context (add var) T,x:C A:B

7.2 直谓式多态演算 • 项的语法（先给→,  预备项的文法） M ::= b | x | x:. M | MM | t: U1 .M | M • 定型规则用来判断项是否为良类型的 (var) (add var) , x : A context , x : A x : A  A : B , x : C context , x : C A : B