Document Open Access Logo

Restricting Tree Grammars with Term Rewriting

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

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2022.14.pdf
  • Filesize: 0.7 MB
  • 19 pages

Document Identifiers

Author Details

Jan Bessai
  • TU Dortmund, Germany
Lukasz Czajka
  • TU Dortmund, Germany
Felix Laarmann
  • TU Dortmund, Germany
Jakob Rehof
  • TU Dortmund, Germany

Acknowledgements

We thank Christoph Stahl for creating the tikz figures. We also thank our reviewers for their insightful and useful comments which improved the final version of the paper.

Cite AsGet BibTex

Jan Bessai, Lukasz Czajka, Felix Laarmann, and Jakob Rehof. Restricting Tree Grammars with Term Rewriting. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 14:1-14:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.FSCD.2022.14

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Tree languages
  • Theory of computation → Automata extensions
  • Theory of computation → Equational logic and rewriting
Keywords
  • tree automata
  • tree grammar
  • term rewriting
  • normalization
  • emptiness
  • finiteness

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, 1999. Google Scholar
  2. J. Bessai, L. Czajka, F. Laarmann, and J. Rehof. Restricting tree grammars with rewriting. https://github.com/FelixLaarmann/tree-grammar, 2022.
  3. Jan Bessai. A type-theoretic framework for software component synthesis. PhD thesis, Technical University of Dortmund, Germany, 2019. URL: http://hdl.handle.net/2003/38387.
  4. Jan Bessai, Tzu-Chun Chen, Andrej Dudenhefner, Boris Düdder, Ugo de'Liguoro, and Jakob Rehof. Mixin composition synthesis based on intersection types. Logical Methods in Computer Science, 14(1), 2018. URL: https://doi.org/10.23638/LMCS-14(1:18)2018.
  5. Hubert Comon, Max Dauchet, Remi Gilleron, Florent Jacquemard, Denis Lugiez, Christof Löding, Sophie Tison, and Marc Tommasi. Tree Automata Techniques and Applications. INRIA, 2008. Google Scholar
  6. Hubert Comon and Florent Jacquemard. Ground reducibility is EXPTIME-complete. In LICS 1997, pages 26-34, 1997. Google Scholar
  7. Hubert Comon and Florent Jacquemard. Ground reducibility is EXPTIME-complete. Inf. Comput., 187(1):123-153, 2003. Google Scholar
  8. Boris Düdder, Moritz Martens, Jakob Rehof, and Pawel Urzyczyn. Bounded combinatory logic. In Patrick Cégielski and Arnaud Durand, editors, Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL, CSL 2012, September 3-6, 2012, Fontainebleau, France, volume 16 of LIPIcs, pages 243-258. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012. URL: https://doi.org/10.4230/LIPIcs.CSL.2012.243.
  9. Guillem Godoy and Omer Giménez. The HOM problem is decidable. J. ACM, 60(4):23:1-23:44, 2013. Google Scholar
  10. Fadil Kallat, Carina Mieth, Jakob Rehof, and Anne Meyer. Using component-based software synthesis and constraint solving to generate sets of manufacturing simulation models. In CIRP, pages 556-561. Elsevier, 2020. URL: https://doi.org/10.1016/j.procir.2020.03.018.
  11. Fadil Kallat, Tristan Schäfer, and Anna Vasileva. CLS-SMT: bringing together combinatory logic synthesis and satisfiability modulo theories. In Giselle Reis and Haniel Barbosa, editors, Proceedings Sixth Workshop on Proof eXchange for Theorem Proving, PxTP 2019, Natal, Brazil, August 26, 2019, volume 301 of EPTCS, pages 51-65, 2019. URL: https://doi.org/10.4204/EPTCS.301.7.
  12. Jinwoo Kim, Qinheping Hu, Loris D'Antoni, and Thomas W. Reps. Semantics-guided synthesis. Proc. ACM Program. Lang., 5(POPL):1-32, 2021. URL: https://doi.org/10.1145/3434311.
  13. Patrick Landwehr and Christof Löding. Tree Automata with Global Constraints for Infinite Trees. In Rolf Niedermeier and Christophe Paul, editors, 36th International Symposium on Theoretical Aspects of Computer Science (STACS 2019), volume 126 of Leibniz International Proceedings in Informatics (LIPIcs), pages 47:1-47:15, Dagstuhl, Germany, 2019. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. Google Scholar
  14. Parthasarathy Madhusudan. Synthesizing reactive programs. In Marc Bezem, editor, Computer Science Logic, 25th International Workshop / 20th Annual Conference of the EACSL, CSL 2011, September 12-15, 2011, Bergen, Norway, Proceedings, volume 12 of LIPIcs, pages 428-442. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2011. URL: https://doi.org/10.4230/LIPIcs.CSL.2011.428.
  15. Hitoshi Ohsaki. Beyond regularity: Equational tree automata for associative and commutative theories. In Laurent Fribourg, editor, Computer Science Logic, 15th International Workshop, CSL 2001. 10th Annual Conference of the EACSL, Paris, France, September 10-13, 2001, Proceedings, volume 2142 of Lecture Notes in Computer Science, pages 539-553. Springer, 2001. Google Scholar
  16. Hitoshi Ohsaki and Hiroyuki Seki. Languages modulo normalization. In Boris Konev and Frank Wolter, editors, Frontiers of Combining Systems, 6th International Symposium, FroCoS 2007, Liverpool, UK, September 10-12, 2007, Proceedings, volume 4720 of Lecture Notes in Computer Science, pages 221-236. Springer, 2007. Google Scholar
  17. Jakob Rehof and Pawel Urzyczyn. Finite combinatory logic with intersection types. In TLCA, volume 6690 of Lecture Notes in Computer Science, pages 169-183. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-21691-6_15.
  18. Jakob Rehof and Moshe Y. Vardi. Design and synthesis from components (dagstuhl seminar 14232). Dagstuhl Reports, 4(6):29-47, 2014. URL: https://doi.org/10.4230/DagRep.4.6.29.
  19. Tristan Schäfer, Jim A. Bergmann, Rafael G. Carballo, Jakob Rehof, and Petra Wiederkehr. A synthesis-based tool path planning approach for machining operations. In CIRP, pages 918-923. Elsevier, 2021. URL: https://doi.org/10.1016/j.procir.2021.11.154.
  20. Terese. Term Rewriting Systems, volume 55 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2003. Google Scholar
  21. Sigrid Wenzel, Jana Stolipin, Jakob Rehof, and Jan Winkels. Trends in automatic composition of structures for simulation models in production and logistics. In WSC, pages 2190-2200. IEEE, 2019. URL: https://doi.org/10.1109/WSC40007.2019.9004959.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact