Generalized-Dyck residual tower

Exact statement

For a generalized Dyck alphabet with k bracket types and any number of neutral symbols, the exact residual carrier consists of finite typed stacks together with an absorbing failure state. A live stack s has future language K_s of words that empty it without failure; failure has the empty future language.

StatusPrecisely stated and self-contained

External reviewNo documented external or specialist review of this FPRD result is recorded.

Context

A generalized Dyck prefix is summarized exactly by its unmatched opener stack unless an earlier mismatch or underflow has made acceptance impossible.

Definitions

The state space is $X=[k]^*\sqcup\{\bot\}$ , where a word in $[k]^*$ lists unmatched opener types from bottom to top and $\bot$ is absorbing failure.
For a live stack $s$ , $K_s=\{w:\operatorname{run}(s,w)=\varepsilon\}$ ; set $K_\bot=\varnothing$ .
If $s=i_1\cdots i_h$ , its canonical completion is $\overline s=c_{i_h}\cdots c_{i_1}$ .

Hypotheses and scope

There is at least one bracket type; the neutral alphabet may be empty.
Closers must match the top opener type, and underflow or mismatch is irreversible.

Proof or evidence

The specification gives total symbol actions and an absorbing failure state. The associated proof identifies every word residual with exactly one future language K_s or K_bottom.

Model and exact residuals →

Verification notes

The state convention, execution order, failure behavior, canonical completion, and readout were reconciled with the M21 proof and closure audit.

Limitations

This is the generalized Dyck model, not an arbitrary context-free language.
The definition alone does not assert finite-state recognizability.

Open work

Add a small worked residual calculation for two bracket types and one neutral symbol.

Notes

The exact carrier is presentation-independent for the selected generalized-Dyck language. Its depth-N shadows retain remaining-suffix observations through input length N; closers act naturally between adjacent grades rather than by choosing representatives of a tail class.