Journal of South China University of Technology (Natural Science Edition) ›› 2011, Vol. 39 ›› Issue (10): 90-95.doi: 10.3969/j.issn.1000-565X.2011.10.016

• Computer Science & Technology • Previous Articles     Next Articles

Corecursion Operations and Its Calculation Laws on Coinductive Data Types

Su Jin-dian1  Yu Shan-shan2   

  1. 1. School of Computer Science and Engineering,South China University of Technology,Guangzhou 510006,Guangdong,China; 2. School of Information Science and Technology,Sun Yet-Sen University,Guangzhou 510275,Guangdong,China
  • Received:2011-03-14 Revised:2011-07-06 Online:2011-10-25 Published:2011-09-01
  • Contact: 苏锦钿(1980-) ，男，博士，讲师，主要从事形式化方法及形式语义、构件技术、共代数与双代数研究 E-mail:SuJD@scut.edu.cn
  • About author:苏锦钿(1980-) ，男，博士，讲师，主要从事形式化方法及形式语义、构件技术、共代数与双代数研究
  • Supported by:

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

PDF

1026

Abstract:

As the coinductive data types in the framework of the category theory can be regarded as the carriers of final coalgebras for some coalgebraic functors,this paper presents the coalgebraic descriptions of the coinductive data types in programming languages from the viewpoint of the category theory and proposes the definitions and coalgebraic calculation laws of corecursion operations based on the finality of final coalgebras. Meanwhile,bifunctors and type functors are used to abstractly describe parametric coinductive data types,and such calculation laws on type functors as unit and fusion ones are put forward via natural transformations. It is proved that these laws can be used to simplify the calculations on coinductive data types,thus improving the dynamic behavior description ability of programming languages for various data types.

Key words: category theory, coinductive data type, corecursion, final coalgebra

CLC Number: