Author:

Abstract:

In logic programming, {\em meta-programming} has been advocated as a major route towards increased knowledge representation and reasoning capabilities. And writing programs that treat other programs as data is not difficult to accomplish within its framework. However, in many cases, the practice seemed to lack a clear {\em semantical foundation}. In the {\em first part} of this thesis, we therefore study a {\em semantics for untyped, vanilla meta-programs, using the non-ground representation} for object level variables. We do not only address the basic vanilla meta-interpreter, but also some interesting extensions, including programs which allow some forms of amalgamation. We show that for stratified object programs, associated meta-programs are weakly stratified. For a large class of object programs, we establish a natural correspondence between the object level perfect and the meta level weakly perfect Herbrand models, thus providing a sensible meta-program semantics. Finally, for definite object programs, we reconsider and generalise these results in the context of an extended Herbrand semantics, designed to closely mirror the operational behaviour of logic programs. Another problem faced by meta-programming applications is a considerable loss of {\em execution efficiency} (compared with reasoning directly at the object level). Specialising meta-interpreters with respect to object programs helps. {\em Partial deduction} constitutes one technique used to pursue this effect. However, its relevance is not limited to this particular setting. This leads us, in the {\em second part} of this thesis, to a study of {\em partial deduction for (pure) definite logic programs}. Within that context, we focus on the (online) {\em control of unfolding}, devising methods to ensure its {\em termination} in a way that reflects structural properties of the query and program to be unfolded. We propose a general framework for finite unfolding, based on well-founded orderings. We extensively investigate several concrete instances and present fully automatic algorithms. Using such unfolding to construct finite SLD-trees, we formulate a sound and complete, always terminating, completely automatic method for partial deduction. Finally, some experiments, comparing various approaches, are briefly discussed. Throughout our presentation, we particularly emphasise detailed formalisations, allowing formal proofs for interesting properties of the various algorithms.