类型系统及其范畴论模型研究
文献类型：学位论文
| 作者 | 周晓聪 |
| 学位类别 | 博士 |
| 答辩日期 | 2000 |
| 授予单位 | 中国科学院软件研究所 |
| 授予地点 | 中国科学院软件研究所 |
| 关键词 | 高阶子类型 插入子 λω×< 受限量词类型 ≤>fibration 带序范畴 PER模型 |
| 学位专业 | 计算机软件与理论 |
| 中文摘要 | 该文提出带高阶子类型的多态类型系统λω×<,≤>,它是[Cro193]的类型系统λω×的扩充,为一般算子引入了子类型关系,并结合多态性使用了受限量词类型,与已有的各种系统F的扩充相比,其特点是区分了各种上下文,使得整个类型系统在逻辑上更严谨,也可更好地研究其语义模型.该文详细研究了类型系统λω×<,≤>的各种结构性质.该文提出λω×<,≤>fibration作为高阶子类型的语义模型,其核心是引入了带序范畴及其插入子的概念,从而将λω×<,≤>fibration基范畴的射之间的关系与全范畴的对象之间关系结合在一起,给出了一般算子之间子类型关系的语义解释,解决了在[CL91]中所说的子类型关系的通用范畴论模型问题.该文的λω×<,≤>fibration结合了[Jaco95]中定义的subtypingfibration和[Phoa92b]中提出的包含射的优点,完整地给出了受限量词的范畴论语义解释,并很好地解释了一般算子之间子类型关系以及有关子类型关系的结构性质,完整地给出了已证明项的语义模型,也给出了有关已证明项的各种结构性质规则的语义解释,证明了该模型对于已证明项的等式理论的合理性. |
| 语种 | 中文 |
| 公开日期 | 2011-03-17 |
| 页码 | 155 |
| 源URL | [http://ir.iscas.ac.cn/handle/311060/6772]  |
| 专题 | 软件研究所_中科院软件所_中科院软件所 |
| 推荐引用方式 GB/T 7714 | 周晓聪. 类型系统及其范畴论模型研究[D]. 中国科学院软件研究所. 中国科学院软件研究所. 2000. |
入库方式： OAI收割
来源：软件研究所
浏览0
下载0
收藏0
其他版本
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。