Skip to main content
SpringerLink
Log in
Book cover

Computer Science Today pp 406–425Cite as

Abstracting unification: A key step in the design of logic program analyses

  • Chapter
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1000))

Abstract

This paper focuses on one of the key steps in the design of semantic based analyses for logic programs — the definition of an abstract unification algorithm for a given notion of data description. We survey some of the major notions of data descriptions proposed in the context of mode and sharing analyses. We demonstrate how a careful and systematic analysis of the underlying concrete unification algorithm contributes to the design of the abstract algorithm. Several relevant properties of concrete substitutions which influence the design of abstract domains and algorithms are described. We make use of a novel representation called abstract equation systems to uniformly represent a a wide range of data descriptions for such analyses proposed in the literature.

This is a preview of subscription content, log in via an institution.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. S. Abramsky and C. Hankin (Eds.). Abstract Interpretation of Declarative Languages. Ellis Horwood Series in Computers and their Applications. Ellis Horwood, Chichester, 1987.

    Google Scholar 

  2. K. R. Apt. Logic programming. In J. van Leeuwen (Ed.), Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, pp. 493–574. Elsevier Science Publ., Amsterdam, 1990.

    Google Scholar 

  3. K. R. Apt and A. Pellegrini. On the occur-check-free Prolog programs. ACM Trans. Prog. Lang. Syst., 16(3):687–726, 1994.

    Article  Google Scholar 

  4. T. Armstrong, K. Marriott, P. Schachte, and H. SØndergaard. Boolean functions for dependency analysis: Algebraic properties and efficient representation. In B. Le Charlier (Ed.), Static Analysis, Proc. 1st Int. Symposium (SAS'94), Lecture Notes in Computer Science, Vol. 864, Springer-Verlag, 1994, pp. 266–280.

    Google Scholar 

  5. R. Barbuti, R. Giacobazzi, and G. Levi. A general framework for semantics-based bottom-up abstract interpretation of logic programs. ACM Trans. Prog. Lang. Syst., 15(1):133–181, Jan. 1993.

    Article  Google Scholar 

  6. M. Bruynooghe. A practical framework for the abstract interpretation of logic programs. The Journal of Logic Programming, 10(2):91–124, 1991.

    Article  Google Scholar 

  7. M. Bruynooghe and M. Codish. Freeness, sharing, linearity and correctness — all at once. In P. Cousot, M. Falaschi, G. Filè, and A. Rauzy (Eds.), Static Analysis, Proc. Third Int. Workshop, Lecture Notes in Computer Science, Vol. 724, Springer-Verlag, 1993, pp. 153–164.

    Google Scholar 

  8. M. Codish, D. Dams, G. Filé, and M. Bruynooghe. Freeness analysis for logic programs — and correctness? In D. S. Warren (Ed.), Proc. Tenth International Conference on Logic Programming, pp. 116–131, Budapest, Hungary, 1993. The MIT Press, Cambridge MA. Revised version to appear in J. of Logic Programming.

    Google Scholar 

  9. M. Codish, D. Dams, and E. Yardeni. Derivation and safety of an abstract unification algorithm for groundness and aliasing analysis. In K. Furukawa (Ed.), Proc. Eighth International Conference on Logic Programming, pp. 79–93, Paris, France, 1991. The MIT Press, Cambridge MA.

    Google Scholar 

  10. M. Codish, D. Dams, and E. Yardeni. Bottom-up abstract interpretation of logic programs. Theoretical Computer Science, 124(1):93–126, Feb. 1994.

    Article  Google Scholar 

  11. M. Codish and B. Demoen. Analysing logic programs using “prop”-ositional logic programs and a magic wand. The Journal of Logic Programming. (to appear).

    Google Scholar 

  12. M. Codish, M. Falaschi, and K. Marriott. Suspension analysis for concurrent logic programs. ACM Trans. Prog. Lang. Syst., 16(3):649–686, May 1994.

    Article  Google Scholar 

  13. M. Codish, A. Mulkers, M. Bruynooghe, M. García de la Banda, and M. Hermenegildo. Improving abstract interpretations by combining domains. In Proc. ACM-SIGPLAN Symp. on Partial Evaluation and Semantics-Based Program Manipulation (PEPM'93), pp. 1942–205, Copenhagen, June 1993. Revised version to appear in ACM Trans. Prog. Lang. Syst.

    Google Scholar 

  14. A. Cortesi and G. Filé. Abstract interpretation of logic programs: An abstract domain for groundness, sharing, freeness and compoundness analysis. In P. Hudak and N. D. Jones (ed.), Proc. ACM-SIGPLAN Symp. on Partial Evaluation and Semantics-Based Program Manipulation, pp. 52–61, 1991.

    Google Scholar 

  15. A. Cortesi, G. Filé, and W. Winsborough. Comparison of abstract interpretations. In: W. Kuich (Ed.), Automata, Languages and Programming, Proc. 19th Int. Colloquium (ICALP'92), Lecture Notes in Computer Science, Vol. 623, Springer-Verlag, 1992, pp. 521–532.

    Google Scholar 

  16. A. Cortesi, B. Le Charlier, and P. Van Hentenryck. Combinations of abstract domains for logic programming. In Proc. 21st ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages (POPL'94), pp. 227–239, Portland, Oregon, 1994. ACM Press.

    Google Scholar 

  17. P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proc. 4th ACM Symposium on Principles of Programming Languages, pp. 238–252, Los Angeles, 1977.

    Google Scholar 

  18. P. Cousot and R. Cousot. Abstract interpretation and application to logic programs. The Journal of Logic Programming, 13(2 and 3):103–179, 1992.

    Article  Google Scholar 

  19. S. K. Debray. Static inference of modes and data dependencies in logic programs. ACM Trans. Prog. Lang. Syst., 11(3):418–450, 1989.

    Article  Google Scholar 

  20. T. W. Getzinger. The costs and benefits of abstract interpretation-driven Prolog optimization. In B. Le Charlier (Ed.), Static Analysis, Proc. 1st Int. Symposium (SAS'94), Lecture Notes in Computer Science, Vol. 864, Springer-Verlag, 1994, pp. 1–25.

    Google Scholar 

  21. M. V. Hermenegildo and F. Rossi. Strict and non-strict independent AND-parallelism in logic programs: Correctness, efficiency, and compile-time conditions. The Journal of Logic Programming, 22(1):1–45, Jan. 1995.

    Article  Google Scholar 

  22. D. Jacobs and A. Langen. Accurate and efficient approximation of variable aliasing in logic programs. In E. L. Lusk and R. A. Overbeek (Eds.), Proc. North American Conference on Logic Programming, pp. 154–165, Cleveland, Ohio, USA, 1989.

    Google Scholar 

  23. D. Jacobs and A. Langen. Static analysis of logic programs for independent AND-parallelism. The Journal of Logic Programming, 13(2 & 3):291–314, 1992.

    Article  Google Scholar 

  24. N. D. Jones and H. SØndergaard. A semantic-based framework for the abstract interpretation of Prolog. In Abramsky and Hankin [1], pp. 123–142.

    Google Scholar 

  25. A. King. A synergistic analysis for sharing and groundness which traces linearity. In D. Sannella (Ed.), Programming Languages and Systems, Proc. Fifth European Symposium (ESOP '94), Lecture Notes in Computer Science, Vol. 788, Springer-Verlag, 1994, pp. 363–378.

    Google Scholar 

  26. A. King and P. Soper. Depth-k sharing and freeness. In P. Van Hentenryck (Ed.), Proc. 11th International Conference on Logic Programming, pp. 553–568, Santa Margherita Ligure, Italy, 1994.

    Google Scholar 

  27. A. Langen. Advanced Techniques for Approximating Variable Aliasing in Logic Programs. Ph. D. thesis, University of Southern California, Mar. 1991.

    Google Scholar 

  28. J.-L. Lassez, M. J. Maher, and K. Marriott. Unification revisited. In J. Minker (Ed.), Foundations of Deductive Databases and Logic Programming, pp. 587–625. Morgan Kaufmann Publishers Inc., Los Altos, 1988.

    Google Scholar 

  29. B. Le Charlier and P. Van Hentenryck. Reexecution in abstract interpretation of Prolog. In K. Apt (Ed.), Proc. Joint International Conference and Symposium on Logic Programming, pp. 750–764, Washington D.C., 1992. The MIT Press, Cambridge MA.

    Google Scholar 

  30. B. Le Charlier and P. Van Hentenryck. Groundness analysis for Prolog: Implementation and evaluation of the domain Prop. In Proc. ACM-SIGPLAN Symp. on Partial Evaluation and Semantics-Based Program Manipulation (PEPM'93), pp. 99–110, Copenhagen, June 1993.

    Google Scholar 

  31. B. Le Charlier and P. Van Hentenryck. Experimental evaluation of a generic abstract interpretation algorithm for Prolog. ACM Trans. Prog. Lang. Syst., 16(1):35–101, Jan. 1994.

    Article  Google Scholar 

  32. J. W. Lloyd. Foundations of Logic Programming. Springer Series: Symbolic Computation — Artificial Intelligence. Springer-Verlag, second, extended edition, 1987.

    Google Scholar 

  33. K. Marriott. Frameworks for abstract interpretation. Acta Informatica, 30(2):103–129, 1993.

    Article  Google Scholar 

  34. K. Marriott and H. SØndergaard. Precise and efficient groundness analysis for logic programs. ACM Lett. Prog. Lang. Syst., 2(1–4):181–196, 1993.

    Article  Google Scholar 

  35. A. Martelli and U. Montanari. An efficient unification algorithm. ACM Trans. Prog. Lang. Syst., 4(2):258–282, Apr. 1982.

    Article  Google Scholar 

  36. C. S. Mellish. The automatic generation of mode declarations for Prolog programs. DAI Research Paper 163, Dept. of Artificial Intelligence, Univ. of Edinburgh, Aug. 1981.

    Google Scholar 

  37. C. S. Mellish. Abstract interpretation of Prolog programs. In Abramsky and Hankin [1], pp. 181–198.

    Google Scholar 

  38. A. Mulkers, W. Simoens, G. Janssens, and M. Bruynooghe. On the practicality of abstract equation systems. In L. Sterling (Ed.), Proc. International Conference on Logic Programming, Kanagawa, Japan, 1995. The MIT Press, Cambridge MA. (To appear.)

    Google Scholar 

  39. K. Muthukumar and M. Hermenegildo. Determination of variable dependence information through abstract interpretation. In E. L. Lusk and R. A. Overbeek (Ed.), Proc. North American Conference on Logic Programming, pp. 166–188, Cleveland, Ohio, USA, 1989.

    Google Scholar 

  40. K. Muthukumar and M. Hermenegildo. Combined determination of sharing and freeness of program variables through abstract interpretation. In K. Furukawa (Ed.), Proc. Eighth International Conference on Logic Programming, pp. 49–63, Paris, France, 1991. The MIT Press, Cambridge MA.

    Google Scholar 

  41. D. A. Plaisted. The occur-check problem in Prolog. J. New Generation Computing, 2(4):309–322, 1984. Also in: Proc. International Symposium on Logic Programming, pp. 272–280, Atlantic City, 1984. IEEE Computer Society Press.

    Google Scholar 

  42. H. SØndergaard. An application of abstract interpretation of logic programs: Occur check reduction. In B. Robinet and R. Wilhelm (Eds.), ESOP'86 — European Symposium on Programming, Proceedings, Lecture Notes in Computer Science, Vol. 213, Springer-Verlag, 1986, pp. 327–338.

    Google Scholar 

  43. P. Van Hentenryck, A. Cortesi, and B. Le Charlier. Evaluation of the domain Prop. The Journal of Logic Programming, 23(3):237–278, 1995.

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, K.U.Leuven, Celestijnenlaan 200A, 3001, Heverlee, Belgium

    Maurice Bruynooghe & Anne Mulkers

  2. Department of Mathematics and Computer Science, Ben-Gurion University, P.O.B. 653, 84105, Beer-Sheva, Israel

    Michael Codish

Authors
  1. Maurice Bruynooghe
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Michael Codish
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Anne Mulkers
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Jan van Leeuwen

Rights and permissions

Reprints and permissions

Copyright information

© 1995 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Bruynooghe, M., Codish, M., Mulkers, A. (1995). Abstracting unification: A key step in the design of logic program analyses. In: van Leeuwen, J. (eds) Computer Science Today. Lecture Notes in Computer Science, vol 1000. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0015257

Download citation

  • DOI: https://doi.org/10.1007/BFb0015257

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-60105-0

  • Online ISBN: 978-3-540-49435-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation