LIPIcs.FSCD.2020.22.pdf
- Filesize: 0.59 MB
- 22 pages
Document
Size-Preserving Translations from Order-(n+1) Word Grammars to Order-n Tree Grammars
Authors
Kazuyuki Asada 
,
Naoki Kobayashi
-
Part of:
Volume:
5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Formal Structures for Computation and Deduction (FSCD) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2020-06-28
File
Document Identifiers
Author Details
Acknowledgements
We would like to thank anonymous referees for useful comments.
Cite AsGet BibTex
Kazuyuki Asada and Naoki Kobayashi. Size-Preserving Translations from Order-(n+1) Word Grammars to Order-n Tree Grammars. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 22:1-22:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.FSCD.2020.22
https://doi.org/10.4230/LIPIcs.FSCD.2020.22
Abstract
Higher-order grammars have recently been studied actively in the context of automated verification of higher-order programs. Asada and Kobayashi have previously shown that, for any order-(n+1) word grammar, there exists an order-n grammar whose frontier language coincides with the language generated by the word grammar. Their translation, however, blows up the size of the grammar, which inhibited complexity-preserving reductions from decision problems on word grammars to those on tree grammars. In this paper, we present a new translation from order-(n+1) word grammars to order-n tree grammars that is size-preserving in the sense that the size of the output tree grammar is polynomial in the size of an input tree grammar. The new translation and its correctness proof are arguably much simpler than the previous translation and proof.
Subject Classification
ACM Subject Classification
- Theory of computation → Formal languages and automata theory
Keywords
- higher-order grammar
- word language
- tree language
- complexity
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- Kazuyuki Asada and Naoki Kobayashi. On word and frontier languages of unsafe higher-order grammars. CoRR, abs/1604.01595, 2016. A summary has been published in Proceedings of ICALP 2016. URL: http://arxiv.org/abs/1604.01595.
- Kazuyuki Asada and Naoki Kobayashi. Pumping lemma for higher-order languages. In 44th International Colloquium on Automata, Languages, and Programming, ICALP 2017, volume 80 of LIPIcs, pages 97:1-97:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.ICALP.2017.97.
- Kazuyuki Asada and Naoki Kobayashi. Lambda-definable order-3 tree functions are well-quasi-ordered. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2018, volume 122 of LIPIcs, pages 14:1-14:15. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2018.14.
- William Blum and C.-H. Luke Ong. The safe lambda calculus. Logical Methods in Computer Science, 5(1), 2009. URL: https://doi.org/10.2168/LMCS-5(1:3)2009.
- Lorenzo Clemente, Paweł Parys, Sylvain Salvati, and Igor Walukiewicz. The diagonal problem for higher-order recursion schemes is decidable. In 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2016, pages 96-105. ACM, 2016. URL: https://doi.org/10.1145/2933575.2934527.
- Werner Damm. The IO- and OI-hierarchies. Theor. Comput. Sci., 20(2):95-207, 1982. URL: https://doi.org/10.1016/0304-3975(82)90009-3.
- Teodor Knapik, Damian Niwiński, Paweł Urzyczyn, and Igor Walukiewicz. Unsafe grammars and panic automata. In 32nd International Colloquium on Automata, Languages and Programming, ICALP 2005, volume 3580 of LNCS, pages 1450-1461. Springer, 2005. URL: https://doi.org/10.1007/11523468_117.
- Naoki Kobayashi. Model checking higher-order programs. Journal of the ACM, 60(3), 2013. URL: https://doi.org/10.1145/2487241.2487246.
- Naoki Kobayashi, Ugo Dal Lago, and Charles Grellois. On the termination problem for probabilistic higher-order recursive programs. In 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, pages 1-14. IEEE, 2019. URL: https://doi.org/10.1109/LICS.2019.8785679.
- Naoki Kobayashi and C.-H. Luke Ong. Complexity of model checking recursion schemes for fragments of the modal mu-calculus. Logical Methods in Computer Science, 7(4), 2011. URL: https://doi.org/10.2168/LMCS-7(4:9)2011.
- C.-H. Luke Ong. On model-checking trees generated by higher-order recursion schemes. In 21th IEEE Symposium on Logic in Computer Science, LICS 2006, pages 81-90. IEEE Computer Society, 2006. URL: https://doi.org/10.1109/LICS.2006.38.
- Paweł Parys. The Complexity of the Diagonal Problem for Recursion Schemes. In 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2017, volume 93 of LIPIcs, pages 45:1-45:14. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2017.45.
- Mitchell Wand. An algebraic formulation of the Chomsky hierarchy. In Category Theory Applied to Computation and Control, volume 25 of LNCS, pages 209-213. Springer, 1974. URL: https://doi.org/10.1007/3-540-07142-3_84.