Lower bounds for runtime complexity of term rewriting. (English) Zbl 1409.68254
Summary: We present the first approach to deduce lower bounds for (worst-case) runtime complexity of term rewrite systems (TRSs) automatically. Inferring lower runtime bounds is useful to detect bugs and to complement existing methods that compute upper complexity bounds. Our approach is based on two techniques: the induction technique generates suitable families of rewrite sequences and uses induction proofs to find a relation between the length of a rewrite sequence and the size of the first term in the sequence. The loop detection technique searches for “decreasing loops”. Decreasing loops generalize the notion of loops for TRSs, and allow us to detect families of rewrite sequences with linear, exponential, or infinite length. We implemented our approach in the tool AProVE and evaluated it by extensive experiments.
MSC:
| 68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
| 68Q17 | Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) |
| 68Q25 | Analysis of algorithms and problem complexity |
| 68Q42 | Grammars and rewriting systems |
References:
| [1] | Albert, E., Genaim, S., Masud, A.N.: On the inference of resource usage upper and lower bounds. ACM Trans. Comput. Log. 14(3), 22 (2013) · Zbl 1353.68045 |
| [2] | AProVE. http://aprove.informatik.rwth-aachen.de/eval/lowerbounds-journal/ |
| [3] | Avanzini, M., Moser, G.: A combination framework for complexity. In: Proceedings of RTA ’13. LIPIcs 21, pp. 55-70 (2013) · Zbl 1356.68092 |
| [4] | Avanzini, M., Moser, G., Schaper, M.: \[{\sf TcT}\] TcT: Tyrolean complexity tool. In: Proceedings of TACAS ’16. LNCS 9636, pp. 407-423 (2016) · Zbl 0388.68003 |
| [5] | Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998) · Zbl 0948.68098 · doi:10.1017/CBO9781139172752 |
| [6] | Boyer, Robert S., Moore, J.S.: A Computational Logic. Academic Press, Cambridge (1979) · Zbl 0448.68020 |
| [7] | de Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: Proceedings of TACAS ’08. LNCS 4963, pp. 337-340 (2008) · Zbl 1102.68649 |
| [8] | Emmes, F., Enger, T., Giesl, J.: Proving non-looping non-termination automatically. In: Proceedings of IJCAR ’12. LNAI 7364, pp. 225-240 (2012) · Zbl 1358.68157 |
| [9] | Frohn, F., Giesl, J., Hensel, J., Aschermann, C., Ströder, T.: Inferring lower bounds for runtime complexity. In: Proceedings of RTA ’15. LIPIcs 36, pp. 334-349 (2015) · Zbl 1366.68116 |
| [10] | Frohn, F., Naaf, M., Hensel, J., Brockschmidt, M., Giesl, J.: Lower runtime bounds for integer programs. In: Proceedings of IJCAR ’16. LNAI 9706, pp. 550-567 (2016) · Zbl 1475.68134 |
| [11] | Fuhs, C., Giesl, J., Parting, M., Schneider-Kamp, P., Swiderski, S.: Proving termination by dependency pairs and inductive theorem proving. J. Autom. Reason. 47(2), 133-160 (2011) · Zbl 1243.68267 · doi:10.1007/s10817-010-9215-9 |
| [12] | Geser, A., Hofbauer, D., Waldmann, J.: Termination proofs for string rewriting systems via inverse match-bounds. J. Autom. Reason. 34(4), 365-385 (2005) · Zbl 1105.68054 · doi:10.1007/s10817-005-9024-8 |
| [13] | Giesl, J., Thiemann, R., Schneider-Kamp, P.: Proving and disproving termination of higher-order functions. In: Proceedings of FroCoS ’05. LNAI 3717, pp. 216-231 (2005) · Zbl 1171.68714 |
| [14] | Giesl, J., Raffelsieper, M., Schneider-Kamp, P., Swiderski, S., Thiemann, R.: Automated termination proofs for Haskell by term rewriting. ACM Trans. Program. Lang. Syst. 33(2), 7 (2011) · Zbl 1151.68444 |
| [15] | 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 \[{{\sf AProVE}}\] AProVE. J. Autom. Reason (to appear). Preliminary version appeared in Proceedings of IJCAR ’14. LNAI 8562, pp. 184-191 (2014) · Zbl 1409.68255 |
| [16] | Hirokawa, N., Moser, G.: Automated complexity analysis based on the dependency pair method. In: Proceedings of IJCAR ’08. LNAI 5195, pp. 364-379 (2008) · Zbl 1165.68390 |
| [17] | Hofbauer, D., Lautemann, C.: Termination proofs and the length of derivations. In: Proceedings of RTA ’89. LNCS 355, pp. 167-177 (1989) · Zbl 1503.68116 |
| [18] | Hofbauer, D., Waldmann, J.: Constructing lower bounds on the derivational complexity of rewrite systems. Slides of a Talk at the 2nd Workshop on Proof Theory and Rewriting. http://www.imn.htwk-leipzig.de/ waldmann/talk/10/pr/main.pdf (2010) · Zbl 1154.68436 |
| [19] | Hofmann, M., Moser, G.: Amortised resource analysis and typed polynomial interpretations. In: Proceedings of RTA-TLCA ’14. LNCS 8560, pp. 272-286 (2014) · Zbl 1416.68093 |
| [20] | Hooper, P.K.: The undecidability of the Turing machine immortality problem. J. Symb. Log. 31(2), 219-234 (1966) · Zbl 0173.01201 · doi:10.2307/2269811 |
| [21] | Knuth, D.: Johann Faulhaber and sums of powers. Math. Comput. 61(203), 277-294 (1993) · Zbl 0797.11026 · doi:10.1090/S0025-5718-1993-1197512-7 |
| [22] | Lynch, C., Morawska, B.: Basic syntactic mutation. In: Proceedings of CADE ’18. LNAI 2392, pp. 471-485 (2002) · Zbl 1072.68581 |
| [23] | Milner, R.: A theory of type polymorphism in programming. J. Comput. Syst. Sci. 17(3), 348-375 (1978) · Zbl 0388.68003 · doi:10.1016/0022-0000(78)90014-4 |
| [24] | Moser, G., Schnabl, A.: The derivational complexity induced by the dependency pair method. Log. Methods Comput. Sci. 7(3:01), 1-38 (2011) · Zbl 1237.68109 |
| [25] | Noschinski, L., Emmes, F., Giesl, J.: Analyzing innermost runtime complexity of term rewriting by dependency pairs. J. Autom. Reason. 51(1), 27-56 (2013) · Zbl 1314.68174 · doi:10.1007/s10817-013-9277-6 |
| [26] | Otto, C., Brockschmidt, M., von Essen, C., Giesl, J.: Automated termination analysis of Java Bytecode by term rewriting. In: Proceedings of RTA ’10. LIPIcs 6, pp. 259-276 (2010) · Zbl 1236.68145 |
| [27] | Payet, É.: Loop detection in term rewriting using the eliminating unfoldings. Theor. Comput. Sci. 403(2-3), 307-327 (2008) · Zbl 1154.68436 · doi:10.1016/j.tcs.2008.05.013 |
| [28] | Termination Comp.http://termination-portal.org/wiki/Termination_Competition |
| [29] | Waldmann, J.: Matchbox: A tool for match-bounded string rewriting. In: Proceedings of RTA ’04. LNCS 3091, pp. 85-94 (2004) · Zbl 1102.68649 |
| [30] | Waldmann, J.: Automatic termination. In: Proceedings of RTA ’09. LNCS 5595, pp. 1-16 (2009) · Zbl 1242.68143 |
| [31] | Zankl, H., Sternagel, C., Hofbauer, D., Middeldorp, A.: Finding and certifying loops. In: Proceedings of SOFSEM ’10. LNCS 5901, pp. 755-766 (2010) · Zbl 1274.68153 |
| [32] | Zankl, H., Korp, M.: Modular complexity analysis for term rewriting. Log. Methods Comput. Sci. 10(1:19), 1-33 (2014) · Zbl 1326.68172 |
| [33] | Zantema, H.: Termination of term rewriting: interpretation and type elimination. J. Symbol. Comput. 17(1), 23-50 (1994) · Zbl 0810.68087 · doi:10.1006/jsco.1994.1003 |
| [34] | Zantema, H.: Termination of string rewriting proved automatically. J. Autom. Reason. 34(2), 105-139 (2005) · Zbl 1102.68649 · doi:10.1007/s10817-005-6545-0 |
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.
