The complexity of downward closures of indexed languages

TL;DR

This work resolves the long-standing open problem of the precise complexity of computing downward closures for indexed languages. By introducing a stack-summaries framework via a finite stack monoid and leveraging recent semigroup techniques, the authors convert indexed grammars into equivalent CFGs while preserving downward closures, enabling triply-exponential upper bounds for NFA representations and quadruple-exponential bounds for DFAs, with matching lower bounds. They also establish coNEXP-completeness for downward-closure inclusion and equivalence, and prove a triply-exponential pumping threshold, tightening the understanding of higher-order language analyses. The combination of algebraic stack abstractions, pump/skip derivations, and a CFG construction provides a tight, broadly applicable approach to analyzing downward closures in higher-order language classes, with implications for verification and model-checking tasks involving indexed languages and beyond.

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.

Figures (2)

• Figure 1: The idea behind the "skip rule" is that if we have a derivation from some non-terminal $A$ in which we pop $N$ consecutive infixes $u_1 \dots u_N$ mapping to the same idempotent $e = (B,X,M, A,X)$, then along every branch we must have a node of the form $A_i[u_{i+1} \cdots u_N]$ with $M(A_i, A_i) = \top$. This means that for any word mapping to $e$, there is a derivation from $A_i$ popping this word, and with the resulting "sentential form" containing $A_i$. The rest of the sentential form can be erased since we are interested in the "downward closure". This non-terminal can be used to "skip" the infix $u_{i+1} \cdots u_N z_e u_1 \cdots u_i$, which maps to $e$. Hence, we can turn a derivation from $A[u_1 \cdots u_N]$ into one from $A[u_1 \cdots u_N z_e u_1 \cdots u_N]$ by popping the right infix along every branch.
• Figure 2: A visual of how "summaries" are constructed. Say we are given a word $z$ of "regular $\Jgreen$-depth" $d$. We read it from right to left. We cut it into "$d$-atoms" by iteratively taking the smallest suffix of "regular $\Jgreen$-depth" $d$. Its summary consists of its leftmost letter and a "$d'$-summary" for its "tail" of depth $d'<d$. In parallel, we read the resulting sequence of atoms $\cdots \alpha_3 \alpha_2 \alpha_1$ from right to left. Every time we find an infix with a "prefix" made of 2N+1 infixes mapping to the same idempotent, we turn it into a "$d$-block" $u_1 u_2 e^+ v_1 v_2$. Finally, whenever we have two blocks corresponding to an idempotent $e$ and such that the infix between their middle parts also evaluates to $e$, we merge them into one "$d$-block".

Theorems & Definitions (87)

• theorem 1
• Remark 2.1
• Remark 2.2
• Remark 2.3
• theorem 2
• theorem 3
• corollary 1
• corollary 2
• theorem 4
• theorem 5