TY - GEN
T1 - Lambda-definable order-3 tree functions are well-quasi-ordered
AU - Asada, Kazuyuki
AU - Kobayashi, Naoki
N1 - Funding Information:
Acknowledgements We would like to thank anonymous referees for useful comments. was supported by JSPS Kakenhi 15H05706 and 18K11156.
PY - 2018/12
Y1 - 2018/12
N2 - 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).
AB - 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).
KW - Higher-order grammar
KW - Kruskal’s tree theorem
KW - Pumping lemma
KW - Simply-typed lambda calculus
KW - Well-quasi-ordering
UR - http://www.scopus.com/inward/record.url?scp=85079494484&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85079494484&partnerID=8YFLogxK
U2 - 10.4230/LIPIcs.FSTTCS.2018.14
DO - 10.4230/LIPIcs.FSTTCS.2018.14
M3 - Conference contribution
AN - SCOPUS:85079494484
T3 - Leibniz International Proceedings in Informatics, LIPIcs
BT - 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2018
A2 - Ganguly, Sumit
A2 - Pandya, Paritosh
PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
T2 - 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2018
Y2 - 11 December 2018 through 13 December 2018
ER -