Indexed Coinduction in a Fibrational Setting
This paper provided some logical structures over fibration including comprehension and equation functor, then described semantic behavior by corecursion, also represented universal coinductive rule in a fibrational setting. Comparing the traditional methods, our works do not rely on special semantics computation context, which can analyze semantics elaborately of indexed coinductive data type and described its coinductive rule.
KeywordsSemantic behavior Coinduction rule Fibration Lift Corecursion
This study is supported by Guangdong Province High School Outstanding Young Teacher Training Project, China (Grant No. YQ2014155) and Guangdong Provincial Natural Science Foundation, China (Grant No. 2018A0303130274).
- 1.Greiner, J.: Programming with inductive and co-inductive types. School of Computer Science, Carnegie Mellon University, Pittsburgh, USA (1992)Google Scholar
- 4.Miao, D.C., Xi, J.Q., Jia, L.Y., et al.: Formal language algebraic model. J. South China Univ. Technol. (Nat. Sci. Ed.) 39(10), 74–78 (2011)Google Scholar