Abstract
We present an overview of the program transformation techniques which have been proposed over the past twenty-five years in the context of logic programming. We consider the approach based on rules and strategies. First, we present the transformation rules and we address the issue of their correctness. Then, we present the transformation strategies and, through some examples, we illustrate their use for improving program efficiency via the elimination of unnecessary variables, the reduction of nondeterminism, and the use of program specialization. We also describe the use of the transformation methodology for the synthesis of logic programs from first-order specifications. Finally, we illustrate some transformational techniques for verifying first-order properties of logic programs and their application to model checking for finite and infinite state concurrent systems.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Alpuente, M., Falaschi, M., Moreno, G., Vidal, G.: A transformation system for lazy functional logic programs. In: Middeldorp, A., Sato, T. (eds.) FLOPS 1999. LNCS, vol. 1722, pp. 147–162. Springer, Heidelberg (1999)
Apt, K.R., Bol, R.N.: Logic programming and negation: A survey. Journal of Logic Programming 19, 20, 9–71 (1994)
Apt, K.R., Pedreschi, D.: Reasoning about termination of pure logic programs. Information and Computation 106, 109–157 (1993)
Aravindan, C., Dung, P.M.: On the correctness of unfold/fold transformation of normal and extended logic programs. Journal of Logic Programming 24(3), 201–217 (1995)
Basin, D., Deville, Y., Flener, P., Hamfelt, A., Fischer Nilsson, J.: Synthesis of programs in computational logic. In: Bruynooghe, M., Lau, K.-K. (eds.) Program Development in Computational Logic. LNCS, vol. 3049, pp. 30–65. Springer, Heidelberg (2004)
Bossi, A., Cocco, N.: Basic transformation operations which preserve computed answer substitutions of logic programs. Journal of Logic Programming 16(1&2), 47–87 (1993)
Bossi, A., Cocco, N.: Preserving universal termination through unfold/fold. In: Rodríguez-Artalejo, M., Levi, G. (eds.) ALP 1994. LNCS, vol. 850, pp. 269–286. Springer, Heidelberg (1994)
Bossi, A., Cocco, N., Dulli, S.: A method for specializing logic programs. ACM Transactions on Programming Languages and Systems 12(2), 253–302 (1990)
Bossi, A., Cocco, N., Etalle, S.: Transforming normal programs by replacement. In: Pettorossi, A. (ed.) META 1992. LNCS, vol. 649, pp. 265–279. Springer, Heidelberg (1992)
Bossi, A., Cocco, N., Etalle, S.: Simultaneous replacement in normal programs. Journal of Logic and Computation 6(1), 79–120 (1996)
Bossi, A., Cocco, N., Etalle, S.: Transforming left-terminating programs: The reordering problem. In: Proietti, M. (ed.) LOPSTR 1995. LNCS, vol. 1048, pp. 33–45. Springer, Heidelberg (1996)
Bossi, A., Etalle, S.: Transforming acyclic programs. ACM Transactions on Programming Languages and Systems 16(4), 1081–1096 (1994)
Bruynooghe, M., De Schreye, D., Krekels, B.: Compiling control. Journal of Logic Programming 6, 135–162 (1989)
Bugliesi, M., Lamma, E., Mello, P.: Partial evaluation for hierarchies of logic theories. In: Debray, S., Hermenegildo, M. (eds.) Logic Programming: Proceedings of the 1990 North American Conference, Austin, Texas, October 1990, pp. 359–376. MIT Press, Cambridge (1990)
Bugliesi, M., Rossi, F.: Partial evaluation in Prolog: Some Improvements about Cut. In: Lusk, E.L., Overbeek, R.A. (eds.) Logic Programming: Proceedings of the North American Conference 1989, Cleveland, Ohio, October 1989, pp. 645–660. MIT Press, Cambridge (1989)
Bundy, A., Smaill, A., Wiggins, G.: The synthesis of logic programs from inductive proofs. In: Lloyd, J.W. (ed.) Computational Logic, Symposium Proceedings, Brussels, November 1990, pp. 135–149. Springer, Berlin (1990)
Burstall, R.M., Darlington, J.: A transformation system for developing recursive programs. Journal of the ACM 24(1), 44–67 (1977)
Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)
De Schreye, D., Glück, R., Jørgensen, J., Leuschel, M., Martens, B., Sørensen, M.H.: Conjunctive partial deduction: Foundations, control, algorithms, and experiments. Journal of Logic Programming 41(2–3), 231–277 (1999)
Debray, S.K.: Optimizing almost-tail-recursive Prolog programs. In: Jouannaud, J.-P. (ed.) FPCA 1985. LNCS, vol. 201, pp. 204–219. Springer, Heidelberg (1985)
Delzanno, G., Podelski, A.: Constraint-based deductive model checking. International Journal on Software Tools for Technology Transfer 3(3), 250–270 (2001)
Etalle, S., Gabbrielli, M.: Transformations of CLP modules. Theoretical Computer Science 166, 101–146 (1996)
Etalle, S., Gabbrielli, M., Marchiori, E.: A transformation system for CLP with dynamic scheduling and CCP. In: PEPM 1997, pp. 137–150. ACM Press, New York (1997)
Etalle, S., Gabbrielli, M., Meo, M.C.: Transformations of ccp programs. ACM Transactions on Programming Languages and Systems 23(3), 304–395 (2001)
Fioravanti, F., Pettorossi, A., Proietti, M.: Verifying CTL properties of infinite state systems by specializing constraint logic programs. In: Proceedings of the ACM Sigplan Workshop on Verification and Computational Logic VCL 2001, Florence (Italy), Technical Report DSSE-TR-2001-3, pp. 85–96. University of Southampton, UK (2001)
Fioravanti, F., Pettorossi, A., Proietti, M.: Transformation rules for locally stratified constraint logic programs. In: Bruynooghe, M., Lau, K.-K. (eds.) Program Development in Computational Logic. LNCS, vol. 3049, pp. 292–340. Springer, Heidelberg (2004)
Flener, P., Lau, K.-K., Ornaghi, M., Richardson, J.: An abstract formalization of correct schemas for program synthesis. Journal of Symbolic Computation 30(1), 93–127 (2000)
Gallagher, J.P.: Transforming programs by specialising interpreters. In: Proceedings Seventh European Conference on Artificial Intelligence, ECAI 1986, pp. 109–122 (1986)
Gallagher, J.P.: Tutorial on specialisation of logic programs. In: Proceedings of the 1993 ACM SIGPLAN Symposium on Partial Evaluation and Semantics Based Program Manipulation, PEPM 1993, Copenhagen, Denmark, pp. 88–98. ACM Press, New York (1993)
Gardner, P.A., Shepherdson, J.C.: Unfold/fold transformations of logic programs. In: Lassez, J.-L., Plotkin, G. (eds.) Computational Logic, Essays in Honor of Alan Robinson, pp. 565–583. MIT, Cambridge (1991)
Hogger, C.J.: Derivation of logic programs. Journal of the ACM 28(2), 372–392 (1981)
Jones, N.D., Gomard, C.K., Sestoft, P.: Partial Evaluation and Automatic Program Generation. Prentice-Hall, Englewood Cliffs (1993)
Komorowski, H.J.: 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, USA, pp. 255–267 (1982)
Kott, L.: The McCarthy’s induction principle: ‘oldy’ but ‘goody’. Calcolo 19(1), 59–69 (1982)
Lamport, L.: A new solution of Dijkstra’s concurrent programming problem. Communications of the ACM 17(8), 453–455 (1974)
Lau, K.-K., Ornaghi, M., Pettorossi, A., Proietti, M.: Correctness of logic program transformation based on existential termination. In: Lloyd, J.W. (ed.) Proceedings of the 1995 International Logic Programming Symposium (ILPS 1995), pp. 480–494. MIT Press, Cambridge (1995)
Leuschel, M., Bruynooghe, M.: Logic program specialisation through partial deduction: Control issues. Theory and Practice of Logic Programming 2(4&5), 461–515 (2002)
Levi, G., Sardu, G.: Partial evaluation of meta programs in a multiple worlds logic language. New Generation Computing 6(2&3), 227–248 (1988)
Lloyd, J.W.: Foundations of Logic Programming, 2nd edn. Springer, Berlin (1987)
Maher, M.J.: A transformation system for deductive database modules with perfect model semantics. Theoretical Computer Science 110, 377–403 (1993)
Manna, Z., Waldinger, R.: A deductive approach to program synthesis. ACM Toplas 2, 90–121 (1980)
The MAP transformation system (1995–2010), http://www.iasi.cnr.it/~proietti/system.html
Pettorossi, A.: A powerful strategy for deriving efficient programs by transformation. In: ACM Symposium on Lisp and Functional Programming, pp. 273–281. ACM Press, New York (1984)
Pettorossi, A., Proietti, M.: Synthesis and transformation of logic programs using unfold/fold proofs. Journal of Logic Programming 41(2&3), 197–230 (1999)
Pettorossi, A., Proietti, M.: Perfect model checking via unfold/fold transformations. In: Palamidessi, C., Moniz Pereira, L., Lloyd, J.W., Dahl, V., Furbach, U., Kerber, M., Lau, K.-K., Sagiv, Y., Stuckey, P.J. (eds.) CL 2000. LNCS (LNAI), vol. 1861, pp. 613–628. Springer, Heidelberg (2000)
Pettorossi, A., Proietti, M., Renault, S.: Derivation of efficient logic programs by specialization and reduction of nondeterminism. Higher-Order and Symbolic Computation 18(1-2), 121–210 (2005)
Pettorossi, A., Proietti, M., Senni, V.: Proving properties of constraint logic programs by eliminating existential variables. In: Etalle, S., Truszczyński, M. (eds.) ICLP 2006. LNCS, vol. 4079, pp. 179–195. Springer, Heidelberg (2006)
Pettorossi, A., Proietti, M., Senni, V.: Automatic correctness proofs for logic program transformations. In: Dahl, V., Niemelä, I. (eds.) ICLP 2007. LNCS, vol. 4670, pp. 364–379. Springer, Heidelberg (2007)
Proietti, M., Pettorossi, A.: Semantics preserving transformation rules for Prolog. In: 1991 ACM SIGPLAN Symposium on Partial Evaluation and Semantics Based Program Manipulation, PEPM 1991, Yale University, New Haven, Connecticut, USA, pp. 274–284. ACM Press, New York (1991)
Proietti, M., Pettorossi, A.: Unfolding-definition-folding, in this order, for avoiding unnecessary variables in logic programs. Theoretical Computer Science 142(1), 89–124 (1995)
Rabin, M.O.: Decidable theories. In: Barwise, J. (ed.) Handbook of Mathematical Logic, pp. 595–629. North-Holland, Amsterdam (1977)
Roychoudhury, A., Narayan Kumar, K., Ramakrishnan, C.R., Ramakrishnan, I.V.: Beyond Tamaki-Sato style unfold/fold transformations for normal logic programs. International Journal on Foundations of Computer Science 13(3), 387–403 (2002)
Roychoudhury, A., Narayan Kumar, K., Ramakrishnan, C.R., Ramakrishnan, I.V.: An unfold/fold transformation framework for definite logic programs. ACM Transactions on Programming Languages and Systems 26, 264–509 (2004)
Roychoudhury, A., Narayan Kumar, K., Ramakrishnan, C.R., Ramakrishnan, I.V., Smolka, S.A.: Verification of parameterized systems using logic program transformations. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol. 1785, pp. 172–187. Springer, Heidelberg (2000)
Safra, S., Shapiro, E.: Meta interpreters for real. In: Kugler, H.J. (ed.) Proceedings Information Processing 1986, pp. 271–278. North-Holland, Amsterdam (1986)
Sato, T., Tamaki, H.: Transformational logic program synthesis. In: Proceedings of the International Conference on Fifth Generation Computer Systems, pp. 195–201. ICOT (1984)
Seki, H.: A comparative study of the well-founded and the stable model semantics: Transformation’s viewpoint. In: Proceedings of the Workshop on Logic Programming and Non-monotonic Logic, pp. 115–123. Cornell University (1990)
Seki, H.: Unfold/fold transformation of stratified programs. Theoretical Computer Science 86, 107–139 (1991)
Seki, H.: Unfold/fold transformation of general logic programs for well-founded semantics. Journal of Logic Programming 16(1&2), 5–23 (1993)
Seki, H.: On inductive and coinductive proofs via unfold/fold transformations. In: De Schreye, D. (ed.) LOPSTR 2009. LNCS, vol. 6037, pp. 82–96. Springer, Heidelberg (2009)
Sterling, L., Beer, R.D.: Incremental flavour-mixing of meta-interpreters for expert system construction. In: Proceedings of 3rd International Symposium on Logic Programming, Salt Lake City, Utah, USA, pp. 20–27. IEEE Press, Los Alamitos (1986)
Tacchella, P., Gabbrielli, M., Meo, M.C.: Unfolding in CHR. In: Proceedings of the 9th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP 2007), pp. 179–186 (2007)
Takeuchi, A., Furukawa, K.: Partial evaluation of Prolog programs and its application to meta-programming. In: Kugler, H.J. (ed.) Proceedings of Information Processing 1986, pp. 415–420. North-Holland, Amsterdam (1986)
Tamaki, H., Sato, T.: Unfold/fold transformation of logic programs. In: Tärnlund, S.-Å. (ed.) Proceedings of the Second International Conference on Logic Programming (ICLP 1984), pp. 127–138. Uppsala University, Uppsala (1984)
Toni, F., Kowalski, R.: An argumentation-theoretic approach to logic program transformation. In: Proietti, M. (ed.) LOPSTR 1995. LNCS, vol. 1048, pp. 61–75. Springer, Heidelberg (1996)
Venken, R.: A Prolog meta-interpretation for partial evaluation and its application to source-to-source transformation and query optimization. In: O’Shea, T. (ed.) Proceedings of ECAI 1984, pp. 91–100. North-Holland, Amsterdam (1984)
Wadler, P.L.: Deforestation: Transforming programs to eliminate trees. Theoretical Computer Science 73, 231–248 (1990)
Zhang, J., Grant, P.W.: An automatic difference-list transformation algorithm for Prolog. In: Proceedings 1988 European Conference on Artificial Intelligence, ECAI 1988, pp. 320–325. Pitman (1988)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Pettorossi, A., Proietti, M., Senni, V. (2010). The Transformational Approach to Program Development. In: Dovier, A., Pontelli, E. (eds) A 25-Year Perspective on Logic Programming. Lecture Notes in Computer Science, vol 6125. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-14309-0_6
Download citation
DOI: https://doi.org/10.1007/978-3-642-14309-0_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-14308-3
Online ISBN: 978-3-642-14309-0
eBook Packages: Computer ScienceComputer Science (R0)