| Constructive Sets in Computable Sets |
| |
| 作者姓名： | Mi Thxi |
| |
| 作者单位： | DepartmentofComputerScience,ShanghaiJiaotongUniversity,Shanghai200030 |
| |
| 摘 要： | The original interpretation of the constructive set theory CZF in Martin-Loef‘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 ω-Set moel of CZF.
|
| 关 键 词： | 打印机 打印理论 可算集 构造集 |
Constructive sets in computable sets |
| |
| Mi Thxi.Constructive Sets in Computable Sets[J].Journal of Computer Science and Technology,1997,12(5):425-440. |
| |
| Authors: | Yuxi Fu |
| |
| Affiliation: | Department of Computer Science; Shanghai Jiaotong University; Shanghai 200030; |
| |
| Abstract: | 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 CZF |
| |
| Keywords: | Type theory constructive set theory w-set |
| 本文献已被 CNKI 维普 SpringerLink 等数据库收录！ |
| 点击此处可从《计算机科学技术学报》浏览原始摘要信息 |
|
点击此处可从《计算机科学技术学报》下载全文 |
