| 类型系统及其范畴论模型研究 |
| 周晓聪
|
| 专业 | 计算机软件与理论
|
| 2000
|
| 学位授予单位 | 中国科学院软件研究所
|
| 学位 | 博士
|
| 学位授予地点 | 中国科学院软件研究所
|
| 关键词 | 高阶子类型
受限量词类型
带序范畴
插入子 Λω×<,≤>fibration
Per模型
|
| 摘要 | 该文提出带高阶子类型的多态类型系统λω×<,≤>,它是[Cro193]的类型系统λω×的扩充,为一般算子引入了子类型关系,并结合多态性使用了受限量词类型,与已有的各种系统F的扩充相比,其特点是区分了各种上下文,使得整个类型系统在逻辑上更严谨,也可更好地研究其语义模型.该文详细研究了类型系统λω×<,≤>的各种结构性质.该文提出λω×<,≤>fibration作为高阶子类型的语义模型,其核心是引入了带序范畴及其插入子的概念,从而将λω×<,≤>fibration基范畴的射之间的关系与全范畴的对象之间关系结合在一起,给出了一般算子之间子类型关系的语义解释,解决了在[CL91]中所说的子类型关系的通用范畴论模型问题.该文的λω×<,≤>fibration结合了[Jaco95]中定义的subtypingfibration和[Phoa92b]中提出的包含射的优点,完整地给出了受限量词的范畴论语义解释,并很好地解释了一般算子之间子类型关系以及有关子类型关系的结构性质,完整地给出了已证明项的语义模型,也给出了有关已证明项的各种结构性质规则的语义解释,证明了该模型对于已证明项的等式理论的合理性. |
| 其他摘要 | Type system is a hot point of the theoretical research in computer science. It takes important application in the design of new programming language and the development of the compiler of new language. In the recent years, with the wide application of object-oriented language, many peoples have studied the type system of object-oriented language deeply. In object-oriented type system, polymorphism and subtype is the core concept. Many peoples have studied the semantic model of polymorphism and subtype. Especially those model based on category theory have been studied widely. Category theory, which is a branch of universal algebraic, have been used widely in theoretical computer science, such as formal semantics, computational model and high-order logic. The key concept of category theory, for example, discover the properties of object through studying its out-look behaviors, have the natural relation with the core concept of object-oriented technology. We believe that category theory will take the important role in the research of the foundations of object-oriented technology. In this thesis, we give a type system named Xcoxs, which is the extension of type systemλω×<,≤in [Crol93]. We introduced subtype relation for all operators and used bounded quantification type. Comparing with those extension of system F, our system distinguished three kind context, that is operator context, subtyping context and term context. Our system has the strict logic, and is easy to study its categorical model. In this thesis, we have study its structural properties in detail in chapter 5.
We provideλω×<,≤fibration as the semantic model of high-order subtyping. The key point ofλω×<,≤fibration are inserter, which give a good bridge between the subtype relation of morphism in base category and the subtype relation of object in total category. The Xcoxs fibration, which combine the ideal of subtyping fibration in [Jaco95] and inclusion map in [Phoa92b], interpret the semantic of bounded quantification completely, and can give the semantic model of subtype relation of all operator. We discuss the semantic interpretation of the structural properties of subtyping and typing rules of type sytem Xcoxs, and proved the soundness theorem of our semantic model. We think we have made a broke progress of the semantic model of high-order subtyping. |
| 页数 | 155
|
| 语种 | 中文
|
| 内容类型 | 学位论文
|
| URI标识 | http://ir.iscas.ac.cn/handle/311060/6772
|
| 专题 | 中科院软件所_中科院软件所
|
推荐引用方式
GB/T 7714 |
周晓聪. 类型系统及其范畴论模型研究[D]. 中国科学院软件研究所. 中国科学院软件研究所,2000.
|
修改评论