The beta version of DROPS 2 is now publicly available! Check this page out at DROPS 2 now!


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/
Go to the corresponding LIPIcs Volume Portal

Bessai, Jan ; Czajka, Lukasz ; Laarmann, Felix ; Rehof, Jakob

Restricting Tree Grammars with Term Rewriting

pdf-format:
LIPIcs-FSCD-2022-14.pdf (0.7 MB)

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

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI