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

摘要

应用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.