Unfold/Fold Transformations For Definite Clause Programs
Manolis Gergatsoulis and Maria Katzouraki
Abstract
An unfold/fold program transformation
system which extends the unfold/fold transformations of H. Tamaki and T. Sato is
presented in this paper. The system consists of unfolding, simultaneous folding,
and generalization + equality introduction rules. The simultaneous folding rule
permits the folding of a set of folded clauses into a single clause, using a set
of folding clauses, while the generalization + equality introduction rule
facilitates the application of the simultaneous folding rule by performing
appropriate abstractions. A proof of the correctness of the proposed
transformations in the sense of the least Herbrand model semantics of the
program is also presented.
Keywords: program transformations, unfold/fold
transformations, program optimization, program synthesis, logic programming