Detecting Optimal Termination Conditions of Logic Programs
In this paper, we begin with an approach to non-termination inference of logic programs. Our framework relies on an extension of the Lifting Theorem, where some specific argument positions can be instantiated while others are generalized. Atomic left looping queries are generated bottom-up from selected subsets of the binary unfoldings of the program of interest. Then non-termination inference is tailored to attempt proofs of optimality of left termination conditions computed by a termination inference tool. For each class of atomic queries not covered by a termination condition, the aim is to ensure the existence of one query from this class which leads to an infinite search tree. An experimental evaluation is reported. When termination and non-termination analysis produce complementary results for a logic procedure, they induce a characterization of the operational behavior of the logic procedure with respect to the left most selection rule and the language used to describe sets of atomic queries.
KeywordsLogic Program Predicate Symbol Relation Symbol Partial Correctness Loop Condition
Unable to display preview. Download preview PDF.
- 1.K. R. Apt. From Logic Programming to Prolog. Prentice Hall, 1997.Google Scholar
- 2.K. R. Apt and D. Pedreschi. Modular termination proofs for logic and pure Prolog programs. In G. Levi, editor, Advances in Logic Programming Theory, pages 183–229. Oxford University Press, 1994.Google Scholar
- 4.T. Arts and H. Zantema. Termination of logic programs using semantic unification. In Logic Program Synthesis and Transformation, volume 1048 of Lecture Notes in Computer Science. Springer-Verlag, Berlin, 1996.Google Scholar
- 5.R. Bol. Loop Checking in Logic Programming. PhD thesis, CWI, Amsterdam, 1991.Google Scholar
- 11.P. Devienne, P. Lebégue, and J-C. Routier. Halting problem of one binary Horn clause is undecidable. In LNCS, volume 665, pages 48–57. Springer-Verlag, 1993. Proc. of STACS’93.Google Scholar
- 12.M. Gabbrielli and R. Giacobazzi. Goal independency and call patterns in the analysis of logic programs. In Proceedings of the ACM Symposium on applied computing, pages 394–399. ACM Press, 1994.Google Scholar
- 13.S. Genaim and M. Codish. Inferring termination condition for logic programs using backwards analysis. In Proceedings of Logic for Programming, Artificial intelligence and Reasoning, Lecture Notes in Computer Science. Springer-Verlag, Berlin, 2001. TerminWeb can be used online from http://www.cs.bgu.ac.il~codish.Google Scholar
- 15.H. J. Komorowski. Partial evaluation as a means for inferencing data structures in an applicative language: a theory and implementation in the case of Prolog. In Proc. of the 9th POPL, pages 255–267, 1982.Google Scholar
- 16.N. Lindenstrauss. TermiLog: a system for checking termination of queries to logic programs, 1997. http://www.cs.huji.ac.ilñaomil.
- 17.F. Mesnard. Inferring left-terminating classes of queries for constraint logic programs by means of approximations. In M. J. Maher, editor, Proc. of the 1996 Joint Intl. Conf. and Symp. on Logic Programming, pages 7–21. MIT Press, 1996.Google Scholar
- 18.F. Mesnard and U. Neumerkel. cTI: a tool for inferring termination conditions of ISO-Prolog, april 2000. http://www.complang.tuwien.ac.at/cti.
- 20.R. O’Keefe. The Craft Of Prolog. MIT Press, 1990.Google Scholar
- 24.C. Speirs, Z. Somogyi, and H. Søndergaard. Termination analysis for Mercury. In P. Van Hentenryck, editor, Proc. of the International Static Analysis Symposium, volume 1302 of LNCS, pages 160–171. Springer-Verlag, 1997.Google Scholar