On hereditary Harrop formulae as a basis for logic programming
James Harland · ERA · 1991
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 whicli 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 NAF, 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 if A D I, 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 Tw 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 "No man is an island, entire of itself..." -John Donne There are many people who have helped me on my way in this long and arduous quest.My supervisor, Don Sannella, has been a constant source of advice, encouragement and enthusiasm.His careful reading of various ill-defined and poorly written documents has been a great boon.Dale Miller has been a patient and reliable source of stimulating discussion, often nudging my hastily thought out and sketchy ideas towards enlightenment.Robin Milner and Cohn Stirling proved themselves very good at plucking the kernel of wheat out of a mountain of chaff.Discussions with a number of people have enriched me, and there are far too many to name them all individually, but chief amongst them are Jamie An-