• Articles • 上一篇    下一篇

Constructive Sets in Computable Sets

傅育熙;   

  1. Department of Computer Science; Shanghai Jiaotong University; Shanghai 200030;
  • 出版日期:1997-09-10 发布日期:1997-09-10

Constructive Sets in Computable Sets

Mi Thxi;   

  1. Department of Computer Science; Shanghai Jiaotong University; Shanghai 200030;
  • Online:1997-09-10 Published:1997-09-10

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…

关键词: multicast routing, protocol, dynamic ring, ad hoc wireless network

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…

Key words: ad hoc wireless network, multicast routing, protocol, dynamic ring



[1] Aczel P. The type theoretic interpretation of constructive set theory. In Logic Colloquium '77, Macintyre A, Pacholski L, Paris J eds., North-Holland, 1978, pp.55-66.

[2] Troelstra A, van Dalen D. Constructivism in Mathematics: An Introduction, II. North-Holland, 1988.

[3] Nordstrom B, Petersson K, Smith J. Programming in Martin-Lof's type theory-An introduction. In International Series of Monographs on Computer Science 7, Oxford University Press, 1990. ……….
[1] . 暂缺[J]. , 2009, 24(1 ): 138-151 .
[2] . 基于转发和控制分离的开放可编程路由器的分析和实现[J]. , 2008, 23(5 ): 769-779 .
[3] . GBP-WAHSN:适用于大型无线自组织传感网络的基于群组结构的路由协议[J]. , 2008, 23(3): 461-480 .
[4] . 一个针对一种秘密集合运算的协议[J]. , 2007, 22(6): 822-829 .
[5] . 基于可满足性求解的认证协议的认知规范验证[J]. , 2006, 21(6): 932-943 .
[6] . 中国信息安全研究进展与展望[J]. , 2006, 21(5): 740-755 .
[7] . 暂缺[J]. , 2006, 21(5): 765-775 .
[8] . [J]. , 2005, 20(2): 0-0.
[9] . [J]. , 2005, 20(1): 0-0.
[10] . [J]. , 2004, 19(6): 0-0.
[11] . [J]. , 2004, 19(6): 0-0.
[12] . [J]. , 2004, 19(4): 0-0.
[13] . [J]. , 2004, 19(2): 0-0.
[14] . [J]. , 2003, 18(6): 0-0.
[15] . [J]. , 2003, 18(5): 0-0.
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
[1] 金兰; 杨元元;. A Modified Version of Chordal Ring[J]. , 1986, 1(3): 15 -32 .
[2] 范植华;. Vectorization for Loops with Three-Forked Jumps[J]. , 1988, 3(3): 186 -202 .
[3] 薛行; 孙钟秀; 周建强; 徐希豪;. A Message-Based Distributed Kernel for a Full Heterogeneous Environment[J]. , 1990, 5(1): 47 -56 .
[4] 郭庆平; Y.Paker;. Communication Analysis and Granularity Assessment for a Transputer-Based System[J]. , 1990, 5(4): 347 -362 .
[5] 廖先湜; 金兰;. A Mechanism Supporting the Client/Server Relationship in the Operating System of Distributed System “THUDS”[J]. , 1991, 6(3): 256 -262 .
[6] 孙玉方;. The UNIX Localization and Chinese Information Processing System[J]. , 1991, 6(4): 370 -375 .
[7] 许满武;. An Implementation of Pure Horn Clause Logic Programming in a Reduction System[J]. , 1993, 8(3): 53 -61 .
[8] 周勇; 唐泽圣;. Constructing Isosurfaces from 3D Data Sets Taking Account of Depth Sorting of Polyhedra[J]. , 1994, 9(2): 117 -127 .
[9] 廖乐健; 史忠植;. Minimal Model Semantics for Sorted Constraint Representation[J]. , 1995, 10(5): 439 -446 .
[10] 赵彧; 张琼; 向辉; 石教英; 何志均;. A Simplified Model for Generating 3D Realistic Sound in the Multimedia and Virtual Reality Systems[J]. , 1996, 11(4): 461 -470 .
版权所有 © 《计算机科学技术学报》编辑部
本系统由北京玛格泰克科技发展有限公司设计开发 技术支持:support@magtech.com.cn
总访问量: