License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2022.14
URN: urn:nbn:de:0030-drops-162953
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/16295/
Bessai, Jan ;
Czajka, Lukasz ;
Laarmann, Felix ;
Rehof, Jakob
Restricting Tree Grammars with Term Rewriting
Abstract
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.
BibTeX - Entry
@InProceedings{bessai_et_al:LIPIcs.FSCD.2022.14,
author = {Bessai, Jan and Czajka, Lukasz and Laarmann, Felix and Rehof, Jakob},
title = {{Restricting Tree Grammars with Term Rewriting}},
booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
pages = {14:1--14:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-233-4},
ISSN = {1868-8969},
year = {2022},
volume = {228},
editor = {Felty, Amy P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2022/16295},
URN = {urn:nbn:de:0030-drops-162953},
doi = {10.4230/LIPIcs.FSCD.2022.14},
annote = {Keywords: tree automata, tree grammar, term rewriting, normalization, emptiness, finiteness}
}
Keywords: |
|
tree automata, tree grammar, term rewriting, normalization, emptiness, finiteness |
Collection: |
|
7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022) |
Issue Date: |
|
2022 |
Date of publication: |
|
28.06.2022 |