抽象数据类型的双代数结构

华南理工大学学报(自然科学版) ›› 2011, Vol. 39 ›› Issue (12): 44-50.

抽象数据类型的双代数结构

苏锦钿¹珊珊²

1．华南理工大学计算机科学与工程学院，广东广州 510006; 2．中山大学信息科学与技术学院，广东广州 510275

收稿日期:2011-03-24 修回日期:2011-07-17 出版日期:2011-12-25 发布日期:2011-11-04
通信作者: 苏锦钿(1980-) ，男，博士，讲师，主要从事形式化方法、形式语义、构件技术、共代数与双代数研究． E-mail:sujd@scut.edu.cn
作者简介:苏锦钿(1980-) ，男，博士，讲师，主要从事形式化方法、形式语义、构件技术、共代数与双代数研究．
基金资助:
国家自然科学基金资助项目( 61103039) ; 高等学校博士学科点专项科研基金资助项目( 20100172120043) ; 华南理工大学中央高校基本科研业务费专项资金资助项目( 2009ZM0158)

Bialgebraic Structure of Abstract Data Types

Su Jin-dian¹Yu Shan-shan²

1. School of Computer Science and Engineering,South China University of Technology,Guangzhou 510006,Guangdong,China; 2. School of Information Science and Technology,Sun Yat-Sen University,Guangzhou 510275,Guangdong,China

Received:2011-03-24 Revised:2011-07-17 Online:2011-12-25 Published:2011-11-04
Contact: 苏锦钿(1980-) ，男，博士，讲师，主要从事形式化方法、形式语义、构件技术、共代数与双代数研究． E-mail:sujd@scut.edu.cn
About author:苏锦钿(1980-) ，男，博士，讲师，主要从事形式化方法、形式语义、构件技术、共代数与双代数研究．
Supported by:
国家自然科学基金资助项目( 61103039) ; 高等学校博士学科点专项科研基金资助项目( 20100172120043) ; 华南理工大学中央高校基本科研业务费专项资金资助项目( 2009ZM0158)

摘要/Abstract

摘要： 对抽象数据类型的语法构造和动态行为的性质及两者的关系而言，单纯利用代数或共代数方法进行研究存在一定的不足．文中结合范畴论及分配律给出抽象数据类型的双代数结构，并通过λ-双代数自然地描述了语法构造与动态行为之间的转换关系; 分别利用分配律对共代数函子及代数函子进行函子化提升，证明这种函子化提升可以将初始代数( 或终结共代数) 提升为初始( 或终结)λ -双代数，并将其应用于递归及共递归函数的定义及计算中．实例表明，这种函子化提升可以扩展代数中的归纳原理和共代数中的共归纳原理，从而提高程序语言对抽象数据类型的描述与性质证明能力．

关键词: 抽象数据类型, 共代数, 双代数, 共递归

Abstract:

As algebraic or coalgebraic methods have some disadvantages in analyzing the relationships and properties between the syntactic constructions and the dynamic behaviors of abstract data types,this paper presents a bialgebraic structure of abstract data types based on the category theory and the distributive laws,usesλ -bialgebras to naturally describe the transformation between the syntactic constructions and the dynamic behaviors,and employs distributive laws to functorially lift coalgebraic and algebraic functors,thus lifting initial algebras ( or final coalgebras) to initial ( or final)λ -bialgebra. Moreover,the functorial lifting is applied to the definition and computation of recursive and corecursive functions. Case study indicates that,as the functorial lifting extends the inductive principles of algebras and the coinductive principles of coalgebras,it helps to improve the abilities of programming languages in describing or proving the properties of abstract data types.

Key words: abstract data type, coalgebras, bialgebras, corecursion

中图分类号:

TP301.2

苏锦钿余珊珊. 抽象数据类型的双代数结构[J]. 华南理工大学学报(自然科学版), 2011, 39(12): 44-50.

Su Jin-dian Yu Shan-shan. Bialgebraic Structure of Abstract Data Types[J]. Journal of South China University of Technology(Natural Science Edition), 2011, 39(12): 44-50.

[1]	苏锦钿余珊珊. 强共归纳数据类型上的 Comonadic 共递归[J]. 华南理工大学学报（自然科学版）, 2014, 42(1): 128-134.
[2]	苏锦钿余珊珊. 范畴数据类型上的子类型[J]. 华南理工大学学报（自然科学版）, 2013, 41(9): 58-64.
[3]	苏锦钿余珊珊. 广义共迭代及其计算律[J]. 华南理工大学学报(自然科学版), 2012, 40(9): 62-68.
[4]	苏锦钿余珊珊. 共归纳数据类型上的共递归操作及其计算定律[J]. 华南理工大学学报（自然科学版）, 2011, 39(10): 90-95.