Semantics of Constructions (I)──The Traditional Approach  

作　　者：傅育熙 

出　　处：《Journal of Computer Science & Technology》2001年第1期13-24,共12页计算机科学技术学报（英文版）

基　　金：This work is funded by the National Natural Science Foundation of China (No.69973030). It is alsosupported by BASICS, Center o

摘　　要：It is well known that impredicative type systems do not have set theoretical semantics. This paper takes a look at semantics of inductive types in impredicative type systems. A generalized inductive type is interpreted as an omega set generated by effectivizing a certain rule set. The result provides a semantic justification of inductive types in the calculus of constructions.It is well known that impredicative type systems do not have set theoretical semantics. This paper takes a look at semantics of inductive types in impredicative type systems. A generalized inductive type is interpreted as an omega set generated by effectivizing a certain rule set. The result provides a semantic justification of inductive types in the calculus of constructions.

关 键 词：type theory inductive type ω-set 

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