Inductive Data Types Based on Fibrations Theory in Programming.
Saved in:
| Title: | Inductive Data Types Based on Fibrations Theory in Programming. |
|---|---|
| Authors: | Decheng Miao1 miaodecheng@sgu.edu.cn, Jianqing Xi2 jianqingxi@163.com, Yubin Guo3 lxm_lsy@126.com, Deyou Tang2 tangdy@163.com |
| Source: | Journal of Computing & Information Technology. 2016, Vol. 24 Issue 1, p1-16. 16p. |
| Subjects: | Data types (Computer science), Computer programming, Mathematical category theory, Semantics, Data analysis |
| Abstract: | Traditional methods including algebra and category theory have some deficiencies in analyzing semantics properties and describing inductive rules of inductive data types, we present a method based on Fibrations theory aiming at those questions above. We systematically analyze some basic logical structures of inductive data types about a fibration such as re-indexing functor, truth functor and comprehension functor, make semantics models of non-indexed fibration, single-sorted indexed fibration and many-sorted indexed fibration respectively. On this basis, we thoroughly discuss semantics properties of fibred, single-sorted indexed and many-sorted indexed inductive data types, and abstractly describe their inductive rules with universality. Furthermore, we briefly introduce applications of the three inductive data types for analyzing semantics properties and describing inductive rules based on Fibrations theory via some examples. Compared with traditional methods, our works have the following three advantages. Firstly, brief descriptions and flexible expansibility of Fibrations theory can analyze semantics properties of inductive data types accurately, whose semantics are computed automatically. Secondly, superior abstractness of Fibrations theory does not rely on particular computing environments to depict inductive rules of inductive data types with universality. Thirdly, its rigorousness and consistence provide sound basis for testing and maintenance of software development. [ABSTRACT FROM AUTHOR] |
| Copyright of Journal of Computing & Information Technology is the property of CIT. Journal of Computing & Information Technology and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.) | |
| Database: | Engineering Source |
| FullText | Links: – Type: pdflink Text: Availability: 0 |
|---|---|
| Header | DbId: egs DbLabel: Engineering Source An: 114682355 AccessLevel: 6 PubType: Academic Journal PubTypeId: academicJournal PreciseRelevancyScore: 0 |
| IllustrationInfo | |
| Items | – Name: Title Label: Title Group: Ti Data: Inductive Data Types Based on Fibrations Theory in Programming. – Name: Author Label: Authors Group: Au Data: <searchLink fieldCode="AR" term="%22Decheng+Miao%22">Decheng Miao</searchLink><relatesTo>1</relatesTo><i> miaodecheng@sgu.edu.cn</i><br /><searchLink fieldCode="AR" term="%22Jianqing+Xi%22">Jianqing Xi</searchLink><relatesTo>2</relatesTo><i> jianqingxi@163.com</i><br /><searchLink fieldCode="AR" term="%22Yubin+Guo%22">Yubin Guo</searchLink><relatesTo>3</relatesTo><i> lxm_lsy@126.com</i><br /><searchLink fieldCode="AR" term="%22Deyou+Tang%22">Deyou Tang</searchLink><relatesTo>2</relatesTo><i> tangdy@163.com</i> – Name: TitleSource Label: Source Group: Src Data: <searchLink fieldCode="JN" term="%22Journal+of+Computing+%26+Information+Technology%22">Journal of Computing & Information Technology</searchLink>. 2016, Vol. 24 Issue 1, p1-16. 16p. – Name: Subject Label: Subjects Group: Su Data: <searchLink fieldCode="DE" term="%22Data+types+%28Computer+science%29%22">Data types (Computer science)</searchLink><br /><searchLink fieldCode="DE" term="%22Computer+programming%22">Computer programming</searchLink><br /><searchLink fieldCode="DE" term="%22Mathematical+category+theory%22">Mathematical category theory</searchLink><br /><searchLink fieldCode="DE" term="%22Semantics%22">Semantics</searchLink><br /><searchLink fieldCode="DE" term="%22Data+analysis%22">Data analysis</searchLink> – Name: Abstract Label: Abstract Group: Ab Data: Traditional methods including algebra and category theory have some deficiencies in analyzing semantics properties and describing inductive rules of inductive data types, we present a method based on Fibrations theory aiming at those questions above. We systematically analyze some basic logical structures of inductive data types about a fibration such as re-indexing functor, truth functor and comprehension functor, make semantics models of non-indexed fibration, single-sorted indexed fibration and many-sorted indexed fibration respectively. On this basis, we thoroughly discuss semantics properties of fibred, single-sorted indexed and many-sorted indexed inductive data types, and abstractly describe their inductive rules with universality. Furthermore, we briefly introduce applications of the three inductive data types for analyzing semantics properties and describing inductive rules based on Fibrations theory via some examples. Compared with traditional methods, our works have the following three advantages. Firstly, brief descriptions and flexible expansibility of Fibrations theory can analyze semantics properties of inductive data types accurately, whose semantics are computed automatically. Secondly, superior abstractness of Fibrations theory does not rely on particular computing environments to depict inductive rules of inductive data types with universality. Thirdly, its rigorousness and consistence provide sound basis for testing and maintenance of software development. [ABSTRACT FROM AUTHOR] – Name: AbstractSuppliedCopyright Label: Group: Ab Data: <i>Copyright of Journal of Computing & Information Technology is the property of CIT. Journal of Computing & Information Technology and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract.</i> (Copyright applies to all Abstracts.) |
| PLink | https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=egs&AN=114682355 |
| RecordInfo | BibRecord: BibEntity: Identifiers: – Type: doi Value: 10.20532/cit.2016.1002716 Languages: – Code: eng Text: English PhysicalDescription: Pagination: PageCount: 16 StartPage: 1 Subjects: – SubjectFull: Data types (Computer science) Type: general – SubjectFull: Computer programming Type: general – SubjectFull: Mathematical category theory Type: general – SubjectFull: Semantics Type: general – SubjectFull: Data analysis Type: general Titles: – TitleFull: Inductive Data Types Based on Fibrations Theory in Programming. Type: main BibRelationships: HasContributorRelationships: – PersonEntity: Name: NameFull: Decheng Miao – PersonEntity: Name: NameFull: Jianqing Xi – PersonEntity: Name: NameFull: Yubin Guo – PersonEntity: Name: NameFull: Deyou Tang IsPartOfRelationships: – BibEntity: Dates: – D: 01 M: 03 Text: 2016 Type: published Y: 2016 Identifiers: – Type: issn-print Value: 13301136 Numbering: – Type: volume Value: 24 – Type: issue Value: 1 Titles: – TitleFull: Journal of Computing & Information Technology Type: main |
| ResultId | 1 |
