Journal of Frontiers of Computer Science and Technology ›› 2016, Vol. 10 ›› Issue (10): 1482-1492.DOI: 10.3778/j.issn.1673-9418.1508047

Previous Articles     Next Articles

Indexed Co-inductive Data Type Based on Fibrations Theory in Programming

MIAO Decheng1+, XI Jianqing2, DAI Jingguo1   

  1. 1. School of Information Science and Engineering, Shaoguan University, Shaoguan, Guangdong 512005, China
    2. School of Software, South China University of Technology, Guangzhou 510640, China
  • Online:2016-10-01 Published:2016-09-29

程序语言中基于Fibrations理论的索引共归纳数据类型

苗德成1+,奚建清2,戴经国1   

  1. 1. 韶关学院 信息科学与工程学院,广东 韶关 512005
    2. 华南理工大学 软件学院,广州 510640

Abstract: Traditional methods including category theory and coalgebra have some drawbacks to analyze semantic    behavior and describe co-inductive rule, this paper explores indexed co-inductive data type (ICDT) in programming by Fibrations theory. Firstly, this paper constructs indexed Fibration by change of base, presents some tools such as equation functor and quotient functor of indexed Fibration, and then analyzes deeply semantic behavior of ICDT by adjunction property and lifting equation-preserving. Based on this, this paper proposes a parameterized co-recursive operation on ICDT to describe abstractly co-inductive rule with universality in the framework of Fibrations theory, also briefly introduces applications of Fibrations theory for ICDT by example. Compared with traditional methods, brief descriptions and flexible expansibility of Fibrations theory can analyze semantic behavior of ICDT accurately, its superior abstractness doesn't rely on particular computing environments to describe co-inductive rule with universality of ICDT.

Key words: semantic behavior, co-induction rule, change of base, lifting, co-recursion

摘要: 传统范畴论与共代数等方法在分析语义行为与描述共归纳规则方面存在不足,应用Fibrations理论对程序语言中索引共归纳数据类型(indexed co-inductive data type,ICDT)进行了研究。通过基变换构造索引Fibration,建立索引Fibration的等式函子与商函子等工具,应用伴随性质与保持等式的提升深入分析ICDT的语义行为;以此为基础,构造ICDT上参数化的共递归操作,在Fibrations理论框架内抽象描述具有普适意义的共归纳规则,并以实例分析简要介绍Fibrations理论在ICDT中的应用。与传统研究方法相比,Fibrations理论具有简洁的描述性与灵活的扩展性,可以精确分析ICDT的语义行为,具有高度的抽象性且不依赖特定的计算环境,描述了ICDT具有普适意义的共归纳规则。

关键词: 语义行为, 共归纳规则, 基变换, 提升, 共递归