Semantics of Constructions (Ⅰ)The Traditional Approach

• 作 者: 傅育熙
• 机 构: Department of Computer Science, Shanghai Jiaotong University, Shanghai 200030, P.R. China E-mail: fu
• 出 处: 计算机科学技术学报(英文版)
• 发表日期: 2001年1期
• 关键词: inductive type

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.