Lambda-definable order-3 tree functions are well-quasi-ordered

Kazuyuki Asada, Naoki Kobayashi

Research output: Chapter in Book/Report/Conference proceedingConference contribution

2 Citations (Scopus)

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).

Original languageEnglish
Title of host publication38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2018
EditorsSumit Ganguly, Paritosh Pandya
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
ISBN (Electronic)9783959770934
DOIs
Publication statusPublished - 2018 Dec
Event38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2018 - Ahmedabad, India
Duration: 2018 Dec 112018 Dec 13

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
Volume122
ISSN (Print)1868-8969

Conference

Conference38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2018
Country/TerritoryIndia
CityAhmedabad
Period18/12/1118/12/13

Keywords

  • Higher-order grammar
  • Kruskal’s tree theorem
  • Pumping lemma
  • Simply-typed lambda calculus
  • Well-quasi-ordering

ASJC Scopus subject areas

  • Software

Cite this