The complexity of downward closures of indexed languages

TL;DR

This paper establishes the exact complexity bounds for computing the downward closure of indexed languages, providing a triply/quadruply exponential construction and matching lower bounds, advancing understanding in formal language theory.

Contribution

It proves the existence of primitive-recursive algorithms for downward closures of indexed languages and provides explicit complexity bounds, using novel semigroup-based techniques.

Findings

Triply exponential automaton construction for nondeterministic case

Quadruply exponential automaton construction for deterministic case

Matching lower bounds confirming the complexity estimates

Abstract

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.