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

摘要：

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

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

所属期刊栏目：10

分类号：TP301.2(计算技术、计算机技术)

资助基金：The National Natural Science Foundation of China under Grant No.61103038;the Natural Science Foundation of Guangdong Province under Grant No.S2013010015944;the High School Outstanding Young Teacher Training Plan Foundation of Guangdong Province under Grant No.YQ2014155

在线出版日期：2016-11-30（万方平台首次上网日期，不代表论文的发表时间）

页数：共11页

页码：1482-1492