A theory of totally correct logic program transformations

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

A theory of totally correct logic program transformations

Full text

Pdf (197 KB)

Source

ACM/SIGPLAN Workshop Partial Evaluation and Semantics-Based Program Manipulation archive
Proceedings of the 2004 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation table of contents

Verona, Italy

Pages: 159 - 168

Year of Publication: 2004

ISBN:1-58113-835-0

Authors

Alberto Pettorossi	University of Roma Tor Vergata, Roma, Italy
Maurizio Proietti	IASI-CNR, Roma, Italy

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages
ACM: Association for Computing Machinery

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 3, Downloads (12 Months): 13, Citation Count: 0

Additional Information:

abstract references index terms collaborative colleagues peer to peer

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/1014007.1014023 What is a DOI?

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 Γ¹ of clauses occurring in P by a new set Γ² of clauses, provided that Γ¹ and Γ² 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.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	Krzysztof R. Apt, Logic programming, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
	2	M. Bezem. Characterizing termination of logic programs with level mappings. In E.L. Lusk and R.A. Overbeek, editors, Proceedings of the North American Conference on Logic Programming, Cleveland, Ohio (USA), pages 69--80. MIT Press, 1989.
	3	Annalisa Bossi , Nicoletta Cocco , Sandro Etalle, On Safe Folding, Proceedings of the 4th International Symposium on Programming Language Implementation and Logic Programming, p.172-186, August 26-28, 1992
	4	A. Bossi, N. Cocco, and S. Etalle. Simultaneous replacement in normal programs. Journal of Logic and Computations, 6(1):79--120, 1996.
	5	R. M. Burstall , John Darlington, A Transformation System for Developing Recursive Programs, Journal of the ACM (JACM), v.24 n.1, p.44-67, Jan. 1977 [doi>10.1145/321992.321996]
	6	B. Courcelle. Infinite trees in normal form and recursive equations having a unique solution. Mathematical Systems Theory, 13:131--180, 1979.
	7	Nachum Dershowitz, Termination of rewriting, Journal of Symbolic Computation, v.3 n.1-2, p.69-116, Feb./April 1987 [doi>10.1016/S0747-7171(87)80022-6]
	8	Manolis Gergatsoulis , Maria Katzouraki, Unfold/Fold Transformations For Definite Clause Programs, Proceedings of the 6th International Symposium on Programming Language Implementation and Logic Programming, p.340-354, September 14-16, 1994
	9	J. Jaffar, M. Maher, K. Marriott, and P. Stuckey. The semantics of constraint logic programming. Journal of Logic Programming, 37:1--46, 1998.
	10	T. Kanamori and H. Fujita. Unfold/fold transformation of logic programs with counters. Technical Report 179, ICOT, Tokyo, Japan, 1986.
	11	M. J. Maher. Correctness of a logic program transformation system. IBM Research Report RC 13496, T. J. Watson Research Center, 1987.
	12	Z. Manna and A. Pnueli. Axiomatic approach to total correctness of programs. Acta Informatica, 3:243--263, 1974.
	13	Helmut A. Partsch, Specification and transformation of programs: a formal approach to software development, Springer-Verlag New York, Inc., New York, NY, 1990
	14	G. D. Plotkin. A structural approach to operational semantics. Technical Report DAIMI FN-19, Computer Science Department, Aarhus University, Aarhus, Denmark, 1981.
	15	Maurizio Proietti , Alberto Pettorossi, Transforming inductive definitions, Proceedings of the 1999 international conference on Logic programming, p.486-499, November 1999, Las Cruces, New Mexico, United States
	16	Abhik Roychoudhury , K. Narayan Kumar , C. R. Ramakrishnan , I. V. Ramakrishnan, An unfold/fold transformation framework for definite logic programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.26 n.3, p.464-509, May 2004 [doi>10.1145/982158.982160]
	17	David Sands, From SOS rules to proof principles: an operational metatheory for functional languages, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.428-441, January 15-17, 1997, Paris, France [doi>10.1145/263699.263760]
	18	H. Tamaki and T. Sato. Unfold/fold transformation of logic programs. In S.-Å. Tärnlund, editor, Proceedings of the Second International Conference on Logic Programming, pages 127--138, Uppsala, Sweden, 1984.
	19	H. Tamaki and T. Sato. A generalized correctness proof of the unfold/fold logic program transformation. Technical Report 86-4, Ibaraki University, Japan, 1986.