论文标题
高阶非逐步逐步
Higher-Order Nonemptiness Step by Step
论文作者
论文摘要
我们展示了一种新的简单算法，该算法检查给定的高阶语法是否会产生非空的树木语言。该算法等于将n命令语法转换为n-1命令语法，保留非空置的语法，并仅呈指数增加规模。重复过程n次后，我们获得了订单0的语法，可以轻松检查其非空性。由于大小在每个步骤呈指数增长，因此总体复杂性是n-oxtime，这是最佳的。更确切地说，假设使用的非末端的弧度是由常数界定的，那么转换（因此整个算法）在语法的大小上是线性的。相同的算法允许检查高阶递归方案生成的无限树是否被交替的安全性（或可及性）自动机接受，因为可以通过使用自动机采用递归方案的产物来减少此问题。 算法的正确性证明在证明助理Coq中正式化。我们的转变是由Asada和Kobayashi（2020）的类似转变转变为n命令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.
