程序语言中的共归纳数据类型及其应用  

Coinductive Data Types and their Applications in Programming Languages

作　　者：苏锦钿[1] 余珊珊[2] 

机构地区：[1]华南理工大学计算机科学与工程学院,广州510640 [2]中山大学信息科学与技术学院,广州510275

出　　处：《计算机科学》2011年第11期114-118,共5页Computer Science

基　　金：2010年高校博士点科研基金-新教师类(20100172120043);华南理工大学中央高校基本科研业务费专项资金(2009ZM0158)资助

摘　　要：归纳数据类型利用代数方法从构造的角度归纳地描述数据类型的有限语法结构,但在描述动态行为方面存在一定的不足。作为归纳数据类型的范畴对偶概念,共归纳数据类型利用共代数方法从观察的角度共归纳地描述了数据类型的动态行为。首先,从范畴论和代数的角度给出程序语言中的归纳数据类型定义,并分析了相应的递归操作;接着,利用共代数给出共归纳数据类型的范畴论定义,并根据共归纳数据类型的终结性分析了相应的共递归操作;最后,指出如何利用λ-双代数及分配律将归纳与共归纳数据类型有机地融合起来,探讨数据类型的语法构造与动态行为关系。Inductive data types mainly focus on the finite syntactic structures inductively in terms of algebras from the construction perspective,but have some disadvantages in describing dynamic behaviors.As their categorical dual notions,coinductive data types aim to coinductively describe the observable behaviors of data types in terms of coalgebras from the observation perspective.We firstly gave the definitions of inductive data types in programming languages from the categorical and algebraic viewpoints.After that,we continued to present the definition of coinductive data types with coalgebras and analyze the corresponding corecursion operations according to the finality of coinductive data types.Finally,we pointed out how to use λ-bialgebras and distributive laws to combine inductive and coinductive data types and discuss the relations between syntactic constructions and dynamic behaviors of data types.

关 键 词：归纳数据类型 共归纳数据类型 范畴论 代数 共代数 双代数 

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