Models and resolution principles for logical meta-programming languages

Overview & Synopsis

Meta-programming extends logic programming with the possibility of having a program to create or analyze other programs represented as data structures and to give queries dynamically to these programs. Thus languages for meta-programming represent a logical formalism in which logical theories can refer to provability in arbitrary other, perhaps dynamically generated, theories. The importance is stressed of allowing variables in the program representation which stand for unknown program fragments, even in the program currently under execution. This can be used, for example, for hypothetical reasoning where a program generates the hypotheses to be tested of for program generation in the sense that an interpreter fills in the missing program parts. It may lead to a more declarative style of, e.g., program generation - the meta-program can specify properties of the desired programs at a higher level of abstraction and the detailed synthesis is put in the hands of an implementation. The declarative semantics is described in terms of Herbrand-models analogous to those normally used for plain logic programs and the well-known fixed-point results generalize immediately. The procedural semantics is given as a resolution method which is shown to be sound and complete. Complete resolution for meta-programming languages is more complicated than usual due to the possibility of uninstantiated variables which stand for unknown parts of the program currently under execution.