Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
K. R. Apt. From Logic Programming to Prolog. Prentice Hall, 1997.
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.
K. R. Apt and M. H. Van Emden. Contributions to the theory of logic programming. Journal of the ACM, 29(3):841–862, 1982.
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.
R. Bol. Loop Checking in Logic Programming. PhD thesis, CWI, Amsterdam, 1991.
M. Bruynooghe, D. De Schreye, and B. Martens. A general criterion for avoiding infinite unfolding during partial deduction. New Generation Computing, 11(1):47–79, 1992.
M. Codish and C. Taboch. A semantic basis for the termination analysis of logic programs. Journal of Logic Programming, 41(1):103–123, 1999.
D. De Schreye, M. Bruynooghe, and K. Verschaetse. On the existence of non-terminating queries for a restricted class of Prolog-clauses. Artificial Intelligence, 41:237–248, 1989.
D. De Schreye and S. Decorte. Termination of logic programs: the never-ending story. Journal of Logic Programming, 19–20:199–260, 1994.
N. Dershowitz, N. Lindenstrauss, Y. Sagiv, and A. Serebrenik. A general framework for automatic termination analysis of logic programs. Applicable Algebra in Engineering,Communication and Computing, 12(1/2):117–156, 2001.
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.
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.
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.
R. Gori and G. Levi. Finite failure is and-compositional. Journal of Logic and Computation, 7(6):753–776, 1997.
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.
N. Lindenstrauss. TermiLog: a system for checking termination of queries to logic programs, 1997. http://www.cs.huji.ac.ilñaomil.
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.
F. Mesnard and U. Neumerkel. cTI: a tool for inferring termination conditions of ISO-Prolog, april 2000. http://www.complang.tuwien.ac.at/cti.
F. Mesnard and U. Neumerkel. Applying static analysis techniques for inferring termination conditions of logic programs. In P. Cousot, editor, Static Analysis Symposium, volume 2126 of Lecture Notes in Computer Science, pages 93–110. Springer-Verlag, Berlin, 2001.
R. O’Keefe. The Craft Of Prolog. MIT Press, 1990.
L. Plümer. Termination proofs for logic programs. Number 446 in LNAI. Springer-Verlag, Berlin, 1990.
Y-D. Shen, L-Y. Yuan, and J-H. You. Loops checks for logic programs with functions. Theoretical Computer Science, 266(1–2):441–461, 2001.
D. Skordev. An abstract approach to some loop detection problems. Fundamenta Informaticae, 31:195–212, 1997.
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.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Mesnard, F., Payet, E., Neumerkel, U. (2002). Detecting Optimal Termination Conditions of Logic Programs. In: Hermenegildo, M.V., Puebla, G. (eds) Static Analysis. SAS 2002. Lecture Notes in Computer Science, vol 2477. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45789-5_35
Download citation
DOI: https://doi.org/10.1007/3-540-45789-5_35
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-44235-6
Online ISBN: 978-3-540-45789-3
eBook Packages: Springer Book Archive