Nontermination inference of logic programs
Tóm tắt
We present a static analysis technique for nontermination inference of logic programs. Our framework relies on an extension of the subsumption test, where some specific argument positions can be instantiated while others are generalized. We give syntactic criteria to statically identify such argument positions from the text of a program. Atomic left looping queries are generated bottom-up from selected subsets of the binary unfoldings of the program of interest. We propose a set of correct algorithms for automating the approach. Then, nontermination inference is tailored to attempt proofs of optimality of left termination conditions computed by a termination inference tool. An experimental evaluation is reported and the analyzers can be tried online at http://www.univ-reunion.fr/~gcc. When termination and nontermination analysis produce complementary results for a logic procedure, then with respect to the leftmost selection rule and the language used to describe sets of atomic queries, each analysis is optimal and together, they induce a
Từ khóa
Tài liệu tham khảo
Apt K. R., From Logic Programming to Prolog
Apt K. R. and Pedreschi D. 1994. Modular termination proofs for logic and pure Prolog programs. In Advances in Logic Programming Theory G. Levi Ed. Oxford University Press 183--229.]] Apt K. R. and Pedreschi D. 1994. Modular termination proofs for logic and pure Prolog programs. In Advances in Logic Programming Theory G. Levi Ed. Oxford University Press 183--229.]]
Arts T., Logic Program Synthesis and Transformation. Lecture Notes in Computer Science, 1048
De Schreye D. and Decorte S. 1994. Termination of logic programs: the never-ending story. J. Logic Prog. 19--20 199--260.]] De Schreye D. and Decorte S. 1994. Termination of logic programs: the never-ending story. J. Logic Prog. 19--20 199--260.]]
De Schreye D., Proceedings of ICLP'90
Deransart P., 1987, Tech. Rep. 87/3, Laboratoire d'Informatique, Département de Mathématiques et d'Informatique, Université d'Orleans.]]
Dershowitz N. Lindenstrauss N. Sagiv Y. and Serebrenik A. 2001. A general framework for automatic termination analysis of logic programs. Applicable Algebra in Engineering Communication and Computing 12 1/2 117--156.]] Dershowitz N. Lindenstrauss N. Sagiv Y. and Serebrenik A. 2001. A general framework for automatic termination analysis of logic programs. Applicable Algebra in Engineering Communication and Computing 12 1/2 117--156.]]
Devienne P., 1988, Proceedings of the International Conference on Fifth Generation Computer Systems 88
Devienne P., 1993, -C
Genaim S., Proceedings of Logic for Programming, Artificial intelligence and Reasoning. Lecture Notes in Computer Science. Springer-Verlag
Lindenstrauss N. 1997. TermiLog: a system for checking termination of queries to logic programs. http://www.cs.huji.ac.il/~naomil.]] Lindenstrauss N. 1997. TermiLog: a system for checking termination of queries to logic programs. http://www.cs.huji.ac.il/~naomil.]]
Lloyd J. W., Foundations of Logic Programming
Mesnard F., 1996, Proceedings of the 1996 Joint International Conference and Symposium on Logic Programming, M. J. Maher, Ed. MIT Press, 7--21
Mesnard F. and Neumerkel U. 2000. cTI: a tool for inferring termination conditions of ISO-Prolog. http://www.univ-reunion.fr/~gcc.]] Mesnard F. and Neumerkel U. 2000. cTI: a tool for inferring termination conditions of ISO-Prolog. http://www.univ-reunion.fr/~gcc.]]
Mesnard F., Static Analysis Symposium, P. Cousot, Ed. Lecture Notes in Computer Science, 2126
Mesnard F., Proceedings of the 9th International Symposium on Static Analysis, M. Hermenegildo and G. Puebla, Eds. Lecture Notes in Computer Science, 2477
O'Keefe R., The Craft of Prolog
Payet E., Proceedings of the 11th International Symposium on Static Analysis, R. Giacobazzi, Ed. Lecture Notes in Computer Science, 3148
Plümer L., Terminations proofs for logic programs. Number 446 in LNAI
Sahlin D., 1990, Proceedings of the 1990 North American Conference on Logic Programming, S. Debray and M. Hermenegildo, Eds. MIT Press