Type system provides a precise description of a programming language. This is a prerequisite for the implementation and use of language. It also conducts mechanical and transparent type-checking on programs to preven...Type system provides a precise description of a programming language. This is a prerequisite for the implementation and use of language. It also conducts mechanical and transparent type-checking on programs to prevent the occurrence of execution error during the running of programs. So, it can be said that, on the one hand, type system works as a formal tool to do mathematical analysis of language; on the other hand, it is a formal method for rigorously and precisely designing and implementing language. In this paper, some basic concepts of type system are discussed first. And then, the implementation of a graph- rewriting- based functional language - SClean's type system is given in details. It is hoped that the proposed method of using and implementing type system is of practical usefulness.展开更多
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 t...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 CZF展开更多
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 ...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.展开更多
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 interprete...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.展开更多
The expansion postponement problem in Pure Type Systems is an open problem raised by R. Pollack in 1992. In this paper, the author presents a set of necessary and sufficient conditions for this problem and a set of su...The expansion postponement problem in Pure Type Systems is an open problem raised by R. Pollack in 1992. In this paper, the author presents a set of necessary and sufficient conditions for this problem and a set of sufficient conditions for it. The author also gives some properties for pure type systems without the expansion rule.展开更多
The paper investigates the internal structures of hereditary inductive types in logical type theory. By defining a bisimulation equality on the inhabitants of each hereditary inductive type, one is able to show that t...The paper investigates the internal structures of hereditary inductive types in logical type theory. By defining a bisimulation equality on the inhabitants of each hereditary inductive type, one is able to show that the inhabitants of a hereditary inductive type satisfy the basic properties of sets. A hereditary inductive type can therefore be conceived as a universe of sets.展开更多
Encodings in polymorphism with finite product types are considered. These encodings aregiven in terms of I-algebras. They have the property that the ground terms are precisely theclosed normal terms of the encoded typ...Encodings in polymorphism with finite product types are considered. These encodings aregiven in terms of I-algebras. They have the property that the ground terms are precisely theclosed normal terms of the encoded types. The proof of a well-known result is transplantedto the setting and it is shown why weak recursion is admissible. The paper also shows how tocarry out the dual encodingS using the existential quantifier.展开更多
基金the National Natural Science Foundation of China (No.69931040), and is also supported by Defense Science and Technology Fundi
文摘Type system provides a precise description of a programming language. This is a prerequisite for the implementation and use of language. It also conducts mechanical and transparent type-checking on programs to prevent the occurrence of execution error during the running of programs. So, it can be said that, on the one hand, type system works as a formal tool to do mathematical analysis of language; on the other hand, it is a formal method for rigorously and precisely designing and implementing language. In this paper, some basic concepts of type system are discussed first. And then, the implementation of a graph- rewriting- based functional language - SClean's type system is given in details. It is hoped that the proposed method of using and implementing type system is of practical usefulness.
文摘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 CZF
基金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.
基金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.
文摘The expansion postponement problem in Pure Type Systems is an open problem raised by R. Pollack in 1992. In this paper, the author presents a set of necessary and sufficient conditions for this problem and a set of sufficient conditions for it. The author also gives some properties for pure type systems without the expansion rule.
文摘The paper investigates the internal structures of hereditary inductive types in logical type theory. By defining a bisimulation equality on the inhabitants of each hereditary inductive type, one is able to show that the inhabitants of a hereditary inductive type satisfy the basic properties of sets. A hereditary inductive type can therefore be conceived as a universe of sets.
文摘Encodings in polymorphism with finite product types are considered. These encodings aregiven in terms of I-algebras. They have the property that the ground terms are precisely theclosed normal terms of the encoded types. The proof of a well-known result is transplantedto the setting and it is shown why weak recursion is admissible. The paper also shows how tocarry out the dual encodingS using the existential quantifier.
