2026-07-22T13:39:17Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:16295 2024-03-06T10:57:10Z ddc:004 open_access

Restricting Tree Grammars with Term Rewriting Bessai, Jan Czajka, Lukasz Laarmann, Felix Rehof, Jakob tree automata tree grammar term rewriting normalization emptiness finiteness We investigate the problem of enumerating all terms generated by a tree-grammar which are also in normal form with respect to a set of directed equations (rewriting relation). To this end we show that deciding emptiness and finiteness of the resulting set is EXPTIME-complete. The emptiness result is inspired by a prior result by Comon and Jacquemard on ground reducibility. The finiteness result is based on modification of pumping arguments used by Comon and Jacquemard. We highlight practical applications and limitations. We provide and evaluate a prototype implementation. Limitations are somewhat surprising in that, while deciding emptiness and finiteness is EXPTIME-complete for linear and nonlinear rewrite relations, the linear case is practically feasible while the nonlinear case is infeasible, even for a trivially small example. The algorithms provided for the linear case also improve on prior practical results by Kallat et al. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Jan Bessai and Lukasz Czajka and Felix Laarmann and Jakob Rehof 2022 Is Part Of LIPIcs, Volume 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2022.14 urn:nbn:de:0030-drops-162953 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.14 eng https://creativecommons.org/licenses/by/4.0/legalcode