Joint spectral radius theory for automated complexity analysis of rewrite systems. (English) Zbl 1307.68042
Winkler, Franz (ed.), Algebraic informatics. 4th international conference, CAI 2011, Linz, Austria, June 21–24, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-21492-9/pbk). Lecture Notes in Computer Science 6742, 1-20 (2011).
Summary: Matrix interpretations can be used to bound the derivational complexity of term rewrite systems. In particular, triangular matrix interpretations over the natural numbers are known to induce polynomial upper bounds on the derivational complexity of (compatible) rewrite systems. Recently two different improvements were proposed, based on the theory of weighted automata and linear algebra. In this paper we strengthen and unify these improvements by using joint spectral radius theory.
For the entire collection see [Zbl 1217.68019].
For the entire collection see [Zbl 1217.68019].
MSC:
| 68Q42 | Grammars and rewriting systems |
| 68Q45 | Formal languages and automata |
| 68Q70 | Algebraic theory of languages and automata |
References:
| [1] | Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998) · Zbl 0948.68098 · doi:10.1017/CBO9781139172752 |
| [2] | Bell, J.: A gap result for the norms of semigroups of matrices. LAA 402, 101–110 (2005) · Zbl 1074.15033 |
| [3] | Droste, M., Kuich, W., Vogler, H. (eds.): Handbook of Weighted Automata. Springer, Heidelberg (2009) · Zbl 1200.68001 |
| [4] | Endrullis, J., Waldmann, J., Zantema, H.: Matrix interpretations for proving termination of term rewriting. JAR 40(2-3), 195–220 (2008) · Zbl 1139.68049 · doi:10.1007/s10817-007-9087-9 |
| [5] | Gebhardt, A., Hofbauer, D., Waldmann, J.: Matrix evolutions. In: WST 2007, pp. 4–8 (2007) |
| [6] | Geser, A., Hofbauer, D., Waldmann, J., Zantema, H.: On tree automata that certify termination of left-linear term rewriting systems. I&C 205(4), 512–534 (2007) · Zbl 1112.68077 |
| [7] | Hirokawa, N., Moser, G.: Automated complexity analysis based on the dependency pair method. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 364–379. Springer, Heidelberg (2008) · Zbl 1165.68390 · doi:10.1007/978-3-540-71070-7_32 |
| [8] | Horn, R., Johnson, C.: Matrix Analysis. Cambridge University Press, Cambridge (1990) · Zbl 0704.15002 |
| [9] | Jungers, R.M., Protasov, V., Blondel, V.D.: Efficient algorithms for deciding the type of growth of products of integer matrices. LAA 428(10), 2296–2311 (2008) · Zbl 1145.65030 |
| [10] | Jungers, R.: The Joint Spectral Radius: Theory and Applications. Springer, Heidelberg (2009) · doi:10.1007/978-3-540-95980-9 |
| [11] | Koprowski, A., Waldmann, J.: Arctic termination...Below zero. In: Voronkov, A. (ed.) RTA 2008. LNCS, vol. 5117, pp. 202–216. Springer, Heidelberg (2008) · Zbl 1145.68450 · doi:10.1007/978-3-540-70590-1_14 |
| [12] | Moser, G.: Proof Theory at Work: Complexity Analysis of Term Rewrite Systems. Habilitation thesis, University of Innsbruck (2009) |
| [13] | Moser, G., Schnabl, A.: The derivational complexity induced by the dependency pair method. LMCS (2011) (to appear), http://arxiv.org/abs/0904.0570 · Zbl 1237.68109 |
| [14] | Moser, G., Schnabl, A., Waldmann, J.: Complexity analysis of term rewriting based on matrix and context dependent interpretations. In: Hariharan, R., Mukund, M., Vinay, V. (eds.) FSTTCS 2008. LIPIcs, vol. 2, pp. 304–315. Schloss Dagstuhl, Dagstuhl (2008) · Zbl 1248.68278 |
| [15] | Neurauter, F., Zankl, H., Middeldorp, A.: Revisiting matrix interpretations for polynomial derivational complexity of term rewriting. In: Fermüller, C.G., Voronkov, A. (eds.) LPAR-17. LNCS(ARCoSS), vol. 6397, pp. 550–564. Springer, Heidelberg (2010) · Zbl 1306.68083 · doi:10.1007/978-3-642-16242-8_39 |
| [16] | Rose, H.E.: Linear Algebra: A Pure Mathematical Approach. Birkhäuser, Basel (2002) · Zbl 1010.15001 · doi:10.1007/978-3-0348-8189-0 |
| [17] | Sakarovitch, J.: Elements of Automata Theory. Cambridge University Press, Cambridge (2009) · Zbl 1188.68177 · doi:10.1017/CBO9781139195218 |
| [18] | Terese: Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science, vol. 55. Cambridge University Press, Cambridge (2003) |
| [19] | Waldmann, J.: olynomially bounded matrix interpretations. In: Lynch, C. (ed.) RTA 2010. LIPIcs, vol. 6, pp. 357–372. Schloss Dagstuhl, Dagstuhl (2010) · Zbl 1236.68155 |
| [20] | Weber, A., Seidl, H.: On the degree of ambiguity of finite automata. TCS 88(2), 325–349 (1991) · Zbl 0738.68059 · doi:10.1016/0304-3975(91)90381-B |
| [21] | Zankl, H., Korp, M.: Modular complexity analysis via relative complexity. In: Lynch, C. (ed.) RTA 2010. LIPIcs, vol. 6, pp. 385–400. Schloss Dagstuhl, Dagstuhl (2010) · Zbl 1236.68158 |
| [22] | Zankl, H., Middeldorp, A.: Satisfiability of non-linear (ir)rational arithmetic. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16. LNCS(LNAI), vol. 6355, pp. 481–500. Springer, Heidelberg (2010) · Zbl 1310.68126 · doi:10.1007/978-3-642-17511-4_27 |
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.
