逐步高阶非空性
Higher-Order Nonemptiness Step by Step
摘要：
我们展示了一个新的简单算法，该算法检查给定的高阶语法是否生成非空的树语言。该算法相当于一个程序，转换为语法的顺序n到语法的顺序n-1，保持非空性，并增加的大小只呈指数。在重复这个过程n次之后，我们得到一个0阶文法，它的非空性可以很容易地检查。由于大小在每一步都呈指数级增长，因此总体复杂度为n-EXPTIME，这是已知的最佳值。更确切地说，假设所使用的非终结符的arity由一个常数限制，则转换（以及整个算法）在文法的大小上是线性的。同样的算法允许检查由高阶递归方案生成的无限树是否被交替安全（或可达性）自动机接受，因为这个问题可以通过取递归方案与自动机的乘积来简化为非空性问题。算法的正确性证明在证明助手Coq中得到了形式化。我们的转换是由Asada和Kobayashi（2020）的类似转换激发的，将n阶的单词语法改变为n-1阶的树语法。一步一步的方法可以反对以前的算法解决非空性问题“在一个步骤”，被强制更复杂。
英文摘要：
We show a new simple algorithm that checks whether a given higher-order 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 n-1, 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 n-EXPTIME, 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 higher-order 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 n-1. The step-by-step approach can be opposed to previous algorithms solving the nonemptiness problem "in one step", being compulsorily more complicated.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
