A method for specializing logic programs

ABSTRACT

A specialization method for logic programs that allows one to restrict a general program to special cases by means of constraint predicates is presented. A set of basic transformation operations, which are shown to produce equivalent programs, is defined. The method uses these operations for propagating the constraint information through the program and for consequently simplifying it whenever possible. Some examples of specializations are given, and some improvements and developments of the method are discussed.

REFERENCES

• 1: Vincenzo Ambriola , Fosca Giannotti , Dino Pedreschi , Franco Turini, Symbolic semantics and program reduction, IEEE Transactions on Software Engineering, v.11 n.8, p.784-794, Aug. 1985 [doi>10.1109/TSE.1985.232527]
• 2: ANDERSON, J. M., AND JOHNSTONE, $. W., JR. Natural Deduction. Wadsworth, Belmont, Calif., 1962.
• 3: Krzysztof R. Apt , M. H. van Emden, Contributions to the Theory of Logic Programming, Journal of the ACM (JACM), v.29 n.3, p.841-862, July 1982 [doi>10.1145/322326.322339]
• 4: Francois Bancilhon , Raghu Ramakrishnan, An amateur's introduction to recursive query processing strategies, Proceedings of the 1986 ACM SIGMOD international conference on Management of data, p.16-52, May 28-30, 1986, Washington, D.C., United States
• 5: Annalisa Bossi , Nicoletta Cocco, Verifying Correctness of Logic Programs, Proceedings of the International Joint Conference on Theory and Practice of Software Development, Volume 2: Advanced Seminar on Foundations of Innovative Software Development II and Colloquium on Current Issues in Programming Languages, p.96-110, March 13-17, 1989
• 6: 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]
• 7: CLARK, K.r. Negation as failure. In Logic and Data Bases, H. Gallaire and J. Minker, Eds. Plenum Press, New York, 1978, 293-322.
• 8: ERSHOV, A. P. Mixed computation potential applications and problems for study. Theor.{ Comput. Sci. 18. I (1982), 41-67.
• 9: FUJITA, H. An algorithm for partial evaluation with constraints. ICOT Tech. Memo. TM-0367, ICOT, Tokyo, Aug. 1987.
• 10: FUTAMURA, Y. Partialevaluationofcomputationprocess--Anapproachtoacompiler-compiler. Syst. Comput. Control 2, 5 (1971), 45-50.
• 11: FUTAMURA, Y. Program evaluation and generalized partial computation. In Proceedings of the International Conference on Fifth Generation Computer Systems (Tokyo, Nov. 1988). pp. 685-692.
• 12: GALLANGHER, J. Transforming logic programs by specializing interpreters. In Proceedings of ECAI 86 (Brighton Center, U.K., 1986). 109-122.
• 13: GHELFO, S., AND LEVl, G. A partial evaluator for metaprograms in a multiple theories logic language. In Proceedings 2nd National Conference on Logic Programming (Turin, May 1987). GULP, Pisa, 1987, 13-24. (In Italian).
• 14: Carlo Ghezzi , Dino Mandrioli , Antonio Tecchio, Program Simplification via Symbolic Interpretation, Proceedings of the Fifth Conference on Foundations of Software Technology and Theoretical Computer Science, p.116-128, December 16-18, 1985
• 15: Fosca Giannotti , Attilio Matteucci, Symbolic evaluation with structural recursive symbolic constants, Science of Computer Programming, v.9 n.2, p.161-177, October 1, 1987 [doi>10.1016/0167-6423(87)90031-1]
• 16: HARALDSSON, A. A program manipulation system based on partial evaluation. Stud. Sci. Technol., Ph.D. dissertation 14, Dept. Computer and Information Sciences, Link6ping Univ., Link6ping, Sweden, 1977.
• 17: C. J. Hogger, Derivation of Logic Programs, Journal of the ACM (JACM), v.28 n.2, p.372-392, April 1981 [doi>10.1145/322248.322258]
• 18: Christopher John Hogger, Introduction to logic programming, Academic Press Professional, Inc., San Diego, CA, 1984
• 19: Neil D. Jones , Peter Sestoft , Harald Sondergaard, An experiment in partial evaluation: the generation of a compiler generator, Proc. of the first international conference on Rewriting techniques and applications, p.124-140, December 1985, Dijon, France
• 20: H. Jan Komorowski, Partial evaluation as a means for inferencing data structures in an applicative language: a theory and implementation in the case of prolog, Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.255-267, January 25-27, 1982, Albuquerque, Mexico [doi>10.1145/582153.582181]
• 21: LEVI, G. Object level reflection of inference rules by partial evaluation (extended abstract). In Workshop on Meta-Level Architectures and Reflection (Sardinia, Italy, 1986). P. Maes and D. Nardi, Eds. Elsevier, Amsterdam, 1988, 313-327.
• 22: J. W. Lloyd, Foundations of logic programming, Springer-Verlag New York, Inc., New York, NY, 1984
• 23: LOGICWARE, INC. SZKI. MPROLOG Language Reference, Release 2.1. Logicware, Inc., Budapest, Sept. 1985.
• 24: MATSUMOTO, Y., TANAKA, H., HIRAKAWA, H., MIYOSHI, H., AND YASUKAWA, H. BUP: A Bottom-Up Parser embedded in Prolog. New Generation Comput. 1, 2 (1983), 145-158.
• 25: H. Partsch , R. Steinbrüggen, Program Transformation Systems, ACM Computing Surveys (CSUR), v.15 n.3, p.199-236, Sept. 1983 [doi>10.1145/356914.356917]
• 26: PETTOROSSI, A., AND PROIETTI, M. Decidability results and characterization of strategies for the development of logic programs. In Logic Programming, Proceedings of the 6th International Conference, G. Levi and M. Martelli, Eds. The MIT Press, Cambridge, Mass., 1989, pp. 539-553.
• 27: PROIETTI, M., AND PETTOROSSI, A. Techniques for the automatic improvement of logic programs. Tech. Rep. IASI-CNR R231, IASI-CNR, Rome, 1988.
• 28: SATO, T., AND TAMAKI, H. Transformational logic program synthesis. In Proceedings of the International Conference on Fifth Generation Computer Systems. 1984, pp. 195-201.
• 29: SEKI, H., AND FURUKAWA, $. Notes on transformation techniques for generate and test logic programs. In Proceedings of the Symposium on Logic Programming. 1987, pp. 215-223.
• 30: TAKEUCHI, A., AND FURUKAWA, K. Partial evaluation of Prolog programs and its application to metaprogramming. In Information Processing 86, H. J. Kugler, Ed. North-Holland, Dublin, 1986, pp. 415-420.
• 31: TAMAKI, H., AND SATO, T. A transformation system for logic programs which preserves equivalence. ICOT Tech. Rep. TR-018, ICOT, Tokyo, Aug. 1983.
• 32: TAMAKI, H., AND SATO, T. Unfold/fold transformation of logic programs. In Proceedings of the 2nd International Logic Programming Conference (Uppsala, Sweden, July 1984). S.-A. T~irnlund, Ed., Uppsala, Univ., 1984, pp. 127-138.
• 33: M. H. Van Emden , R. A. Kowalski, The Semantics of Predicate Logic as a Programming Language, Journal of the ACM (JACM), v.23 n.4, p.733-742, Oct. 1976 [doi>10.1145/321978.321991]
• 34: VIELLE, L. Recursion in deductive databases: A DB-complete proof procedure based on SLD- resolution. Tech. Rep. Kb-15, Munich, Nov. 1986.
• 35: ZANIOLO, C., AND SACCA, D. Implementation of recursive queries for a data language based on pure Horn logic. In Proceedings of the 4th International Conference on Logic Programming (Melbourne, May 1987). J.-L. Lasser, Ed. MIT Press, Cambridge, Mass., 1987, 104-135.

INDEX TERMS

Primary Classification:
  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.2 Automatic Programming
          Subjects: Program transformation

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Correctness proofs

  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.3 Deduction and Theorem Proving
          Subjects: Logic programming

General Terms:
Design, Languages, Verification