Skoči na glavni sadržaj

Izvorni znanstveni članak

Inductive Data Types Based on Fibrations Theory in Programming

Decheng Miao ; School of Information Science and Engineering, Shaoguan University, Shaoguan, China
Jianqing Xi ; School of Software, South China University of Technology, Guangzhou, China
Yubin Guo ; School of Information, South China University of Agriculture, Guangzhou, China
Deyou Tang ; School of Software, South China University of Technology, Guangzhou, China

Puni tekst: engleski pdf 687 Kb

str. 1-16

preuzimanja: 377



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 dana 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.

Ključne riječi

inductive data types, Fibrations theory, semantics properties, induction rules, ad joint functor

Hrčak ID:



Posjeta: 669 *