Pushdown languages and finite observation

Dyck Hankel ranks and finite future quotients

A Dyck prefix is summarized by its unmatched opener stack. That coordinate gives exact finite Hankel ranks. Adding a finite controller changes which stack/controller pairs are reachable, but balanced-word saturation and bounded future signatures still produce a computable tower whose limit recovers the exact observable semantics.

FPRD-D20 · definition

Bounded futures and exact midpoint cuts are different

Let $D_{k,\ell}$ have $k\ge1$ matched opener/closer types and $\ell\ge0$ neutral letters. A valid prefix leaves a typed stack $s\in[k]^*$ ; underflow or a mismatched closer enters an absorbing failure state. Acceptance means ending with the empty stack without failure.

Bounded residual window

Rows are live stacks visible through height $N$ , and columns are all continuations of length at most $N$ . It records every finite future through the selected horizon.

Exact midpoint window

Rows and columns are literal words of length exactly $N$ . It is the cut after the first half of inputs of total length $2N$ .

Field rank, Boolean factor rank, the number of distinct rows, and deterministic midpoint configurations are related but not interchangeable. In particular, the reachable all-zero failure row adds one semantic row and no rank dimension.

FPRD-T38 · theorem

The saved stack gives the exact ranks

Put $S_k(N)=\sum_{h=0}^{N}k^h.$ The bounded residual window has field rank and Boolean factor rank exactly $S_k(N)$ . For the exact midpoint window both ranks equal

A_{k,\ell}(N)= \begin{cases} \displaystyle\sum_{h=0}^{N}k^h,&\ell\ge1,\\[4pt] \displaystyle\sum_{j=0}^{\lfloor N/2\rfloor}k^{N-2j},&\ell=0. \end{cases}

Proof idea. For a stack $s=i_1\cdots i_h$ , its canonical closer is $\bar s=c_{i_h}\cdots c_{i_1}$ . The matrix restricted to selected stack rows and their canonical closers is the identity: another stack is either too short, too long, or mismatched. This is a field-rank lower bound and a Boolean fooling-set lower bound. Factoring every response through the saved-stack coordinate supplies the matching upper bounds.

At an exact length- $N$ cut, a neutral letter pads any height. Without neutrals, pushes and pops change height parity, so only heights congruent to $N\bmod2$ occur. Balanced opener–closer pairs provide the required even padding. ∎

FPRD-D21 · definition

A finite controller changes reachability, not stack typing

A controlled-Dyck system combines the visible stack action with a finite total controller $Q$ . A raw live configuration is $(s,q)$ . Only configurations reachable from $(\epsilon,q_0)$ are retained.

For horizon $N$ , the bounded future signature is $B_N(x)=\bigl(o(x\cdot w)\bigr)_{|w|\le N}.$ States of height greater than $N$ cannot empty within the horizon, so their signature is all false, just like absorbing failure. The quotient $S_N=C_N/\ker B_N$ keeps exactly the distinctions visible at that horizon. Exact-length signatures use only $|w|=j$ and belong to the separate fixed-length cut theorem.

FPRD-T40 · theorem

Finite saturation computes every bounded quotient

Let $W\subseteq Q\times Q$ be the least relation containing identities and neutral transitions and closed under concatenation and matched wrapping. It records the controller effects of all balanced words, including arbitrarily long detours. Because $Q$ is finite, this closure stabilizes.

Any prefix ending with unmatched stack $i_1\cdots i_h$ decomposes into $h+1$ balanced segments around those unmatched openers. Applying $W$ between successive pushes therefore computes every reachable controller state over every stack of height at most $N$ . Partitioning those finite carriers by $B_N$ computes $S_N$ .

Reconstruction. Restricting a horizon- $N+1$ signature gives a surjective bonding map to horizon $N$ . Letter actions lower the required future depth by one. The inverse limit of these quotients is homeomorphic to the exact semantic quotient when the latter carries the topology of agreement on bounded futures.

A compatible thread whose represented stack heights stay bounded stabilizes on an exact semantic class, since only finitely many bounded raw configurations exist. If the heights escape every bound, every fixed-horizon future is all false; that thread is the existing absorbing-failure class. This is the missing surjectivity step. It also explains why the topology must be stated: the claim is about observational convergence, not an unspecified discrete topology.

The minimum is relative to reachable surjective graded summaries preserving readout, bonds, and named degree-lowering actions. It is not a minimum over arbitrary visibly pushdown machine formats.

Hostile boundaries

The all-zero failure row changes row and state counts but not either algebraic rank.
Without a neutral letter, exact midpoint heights obey a parity constraint; the bounded window does not.
A stack deeper than the observation horizon is not semantically equal to failure at every horizon, but it has the same current bounded signature.
No finite level is claimed to recover all infinite-horizon distinctions.
The computations below test finite instances and do not replace the unrestricted stack and saturation arguments.

Sources and evidence

Noam Chomsky and Marcel-Paul Schützenberger, The Algebraic Theory of Context-Free Languages, in P. Braffort and D. Hirschberg (eds.), Computer Programming and Formal Systems, Studies in Logic and the Foundations of Mathematics 35, North-Holland, 1963, pp. 118–161. This is the classical Dyck-language representation source; it does not own the rank formulas proved here.
Rajeev Alur and P. Madhusudan, Visibly Pushdown Languages, Proceedings of STOC 2004, ACM, pp. 202–211. This supplies the standard visible push/pop/internal machine setting used as a comparator.
Nadia Labai and Johann A. Makowsky, Hankel Matrices for Weighted Visibly Pushdown Automata, LATA 2016, LNCS 9618, pp. 464–477, arXiv:1512.02430. Their nested Hankel characterization is neighboring weighted theory; it is not the finite Boolean-window formula above.

Independent review evidence. Scope and reproduction instructions, exact checker, and committed output, with its hash certificate.