Constructive Sets in Computable Sets  

作　　者：傅育熙 

出　　处：《Journal of Computer Science & Technology》1997年第5期425-440,共16页计算机科学技术学报（英文版）

摘　　要：The original interpretation of the constructive set theory CZF in Martin-Lof's type theory uses the 'extensional identity types'. It is generally believed that these 'types' do not belong to type theory. In this paper it will be shown that the interpretation goes through without identity types. This paper will also show that the interpretation can be given in an intensional type theory. This reflects the computational nature of the interpretation. This computational aspect is reinforced by an w-Set model of CZFThe original interpretation of the constructive set theory CZF in Martin-Lof's type theory uses the 'extensional identity types'. It is generally believed that these 'types' do not belong to type theory. In this paper it will be shown that the interpretation goes through without identity types. This paper will also show that the interpretation can be given in an intensional type theory. This reflects the computational nature of the interpretation. This computational aspect is reinforced by an w-Set model of CZF

关 键 词：Type theory constructive set theory w-set 

分 类 号：TP334.8[自动化与计算机技术—计算机系统结构]