Indexed languages are a classical notion in formal language theory, which has attracted attention in recent decades due to its role in higher-order model checking: They are precisely the languages accepted by order-2 pushdown automata. The downward closure of an indexed language -- the set of all (scattered) subwords of its members -- is well-known to be a regular over-approximation. It was shown by Zetzsche (ICALP 2015) that the downward closure of a given indexed language is effectively computable. However, the algorithm comes with no complexity bounds, and it has remained open whether a primitive-recursive construction exists. We settle this question and provide a triply (resp.\ quadruply) exponential construction of a non-deterministic (resp.\ deterministic) automaton. We also prove (asymptotically) matching lower bounds. For the upper bounds, we rely on recent advances in semigroup theory, which let us compute bounded-size summaries of words with respect to a finite semigroup. By replacing stacks with their summaries, we are able to transform an indexed grammar into a context-free one with the same downward closure, and then apply existing bounds for context-free grammars.

翻译：索引语言是形式语言理论中的一个经典概念，近几十年来因其在高阶模型检验中的作用而备受关注：它们恰好是由二阶下推自动机接受的语言。索引语言的向下闭包——即其成员所有（离散）子字的集合——被公认为是一种正则的过近似。Zetzsche（ICALP 2015）的研究表明，给定索引语言的向下闭包是可有效计算的。然而，该算法并未给出复杂度上界，且是否存在原始递归构造的问题一直悬而未决。我们解决了这一问题，并给出了非确定性（确定性）自动机的三重（四重）指数级构造。我们还证明了（渐近）匹配的下界。对于上界，我们依赖于半群理论的最新进展，该理论允许我们计算关于有限半群的有限大小字摘要。通过用其摘要替换栈，我们能够将索引文法转换为具有相同向下闭包的上下文无关文法，进而应用上下文无关文法的现有界。