归纳数据类型的范畴论方法

摘要：

归纳数据类型是类型论研究的重要分支,传统的数理逻辑或代数方法侧重于描述归纳数据类型的有限语法构造,在语义性质与归纳规则的分析与设计方面存在一定的不足.基于范畴论的方法,在集合范畴的框架内给出谓词的形式化定义,分析谓词范畴与代数范畴的构成与性质,并探讨集合范畴上自函子到谓词范畴上自函子的提升,最后利用伴随函子及其伴随性质深入分析了归纳数据类型具有普适意义的归纳规则.

关键词：归纳数据类型、范畴论、谓词范畴、提升、伴随函子

所属期刊栏目：42

分类号：TP301.2(计算技术、计算机技术)

资助基金：国家自然科学基金项目61103038;广东省自然科学基金项目S2013010015944,2012A010701011;韶关市科技计划项目2013CX/K61

在线出版日期：2015-07-06（万方平台首次上网日期，不代表论文的发表时间）

页数：共4页

页码：8-11