Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
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.
K. R. Apt and A. Pellegrini. On the occur-check-free Prolog programs. ACM TOPLAS, 16(3):687–726, 1994.
T. Armstrong, K. Marriott, P. Schachte, and H. SØndergaard. Two classes of Boolean functions for dependency analysis. To appear in Sci. Comp. Prog.
J. Beer. The occur-check problem revisited. J. Logic Prog., 5:243–261, 1988.
R. Chadha and D. A. Plaisted. Correctness of unification without occur check in Prolog. J. Logic Prog., 18:99–122, 1994.
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.
P. Cousot and R. Cousot. Abstract interpretation and application to logic programs. J. Logic Prog., 13(2&3):103–179, 1992.
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.
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.
P. Deransart and J. Małuszyński. Relating logic programs and attribute grammars. J. Logic Prog., 2(2):119–156, 1985.
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.
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.
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.
B. Le Charlier and P. Van Hentenryck. Experimental evaluation of a generic abstract interpretation algorithm for Prolog. ACM TOPLAS, 16(1):35–101, 1994.
K. Marriott and H. SØndergaard. On Prolog and the occur check problem. SIGPLAN Notices, 24(5):76–82, 1989.
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.
K. Marriott, H. SØndergaard, and N. Jones. Denotational abstract interpretation of logic programs. ACM TOPLAS, 16(3):607–648, 1994.
K. Muthukumar and M. Hermenegildo. Compile-time derivation of variable dependency using abstract interpretation. J. Logic Prog., 13(2&3):315–347, 1992.
D. A. Plaisted. The occur-check problem in Prolog. New Generation Computing, 2(4):309–322, 1984.
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.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Crnogorac, L., Kelly, A.D., SØndergaard, H. (1996). A comparison of three occur-check analysers. In: Cousot, R., Schmidt, D.A. (eds) Static Analysis. SAS 1996. Lecture Notes in Computer Science, vol 1145. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61739-6_40
Download citation
DOI: https://doi.org/10.1007/3-540-61739-6_40
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61739-6
Online ISBN: 978-3-540-70674-8
eBook Packages: Springer Book Archive