Synthesizing memory that survives substitutions

30 September 2026. Written proof with finite executable checks. This is an application of classical permutation automata and finite-algebra constructions; no novelty claim is made for those ingredients or for the resulting theorem.

Suppose we remember only whether a word contains an even number of a symbols. That is enough to append a symbol and to undo a correctly specified last symbol. It is not enough if a later operation swaps a with b: the new answer depends on the old number of b symbols. Remembering both parities repairs the problem.

The question is whether this refinement process can be made to terminate. For total word histories, fixed substitutions and fixed surrounding words, the answer is yes whenever the original observation admits finite reversible memory. The proof constructs the extra memory rather than assuming it exists.

1. The exact problem

Fix a finite alphabet A and a finite observation f:A* -> O, supplied by a total finite Moore machine. Histories are chronological words. The initial history is the empty word. There are three kinds of request:

1. append a, replacing w by wa, for each a in A;
2. a correctly typed, legal undo, replacing wa by w; and
3. one of a fixed finite list of transformations

$$T_j(w)=u_j h_j(w)v_j, \tag{1}$$

where u_j,v_j are fixed words and h_j:A* -> A* is a word homomorphism given by its finite images of letters. Those images may be empty or longer than one letter. Every append and every transformation is available at every history. Undo legality is promised, not observed.

All finite legal interleavings of these operations must be handled. After a transformation, undo acts on the resulting word, not on a saved pre-transform version. Transformation is an atomic operation of this abstract specification; we do not assume that a raw-word machine can materialize its output in one step. The implementation only has to maintain the specified observations and summary equations.

A realization is a finite set S, a history-functional map sigma:A* -> S, an initial value sigma(epsilon), and fixed finite tables U_a,D_a,R_j satisfying

$$\begin{aligned} f(w)&=o_S(\sigma(w)),\\ U_a(\sigma(w))&=\sigma(wa),\\ D_a(\sigma(wa))&=\sigma(w),\\ R_j(\sigma(w))&=\sigma(T_j(w)). \tag{2} \end{aligned}$$

There is no history pointer, auxiliary heap, allocation, scan, unbounded integer, or silent computation. A fixed table transition is one operation. No inverse of T_j is required. Two operation sequences reaching the same word must have the same summary. This last requirement explicitly defines the representation class; we do not infer it for every history-dependent machine.

2. An effective characterization

Minimize the supplied Moore machine for all forward observations. Write its accessible minimal machine as M=(Q,A,delta,q0,o) and let n=|Q|.

Theorem. A realization satisfying (2) exists if and only if, for every letter a, the map q -> delta(q,a) is a permutation of Q. When it exists, one can effectively construct a realization with

$$|S|\le |G|^{|G|^{|A|}} \le (n!)^{(n!)^{|A|}}, \tag{3}$$

where G is the transition group of M. These are construction bounds, not optimal state counts or practical complexity estimates. The test is ordinary finite minimization followed by checking letter permutations. It does not assume a stable cover or a finite-index closure.

In particular, for this transformation class, adding arbitrarily many uses of the installed transformations does not create an existence obstruction beyond the original reversible-memory test. It can require a larger summary.

Necessity: undo forces permutations

Restrict any realization to its realized states S=sigma(A*). Every U_a is total and injective: applying D_a to equal successors recovers equal predecessors. It is therefore a permutation of the finite set S. Equal summaries have equal observations after every future append word, so there is a surjection pi:S -> Q commuting with append transitions.

If U_a has finite order d, then delta(pi(s),a^d)=pi(U_a^d(s))=pi(s) for every s. Surjectivity gives delta_a^d=id_Q, so each minimal letter transition is a permutation. This argument already uses only append and promised undo.

Construction: close the possible interpretations of a word

Let G be the finite group generated by the letter permutations of M. Use multiplication in reading order: first apply the left factor, then the right factor. Let mu:A* -> G send a word to its transition permutation. Then f(w)=o(q0 mu(w)).

A homomorphism phi:A* -> G is determined by its |A| letter values. There are at most |G|^{|A|} such homomorphisms. Starting with mu, repeatedly add phi composed with h_j for every currently stored phi and installed substitution h_j. This process terminates within that bound. Call the resulting finite set E.

Now keep the tuple

$$\sigma(w)=(\phi(w))_{\phi\in E}. \tag{4}$$

The mu coordinate recovers f(w). Append and undo are coordinatewise right multiplication and its inverse:

$$U_a(s)_\phi=s_\phi\phi(a),\qquad D_a(s)_\phi=s_\phi\phi(a)^{-1}. \tag{5}$$

The transform table is

$$R_j(s)_\phi=\phi(u_j)\, s_{\phi\circ h_j}\,\phi(v_j). \tag{6}$$

The referenced coordinate belongs to E by construction. Substituting s=sigma(w) into (6) gives phi(u_j h_j(w)v_j) at every coordinate, which is exactly the required summary. Thus equal summaries remain equal after every installed transformation, including any finite composition of them.

For an explicit transition table, enumerate the tuples reachable from the all-identity tuple under appends. This set is S=sigma(A*), a finite submonoid of the finite group G^E, hence a subgroup. Inverse updates remain in it. Formula (6) also maps it into itself because (1) maps words to words. All tables are therefore effective. Induction on legal operation sequences proves every equation and observation in (2), for unbounded history length.

This proves the theorem. The small epsilon-delta-like point is the choice of information: retain enough coordinates in advance that every allowed future change acts on the retained tuple. No continuity statement alone would give this finite construction or its termination bound.

3. What refinement buys, and where it fails

Two states must become four

Observe f(w)=|w|_a mod 2 over {a,b} and install the swap h(a)=b, h(b)=a. The minimum local observation machine has two states. It merges epsilon with b, but their swapped observations differ.

The closure E has the two evaluations counting a and counting b modulo two. Their tuple has exactly four reachable states. Appends toggle the appropriate bit, typed undo does the same, and swap exchanges the bits.

Four is necessary here: any stable summary must determine both f(w) and f(h(w)), and all four pairs occur. Thus this is a case where failure of the minimum local cover is repaired by a strictly larger finite cover.

Expansion and erasure can still work

For the same observation, the substitution a -> ab, b -> a can increase word length repeatedly. On the pair (p_a,p_b) of parities it is simply (p_a,p_b) -> (p_a+p_b,p_a) over the two-element field. Erasing b acts as (p_a,p_b) -> (p_a,0). These maps need not be invertible: only typed append-undo pairs require inverses. Fixed prefixes and suffixes add their own parity contributions.

The construction also works for noncommutative transition groups. It retains word order whenever the observation depends on it; it is not restricted to counting letters.

A regular observation may already fail

The predicate “ends in b” has a two-state forward machine whose b transition merges both states. It fails the permutation test. No finite summary can support both total appends and promised typed undo for that observation, even before any substitutions are added.

General finite-state transformations remain outside the theorem

Start instead with the locally reversible parity observation. The subsequential transformation sending a word to a exactly when it ends in b, and to epsilon otherwise, forces the forbidden last-b observation. No finite reversible refinement can support it. If every b transition entered an accepting state in a finite permutation machine, surjectivity would make every state accepting, contradicting rejection of epsilon.

Consequently the theorem does not extend to arbitrary deterministic subsequential transformations. Neither regularity of the transform nor existence of the local cover suffices. The obstruction concerns every finite history-functional summary in this model, not every presentation of a language and not an implementation with an extra undo stack.

4. Finite horizons do not guarantee one finite memory

There is a stronger boundary example than revealing the last symbol. Let P(w) retain positions 1, 3, 5, and so on, and still observe only f(w)=|w|_a mod 2. A two-state sequential transducer implements P: its state toggles on every input letter, emitting the letter in one state and nothing in the other. Both input letters permute its control states. It has empty terminal output. Thus even reversible transducer control does not supply the closure property of a word homomorphism.

Proposition. No finite history-functional summary can preserve f and support arbitrary repetitions of P, even without undo. Nevertheless, for every fixed r, the observations f(w),f(P(w)),...,f(P^r(w)) admit one finite summary with total appends and promised typed undo.

Proof of the obstruction. Put w_j=b^(2^j)a, for j>=0. The single a begins in position 2^j+1. After k applications of P, the retained original positions are exactly those congruent to 1 modulo 2^k. Therefore

$$f(P^k(w_j))= \begin{cases}1,&k\le j,\\0,&k>j.\end{cases} \tag{7}$$

For j<ell, the experiment P^(j+1) separates w_j and w_ell. They must have different stable summaries. Infinitely many such histories rule out every finite S, irrespective of how it is encoded. The proof requires only observation preservation and a fixed update table for P. It does not require the append tables to be invertible.

Proof for each finite horizon. For a fixed r>=0, retain word length modulo 2^r and r+1 bits. Bit k is the parity of the a symbols in positions congruent to 1 modulo 2^k, for 0<=k<=r. When appending a at new position n+1, toggle bit k precisely when n=0 mod 2^k; appending b changes no bits. Increment the length residue. Typed undo decrements that residue first and reverses those same toggles for the supplied letter. These are finite permutation updates. Initialization is the all-zero state. All requested horizon observations are the corresponding bits. A bound is 2^(2r+1) states; no optimality claim is made. This summary is not asserted closed under another P operation, which can demand the next missing bit. This proves the proposition.

For the experiment family consisting only of repetitions of P, define distance as 2^(-k) where k is the first differing observation. Equation (7) gives

$$d(w_j,w_ell)=2^{-(j+1)}\quad(j<ell).$$

Thus the words can agree over longer and longer future horizons while still requiring distinct exact summaries. The relevant quantifier distinction is “for every horizon, some finite memory” versus “one finite memory for all horizons.” This is not an impossibility result for persistent graphs: an implementation allowed to allocate records after internal operations is outside the proposition’s finite-summary model.

5. Nested calls and the scaffold consequence

For finitely many module types, apply the construction separately to each alphabet and observation. Include all finite call choices and exit outputs in that type’s observation before minimizing. Suppose each active module has total internal histories, promised legal typed undo, and return effects of form (1), selected from a finite table by the call and child outcome.

Save (caller type, call type, caller summary) in an immutable call frame, initialize the child at the all-identity tuple, and on a promised legal return apply (6) to the saved summary. Induction preserves the summaries of every suspended caller and the active child, at every finite nesting depth. This establishes sufficiency even when some calls or exits are disabled by the finite observation. No assertion about an unobserved transformation at an impossible exit is needed.

If type i uses N_i summary states, a coarse bound is sum_i N_i active states and |C| sum_i N_i frame labels. Only calls allocate, at most one finite-labelled record with one predecessor field. Returns read the top frame and restore its predecessor root. Internal operations use no heap access or allocation. Initialization is an empty root and the root type’s empty-word summary. These bounds are not claimed optimal.

This target satisfies the reviewed simultaneous-record compiler: one root, one record field, at most one allocation, old-address radius one, no pointer identity, and finite initialization. It therefore has a degree-two, native-distance-two scaffold implementation of its observation transitions on promised legal traces, one physical scaffold node per request.

The promise matters for languages. The construction does not detect an incorrect typed undo. It cannot on its own recognize the language of all and only legal source traces. For any chosen total completion of the target on invalid requests, the compiler preserves that completed target’s language on the same words; the corresponding PEG recognizes its reversal, once. Equating that language with an exact legal-source-trace language additionally requires a proved validator. Adding a validator may change the resource bounds. There is no claim of raw stored-graph equivalence or preservation under arbitrary scaffold-port observations.

6. Relation to established theory

The group criterion is the total-transition case of classical reversible automata. Golovkins and Pin’s Varieties Generated by Certain Models of Reversible Finite Automata, Section 2, identifies complete permutation automata with group languages. The preceding regular-history note supplies the exact broader partial-transition result and its original sources.

There is also a classical algebraic explanation of termination. Taking every assignment A -> G in (4) records the word function on a fixed finite group. These functions form a finite group under pointwise multiplication, and substitution preserves equality of word functions. This is the free algebra/relatively free group construction for the variety generated by G. Burris and Sankappanavar’s A Course in Universal Algebra, II.10.2, II.10.12 and II.10.16, give term functions, the product construction, and local finiteness for a variety generated by finitely many finite algebras. The orbit E simply keeps fewer coordinates when only selected substitutions are installed.

Nested caller-state storage remains classical nested-word/recursive-state machinery, as documented in the composition note. This argument is not a transducer-uniformization theorem: all transforms are supplied deterministic functions, and there is no selection problem over a relation. It imports no new pointer-machine or cell-probe lower bound.

Residual separation by future experiments is classical. The every-other-symbol example uses that method to separate finite-horizon reversible summaries from one invariant finite summary, even for a two-state transducer with permutation input transitions. This is a direct counterexample, not a new general lower bound method or a claim that the example is absent from prior literature.

The contribution to this program is an explicit terminating synthesis route with legal-undo, repeated-transformation and bounded-allocation contracts. It resolves the saved subclass question and provides a strict refinement example. The algebraic construction is established; the precise application has not been established as novel. It should remain a research note.

7. Verification and remaining question

The executable construction builds the finite evaluation orbit, enumerates every reachable summary in selected examples, and checks every push/inverse and installed-transform table entry. It independently evaluates raw words through the recorded length, including a noncommutative group example. Its output separates exhaustive finite-table checks from bounded word corroboration. The general theorem above is a written proof, not a proof-assistant result.

The checker also verifies (7) on a recorded finite family and compares the finite-horizon summary against raw words. The infinite separating family and all-horizon construction are established by the written proof, not those finite tests.

The next question should return to bounded persistent memory. Over the same binary-history interface, allow a fixed number of roots, finite labels, bounded record arity, bounded local pointer access and a fixed number of immutable allocations per request. Can this model maintain parity under append, promised typed undo and the every-other-symbol operation P with worst-case constant work per request? The source operation is still abstract; the target must actually meet the resource contract. A construction would show exactly how persistent structure overcomes the finite-summary boundary. A lower bound must quantify over every representation in that explicit model. An amortized construction, a failure of one layout, or the finite-summary proposition would not settle it. General subsequential finite-summary synthesis also remains open, but this representation question connects more directly to the program’s central goal.

Change record

Initial note, 30 September 2026. The language-transfer paragraph explicitly separates promised behavior from recognition of legal operation traces. The companion composition note’s second version adopts that qualification and states its supplied-summary and reachable-call domains explicitly.