Controlling generalization and polyvariance in partial deduction of normal logic programs

ABSTRACT

Given a program and some input data, partial deduction computes a specialized program handling any remaining input more efficiently. However, controlling the process well is a rather difficult problem. In this article, we elaborate global control for partial deduction: for which atoms, among possibly infinitely many, should specialized relations be produced, meanwhile guaranteeing correctness as well as termination? Our work is based on two ingredients. First, we use the concept of a characteristic tree, encapsulating specialization behavior rather than syntactic structure, to guide generalization and polyvariance, and we show how this can be done in a correct and elegant way. Second, we structure combinations of atoms and associated characteristic trees in global trees registering “causal” relationships among such pairs. This allows us to spot looming nontermination and perform proper generalization in order to avert the danger, without having to impose a depth bound on characteristic trees. The practical relevance and benefits of the work are illustrated through extensive experiments. Finally, a similar approach may improve upon current (on-line) control strategies for program transformation in general such as (positive) supercompilation of functional programs. It also seems valuable in the context of abstract interpretation to handle infinite domains of infinite height with more precision.

REFERENCES

• 1: Alfred V. Aho , Ravi Sethi , Jeffrey D. Ullman, Compilers: principles, techniques, and tools, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1986
• 2: M. Alpuente , M. Falaschi , P. Julián , G. Vidal, Specialization of lazy functional logic programs, Proceedings of the 1997 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, p.151-162, June 12-13, 1997, Amsterdam, The Netherlands
• 3: María Alpuente , Moreno Falaschi , Germán Vidal, Narrowing-Driven Partial Evaluation of Functional Logic Programs, Proceedings of the 6th European Symposium on Programming Languages and Systems, p.45-61, April 22-24, 1996
• 4: BENKERIMI, I~. AND HILL, P. M. 1993. Supporting transformations for the partial evaluation of logic programs. J. Logic Comput. 3, 5 (Oct.), 469-486.
• 5: Kerima Benkerimi , John W. Lloyd, A partial evaluation procedure for logic programs, Proceedings of the 1990 North American conference on Logic programming, p.343-358, January 1990, Austin, Texas, United States
• 6: BOL, R. 1993. Loop checking in partial deduction. J. Logic Progam. 16, 1-2, 25-46.
• 7: Annalisa Bossi , Nicoletta Cocco, Preserving Universal Termination through Unfold/Fold, Proceedings of the 4th International Conference on Algebraic and Logic Programming, p.269-286, September 14-16, 1994
• 8: A. Bossi , N. Cocco , S. Dulli, A method for specializing logic programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.12 n.2, p.253-302, April 1990 [doi>10.1145/78942.78947]
• 9: Annalisa Bossi , Nicoletta Cocco , Sandro Etalle, Transformation of Left Terminating Programs: the Reordering Problem, Proceedings of the 5th International Workshop on Logic Programming Synthesis and Transformation, p.33-45, September 20-22, 1995
• 10: Maurice Bruynooghe, A practical framework for the abstract interpretation of logic programs, Journal of Logic Programming, v.10 n.2, p.91-124, Feb. 1991 [doi>10.1016/0743-1066(91)80001-T]
• 11: BRUYNOOGHE, iV{., DE SCHREYE, D., AND MARTENS, B. 1992. A general criterion for avoiding infinite unfolding during partial deduction. New Gen. Comput. 11, 1, 47-79.
• 12: Maurice Bruynooghe , Michael Leuschel , Konstantinos F. Sagonas, A Polyvariant Binding-Time Analysis for Off-line Partial Deduction, Proceedings of the 7th European Symposium on Programming: Programming Languages and Systems, p.27-41, March 28-April 04, 1998
• 13: 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]
• 14: D. Chan , M. Wallace, A treatment of negation during partial evaluation, Meta-programming in logic programming, MIT Press, Cambridge, MA, 1989
• 15: Charles Consel , Olivier Danvy, Tutorial notes on partial evaluation, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.493-501, March 1993, Charleston, South Carolina, United States [doi>10.1145/158511.158707]
• 16: Patrick Cousot , Rahida Cousot, Abstract interpretation and application to logic programs, Journal of Logic Programming, v.13 n.2-3, p.103-179, July 1992 [doi>10.1016/0743-1066(92)90030-7]
• 17: DE SCHREYE, D., LEUSCHEL, ~/{., AND MARTENS, B. 1995. Tutorial on program specialisation (abstract). In Proceedings of ILPS'95, the International Logic Programming Symposium, J. W. Lloyd, Ed. MIT Press, Cambridge, Mass., 615-616.
• 18: DE WAAL, D. t. 1994. Analysis and transformation of proof procedures. Ph.D. thesis, Dept. of Computer Science, Univ. of Bristol, Bristol, U.K.
• 19: DE WAAL, D. t. AND GALLAGHER, J. 1991. Specialisation of a unification algorithm. In Logic Program Synthesis and Transformation. Proceedings of LOPSTR'91, T. Clement and K.-K. Lau, Eds. Workshops in Computing. Springer-Verlag, Berlin, 205-220.
• 20: D. Andre de Waal , John P. Gallagher, The Applicability of Logic Program Analysis and Transformation to Theorem Proving, Proceedings of the 12th International Conference on Automated Deduction, p.207-221, June 26-July 01, 1994
• 21: Saumya Debray, Resource-bounded partial evaluation, Proceedings of the 1997 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, p.179-192, June 12-13, 1997, Amsterdam, The Netherlands
• 22: Saumya K. Debray , Nai-Wei Lin, Cost analysis of logic programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.15 n.5, p.826-875, Nov. 1993 [doi>10.1145/161468.161472]
• 23: DEBRAY, S., LOPEZ GARCfA, P., HERMENEGILDO, iV{., AND LIN, N.-W. 1994. Estimating the computational cost of logic programs. In Proceedings of SAS'9Z, B. Le Charlier, Ed. Lecture Notes in Computer Science, vol. 864. Springer-Verlag, Berlin, 255-265.
• 24: 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]
• 25: Nachum Dershowitz , Jean-Pierre Jouannaud, Rewrite systems, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• 26: Yoshihiko Futamura , Kenroku Nogi , Akihiko Takano, Essence of generalized partial computation, Theoretical Computer Science, v.90 n.1, p.61-79, Nov. 1991 [doi>10.1016/0304-3975(91)90299-H]
• 27: GALLAGHER, J. 1991. A system for specialising logic programs. Tech. Rep. TR-91-32, Univ. of Bristol, Bristol, U.K.
• 28: J. P. Gallagher, Tutorial on specialisation of logic programs, Proceedings of the 1993 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, p.88-98, June 14-16, 1993, Copenhagen, Denmark [doi>10.1145/154630.154640]
• 29: GALLAGHER, J. AND BRUYNOOGHE, M. 1990. Some low-level transformations for logic programs. In Proceedings of the META '90 Workshop on Meta Programming in Logic, M. Bruynooghe, Ed. K.U. Leuven, Belgium, 229-244.
• 30: GALLAGHER, J. AND BRUYNOOGHE, M. 1991. The derivation of an algorithm for program specialisation. New Gen. Comput. 9, 3-4, 305-333.
• 31: GALLAGHER, J. AND DE WAAL, D. t. 1992. Deletion of redundant unary type predicates from logic programs. In Logic Program Synthesis and Transformation. Proceedings of LOPSTR'92, K.-K. Lau and T. Clement, Eds. Workshops in Computing. Springer-Verlag, Berlin, 151-167.
• 32: John P. Gallagher , Laura Lafave, Regular Approximation of Computation Paths in Logic and Functional Languages, Selected Papers from the Internaltional Seminar on Partial Evaluation, p.115-136, February 12-16, 1996
• 33: Robert Glück , Andrei V. Klimov, Occam's Razor in Metacompuation: the Notion of a Perfect Process Tree, Proceedings of the Third International Workshop on Static Analysis, p.112-123, September 22-24, 1993
• 34: Robert Glück , Morten Heine Sørensen, A Roadmap to Metacomputation by Supercompilation, Selected Papers from the Internaltional Seminar on Partial Evaluation, p.137-160, February 12-16, 1996
• 35: Robert Glück , Jesper Jørgensen , Bern Martens , Morten Heine Sørensen, Controlling Conjunctive Partial Deduction, Proceedings of the 8th International Symposium on Programming Languages: Implementations, Logics, and Programs, p.152-166, September 24-27, 1996
• 36: GURR, C. A. 1994. A self-applicable partial evaluator for the logic programming language GSdel. Ph.D. thesis, Dept. of Computer Science, Univ. of Bristol, Bristol, U.K.
• 37: GUSTEDT, J. 1992. Algorithmic aspects of ordered structures. Ph.D. thesis, Technische UniversitS~t Berlin, Berlin, Germany.
• 38: HEINTZE, N. 1992. Practical aspects of set based analysis. In Proceedings of the Joint International Conference and Symposium on Logic Programming. MIT Press, Cambridge, Mass., 765-779.
• 39: HIGMAN, G. 1952. Ordering by divisibility in abstract algebras. Proc. London Math. Soc. 2, 326-336.
• 40: HILL, P. AND GALLAGHER, J. 1994. Meta-programming in logic programming. Tech. Rep. 94.22, School of Computer Studies, Univ. of Leeds. To be published in Handbook of Logic in Artificial Intelligence and Logic Programming, Vol. 5. Oxford Science Publications, Oxford University Press.
• 41: John E. Hopcroft , Jeffrey D. Ullman, Introduction To Automata Theory, Languages, And Computation, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1990
• 42: HORVJtTH, T. 1993. Experiments in partial deduction. M.S. thesis, Departement Computerwetenschappen, K.U. Leuven, Belgium.
• 43: G. Janssens , M. Bruynooghe, Deriving descriptions of possible values of program variables by means of abstract interpretation, Journal of Logic Programming, v.13 n.2-3, p.205-258, July 1992 [doi>10.1016/0743-1066(92)90032-X]
• 44: Neil D. Jones , Carsten K. Gomard , Peter Sestoft, Partial evaluation and automatic program generation, Prentice-Hall, Inc., Upper Saddle River, NJ, 1993
• 45: Jesper Jørgensen , Michael Leuschel, Efficiently Generating Efficient Generating Extensions in Prolog, Selected Papers from the Internaltional Seminar on Partial Evaluation, p.238-262, February 12-16, 1996
• 46: Jesper Jørgensen , Michael Leuschel , Bern Martens, Conjunctive Partial Deduction in Practice, Proceedings of the 6th International Workshop on Logic Programming Synthesis and Transformation, p.59-82, August 28-30, 1996
• 47: KNUTH, D. E., MORRIS, J. H., AND PRATT, V. R. 1977. Fast pattern matching in strings. SIAM J. Comput. 6, 2, 323-350.
• 48: Henryk Jan Komorowski, An Introduction to Partial Deduction, Proceedings of the 3rd International Workshop on Meta-Programming in Logic, p.49-69, June 10-12, 1992
• 49: KRUSKAL, J. B. 1960. Well-quasi ordering, the tree theorem, and Vazsonyi's conjecture. Trans. Am. Math. Soc. 95, 210-225.
• 50: Laura Lafave , John P. Gallagher, Constraint-Based Partial Evaluation of Rewriting-Based Functional Logic Programs, Proceedings of the 7th International Workshop on Logic Programming Synthesis and Transformation, p.168-188, July 10-12, 1997
• 51: LAM, J. AND KUSALIK, t. 1990. A comparative analysis of partial deductors for pure Prolog. Tech. Rep. Dept. of Computational Science, Univ. of Saskatchewan, Canada. Revised April 1991.
• 52: J.-L. Lassez , M. J. Maher , K. Marriott, Unification revisited, Foundations of deductive databases and logic programming, Morgan Kaufmann Publishers Inc., San Francisco, CA, 1988
• 53: Michael Leuschel, Partial Evaluation of the "Real Thing", Proceedings of the 4th International Workshops on Logic Programming Synthesis and Transformation - Meta-Programming in Logic, p.122-137, June 20-21, 1994
• 54: Michael Leuschel, Ecological Partial Deduction: Preserving Characteristic Trees Without Constraints, Proceedings of the 5th International Workshop on Logic Programming Synthesis and Transformation, p.1-16, September 20-22, 1995
• 55: LEUSCHEL, M. 1996. The ECCE partial deduction system and the DPPD library of benchmarks. Obtainable via http://www.cs.kuleuven.ac.be/-lpai.
• 56: LEUSCHEL, M. 1997a. Advanced techniques for logic program speciMisation. Ph.D. thesis, K.U. Leuven. Accessible via http://www.cs.kuleuven.ac.be/-michael.
• 57: LEUSCHEL, M. 1997b. Extending homeomorphic embedding in the context of logic programming. In Proceedings of the 12th Workshop on Logic Programming (WLP'97), F.Bry, B. Freitag and D. Seipel, Eds. 92-103. Extended version as Tech. Rep. CW 252, K.U. Leuven, Belgium..
• 58: Michael Leuschel , Danny De Schreye, Towards creating specialised integrity checks through partial evaluation of meta-interpreters, Proceedings of the 1995 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, p.253-263, June 21-23, 1995, La Jolla, California, United States [doi>10.1145/215465.215598]
• 59: LEUSCHEL, M. AND DE SCHREYE, D. 1996a. Creating speciMised integrity checks through partial evaluation of meta-interpreters. Tech. Rep. CW 237, K.U. Leuven, Belgium. To appear in J. Logic Progam.
• 60: Michael Leuschel , Danny De Schreye, Logic Program Specialisation: How To Be More Specific, Proceedings of the 8th International Symposium on Programming Languages: Implementations, Logics, and Programs, p.137-151, September 24-27, 1996
• 61: Michael Leuschel , Danny De Schreye, Constrained partial deduction and the preservation of characteristic trees, New Generation Computing, v.16 n.3, p.283-342, 1998 [doi>10.1007/BF03037483]
• 62: Michael Leuschel , Bern Martens, Global Control for Partial Deduction through Characteristic Atoms and Global Trees, Selected Papers from the Internaltional Seminar on Partial Evaluation, p.263-283, February 12-16, 1996
• 63: Michael Leuschel , Morten Heine Sørensen, Redundant Argument Filtering of Logic Programs, Proceedings of the 6th International Workshop on Logic Programming Synthesis and Transformation, p.83-103, August 28-30, 1996
• 64: LEUSCHEL, M., DE SCHREYE, D., AND DE WAAL, A. 1996. A conceptual embedding of folding into partial deduction: Towards a maximal integration. In Proceedings of the Joint International Conference and Symposium on Logic Programming JICSLP'96, M. Maher, Ed. MIT Press, Cambridge, Mass., 319-332. Extended version as Tech. Rep. CW 225, K.U. Leuven.
• 65: J. W. Lloyd, Foundations of logic programming; (2nd extended ed.), Springer-Verlag New York, Inc., New York, NY, 1987
• 66: J. W. Lloyd , J. C. Shepherdson, Partial evaluation in logic programming, Journal of Logic Programming, v.11 n.3-4, p.217-242, Oct./Nov. 1991 [doi>10.1016/0743-1066(91)90027-M]
• 67: MARLET, R. 1994. Vers une formalisation de l'tS~valuation partielle. Ph.D. thesis, Universit6 de Nice-Sophia Antipolis.
• 68: MARTENS, B. 1994. On the semantics of meta-programming and the control of partial deduction in logic programming. Ph.D. thesis, K.U. Leuven.
• 69: MARTENS, B. AND DE SCHREYE, D. 1996. Automatic finite unfolding using well-founded measures. J. Logic Progam. 28, 2 (August), 89-146.
• 70: B. Martens , J. Gallagher, Ensuring Global Termination of Partial Deduction while Allowing Flexible Polyvariance, University of Bristol, Bristol, UK, 1995
• 71: Bern Martens , Danny De Schreye , Tamás Horváth, Sound and complete partial deduction with unfolding based on well-founded measures, Theoretical Computer Science, v.122 n.1-2, p.97-117, Jan. 3, 1994
• 72: MEULEMANS, D. 1995. Parti~le deductie: Een substanti~le vergelijkende studie. M.S. thesis, Departement Computerwetenschappen, K.U. Leuven, Belgium.
• 73: MOGENSEN, T. AND BONDORF, A. 1992. Logimix: A self-applicable partial evaluator for Prolog. In Logic Program Synthesis and Transformation. Proceedings of LOPSTR'92, K.-K. Lau and T. Clement, Eds. Workshops in Computing. Springer-Verlag, Berlin, 214-227.
• 74: PETTOROSSI, A. AND PROIETTI, M. 1994. Transformation of logic programs: Foundations and techniques. J. Logic Progam. 19-20, 261-320.
• 75: David L Poole , Randy Goebel, Gracefully adding negation and disjunction to Prolog, Proceedings on Third international conference on logic programming, p.635-641, September 1986, London, United Kingdom
• 76: PRESTWICH, S. 1992a. The PADDY partial deduction system. Tech. Rep. ECRC-92-6, ECRC, Munich, Germany.
• 77: PRESTWICH, S. 1992b. An unfold rule for full Prolog. In Logic Program Synthesis and Transformation. Proceedings of LOPSTR'92, K.-K. Lau and T. Clement, Eds. Workshops in Computing. Springer-Verlag, Berlin, 199-213.
• 78: Steven Prestwich, Online partial deduction of logic programs, Proceedings of the 1993 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, p.111-118, June 14-16, 1993, Copenhagen, Denmark [doi>10.1145/154630.154642]
• 79: Maurizio Proietti , Alberto Pettorossi, Semantics preserving transformation rules for Prolog, ACM SIGPLAN Notices, v.26 n.9, p.274-284, Sept. 1991
• 80: Maurizio Proietti , Alberto Pettorossi, Unfolding-definition-folding, in this order, for avoiding unnecessary variables in logic programs, Selected papers of the symposium on Programming language implementation and logic programming, p.89-124, May 1995, Passau, Germany
• 81: Germán Puebla , Manuel Hermenegildo, Implementation of multiple specialization in logic programs, Proceedings of the 1995 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, p.77-87, June 21-23, 1995, La Jolla, California, United States [doi>10.1145/215465.215561]
• 82: SAHLIN, D. 1991. An automatic partial evaluator for full Prolog. Ph.D. thesis, Swedish Institute of Computer Science.
• 83: Dan Sahlin, Mixtus: an automatic partial evaluator for full Prolog, New Generation Computing, v.12 n.1, p.7-51, 1993 [doi>10.1007/BF03038271]
• 84: Donald A. Smith, Partial evaluation of pattern matching in constraint logic programming languages, ACM SIGPLAN Notices, v.26 n.9, p.62-71, Sept. 1991
• 85: Donald A. Smith , Timothy J. Hickey, Partial evaluation of a CLP language, Proceedings of the 1990 North American conference on Logic programming, p.119-138, January 1990, Austin, Texas, United States
• 86: SORENSEN, M. H. AND GLUCK, R. 1995. An algorithm of generalization in positive supercompilation. In Proceedings of ILPS'95, the International Logic Programming Symposium, J. W. Lloyd, Ed. MIT Press, Cambridge, Mass., 465-479.
• 87: Michael Sperber, Self-Applicable Online Partial Evaluation, Selected Papers from the Internaltional Seminar on Partial Evaluation, p.465-480, February 12-16, 1996
• 88: Jonathan Stillman, Computational problems in equational theorem proving, 1989
• 89: Valentin F. Turchin, The concept of a supercompiler, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.3, p.292-325, July 1986 [doi>10.1145/5956.5957]
• 90: TURCHIN, V. F. 1988. The algorithm of generalization in the supercompiler. In Partial Evaluation and Mixed Computation, D. BjCrner, A. P. Ershov, and N. D. Jones, Eds. North-Holland, 531- 549.
• 91: Wim Vanhoof , Bern Martens, To Parse or Not To Parse, Proceedings of the 7th International Workshop on Logic Programming Synthesis and Transformation, p.322-342, July 10-12, 1997
• 92: Philip Wadler, Deforestation: transforming programs to eliminate trees, Theoretical Computer Science, v.73 n.2, p.231-248, June 22, 1990
• 93: Daniel Weise , Roland Conybeare , Erik Ruf , Scott Seligman, Automatic online partial evaluation, Proceedings of the 5th ACM conference on Functional programming languages and computer architecture, p.165-191, June 1991, Cambridge, Massachusetts, United States
• 94: Will Winsborough, Multiple specialization using minimal-function graph semantics, Journal of Logic Programming, v.13 n.2-3, p.259-290, July 1992 [doi>10.1016/0743-1066(92)90033-Y]

INDEX TERMS

Primary Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES

Additional Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
  D.3 PROGRAMMING LANGUAGES
      D.3.4 Processors
          Subjects: Optimization

  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Logic and constraint programming

  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.2 Automatic Programming
          Subjects: Program transformation
      I.2.3 Deduction and Theorem Proving
          Subjects: Logic programming

General Terms:
Algorithms, Languages, Performance, Theory

Keywords:
flow analysis, partial deduction, partial evaluation, program transformation, supercompilation