8.2带依赖类型的演算 8.2.1依赖积类型 介绍一种最简单的依赖类型系统入F,它是奠定逻 辑框架Edinburgh LF的类型系统的一种简化版本 索引类型A上的依赖积类型x:A.B -是一族集合{B(x)|x∈A的笛卡儿积 -积的元素都是函数f,对每个a∈A有几aeIa/xB 若x在表达式B中没有自由出现 则对每个a∈A都有a)∈B -依赖积类型x:A.B退化为函数类型A→B 依赖积类型x:A.B是函数类型A→B的一种拓广8.2 带依赖类型的演算 8.2.1 依赖积类型 介绍一种最简单的依赖类型系统 LF，它是奠定逻 辑框架Edinburgh LF的类型系统的一种简化版本 •索引类型A上的依赖积类型x:A.B –是一族集合{B(x) | xA}的笛卡儿积 –积的元素都是函数f，对每个aA有f(a)[ax]B 若x在表达式B中没有自由出现 –则对每个aA都有f(a)B –依赖积类型x:A.B退化为函数类型A→B 依赖积类型x:A.B是函数类型A→B的一种拓广