Abstract
An Unfold/Fold transformation system is a source-to-source rewriting methodology devised to improve the efficiency of a program. Any such transformation should preserve the main properties of the initial program: among them, termination. When dealing with logic programs such as PROLOG programs, one is particularly interested in preserving left termination i.e. termination wrt the leftmost selection rule, which is by far the most widely employed of the search rules. Unfortunately, the most popular Unfold/Fold transformation systems ([TS84, Sek91]) do not preserve the above termination property. In this paper we study the reasons why left termination may be spoiled by the application of a transformation operation and we present a transformation system based on the operations of Unfold, Fold and Switch which — if applied to a left terminating programs — yields a program which is left terminating as well.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
K. R. Apt and M. Bezem. Acyclic programs. In D. H. D. Warren and P. Szeredi, editors, Proceedings of the Seventh International Conference on Logic Programming, pages 617–633. The MIT Press, 1990.
K.R. Apt and E. Marchiori. Reasoning about Prolog programs: from modes through types to assertions. Formal Aspects of Computing, 1994. In print. Also Technical report CS-R9358, CWI, Amsterdam, The Netherlands. Available via anonymous ftp at ftp.cwi.nl, or via xmosaic at http://www.cwi.nl/cwi/publications/index.html.
K. R. Apt and D. Pedreschi. Studies in Pure Prolog: termination. In J. W. Lloyd, editor, Symposium on Computational Logic, pages 150–176. Springer-Verlag, 1990.
K. R. Apt and D. Pedreschi. Reasoning about termination of pure Prolog programs. Information and Computation, 106(1):109–157, 1993.
K. R. Apt. Introduction to Logic Programming. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics, pages 495–574. Elsevier, Amsterdam and The MIT Press, Cambridge, 1990.
M. Baudinet. Logic Programming Semantics: Techniques and Applications. PhD thesis, Stanford University, Stanford, California, 1989.
A. Bossi and N. Cocco. Preserving universal termination through unfold/fold. In G. Levi and M. Rodríguez-Artalejo, editors, Proc. Fourth Int'l Conf. on Algebraic and Logic Programming, volume 850 of Lecture Notes in Computer Science, pages 269–286. Springer-Verlag, Berlin, 1994.
A. Bossi, N. Cocco, and S. Etalle. Transformation of Left Terminating Programs: The Reordering Problem. Technical Report CS96-1, Dip. Matematica Applicata e Informatica, Università Ca' Foscari di Venezia, Italy”, 1996.
A. Bossi, N. Cocco, and M. Fabris. Norms on Terms and their use in Proving Universal Termination of a Logic Program. Theoretical Computer Science, 124:297–328, 1994.
R.M. Burstall and J. Darlington. A transformation system for developing recursive programs. Journal of the ACM, 24(1):44–67, January 1977.
A. Bossi and S. Etalle. Transforming Acyclic Programs. ACM Transactions on Programming Languages and Systems, 16(4):1081–1096, July 1994.
J. Cook and J.P. Gallagher. A transformation system for definite programs based on termination analysis. In F. Turini, editor, Proc. Fourth Workshop on Logic Program Synthesis and Transformation. Springer-Verlag, 1994.
K.L. Clark and S. Sickel. Predicate logic: a calculus for deriving programs. In Proceedings of IJCAI'77, pages 419–120, 1977.
S. Decorte, D. De Schreye, and M. Fabris. Automatic Inference of Norms: a Missing Link in Automatic Termination Analysis. In D. Miller, editor, Proc. 1993 Int'l Symposium on Logic Programming. The MIT Press, 1993.
S. Etalle and M. Gabbrielli. Transformations of CLP Modules. Technical Report CS-R9515, CWI, Amsterdam, 1994.
C.J. Hogger. Derivation of logic programs. Journal of the ACM, 28(2):372–392, April 1981.
T. Kawamura and T. Kanamori. Preservation of Stronger Equivalence in Unfold/Fold Logic Programming Transformation. In Proc. Int'l Conf. on Fifth Generation Computer Systems, pages 413–422. Institute for New Generation Computer Technology, Tokyo, 1988.
T. Kawamura and T. Kanamori. Preservation of Stronger Equivalence in Unfold/Fold Logic Programming Transformation. Theoretical Computer Science, 75(1&2):139–156, 1990.
H. Komorowski. Partial evaluation as a means for inferencing data structures in an applicative language: A theory and implementation in the case of Prolog. In Ninth ACM Symposium on Principles of Programming Languages, Albuquerque, New Mexico, pages 255–267. ACM, 1982.
J. W. Lloyd. Foundations of Logic Programming. Springer-Verlag, Berlin, 1987. Second edition.
Mycroft A. N.Jones. Stepwise development of operational and denotational semantics for Prolog. In International Symposium on Logic Programming, Atlantic City, NJ, (U.S.A.), pages 289–298, 1984.
L. Plümer. Termination Proofs for Logic Programs. Lecture Notes in Artificial Intelligence 446. Springer-Verlag, 1990.
M. Proietti and A. Pettorossi. Semantics preserving transformation rules for prolog. In ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation (PEPM '91). ACM press, 1991.
H. Seki. Unfold/fold transformation of stratified programs. Theoretical Computer Science, 86(1):107–139, 1991.
H. Seki. Unfold/fold transformation of general logic programs for the Well-Founded semantics. Journal of Logic Programming, 16(1&2):5–23, 1993.
H. Tamaki and T. Sato. Unfold/Fold Transformations of Logic Programs. In Sten-Åke Tärnlund, editor, Proc. Second Int'l Conf. on Logic Programming, pages 127–139, 1984.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bossi, A., Cocco, N., Etalle, S. (1996). Transformation of left terminating programs: The reordering problem. In: Proietti, M. (eds) Logic Program Synthesis and Transformation. LOPSTR 1995. Lecture Notes in Computer Science, vol 1048. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60939-3_3
Download citation
DOI: https://doi.org/10.1007/3-540-60939-3_3
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60939-1
Online ISBN: 978-3-540-49745-5
eBook Packages: Springer Book Archive