When does a finite summary make forgetting local?

Research note, 30 September 2026. Written proof, not proof-assistant verified. The source model and preservation contract are explicit below. Classical ingredients and the closest comparison found are credited in Section 8. Novelty is not established.

1. The missing operation is restoration

The preceding erasure criterion allowed no new information in projected control. That made it exact but deliberately strict. Two histories can need different next actions even when their projected controls and visible stack tops agree. A finite summary of the hidden stack can sometimes retain the missing distinction.

Push is the easy direction. If a new symbol is placed on top of a stack, a finite summary can often be updated from the symbol and the old summary. Pop is the hard direction. Once a hidden top frame has been discarded, the summary of the exposed tail is not automatically recoverable from the current summary. Reading it from the old concrete record would retain precisely the memory that the quotient was supposed to erase.

This note gives a necessary-and-sufficient finite test for a supplied finite-monoid summary. The test makes restoration part of the local quotient contract. Passing it means that the erased machine itself can update the summary from its current finite control, visible top and input. No concrete stack pointer, predecessor graph or historical oracle is available at run time.

2. Model, summary and exact observation

Let P be a finite, possibly nondeterministic and partial, real-time pushdown machine. It has finite control Q, input alphabet Sigma, stack alphabet Gamma, a finite nonempty set of initial controls and initially empty stacks. One input letter causes one push, pop or keep. Rules inspect only the current control and one raw top symbol or emptiness. Empty pop is disabled or normalized to keep. There are no epsilon moves, top rewrites, scans or post-input steps. The acceptance bit o(q,g) may inspect control and raw top or emptiness. Every finite legal run counts, including rejecting and stuck-prefix runs.

Supply:

1. a control map kappa:Q -> Qbar;
2. a label map pi:Gamma -> Gammabar union {epsilon};
3. a finite monoid (M, multiplication, 1) and a map mu:Gamma -> M.

The third map extends uniquely to a monoid morphism

$$\eta:\Gamma^*\longrightarrow M, \qquad \eta(gu)=\mu(g)\eta(u). \tag{1}$$

Stacks are written top first. The finite multiplication table, identity and generator map are part of the input, so associativity and the identity laws are directly checkable. Any regular finite observation can be refined to a transition-monoid observation, although that refinement need not be minimal.

Define

$$E_\eta(q,s)=\bigl((\kappa(q),\eta(s)),\pi(s)\bigr). \tag{2}$$

The desired quotient Phat has exactly the controls Qbar x M, stack alphabet Gammabar, empty initial stack and initial finite controls (kappa(q0),1). Its transition and acceptance tables inspect only their finite control and one projected top symbol or emptiness. They use the same unit push, pop and keep operations. For every reachable source configuration x and input letter a, require

$$o(x)=\widehat o(E_\eta(x)),\qquad \{E_\eta(y):x\xrightarrow a_Py\} =\{z:E_\eta(x)\xrightarrow a_{\widehat P}z\}. \tag{3}$$

These are successor sets, not multisets. Thus (3) preserves observations and input-labelled branching, but not run multiplicity. The question is about this supplied projection, summary and local interface. It is not a question about every presentation of the same language.

3. Finite restoration descriptors

Use bot for an empty raw or projected top. For a nonempty stack s=gu, record

$$(q,g,m,t,\tau) =\bigl(q,g,\eta(s),\operatorname{top}(\pi(s)),\eta(u)\bigr). \tag{4}$$

For the empty stack use (q,bot,1,bot,1). Call a descriptor realizable when some reachable source configuration has those values.

For a source rule enabled at (q,g) define its summary-aware projected signature. If its target control is q', the signature contains the next abstract control and projected stack operation:

The target control component is always kappa(q'). Let S_eta(q,g,m,t,tau,a) be the set of these signatures over all source rules on input a, with duplicates removed.

Group realizable descriptors by the local abstract cell

$$(\kappa(q),m,t). \tag{5}$$

Finite summary criterion. In each group require:

1. every source acceptance bit o(q,g) is the same;
2. for each input a, every signature set S_eta is the same.

The tail summary tau appears in the descriptor because a pop may expose it. It is not supplied to the quotient rule. Uniformity asks whether the quotient can determine the correct successor without seeing it.

Theorem 1 (finite-summary local quotient characterization). The criterion holds if and only if a one-top unit-stack quotient satisfying (3) exists for the supplied kappa, pi and eta. The criterion is decidable and constructs the quotient when it succeeds.

This is a characterization of the stated representation class, not of all finite summaries or all bounded persistent representations.

Deciding realizability

For each source control q, classical pushdown saturation computes a finite automaton for the reachable stack language R_q. For g in Gamma, a candidate descriptor is realizable exactly when the following regular language is nonempty:

$$R_q\cap g\eta^{-1}(\tau)\cap\eta^{-1}(m) \cap\pi^{-1}(\operatorname{Top}_t). \tag{6}$$

The empty case is checked separately. Each monoid fiber is regular, and inverse homomorphisms preserve regularity. Since m=mu(g)tau for a nonempty stack, there are at most

$$|Q|(|\Gamma|+1)|M|(|\bar\Gamma|+1)$$

consistent candidates. No stack-depth bound is used.

As in the previous note, a supplied regular inductive invariant I can replace exact reachability. Initial inclusion and transition closure are decidable by finite-automaton operations. The criterion is then necessary and sufficient on all configurations in I, and sufficient for reachable behavior. Failure on a strict overapproximation need not imply failure on the true reachable set. The executable checker uses this invariant form.

4. Proof of Theorem 1

Sufficiency

For each realized cell (u,m,t), use its common signature set as the quotient transition table and its common acceptance bit as the quotient observation. The table contains the next monoid element as part of finite control. It does not compute that element by visiting an erased record.

Every source operation commutes with (2). Push follows the monoid law (1). Keep leaves both stack and summary fixed. A source pop of s=gu changes the summary to the descriptor’s tau=eta(u) and changes the projected stack by pop exactly when g is public. Thus every source successor projects to a quotient successor with its listed signature.

Conversely, signature-set equality says that every quotient signature is available from every represented concrete configuration in its local cell. Choosing a corresponding source rule lifts the quotient step. This proves both inclusions in (3). Reachability is closed under transitions, so induction gives back-and-forth run correspondence and identical existential acceptance after every input prefix, including the empty prefix.

If the source is deterministic, each realized table entry has at most one signature and the quotient is deterministic. If the source is complete, each realized table entry is nonempty. Fill unrealized cells with arbitrary keep rules; they remain unreachable by the lifting argument. This produces a complete quotient without adding a new state.

Necessity

Fix a projected stack word v. A normalized signature has a unique effect on v: push increases length and identifies the pushed label, pop decreases length, keep preserves length, and the successor finite control identifies both the projected source control and next monoid summary. Hence the successor set at v uniquely determines the signature set.

A one-top quotient must use one transition table at every stack with the same finite control (u,m) and projected top t, regardless of its deeper projected tail. Equation (3), applied separately at each represented word v, therefore forces every concrete descriptor in cell (u,m,t) to have that same signature set. Its acceptance table forces the observation bits to agree. These are exactly the two finite conditions.

This also isolates restoration. In the deterministic case, two reachable configurations in one local cell cannot pop to different next summaries. If they do, no local quotient can repair the conflict by inspecting the erased tail.

5. Resource and observation consequences

A passing quotient has at most |Qbar||M| finite controls, uses the projected stack alphabet, consumes exactly one source input per step and allocates a logical stack frame only on a projected push. The summary occupies finite control. It adds no pointer field and no historical lookup.

If a complete source also has a supplied bound on pairwise projected stack height spread, the earlier bounded-spread theorem applies to this quotient. The resulting implementation has one logical stack root, one field per logical record, at most one logical allocation per input, degree two and native access distance two, with fixed virtual initialization and no padding letters. It recognizes the same-word source language. Transferring the scaffold to a PEG gives the reversed language, exactly once:

$$L(P)\quad\longmapsto\quad L(P)^R.$$

The construction preserves acceptance and projected branching. It does not preserve erased raw frames, run multiplicity, an individual nondeterministic history, or the raw graph vocabulary.

For a deterministic passing source, pulling the quotient prefix metric back through E_eta again gives

$$d_\eta(F_a x,F_a y)\leq2d_\eta(x,y). \tag{7}$$

Here equality at distance zero includes agreement of the retained monoid summary. If acceptance reads the projected top, agreement through r+1 projected cells gives identical acceptance answers for every continuation of length at most r; control-only acceptance needs r cells. Equation (7) describes the fixed quotient controller, not arbitrary future scaffold-testing contexts. Native endpoint observations still use the reviewed frontier layer.

6. Positive examples

Exact restoration of a parity summary

Let X be private and A public. Use source controls q_i, b_i, d_i for i in {0,1}. Their exact reachable stack invariants are

$$q_i:(XA)^n\text{ with }n\equiv i\pmod2, \qquad b_i,d_i:A(XA)^n\text{ with }n\equiv i\pmod2. \tag{8}$$

From q_i, input u pushes A and enters b_i; from b_i, input v pushes private X and enters q_{1-i}. From a nonempty q_i, input x pops X and enters d_{1-i}; from d_i, input a pops A and enters q_i. The source accepts exactly in q_0 at the cuts being observed.

Project X to epsilon and A to A. Merge the parity-indexed copies of each control family. Without a summary the projection fails: reachable q_0 and q_1 configurations can have the same projected top A but different acceptance bits.

Now take M=Z/2Z and let eta count X frames modulo two. A private X pop becomes a projected keep while flipping the finite summary. A public A pop leaves the summary fixed. The regular invariant certificate verifies all four unbounded families and the local criterion without a depth cutoff. This is a genuine pop-restoration example: the quotient updates the retained bit from its current bit and local rule, not from the popped concrete node.

Repairing the missing deeper control bit

The preceding note’s finite obstruction built AB0 and AB1 in controls that were projected to one control. On the next input the two histories had to push C0 and C1. A one-top quotient could not choose between them.

Use the three-element monoid that records the rightmost occurrence of B0 or B1, treating all other symbols as the identity. Its multiplication returns the right operand when that operand is nonidentity, and otherwise the left operand. The summaries of AB0 and AB1 are different, so the enlarged local cells select the correct pushes. The seven reachable configurations pass the new criterion; the trivial one-element summary reproduces the old failure.

This repairs that presentation. It is not a claim that every locality failure has a useful small summary.

7. A pop obstruction for a familiar summary

Let the only raw stack symbol be private X, and erase it. Input p pushes X; input r pops it when nonempty. Consider the finite summary

$$\eta(s)=\{\text{labels occurring in }s\},$$

whose monoid operation is set union. Push is perfectly local. Yet stacks X and XX have the same projected stack, the same raw top and the same current summary {X}. After one pop their summaries are respectively the empty set and {X}. The source configurations are both reachable.

The criterion therefore rejects this summary with the exact witnesses X and XX. A saved predecessor or concrete tail pointer can restore the old set, but an erased one-top quotient cannot. This is a limitation of this summary and interface, not an impossibility theorem for all summaries or pumping methods.

8. Relation to established work

Regular stack observations are classical. Esparza, Kucera and Schwoon, Model-Checking LTL with Regular Valuations for Pushdown Systems, allow atomic propositions to denote regular configuration sets. That supplies an important offline verification mechanism; it does not by itself make a regular whole-stack property locally maintainable after erasure.

Earl, Might and Van Horn, Stack-Summarizing Control-Flow Analysis of Higher-Order Programs, explicitly add client-defined finite stack summaries and a push operation. For pop, their analysis restores older summaries through matching paths and a predecessor relation in the Dyck-state graph. That is precisely the resource distinction at issue here. Their theorem establishes sound abstract analysis; the present theorem asks when an exact real-time quotient can perform the same restoration using only its current local state.

The semantic quotient step remains an instance of classical homomorphism and bisimulation theory, as in Rutten’s Universal coalgebra. Effective reachability continues to import the regular post* construction of Esparza, Hansel, Rossmanith and Schwoon. Finite monoids as recognizers of regular word properties are classical.

The additional argument here is the explicit restoration descriptor, the necessary-and-sufficient local signature test for a supplied monoid summary, and its composition with the bounded persistent compiler. It is a narrow exactness and resource theorem, not a new theory of stack summaries. A literature search and these comparisons do not establish novelty.

9. Verification and next question

The executable checker verifies finite monoid laws, regular invariant closure and every realized finite descriptor for the parity construction. It confirms that the parity summary passes while the trivial summary fails, that the rightmost-tag summary repairs the finite missing-bit example, and that the frame-set summary fails on X versus XX. The DFA products cover the stated regular invariants without a stack-depth cutoff. See the recorded output.

The checker does not implement general pushdown saturation, synthesize a summary, minimize one, generate a scaffold or verify the written theorem in a proof assistant.

The next decisive question is intrinsic rather than another supplied-certificate variant. For fixed source maps kappa and pi, define the least equivalence on reachable stack histories that separates conflicting local successor and acceptance behavior and is stable under adding a raw top symbol. Does a finite locally restorable summary exist exactly when this restoration congruence has finite index? For which deterministic or visibly structured subclasses can that index, or a least finite summary, be computed? A positive answer would turn the present sufficient input format into a Myhill-Nerode-style characterization. A negative answer should retain the precise source class and resource interface.