Declarative foundations of higher-order logic programming

The purpose of this dissertation is to develop a model theoretic semantics for higher-order logic programming languages. Model theoretic semantics has been proved to be successful for first-order logic programming. The usual semantics for first-order logic is two-level: i.e., at a lower level we define a domain of individuals, and then, we define the satisfaction of formulas with respect to this domain. In a higher-order logic which includes the propositional type in its set of primitive types, the definition of satisfaction of formulas is mutually recursive with the process of evaluation of terms. As a result of this mutual recursion it is extremely difficult to define an effective semantics. For example, to define the T$\sb{\cal P}$ operator for a logic program ${\cal P},$ we need a fixed domain independent of interpretations. In the usual semantics for higher-order logic, domain is dependent on interpretation. In order to overcome this problem, intentions rather than extensions are taken to be the main objects of the domain of discourse in higher-order logic programming. With this domain our semantics is proved to provide a more suitable declarative basis for higher-order logic programming than the usual general model theoretic semantics. Higher-order logic programming is shown to possess such semantic properties of first-order logic programming as the least model and the least fixpoint. A quotient of the domain of our model is shown to be a model of various equality theories, and is successfully employed to describe the semantics of logic programs with these equality theories. The second part of this thesis is devoted to studying the semantical properties of variants of definite programs: (1) general programs whose clause bodies may contain negation symbols, and (2) a special class of definite programs that behave extensionally. Our semantics is shown to be general enough to study the properties of these variants of definite programs. A negation as failure rule is also defined and is proved to be sound with respect to our semantics.