On the occur-check-free PROLOG programs

ABSTRACT

In most PROLOG implementations, for efficiency occur-check is omitted from the unification algorithm. This paper provides natural syntactic conditions that allow the occur-check to be safely omitted. The established results apply to most well-known PROLOG programs, including those that use difference lists, and seem to explain why this omission does not lead in practice to any complications. When applying these results to general programs, we show their usefulness for proving absence of floundering. Finally, we propose a program transformation that transforms every program into a program for which only the calls to the built-in unification predicate need to be resolved by a unification algorithm with the occur-check.

REFERENCES

• 1: Luc Albert , Rafael Casas , François Fages, Average-case analysis of unification algorithms, Theoretical Computer Science, v.113 n.1, p.3-34, May 24, 1993
• 2: Krzysztof R. Apt, Logic programming, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• 3: APT, K. R. AND DOLTS, K. 1994. A new definition of SLDNF-resolution. J. Logic Program. 18, 177-190.
• 4: Krzysztof R. Apt , Alessandro Pellegrini, Why the Occur-Check is Not a Problem, Proceedings of the 4th International Symposium on Programming Language Implementation and Logic Programming, p.69-86, August 26-28, 1992
• 5: Krzysztof R. Apt , Peter Emde Boas , Angelo Welling, The STO-problem is NP-hard, CWI (Centre for Mathematics and Computer Science), Amsterdam, The Netherlands, 1994
• 6: Joachim Beer, The occur-check problem revisited, Journal of Logic Programming, v.5 n.3, p.243-261, Sept. 1988 [doi>10.1016/0743-1066(88)90012-X ]
• 7: BossI, A., AND Cocco, N. 1990. Basic transformation operations for logic programs which preserve computed answer substitutions. Tech. Rep. 16, Dipartimento di Matematica Puraed Applicata, Universit~ di Padova, Italy.
• 8: CHADHA, R., AND PLAISTED, D. A. 1994. Correctness of unification without occur check in Prolog. J. Logic Program. 18, 99-122.
• 9: CLARK, K.L. 1979. Predicate logic as a computational formalism. Res. Rep. DOC 79/59, Dept. of Computing, Imperial College, London.
• 10: CURRY, H. B., AND FEYS, R. 1958. Combinatory Logic. Vol. I. Studies zn Logic and the Foundation of Mathematics. North-Holland, Amsterdam.
• 11: DECKER, H. 1991. On generalized cover axioms. In Proceedings of the 8th international Conference on Logic Programming, K. Furukawa, Ed. MIT Press, Paris, France, 693-707.
• 12: DEMBINSKI, P., AND MALUSZYNSKI, J. 1985. AND-parallelism with intelligent backtracking for annotated logic programs. In Proceedings of the International Symposium on Logic Programming (Boston, Mass.). 29-38.
• 13: DERANSART, P., AND MALUSZYNSKI, J. 1985. Relating logic programs and attribute grammars. J. Logtc Program., 2, 119-156.
• 14: DERANSART, P., FERRAND, G., AND TI~GUIA, M. 1991. NSTO programs (not subject to occur-check). In Proceedings of the International Logtc Symposium, V. Saraswat and K. Ueda, Eds. MIT Press, Cambridge, Mass., 533-547.
• 15: DRABENT, W. 1987. Do logic programs resemble programs in conventional languages? In International Symposium on Logic Programmtng (San Francisco, Calif., Aug.) IEEE, New York, 389-396.
• 16: DUMANT, B. 1992. Checking soundness of resolution schemes. In Proceedings of the Joint International Conference and Symposium on Logic Programming, K. R. Apt, Ed. MIT Press, Cambridge, Mass., 37-51.
• 17: J.-L. Lassez , M. J. Maher , K. Marriott, Unification revisited, Foundations of deductive databases and logic programming, Morgan Kaufmann Publishers Inc., San Francisco, CA, 1988
• 18: J. W. Lloyd, Foundations of logic programming; (2nd extended ed.), Springer-Verlag New York, Inc., New York, NY, 1987
• 19: Kim Marriott , Harald Søndergaard , Philip Dart, A characterization of non-floundering logic programs, Proceedings of the 1990 North American conference on Logic programming, p.661-680, January 1990, Austin, Texas, United States
• 20: Alberto Martelli , Ugo Montanari, An Efficient Unification Algorithm, ACM Transactions on Programming Languages and Systems (TOPLAS), v.4 n.2, p.258-282, April 1982 [doi>10.1145/357162.357169]
• 21: MELLISH, C.S. 1981. The automatic generation of mode declarations for Prolog programs. DAI Res. Pap. 163, Dept of Artificial Intelligence, Univ. of Edinburgh, Aug.
• 22: PLAISTED, D.A. 1984. The occur-check problem in Prolog. In Proceedings of the International Conference on Logic Programming. IEEE, New York, 272-280.
• 23: REDD~, W. ~. 1984. Transformation of logic programs into functional programs. In Interna- tional Sympostum on Logic Programming (Silver Spring, Md., Feb.). IEEE, New York, 187-198.
• 24: REDDY, U.S. 1986. On the relationship between logic and functional languages. In Functional and Logic Programming, D. DeGroot and G. Lindstrom, Eds. Prentice-Hall, Englewood Cliffs, N.J., 3-36.
• 25: ROSENBLUETH, D.A. 1991. Using program transformation to obtain methods for eliminating backtracking in fixed-mode logic programs. Tech Rep. 7, Instituto de Investigaclones en Matematicas Aplicadas yen Sistemas. Universidad Nacional Autonoma de Mexico
• 26: John C. Shepherdson, Unsolvable problems for SLDF resolution, Journal of Logic Programming, v.10 n.1, p.19-22, Jan. 1991 [doi>10.1016/0743-1066(91)90003-8 ]
• 27: H Sondergaard, An application of abstract interpretation of logic programs: occur check reduction, Proc. of the European symposium on programming on ESOP 86, p.327-338, March 1986, Saarbru:9Aicken, Germany
• 28: STERLING, L., AND SHAPIRO, E. 1986. The Art ofProlog, MIT Press, Cambridge, Mass.
• 29: STROETMAN, K. 1993. A completeness result for SLDNF resolution. J. Logic Program. 15, 337-357.
• 30: TAMAKI, H., AND SATO, T. 1984. Unfold/fold transformation of logic programs. In Proceedings of the 2nd International Conference on Logic Programming (Uppsala, Sweden). 127-137.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications

          Nouns: Prolog

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Correctness proofs
  D.3 PROGRAMMING LANGUAGES
      D.3.4 Processors
          Subjects: Preprocessors

  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Logic and constraint programming; Mechanical theorem proving

General Terms:
Algorithms, Languages, Theory

Keywords:
PROLOG programs, moded programs, occur-check problem, unification algorithm