Semantics of Constructions(Ⅱ) — The Initial Algebraic Approach

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