Abstract
In this paper, we define two particular forms of non-termination, namely loops and binary chains, in an abstract framework that encompasses term rewriting and logic programming. The definition of loops relies on the notion of compatibility of binary relations. We also present a syntactic criterion for the detection of a special case of binary chains. Moreover, we describe our implementation NTI and compare its results at the Termination Competition 2023 with those of leading analyzers.
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.References
Apt, K.R.: From Logic Programming to Prolog. Prentice Hall International series in computer science. Prentice Hall, Hoboken (1997)
Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)
Bol, R.N., Apt, K.R., Klop, J.W.: An analysis of loop checking mechanisms for logic programs. Theoret. Comput. Sci. 86(1), 35–79 (1991)
Codish, M., Taboch, C.: A semantic basis for the termination analysis of logic programs. J. Logic Program. 41(1), 103–123 (1999)
Dershowitz, N.: Termination of rewriting. J. Symbol. Comput. 3(1/2), 69–116 (1987)
Emmes, F., Enger, T., Giesl, J.: Proving non-looping non-termination automatically. In: Gramlich, B., Miller, D., Sattler, U. (eds.) Proceedings of the 6th International Joint Conference on Automated Reasoning (IJCAR’12). LNCS, vol. 7364, pp. 225–240. Springer, Berlin (2012)
Endrullis, J., Zantema, H.: Proving non-termination by finite automata. In: Fernández, M. (ed.) Proceedings of the 26th International Conference on Rewriting Techniques and Applications (RTA’15). Leibniz International Proceedings in Informatics (LIPIcs), vol. 36, pp. 160–176. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik (2015)
Gabbrielli, M., Giacobazzi, R.: Goal independency and call patterns in the analysis of logic programs. In: Berghel, H., Hlengl, T., Urban, J.E. (eds.) Proceedings of the 1994 ACM Symposium on Applied Computing (SAC’94), pp. 394–399. ACM, New York (1994)
Geser, A., Zantema, H.: Non-looping string rewriting. RAIRO Theoret. Inf. Appl. 33(3), 279–302 (1999)
Giesl, J., Aschermann, C., Brockschmidt, M., Emmes, F., Frohn, F., Fuhs, C., Hensel, J., Otto, C., Plücker, M., Schneider-Kamp, P., Ströder, T., Swiderski, S., Thiemann, R.: Analyzing program termination and complexity automatically with AProVE. J. Automat. Reason. 58(1), 3–31 (2017)
Giesl, J., Thiemann, R., Schneider-Kamp, P.: Proving and disproving termination of higher-order functions. In: Gramlich, B. (ed.) Proceedings of the 5th International Workshop on Frontiers of Combining Systems (FroCoS’05). LNAI, vol. 3717, pp. 216–231. Springer, Berlin (2005)
Giesl, J., et al.: AProVE (Automated Program Verification Environment). http://aprove.informatik.rwth-aachen.de/ (2023)
Gupta, A., Henzinger, T.A., Majumdar, R., Rybalchenko, A., Xu, R.-G.: Proving non-termination. In: Necula, G.C., Wadler, P. (eds.) Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’08), pp. 147–158. ACM, New York (2008)
Guttag, J.V., Kapur, D., Musser, D.R.: On proving uniform termination and restricted termination of rewriting systems. SIAM J. Comput. 12(1), 189–214 (1983)
Hofbauer, D.: MnM (MultumNonMulta) (2023)
Karp, R.M., Miller, R.E.: Parallel program schemata. J. Comput. Syst. Sci. 3(2), 147–195 (1969)
Lloyd, J.W.: Foundations of Logic Programming, 2nd edn. Springer, Berlin (1987)
Lucas, S., Gutiérrez, R.: MU-TERM. http://zenon.dsic.upv.es/muterm/ (2019)
Oppelt, M.: Automatische Erkennung von Ableitungsmustern in nichtterminierenden Wortersetzungssystemen. Diploma Thesis, HTWK Leipzig, Germany (2008)
Park, D.M.R.: Concurrency and automata on infinite sequences. In: Deussen, P. (ed.) Proceedings of the 5th GI-Conference on Theoretical Computer Science. LNCS, vol. 104, pp. 167–183. Springer, Berlin (1981)
Payet, É.: Loop detection in term rewriting using the eliminating unfoldings. Theoret. Comput. Sci. 403(2–3), 307–327 (2008)
Payet, É.: Guided unfoldings for finding loops in standard term rewriting. In: Mesnard, F., Stuckey, P.J. (eds.) Proceedings of the 28th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR’18), Revised Selected Papers, LNCS, vol. 11408, pp. 22–37. Springer, Berlin (2018)
Payet, É.: Binary non-termination in term rewriting and logic programming. In: Yamada, A. (ed.) Proceedings of the 19th International Workshop on Termination (WST’23) (2023)
Payet, É.: NTI (Non-Termination Inference). http://lim.univ-reunion.fr/staff/epayet/Research/NTI/NTI.html and https://github.com/etiennepayet/nti (2023)
Payet, É., Mesnard, F.: Nontermination inference of logic programs. ACM Trans. Program. Lang. Syst. 28(2), 256–289 (2006)
Sahlin, D.: The Mixtus approach to automatic partial evaluation of full Prolog. In: Debray, S.K., Hermenegildo, M.V. editors, Proc. of the 1990 North American Conference on Logic Programming, pages 377–398. MIT Press (1990)
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: Warren, D.H.D., Szeredi, P. (eds.) Proceedings of the 7th International Conference on Logic Programming (ICLP’90), pp. 649–663. MIT, New York (1990)
Shen, Y.-D.: An extended variant of atoms loop check for positive logic programs. New Gen Comput. 15(2), 187–204 (1997)
Sternagel, C., Middeldorp, A.: \({\sf T}_{{\sf T}}{\sf T}_{{\sf 2}}\) (Tyrolean Termination Tool 2). http://cl-informatik.uibk.ac.at/software/ttt2/ (2020)
Terese: Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science, vol. 55. Cambridge University Press, Cambridge (2003)
The Annual International Termination Competition. http://termination-portal.org/wiki/Termination_Competition
Termination Problems Data Base. http://termination-portal.org/wiki/TPDB
Waldmann, J.: Matchbox: a tool for match-bounded string rewriting. In: van Oostrom, V. (ed.) Proceedings of the 15th International Conference on Rewriting Techniques and Applications (RTA’04). LNCS, vol. 3091, pp. 85–94. Springer, Berlin (2004)
Wang, Y., Sakai, M.: On non-looping term rewriting. In: Geser, A., Søndergaard, H. (ed.) Proceedings of the 8th International Workshop on Termination (WST’06), pp. 17–21 (2006)
Yamada, A.: NaTT (Nagoya Termination Tool). https://www.trs.css.i.nagoya-u.ac.jp/NaTT/ (2023)
Zankl, H., Middeldorp, A.: Nontermination of string rewriting using SAT. In: Hofbauer, D., Serebrenik, A. (ed.) Proceedings of the 9th International Workshop on Termination (WST’07), pp. 52–55 (2007)
Zantema, H.: Termination of string rewriting proved automatically. J. Automat. Reason. 34(2), 105–139 (2005)
Zantema, H., Geser, A.: Non-looping rewriting. Universiteit Utrecht. UU-CS, Department of Computer Science. Utrecht University, The Netherlands (1996)
Acknowledgements
The author is very grateful to the anonymous reviewers for their insightful and constructive comments and suggestions on this work.
Author information
Authors and Affiliations
Corresponding author
Additional information
Publisher's Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
Rights and permissions
Springer Nature or its licensor (e.g. a society or other partner) holds exclusive rights to this article under a publishing agreement with the author(s) or other rightsholder(s); author self-archiving of the accepted manuscript version of this article is solely governed by the terms of such publishing agreement and applicable law.
About this article
Cite this article
Payet, É. Non-termination in Term Rewriting and Logic Programming. J Autom Reasoning 68, 4 (2024). https://doi.org/10.1007/s10817-023-09693-z
Received:
Accepted:
Published:
DOI: https://doi.org/10.1007/s10817-023-09693-z