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

来源：计算机科学与探索杂志2016年第10期北京时间：

作者：苗德成，奚建清，戴经国

单位：1. 韶关学院 信息科学与工程学院，广东 韶关 5120052. 华南理工大学 软件学院，广州 510640

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

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