⑧.2带依赖类型的演算 良形上下文的公理和推理规则 -有项、类型和种类三种语法范畴 未经检查的预备种类、预备类型和预备项的文法 语法范畴 项目 具体形式 种类 K TpelΠIx:ok 类型 = b|t|Πx:o.ooM 项 M = c x Xx:o.M MM 特点：依赖积类型和类型应用作为类型。在σM 中，σ只允许是依赖积类型，它决定了一个类型 族。种类用来区分常规类型和类型族
8.2 带依赖类型的演算 • 良形上下文的公理和推理规则 – 有项、类型和种类三种语法范畴 – 未经检查的预备种类、预备类型和预备项的文法 语法范畴 项目 具体形式 种类 ::= Type | x:.k 类型 ::= b | t | x:. | M 项 M ::= c | x | x:.M | MM – 特点：依赖积类型和类型应用作为类型。在M 中，只允许是依赖积类型，它决定了一个类型 族。种类用来区分常规类型和类型族
8.2 带依赖类型的演算 ·上下文T T:=☑|T,x:oT,t:k 项变量的类型约束、类型变量的种类约束 把Γ看成有序的，设计证明系统来证明上下文良 形与否并不困难 下面把T看成无序的集合，以简化定类规则和定 型规则的设计
8.2 带依赖类型的演算 • 上下文 ::= | , x : | , t : k – 项变量的类型约束、类型变量的种类约束 – 把看成有序的，设计证明系统来证明上下文良 形与否并不困难 – 下面把看成无序的集合，以简化定类规则和定 型规则的设计
⑧.2带依赖类型的演算 ·良形种类的两条形成规则 Type (base kind) T o:Type T,x:o (type family kind TΠx:ok
8.2 带依赖类型的演算 • 良形种类的两条形成规则 Type (base kind) (type family kind) : Type , x : k x:.k
⑧.2带依赖类型的演算 定类规则 b:K(对基调中的每个类型常量b:K) (cst这∈TTK T t:K Tσ：Tpe T,x:o:Type (vark) T Πx:O2):Tpe (Type IntroΠ O:Πx:OK)T M:O M:[Mix]K (k Elim） T K1-K 0:K2 (kind eq)
8.2 带依赖类型的演算 • 定类规则 b : (对基调中的每个类型常量b : ) (cstk ) (vark ) (Type Intro ) (k Elim) (kind eq) 1 : Type , x : 1 2 : Type ( x : 1 . 2 ) : Type t : t : 1 : (x:2 .) M : 2 1M : [M/x] : 1 1=2 : 2
8.2带依赖类型的演算 定型规则 C:σ (对基调中的每个项常量c:o x:o∈TT o:Type T x:O T 1:Type T,x:o1 M:02 ΠIntro T 入x:O1M:Πx:OO2) TM1:Πx:o.O)T M2:O1 ΠElim) MM,:[Mx]o M:1Tσ=2 (type eq) M:O2
8.2 带依赖类型的演算 • 定型规则 c : (对基调中的每个项常量c : ) (cst) (var) ( Intro) ( Elim) (type eq) x : : Type x : 1 : Type , x : 1 M :2 x: 1 .M : ( x : 1 . 2 ) M1 : (x:1 .2 ) M2 : 1 M1M2 : [M2 /x]2 M : 1 1=2 M : 2