Fibrations理论在索引归纳数据类型语法构造中的应用  

Syntax construction of indexed inductive data types based on Fibrations theory

作　　者：苗德成[1] 奚建清[2] 刘新盛 MIAO Decheng;XI Jianqing;LIU Xinsheng(School of Information Science and Engineering, Shaoguan University, Shaoguan, Guangdong 512005, China;School of Software, South China University of Technology, Guangzhou 510640, China;Department of Missiles and Shells Integration, Air Defense Forces Academy of PLA, Zhengzhou 450052, China)

机构地区：[1]韶关学院信息科学与工程学院 [2]华南理工大学软件学院 [3]解放军防空兵学院弹炮一体系

出　　处：《计算机工程与应用》2017年第4期70-74,134,共6页Computer Engineering and Applications

基　　金：广东省自然科学基金(No.S2013010015944);广东省高等学校优秀青年教师培养计划项目(No.YQ2014155);广东省战略性新兴产业核心技术攻关项目(No.2012A010701011);广东省科技计划项目(No.2014B010112007)

摘　　要：应用Fibrations理论对索引归纳数据类型的语法构造进行了研究。提出了索引fibration及其真值与内涵函子的定义,构造了索引与代数范畴,利用折叠函数与伴随函子等工具构造了索引范畴中一类相对复杂的索引归纳数据类型,辅以实例进行了简要分析,并通过相关工作的论述指出了Fibrations理论研究方法的优势。Based on Fibrations theory this paper presents a syntax construction method of indexed inductive data types.Firstly, it proposes the definitions of indexed fibration and its truth and comprehension functors, and constructs the indexed and algebra categories; secondly, it constructs a more complex indexed inductive data types in indexed category by some tools including fold function and ad joint functors; thirdly, it briefly introduces the work by example. At last, it states advantages of the application by comparing with some related works.

关 键 词：语法构造 索引归纳数据类型 Fibrations理论 范畴 提升 

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