Abstract
Termination has been a subject of intensive research in the logic programming community for the last two decades. Most works deal with proving universal left termination of a given class of queries, i.e. finiteness of all the possible derivations produced by a Prolog engine from any query in that class. In contrast, the study of the dual problem: non-termination w.r.t. the left selection rule i.e the existence of one query in a given class of queries which admits an infinite left derivation, has given rise to only a few papers. In this article, we study non-termination in the more general constraint logic programming framework. We rephrase our previous logic programming approach into this more abstract setting, which leads to a criterion expressed in a logical way and simpler proofs, as expected. Also, by reconsidering our previous work, we now prove that in some sense, we already had the best syntactic criterion for logic programming. Last but not least, we offer a set of correct algorithms for inferring non-termination for CLP.
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
Clark, K.L.: Negation as failure. In: Gallaire, H., Minker, J. (eds.) Logic and Databases, pp. 293–322. Plenum Press, New York (1978)
Codish, M., Taboch, C.: A semantic basis for the termination analysis of logic programs. Journal of Logic Programming 41(1), 103–123 (1999)
De Schreye, D., Bruynooghe, M., Verschaetse, K.: On the existence of nonterminating queries for a restricted class of Prolog-clauses. Artificial Intelligence 41, 237–248 (1989)
De Schreye, D., Decorte, S.: Termination of logic programs: the never-ending story. Journal of Logic Programming 19-20, 199–260 (1994)
De Schreye, D., Verschaetse, K., Bruynooghe, M.: A practical technique for detecting non-terminating queries for a restricted class of Horn clauses, using directed, weighted graphs. In: Proc. of ICLP 1990, pp. 649–663. The MIT Press, Cambridge (1990)
Gabbrielli, M., Giacobazzi, R.: Goal independency and call patterns in the analysis of logic programs. In: Proceedings of the ACM Symposium on applied computing, pp. 394–399. ACM Press, New York (1994)
Genaim, S., Codish, M.: Inferring termination condition for logic programs using backwards analysis. In: Proceedings of Logic for Programming, Artificial intelligence and Reasoning. LNCS, Springer, Berlin (2001)
Jaffar, J., Lassez, J.L.: Constraint logic programming. In: Proc. of the ACM Symposium on Principles of Programming Languages, pp. 111–119. ACM Press, New York (1987)
Jaffar, J., Maher, M.J., Marriott, K., Stuckey, P.J.: The semantics of constraint logic programs. Journal of Logic Programming 37(1-3), 1–46 (1998)
Lloyd, J.W.: Foundations of Logic Programming. Springer, Heidelberg (1987)
Mesnard, F.: Inferring left-terminating classes of queries for constraint logic programs by means of approximations. In: Maher, M.J. (ed.) Proc. of the 1996 Joint Intl. Conf. and Symp. on Logic Programming, pp. 7–21. MIT Press, Cambridge (1996)
Mesnard, F., Neumerkel, U.: Applying static analysis techniques for inferring termination conditions of logic programs. In: Cousot, P. (ed.) SAS 2001. LNCS, vol. 2126, pp. 93–110. Springer, Heidelberg (2001)
Mesnard, F., Payet, E., Neumerkel, U.: Detecting optimal termination conditions of logic programs. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 509–525. Springer, Heidelberg (2002)
Mesnard, F., Ruggieri, S.: On proving left termination of constraint logic programs. ACM Transactions on Computational Logic, 207–259 (2003)
Refalo, P., Van Hentenryck, P.: CLP (Rlin) revised. In: Maher, M. (ed.) Proc. of the Joint International Conf. and Symposium on Logic Programming, pp. 22–36. The MIT Press, Cambridge (1996)
Shoenfield, J.: Mathematical Logic. Addison Wesley, Reading (1967)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Payet, E., Mesnard, F. (2004). Non-termination Inference for Constraint Logic Programs. In: Giacobazzi, R. (eds) Static Analysis. SAS 2004. Lecture Notes in Computer Science, vol 3148. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-27864-1_27
Download citation
DOI: https://doi.org/10.1007/978-3-540-27864-1_27
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-22791-5
Online ISBN: 978-3-540-27864-1
eBook Packages: Springer Book Archive