The exact cost of restoring a regular history

30 September 2026. Written proof and executable finite construction.

Suppose a controller accepts a sequence of operations, and a legal undo request names the operation being undone. Can the history itself be discarded while retaining enough finite memory to restore the controller?

For a regular history protocol, classical reversible-automata theory answers this question effectively. The answer depends on how many distinct memory states must sit above each forward behavioral state. Merges consume that capacity. A particular merge into a cycle demands more capacity than any finite memory can supply.

This note gives a self-contained proof for the observation and restoration contract below. The obstruction and minimum-copy construction are established reversible-automata results, not a newly discovered FPRD theorem.

1. The protocol and what is observed

Use chronological words, with a new operation appended on the right. Let M=(Q,A,delta,q0,o) be an accessible finite partial Moore machine with finite output alphabet. A word w is legal when delta(q0,w) is defined; write K for this prefix-closed regular language. Its observation is f(w)=o(delta(q0,w)).

The source configuration is the whole current legal history w in K, not just its state in M. Push a changes w to wa when legal. The protocol may also submit a correctly typed pop wa -> w. Any interleaving of legal pushes and such pops is allowed, from the fixed initial history epsilon.

The summary must preserve:

• the observation after every operation;
• exactly which next pushes are permitted; and
• the previous summary after every legally supplied typed pop.

It need not detect pop underflow or verify that the supplied pop type matches the top of the discarded history. Thus reverse enabledness is not part of the observation. No source-history pointer, scan, or external restoration data is available to the summary.

A finite realization consists of a finite realized set S, a map sigma:K -> S, a fixed s0=sigma(epsilon), an output map, and fixed push and pop tables U_a,D_a. On every legal edge,

$$U_a(\sigma(w))=\sigma(wa),\qquad D_a(\sigma(wa))=\sigma(w).$$

The domain of U_a reflects push legality exactly. Values of D_a on requests that are illegal at the concrete history are immaterial.

First minimize M with both output and undefinedness observable. In the rest of the theorem, Q is this minimal forward residual. Failing the test on an unminimized presentation would not rule out a better summary.

2. The counting theorem

For a state r and operation a, define Pred_a(r)={q:delta(q,a)=r}.

Theorem. A finite realization with this contract exists if and only if there are positive integers m(q), one for each forward residual state, satisfying

$$\sum_{q\in\operatorname{Pred}_a(r)}m(q)\leq m(r) \quad\text{for every }r,a. \tag{1}$$

Equivalently, there must be no pair of distinct states p,q and operation a with

$$\delta(p,a)=\delta(q,a)=r \quad\text{and a path from }r\text{ back to }q. \tag{2}$$

This is the classical forbidden merge pattern. A path of length zero is allowed in (2).

When (2) is absent, the optimum total number of realized summary states is computable. Partition the transition graph into strongly connected components (SCCs), and process them in topological order. Set

$$c(C)=\max\left(1,\;\max_{r\in C,\ a\in A} \sum_{\substack{q\notin C\\\delta(q,a)=r}}c(C_q)\right), \qquad c(q)=c(C_q). \tag{3}$$

Then

$$N_{\min}=\sum_{q\in Q}c(q). \tag{4}$$

The minimum vector of fiber sizes is unique. The transition tables attaining it need not be unique. These are state counts, not counts of stored graph nodes and not lower bounds on the size of every recognizer for the same language.

Proof: why memory must satisfy the inequalities

Equal summary states have equal outputs and equal future push domains. Induction on a forward word shows that they belong to the same forward residual. Hence every realization has a surjection pi:S -> Q.

Let S_q=pi^{-1}(q) and m(q)=|S_q|. If delta(q,a)=r, every state in S_q has an a update into S_r. The inverse table makes U_a injective over its entire domain: if two updates agree, applying D_a recovers the same predecessor summary. The images for distinct predecessors of r must therefore be disjoint. Counting gives (1).

An edge q -> r implies m(q)<=m(r). Along paths in both directions, fiber sizes in an SCC must be equal. If (2) occurs, q,r have equal fiber sizes, but (1) requires m(r)>=m(q)+m(p), impossible because m(p)>=1.

Proof: why the absence of the pattern is sufficient

Without (2), whenever an a edge into r comes from its own SCC, it is the only a edge into r. Its constraint is therefore just equality of the two component sizes. All other incoming edges come from earlier SCCs. Formula (3) is exactly the smallest capacity that accommodates those edges. Induction over the component order proves that c is feasible and componentwise no larger than any positive feasible vector.

Make c(q) copies of every state q. For each target r and letter a, order its predecessors. Assign each predecessor’s copies a disjoint block of copies of r; inequality (1) provides room. The update preserves the index within that block. This defines a partial-injective U_a; its inverse defines D_a on its image. Label each copy of q by o(q).

Start at any copy of q0 and retain the states reachable by legal pushes. They still cover every state of M, since M is accessible. Their fiber sizes satisfy (1), so they cannot be smaller than c. Consequently every allocated copy is reachable. There is only one copy of the initial SCC, including q0: it has no incoming edges from other accessible components.

Define sigma(w) by following the lifted push path for w. Each legal pop restores its predecessor by injectivity. Induction on any interleaving of pushes and pops proves the restoration equations and all observations. The lower bound already proved gives (4).

3. Examples that separate the cases

One merge costs one extra state

Use states s,p,q,r, outputs start,0,1,2, and edges s -0-> p, s -1-> q, p -a-> r, q -a-> r. Every SCC is a singleton. Formula (3) gives fiber sizes 1,1,1,2. Five summary states are necessary and sufficient, even though the forward behavior has four.

A repeatable region can retain finite memory

Add a b self-loop at r. The merge uses a, while the loop uses b, so the forbidden pattern is absent. Two copies of r suffice for arbitrarily many legal b operations, and legal pops restore them. Changing the loop to a creates (2), making finite restoration impossible. It is the operation-specific merge and return path that matter.

A regular protocol can require unbounded restoration memory

Take K=a*b* and a constant output. There are two forward residual states: before the first b, and after it. The latter has both the incoming first b and a b self-loop. The capacity constraint reads m(after)>=m(before)+m(after), so no finite summary works.

This obstruction ranges over every finite summary satisfying the stated protocol, not just the displayed two-state machine. It does not make a*b* hard to recognize, and does not prohibit an immutable undo stack.

The finite overhead can be exponential

For n>=1, permit binary histories of length at most n, observing their last bit, with a distinct output at epsilon. The forward residual has 2n+1 states: epsilon and the two possible last bits at each positive depth. Different depths have different remaining push domains.

There are no cycles. At depth d>=1, each last-bit state needs 2^{d-1} copies. Hence the exact optimum is

$$N_{\min}=1+2\sum_{d=1}^{n}2^{d-1}=2^{n+1}-1.$$

All current words of a given length must stay distinct: remove their common suffix by the same legal typed pops until their different last bits become observable. Different lengths were already separated by push legality. This gives a second, direct proof of the bound. The overhead is exponential in behavioral states, but only linear in n when measured in memory bits.

4. Two observation contracts must remain separate

The preceding partial-restoration note correctly proves a finite-index theorem when reverse enabledness is observable, but its claimed specialization to the earlier hidden-stack group theorem was too broad. On the actual word carrier A*, a push is total but is not surjective: epsilon has no predecessor. Its inverse pop has a proper domain.

Indeed, for any prefix-closed history language K, if all typed pop domains are observable then every two distinct histories are distinguishable. Pop their longest common suffix. Either one reaches epsilon first, or their remaining top types differ. One further pop is legal from only one history. Thus the symmetric residual is equality on K, even with constant output. An exact finite realization in that stronger contract exists exactly when K is finite. For a finite automaton for K, this is decidable by checking for a reachable directed cycle.

By contrast, parity on A* has a two-state summary under a legal-pop promise. This does not detect underflow. The group theorem applies to that weaker contract. Total generators in a finite realized quotient are permutations; that fact does not make reverse legality in the concrete word tree observable.

All these contexts are contexts over the specified push/pop interface. They are not arbitrary contexts allowed to inspect every port of a scaffold.

5. What the metric statement does and does not say

On the symmetric residual quotient, the discrete zero-or-one distance is preserved by each partial bijection. This records cancellation. It does not measure how soon a difference becomes observable.

For a horizon-sensitive version, let k(x,y) be the least length of a two-way experiment distinguishing output or definedness, and put d_H(x,y)=2^{-k(x,y)}, or zero when no experiment distinguishes them. This is a pseudoultrametric: agreement through each horizon is an equivalence relation, and the horizons are nested.

When a reversible operation P is defined at both configurations, prefixing an experiment by P or its inverse proves

$$\tfrac12 d_H(x,y)\le d_H(Px,Py)\le 2d_H(x,y).$$

The fork example has distance one between differently observed predecessors, and distance one-half between their equally observed successors. Thus the horizon metric need not be an isometry. The discrete and horizon claims are different, and neither alone bounds the cost of storing a representation.

6. Resources, persistence, and the next boundary

For fixed M passing the test, the constructed machine uses N_min finite states, hence ceil(log2 N_min) bits under binary encoding, one fixed table transition per operation, and zero dynamically allocated records. The explicit transition table has at most |A| N_min push entries and as many inverse entries. The machine depends on the protocol, not on history length. These are finite-control resources; a succinct arithmetic description does not by itself give uniform constant-time arithmetic as the protocol grows.

Every finite controller also has a simple persistent alternative, even when the finite-summary test fails: on each push, allocate one immutable record holding the old controller state and the previous root. On pop, read the old state from the root record and follow its predecessor pointer. This uses bounded local access and at most one logical allocation per operation. Adding the pushed type supports exact pop-legality checks as well. This familiar persistent-stack construction explains why the theorem limits erasure of history, not bounded persistent realization in general.

A whole-machine scaffold consequence still requires the other components to satisfy the existing simultaneous-record compiler’s contract, including fixed virtual initialization and strict timing. Language transfer is unchanged: the scaffold recognizes the same words as its source, and the PEG recognizes their reversal. This note makes no claim about an optimum scaffold degree, stored-graph equivalence, or unrestricted PEG pumping.

The next substantive question is how much predecessor structure can be eliminated in a controller that already has a retained stack. A useful result must use that unbounded visible structure, rather than reprove finite reversible-automata minimization. The immediate test is whether a checked finite restoration summary for each visible boundary type can be synthesized, instead of merely supplied, while preserving the prior local erasure contract.

7. Evidence and source-to-claim map

The checker minimizes partial Moore machines, finds cycle/merge witnesses, calculates capacities, constructs the lift and its inverse tables, and checks reachability and all local equations. For the bounded binary family it also enumerates every legal word and checks the restoration edges. Its recorded output states the exact finite scope. No proof-assistant or infinite pushdown synthesis verification is claimed.

The literature comparison identifies the finite-controller bottleneck as settled:

• Holzer, Jakobi and Kutrib, Minimal reversible deterministic finite automata (DLT 2015), is the source credited for the single-initial-state forbidden pattern and minimal construction by Lavado, Pighizzini and Prigioniero. The latter’s primary paper, Theorem 1 and Lemmas 2-3, also establishes componentwise copy minimality and equality of copy counts inside SCCs.
• Lavado and Prigioniero, Concise Representations of Reversible Automata (2019), Algorithm 2 and Theorem 9, gives the same component recurrence and an interval-index construction of a minimum-size reversible automaton. These match (3) and the construction above.

Accordingly, FPRD’s work here is an explicit adaptation to finite observations, push-domain preservation and promised typed restoration, with a self-contained counting proof and executable construction. The exponential phenomenon is also established; the binary-history family is an explanatory instance. No originality claim is made for the automata theorem or algorithm.

The important research outcome is that the previous open question is resolved for regular-history controllers, and the next boundary is now clearly in the interaction with retained persistent structure.