Partial evaluation in logic programming

Under the conditions of closedness and independence stated in Lloyd and Shepherdson [1991], correctness of the specialized program is guaranteed.

“Under the conditions stated in Lloyd and Shepherdson [1991], namely closedness and independence, correctness of the specialized program is guaranteed.”

There is no fundamental difference between the approach that throws away the original program and the Lloyd and Shepherdson framework; keeping part of the original program can be simulated by using unconstrained characteristic atoms of the form (A, {}) combined with a renaming α such that α((A, {})) = A.

“However, there is no fundamental difference between these two approaches: keeping part of the original program can be simulated in our approach by using unconstrained characteristic atoms of the form (A, { }) combined with a renaming α such that α((A, { })) = A.”

If ← A resolves with C to G then G fails finitely in P.

“We also need the following lemma from Lloyd and Shepherdson [1991], where it is Lemma 4.10.If ← A resolves with C to G then G fails finitely in P .”

The partial deduction framework of [60] does not guarantee the preservation of the sequence of computed answers; it only preserves the computed answers but not their sequence.

“This for instance is not guaranteed by the partial deduction framework of [60], which only preserves the computed answers but not their sequence.”

Partial evaluation of ITE-Prolog can be situated somewhere between partial deduction of pure logic programs and partial evaluation of full Prolog.

“In summary, partial evaluation of ITE-Prolog, can be situated somewhere between partial deduction of pure logic programs (see [60,31,10,69,68] and systems like sP [30,29], sAGE [34,33] or more recently ECCE [50,51,57]) and partial evaluation of full Prolog (e.g. MIXTUs [83,82] or PADDY [76–78]).”