Composing restoration memory across nested calls

Version 2, 30 September 2026. Written proof with an executable finite checker. The construction uses classical saved-call-state semantics and the reversible cover from the preceding regular-history note. Novelty is not established.

The visible stack changes the restoration problem. An internal operation can be forgotten only through a finite reversible summary, but a call is allowed to save that summary in a new visible frame. When the child returns, the frame can restore the caller after arbitrarily deep nesting.

For a pure resume, this composition adds no new obstruction: finite local covers compose. A child-dependent return is different. It may ask for a distinction that the caller’s local cover deliberately merged. This note states the exact compatibility condition for supplied covers, gives a finite test for subsequential boundary transformations, and exhibits a regular counterexample in which every local segment is finitely restorable but no finite nested realization exists in the stated representation class.

1. Nested history protocols

Fix finitely many module types. Type i has a finite alphabet A_i, a nonempty prefix-closed regular history language K_i, and a finite observation f_i:K_i -> O_i. Histories are chronological words.

An internal push appends a letter when the result belongs to K_i. A typed internal pop is submitted only when it is legal and correctly typed. The implementation must restore the preceding summary, but need not detect pop underflow or a mistyped pop. Push enabledness and f_i are observed.

Calls and returns are well nested. A call symbol c, when enabled at caller history w, suspends w and starts a designated child type at its empty history. A return is submitted only at a permitted child exit. Its finite outcome is y. The call frame is removed and a supplied boundary transformation

$$T_{i,c,y}:K_i\longrightarrow K_i$$

replaces the suspended caller history w by T_{i,c,y}(w). Pure resume is the special case T(w)=w. Call enabledness, child type, child initial configuration, exit outcome, and the post-return observation are part of the source protocol. Return legality itself is promised rather than observed.

Initialization is one designated type with empty history and an empty call stack. All finite legal interleavings and all finite nesting depths count. There are no silent steps, scans, or post-input repair phases.

The target has finite active control and one immutable linked stack of call frames. Internal pushes and pops change only active control. A call allocates one frame containing a label from a fixed finite alphabet and one predecessor pointer. A return reads and removes the top frame. No raw-history pointer, auxiliary heap, mutable field, unbounded integer, or pointer-identity test is available.

The representation class here is explicitly history-functional: the active summary of a type depends only on its current word, independently of the ancestor stack or the sequence that produced that word. A supplied-summary implementation has active state (i,s) and saves only (i,c,s) in a frame. Allowing additional finite distinctions means supplying a finer summary. No necessity theorem for arbitrary context-dependent implementations is asserted.

This is a theorem about the nested operation interface. It is stronger than language equivalence and weaker than equality under arbitrary scaffold-port contexts. It does not require the stored target graph to equal a source graph.

2. The supplied-cover composition theorem

For every type i, supply a finite set S_i, an initial state s_i^0, and a map sigma_i:K_i -> S_i. It is a local reversible cover when:

1. observations and push domains depend only on sigma_i(w);
2. every legal push has a fixed update U_{i,a}; and
3. every promised legal typed pop has a fixed inverse D_{i,a}, so D_{i,a}(sigma_i(wa))=sigma_i(w).

Call enabledness and selected child type must also depend only on the caller summary. Child exits have finitely many outcomes, each determined by the child summary.

For a boundary transformation, let B_{i,c,y} be the caller histories at which the call is enabled and a legal child execution can return outcome y. For pairs w,w' in this domain, define the compatibility condition

$$\sigma_i(w)=\sigma_i(w') \quad\Longrightarrow\quad \sigma_i(T_{i,c,y}(w))=\sigma_i(T_{i,c,y}(w')). \tag{1}$$

It says exactly that the required part of a finite return table R_{i,c,y}:S_i -> S_i is well defined. Values on impossible call/outcome combinations are irrelevant. Requiring this on all of K_i is a stronger sufficient condition, not a necessary one when calls are partial.

Theorem 1 (nested composition for supplied covers). The supplied family has the supplied-summary nested implementation just defined if and only if all local cover, call, exit, and boundary-compatibility conditions hold.

Construction

Active control is a pair (i,s) with s in S_i. A call from (i,s) to child type j pushes the finite frame (i,c,s) and changes active control to (j,s_j^0). Internal operations use the child’s local tables. If it exits with outcome y, return reads (i,c,s), removes the frame, and sets active control to

$$(i,R_{i,c,y}(s)).$$

Induction on the nested execution proves the invariant: every frame holds the summary of its suspended source history, while active control holds the summary of the active source history. Local steps use the cover equations. Call establishes the invariant for a new empty child. Equation (1) establishes it again on return. Observations, push domains, call choices and outcomes therefore agree after every prefix.

Necessity

With active state (i,s) and saved caller payload (i,c,s), each internal step must obey its supplied summary equation. At an enabled call, equal caller summaries save the same data and start the same child type. Follow the same legal child execution yielding outcome y. Return sees identical local data, so its required caller summaries must agree. This gives (1) on B_{i,c,y}.

Consequently, within this uniform history-functional summary class, existence is equivalent to existence of finite local covers satisfying the reachable call, exit and return conditions. This is not a decision procedure for finding an unknown cover, and does not establish necessity for a broader class of context-dependent finite control with an immutable stack. The finite product in Section 4 decides the stronger whole-domain test for a supplied cover and total transformation; restricted domains require their own effective description.

3. Pure resume has no additional obstruction

If every return is pure resume, (1) is automatic.

Corollary 2. For finitely many reachable regular-history module types with promised typed internal pops and pure-resume returns, a finite nested realization exists if and only if every type has a finite local reversible cover.

Include finite call choices and exit outcomes in each type’s output, then minimize its partial Moore controller with output and undefined push domains observed. Run the preceding forbidden-merge test:

$$\sum_{\delta(q,a)=r}m(q)\le m(r) \qquad\text{for every }r,a. \tag{2}$$

The test and the minimum local cover are effective. If type i has N_i cover states, the nested construction has N=\sum_i N_i active states. A coarse frame-alphabet bound is |C|N, where C is the finite call alphabet. It uses one predecessor field, one top-frame read on return, and at most one logical allocation per input, only at calls. These are construction bounds, not optima.

Necessity is representation-independent inside the stated target class. An impossible local type cannot be repaired by unused call frames: hold the caller stack fixed and remain in that type. Sufficiency is the saved-summary construction. The result is a modular closure theorem, not a new reversible-automata algorithm.

4. Checking a finite-state boundary transformation

Suppose T:K_i -> K_i is supplied by a deterministic subsequential transducer: each input letter produces a finite output word, and a finite terminal output is emitted at end of input.

Compatibility with a supplied cover is decidable without enumerating history depth. Form the finite product whose state records:

• the cover state after the input prefix;
• the transducer state; and
• the cover state after the output produced so far.

Explore all legal input transitions. At each reachable product state, apply the transducer’s terminal output to the accumulated output-cover state. For each input-cover state s, collect all resulting output-cover states. Condition (1) holds exactly when every such set is a singleton. The same product checks that every produced word belongs to K_i.

This is a certificate check for a proposed cover, not a synthesis algorithm for the least stable cover. Deterministic subsequential transducers and their minimization theory are classical.

5. Local covers do not suffice for transforming returns

Let one caller type have history language {a,b}^* and observe the parity of the number of a symbols. Internal pushes are total; typed pops are promised legal. The two-state summary

$$\sigma(w)=|w|_a\pmod 2$$

is a local reversible cover: a swaps its two states and b fixes them. Use one trivial child and allow a call at every caller history.

On return, transform the suspended caller by

$$T(w)= \begin{cases} a,&\text{if }w\text{ ends in }b,\\ \epsilon,&\text{otherwise.} \end{cases} \tag{3}$$

This is a three-state subsequential transformation: it emits no transition output and emits its one-letter terminal output exactly in the “last symbol was b” state. The post-return parity is therefore the last-b predicate.

Proposition 3. This nested protocol has no finite realization in the stated target class, even though both local module types have finite reversible covers.

Proof. Suppose a realization exists. Before the call, its finite caller summary must update reversibly under both total pushes. On a finite set, each update is therefore a permutation. The finite payload saved by the call is a function of that summary. Because the child is always identical, the post-return observation forces “the word ends in b” to be a function of the caller summary.

But no finite permutation automaton recognizes that predicate. From every reachable state, applying b must reach an accepting state. The b-transition is a permutation of the reachable state set, so its image is the whole set. Every state would be accepting, contradicting rejection of the empty word and of words ending in a. Hence no finite reversible refinement can make (3) compatible. ∎

This is a representation-independent obstruction for the explicitly stated finite-control/immutable-call-stack model. It is not a lower bound for every recognizer of the resulting trace language and not an obstruction to keeping a separate record for each internal operation.

By contrast, T_y(w)=wa for child outcome y=1 and T_y(w)=wb for y=0 is compatible with the parity cover: return applies the already available a or b update. Child-dependent returns are not themselves the problem. The boundary transformer must respect the information retained by the caller summary.

6. Examples and observation boundaries

• An unbounded unary parity segment has a two-state cover. Arbitrarily many nested pure-resume calls compose by saving one parity bit per frame.
• A module containing the same-letter merge/return cycle from the regular history note has no finite local cover. Nesting cannot repair it.
• The transformation (3) defeats every finite reversible caller summary, although its subsequential transducer is finite and both modules separately pass their local tests.
• If visible-return legality must be detected rather than promised, the bounded-hidden-block theorem applies instead. For AX^*, parity cannot decide when A is exposed. This note does not weaken that result.

These examples separate three issues: restoration inside a segment, checkpointing across nesting, and compatibility of a boundary effect. A failure in one layer cannot be repaired merely by success in the other two.

7. Compilation and established theory

The construction uses one root, one immutable finite-labelled record per call, one predecessor field, and old-address radius one. It uses no pointer identity. Initialization is a finite control state and empty root. The reviewed simultaneous-record compiler therefore gives degree two and native access distance two. It preserves observation transitions on promised legal traces. The summary does not itself validate typed undo. For a chosen total completion on invalid requests, compilation preserves that completed target’s same-word language, and its PEG recognizes the reversal, exactly once. Identifying this with the language of all legal source traces requires a separately proved validator, which may change the resource bounds. It does not preserve the raw source history graph.

The saved caller state and child-state join are standard. Alur and Madhusudan’s nested-word automata define a return transition from the current linear state and the state propagated from the matching call. Their Marrying Words and Trees, Section 3.1, makes this two-input return rule explicit. Alur, Benedikt, Etessami, Godefroid, Reps and Yannakakis’s Analysis of Recursive State Machines models recursive component calls with finite entry and exit interfaces.

Those theories establish the general finite-state call/return architecture. The local reversible-cover obstruction and capacity calculation are imported from reversible automata as credited in the preceding note. Subsequential transducers are classical; see Choffrut’s Minimizing Subsequential Transducers: a Survey.

The additional result here is the explicit composition boundary for this restoration-resource problem: pure resume is exactly modular, while a transforming return requires stability of the reversible caller cover, and finite local realizability alone is not sufficient. The last-b counterexample makes that extra obstruction representation-independent in the stated model. These comparisons do not establish novelty.

8. Verification and next question

The checker constructs minimum local covers for finite examples, checks subsequential-transformer compatibility by the finite product above, and simulates nested calls and returns through the recorded depth. It verifies pure-resume parity nesting, an outcome-dependent compatible return, rejection of the last-b transformation by the parity cover, and the local forbidden-merge instance. It also exhaustively enumerates permutation transition tables through the recorded size as finite corroboration of Proposition 3.

The checker does not prove Proposition 3 for unbounded state size, synthesize a stable cover, verify a pushdown theorem in a proof assistant, or generate a scaffold.

The next mathematical bottleneck is synthesis rather than composition. Given regular local protocols and subsequential boundary transformations, decide whether some finite reversible covers stable under every transformation exist. The minimum local cover need not be stable, and a stable refinement may exist even when that minimum cover fails the supplied-cover test. The last-b example proves that refinement does not always succeed. A useful next theorem should either give an effective construction for a natural transformer subclass, or establish undecidability while retaining the exact subsequential, promised-return, and storage hypotheses.

Version history

Version 2 states the uniform history-functional representation class explicitly, restricts necessary return compatibility to possible call/outcome pairs, and separates promised-trace correctness from recognition of legal source traces. The supplied construction and the everywhere-enabled last-symbol example are unchanged. The pure-resume test now explicitly includes call and exit outputs. The earlier version 1 is retained. The substitution synthesis note gives a terminating construction for total histories with homomorphic transformations, and an iteration obstruction outside that class.