Document Open Access Logo

On Word and Frontier Languages of Unsafe Higher-Order Grammars

Authors Kazuyuki Asada, Naoki Kobayashi

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2016.111.pdf
  • Filesize: 0.55 MB
  • 13 pages

Document Identifiers

Author Details

Kazuyuki Asada
Naoki Kobayashi

Cite AsGet BibTex

Kazuyuki Asada and Naoki Kobayashi. On Word and Frontier Languages of Unsafe Higher-Order Grammars. In 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 55, pp. 111:1-111:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
https://doi.org/10.4230/LIPIcs.ICALP.2016.111

Abstract

Higher-order grammars are an extension of regular and context-free grammars, where nonterminals may take parameters. They have been extensively studied in 1980's, and restudied recently in the context of model checking and program verification. We show that the class of unsafe order-(n+1) word languages coincides with the class of frontier languages of unsafe order-n tree languages. We use intersection types for transforming an order-(n+1) word grammar to a corresponding order-n tree grammar. The result has been proved for safe languages by Damm in 1982, but it has been open for unsafe languages, to our knowledge. Various known results on higher-order grammars can be obtained as almost immediate corollaries of our result.
Keywords
  • intersection types
  • higher-order grammars

Metrics

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

References

  1. Klaus Aehlig, Jolie G. de Miranda, and C.-H. Luke Ong. Safety is not a restriction at level 2 for string languages. In Proceedings of FoSSaCS 2005, volume 3441 of LNCS, pages 490-504. Springer, 2005. Google Scholar
  2. Kazuyuki Asada and Naoki Kobayashi. On word and frontier languages of unsafe higher-order grammars. CoRR, abs/1604.01595, 2016. Google Scholar
  3. William Blum and C.-H. Luke Ong. The safe lambda calculus. Logical Methods in Computer Science, 5(1), 2009. Google Scholar
  4. Lorenzo Clemente, Pawel Parys, Sylvain Salvati, and Igor Walukiewicz. The diagonal problem for higher-order recusion schemes is decidable. In Proceedings of LICS 2016, 2016. Google Scholar
  5. Wojciech Czerwinski and Wim Martens. A note on decidable separability by piecewise testable languages. CoRR, abs/1410.1042, 2014. URL: http://arxiv.org/abs/1410.1042.
  6. Werner Damm. The IO- and OI-hierarchies. Theor. Comput. Sci., 20:95-207, 1982. Google Scholar
  7. Joost Engelfriet. Iterated stack automata and complexity classes. Info. Comput., 95(1):21-75, 1991. Google Scholar
  8. Joost Engelfriet and Heiko Vogler. High level tree transducers and iterated pushdown tree transducers. Acta Inf., 26(1/2):131-192, 1988. Google Scholar
  9. Matthew Hague, Jonathan Kochems, and C.-H. Luke Ong. Unboundedness and downward closures of higher-order pushdown automata. In Proceedings of POPL 2016, pages 151-163, 2016. URL: http://dx.doi.org/10.1145/2837614.2837627.
  10. Teodor Knapik, Damian Niwinski, and Pawel Urzyczyn. Deciding monadic theories of hyperalgebraic trees. In TLCA 2001, volume 2044 of LNCS, pages 253-267. Springer, 2001. Google Scholar
  11. Naoki Kobayashi. Model checking higher-order programs. Journal of the ACM, 60(3), 2013. Google Scholar
  12. Naoki Kobayashi. Pumping by typing. In Proceedings of LICS 2013, pages 398-407. IEEE Computer Society, 2013. Google Scholar
  13. Naoki Kobayashi, Kazuhiro Inaba, and Takeshi Tsukada. Unsafe order-2 tree languages are context-sensitive. In Proceedings of FoSSaCS 2014, volume 8412 of LNCS, pages 149-163. Springer, 2014. Google Scholar
  14. Naoki Kobayashi, Kazutaka Matsuda, Ayumi Shinohara, and Kazuya Yaguchi. Functional programs as compressed data. Higher-Order and Symbolic Computation, 2013. Google Scholar
  15. Naoki Kobayashi and C.-H. Luke Ong. A type system equivalent to the modal mu-calculus model checking of higher-order recursion schemes. In Proceedings of LICS 2009, pages 179-188. IEEE Computer Society Press, 2009. Google Scholar
  16. Gregory M. Kobele and Sylvain Salvati. The IO and OI hierarchies revisited. Inf. Comput., 243:205-221, 2015. Google Scholar
  17. C.-H. Luke Ong. On model-checking trees generated by higher-order recursion schemes. In LICS 2006, pages 81-90. IEEE Computer Society Press, 2006. Google Scholar
  18. Pawel Parys. How many numbers can a lambda-term contain? In Proceedings of FLOPS 2014, volume 8475 of LNCS, pages 302-318. Springer, 2014. URL: http://dx.doi.org/10.1007/978-3-319-07151-0_19.
  19. Sylvain Salvati and Igor Walukiewicz. Typing weak MSOL properties. In Andrew M. Pitts, editor, Proceedings of FoSSaCS 2015, volume 9034 of LNCS, pages 343-357. Springer, 2015. URL: http://dx.doi.org/10.1007/978-3-662-46678-0_22.
  20. Takeshi Tsukada and C.-H. Luke Ong. Compositional higher-order model checking via ω-regular games over böhm trees. In Proceedings of CSL-LICS'14, pages 78:1-78:10. ACM, 2014. URL: http://dx.doi.org/10.1145/2603088.2603133.
  21. Georg Zetzsche. An approach to computing downward closures. In Proceedings of ICALP 2015, volume 9135 of LNCS, pages 440-451. Springer, 2015. URL: http://dx.doi.org/10.1007/978-3-662-47666-6_35.
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact