On the internal structures of inductive types

被引:0
作者
Fu, YX [1 ]
机构
[1] Shanghai Jiao Tong Univ, Dept Comp Sci, Shanghai 200030, Peoples R China
来源
SCIENCE IN CHINA SERIES E-TECHNOLOGICAL SCIENCES | 2000年 / 43卷 / 05期
关键词
type theory; inductive type; construction;
D O I
暂无
中图分类号
T [工业技术];
学科分类号
08 ;
摘要
The paper investigates the internal structures of hereditary inductive types in logical type theory. By defining a bisimulation equality on the inhabitants of each hereditary inductive type, one is able to show that the inhabitants of a hereditary inductive type satisfy the basic properties of sets. A hereditary inductive type can therefore be conceived as a universe of sets.
引用
收藏
页码:542 / 560
页数:19
相关论文
共 29 条
  • [1] ACZEL P, 1986, TYPE THEORETIC INTER
  • [2] ACZEL P, 1977, INTRO INDUCTIVE DEFI, P739
  • [3] Aczel P., 1978, LOGIC C, V77, P55
  • [4] COQUAND T, 1990, LNCS 417, P55
  • [5] COQUAND T, 1990, MATH INVESTIGATIONS, P91
  • [6] DYBJER P, 1991, P 1 WORKSH LOG FRAM, P280
  • [7] FU YI, 1996, FUNDAMENTA INFORMATI, V26, P115
  • [8] Fu Yu-Xi, 1998, Journal of Software, V9, P236
  • [9] Structures definable in polymorphism
    Yuxi Fu
    [J]. Journal of Computer Science and Technology, 1998, 13 (6) : 579 - 587
  • [10] FU YX, 1994, P INT WORKSH ADV SOF, P153