Higher-Order Nonemptiness Step by Step

TL;DR

This paper introduces a simple, step-by-step algorithm for checking the nonemptiness of higher-order grammars, transforming them iteratively to lower orders while preserving nonemptiness, with proven correctness and optimal complexity.

Contribution

The paper presents a novel iterative transformation-based algorithm for nonemptiness checking of higher-order grammars, formalized in Coq, and demonstrates its optimal complexity.

Findings

Algorithm operates in n-EXPTIME, matching known complexity bounds.

Transformation preserves nonemptiness at each step.

Algorithm is formalized and verified in Coq.

Abstract

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.