Online partial deduction of logic programs

ABSTRACT

Partial deduction systems must be guided by an unfolding strategy, telling them which atoms to unfold and when to stop unfolding. Online strategies exploit knowledge accumulated during the unfolding itself, for example in a goal stack, while offline strategies are fixed before unfolding begins. Online strategies are more powerful, but a major overhead for large programs is the analysis time spent on each atom, which increases as the knowledge grows. We describe an online strategy whose analysis time for each atom is independent of the amount of knowledge about that atom. This reduces transformation times for programs with large search spaces by an order of magnitude, while retaining the power of online analysis. Correctness, termination and nontriviality are shown.

REFERENCES

• Aug85: Lennart Augustsson, Compiling pattern matching, Proc. of a conference on Functional programming languages and computer architecture, p.368-381, January 1985, Nancy, France
• BD77: 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]
• Bir82: R. S. Bird, Tabulation Techniques for Recursive Programs, ACM Computing Surveys (CSUR), v.12 n.4, p.403-417, Dec. 1980 [doi>10.1145/356827.356831]
• Chi90: Wei-Ngan Chin. Automatic Methods }or Program Transformation. PhD thesis, Imperial College, University of London, March 1990.
• Chi92a: Wei-Ngan Chin, Safe fusion of functional expressions, Proceedings of the 1992 ACM conference on LISP and functional programming, p.11-20, June 22-24, 1992, San Francisco, California, United States
• Chi92b: Wei-Ngan Chin. Synthesizing parallel lemma. In Proc of a JSPS Seminar on Parallel Programming Systems, World Scientific Publishing, pages 201- 217, Tokyo, Japan, May 1992.
• Chi93: Wei-Ngan Chin. Safe fusion of functional expressions II: Further improvements. TR/DPSG 1, Dept of IS/CS, NUS, February 1993.
• Coh83: Norman H. Cohen, Eliminating Redundant Recursive Calls., ACM Transactions on Programming Languages and Systems (TOPLAS), v.5 n.3, p.265-299, July 1983 [doi>10.1145/2166.2167]
• Dar81: John Darlington. An experimental program transformation and synthesis system. Artificial Intelligence, 16:1-46, 1981.
• Har88: Peter G. Harrison, Linearisation: an optimisation for nonlinear functional programs, Science of Computer Programming, v.10 n.3, p.281-318, June 1988 [doi>10.1016/0167-6423(88)90052-4]
• Kno87: Hessam Knoshnevisan. Automatic Transformation Systems based on Function-Level Reasoning. PhD thesis, Imperial College, University of London, july 1987.
• Mic68: Donald Michie. Memo functions and machine learning. Nature, 218:19-22, 1968.
• Pet84: Alberto Pettorossi, A powerful strategy for deriving efficient programs by transformation, Proceedings of the 1984 ACM Symposium on LISP and functional programming, p.273-281, August 06-08, 1984, Austin, Texas, United States [doi>10.1145/800055.802044]
• Pip80: N Pippenger. Pebbling. Rc 8258 (# 35937), IBM Thomas J Watson Reserach Centre, May 1980.
• PP91: 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
• Wad87: P. Wadler, Views: a way for pattern matching to cohabit with data abstraction, Proceedings of the 14th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.307-313, January 21-23, 1987, Munich, West Germany [doi>10.1145/41625.41653]
• Wad88: Philip Wadler, Deforestation: transforming programs to eliminate trees, Proceedings of the Second European Symposium on Programming, p.231-248, January 1988, Nancy, France

INDEX TERMS

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

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS

General Terms:
Algorithms, Languages