On Hereditary Harrop Formulae as a Basis for Logic Programming

James Harland

Abstract: This thesis examines the use of first-order hereditary Harrop formulae, a generalisation of Horn clauses due to Miller, as a foundation for logic programming. As this framework is constructive, this will sometimes dictate an approach which differs slightly from the traditional (classical) one.

We discuss the foundational problems involved in adding negation to the framework of first-order hereditary Harrop formulae, including the role of the Negation as Failure (NAF) rule and the Closed World Assumption (CWA) in a constructive setting, and introduce the notion of a completely defined predicate. This notion may be used to define a notion of NAF for a more general class of goals than literals. We also discuss the possibilities for forms of negation other than NA, and explore the relationships between NAF and more explicit forms.

Clark's completion of a program is often used in this context, and we show how a more explicit version of the completion may be given in hereditary Harrop formulae. We may think of the completion as specifying a theory in which an atom A fails iff A \supset \perp, and hence is an explicit axiomatisation of failure, which in our case is more computationally meaningful than Clark's completion.

The problem of finding answer substitutions for existentially quantified negated goals requires more powerful techniques than unification alone, and so we give an algorithm which is suitable for this purpose, and show how it may be incorporated into the goal reduction process.

A constructive framework necessitates a different approach to model theory, and we give a Kripke-like model for the extended class of programs for which negation is implemented by the Negation as Failure rule. This is based on the model theory developed by Miller for hereditary Harrop formulae. No restriction on the class of programs is used, which requires some departures from the usual T^{w} process, but the spirit of the construction remains the same.

The Kripke-like model suggests some structural properties of first-order hereditary Harrop formulae which are of semantic interest. One important question is the precise strength of the class of formulae involved. We consider the redundant features of Miller's langauge, and show how they may be removed. This leads to a discussion of equivalence for this class of programs, which necessitates the use of an intermediate logic, in which programs which are operationally equivalent are logically equivalent.

Implication in the bodies of clauses also allows a notion of meta-programming within a first-order framework. We explore this possibility to some extent by showing how the application of some of our results allow memoisation to take place, which may be thought of as reflecting meta-level information back into programs by a subtle separation of object and meta-levels. This also demonstrates an elegant connection between removing redundancies from programs and the derivation of a goal in this framework.

Ph.D Thesis - Price £9.00

LFCS report ECS-LFCS-91-170 (also published as CST-81-91)

Previous | Index | Next