Journal of South China University of Technology (Natural Science Edition) ›› 2014, Vol. 42 ›› Issue (1): 128-134.doi: 10.3969/j.issn.1000-565X.2014.01.022

• Computer Science & Technology • Previous Articles     Next Articles

Comonadic Corecursions on Strong 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.College of Medical Information Engineering,Guangdong Pharmaceutical University,Guangzhou 510006,Guangdong,China
  • Received:2013-07-16 Revised:2013-09-29 Online:2014-01-25 Published:2013-12-01
  • Contact: 苏锦钿(1980-)，男，博士，副教授，主要从事形式化方法、形式语义、构件技术、共代数与双代数研究 E-mail:SuJD@scut.edu.cn
  • About author:苏锦钿(1980-)，男，博士，副教授，主要从事形式化方法、形式语义、构件技术、共代数与双代数研究
  • Supported by:

    国家自然科学基金资助项目(61103038);高等学校博士学科点专项科研基金资助项目(20100172120043);华南理工大学中央高校基本科研业务费专项资金资助项目(2013ZZ0055)

PDF

684

Abstract:

As the unfold on coinductive data types can not describe the corecursive functions with parameters,thefinal coalgebras on Cartesian closed category are proved to be strongly final,and a category- theoretical definition ofstrong coinductive data types as well as the corresponding corecursion with fixed parameters,which is called pun-fold,is proposed.As a result,the corecursion defined on coinductive data types may include extra parameters asthe input of calculation.Moreover,the comonadic corecursions based on comonads is used to give a unified de-scription for unfold and punfold,and various calculation laws for punfold are further analyzed.Thus,the researchesof Pardo on the recursions with parameters via Comonads are successfully extended to coinductive data types.

Key words: recursive functor, coinductive data type, final coalgebra, corecursion, comonads

CLC Number: