Semantics Preserving Transformation Rules for Prolog

The application of the transformational methodology to the area of logic programming is based on theoretical results which show that the Unfold/Fold transformation rules preserve both the least Herbrand model semantics and the set of answer substitutions semantics of logic programs [Tamaki-Sato 84, Kawamura-Kanamori 88]. Unfortunately, those semantics do not capture the termination behaviour of logic programs when they are evaluated under the standard depth-first search strategy of Prolog, which is the basis of most existing implementations of logic programming. As a consequence, the programmer is left with the hard task of checking that the transformation techniques given in the literature, behave conveniently when used for Prolog programs. In the present work we study the applicability of those techniques when logic programs are evaluated according to the Prolog depth-first search strategy, and in particular, we study the correctness of the Unfold/Fold transformations for Prolog programs.