×

A combination framework for complexity. (English) Zbl 1339.68135

Summary: In this paper we present a combination framework for the automated polynomial complexity analysis of term rewrite systems. The framework covers both derivational and runtime complexity analysis, and is employed as theoretical foundation in the automated complexity tool TCT. We present generalisations of powerful complexity techniques, notably a generalisation of complexity pairs and (weak) dependency pairs. Finally, we also present a novel technique, called dependency graph decomposition, that in the dependency pair setting greatly increases modularity.

MSC:

68Q42 Grammars and rewriting systems
68Q25 Analysis of algorithms and problem complexity
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)

Software:

Tyrolean
PDFBibTeX XMLCite
Full Text: DOI

References:

[2] Ben-Amram, A.; Vainer, M., Bounded termination of monotonicity-constraint transition systems, CoRR
[3] Bonfante, G.; Cichon, A.; Marion, J.-Y.; Touzet, H., Algorithms with polynomial interpretation termination proof, J. Funct. Program., 11, 1, 33-53 (2001) · Zbl 0987.68042
[4] Hofbauer, D.; Lautemann, C., Termination proofs and the length of derivations, (Proc. of 3rd International Conference on Rewriting Techniques and Applications. Proc. of 3rd International Conference on Rewriting Techniques and Applications, LNCS, vol. 355 (1989), Springer), 167-177 · Zbl 1503.68116
[5] Hirokawa, N.; Moser, G., Automated complexity analysis based on the dependency pair method, (Proc. of 4th International Joint Conference on Automated Reasoning. Proc. of 4th International Joint Conference on Automated Reasoning, LNAI, vol. 5195 (2008), Springer), 364-380 · Zbl 1165.68390
[6] Avanzini, M.; Moser, G., Closing the gap between runtime complexity and polytime computability, (Proc. of 21st International Conference on Rewriting Techniques and Applications. Proc. of 21st International Conference on Rewriting Techniques and Applications, LIPIcs, vol. 6 (2010), Leibniz-Zentrum für Informatik), 33-48 · Zbl 1236.68119
[7] Dal Lago, U.; Martini, S., On constructor rewrite systems and the lambda calculus, Log. Methods Comput. Sci., 8, 3, 1-27 (2012) · Zbl 1256.68091
[8] Avanzini, M.; Eguchi, N.; Moser, G., A new order-theoretic characterisation of the polytime computable functions, Theor. Comput. Sci., 585, 3-24 (2015) · Zbl 1327.68142
[10] Moser, G.; Schnabl, A.; Waldmann, J., Complexity analysis of term rewriting based on matrix and context dependent interpretations, (Proc. of 28th Conference on Foundations of Software Technology and Theoretical Computer Science. Proc. of 28th Conference on Foundations of Software Technology and Theoretical Computer Science, LIPIcs (2008), Leibniz-Zentrum für Informatik), 304-315 · Zbl 1248.68278
[11] Noschinski, L.; Emmes, F.; Giesl, J., A dependency pair framework for innermost complexity analysis of term rewrite systems, (Proc. of 23rd CADE. Proc. of 23rd CADE, LNAI (2011), Springer), 422-438 · Zbl 1314.68173
[12] Avanzini, M., POP* and semantic labeling using SAT, (Interfaces: Explorations in Logic, Language and Computation, ESSLLI 2008 and ESSLLI 2009 Student Sessions. Selected Papers. Interfaces: Explorations in Logic, Language and Computation, ESSLLI 2008 and ESSLLI 2009 Student Sessions. Selected Papers, LNCS, vol. 6211 (2010), Springer), 155-166 · Zbl 1286.68257
[13] Zankl, H.; Korp, M., Modular complexity analysis via relative complexity, (Proc. of 21st International Conference on Rewriting Techniques and Applications. Proc. of 21st International Conference on Rewriting Techniques and Applications, LIPIcs, vol. 6 (2010), Leibniz-Zentrum für Informatik), 385-400 · Zbl 1236.68158
[14] Moser, G., Proof theory at work: complexity analysis of term rewrite systems, habilitation thesis, CoRR
[15] Hirokawa, N.; Moser, G., Complexity, graphs, and the dependency pair method, (Proc. of 15th International Conferences on Logic for Programming, Artificial Intelligence and Reasoning (2008)), 652-666 · Zbl 1182.68095
[16] Hirokawa, N.; Moser, G., Automated complexity analysis based on the dependency pair method, CoRR · Zbl 1165.68390
[17] Avanzini, M.; Moser, G., Tyrolean complexity tool: features and usage, (Proc. of 24th International Conference on Rewriting Techniques and Applications. Proc. of 24th International Conference on Rewriting Techniques and Applications, LIPIcs, vol. 21 (2013), Leibniz-Zentrum für Informatik), 71-80 · Zbl 1356.68093
[18] Hirokawa, N.; Moser, G., Automated complexity analysis based on context-sensitive rewriting, (Proc. of 25th International Conference on Rewriting Techniques and Applications and the 12th International Conference on Typed Lambda Calculi and Applications (2014)) · Zbl 1416.68092
[19] Gulwani, S.; Zuleger, F., The reachability-bound problem, (Proc. of the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation (2010), ACM), 292-304
[20] Zuleger, F.; Gulwani, S.; Sinn, M.; Veith, H., Bound analysis of imperative programs with the size-change abstraction, (Proc. of 18th International Symposium on Static Analysis. Proc. of 18th International Symposium on Static Analysis, LNCS, vol. 6887 (2011), Springer), 280-297
[21] Hoffmann, J.; Aehlig, K.; Hofmann, M., Resource aware ML, (Proc. of 24th International Conference on Computer Aided Verification. Proc. of 24th International Conference on Computer Aided Verification, LNCS, vol. 7358 (2012), Springer), 781-786
[22] Bonfante, G.; Marion, J.-Y.; Péchoux, R., Quasi-interpretation synthesis by decomposition and an application to higher-order programs, (Proc. of 4th International Conference on Theoretical Aspects of Computing. Proc. of 4th International Conference on Theoretical Aspects of Computing, LNCS, vol. 4711 (2007), Springer), 410-424 · Zbl 1147.68431
[23] Avanzini, M.; Moser, G., A combination framework for complexity, (Proc. of 24th International Conference on Rewriting Techniques and Applications. Proc. of 24th International Conference on Rewriting Techniques and Applications, LIPIcs, vol. 21 (2013), Leibniz-Zentrum für Informatik), 55-70 · Zbl 1356.68092
[24] Avanzini, M., Verifying polytime computability automatically (2013), University of Innsbruck, available at
[25] Choppy, C.; Kaplan, S.; Soria, M., Complexity analysis of term-rewriting systems, Theor. Comput. Sci., 67, 2-3, 261-282 (1989) · Zbl 0686.68031
[26] Bellantoni, S.; Cook, S., A new recursion-theoretic characterization of the polytime functions, Comput. Complex., 2, 2, 97-110 (1992) · Zbl 0766.68037
[27] Hoffmann, J.; Aehlig, K.; Hofmann, M., Multivariate amortized resource analysis, (Proc. of 38th Annual Symposium on Principles of Programming Languages (2011), ACM), 357-370 · Zbl 1284.68132
[28] Albert, E.; Arenas, P.; Genaim, S.; Gómez-Zamalloa, M.; Puebla, G.; Ramírez, D.; Román, G.; Zanardini, D., Termination and cost analysis with COSTA and its user interfaces, Electron. Notes Theor. Comput. Sci., 258, 1, 109-121 (2009)
[29] Alias, C.; Darte, A.; Feautrier, P.; Gonnord, L., Multi-dimensional rankings, program termination, and complexity bounds of flowchart programs, (Proc. 17th SAS. Proc. 17th SAS, LNCS, vol. 6337 (2010)), 117-133 · Zbl 1306.68017
[30] Hofmann, M.; Rodriguez, D., Automatic type inference for amortised heap-space analysis, (Proc. of 22nd European Symposium on Programming. Proc. of 22nd European Symposium on Programming, LNCS, vol. 7792 (2013), Springer), 593-613 · Zbl 1381.68041
[31] Baader, F.; Nipkow, T., Term Rewriting and All That (1998), Cambridge University Press
[32] Thiemann, R., The DP framework for proving termination of term rewriting (2007), University of Aachen, available as Technical report AIB-2007-17
[33] Korp, M.; Sternagel, C.; Zankl, H.; Middeldorp, A., Tyrolean termination tool 2, (Proc. of 20th International Conference on Rewriting Techniques and Applications. Proc. of 20th International Conference on Rewriting Techniques and Applications, LNCS, vol. 5595 (2009), Springer), 295-304
[34] 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
[35] Giesl, J.; Arts, T.; Ohlebusch, E., Modular termination proofs for rewriting using dependency pairs, J. Symb. Comput., 34, 21-58 (2002) · Zbl 1010.68073
[36] Arts, T.; Giesl, J., Termination of term rewriting using dependency pairs, Theor. Comput. Sci., 236, 1-2, 133-178 (2000) · Zbl 0938.68051
[38] Hirokawa, N.; Middeldorp, A., Dependency pairs revisited, (Proc. of 15th International Conference on Rewriting Techniques and Applications. Proc. of 15th International Conference on Rewriting Techniques and Applications, LNCS, vol. 3091 (2004), Springer), 249-268 · Zbl 1187.68275
[39] Lee, C. S.; Jones, N. D.; Ben-Amram, A. M., The size-change principle for program termination, (Proc. of 28th Annual Symposium on Principles of Programming Languages (2001), ACM), 81-92 · Zbl 1323.68216
[40] Hirokawa, N.; Middeldorp, A.; Zankl, H., Uncurrying for termination and complexity, J. Autom. Reason., 50, 3, 279-315 (2013) · Zbl 1286.68262
[41] Middeldorp, A.; Moser, G.; Neurauter, F.; Waldmann, J.; Zankl, H., Joint spectral radius theory for automated complexity analysis of rewrite systems, (Proc. of 4th International Conference on Algebraic Informatics. Proc. of 4th International Conference on Algebraic Informatics, LNCS, vol. 6742 (2011), Springer), 1-20 · Zbl 1307.68042
[42] Giesl, J.; Schneider-Kamp, P.; Thiemann, R., Automatic termination proofs in the dependency pair framework, (Proc. of 3rd International Joint Conference on Automated Reasoning. Proc. of 3rd International Joint Conference on Automated Reasoning, LNCS, vol. 4130 (2006), Springer), 281-286
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.