An unfold/fold transformation framework for definite logic programs

ABSTRACT

Given a logic program P, an unfold/fold program transformation system derives a sequence of programs P = P₀, P₁, …, P_n, such that P_i+1 is derived from P_i by application of either an unfolding or a folding step. Unfold/fold transformations have been widely used for improving program efficiency and for reasoning about programs. Unfolding corresponds to a resolution step and hence is semantics-preserving. Folding, which replaces an occurrence of the right hand side of a clause with its head, may on the other hand produce a semantically different program. Existing unfold/fold transformation systems for logic programs restrict the application of folding by placing (usually syntactic) conditions that are sufficient to guarantee the correctness of folding. These restrictions are often too strong, especially when the transformations are used for reasoning about programs. In this article we develop a transformation system (called SCOUT) for definite logic programs that is provably more powerful (in terms of transformation sequences allowed) than existing transformation systems. This extra power is needed for a novel use of logic program transformations: for the verification of a specific class of concurrent systems, called parameterized concurrent systems.Our transformation system is constructed by developing a framework, which is parameterized by a "measure space" and associated measure functions. This framework places no syntactic restriction on the application of folding, and it can be used to derive transformation systems (by fixing the measure space and functions). The power of the system is determined by the choice of the measure space and functions; thus the relative power of different transformation systems can be compared by considering their measure spaces and functions. The correctness of these transformation systems follows from the correctness of the framework. We show that various existing transformation systems can be obtained as instances of our framework. We extend the unfold/fold transformation framework with a goal replacement transformation that allows semantically equivalent conjunctions of atoms to be interchanged. We then derive a new transformation system SCOUT as an instance of the framework and show its power relative to the existing transformation systems. SCOUT has been used to inductively prove temporal properties of parameterized concurrent systems (infinite families of finite state concurrent systems). We demonstrate the use of the additional power of SCOUT in constructing such induction proofs.

REFERENCES

• 1: Torben Amtoft, Unfold/fold Transformations Preserving Termination Properties, Proceedings of the 4th International Symposium on Programming Language Implementation and Logic Programming, p.187-201, August 26-28, 1992
• 2: K R Apt , D C Kozen, Limits for automatic verification of finite-state concurrent systems, Information Processing Letters, v.22 n.6, p.307-309, May 30,1986 [doi>10.1016/0020-0190(86)90071-2 ]
• 3: Aravindan, C. and Dung, P. 1995. On the correctness of unfold/fold transformations of normal and extended logic programs. J. Logic Prog. 24, 3, 295--322.
• 4: N. Bensaou , I. Guessarian, Transforming constraint logic programs, Theoretical Computer Science, v.206 n.1-2, p.81-125, Oct. 6, 1998 [doi>10.1016/S0304-3975(97)00077-7 ]
• 5: 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
• 6: 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]
• 7: Annalisa Bossi , Nicoletta Cocco , Sandro Etalle, On Safe Folding, Proceedings of the 4th International Symposium on Programming Language Implementation and Logic Programming, p.172-186, August 26-28, 1992
• 8: Bossi, A., Cocco, N., and Etalle, S. 1996. Simultaneous replacement in normal programs. J. Logic Computation 6, 1 (February), 79--120.
• 9: Dmitri Boulanger , Maurice Bruynooghe, Deriving fold/unfold transformations of logic programs using extended OLDT-based abstract interpretation, Journal of Symbolic Computation, v.15 n.5-6, p.495-521, May/June 1993 [doi>10.1016/S0747-7171(06)80003-9]
• 10: Robert S. Boyer , J. Strother Moore, Proving Theorems about LISP Functions, Journal of the ACM (JACM), v.22 n.1, p.129-144, Jan. 1975 [doi>10.1145/321864.321875]
• 11: Robert S. Boyer , J. Strother Moore, A Theorem Prover for a Computational Logic, Proceedings of the 10th International Conference on Automated Deduction, p.1-15, July 24-27, 1990
• 12: Alan Bundy , Frank van Harmelen , Christian Horn , Alan Smaill, The Oyster-Clam System, Proceedings of the 10th International Conference on Automated Deduction, p.647-648, July 24-27, 1990
• 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: Weidong Chen , David S. Warren, Tabled evaluation with delaying for general logic programs, Journal of the ACM (JACM), v.43 n.1, p.20-74, Jan. 1996 [doi>10.1145/227595.227597]
• 15: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 16: Hubert Comon , Robert Nieuwenhuis, Induction = I-axiomatization + first-order consistency, Information and Computation, v.159 n.1-2, p.151-186, May 25/June 25 2000 [doi>10.1006/inco.2000.2875 ]
• 17: Das, S. K. 1992. Deductive Databases and Logic Programming. Addison-Wesley, Boston, USA.
• 18: De Schreye, D., Gluck, R., Jorgensen, J., Leuschel, M., Martens, B., and Sorensen, M. 1999. Conjunctive partial deduction: Foundations, control, algorithms, and experiments. J. Logic Prog. 41, 233--277.
• 19: Sandro Etalle , Maurizio Gabbrielli, Transformations of CLP modules, Theoretical Computer Science, v.166 n.1-2, p.101-146, Oct. 20, 1996 [doi>10.1016/0304-3975(95)00148-4 ]
• 20: Sandro Etalle , Maurizio Gabbrielli , Maria Chiara Meo, Transformations of CCP programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.23 n.3, p.304-395, May 2001 [doi>10.1145/503502.503504]
• 21: Francesco, N. D. and Santone, A. 1998. A transformation system for concurrent processes. Acta Informatica 35, 12, 1037--1073.
• 22: Manolis Gergatsoulis , Maria Katzouraki, Unfold/Fold Transformations For Definite Clause Programs, Proceedings of the 6th International Symposium on Programming Language Implementation and Logic Programming, p.340-354, September 14-16, 1994
• 23: J. Hsiang , Mandayam Srivas, Automatic inductive theorem proving using PROLOG, Theoretical Computer Science, v.54 n.1, p.3-28, 1987 [doi>10.1016/0304-3975(87)90016-8 ]
• 24: Neil D. Jones , Carsten K. Gomard , Peter Sestoft, Partial evaluation and automatic program generation, Prentice-Hall, Inc., Upper Saddle River, NJ, 1993
• 25: Tadashi Kanamori , Hiroshi Fujita, Formulation of Induction Formulas in Verification of Prolog Programs, Proceedings of the 8th International Conference on Automated Deduction, p.281-299, July 27-August 01, 1986
• 26: Kanamori, T. and Fujita, H. 1987. Unfold/fold transformation of logic programs with counters. In USA-Japan Seminar on Logics of Programs, Also available as ICOT Technical Report.
• 27: T. Kawamura , T. Kanamori, Preservation of stronger equivalence in unfold/fold logic program transformation, Theoretical Computer Science, v.75 n.1-2, p.139-156, Sep. 1990 [doi>10.1016/0304-3975(90)90065-P ]
• 28: 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]
• 29: L Kott, Unfold/fold program transformations, Algebraic methods in semantics, Cambridge University Press, New York, NY, 1986
• 30: John Wylie Lloyd, Foundations of Logic Programming, Springer-Verlag New York, Inc., Secaucus, NJ, 1993
• 31: Maher, M. 1987. Correctness of a logic program transformation system. Tech. rep., IBM T.J. Watson Research Center.
• 32: Michael J. Maher, A transformation system for deductive database modules with perfect model semantics, Theoretical Computer Science, v.110 n.2, p.377-403, March 29, 1993 [doi>10.1016/0304-3975(93)90013-J ]
• 33: Pettorossi, A. and Proietti, M. 1998. Transformation of logic programs. Handbook of Logic in Artificial Intelligence, vol. 5. Oxford University Press, UK, 697--787.
• 34: Pettorossi, A. and Proietti, M. 1999. Synthesis and transformation of logic programs using unfold/fold proofs. J. Logic Prog. 41, 2--3, 197--230.
• 35: Alberto Pettorossi , Maurizio Proietti, Perfect Model Checking via Unfold/Fold Transformations, Proceedings of the First International Conference on Computational Logic, p.613-628, July 01, 2000
• 36: Alberto Pettorossi , Maurizio Proietti , Sophie Renault, Reducing nondeterminism while specializing logic programs, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.414-427, January 15-17, 1997, Paris, France [doi>10.1145/263699.263759]
• 37: Abhik Roychoudhury , I. V. Ramakrishnan, Program transformations for verifying parameterized systems, 2000
• 38: Roychoudhury, A., Narayan Kumar, K., Ramakrishnan, C. R., and Ramakrishnan, I. V. 2002. Beyond Tamaki-Sato style unfold/fold transformations for normal logic programs. Int. J. Found. Comput. Sci. 13, 3, 387--403.
• 39: Abhik Roychoudhury , K. Narayan Kumar , C. R. Ramakrishnan , I. V. Ramakrishnan , Scott A. Smolka, Verification of Parameterized Systems Using Logic Program Transformations, Proceedings of the 6th International Conference on Tools and Algorithms for Construction and Analysis of Systems: Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS 2000, p.172-187, March 25-April 02, 2000
• 40: Abhik Roychoudhury , I. V. Ramakrishnan, Automated Inductive Verification of Parameterized Protocols, Proceedings of the 13th International Conference on Computer Aided Verification, p.25-37, July 18-22, 2001
• 41: David Sands, Total correctness by local improvement in the transformation of functional programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.18 n.2, p.175-234, March 1996 [doi>10.1145/227699.227716]
• 42: Taisuke Sato, Equivalence-preserving first-order unfold/fold transformation systems, Theoretical Computer Science, v.105 n.1, p.57-84, Oct. 26, 1992 [doi>10.1016/0304-3975(92)90287-P ]
• 43: Hiroshisa Seki, Unfold/fold transformation of stratified programs, Theoretical Computer Science, v.86 n.1, p.107-139, Aug. 18, 1991 [doi>10.1016/0304-3975(91)90007-O]
• 44: Seki, H. 1993. Unfold/fold transformation of general logic programs for well-founded semantics. J. Logic Prog. 16, 1, 5--23.
• 45: Tamaki, H. and Sato, T. 1984. Unfold/fold transformations of logic programs. In Proceedings of International Conference on Logic Programming. 127--138.
• 46: Tamaki, H. and Sato, T. 1986a. A generalized correctness proof of the unfold/ fold logic program transformation. Tech. rep., Ibaraki University, Japan.
• 47: Hisao Tamaki , Taisuke Sato, OLD resolution with tabulation, Proceedings on Third international conference on logic programming, p.84-98, September 1986, London, United Kingdom

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications
          Subjects: Constraint and logic languages

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages

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

General Terms:
Languages, Theory, Verification

Keywords:
Logic programming, folding, inductive theorem proving, program transformation, unfolding