The Def-inite Approach to Dependency Analysis

  • Samir Genaim
  • Michael Codish
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2028)


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.


Normal Form Boolean Function Logic Program Dependency Analysis Incidence Structure 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    T. Armstrong, K. Marriott, P. Schachte, and H. Søndergaard. Two classes of Boolean functions for dependency analysis. Science of Computer Programming, 31(1):3–45, 1998.zbMATHCrossRefMathSciNetGoogle Scholar
  2. 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. 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
  4. 4.
    R. Bryant. Symbolic Boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys, 24(3):293–318, 1992.CrossRefGoogle Scholar
  5. 5.
    M. Codish. Efficient goal directed bottom-up evaluation of logic programs. Journal of Logic Programming, 38(3):354–370, 1999.CrossRefMathSciNetGoogle Scholar
  6. 6.
    M. Codish. Worst-case groundness analysis using positive Boolean functions. Journal of Logic Programming, 41(1):125–128, 1999.zbMATHCrossRefMathSciNetGoogle Scholar
  7. 7.
    M. Codish and V. Lagoon. Type dependencies for logic programs using aciunification. Theoretical Computer Science, 2000.Google Scholar
  8. 8.
    M. Codish, V. Lagoon, and Bueno F. An algebraic approach to sharing analysis of logic programs. Journal of Logic Programming, 41(2):110–149, 2000.MathSciNetGoogle Scholar
  9. 9.
    M. Codish and H. Søndergaard. The Boolean logic of set sharing analysis. In C. Palamidessi, H. Glaser, and K. Meinke, editors, Principles of Declarative Programming, volume 1490 of LNCS, pages 89–101, Berlin, 1998. Springer.CrossRefGoogle Scholar
  10. 10.
    M. Codish, H. Søndergaard, and P. J. Stuckey. Sharing and groundness dependencies in logic programs. ACM Transactions on Programming Languages and Systems, 21(5):948–976, 1999.CrossRefGoogle Scholar
  11. 11.
    A. Cortesi, G. Filé, and W. Winsborough. The quotient of an abstract interpretation. Theoretical Computer Science, 202(1-2):163–192, 1998.zbMATHCrossRefMathSciNetGoogle Scholar
  12. 12.
    A. Cortesi, B. Le Charlier, and P. Van Hentenryck. Evaluation of the domain Prop. Journal of Logic Programming, 23(3):237–278, 1995.zbMATHCrossRefMathSciNetGoogle Scholar
  13. 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. 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. 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. 16.
    S. Genaim and M. Codish. The Def-inite Approach to Dependency Analysis. Technical report, Computer Science, Ben-Gurion University, 2000.
  17. 17.
    S. Genaim, J.M. Howe, and M. Codish. Worst-case groundness analysis using definite boolean functions, September 2000.Google Scholar
  18. 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. 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. 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
  21. 21.
    Taisuke Sato and Hisao Tamaki. Enumeration of success patterns in logic programs. Theoretical Computer Science, 34(1-2):227–240, November 1984.zbMATHCrossRefMathSciNetGoogle Scholar
  22. 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

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Samir Genaim
    • 1
  • Michael Codish
    • 1
  1. 1.The Department of Computer ScienceBen-Gurion University of the NegevBeer-ShevaIsrael

Personalised recommendations