We address the problem of proving total correctness of transformation rules for 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 clause replacement is 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 constructing from the given program P an annotated program α (P), (ii) applying clause replacements and transforming the annotated program α (P) into a terminating annotated program β(Q), and (iii) erasing the annotations from β(Q), thereby getting Q. Our method does not require that either P or Q terminates and it is parametric w.r.t. the annotations. By providing different definitions for these annotations, we can easily prove the total correctness of many versions of the unfolding, folding, and goal replacement rules proposed in the literature.

Pettorossi, A., Proietti, M. (2004). A theory of totally correct logic program transformations. In Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation (pp.159-168) [10.1145/1014007.1014023].

A theory of totally correct logic program transformations

PETTOROSSI, ALBERTO;
2004-01-01

Abstract

We address the problem of proving total correctness of transformation rules for 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 clause replacement is 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 constructing from the given program P an annotated program α (P), (ii) applying clause replacements and transforming the annotated program α (P) into a terminating annotated program β(Q), and (iii) erasing the annotations from β(Q), thereby getting Q. Our method does not require that either P or Q terminates and it is parametric w.r.t. the annotations. By providing different definitions for these annotations, we can easily prove the total correctness of many versions of the unfolding, folding, and goal replacement rules proposed in the literature.
Proceedings of the 2004 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, PEPM'04
Verona
2004
ACM SIGPLAN
Rilevanza internazionale
2004
Settore ING-INF/05 - SISTEMI DI ELABORAZIONE DELLE INFORMAZIONI
English
Logic programming; Partial and total correctness; Program transformation rules; Well-founded orderings
Intervento a convegno
Pettorossi, A., Proietti, M. (2004). A theory of totally correct logic program transformations. In Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation (pp.159-168) [10.1145/1014007.1014023].
Pettorossi, A; Proietti, M
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/2108/41705
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact