Hostname: page-component-74656f9884-npj9w Total loading time: 0 Render date: 2026-11-10T05:17:45.427Z Has data issue: false hasContentIssue false
  • English
  • Français

A practical analysis of non-termination in large logic programs

Published online by Cambridge University Press:  25 September 2013

SENLIN LIANG  and
MICHAEL KIFER
SENLIN LIANG
Affiliation:
Department of Computer Science, Stony Brook University, USA (e-mail: sliang@cs.stonybrook.edu, kifer@cs.stonybrook.edu)
MICHAEL KIFER
Affiliation:
Department of Computer Science, Stony Brook University, USA (e-mail: sliang@cs.stonybrook.edu, kifer@cs.stonybrook.edu)
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the 'Save PDF' action button.

A large body of work has been dedicated to termination analysis of logic programs but relatively little has been done to analyze non-termination. In our opinion, explaining non-termination is a much more important task because it can dramatically improve a user's ability to effectively debug large, complex logic programs without having to abide by punishing syntactic restrictions. Non-termination analysis examines program execution history when the program is suspected to not terminate and informs the programmer about the exact reasons for this behavior. In Liang and Kifer (2013), we studied the problem of non-termination in tabled logic engines with subgoal abstraction, such as XSB, and proposed a suite of algorithms for non-termination analysis, called Terminyzer. These algorithms analyze forest logging traces and output sequences of tabled subgoal calls that are the likely causes of non-terminating cycles. However, this feedback was hard to use in practice: the same subgoal could occur in multiple rule heads and in even more places in rule bodies, so Terminyzer left too much tedious, sometimes combinatorially large amount of work for the user to do manually.

Here we propose a new suite of algorithms, Terminyzer+, which closes this usability gap. Terminyzer+ can detect not only sequences of subgoals that cause non-termination, but, importantly, the exact rules where they occur and the rule sequences that get fired in a cyclic manner, thus causing non-termination. This makes Terminyzer+ suitable as a back-end for user-friendly graphical interfaces on top of Terminyzer+, which can greatly simplify the debugging process. Terminyzer+ back-ends exist for the SILK system as well as for the open-source ${\cal F}$lora-2 system. A graphical interface has been developed for SILK and is currently underway for ${\cal F}$lora-2. We also report experimental studies, which confirm the effectiveness of Terminyzer+ on a host of large real-world knowledge bases. All tests used in this paper are available online.1

In addition, we make a step towards automatic remediation of non-terminating programs by proposing an algorithm that heuristically fixes some causes of misbehavior. Furthermore, unlike Terminyzer, Terminyzer+ does not require the underlying logic engine to support subgoal abstraction, although it can make use of it.

Keywords

terminyzertermination and non-termination analysislogic programming

Information

Type
Regular Papers
Information
Theory and Practice of Logic Programming , Volume 13 , Special Issue 4-5: 29th International Conference on Logic Programming , July 2013 , pp. 705 - 719
Copyright
Copyright © 2013 [SENLIN LIANG and MICHAEL KIFER] 

References

Bol, R. N., Apt, K. R. and Klop, J. W. 1991. An analysis of loop checking mechanisms for logic programs. Theoretical Computer Science 86, 1, 35–79.CrossRefGoogle Scholar
Bruynooghe, M., Codish, M., Gallagher, J. P., Genaim, S. and Vanhoof, W. 2007. Termination analysis of logic programs through combination of type-based norms. ACM Transactions on Programming Languages and Systems 29, 1–44.CrossRefGoogle Scholar
Chen, W., Kifer, M. and Warren, D. S. 1993. HiLog: A foundation for higher-order logic programming. Journal of Logic Programming 15, 3, 187–230.CrossRefGoogle Scholar
Costa, V. S., Damas, L. and Rocha, R. 2012. The YAP prolog system. Theory and Practice of Logic Programming 12, 5–34.CrossRefGoogle Scholar
Hermenegildo, M. V., Bueno, F., Carro, M., López-García, P., Mera, E., Morales, J. F. and Puebla, G. 2012. An overview of Ciao and its design philosophy. Theory and Practice of Logic Programming 12, 1–2, 219–252.CrossRefGoogle Scholar
Kifer, M., Lausen, G. and Wu, J. 1995. Logical foundations of object-oriented and frame-based languages. Journal of ACM 42, 741–843.CrossRefGoogle Scholar
Liang, S. and Kifer, M. 2013. Terminyzer: An automatic non-termination analyzer for large logic programs. In Practical Aspects of Declarative Languages. Springer-Verlag, Berlin, Heidelberg, New York.Google Scholar
Lindenstrauss, N., Sagiv, Y. and Serebrenik, A. 2004. Proving termination for logic programs by the query-mapping pairs approach. In Program Developments in Computational Logic, Springer-Verlag LNCS, Berlin, Heidelberg, 453–498.CrossRefGoogle Scholar
Nguyen, M. T. and De Schreye, D. 2007. Polytool: Proving termination automatically based on polynomial interpretations. In Logic-Based Program Synthesis and Transformation, Springer-Verlag, Berlin, Heidelberg, 210–218.CrossRefGoogle Scholar
Nguyen, M. T., Giesl, J., Schneider-Kamp, P. and De Schreye, D. 2008. Termination analysis of logic programs based on dependency graphs. In Logic-Based Program Synthesis and Transformation, Springer-Verlag, Berlin, Heidelberg, 8–22.CrossRefGoogle Scholar
Schneider-kamp, P., Giesl, J., Ströder, T., Serebrenik, A. and Thiemann, R. 2010. Automated termination analysis for logic programs with cut. Theory and Practice of Logic Programming 10, 4–6 (July), 365–381.CrossRefGoogle Scholar
Schreye, D. D. and Decorte, S. 1994. Termination of logic programs: The never-ending story. Journal of Logic Programming 19/20, 199–260.CrossRefGoogle Scholar
Sipser, M. 1996. Introduction to the Theory of Computation, 1st ed. International Thomson Publishing, Washington, DC.CrossRefGoogle Scholar
Swift, T. and Warren, D. S. 2012. XSB: Extending prolog with tabled logic programming. Theory and Practice of Logic Programming 12, 157–187.CrossRefGoogle Scholar
Verbaeten, S., De Schreye, D. and Sagonas, K. 2001. Termination proofs for logic programs with tabling. ACM Transactions on Computational Logic 2, 1 (January), 57–92.CrossRefGoogle Scholar
Zhou, N.-F. 2012. The language features and architecture of B-Prolog. Theory and Practice of Logic Programming 12, 1–2, 189–218.CrossRefGoogle Scholar
Supplementary material: PDF

Liang and Kifer supplementary material

Appendix

Download Liang and Kifer supplementary material(PDF)
PDF 346.3 KB