Computer Science & Technology

Corecursion Operations and Its Calculation Laws on Coinductive Data Types

Expand
  • 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
苏锦钿(1980-) ,男,博士,讲师,主要从事形式化方法及形式语义、构件技术、共代数与双代数研究

Received date: 2011-03-14

  Revised date: 2011-07-06

  Online published: 2011-09-01

Supported by

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

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.

Cite this article

Su Jin-dian Yu Shan-shan . Corecursion Operations and Its Calculation Laws on Coinductive Data Types[J]. Journal of South China University of Technology(Natural Science), 2011 , 39(10) : 90 -95 . DOI: 10.3969/j.issn.1000-565X.2011.10.016

Outlines

/