Browse Reports

The objective of this thesis is to provide a formal basis for higher-order features in the paradigm of logic programming. Towards this end, a non-extensional form of higher-order logic that is based on Church''s simple theory of types is used to provide a generalisation to the definite clauses of first-order logic. Specifically, a class of formulas that are called higher-order definite sentences is described. These formulas extend definite clauses by replacing first-order terms by the terms of a typed $\lambda$ -calculus and by providing for quantification over predicate and function variables. It is shown that these formulas, together with the notion of a proof in the higher-order logic, provide an abstract description of computation that is akin to the one in the first-order case. While the construction of a proof in a higher-order logic is often complicated by the task of finding appropriate substitutions for predicate variables, it is shown that the necessary substitutions for predicate variables can be tightly constrained in the context of higher-order definite sentences. This observation enables the description of a complete theorem-proving procedure for these formulas. The procedure constructs proofs essentially by interweaving higher-order unification with backchaining on implication, and constitutes a generalisation, to the higher-order context, of the well-known SLD-resolution procedure for definite clauses. The results of these investigations are used to describe a logic programming language called $\lambda$ Prolog. This language contains all the features of a language such a Prolog, and, in addition, possesses certain higher-order features. The nature of these additional features is illustrated, and it is shown how the use of the terms of a (typed) $\lambda$ -calculus as data structures provides a source of richness to the logic programming paradigm.