Totally correct logic program transformations via well-founded annotations

    loading  Checking for direct PDF access through Ovid


We address the problem of proving the total correctness of transformations of definite logic programs. We consider a general transformation rule, called clause replacement, which consists in transforming a program P into a new program Q by replacing a set Γ1 of clauses occurring in P by a new set Γ2 of clauses, provided that Γ1 and Γ2 are equivalent in the least Herbrand model M(P) of the program P.

We propose a general method for proving that transformations based on clause replacement are totally correct, that is, M(P)=M(Q). Our method consists in showing that the transformation of P into Q can be performed by: (i) adding extra arguments to predicates, thereby deriving from the given program P an annotated program JOURNAL/hosc/04.02/00125279-200821010-00008/OV0440/v/2017-10-10T043149Z/r/image-png, (ii) applying a variant of the clause replacement rule and transforming the annotated program JOURNAL/hosc/04.02/00125279-200821010-00008/OV0440/v/2017-10-10T043149Z/r/image-png into a terminating annotated program 𝑄̅, and (iii) erasing the annotations from 𝑄̅, thereby getting Q.

Our method does not require that either P or Q are terminating and it is parametric with respect to the annotations. By providing different annotations we can easily prove the total correctness of program transformations based on various versions of the popular unfolding, folding, and goal replacement rules, which can all be viewed as particular cases of our clause replacement rule.

Related Topics

    loading  Loading Related Articles