Document Open Access Logo

Pumping Lemma for Higher-order Languages

Authors Kazuyuki Asada, Naoki Kobayashi

PDF

File

Thumbnail PDF
PDF
LIPIcs.ICALP.2017.97.pdf
  • Filesize: 0.59 MB
  • 14 pages

Document Identifiers

Subject Classification

Keywords
  • pumping lemma
  • higher-order grammars
  • Kruskal's tree theorem

Metrics

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

Abstract

We study a pumping lemma for the word/tree languages generated by higher-order grammars. Pumping lemmas are known up to order-2 word languages (i.e., for regular/context-free/indexed languages), and have been used to show that a given language does not belong to the classes of regular/context-free/indexed languages. We prove a pumping lemma for word/tree languages of arbitrary orders, modulo a conjecture that a higher-order version of Kruskal's tree theorem holds.  We also show that the conjecture indeed holds for the order-2 case, which yields a pumping lemma for order-2 tree languages and order-3 word languages.

Cite As Get BibTex

Kazuyuki Asada and Naoki Kobayashi. Pumping Lemma for Higher-order Languages. In 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 80, pp. 97:1-97:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017) https://doi.org/10.4230/LIPIcs.ICALP.2017.97

Author Details

Kazuyuki Asada
Naoki Kobayashi

References

  1. 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), volume 55 of LIPIcs, pages 111:1-111:13. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016. Google Scholar
  2. Yehoshua Bar-Hillel, Micha A. Perles, and Eli Shamir. On formal properties of simple phrase structure grammars. Z. Phonetik Sprachwiss. und Kommunikat., 14:143-172, 1961. Google Scholar
  3. 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
  4. Werner Damm. The IO- and OI-hierarchies. Theor. Comput. Sci., 20:95-207, 1982. Google Scholar
  5. Joost Engelfriet. Iterated stack automata and complexity classes. Info. Comput., 95(1):21-75, 1991. Google Scholar
  6. Joost Engelfriet and Heiko Vogler. High level tree transducers and iterated pushdown tree transducers. Acta Inf., 26(1/2):131-192, 1988. Google Scholar
  7. Takeshi Hayashi. On derivation trees of indexed grammars - an extension of the uvwxy-theorem. Publ. RIMS, Kyoto Univ., pages 61-92, 1973. Google Scholar
  8. Alexander Kartzow. Personal communication, via Pawel Parys, 2013. Google Scholar
  9. 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
  10. Naoki Kobayashi. Types and higher-order recursion schemes for verification of higher-order programs. In Proc. of POPL, pages 416-428. ACM Press, 2009. 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. J. B. Kruskal. Well-quasi-ordering, the tree theorem, and vazsonyi’s conjecture. Transactions of the American Mathematical Society, 95(2):210-225, 1960. URL: http://www.jstor.org/stable/1993287.
  18. A. N. Maslov. The hierarchy of indexed languages of an arbitrary level. Soviet Math. Dokl., 15:1170-1174, 1974. Google Scholar
  19. C. St. J. A. Nash-Williams. On well-quasi-ordering finite trees. Mathematical Proceedings of the Cambridge Philosophical Society, 59(4):833-835, 1963. Google Scholar
  20. 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
  21. Pawel Parys. A pumping lemma for pushdown graphs of any level. In Proceedings of STACS 2012, volume 14 of LIPIcs, pages 54-65. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2012. Google Scholar
  22. 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.
  23. Pawel Parys. Intersection types and counting. CoRR, abs/1701.05303, 2017. A shorter version will appear in Post-proceedings of ITRS 2016. URL: http://arxiv.org/abs/1701.05303.
  24. Sylvain Salvati and Igor Walukiewicz. Krivine machines and higher-order schemes. In Proceedings of ICALP 2011, volume 6756 of LNCS, pages 162-173. Springer, 2011. Google Scholar
  25. Kazushige Terui. Semantic evaluation, intersection types and complexity of simply typed lambda calculus. In 23rd International Conference on Rewriting Techniques and Applications (RTA'12), volume 15 of LIPIcs, pages 323-338. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2012. Google Scholar
  26. 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. Google Scholar
  27. Marek Zaionc. Word operation definable in the typed lambda-calculus. Theor. Comput. Sci., 52:1-14, 1987. URL: http://dx.doi.org/10.1016/0304-3975(87)90077-6.
  28. Marek Zaionc. On the "lambda"-definable tree operations. In Algebraic Logic and Universal Algebra in Computer Science, Conference, Ames, Iowa, USA, June 1-4, 1988, Proceedings, volume 425 of Lecture Notes in Computer Science, pages 279-292, 1990. Google Scholar
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact