程序语言中共归纳数据类型的一种fibrations方法

范畴论与共代数是程序语言中共归纳数据类型研究的传统方法,这些方法在语义行为分析与共归纳规则描述等方面存在一定的不足。针对以上问题,提出了一种fibrations方法以对共归纳数据类型的语义行为与共归纳规则进行研究。该方法系统分析了fibration上共归纳数据类型的重索引函子、对偶重索引函子与真值函子等基本逻辑结构,应用等式函子与商函子等工具建立共归纳数据类型与其语义行为在程序逻辑上的对应关系,深入分析共归纳数据类型的语义行为;并以基范畴上自函子及其在全范畴上保持等式的提升为工具构造共递归操作,抽象描述共归纳数据类型具有普适意义的共归纳规则;最后通过实例分析简要介绍了fibrations方法的应用。

Fibrations Method of Co-inductive Data Types in Programming

Traditional methods of co-inductive data types in programming,such as co-algebra and category theory,have some problems in analyzing semantics behaviors and describing co-inductive rules.Considering the status quo of co-inductive data types researches both at home and abroad,a fibrations method was proposed in this paper.Firstly, some basic logical structures of co-inductive data types are systematically analyzed over a fibration including reindexed functor,op-reindexed functor and truth functor,and the corresponding relationship between co-inductive data types and their semantic behaviors on program logic is established by equality functor and quotient functor.Then semantic behaviors of co-inductive data types are deeply analyzed .Secondly, co-recursive operations are constructed to describe abstractly co-inductive rules of co-inductive data types with universality by endo-functors in base categories and their equality-preserving lifting in total categories.At last applications of fibrations method are briefly introduced by examples.