Abstract
We show a new simple algorithm that checks whether a given higherorder grammar generates a nonempty language of trees. The algorithm amounts to a procedure that transforms a grammar of order n to a grammar of order n1, preserving nonemptiness, and increasing the size only exponentially. After repeating the procedure n times, we obtain a grammar of order 0, whose nonemptiness can be easily checked. Since the size grows exponentially at each step, the overall complexity is nEXPTIME, which is known to be optimal. More precisely, the transformation (and hence the whole algorithm) is linear in the size of the grammar, assuming that the arity of employed nonterminals is bounded by a constant. The same algorithm allows to check whether an infinite tree generated by a higherorder recursion scheme is accepted by an alternating safety (or reachability) automaton, because this question can be reduced to the nonemptiness problem by taking a product of the recursion scheme with the automaton.
A proof of correctness of the algorithm is formalised in the proof assistant Coq. Our transformation is motivated by a similar transformation of Asada and Kobayashi (2020) changing a word grammar of order n to a tree grammar of order n1. The stepbystep approach can be opposed to previous algorithms solving the nonemptiness problem "in one step", being compulsorily more complicated.
BibTeX  Entry
@InProceedings{parys:LIPIcs:2020:13294,
author = {Pawe{\l} Parys},
title = {{HigherOrder Nonemptiness Step by Step}},
booktitle = {40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
pages = {53:153:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959771740},
ISSN = {18688969},
year = {2020},
volume = {182},
editor = {Nitin Saxena and Sunil Simon},
publisher = {Schloss DagstuhlLeibnizZentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2020/13294},
URN = {urn:nbn:de:0030drops132941},
doi = {10.4230/LIPIcs.FSTTCS.2020.53},
annote = {Keywords: Higherorder grammars, Nonemptiness, Modelchecking, Transformation, Order reduction}
}
Keywords: 

Higherorder grammars, Nonemptiness, Modelchecking, Transformation, Order reduction 
Collection: 

40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020) 
Issue Date: 

2020 
Date of publication: 

04.12.2020 
Supplementary Material: 

Coq formalisation: https://github.com/pparys/hotransformsbs 