Non-termination in term rewriting and logic programming. (English) Zbl 1540.68112
Summary: 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.
MSC:
| 68Q42 | Grammars and rewriting systems |
| 68N17 | Logic programming |
| 68V15 | Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) |
References:
| [1] | Apt, KR, From Logic Programming to Prolog. Prentice Hall International series in computer science (1997), Hoboken: Prentice Hall, Hoboken |
| [2] | Baader, F.; Nipkow, T., Term Rewriting and All That (1998), Cambridge: Cambridge University Press, Cambridge · Zbl 0948.68098 · doi:10.1017/CBO9781139172752 |
| [3] | Bol, RN; Apt, KR; Klop, JW, An analysis of loop checking mechanisms for logic programs, Theoret. Comput. Sci., 86, 1, 35-79 (1991) · Zbl 0741.68027 · doi:10.1016/0304-3975(91)90004-L |
| [4] | Codish, M.; Taboch, C., A semantic basis for the termination analysis of logic programs, J. Logic Program., 41, 1, 103-123 (1999) · Zbl 0948.68114 · doi:10.1016/S0743-1066(99)00006-0 |
| [5] | Dershowitz, N., Termination of rewriting, J. Symbol. Comput., 3, 1-2, 69-116 (1987) · Zbl 0637.68035 · doi:10.1016/S0747-7171(87)80022-6 |
| [6] | Emmes, F.; Enger, T.; Giesl, J.; Gramlich, B.; Miller, D.; Sattler, U., Proving non-looping non-termination automatically, Proceedings of the 6th International Joint Conference on Automated Reasoning (IJCAR’12), 225-240 (2012), Berlin: Springer, Berlin · Zbl 1358.68157 · doi:10.1007/978-3-642-31365-3_19 |
| [7] | 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) · Zbl 1366.68115 |
| [8] | Gabbrielli, M.; Giacobazzi, R.; Berghel, H.; Hlengl, T.; Urban, JE, Goal independency and call patterns in the analysis of logic programs, Proceedings of the 1994 ACM Symposium on Applied Computing (SAC’94), 394-399 (1994), New York: ACM, New York · doi:10.1145/326619.326789 |
| [9] | Geser, A.; Zantema, H., Non-looping string rewriting, RAIRO Theoret. Inf. Appl., 33, 3, 279-302 (1999) · Zbl 0951.68054 · doi:10.1051/ita:1999118 |
| [10] | 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) · Zbl 1409.68255 · doi:10.1007/s10817-016-9388-y |
| [11] | Giesl, J.; Thiemann, R.; Schneider-Kamp, P.; Gramlich, B., Proving and disproving termination of higher-order functions, Proceedings of the 5th International Workshop on Frontiers of Combining Systems (FroCoS’05), 216-231 (2005), Berlin: Springer, Berlin · Zbl 1171.68714 · doi:10.1007/11559306_12 |
| [12] | Giesl, J., et al.: AProVE (Automated Program Verification Environment). http://aprove.informatik.rwth-aachen.de/ (2023) |
| [13] | Gupta, A.; Henzinger, TA; Majumdar, R.; Rybalchenko, A.; Xu, R-G; Necula, GC; Wadler, P., Proving non-termination, Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’08), 147-158 (2008), New York: ACM, New York · Zbl 1295.68158 |
| [14] | Guttag, JV; Kapur, D.; Musser, DR, On proving uniform termination and restricted termination of rewriting systems, SIAM J. Comput., 12, 1, 189-214 (1983) · Zbl 0526.68036 · doi:10.1137/0212012 |
| [15] | Hofbauer, D.: MnM (MultumNonMulta) (2023) |
| [16] | Karp, RM; Miller, RE, Parallel program schemata, J. Comput. Syst. Sci., 3, 2, 147-195 (1969) · Zbl 0198.32603 · doi:10.1016/S0022-0000(69)80011-5 |
| [17] | Lloyd, JW, Foundations of Logic Programming (1987), Berlin: Springer, Berlin · Zbl 0668.68004 · doi:10.1007/978-3-642-83189-8 |
| [18] | Lucas, S., Gutiérrez, R.: MU-TERM. http://zenon.dsic.upv.es/muterm/ (2019) |
| [19] | Oppelt, M.: Automatische Erkennung von Ableitungsmustern in nichtterminierenden Wortersetzungssystemen. Diploma Thesis, HTWK Leipzig, Germany (2008) |
| [20] | Park, DMR; Deussen, P., Concurrency and automata on infinite sequences, Proceedings of the 5th GI-Conference on Theoretical Computer Science, 167-183 (1981), Berlin: Springer, Berlin · Zbl 0457.68049 · doi:10.1007/BFb0017309 |
| [21] | Payet, É., Loop detection in term rewriting using the eliminating unfoldings, Theoret. Comput. Sci., 403, 2-3, 307-327 (2008) · Zbl 1154.68436 · doi:10.1016/j.tcs.2008.05.013 |
| [22] | Payet, É.; Mesnard, F.; Stuckey, PJ, Guided unfoldings for finding loops in standard term rewriting, Proceedings of the 28th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR’18), Revised Selected Papers, LNCS, 22-37 (2018), Berlin: Springer, Berlin · Zbl 1524.68165 · doi:10.1007/978-3-030-13838-7_2 |
| [23] | 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) |
| [24] | Payet, É.: NTI (Non-Termination Inference). http://lim.univ-reunion.fr/staff/epayet/Research/NTI/NTI.html and https://github.com/etiennepayet/nti (2023) |
| [25] | Payet, É.; Mesnard, F., Nontermination inference of logic programs, ACM Trans. Program. Lang. Syst., 28, 2, 256-289 (2006) · doi:10.1145/1119479.1119481 |
| [26] | 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) |
| [27] | De Schreye, D.; Verschaetse, K.; Bruynooghe, M.; Warren, DHD; Szeredi, P., A practical technique for detecting non-terminating queries for a restricted class of Horn clauses, using directed, weighted graphs, Proceedings of the 7th International Conference on Logic Programming (ICLP’90), 649-663 (1990), New York: MIT, New York |
| [28] | Shen, Y-D, An extended variant of atoms loop check for positive logic programs, New Gen Comput., 15, 2, 187-204 (1997) · doi:10.1007/BF03037237 |
| [29] | 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) |
| [30] | Terese, Term Rewriting Systems (2003), Cambridge: Cambridge University Press, Cambridge · Zbl 1030.68053 |
| [31] | The Annual International Termination Competition. http://termination-portal.org/wiki/Termination_Competition |
| [32] | Termination Problems Data Base. http://termination-portal.org/wiki/TPDB |
| [33] | Waldmann, J.; van Oostrom, V., Matchbox: a tool for match-bounded string rewriting, Proceedings of the 15th International Conference on Rewriting Techniques and Applications (RTA’04), 85-94 (2004), Berlin: Springer, Berlin · doi:10.1007/978-3-540-25979-4_6 |
| [34] | 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) |
| [35] | Yamada, A.: NaTT (Nagoya Termination Tool). https://www.trs.css.i.nagoya-u.ac.jp/NaTT/ (2023) |
| [36] | 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) |
| [37] | Zantema, H., Termination of string rewriting proved automatically, J. Automat. Reason., 34, 2, 105-139 (2005) · Zbl 1102.68649 · doi:10.1007/s10817-005-6545-0 |
| [38] | Zantema, H., Geser, A.: Non-looping rewriting. Universiteit Utrecht. UU-CS, Department of Computer Science. Utrecht University, The Netherlands (1996) |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
