关键词: 语义行为, 共归纳规则, 基变换, 提升, 共递归

Abstract: Traditional methods including category theory and coalgebra have some drawbacks to analyze semantic    behavior and describe co-inductive rule, this paper explores indexed co-inductive data type (ICDT) in programming by Fibrations theory. Firstly, this paper constructs indexed Fibration by change of base, presents some tools such as equation functor and quotient functor of indexed Fibration, and then analyzes deeply semantic behavior of ICDT by adjunction property and lifting equation-preserving. Based on this, this paper proposes a parameterized co-recursive operation on ICDT to describe abstractly co-inductive rule with universality in the framework of Fibrations theory, also briefly introduces applications of Fibrations theory for ICDT by example. Compared with traditional methods, brief descriptions and flexible expansibility of Fibrations theory can analyze semantic behavior of ICDT accurately, its superior abstractness doesn't rely on particular computing environments to describe co-inductive rule with universality of ICDT.

Key words: semantic behavior, co-induction rule, change of base, lifting, co-recursion