Abstract
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.
Chapter PDF
References
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.
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.
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.
R. Bryant. Symbolic Boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys, 24(3):293–318, 1992.
M. Codish. Efficient goal directed bottom-up evaluation of logic programs. Journal of Logic Programming, 38(3):354–370, 1999.
M. Codish. Worst-case groundness analysis using positive Boolean functions. Journal of Logic Programming, 41(1):125–128, 1999.
M. Codish and V. Lagoon. Type dependencies for logic programs using aciunification. Theoretical Computer Science, 2000.
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.
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.
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.
A. Cortesi, G. Filé, and W. Winsborough. The quotient of an abstract interpretation. Theoretical Computer Science, 202(1-2):163–192, 1998.
A. Cortesi, B. Le Charlier, and P. Van Hentenryck. Evaluation of the domain Prop. Journal of Logic Programming, 23(3):237–278, 1995.
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.
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.
P. W. Dart. On derived dependencies and connected databases. The Journal of Logic Programming, 11 (1 & 2):163–188, July 1991.
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.
S. Genaim, J.M. Howe, and M. Codish. Worst-case groundness analysis using definite boolean functions, September 2000.
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.
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.
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.
Taisuke Sato and Hisao Tamaki. Enumeration of success patterns in logic programs. Theoretical Computer Science, 34(1-2):227–240, November 1984.
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.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Genaim, S., Codish, M. (2001). The Def-inite Approach to Dependency Analysis. In: Sands, D. (eds) Programming Languages and Systems. ESOP 2001. Lecture Notes in Computer Science, vol 2028. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45309-1_28
Download citation
DOI: https://doi.org/10.1007/3-540-45309-1_28
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41862-7
Online ISBN: 978-3-540-45309-3
eBook Packages: Springer Book Archive