LIPIcs.FSTTCS.2018.14.pdf
- Filesize: 0.53 MB
- 15 pages
Document
Lambda-Definable Order-3 Tree Functions are Well-Quasi-Ordered
Authors
Kazuyuki Asada 
,
-
Part of:
Volume:
38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2018-12-05
File
Document Identifiers
Author Details
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
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).
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)
0PDF Downloads
References
-
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.
- 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.
-
Werner Damm. The IO- and OI-Hierarchies. Theor. Comput. Sci., 20:95-207, 1982.
- 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.
-
Takeshi Hayashi. On Derivation Trees of Indexed Grammars -An Extension of the uvwxy-Theorem-. Publ. RIMS, Kyoto Univ., pages 61-92, 1973.
-
Graham Higman. Ordering by divisibility in abstract algebras. Proceedings of the London Mathematical Society, 3(1):326-336, 1952.
- 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.
- 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.
- 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.
-
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.
- 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.
-
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.
- 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.