When can stack information be forgotten?

Research note, 30 September 2026. Written argument, not proof-assistant verified. Classical ingredients are credited below; novelty is unestablished.

A frame can be hidden and still matter

Read stacks from top to bottom. Suppose X is called private and is erased by a proposed observation, while A remains visible. The stacks A and XA then look identical. An ordinary pop, however, leaves the projected stacks empty and A, respectively. The private frame delayed the useful pop. With a later empty-stack query, that difference changes an answer.

There are two questions here. Can a machine keep a pointer to the next nonprivate record cheaply? Yes, by saving a pointer when each frame is created. Can it then throw away the private records without changing its future behavior? Only if their effects on future transitions can also be discarded. The first question is about access; the second is about semantics.

This note gives a finite criterion for the second question in a specific model, and a strict persistent construction for the first. It then composes the semantic quotient with the earlier bounded-spread theorem. The result allows unbounded disagreement in raw stack heights when the disagreement really is irrelevant to the retained transition behavior.

1. Source, projection and desired quotient

Let P have finite control Q, input alphabet Sigma, stack alphabet Gamma, a finite nonempty initial-state set, and empty initial stacks. One transition consumes one input letter. Its guard reads the control and one top symbol or emptiness; its action pushes one symbol, pops one symbol, or keeps the stack. Empty pops are disabled or explicitly no-ops. There are no epsilon moves, top rewrites, hidden scans or post-input steps. Rules may be nondeterministic and partial. The acceptance bit o(q,g) depends on control and top/empty. All legal runs, including rejecting ones, count.

Supply finite maps

$$\kappa:Q\to\bar Q,\qquad \pi:\Gamma\to\bar\Gamma\cup\{\epsilon\}.$$

Extend pi by concatenation. It may relabel public frames as well as erase private ones. Define the projected configuration

$$E(q,s)=(\kappa(q),\pi(s)). \tag{1}$$

A one-top unit-stack quotient for this projection is a finite pushdown machine Pbar whose control is exactly Qbar, whose stack alphabet is Gammabar, and whose rules and acceptance depend only on its control and one projected top symbol or emptiness. It uses the same unit operations. For every reachable concrete configuration x and input a, require

$$o(x)=\bar o(E(x)),\qquad \{E(y):x\xrightarrow{a}_P y\} =\{z:E(x)\xrightarrow{a}_{\bar P}z\}. \tag{2}$$

Successors here are sets, not multisets: counting runs is not preserved. The quotient starts in the projected initial states with empty stack. Equation (2) preserves input-labelled branching and observations, a stronger contract than equality of accepted languages. We ask whether such a quotient exists, without being given its transition table or an implementation.

2. A finite table determines the answer

Use bot for the top of an empty stack. For a concrete local rule, define its projected signature to be (kappa(next control), operation), with:

For each concrete control q, concrete top/empty g, and input a, let S(q,g,a) be the finite set of these signatures over all enabled rules. It can be computed directly from the source table. Duplicates are discarded.

Let R_q be the set of reachable top-first stack words in control q. Compute all realizable triples (q,g,t) such that

$$\exists s\in R_q:quad \operatorname{top}(s)=g, \quad\operatorname{top}(\pi(s))=t. \tag{3}$$

Finite criterion. Group realizable triples by (kappa(q),t). Within each group require both:

1. all acceptance bits o(q,g) agree;
2. for every input a, all sets S(q,g,a) agree.

Theorem 1 (exact criterion for the specified quotient class). A one-top unit-stack quotient satisfying (2) on reachable configurations exists if and only if this finite criterion holds. The criterion is decidable and constructs the quotient when it succeeds.

The qualification matters: the theorem characterizes quotients with this fixed projection, these fixed projected controls, this observation interface and these unit operations. It does not characterize all representations of the language, all bisimulation quotients, or all bounded-cost controllers. No extra hidden summary is allowed in the claimed necessity direction.

Computing the realizable classes

Forget input labels only for the offline reachability calculation. Standard pushdown saturation computes a finite automaton for each R_q: the reachable configurations from a regular initial set are effectively regular. A bottom sentinel encodes empty-stack guards; normalized pushes replace a top symbol by at most two symbols. This is the classical post* construction, not a new reachability theorem.

For each triple, intersect R_q with the regular language having concrete top g and with the inverse image under pi of the regular language having projected top t. Emptiness of this finite-automaton intersection decides (3). Erasing homomorphisms cause no problem for inverse images. The number of triples is at most |Q|(|Gamma|+1)(|Gammabar|+1).

Alternatively, supply a regular set I containing the initial configurations and closed under every source transition. Both properties can be checked by finite-automaton operations. The same criterion is then necessary and sufficient for (2) on all of I, and sufficient for reachable behavior. A failure on an overapproximation I need not imply failure on the true reachable set. The executable certificate checker uses this alternative.

Proof of sufficiency

For each realized abstract pair (u,t), use the common signature set as the quotient’s rule table and the common acceptance bit as its observation. Unrealized pairs may have no rules. A projected pop is legal whenever it appears, since its concrete top was nonprivate and hence the projected stack is nonempty.

For every concrete stack s, applying a source rule and then projecting has the same effect as applying its signature to pi(s). For a private pop or push the projection stays fixed; for a public pop or push it changes by the indicated unit operation. Thus every concrete successor projects to a quotient successor. Conversely, every quotient signature is available from each concrete configuration in the group, by equality of the signature sets. Choosing such a rule lifts each quotient step to a concrete step. This proves (2). Closure of reachability, or of I, permits iteration.

Starting from corresponding initial configurations, induction gives both directions of finite-run correspondence and the same existential acceptance after every prefix, including the empty prefix. From any two represented configurations with the same projection, every future input has the same existential acceptance. The graph of E is an observation-preserving bisimulation between the source and the reachable quotient.

If P is complete, the common signature sets on realized pairs are nonempty. Fill unrealized pairs with an arbitrary keep rule and observation. Those pairs cannot become reachable: every quotient step from an image configuration lifts to a source step. This yields a complete quotient without adding a state or altering any represented behavior.

Proof of necessity

At a fixed projected stack word v, normalized signatures have distinct effects. Push increases its length and identifies the pushed letter; pop decreases its length; keep preserves it. The resulting control identifies the other component. At empty, normalize an allowed bottom pop to keep. Thus a successor set uniquely determines the signature set at v.

A one-top quotient must use the same rule-signature set at every stack with the same projected top and control, even when the deeper stacks differ. Equation (2) and the preceding injectivity therefore force the equalities in the criterion. Its observation table likewise forces the acceptance bits to agree. This proves necessity and completes the theorem.

3. Bounded spread may now concern only relevant frames

Corollary 2. Let P be complete, and let its supplied maps pass Theorem 1. For a supplied integer B >= 0, suppose every two legal source runs on the same word have projected stack lengths differing by at most B:

$$\forall w,\rho,\sigma: \bigl||\pi(s_\rho(w))|-|\pi(s_\sigma(w))|\bigr|\le B. \tag{4}$$

Condition (4) is decidable. If it holds, L(P) has a deterministic persistent implementation with one root, one field per logical record and at most one new logical record per input. The reviewed compiler gives a degree-two, native-distance-two scaffold, one physical node per input. The PEG language is L(P)^R, with exactly one reversal.

Proof. Run correspondence identifies the source’s reachable projected stacks on each word with the quotient’s reachable stacks on that same word. Check the quotient’s pairwise bound with the first-exit construction in stack-observer-compilation.md, then apply its complete-source bounded-spread corollary. Initialization remains empty, with fixed virtual scaffold initialization and no extra input letters.

The result preserves future acceptance through the quotient. It need not preserve discarded physical frames, raw source graph observations, run counts or individual nondeterministic histories. The bound is supplied; neither unknown-bound decidability nor optimal degree is asserted.

A nonregular positive example with unbounded raw disagreement

Use inputs c,r,#,p. Before #, a source checks the block protocol c* r*, pushing public A on c and popping on r; an underflow or wrong order enters a rejecting keep-only state. At #, keep the stack and enter an accepting log state exactly if the stack is empty, otherwise a rejecting log state. In either log state each p nondeterministically pushes private X or keeps. Other inputs enter the rejecting keep-only state. All omitted local cases are rejecting, so the source is complete. Initial state is the pre-return phase with empty stack; only the accepting log state accepts.

Its language is

$$\{c^n r^n\#p^j:n,j\ge0\}.$$

Take identity on controls, pi(A)=A, pi(X)=epsilon. Private frames occur only in log or rejecting states, where their presence changes neither projected actions nor acceptance. The finite criterion passes. The quotient is deterministic: the two log actions both become keep. Its spread is zero. On the input #p^j, however, source heights range from zero to j. This source fails every bound on raw height spread while satisfying the projected criterion. The language is nonregular, since intersection with c*r*# and removal of the terminal marker yields the usual equal-block language.

This is a broader sufficient condition on source presentations. It is not a new language class beyond the established deterministic stack baseline.

4. Locality and semantic equality are different requirements

A private frame can change a future answer. The initial A versus XA example fails the signature test on pop: one signature pops a projected symbol and the other keeps. A following empty query can distinguish them. No present label inspection is needed to make a hidden frame matter.

A private label can change a branch. If two erased labels select different next projected controls, the signature sets already differ, even though the projected stacks are both empty. Equal projected heights alone gives no license to forget those labels.

A semantic quotient may need more than one top symbol. There is also a small obstruction to the necessity claim being broadened. Build two legal histories 0a and 1a, with stacks AB0 and AB1 in distinct controls q0,q1. The first letter pushes Bi, the second pushes A. On z, control qi pushes Ci, then stops. Project controls q0,q1 to one control q and retain all stack symbols; keep other controls distinct. The projection is injective on the finitely many reachable configurations, so it has a perfectly valid abstract transition system. But at projected control q and top A, the required pushes differ. No one-top quotient with those projected controls can implement it. Reading the second symbol or retaining the missing control bit repairs the problem. The criterion properly rejects this example; it does not refute other local encodings.

5. Cheap filtered access without semantic erasure

For any deterministic source in the model and any supplied label erasure, one can maintain both its full stack and its filtered stack at constant local cost, even if Theorem 1 fails. This construction does not discard the private information or assert that it is irrelevant.

Keep roots R for the full stack and E for its first nonprivate frame. Each immutable record stores its original label and two pointers:

• tail: the old full-stack root when this frame was pushed;
• saved: the old filtered root when this frame was pushed.

Start with both roots missing. A push of g allocates one record n=(g,R,E), sets R'=n, and sets E'=n if g is public, otherwise E'=E. A nonempty pop sets R'=R.tail and E'=R.saved. Keep and an allowed empty pop leave both roots unchanged.

Induction proves that R decodes the full source stack. E, followed by the saved fields of its public records, decodes exactly pi(s). On pop, the saved root restores the filtered view of precisely the tail now exposed, including when a private frame is popped. Old records and old root pairs continue to decode their old versions. This is ordinary persistent stack augmentation, with a direct worst-case bound rather than an amortized appeal.

The source controller reads R’s label or emptiness. The filtered top is available at E without scanning private prefixes. All copied old addresses are roots or one field from a root. Thus the record interface has

$$s=2,\quad q=2,\quad A=1,\quad r=1, \qquad d=\max(1,s+Aq)=4,\quad k=r+1=2.$$

These are sufficient construction bounds, not lower bounds. The decoder preserves full and filtered stack contents and source control, but the additional pointers change the raw graph vocabulary. There is no physical identity test. The extra native observation layer distinguishes terminal cases as in the existing compiler contract. Arbitrary old versions remain valid if their root pairs are retained; no constant-cost arbitrary historical version lookup is claimed.

6. Observation modulus

For a deterministic source whose projection passes Theorem 1, use the previous note’s prefix metric on quotient configurations and pull it back:

$$d_E(x,y)=d(E(x),E(y)).$$

This is a pseudometric on concrete configurations: different private stacks may have distance zero. Since E(F_a x)=Fbar_a(E(x)) and the quotient is a deterministic unit-stack machine,

$$d_E(F_a x,F_a y)\le2d_E(x,y). \tag{5}$$

For partial machines, (5) concerns common enabled steps; the exact quotient also preserves which inputs are enabled when projected configurations agree. For a total deterministic source it holds for every letter and every pair of reachable configurations. Zero distance is preserved for every future word, and acceptance is preserved. Because acceptance here may inspect the top, agreement through t+1 projected cells suffices for all acceptance answers through horizon t; if acceptance depends only on projected control, t cells suffice. This is an exact finite-horizon guarantee.

For nondeterministic sources Theorem 1 gives back-and-forth matching of successors. It does not say arbitrary independently chosen successors remain close; (5) is stated only for deterministic updates. These observations concern the fixed machine’s projected behavior, not every possible scaffold testing context. Cheap filtered access in Section 5 alone does not prove (5).

7. Dependencies, contribution and verification

The semantic core is classical homomorphism/bisimulation theory. Rutten’s Universal coalgebra: a theory of systems, Propositions 5.7 and 5.8, relate homomorphism kernels and bisimulation quotients. The additional demand here is a finite one-top implementation with an exact, specified stack projection. Equation (2) is stronger than language residual equivalence; a failed certificate need not distinguish the accepted languages.

Exact abstraction is also an established subject of abstract interpretation; see Giacobazzi, Ranzato and Scozzari, Making Abstract Interpretations Complete. Their work studies information-preserving abstract computations and changes to abstract domains. We do not import an optimal-domain construction or identify semantic completeness alone with our local resource contract.

Effective regular reachability is imported from Esparza, Hansel, Rossmanith and Schwoon, Efficient Algorithms for Model Checking Pushdown Systems, Section 3, Theorem 3 and the preceding post* construction. This permits computing the finite classes from the source, rather than assuming a finite quotient or using bounded-depth samples as a reachability oracle.

Persistent linked structures are established technology; see Driscoll, Sarnak, Sleator and Tarjan, Making Data Structures Persistent. The two-root proof above states its own strict access/allocation bounds. The scaffold constants come from the reviewed record compiler, not a general amortized persistence theorem. The preceding bounded-spread theorem imports corrected visibly pushdown determinization and classical synchronized products. No transducer uniformization or unrestricted pumping theorem is inferred.

The additional work is the finite signature criterion and its necessity for this quotient interface, the separation between semantic erasure and cheap filtered access, and their composition with bounded-spread compilation. It is an elementary specialization and construction, not a claimed new general bisimulation theorem. Novelty remains unestablished.

The executable checker verifies supplied regular invariants and their finite signature certificates using finite automata. It also checks bounded example traces and persistent snapshots; see the exact recorded scope. It does not implement the imported general post* saturation, the VPA determinizer, the scaffold compiler or a proof assistant. The unbounded claims rest on the written proofs and imported theorems, not the finite trace samples.

8. Next unresolved question

The current criterion refuses to introduce new memory into the projected control. The two-history counterexample shows why that can be too strict: a small retained summary can restore local behavior without retaining every detail. The next concrete question is to allow a supplied finite automaton to summarize the stack, and determine whether that summary can be maintained under push and pop at strict constant cost while making projected transitions local. The challenge is to check the enlarged contract from finite source data, including restoration on pop, instead of treating a summary of the whole stack as a free observation. This would connect observational quotients to the cost of retaining just enough information for future use.