The Declarative Semantics Of Logic Programming Language G(?)del

G(o|¨)del is a declarative logic programming language succeeded to Prolog.It is based on many-sorted first order logic with parametric polymorphism,discards the features of Prolog which are non-logical,introduces type system,integrates the merit of many languages,adds some new language components which let it be efficient declarative programming language.However,the complexity of language G(o|¨)del is greatly increased with the introduction of type system,modular structure,delay calculation,pruning operation.Because the methods and techniques in compiler of the logic programming language with recursive and descriptive characteristics are completely different from that used in the compiler of process-oriented programming language,the methods and techniques can not transplantation.The basic theory research is lag behind,so the research and development of the compiler system of language G(o|¨)del is still in slow progress.In order to facilitate the promotion and in-depth research of language G(o|¨)del,a strict mathematical basis of language G(o|¨)del is established in this paper,including its grammar and declarative semantic theory,which can lay a reliable theoretical basis for the realization of the compiler system of language G(o|¨)del.In view of the limitations of the traditional first order logic language,the traditional language of first-order is expanded,and a complete definition of typed first-order language is given.Finally,the theory of typed first order logic is established,and the syntax part of language G(o|¨)del is given by use of the Horn subset of typed first-order language.On this basis,the general definition of explanation or assignment is given,and then the true value discriminance of typed well-formed formula based on reasonable explanation is discussed.The model of typed first order logic system is established,and then the declarative semantics of G(o|¨)del program is discussed through the H-model of typed first-order language.And ultimately concluded that the least H-model Mp can be used as the formal semantics of program P in G(o|¨)del on the grounds that the composition of Mp is the base atoms which infer from P in logic.Finally,this paper proposed the algorithm to realize the control facility in G(o|¨)del language which can support the fully realized of G(o|¨)del language.