摘要
范畴论与共代数是程序语言中共归纳数据类型研究的传统方法,这些方法在语义行为分析与共归纳规则描述等方面存在一定的不足。针对以上问题,提出了一种fibrations方法以对共归纳数据类型的语义行为与共归纳规则进行研究。该方法系统分析了fibration上共归纳数据类型的重索引函子、对偶重索引函子与真值函子等基本逻辑结构,应用等式函子与商函子等工具建立共归纳数据类型与其语义行为在程序逻辑上的对应关系,深入分析共归纳数据类型的语义行为;并以基范畴上自函子及其在全范畴上保持等式的提升为工具构造共递归操作,抽象描述共归纳数据类型具有普适意义的共归纳规则;最后通过实例分析简要介绍了fibrations方法的应用。
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 coinductive 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.
出处
《计算机科学》
CSCD
北大核心
2016年第3期188-192,212,共6页
Computer Science
基金
国家自然科学基金项目(61103038)
广东省自然科学基金项目(S2013010015944)
广东省战略性新兴产业核心技术攻关项目(2011A010801008
2012A010701011
2012A010701003)
韶关市科技计划项目(2013CX/K61)资助
