A comparison of three occur-check analysers

  • Lobel Crnogorac
  • Andrew D. Kelly
  • Harald SØndergaard
Contributed Papers
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1145)


A well known problem with many Prolog interpreters and compilers is the lack of occur-check in the implementation of the unification algorithm. This means that such systems are unsound with respect to first-order predicate logic. Static analysis offers an appealing approach to the problem of occur-check reduction, that is, the safe omission of occur-checks in unification. We compare, for the first time, three static methods that have been suggested for occur-check reduction, two based on assigning “modes∝ to programs and one which uses abstract interpretation. In each case, the analysis or some essential part of it had not been implemented so far. Of the mode-based methods, one is due to Chadha and Plaisted and the other is due to Apt and Pellegrini. The method using abstract interpretation is based on earlier work by Plaisted, SØndergaard and others who have developed groundness and sharing analyses for logic programs. The conclusion is that a truly global analysis based on abstract interpretation leads to markedly higher precision and hence fewer occur-checks at run-time. Given the potential run-time speedups, a precise analysis would be well worth the extra time.


Logic Program Abstract Interpretation Calling Pattern Argument Position Normalise Program 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    K. R. Apt and A. Pellegrini. Why the occur-check is not a problem. In M. Bruynooghe and M. Wirsing, editors, Proc. PLILP '92, LNCS 631, pages 69–86. Springer-Verlag, 1992.Google Scholar
  2. 2.
    K. R. Apt and A. Pellegrini. On the occur-check-free Prolog programs. ACM TOPLAS, 16(3):687–726, 1994.Google Scholar
  3. 3.
    T. Armstrong, K. Marriott, P. Schachte, and H. SØndergaard. Two classes of Boolean functions for dependency analysis. To appear in Sci. Comp. Prog. Google Scholar
  4. 4.
    J. Beer. The occur-check problem revisited. J. Logic Prog., 5:243–261, 1988.Google Scholar
  5. 5.
    R. Chadha and D. A. Plaisted. Correctness of unification without occur check in Prolog. J. Logic Prog., 18:99–122, 1994.Google Scholar
  6. 6.
    M. Codish, D. Dams, and E. Yardeni. Derivation and safety of an abstract unification algorithm for groundness and aliasing analysis. In K. Furukawa, editor, Logic Programming: Proc. Eighth Int. Conf., pages 79–93. MIT Press, 1991.Google Scholar
  7. 7.
    P. Cousot and R. Cousot. Abstract interpretation and application to logic programs. J. Logic Prog., 13(2&3):103–179, 1992.Google Scholar
  8. 8.
    L. Crnogorac, A. D. Kelly, and H. SØndergaard. A comparison of three occur-check analyses. Technical Report 96/20, Dept. of Computer Science, The University of Melbourne, 1996.Google Scholar
  9. 9.
    P. Deransart, G. Ferrand, and M. Téguia. NSTO programs (Not Subject To Occur-check). In V. Saraswat and K. Ueda, editors, Logic Programming: Proc. 1991 Int. Symp., pages 533–547. MIT Press, 1991.Google Scholar
  10. 10.
    P. Deransart and J. Małuszyński. Relating logic programs and attribute grammars. J. Logic Prog., 2(2):119–156, 1985.Google Scholar
  11. 11.
    B. Dumant. Checking the soundness of resolution schemes. In K. Apt, editor, Logic Programming: Proc. Joint Int. Conf. Symp., pages 37–51. MIT Press, 1992.Google Scholar
  12. 12.
    M. Hermenegildo, G. Puebla, K. Marriott, and P. Stuckey. Incremental analysis of logic programs. In L. Sterling, editor, Logic Programming: Proc. Twelfth Int. Conf., pages 797–811. MIT Press, 1995.Google Scholar
  13. 13.
    A. D. Kelly, A. Macdonald, K. Marriott, H. SØndergaard, P. Stuckey, and R. Yap. An optimizing compiler for CLP({ie173-01}). In U. Montanari and F. Rossi, editors, Proc. CP'95, LNCS 976, pages 222–239. Springer-Verlag, 1995.Google Scholar
  14. 14.
    B. Le Charlier and P. Van Hentenryck. Experimental evaluation of a generic abstract interpretation algorithm for Prolog. ACM TOPLAS, 16(1):35–101, 1994.Google Scholar
  15. 15.
    K. Marriott and H. SØndergaard. On Prolog and the occur check problem. SIGPLAN Notices, 24(5):76–82, 1989.Google Scholar
  16. 16.
    K. Marriott and H. SØndergaard. Precise and efficient groundness analysis for logic programs. ACM Letters on Programming Languages and Systems, 2:181–196, 1993.Google Scholar
  17. 17.
    K. Marriott, H. SØndergaard, and N. Jones. Denotational abstract interpretation of logic programs. ACM TOPLAS, 16(3):607–648, 1994.Google Scholar
  18. 18.
    K. Muthukumar and M. Hermenegildo. Compile-time derivation of variable dependency using abstract interpretation. J. Logic Prog., 13(2&3):315–347, 1992.Google Scholar
  19. 19.
    D. A. Plaisted. The occur-check problem in Prolog. New Generation Computing, 2(4):309–322, 1984.Google Scholar
  20. 20.
    H. SØndergaard. An application of abstract interpretation of logic programs: Occur check reduction. In B. Robinet and R. Wilhelm, editors, Proc. European Symposium on Programming, LNCS 213, pages 327–338. Springer-Verlag, 1986.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1996

Authors and Affiliations

  • Lobel Crnogorac
    • 1
  • Andrew D. Kelly
    • 2
  • Harald SØndergaard
    • 1
  1. 1.Dept. of Computer ScienceUniversity of MelbourneParkvilleAustralia
  2. 2.Dept. of Computer ScienceMonash UniversityClaytonAustralia

Personalised recommendations