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. Amtoft, T. 1992. Unfold/fold transformations preserving termination properties. In 4th International Symposium on Programming Language Implementation and Logic Programming (PLILP '92), Leuven, Belgium, M. Bruynooghe and M. Wirsing, Eds. LNCS, vol. 631. Springer-Verlag, Germany, 187--201.]]
2. Apt, K. and Kozen, D. 1986. Limits for automatic verification of finite-state systems. Information Processing Letters 15, 307--309.]]
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. Bensaou, N. and Guessarian, I. 1998. Transforming constraint logic programs. Theor. Comput. Sci. 206, 81--125.]]
5. Bossi, A. and Cocco, N. 1994. Preserving universal termination through unfold/fold. In International Conference on Algebraic and Logic Programming (ALP). LNCS, vol. 850. Springer Verlag, Germany, 269--286.]]
6. Bossi, A., Cocco, N., and Dulli, S. 1990. A method of specializing logic programs. ACM Trans. Prog. Lang. Syst. 12, 2, 253--302.]]
7. Bossi, A., Cocco, N., and Etalle, S. 1992. On safe folding. In International Symposium on Programming Language Implementation and Logic Programming (PLILP). LNCS, vol. 631. Springer Verlag, Germany, 172--186.]]
8. Bossi, A., Cocco, N., and Etalle, S. 1996. Simultaneous replacement in normal programs. J. Logic Computation 6, 1 (February), 79--120.]]
9. Boulanger, D. and Bruynooghe, M. 1993. Deriving unfold/fold transformations of logic programs using extended OLDT-based abstract interpretation. J. Symbol. Computation 15, 5/6, 495--521.]]
10. Boyer, R. and Moore, J. 1975. Proving theorems about Lisp functions. JACM 22, 1, 129--144.]]
11. Boyer, R. and Moore, J. 1990. A Theorem Prover for a Computational Logic. In International Conference on Automated Deduction (CADE). LNAI, vol. 449. Springer Verlag, Germany, 1--15.]]
12. Bundy, A. van Harmelen, F., Horn, C., Smaill, A. 1990. The oyster-clam system. In International Conference on Automated Deduction (CADE). LNAI, vol. 449. Springer Verlag, Germany, 647--648.]]
13. Burstall, R. and Darlington, J. 1977. A transformation system for developing recursive programs. JACM 24, 1, 44--67.]]
14. Chen, W. and Warren, D. 1996. Tabled evaluation with delaying for general logic programs. JACM 43, 1, 20--74.]]
15. Clarke, E., Grumberg, O., and Peled, D. 1999. Model Checking. MIT Press, Massachusetts.]]
16. Comon, H. and Nieuwenhuis, R. 2000. Induction=i-axiomatization + first-order consistency. Information and Computation 159, 1-2, 151--186.]]
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. Etalle, S. and Gabbrielli, M. 1996. Transformations of CLP modules. Theoretical Comput. Sci. 166, 1, 101--146.]]
20. Etalle, S., Gabrielli, M., and Meo, M. 2001. Transformations of CCP programs. ACM Trans. Prog. Lang. Syst. 23, 3, 304--395.]]
21. Francesco, N. D. and Santone, A. 1998. A transformation system for concurrent processes. Acta Informatica 35, 12, 1037--1073.]]
22. Gergatsoulis, M. and Katzouraki, M. 1994. Unfold/fold transformations for definite clause programs. In International Symposium on Programming Language Implementation and Logic Programming (PLILP). LNCS, vol. 844. Springer Verlag, Germany, 340--354.]]
23. Hsiang, J. and Srivas, M. 1987. Automatic inductive theorem proving using Prolog. Theoretical Comput. Sci. 54, 3--28.]]
24. Jones, N., Gomard, C., and Sestoft, P. 1993. Partial Evaluation and Automatic Program Generation. Prentice Hall.]]
25. Kanamori, T. and Fujita, H. 1986. Formulation of Induction Formulas in Verification of Prolog Programs. In International Conference on Automated Deduction (CADE). LNCS, vol. 230. Springer Verlag, Germany, 281--299.]]
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. Kawamura, T. and Kanamori, T. 1990. Preservation of stronger equivalence in unfold/fold logic program transformation. Theoretical Comput. Sci. 75, 1&2, 139--156.]]
28. Komorowski, J. 1982. Partial evaluation as a means for inferencing data structures in an applicative language: A theory and implementation in the case of prolog. In ACM SIGPLAN International Conference on Principles of Programming Languages (POPL). ACM, New York.]]
29. Kott, L. 1985. Unfold/fold program transformations. Algebraic Methods in Semantics. Cambridge University Press, UK, 412--433.]]
30. Lloyd, J. 1993. Foundations of Logic Programming, Second Edition. Springer-Verlag, Germany.]]
31. Maher, M. 1987. Correctness of a logic program transformation system. Tech. rep., IBM T.J. Watson Research Center.]]
32. Maher, M. J. 1993. A transformation system for deductive database modules with perfect model semantics. Theoretical Comput. Sci. 110, 377--403.]]
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. Pettorossi, A. and Proietti, M. 2000. Perfect model checking via unfold/fold transformations. In Computational Logic. LNCS, vol. 1861. Springer Verlag, Germany.]]
36. Pettorossi, A., Proietti, M., and Renault, S. 1997. Reducing nondeterminism while specializing logic programs. In ACM SIGPLAN International Conference on Principles of Programming Languages (POPL). ACM, New York, USA, 414--427.]]
37. Roychoudhury, A. 2000. Program transformations for verifying parameterized systems. Ph.D. thesis, State University of New York at Stony Brook, Available from http://www.comp.nus.edu.sg/∼abhik/papers.html.]]
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. Roychoudhury, A., Narayan Kumar, K., Ramakrishnan, C. R., Ramakrishnan, I. V., and Smolka, S. A. 2000. Verification of parameterized systems using logic program transformations. In International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS). LNCS, vol. 1785. Springer-Verlag, Germany, 172--187.]]
40. Roychoudhury, A. and Ramakrishnan, I. V. 2001. Automated inductive verification of parameterized protocols. In International Conference on Computer Aided Verification (CAV). LNCS, vol. 2102. Springer-Verlag, Germany, 25--37.]]
41. Sands, D. 1996. Total correctness by local improvement in the transformation of functional programs. ACM Trans. Prog. Lang. Syst. 18, 2, 175--234.]]
42. Sato, T. 1992. Equivalence-preserving first-order unfold/fold transformation systems. Theoretical Comput. Sci. 105, 57--84.]]
43. Seki, H. 1991. Unfold/fold transformation of stratified programs. Theoretical Comput. Sci. 86, 1, 107--139.]]
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. Tamaki, H. and Sato, T. 1986b. OLDT resolution with tabulation. In Third International Conference on Logic Programming. 84--98.]]

Index Terms

• Software and its engineering

  • Software notations and tools

    • General programming languages

      • Language types

        • Constraint and logic languages

• Theory of computation

  • Semantics and reasoning

    • Program semantics