Document Open Access Logo

Lambda-Definable Order-3 Tree Functions are Well-Quasi-Ordered

Authors Kazuyuki Asada , Naoki Kobayashi

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSTTCS.2018.14.pdf
  • Filesize: 0.53 MB
  • 15 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Lambda calculus
Keywords
  • higher-order grammar
  • pumping lemma
  • Kruskal's tree theorem
  • well-quasi-ordering
  • simply-typed lambda calculus

Metrics

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

Abstract

Asada and Kobayashi [ICALP 2017] conjectured a higher-order version of Kruskal's tree theorem, and proved a pumping lemma for higher-order languages modulo the conjecture. The conjecture has been proved up to order-2, which implies that Asada and Kobayashi's pumping lemma holds for order-2 tree languages, but remains open for order-3 or higher. In this paper, we prove a variation of the conjecture for order-3. This is sufficient for proving that a variation of the pumping lemma holds for order-3 tree languages (equivalently, for order-4 word languages).

Cite As Get BibTex

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). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 14:1-14:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.FSTTCS.2018.14

Author Details

Kazuyuki Asada
  • Tohoku University, Sendai, Japan
Naoki Kobayashi
  • The University of Tokyo, Tokyo, Japan

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. Kazuyuki Asada and Naoki Kobayashi. Pumping Lemma for Higher-order Languages. In Ioannis Chatzigiannakis, Piotr Indyk, Fabian Kuhn, and Anca Muscholl, editors, 44th International Colloquium on Automata, Languages, and Programming, ICALP 2017, July 10-14, 2017, Warsaw, Poland, volume 80 of LIPIcs, pages 97:1-97:14. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2017. URL: http://dx.doi.org/10.4230/LIPIcs.ICALP.2017.97.
  3. Werner Damm. The IO- and OI-Hierarchies. Theor. Comput. Sci., 20:95-207, 1982. Google Scholar
  4. Nachum Dershowitz. Orderings for term-rewriting systems. Theoretical Computer Science, 17(3):279-301, 1982. URL: http://dx.doi.org/10.1016/0304-3975(82)90026-3.
  5. Takeshi Hayashi. On Derivation Trees of Indexed Grammars -An Extension of the uvwxy-Theorem-. Publ. RIMS, Kyoto Univ., pages 61-92, 1973. Google Scholar
  6. Graham Higman. Ordering by divisibility in abstract algebras. Proceedings of the London Mathematical Society, 3(1):326-336, 1952. Google Scholar
  7. Joseph 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.
  8. Pawel Parys. Intersection Types and Counting. In Naoki Kobayashi, editor, Proceedings Eighth Workshop on Intersection Types and Related Systems, ITRS 2016, Porto, Portugal, 26th June 2016., volume 242 of EPTCS, pages 48-63, 2016. URL: http://dx.doi.org/10.4204/EPTCS.242.6.
  9. Pawel Parys. The Complexity of the Diagonal Problem for Recursion Schemes. In Satya V. Lokam and R. Ramanujam, editors, 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2017, December 11-15, 2017, Kanpur, India, volume 93 of LIPIcs, pages 45:1-45:14. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2017. URL: http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2017.45.
  10. 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
  11. 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.
  12. 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
  13. Marek Zaionc. Lambda Representation of Operations Between Different Term Algebras. In Leszek Pacholski and Jerzy Tiuryn, editors, Computer Science Logic, 8th International Workshop, CSL '94, Kazimierz, Poland, September 25-30, 1994, Selected Papers, volume 933 of Lecture Notes in Computer Science, pages 91-105. Springer, 1994. URL: http://dx.doi.org/10.1007/BFb0022249.
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