Partial evaluation in logic programming

AbstractThis paper gives a theoretical foundation for partial evaluation in logic programming. Let P be a normal program, G a normal goal, A a finite set of atoms, and P′ a partial evaluation of P wrt A. We study, for both the declarative and procedural semantics, conditions under which P′ is sound and complete wrt P for the goal G. We identify two relevant conditions, those of closedness and independence. For the procedural semantics, we show that, if P′ ∪ {G} is A-closed and A is independent, then P′ is sound and complete wrt P for the goal G. For the declarative semantics, we show that, if P′ ∪ {G} is A-closed, then P′ is sound wrt P for the goal G. However, we show that, unless strong conditions are imposed, we do not have completeness for the declarative semantics. A practical consequence of our results is that partial evaluators should enforce the closedness and independence conditions