Computer Engineering and Applications ›› 2017, Vol. 53 ›› Issue (4): 70-74.DOI: 10.3778/j.issn.1002-8331.1605-0259

Previous Articles     Next Articles

Syntax construction of indexed inductive data types based on Fibrations theory.

MIAO Decheng1, XI Jianqing2, LIU Xinsheng3   

  1. 1.School of Information Science and Engineering, Shaoguan University, Shaoguan, Guangdong 512005, China
    2.School of Software, South China University of Technology, Guangzhou 510640, China
    3.Department of Missiles and Shells Integration, Air Defense Forces Academy of PLA, Zhengzhou 450052, China
  • Online:2017-02-15 Published:2017-05-11



  1. 1.韶关学院 信息科学与工程学院,广东 韶关 512005
    2.华南理工大学 软件学院,广州 510640
    3.解放军防空兵学院 弹炮一体系,郑州 450052

Abstract: 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.

Key words: syntax construction, indexed inductive data types, Fibrations theory, category, lifting

摘要: 应用Fibrations理论对索引归纳数据类型的语法构造进行了研究。提出了索引fibration及其真值与内涵函子的定义,构造了索引与代数范畴,利用折叠函数与伴随函子等工具构造了索引范畴中一类相对复杂的索引归纳数据类型,辅以实例进行了简要分析,并通过相关工作的论述指出了Fibrations理论研究方法的优势。

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