8.2带依赖类型的演算 良形的种类断言、定类断言和定型断言是相 互定义的，导致的结果是 在证明该系统中的性质时，需要使用同时结构归 纳或者使用全面度量的推导高度，来对不同形式 的断言进行同时证明
8.2 带依赖类型的演算 • 良形的种类断言、定类断言和定型断言是相 互定义的，导致的结果是 – 在证明该系统中的性质时，需要使用同时结构归 纳或者使用全面度量的推导高度，来对不同形式 的断言进行同时证明
8.2带依赖类型的演算 依赖类型用于表示其它类型理论和形式系统 例 描述语言：基于依赖类型系统的语言 对象语言：简单类型化入演算 对象语言的类型和各种类型的项都用描述语言的 项表示 它们分属描述语言的不同类型，以便体现对象语 言的类型系统 若不出现依赖性，则在描述语言中，工x:σ.k和 Πx:oo分别简化成o→k和o1→σ的形式
8.2 带依赖类型的演算 • 依赖类型用于表示其它类型理论和形式系统 • 例 – 描述语言：基于依赖类型系统的语言 – 对象语言：简单类型化演算 – 对象语言的类型和各种类型的项都用描述语言的 项表示 – 它们分属描述语言的不同类型，以便体现对象语 言的类型系统 – 若不出现依赖性，则在描述语言中，x:.k和 x:1 .2分别简化成→ k和1 → 2的形式
8.2带依赖类型的演算 具体描述 Ty: Type ∥Ty用于表示对象语言的类型 Tm: Ty→Type∥Tm用于表示对象语言的项 base: Ty arrow: Ty>Ty→T pp:ΠA:T.ΠB:T.Tn(arrow A B)-→TmA-→TmB la:LA:T.ΠB:T.(TnA→>TmB)-→Tm(arrow A B) A:Ty /A是对象语言的一个类型 TmA:Type ∥TmA是种类Tpe的另一个类型 x:TmA /x是对象语言中类型A的项
8.2 带依赖类型的演算 – 具体描述 Ty: Type // Ty用于表示对象语言的类型 Tm: Ty → Type // Tm用于表示对象语言的项 base: Ty arrow: Ty → Ty → Ty app: A:Ty.B:Ty.Tm(arrow A B) → Tm A → Tm B lam: A:Ty.B:Ty.(Tm A→Tm B) → Tm(arrow A B) A:Ty // A是对象语言的一个类型 TmA:Type // TmA是种类Type的另一个类型 x:TmA // x是对象语言中类型A的项
8. 2带依赖类型的演算 具体描述 Ty: Type /Ty用于表示对象语言的类型 Tm: Ty→Type∥Tm用于表示对象语言的项 base: Ty arrow: Ty>Ty→T pp:ΠA:T.ΠB:T.Tm(arrow A B)→TmA→TmB la:ΠLA:Ty.ΠB:T.(TmA→TmB)→Tm(arrow A B arrowAB:Ty∥arrowAB是对象语言的函数类型 lam AA (Ax:TmAx):Tm(arrow AA) /对象语言的恒等函数入x:Ax
8.2 带依赖类型的演算 – 具体描述 Ty: Type // Ty用于表示对象语言的类型 Tm: Ty → Type // Tm用于表示对象语言的项 base: Ty arrow: Ty → Ty → Ty app: A:Ty.B:Ty.Tm(arrow A B) → Tm A → Tm B lam: A:Ty.B:Ty.(Tm A→Tm B) → Tm(arrow A B) arrowAB :Ty // arrowAB是对象语言的函数类型 lam A A (x:Tm A.x) : Tm(arrow A A) // 对象语言的恒等函数x:A.x
8. 2带依赖类型的演算 具体描述 Ty: Type /T用于表示对象语言的类型 Tm: Ty→Tpe∥Tm用于表示对象语言的项 Int:Ty Bool:Ty arrow((arrow Int Int)Int):Ty arrow: Ty→Ty→T arrow Int Int:Ty pp:ΠA:T.ΠB:T.Tm(arrow A B)-→TmA→TmB la:ΠLA:Ty.ΠB:T.(TmA→TmB)→Tm(arrow A B) lam Int Int (Ax:Tm Intx):Tm(arrow Int Int) y:Tm Int app IntInt (lam Int Int (Ax:Tm Int.x))y:Tm Int
8.2 带依赖类型的演算 – 具体描述 Ty: Type // Ty用于表示对象语言的类型 Tm: Ty → Type // Tm用于表示对象语言的项 Int:Ty Bool:Ty arrow((arrow Int Int) Int):Ty arrow: Ty → Ty → Ty arrow Int Int:Ty app: A:Ty.B:Ty.Tm(arrow A B) → Tm A → Tm B lam: A:Ty.B:Ty.(Tm A→Tm B) → Tm(arrow A B) lam Int Int (x:Tm Int.x):Tm(arrow Int Int) y:Tm Int app Int Int (lam Int Int (x:Tm Int.x)) y :Tm Int