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

Category Theoretical Method of Inductive Data Types

作　　者：苗德成[1] 奚建清[2] 苏锦钿[2] 

机构地区：[1]韶关学院数学与信息科学学院,韶关512005 [2]华南理工大学计算机科学与工程学院,广州510640

出　　处：《计算机科学》2015年第6期8-11,共4页Computer Science

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

摘　　要：归纳数据类型是类型论研究的重要分支,传统的数理逻辑或代数方法侧重于描述归纳数据类型的有限语法构造,在语义性质与归纳规则的分析与设计方面存在一定的不足。基于范畴论的方法,在集合范畴的框架内给出谓词的形式化定义,分析谓词范畴与代数范畴的构成与性质,并探讨集合范畴上自函子到谓词范畴上自函子的提升,最后利用伴随函子及其伴随性质深入分析了归纳数据类型具有普适意义的归纳规则。Inductive data types are important research branch of type theory, and traditional methods including mathe- matical logic and algebra focus on describing finite syntax construction for inductive data types, resulting in some defi- ciencies for analyzing and designing semantics properties and inductive rules. This paper provided formal definition of predicate in the framework of set category by category theoretical methods, analyzed the construction and properties of predicate category and algebra category,and probed lifting of endofunctors from set category to predicate category, and at last deeply researched universal inductive rules of inductive data types by adjoint functor and its adjoint properties.

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

分 类 号：TP301.2[自动化与计算机技术—计算机系统结构]