Fibrations理论在索引归纳数据类型不确定语义中的应用

Applications of Fibrations Theory to Uncertainty Semantic Computation for Indexed Inductive Data Types

应用Fibrations理论对索引归纳数据类型的不确定语义计算进行了研究。论证了索引范畴的构造,提出了索引Fibration及其真值函子与内涵函子,建立了索引范畴上自函子的一种保持真值的提升,提出了部分F-代数的定义,并应用折叠函数等工具抽象描述了索引归纳数据类型不确定语义计算,辅以实例进行了简要分析,最后通过相关工作的论述指出了Fibrations理论研究方法的优势。

This paper discussed the uncertainty semantic computation of indexed inductive data types using Fibrations theory.Firstly,we demonstrated the construction of indexed category,presented the concept of indexed Fibration and its truth and comprehension functors.And then,we proposed a truth-preserving lifting on endo-functor in indexed category.We also presented the definition of partial F-algebra,abstractly described the uncertainty semantic computation of indexed inductive data types using some tools including fold function,and briefly introduced the application by example.At last,we stated the advantages of Fibrations theory by comprising with some related works.