Tehnički vjesnik, Vol. 27 No. 2, 2020.
Izvorni znanstveni članak
https://doi.org/10.17559/TV-20191130092745
A Fibrational Method of Indexed Coinductive Data Types
Decheng Miao
; School of Information Science and Engineering, Shaoguan University, No. 288, Daxue Road, Zhenjiang District, Shaoguan, China
Chaoyang Wang
; School of Journalism and Communication, Guangzhou University, No. 230, Waihuanxi Road, Panyu District,Guangzhou, China
Xinsheng Liu
; Army Artillery and Air Defense Force Academy, No. 31, Dongdaying Road, Shenhe District, Shenyang, China
Yonglin Liang
; School of Information Science and Engineering, Shaoguan University, No. 288, Daxue Road, Zhenjiang District, Shaoguan, China
Sažetak
As a fundamental issue in type theory, indexed coinductive data types (ICDT, for short) is of crucial importance, which is essentially semantic computing problem in programming. Based on fibrational method, this paper analyses semantic behaviours of ICDT and describes their universal coinductive rules. We executed some works in semantic computing and program logic of ICDT including their math structures and categorical properties. Example analyses prove the effectiveness of the proposed fibrational method and its applicability in program languages. Our work is based on fibration; a general math setting that can compute semantics automatically rather than depend on particular computing environments and syntactic forms of ICDT.
Ključne riječi
category; coinductive data types; computation; fibration; programming
Hrčak ID:
236789
URI
Datum izdavanja:
15.4.2020.
Posjeta: 1.447 *