2026-10-01T10:23:02Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:9913 2026-09-23T05:44:37Z ddc:004 open_access

Lambda-Definable Order-3 Tree Functions are Well-Quasi-Ordered Asada, Kazuyuki Kobayashi, Naoki higher-order grammar pumping lemma Kruskal's tree theorem well-quasi-ordering simply-typed lambda calculus 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). Schloss Dagstuhl – Leibniz-Zentrum für Informatik Kazuyuki Asada and Naoki Kobayashi 2018 Is Part Of LIPIcs, Volume 122, 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSTTCS.2018.14 urn:nbn:de:0030-drops-99138 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.14 eng https://creativecommons.org/licenses/by/3.0/legalcode