Constant runtime complexity of term rewriting is semi-decidable. (English) Zbl 1478.68111
Summary: We prove that it is semi-decidable whether the runtime complexity of a term rewrite system is constant. Our semi-decision procedure exploits that constant runtime complexity is equivalent to termination of a restricted form of narrowing, which can be examined by considering finitely many start terms. We implemented our semi-decision procedure in the tool AProVE to show its efficiency and its success for systems where state-of-the-art complexity analysis tools fail.
MSC:
| 68Q42 | Grammars and rewriting systems |
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
| 68Q25 | Analysis of algorithms and problem complexity |
Keywords:
computational complexity; decidability; formal methods; program correctness; term rewritingReferences:
| [2] | Alpuente, M.; Escobar, S.; Iborra, J., Termination of narrowing revisited, Theor. Comput. Sci., 410, 46, 4608-4625, (2009) · Zbl 1187.68271 |
| [3] | Avanzini, M.; Moser, G.; Schaper, M., tct: Tyrolean complexity tool, (TACAS’16, LNCS, vol. 9636, (2016)), 407-423 |
| [4] | Baader, F.; Nipkow, T., Term rewriting and all that, (1998), Cambridge University Press · Zbl 0948.68098 |
| [5] | Bouchard, C.; Gero, K. A.; Lynch, C.; Narendran, P., On forward closure and the finite variant property, (FroCoS’13, LNCS, vol. 8152, (2013)), 327-342 · Zbl 1398.68271 |
| [6] | Frohn, F.; Giesl, J., Complexity analysis for Java with aprove, (iFM’17, LNCS, vol. 10510, (2017)), 85-101 · Zbl 1498.68065 |
| [7] | Frohn, F.; Giesl, J.; Hensel, J.; Aschermann, C.; Ströder, T., Lower bounds for runtime complexity of term rewriting, J. Autom. Reason., 59, 1, 121-163, (2017) · Zbl 1409.68254 |
| [8] | Giesl, J.; Ströder, T.; Schneider-Kamp, P.; Emmes, F.; Fuhs, C., Symbolic evaluation graphs and term rewriting: a general methodology for analyzing logic programs, (PPDP’12, (2012)), 1-12 |
| [9] | 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 |
| [10] | Hirokawa, N.; Moser, G., Automated complexity analysis based on the dependency pair method, (IJCAR’08, LNCS, vol. 5195, (2008)), 364-379 · Zbl 1165.68390 |
| [11] | Hofbauer, D.; Lautemann, C., Termination proofs and the length of derivations, (RTA’89, LNCS, vol. 355, (1989)), 167-177 · Zbl 1503.68116 |
| [12] | Hughes, C. E.; Selkow, S. M., The finite power property for context-free languages, Theor. Comput. Sci., 15, 111-114, (1981) · Zbl 0472.68037 |
| [13] | Hullot, J. M., Canonical forms and unification, (CADE’80, LNCS, vol. 87, (1980)), 318-334 · Zbl 0441.68108 |
| [14] | Moser, G.; Schaper, M., From jinja bytecode to term rewriting: a complexity reflecting transformation · Zbl 1395.68160 |
| [15] | 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 |
| [16] | Oops |
| [17] | TermComp · Zbl 1465.68282 |
| [18] | TPDB |
| [19] | Zankl, H.; Korp, M., Modular complexity analysis for term rewriting, Log. Methods Comput. Sci., 10, 1:19, 1-33, (2014) · Zbl 1326.68172 |
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.
