Computer Science ›› 2015, Vol. 42 ›› Issue (6): 8-11.doi: 10.11896/j.issn.1002-137X.2015.06.002

Previous Articles     Next Articles

Category Theoretical Method of Inductive Data Types

MIAO De-cheng, XI Jian-qing and SU Jin-dian   

  • Online:2018-11-14 Published:2018-11-14

Abstract: Inductive data types are important research branch of type theory,and traditional methods including mathematical logic and algebra focus on describing finite syntax construction for inductive data types,resulting in some deficiencies for analyzing and designing semantics properties and inductive rules.This paper provided formal definition of predicate in the framework of set category by category theoretical methods,analyzed the construction and properties of predicate category and algebra category,and probed lifting of endofunctors from set category to predicate category,and at last deeply researched universal inductive rules of inductive data types by adjoint functor and its adjoint properties.

Key words: Inductive data types,Category theory,Predicate category,Lift,Adjoint functor

[1] Rutten J J M M,Turi D.Initial algebra and final coalgebra semantics for concurrency[M]∥A Decade of Concurrency Reflections and Perspectives.1993:530-582
[2] Rutten J J M M.Universal coalgebra:a theory of systems[J].Theoretical Computer Science,2000,249(1):3-80
[3] 苗德成,奚建清,贾连印,等.一种形式语言代数模型[J].华南理工大学学报:自然科学版,2011,9(10):74-78 Miao D C,Xi J Q,Jia L Y,et al.A Formal Language Algebraic Model[J].Journal of South China University of Technology(Natural Science Edition),2011,39(10):74-78
[4] Bird R.Introduction to functional programming using Haskell(2nd Edition)[M].Prentice-Hall,UK,1998:15-47
[5] Bird R S,Moor O D.Algebra of Programming[M].Prentice-Hall,UK,1997:107-156
[6] Hutton G.Fold and unfold for program semantics[C]∥Proc.of the 3rd ACM SIGPLAN Int.Conf.on Functional Programming,1998.NewYork:ACM,1998:280-288
[7] 苏锦钿,余珊珊.抽象数据类型的双代数结构及其计算[J].计算机研究与发展,2012,9(8):1787-1803 Su J D,Yu S S.Bialgebraic structures for abstract data types and their computations[J].Journal of Computer Research and Development,2012,9(8):1787-1803
[8] Barr M,Wells C.Category theory for computing science[M].NewYork:Prentice-Hall,1990:14-16
[9] 屈延文.形式语义学基础与形式说明[M].北京:科学出版社,2010:120-121 Qu Y W.Foundations of formal semantics and formal descriptions[M].Beijing:Science Press,2010:120-121
[10] 陈意云.计算机科学中的范畴论[M].合肥:中国科技大学出版社,1993:36-43 Chen Y Y.Category theory for computer science[M].Hefei:University of Science and Technology of China Press,1993:36-43
[11] Hermida C,Jacobs B.Structural induction and coinduction in a fibrational setting[J].Information and Computation,1998,5(2):107-152
[12] 贺伟.范畴论[M].北京:科学出版社,2006:15-16 He W.Category theory[M].Beijing:Science Press,2006:15-16
[13] Ghani N,Johann P,Fumex C.Fibrational induction rules for initial algebras[C]∥Proceedings,Computer Science Logic.2010:336-350
[14] Bengt N,Kent P,Jan M S.Martin-Lf类型论程序设计导引[M].宋方敏,译.南京:南京大学出版社,2002:1-15 Bengt N,Kent P,Jan M S.Programming in Martin-Lf type theory:an introduction[M].Song F M ed.Nanjing:Nanjing University Press,2002:1-15
[15] Reynolds J.Polymorphism is not set theoretic[M]∥LectureNotes in Computer Science 173.Berlin:Springer-Verlag,1984:145-156
[16] Pitts A.Polymorphism is set theoretic,constructively[M]∥Lecture Notes in Computer Science 283.Berlin:Springer-Verlag,1987:12-39
[17] Hyland M.The effective topos[M]∥The L.E.J.Brouwer Centenary Symposium,1982.North-Holland,1982:165-216
[18] Longo G,Moggi E.Constructive natural deduction and its’Modest’ interpretation[M]∥Semantics of Natural and Computer Languages.Massachusatts:M.I.T.Press,1990:96-116
[19] Coquand T,Paulin-Mohring C.Inductively defined types[M]∥Lecture Notes in Computer Science 417.Berlin:Springer-Verlag,1990:50-66
[20] Dybier P.Inductive sets and families in Martin-Lof type theory and their set theoretical semantics[M].Cambridge University Press,1991:3-27
[21] Fu Y X.Recursive models of general inductive types[J].Fundamenta Informatica,1996,26:115-131
[22] 傅育熙.归纳类型的构造集语义[J].软件学报,1998,9(3):236-240 Fu Y X.Constructive semantics of inductive types[J].Journal of Software,1998,9(3):236-240
[23] Turi D,Plotkin G D.Towards a Mathematical Operational Se-mantics[C]∥Proc.of the 12th Symp.On Logic in Computer Scie-nce,1997.Los Alamitos,CA:IEEE,Computer Science Press,1997:280-291
[24] Hermida C A.Fibrations,Logical Predicates and Indeterminates[D].Edinburg:University of Edinburg,1993
[25] Ghani N,Johann P,Fumex C.Indexed Induction and Coinduction,Fibrationally[J].Logical Methods in Computer Science,2013,9(3-6):1-31
[26] Ghani N,Johann P,Fumex C.Generic Fibrational Induction[J].Logical Methods in Computer Science,2012,8(2):1-27
[27] Fumex C.Induction and Coinduction Schemes in Category Theory[D].Glasgow:University of Strathclyde,2012

No related articles found!
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!