Semantics of Constructions (Ⅱ)─ The Initial Algebraic Approach  

作　　者：傅育熙 

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

基　　金：the National Natural Science Foundation of China (No.69973030). It is alsosupported by BASICS, Center of Basic Studies in Comp

摘　　要：Inductive types can be formulated by incorporating the idea of initial T-algebra. The interpretation of an inductive type of this kind boils down to finding out the initial T-algebra defined by the inductive type. In this paper the issue in the semantic domain of omega sets is examined. Based on the semantic results, a new class of inductive types, that of local inductive types, is proposed.Inductive types can be formulated by incorporating the idea of initial T-algebra. The interpretation of an inductive type of this kind boils down to finding out the initial T-algebra defined by the inductive type. In this paper the issue in the semantic domain of omega sets is examined. Based on the semantic results, a new class of inductive types, that of local inductive types, is proposed.

关 键 词：type theory inductive type w-set T-algebra 

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