The Def-inite Approach to Dependency Analysis
We propose a new representation for the domain of Definite Boolean functions. The key idea is to view the set of models of a Boolean function as an incidence relation between variables and models. This enables two dual representations: the usual one, in terms of models, specifying which variables they contain; and the other in terms of variables, specifying which models contain them. We adopt the dual representation which provides a clean theoretical basis for the definition of efficient operations on Def in terms of classic ACI1 unification theory. Our approach illustrates in an interesting way the relation of Def to the well-known set-Sharing domain which can also be represented in terms of sets of models and ACI1 unification. From the practical side, a prototype implementation provides promising results which indicate that this representation supports efficient groundness analysis using Def formula. Moreover, widening on this representation is easily defined.
KeywordsNormal Form Boolean Function Logic Program Dependency Analysis Incidence Structure
- 2.F. Baader and J. Siekmann. Unification theory. In D. Gabbay, C. Hogger, and J. Robinson, editors, Handbook of Logic in Artificial Intelligence and Logic Programming, volume 2, pages 41–126. Oxford Science Publications, 1994.Google Scholar
- 3.R. Bagnara and P. Schachte. Factorizing equivalent variable pairs in ROBDD-based implementations of Pos. In A. M. Haeberer, editor, AMAST’98, volume 1548 of LNCS, pages 471–485, Amazonia, Brazil, 1999. Springer-Verlag, Berlin.Google Scholar
- 7.M. Codish and V. Lagoon. Type dependencies for logic programs using aciunification. Theoretical Computer Science, 2000.Google Scholar
- 13.P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the Fourth ACM Symposium on Principles of Programming Languages, pages 238–252, January 1977.Google Scholar
- 14.P. Cousot and R. Cousot. Comparing the Galois connection and widening/narrowing approaches to abstract interpretation. Number 631 in LNCS, pages 269–295, Leuven, Belgium, 1992. Springer-Verlag, Berlin.Google Scholar
- 15.P. W. Dart. On derived dependencies and connected databases. The Journal of Logic Programming, 11 (1 & 2):163–188, July 1991.Google Scholar
- 16.S. Genaim and M. Codish. The Def-inite Approach to Dependency Analysis. Technical report, Computer Science, Ben-Gurion University, 2000. http://www.cs.bgu.ac.il/~mcodish/Papers/ppapers.html.
- 17.S. Genaim, J.M. Howe, and M. Codish. Worst-case groundness analysis using definite boolean functions, September 2000.Google Scholar
- 18.A. Heaton, M. Abo-Zaed, M. Codish, and A. King. A Simple Polynomial Groundness Analysis for Logic Programs. Journal of Logic Programming, 45:143–156.Google Scholar
- 19.J. M. Howe and A. King. Implementing groundness analysis with definite Boolean functions. In G. Smolka, editor, ESOP, volume 1782 of Lecture Notes in Computer Science. Springer-Verlag, March 2000.Google Scholar
- 20.A. King, J. G. Smaus, and P. Hill. Quotienting share for dependency analysis. In Doaitse Swierstra, editor, ESOP, volume 1576 of LNCS, pages 59–73. Springer-Verlag, April 1999.Google Scholar
- 22.J. Wunderwald. Memoing evaluation by source-to-source transformation. In Maurizio Proietti, editor, Proceedings of the Fifth International Workshop on Logic Program Synthesis and Transformation, volume 1048 of LNCS, pages 17–32. Springer.Google Scholar