Synthesis and transformation of logic programs using unfold/fold proofs

We present a method for proving properties of definite logic programs. This method is called unfold/fold proof method because it is based on the unfol d/fold transformation rules. Given a program P and two goals (that is, conj unctions of atoms) F((X) over bar, (Y) over bar) and G((X) over bar, (Y) ov er bar), where (X) over bar, (Y) over bar, and (Z) over bar are pairwise di sjoint vectors of variables, the unfold/fold proof method can be used to sh ow that the equivalence formula For All (X) over bar (There Exists (Y) over bar F((X) over bar, (Y) over bar) <-> There Exists (Z) over bar G((X) over bar, (Z) over bar)) holds in the least Herbrand model of P. Equivalence fo rmulas of that form can be used to justify goal replacement steps, which al low us to transform logic programs by replacing old goals, such as F((X) ov er bar, (Y) over bar), by equivalent new goals, such as G((X) over bar, (Z) over bar). These goal replacements preserve the least Herbrand model seman tics if we find non-ascending unfold/fold proofs of the corresponding equiv alence formulas, that is, unfold/fold proofs which ensure suitable well-fou nded orderings between the successful SLD-derivations of F((X) over bar, (Y ) over bar) and G((X) over bar, (Z) over bar), respectively. We also presen t a method for program synthesis from implicit definitions, It can be used to derive a definite logic program for the predicate newp implicitly define d by an equivalence formula of the form For All (X) over bar(There Exists ( Y) over bar F((X) over bar, (Y) over bar) <-> There Exists (Z) over bar(H(( X) over bar, (Z) over bar), newp((X) over bar, (Z) over bar))), such that t he predicates occurring in the goals F((X) over bar, (Y) over bar) and H((X ) over bar, (Z) over bar) are defined in a given program P, and newp is a p redicate symbol not occurring in P. The set of clauses defining newp, say E ureka, allows us to prove that the above equivalence formula holds in the l east Herbrand model of P boolean OR Eureka using an unfold/fold proof. Thus , the correctness of our synthesis method derives from the one of the unfol d/fold proof method. We finally illustrate our synthesis method through som e examples of program specialization, program synthesis, and program transf ormation, which can all be viewed as program syntheses from implicit defini tions. (C) 1999 Elsevier Science Inc. All rights reserved.