Match-bounds revisited. (English) Zbl 1192.68399
Summary: The use of automata techniques to prove the termination of string rewrite systems and left-linear term rewrite systems is advocated by Geser et al. in a recent sequence of papers. We extend their work to non-left-linear rewrite systems. The key to this extension is the introduction of so-called raise rules and the use of tree automata that are not quite deterministic. Furthermore, to increase the applicability of the method we show how it can be incorporated into the dependency pair framework. To achieve this we introduce two new enrichments which take the special properties of dependency pair problems into account.
MSC:
| 68Q42 | Grammars and rewriting systems |
References:
| [1] | Geser, A.; Hofbauer, D.; Waldmann, J., Match-bounded string rewriting systems, Applicable Algebra in Engineering, Communication and Computing, 15, 3-4, 149-171 (2004) · Zbl 1101.68048 |
| [2] | Geser, A.; Hofbauer, D.; Waldmann, J.; Zantema, H., On tree automata that certify termination of left-linear term rewriting systems, Information and Computation, 205, 4, 512-534 (2007) · Zbl 1112.68077 |
| [3] | J. Endrullis, D. Hofbauer, J. Waldmann, Decomposing terminating rewrite relations, in: Proceedings of the Eighth International Workshop on Termination (WST), 2006, pp. 39-43.; J. Endrullis, D. Hofbauer, J. Waldmann, Decomposing terminating rewrite relations, in: Proceedings of the Eighth International Workshop on Termination (WST), 2006, pp. 39-43. |
| [4] | Geser, A.; Hofbauer, D.; Waldmann, J., Termination proofs for string rewriting systems via inverse match-bounds, Journal of Automated Reasoning, 34, 4, 365-385 (2005) · Zbl 1105.68054 |
| [5] | Geser, A.; Hofbauer, D.; Waldmann, J.; Zantema, H., Finding finite automata that certify termination of string rewriting systems, International Journal of Foundations of Computer Science, 16, 3, 471-486 (2005) · Zbl 1097.68052 |
| [6] | J. Giesl, P. Schneider-Kamp, R. Thiemann, AProVE 1.2: automatic termination proofs in the dependency pair framework, in: Proceedings of the Third International Joint Conference on Automated Reasoning (IJCAR), Lecture Notes in Artificial Intelligence, vol. 4130, 2006, pp. 281-286.; J. Giesl, P. Schneider-Kamp, R. Thiemann, AProVE 1.2: automatic termination proofs in the dependency pair framework, in: Proceedings of the Third International Joint Conference on Automated Reasoning (IJCAR), Lecture Notes in Artificial Intelligence, vol. 4130, 2006, pp. 281-286. |
| [7] | Jambox, Available from: <http://joerg.endrullis.de/; Jambox, Available from: <http://joerg.endrullis.de/ |
| [8] | J. Waldmann, Matchbox: a tool for match-bounded string rewriting, in: Proceedings of the 15th International Conference on Rewriting Techniques and Applications (RTA), Lecture Notes in Computer Science, vol. 3091, 2004, pp. 85-94.; J. Waldmann, Matchbox: a tool for match-bounded string rewriting, in: Proceedings of the 15th International Conference on Rewriting Techniques and Applications (RTA), Lecture Notes in Computer Science, vol. 3091, 2004, pp. 85-94. |
| [9] | Zantema, H., Termination of rewriting proved automatically, Journal of Automated Reasoning, 34, 2, 105-139 (2005) · Zbl 1102.68649 |
| [10] | J. Giesl, R. Thiemann, P. Schneider-Kamp, The dependency pair framework: combining techniques for automated termination proofs, in: Proceedings of the 11th International Conference on Logic Programming and Automated Reasoning (LPAR), Lecture Notes in Artificial Intelligence, vol. 3425, 2004, pp. 301-331.; J. Giesl, R. Thiemann, P. Schneider-Kamp, The dependency pair framework: combining techniques for automated termination proofs, in: Proceedings of the 11th International Conference on Logic Programming and Automated Reasoning (LPAR), Lecture Notes in Artificial Intelligence, vol. 3425, 2004, pp. 301-331. · Zbl 1108.68477 |
| [11] | R. Thiemann, The DP framework for proving termination of term rewriting, Ph.D. Thesis, RWTH Aachen, Available as technical report AIB-2007-17 (2007).; R. Thiemann, The DP framework for proving termination of term rewriting, Ph.D. Thesis, RWTH Aachen, Available as technical report AIB-2007-17 (2007). |
| [12] | M. Korp, A. Middeldorp, Proving termination of rewrite systems using bounds, in: Proceedings of the 18th International Conference on Rewriting Techniques and Applications (RTA), Lecture Notes in Computer Science, vol. 4533, 2007, pp. 273-287.; M. Korp, A. Middeldorp, Proving termination of rewrite systems using bounds, in: Proceedings of the 18th International Conference on Rewriting Techniques and Applications (RTA), Lecture Notes in Computer Science, vol. 4533, 2007, pp. 273-287. · Zbl 1203.68077 |
| [13] | M. Korp, A. Middeldorp, Match-bounds with dependency pairs for proving termination of rewrite systems, in: Proceedings of the Second International Conference on Language and Automata Theory and Applications (LATA), Lecture Notes in Computer Science, vol. 5196, 2008, pp. 321-332.; M. Korp, A. Middeldorp, Match-bounds with dependency pairs for proving termination of rewrite systems, in: Proceedings of the Second International Conference on Language and Automata Theory and Applications (LATA), Lecture Notes in Computer Science, vol. 5196, 2008, pp. 321-332. · Zbl 1156.68430 |
| [14] | Baader, F.; Nipkow, T., Term Rewriting and All That (1998), Cambridge University Press: Cambridge University Press Cambridge |
| [15] | H. Comon, M. Dauchet, R. Gilleron, F. Jacquemard, D. Lugiez, S. Tison, M. Tommasi, Tree automata techniques and applications, 2002. Available from: <www.grappa.univ-lille3.fr/tata; H. Comon, M. Dauchet, R. Gilleron, F. Jacquemard, D. Lugiez, S. Tison, M. Tommasi, Tree automata techniques and applications, 2002. Available from: <www.grappa.univ-lille3.fr/tata |
| [16] | Dershowitz, N., Orderings for term-rewriting systems, Theoretical Computer Science, 17, 3, 279-301 (1982) · Zbl 0525.68054 |
| [17] | T. Genet, Decidable approximations of sets of descendants and sets of normal forms, in: Proceedings of the Ninth International Conference on Rewriting Techniques and Applications (RTA), Lecture Notes in Computer Science, vol. 1379, 1998, pp. 151-165.; T. Genet, Decidable approximations of sets of descendants and sets of normal forms, in: Proceedings of the Ninth International Conference on Rewriting Techniques and Applications (RTA), Lecture Notes in Computer Science, vol. 1379, 1998, pp. 151-165. |
| [18] | A. Middeldorp, Approximating dependency graphs using tree automata techniques, in: Proceedings of the First International Joint Conference on Automated Reasoning (IJCAR), Lecture Notes in Artificial Intelligence, vol. 2083, 2001, pp. 593-610.; A. Middeldorp, Approximating dependency graphs using tree automata techniques, in: Proceedings of the First International Joint Conference on Automated Reasoning (IJCAR), Lecture Notes in Artificial Intelligence, vol. 2083, 2001, pp. 593-610. · Zbl 0988.68162 |
| [19] | Nagaya, T.; Toyama, Y., Decidability for left-linear growing term rewriting systems, Information and Computation, 178, 2, 499-514 (2002) · Zbl 1049.68075 |
| [20] | Arts, T.; Giesl, J., Termination of term rewriting using dependency pairs, Theoretical Computer Science, 236, 1-2, 133-178 (2000) · Zbl 0938.68051 |
| [21] | J. Giesl, R. Thiemann, P. Schneider-Kamp, Proving and disproving termination of higher-order functions, in: Proceedings of the Fifth International Workshop on Frontiers of Combining Systems (FroCoS), Lecture Notes in Artificial Intelligence, vol. 3717, 2005, pp. 216-231.; J. Giesl, R. Thiemann, P. Schneider-Kamp, Proving and disproving termination of higher-order functions, in: Proceedings of the Fifth International Workshop on Frontiers of Combining Systems (FroCoS), Lecture Notes in Artificial Intelligence, vol. 3717, 2005, pp. 216-231. · Zbl 1171.68714 |
| [22] | J. Giesl, R. Thiemann, P. Schneider-Kamp, S. Falke, Improving dependency pairs, in: Proceedings of the 10th International Conference on Logic Programming and Automated Reasoning (LPAR), Lecture Notes in Artificial Intelligence, vol. 2850, 2003, pp. 167-182.; J. Giesl, R. Thiemann, P. Schneider-Kamp, S. Falke, Improving dependency pairs, in: Proceedings of the 10th International Conference on Logic Programming and Automated Reasoning (LPAR), Lecture Notes in Artificial Intelligence, vol. 2850, 2003, pp. 167-182. · Zbl 1273.68320 |
| [23] | Hirokawa, N.; Middeldorp, A., Tyrolean termination tool: techniques and features, Information and Computation, 205, 4, 474-511 (2007) · Zbl 1111.68048 |
| [24] | Giesl, J.; Thiemann, R.; Schneider-Kamp, P.; Falke, S., Mechanizing and improving dependency pairs, Journal of Automated Reasoning, 37, 3, 155-203 (2006) · Zbl 1113.68088 |
| [25] | O. Geupel, Overlap closures and termination of term rewriting systems, Report MIP-8922; O. Geupel, Overlap closures and termination of term rewriting systems, Report MIP-8922 |
| [26] | N. Dershowitz, Termination of linear rewriting systems (preliminary version), in: Proceedings of the Eighth International Colloquium on Automata, Languages and Programming (ICALP), vol. 115, 1981, pp. 448-458.; N. Dershowitz, Termination of linear rewriting systems (preliminary version), in: Proceedings of the Eighth International Colloquium on Automata, Languages and Programming (ICALP), vol. 115, 1981, pp. 448-458. · Zbl 0465.68009 |
| [27] | Tyrolean Termination Tool 2, Available from: <http://cl-informatik.uibk.ac.at/software/ttt2; Tyrolean Termination Tool 2, Available from: <http://cl-informatik.uibk.ac.at/software/ttt2 |
| [28] | Hirokawa, N.; Middeldorp, A., Automating the dependency pair method, Information and Computation, 199, 1-2, 172-199 (2005) · Zbl 1081.68038 |
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.
