Sparse tiling through overlap closures for termination of string rewriting. (English) Zbl 1528.68163
Geuvers, Herman (ed.), 4th international conference on formal structures for computation and deduction, FSCD 2019, Dortmund, Germany, June 24–30, 2019. Wadern: Schloss Dagstuhl – Leibniz-Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 131, Article 21, 21 p. (2019).
Summary: A strictly locally testable language is characterized by its set of admissible factors, prefixes and suffixes, called tiles. We over-approximate reachability sets in string rewriting by languages defined by sparse sets of tiles, containing only those that are reachable in derivations. Using the partial algebra defined by a tiling for semantic labeling, we obtain a transformational method for proving local termination. These algebras can be represented efficiently as finite automata of a certain shape. Using a known result on forward closures, and a new characterisation of overlap closures, we can automatically prove termination and relative termination, respectively. We report on experiments showing the strength of the method.
For the entire collection see [Zbl 1414.68005].
For the entire collection see [Zbl 1414.68005].
References:
| [1] | Ronald V. Book and Friedrich Otto. String-rewriting systems. Texts and Monographs in Computer Science. Springer, New York, 1993. · Zbl 0832.68061 |
| [2] | Nachum Dershowitz. Termination of Linear Rewriting Systems. In Shimon Even and Oded Kariv, editors, Automata, Languages and Programming, 8th Colloquium, Acre (Akko), Israel, July 13-17, 1981, Proceedings, volume 115 of LNCS, pages 448-458. Springer, 1981. doi: 10.1007/3-540-10843-2_36. · Zbl 0465.68009 · doi:10.1007/3-540-10843-2_36 |
| [3] | Jörg Endrullis, Roel C. de Vrijer, and Johannes Waldmann. Local Termination: theory and practice. Logical Methods in Computer Science, 6(3), 2010. arXiv:1006.4955. · Zbl 1211.68085 |
| [4] | Bertram Felgenhauer and René Thiemann. Reachability, confluence, and termination analysis with state-compatible automata. Inf. Comput., 253:467-483, 2017. doi:10.1016/j.ic.2016. 06.011. · Zbl 1362.68137 · doi:10.1016/j.ic.2016.06.011 |
| [5] | Thomas Genet. Decidable Approximations of Sets of Descendants and Sets of Normal Forms. In Tobias Nipkow, editor, Rewriting Techniques and Applications, 9th International Conference, RTA-98, Tsukuba, Japan, March 30 -April 1, 1998, Proceedings, volume 1379 of LNCS, pages 151-165. Springer, 1998. doi:10.1007/BFb0052368. · doi:10.1007/BFb0052368 |
| [6] | Alfons Geser, Dieter Hofbauer, and Johannes Waldmann. Match-Bounded String Rewriting Systems. Appl. Algebra Eng. Commun. Comput., 15(3-4):149-171, 2004. doi:10.1007/ s00200-004-0162-8. · Zbl 1101.68048 · doi:10.1007/s00200-004-0162-8 |
| [7] | Alfons Geser and Hans Zantema. Non-looping string rewriting. ITA, 33(3):279-302, 1999. doi:10.1051/ita:1999118. · Zbl 0951.68054 · doi:10.1051/ita:1999118 |
| [8] | Dora Giammaresi and Antonio Restivo. Two-Dimensional Languages. In Arto Salomaa and Grzegorz Rozenberg, editors, Handbook of Formal Languages, volume 3, pages 215-267. Springer, 1997. |
| [9] | Jürgen Giesl, Cornelius Aschermann, Marc Brockschmidt, Fabian Emmes, Florian Frohn, Carsten Fuhs, Jera Hensel, Carsten Otto, Martin Plücker, Peter Schneider-Kamp, Thomas Ströder, Stephanie Swiderski, and René Thiemann. Analyzing Program Termination and Complexity Automatically with AProVE. J. Autom. Reasoning, 58(1):3-31, 2017. doi: 10.1007/s10817-016-9388-y. · Zbl 1409.68255 · doi:10.1007/s10817-016-9388-y |
| [10] | John V. Guttag, Deepak Kapur, and David R. Musser. On Proving Uniform Termination and Restricted Termination of Rewriting Systems. SIAM J. Comput., 12(1):189-214, 1983. doi:10.1137/0212012. · Zbl 0526.68036 · doi:10.1137/0212012 |
| [11] | Miki Hermann. Divergence des systèmes de réécriture et schématisation des ensembles infinis de termes. Habilitation, Université de Nancy, France, March 1994. |
| [12] | Dieter Hofbauer. System description: MultumNonMulta. In A. Middeldorp and R. Thiemann, editors, 15th Intl. Workshop on Termination, WST 2016, Obergurgl, Austria, 2016, Proceedings, page 90, 2016. |
| [13] | Dieter Hofbauer. MultumNonMulta at TermComp 2018. In S. Lucas, editor, 16th Intl. Workshop on Termination, WST 2016, Oxford, U. K., 2018, Proceedings, page 80, 2018. |
| [14] | Martin Korp, Christian Sternagel, Harald Zankl, and Aart Middeldorp. Tyrolean Termination Tool 2. In Ralf Treinen, editor, Rewriting Techniques and Applications, 20th International Conference, RTA 2009, Brasília, Brazil, June 29 -July 1, 2009, Proceedings, volume 5595 of LNCS, pages 295-304. Springer, 2009. doi:10.1007/978-3-642-02348-4_21. · doi:10.1007/978-3-642-02348-4_21 |
| [15] | Dallas S. Lankford and D. R. Musser. A finite termination criterion. Technical report, Information Sciences Institute, Univ. of Southern California, Marina-del-Rey, CA, 1978. |
| [16] | Robert McNaughton and Seymour Papert. Counter-Free Automata. MIT Press, 1971. · Zbl 0232.94024 |
| [17] | Aart Middeldorp, Hitoshi Ohsaki, and Hans Zantema. Transforming Termination by Self-Labelling. In Michael A. McRobbie and John K. Slaney, editors, Automated Deduction -CADE-13, 13th International Conference on Automated Deduction, New Brunswick, NJ, USA, July 30 -August 3, 1996, Proceedings, volume 1104 of LNCS, pages 373-387. Springer, 1996. doi:10.1007/3-540-61511-3_101. · Zbl 1412.68112 · doi:10.1007/3-540-61511-3_101 |
| [18] | Jacques Sakarovitch. Éléments the théorie des automates. Vuibert Informatique, 2003. · Zbl 1178.68002 |
| [19] | Christian Sternagel and Aart Middeldorp. Root-Labeling. In Andrei Voronkov, editor, Rewriting Techniques and Applications, 19th International Conference, RTA 2008, Hagenberg, Austria, July 15-17, 2008, Proceedings, volume 5117 of LNCS, pages 336-350. Springer, 2008. doi:10.1007/978-3-540-70590-1_23. · Zbl 1145.68453 · doi:10.1007/978-3-540-70590-1_23 |
| [20] | Christian Sternagel and René Thiemann. Modular and Certified Semantic Labeling and Unla-beling. In Manfred Schmidt-Schauß, editor, Proceedings of the 22nd International Conference on Rewriting Techniques and Applications, RTA 2011, May 30 -June 1, 2011, Novi Sad, Serbia, volume 10 of LIPIcs, pages 329-344. Schloss Dagstuhl -Leibniz-Zentrum für Informatik, 2011. doi:10.4230/LIPIcs.RTA.2011.329. · Zbl 1236.68151 · doi:10.4230/LIPIcs.RTA.2011.329 |
| [21] | Vincent van Oostrom. Bowls and Beans. CWI puzzle, http://www.phil.uu.nl/ oostrom/ publication/misc.html, accessible via https://web.archive.org/, 2004. |
| [22] | Johannes Waldmann. Efficient Completion of Weighted Automata. In Andrea Corradini and Hans Zantema, editors, Proceedings 9th International Workshop on Computing with Terms and Graphs, TERMGRAPH 2016, Eindhoven, The Netherlands, April 8, 2016., volume 225 of EPTCS, pages 55-62, 2016. doi:10.4204/EPTCS.225.8. · Zbl 1483.68152 · doi:10.4204/EPTCS.225.8 |
| [23] | Yechezkel Zalcstein. Locally testable languages. Journal of Computer and System Sciences, 6(2):151-167, 1972. doi:10.1016/S0022-0000(72)80020-5. · Zbl 0242.68038 · doi:10.1016/S0022-0000(72)80020-5 |
| [24] | Hans Zantema. Termination of Term Rewriting by Semantic Labelling. Fundam. Inform., 24(1/2):89-105, 1995. doi:10.3233/FI-1995-24124. · Zbl 0839.68050 · doi:10.3233/FI-1995-24124 |
| [25] | Hans Zantema. Termination. In Terese, editor, Term Rewriting Systems, pages 181-259. Cambrigde Univ. Press, 2003. |
| [26] | Hans Zantema. Termination of String Rewriting Proved Automatically. J. Autom. Reasoning, 34(2):105-139, 2005. doi:10.1007/s10817-005-6545-0. · 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.
