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

Fibrations Method of Co-inductive Data Types in Programming

作　　者：苗德成[1] 奚建清[2] 戴经国[1] 苏锦钿[3] 

机构地区：[1]韶关学院信息科学与工程学院,韶关512005 [2]华南理工大学软件学院,广州510640 [3]华南理工大学计算机科学与工程学院,广州510640

出　　处：《计算机科学》2016年第3期188-192,212,共6页Computer Science

基　　金：国家自然科学基金项目(61103038);广东省自然科学基金项目(S2013010015944);广东省战略性新兴产业核心技术攻关项目(2011A010801008;2012A010701011;2012A010701003);韶关市科技计划项目(2013CX/K61)资助

摘　　要：范畴论与共代数是程序语言中共归纳数据类型研究的传统方法,这些方法在语义行为分析与共归纳规则描述等方面存在一定的不足。针对以上问题,提出了一种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.

关 键 词：语义行为 共归纳规则 fibrations方法 共归纳数据类型 提升 

分 类 号：TP301.2[自动化与计算机技术—计算机系统结构]