When retained frames can carry the missing history

30 September 2026. Research note with a written proof and finite executable checks. Novelty is not established; the construction uses ordinary finite buffering and persistent-stack checkpoints.

Suppose private stack frames are to disappear, while public frames remain. Keeping the parity of the private depth can be enough to undo a promised private push. It cannot tell us whether a public frame is now exposed. For example, after one private pop, AX exposes A, while AXXX does not. The private depths initially have the same parity.

This boundary matters when a return must be checked, rather than promised legal. The result below gives an effective characterization for a particular stack interface. It allows unbounded total depth and unboundedly many erased frames, but requires a uniform bound on each consecutive private block. The retained public frames then store the bounded information needed when an older part of the stack becomes active again.

1. Model and permitted representations

Stacks are written chronologically, with the top on the right. Fix disjoint finite alphabets H (hidden) and V (visible), and Gamma=H union V. The legal stack words form a nonempty prefix-closed regular language K. An accessible finite partial deterministic Moore machine M=(Q,Gamma,delta,q0,o) presents it: s belongs to K exactly when delta(q0,s) is defined. Outputs belong to a finite alphabet. A DFA for K and a separate regular observation can be combined by a finite product.

There is one request +g and one request -g for each raw label g. From stack s, +g appends g exactly when sg belongs to K. The request -g deletes the last label exactly when it is g. The empty stack has no pop. Every such pop is available; there are no extra control restrictions on returning. The observation is o(delta(q0,s)). We start at the empty stack and require correct behavior for every sequence of requests, including exact rejection of illegal requests. Each successful request takes one step. There are no silent steps or scans.

The target has finite control S and a single immutable linked stack of visible frames. Its root represents exactly the visible projection of the raw stack. Each visible frame may carry a label from a fixed finite payload alphabet, chosen on allocation, and one predecessor pointer. Rules may read finite control and the top frame, including whether the root is empty.

• A hidden push or pop changes only finite control. It cannot allocate, modify a record, change the root, or keep an auxiliary pointer.
• A visible push allocates one frame above the current root. Its finite payload is computed locally.
• A visible pop drops the top frame and may restore finite control from its payload. It reads no deeper frame in that step.

All control registers count in S; the payload alphabet is fixed independently of history length. There is no raw-history oracle, arithmetic counter of unbounded size, auxiliary heap, mutable annotation or pointer-identity test. The theorem ranges over every representation satisfying these restrictions, including refinements other than monoid summaries. It does not restrict all persistent pointer machines or all recognizers of a language.

The required observations are the output and all push and typed-pop domains. The target must preserve these and the successor behavior under every legal request. These are contexts over this stack interface, not arbitrary scaffold port-inspection contexts. The contract is stronger than language equivalence.

2. Characterization and effective test

A hidden block is a consecutive factor consisting only of symbols of H. Let B be the supremum of its lengths over words in K, counting the initial and final blocks too; set B=0 if no hidden symbol occurs.

Theorem (bounded hidden blocks). A realization in the preceding model exists if and only if B is finite. Given M, finiteness and the least such B are computable. If B is finite, write

$$T_B=\sum_{j=0}^{B}|H|^j.$$

There is a realization with at most |Q| T_B control states and |V| |Q| T_B frame labels, one predecessor pointer per frame, one top-record read per request and at most one allocation, only on a visible push. Use T_B=1 when H is empty. These are construction bounds, not claimed optimal state or alphabet sizes.

For the decision procedure, discard unreachable states of M, then keep only its hidden-labelled edges. A directed cycle exists in that graph exactly when B is infinite. Otherwise B is the longest path length in this acyclic graph, and in particular B<=|Q|-1.

This test concerns the supplied legal stack language, not a proposed summary. It is independent of which deterministic presentation is used: a hidden path spells an actual allowed block, and every allowed block induces such a path. A reachable hidden cycle can be repeated after a prefix reaching it. Conversely, a path longer than the state count repeats a state. No residual minimization is needed for this boundedness test.

3. Why unbounded hidden blocks are impossible here

First, distinct raw stack words have different interface behavior, even with constant output. Pop their longest common suffix using matching requests. Then either one remaining stack is empty and the other is not, or their top labels differ. A further typed-pop request is legal from only one. This is an elementary residual-distinguishability argument.

Fix a reachable prefix u that is empty or ends in a visible symbol. Execute its pushes from initialization and hold the resulting target visible stack fixed. For every hidden continuation

$$W_u=\{w\in H^*:uw\in K\},$$

reach uw by hidden pushes from that same target configuration. No such push can change a frame or the root. Distinct words of W_u must therefore have distinct finite controls: otherwise the whole target configurations agree, but the preceding pop experiment distinguishes their sources. Thus every realization has the lower bound

$$|S|\geq |W_u|\quad\text{for every such }u. \tag{1}$$

In particular, a hidden block of length n supplies all n+1 prefixes in one W_u, because K is prefix-closed. Hence n+1<=|S|. Unbounded block length contradicts finiteness of S.

The proof permits arbitrary finite visible payloads. They cannot change during the hidden block. It does not assume the implementation stores a particular quotient, follows a monoid law, or uses minimal forward states. It does assume the immutable-root and exact-domain contract stated above. For example, a separate immutable cell per hidden push defeats this lower bound by changing the permitted storage model.

4. Construction and restoration across older visible frames

Assume B is finite. Write a stack uniquely as

$$w_0v_1w_1\cdots v_kw_k, \qquad w_i\in H^{\leq B},\quad v_i\in V.$$

Finite control is (p,w). Here w=w_k is the current hidden block and p is the Moore state immediately after the most recent visible symbol, or q0 if there is none. The current Moore state is q=delta(p,w). Every visible frame stores (v,p_old,w_old), the caller’s finite control just before that visible push, together with its predecessor pointer. This saves at most B raw hidden labels in each frame, not an unbounded history.

Initialization has control (q0,epsilon) and an empty root. The rules are:

No legal hidden push exceeds B, by its definition. The output is o(q). All word operations in this table are functions on fixed finite sets and can be precomputed as finite transition tables. The theorem does not charge an unbounded scan of w to one step. For each fixed input machine and bound, w is part of finite control.

The invariant follows by induction on the decomposition. Hidden requests alter just its final block. A visible push creates its new final separator, saving the old active block and its starting Moore state in that separator. A visible pop is legal only when the final hidden block is empty. Its saved payload is exactly the old active block, including its old starting state; reading that payload restores the full invariant in one step. The predecessor frames have never changed. Thus a return to an arbitrarily old visible frame is covered by the same induction, with no bound on the number of visible frames or on how long ago they were created.

The tests agree exactly with the source domains. Prefix closure ensures that every matching raw pop remains in K. Moore outputs agree by the invariant. Induction on arbitrary interleavings establishes the whole-run claim, not just behavior along a push-only history. Equivalently, the encoding commutes with every legal request and reflects every illegal one.

5. Examples and failed alternatives

Unbounded total hidden memory can still be packed. Let K=Pref((AX)*), with A visible and X hidden. The stack can contain arbitrarily many X frames, but each hidden block has length at most one. The construction succeeds. A Moore observation can count all X symbols modulo two. On the stack AXA, popping the last A must restore the older active block X; simply resetting the active block to empty fails immediately. This is the essential checkpoint test.

The earlier alternating private-X/visible-A parity controller uses a more restricted request discipline and control phases. It already passes its own supplied-summary test. The example here preserves the same unbounded alternation phenomenon under the stronger full typed-pop interface; it is not a claim that the two source controllers are identical.

One visible anchor does not suffice for an unbounded gap. Let K={epsilon} union AX*. After the first A, the retained stack has just one unchanging frame while the hidden suffix grows. No finite control can validate all typed pops. In particular AX and AXXX have the same parity, but after -X, the request -A is legal only for the first. A two-state reversible parity action within that region does not supply a valid boundary interface. Boundary-indexed capacity tests that ignore return legality are therefore insufficient for this exact contract.

The X/XX obstruction persists. With K=X* and no visible symbols, all hidden depth is erased. The frame-set summary already fails on X and XX; (1) now rules out every finite refinement that must validate all pops. Under a legal-pop promise and parity-only output, two states still suffice. Removing exact-domain observation changes the theorem.

Finite gaps need not alternate singly. A protocol permitting any word with at most two consecutive hidden labels from {X,Y} has B=2 while visible depth is unbounded. A buffer of at most two labels plus the stored Moore state suffices. Arbitrary hidden branching matters quantitatively: if all hidden words through depth B are allowed above one fixed prefix, (1) forces at least T_B control states. This lower bound matches the buffer’s word count, not necessarily the complete construction’s state count.

When every symbol is visible, B=0 and this is the ordinary saved-state stack. When no symbol is visible, bounded hidden blocks means that K is finite, recovering the exact typed-pop boundary from the preceding note.

6. Compilation and what is preserved

The implementation has one root, immutable finite-labelled records with one pointer field, at most one allocation, and old-pointer paths of length at most one. It inspects the top label or empty root and never tests physical alias identity. Initialization is empty, or equivalently a fixed virtual sentinel. The reviewed simultaneous-record compiler therefore applies with s=1, A=1, q=1, r=1, giving degree two and native access distance two. This is a construction bound; there is no degree optimum claim.

For language recognition, totalize illegal requests into a rejecting absorbing state, using no logical allocation on them. Choose any accepting Moore outputs. This gives a strict one-input-step recognizer, including its empty-input decision. The scaffold recognizes the same operation-trace language; the PEG recognizes its reversal, exactly once.

The compressed records do not have the same raw graph vocabulary as the original stack. The decoding reconstructs the current logical stack, but arbitrary port observers can distinguish the physical representations. Compiler preservation of decoded records and a fixed controller’s language must not be confused with raw stored-graph equivalence. The scaffold itself still adds one physical node per input, even when the source allocates no logical frame.

7. Established ingredients and the remaining contribution

The lower bound uses classical future-residual distinguishability and finite state counting. The positive construction uses finite buffering and saved caller data, not a new persistence method. Driscoll, Sarnak, Sleator and Tarjan’s Making Data Structures Persistent (1989) is a primary persistence reference. Our direct immutable list requires none of its general transformation machinery.

Alur and Madhusudan’s Visibly Pushdown Languages (STOC 2004; this author manuscript is dated 2005), Section 2.1, fixes stack operations by input class. It also describes moving top information into finite control while storing restoration data in the stack alphabet. Our source requests are visibly pushdown operations; the target reclassifies hidden pushes and pops as internal steps. The question here is when this specified reduction in allocation can preserve exact interface behavior. It is not their general VPL characterization or determinization theorem.

The preceding reversible-automata comparison remains relevant precisely because it preserves promised undo, not observable pop legality. Its capacity inequalities cannot simply be applied independently to regions while omitting the region-exit test. No general transducer uniformization theorem or pointer-machine lower bound is imported here. General pointer machines with extra allocations are outside this restriction. No claim about effective PEG pumping follows.

The additional result in this note is the explicit equivalence between a checkable property of the legal stack language and existence of any finite annotation implementation in the specified immutable visible-stack class, together with its exact restoration invariant and compiler parameters. The elementary ingredients and comparisons do not establish originality. This is a research characterization of a narrow resource interface, not yet a fundamental theorem about arbitrary persistent computation.

8. Evidence and next boundary

The checker detects hidden cycles, computes finite longest-path bounds, and checks the checkpoint construction against a raw-stack interpreter on all legal words up to the recorded depth, including every enabled and disabled operation at those words. It includes a mutation that discards the saved hidden block and fails on AXA -> AX. See the recorded scope and output. These finite checks corroborate the construction. The unbounded theorem is the written argument above; it is not proof-assistant verified.

Exact typed-pop observation separates every raw stack, so this theorem compresses a representation without identifying different logical stacks. It is lossless packing, not semantic forgetting. This is a useful boundary for the broader program: genuine forgetting must exploit a smaller family of observable futures.

The next question is what replaces the gap bound when a controller exposes only some returns, or promises their legality. In that setting distinct hidden words may have identical future behavior and genuinely compressible unbounded gaps reappear. A useful successor theorem must specify the boundary-exit observations and compose restoration summaries across saved frames. It must include both the exact-domain theorem above and the parity example with promised returns, rather than silently changing from one contract to the other.