Tuple interpretations for termination of term rewriting. (English) Zbl 1511.68135
Summary: Interpretation methods constitute a foundation of the termination analysis of term rewriting. From time to time, remarkable instances of interpretation methods appeared, such as polynomial interpretations, matrix interpretations, arctic interpretations, and their variants. In this paper, we introduce a general framework, the tuple interpretation method, that subsumes these variants as well as many previously unknown interpretation methods as instances. Employing the notion of derivers, we prove the soundness of the proposed method in an elegant way. We implement the proposed method in the termination prover NaTT and verify its significance through experiments.
MSC:
| 68Q42 | Grammars and rewriting systems |
Software:
StarExec; CeTA; AProVE; z3; Nagoya Termination Tool; NaTT; Tyrolean; CiME; MU-TERM; CoLoR; TPDBReferences:
| [1] | Arts, T.; Giesl, J., Termination of term rewriting using dependency pairs, Theor. Comput. Sci., 236, 1-2, 133-178 (2000) · Zbl 0938.68051 · doi:10.1016/S0304-3975(99)00207-8 |
| [2] | Baader, F.; Nipkow, T., Term Rewriting and All That (1998), Cambridge: Cambridge University Press, Cambridge · Zbl 0948.68098 · doi:10.1017/CBO9781139172752 |
| [3] | Barrett, C.W., Tinelli, C.: Satisfiability modulo theories. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 305-343. Springer, Cham (2018). doi:10.1007/978-3-319-10575-8_11 · Zbl 1392.68379 |
| [4] | Ben-Amram, A.M., Codish, M.: A SAT-based approach to size change termination with global ranking functions. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 218-232. Springer, Heidelberg (2008). doi:10.1007/978-3-540-78800-3_16 · Zbl 1134.68398 |
| [5] | Blanqui, F.; Koprowski, A., CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates, Math. Struct. Comput. Sci., 21, 4, 827-859 (2011) · Zbl 1223.68101 · doi:10.1017/S0960129511000120 |
| [6] | Contejean, É., Courtieu, P., Forest, J., Pons, O., Urbain, X.: Automated certified proofs with CiME3. In: Schmidt-Schauß, M. (ed.) RTA 2011. LIPIcs, vol. 10, pp. 21-30. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl (2011). doi:10.4230/LIPIcs.RTA.2011.21 · Zbl 1236.68219 |
| [7] | Courtieu, P., Gbedo, G., Pons, O.: Improved matrix interpretation. In: van Leeuwen, J., Muscholl, A., Peleg, D., Pokorný, J., Rumpe, B. (eds.) SOFSEM 2010. LNCS, vol. 5901, pp. 283-295. Springer, Heidelberg (2010). doi:10.1007/978-3-642-11266-9_24 · Zbl 1274.68148 |
| [8] | de Moura, L.M., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337-340. Springer, Heidelberg (2008). doi:10.1007/978-3-540-78800-3_24 |
| [9] | Dershowitz, N.: 33 examples of termination. In: Comon, H., Jounnaud, J.P. (eds.) Term Rewriting. pp. 16-26. Springer, Cham (1995). doi:10.1007/3-540-59340-3_2 |
| [10] | Endrullis, J.; Waldmann, J.; Zantema, H., Matrix interpretations for proving termination of term rewriting, J. Autom. Reason., 40, 2-3, 195-220 (2008) · Zbl 1139.68049 · doi:10.1007/s10817-007-9087-9 |
| [11] | Fuhs, C., Giesl, J., Middeldorp, A., Schneider-Kamp, P., Thiemann, R., Zankl, H.: Maximal termination. In: Voronkov, A. (ed.) RTA 2008. LNCS, vol. 5117, pp. 110-125. Springer, Heidelberg (2008). doi:10.1007/978-3-540-70590-1_8 · Zbl 1145.68446 |
| [12] | Giesl, J., Thiemann, R., Schneider-Kamp, P.: The dependency pair framework: Combining techniques for automated termination proofs. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS, vol. 3452, pp. 301-331. Springer, Heidelberg (2004). doi:10.1007/978-3-540-32275-7_21 · Zbl 1108.68477 |
| [13] | Giesl, J.; Thiemann, R.; Schneider-Kamp, P.; Falke, S., Mechanizing and improving dependency pairs, J. Autom. Reason., 37, 3, 155-203 (2006) · Zbl 1113.68088 · doi:10.1007/s10817-006-9057-7 |
| [14] | 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. Autom. Reason., 58, 1, 3-31 (2017) · Zbl 1409.68255 · doi:10.1007/s10817-016-9388-y |
| [15] | Giesl, J., Rubio, A., Sternagel, C., Waldmann, J., Yamada, A.: The termination and complexity competition. In: Beyer, D., Huisman, M., Kordon, F., Steffen, B. (eds.) TACAS 2019 (3). LNCS, vol. 11429, pp. 156-166. Springer, Cham (2019). doi:10.1007/978-3-030-17502-3_10 |
| [16] | Gutiérrez, R., Lucas, S.: mu-term: Verify termination properties automatically (system description). In: Peltier, N., Sofronie-Stokkermans, V. (eds.) IJCAR 2020 (2). LNCS, vol. 12167, pp. 436-447. Springer, Cham (2020). doi:10.1007/978-3-030-51054-1_28 · Zbl 07614689 |
| [17] | Hirokawa, N., Middeldorp, A.: Dependency pairs revisited. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol. 3091, pp. 249-268. Springer, Heidelberg (2004). doi:10.1007/978-3-540-25979-4_18 · Zbl 1187.68275 |
| [18] | Hirokawa, N., Middeldorp, A.: Polynomial interpretations with negative coefficients. In: Buchberger, B., Campbell, J.A. (eds.) AISC 2004. LNAI, vol. 3249, pp. 185-198. Springer, Heidelberg (2004). doi:10.1007/978-3-540-30210-0_16 · Zbl 1109.68501 |
| [19] | Hofbauer, D., Waldmann, J.: Termination of string rewriting with matrix interpretations. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol. 4098, pp. 328-342. Springer, Heidelberg (2006). doi:10.1007/11805618_25 · Zbl 1151.68447 |
| [20] | Jouannaud, J., Rubio, A.: The higher-order recursive path ordering. In: LICS 1999, pp. 402-411. IEEE Computer Society (1999). doi:10.1109/LICS.1999.782635 |
| [21] | Kop, C., Vale, D.: Tuple interpretations for higher-order complexity. In: Kobayashi, N. (ed.) FSCD 2021. LIPIcs, vol. 195, pp. 31:1-31:22. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Wadern (2021). doi:10.4230/LIPIcs.FSCD.2021.31 · Zbl 07700636 |
| [22] | Kop, C., van Raamsdonk, F.: Dynamic dependency pairs for algebraic functional systems. Log. Methods Comput. Sci. (2012). doi:10.2168/LMCS-8(2:10)2012 · Zbl 1242.68136 |
| [23] | Koprowski, A.; Waldmann, J., Max/plus tree automata for termination of term rewriting, Acta Cybern., 19, 2, 357-392 (2009) · Zbl 1224.68041 |
| [24] | Korp, M., Sternagel, C., Zankl, H., Middeldorp, A.: Tyrolean Termination Tool 2. In: Treinen, R. (ed.) RTA 2009. LNCS, vol. 5595, pp. 295-304. Springer, Heidelberg (2009). doi:10.1007/978-3-642-02348-4_21 |
| [25] | Kusakari, K., Nakamura, M., Toyama, Y.: Argument filtering transformation. In: Nadathur, G. (ed.) PPDP 1999. LNCS, vol. 1702, pp. 47-61. Springer, Heidelberg (1999). doi:10.1007/10704567_3 · Zbl 0953.68068 |
| [26] | Lankford, D.: Canonical algebraic simplification in computational logic. Tech. Rep. ATP-25, University of Texas (1975) |
| [27] | Lucas, S.; Gutiérrez, R., Automatic synthesis of logical models for order-sorted first-order theories, J. Autom. Reason., 60, 4, 465-501 (2018) · Zbl 1398.68095 · doi:10.1007/s10817-017-9419-3 |
| [28] | Manna, Z., Ness, S.: On the termination of Markov algorithms. In: The 3rd Hawaii International Conference on System Science, pp. 789-792 (1970) |
| [29] | Sternagel, C., Thiemann, R.: The certification problem format. In: Benzmüller, C., Paleo, B.W. (eds.) UITP 2014. EPTCS, vol. 167, pp. 61-72 (2014). doi:10.4204/EPTCS.167.8 |
| [30] | Sternagel, C., Thiemann, R.: Formalizing monotone algebras for certification of termination and complexity proofs. In: Dowek, G. (ed.) RTA-TLCA 2014. LNCS, vol. 8560, pp. 441-455. Springer, Heidelberg (2014). doi:10.1007/978-3-319-08918-8_30 · Zbl 1416.68180 |
| [31] | Stump, A., Sutcliffe, G., Tinelli, C.: StarExec: A cross-community infrastructure for logic solving. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR. LNCS, vol. 8562, pp. 367-373. Springer, Cham (2014). doi:10.1007/978-3-319-08587-6_28 |
| [32] | Thiemann, R., Sternagel, C.: Certification of termination proofs using CeTA. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 452-468. Springer, Heidelberg (2009). doi:10.1007/978-3-642-03359-9_31 · Zbl 1252.68265 |
| [33] | Thiemann, R., Schöpf, J., Sternagel, C., Yamada, A.: Certifying the Weighted Path Order (Invited Talk). In: Ariola, Z.M. (ed.) FSCD 2020. LIPIcs, vol. 167, pp. 4:1-4:20. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, Dagstuhl (2020). doi:10.4230/LIPIcs.FSCD.2020.4 |
| [34] | TPDB: The termination problem data base. http://termination-portal.org/wiki/TPDB |
| [35] | Watson, T., Goguen, J., Thatcher, J., Wagner, E.: An initial algebra approach to the specification, correctness, and implementation of abstract data types. In: Current Trends in Programming Methodology. Prentice Hall, Englewood Cliffs (1976) |
| [36] | Yamada, A.: Multi-dimensional interpretations for termination of term rewriting. In: Platzer, A., Sutcliffe, G. (eds.) CADE-28. LNCS, vol. 12699, pp. 273-290. Springer, Cham (2021). doi:10.1007/978-3-030-79876-5_16 · Zbl 1540.68115 |
| [37] | Yamada, A., Kusakari, K., Sakabe, T.: Nagoya Termination Tool. In: Dowek, G. (ed.) RTA-TLCA 2014. LNCS, vol. 8560, pp. 466-475. Springer, Heidelberg (2014). doi:10.1007/978-3-319-08918-8_32 · Zbl 1416.68183 |
| [38] | Yamada, A.; Kusakari, K.; Sakabe, T., A unified order for termination proving, Sci. Comput. Program., 111, 110-134 (2015) · doi:10.1016/j.scico.2014.07.009 |
| [39] | Zantema, H., Termination of term rewriting: interpretation and type elimination, J. Symb. Comput., 17, 1, 23-50 (1994) · Zbl 0810.68087 · doi:10.1006/jsco.1994.1003 |
| [40] | Zantema, H., The termination hierarchy for term rewriting, Appl. Algebr. Eng. Commun. Comput., 12, 1-2, 3-19 (2001) · Zbl 0973.68099 · doi:10.1007/s002000100061 |
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.
