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 is known since 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.

翻译：索引语言是形式语言理论中的经典概念，近年来因其在高阶模型检验中的作用而受到关注：它们正是由二阶下推自动机接受的语言。索引语言的下闭包——其成员所有（分散）子词的集合——是众所周知的正则超近似。自2015年起，已知给定索引语言的下闭包是可有效计算的。然而，该算法没有复杂度界限，且是否存在原始递归构造的问题仍然悬而未决。我们解决了这一问题，并给出了非确定性（分别为确定性）自动机的三重（分别为四重）指数构造。我们还证明了（渐近）匹配的下界。对于上界，我们依赖于半群理论的最新进展，这使我们能够针对有限半群计算单词的有界大小摘要。通过用摘要替换栈，我们能够将索引文法转换为具有相同下闭包的上下文无关文法，然后应用上下文无关文法的现有界限。