文章基本信息

标题：Lambda-Definable Order-3 Tree Functions are Well-Quasi-Ordered
本地全文：下载
作者：Kazuyuki Asada ; Naoki Kobayashi
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2018
卷号：122
页码：1-15
DOI：10.4230/LIPIcs.FSTTCS.2018.14
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：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).
关键词：higher-order grammar; pumping lemma; Kruskal's tree theorem; well-quasi-ordering; simply-typed lambda calculus