FPRD LabShare an approach

Partial restoration: two residuals and the memory between them

Status, 30 September 2026. The main arbitrary-context theorem below has a complete paper proof. Its finite examples have exact executable certificates. The fixed-controller result is an exact reformulation as a reversible congruence/cover problem, not yet an effective characterization for infinite visibly structured sources. Novelty is unestablished.

Contents

1. The distinction that restricted reachability forces

The full hidden-stack cone studied in the preceding note permits every hidden push and every correctly typed inverse pop. That symmetry forced the finite summary updates to be permutations. A real controller often exposes only part of the cone: an operation is enabled only at some boundary configurations, and the controller may never ask every reverse question.

There are then two different meanings of “same future.”

  1. Arbitrary reversible context. Every legal push and pop is a possible future test, including whether the operation is enabled.
  2. One fixed controller. Only the traces admitted by that controller are observed. Two states can have the same forward future even though a later restoration step must remember which predecessor produced them.

The first meaning has a canonical minimal residual. The second may require a finer reversible cover. Confusing them gives a false characterization.

2. Model and quantifiers

Fix a finite set H of operation types and an involutive alphabet

A = {+h,-h : h in H}.

Let X be the carrier of boundary configurations reachable from a specified initial set I. Multiple elements of I allow different input-controlled or nondeterministic entries into the same boundary protocol. For every h, the source supplies a partial injection

P_h : X ⇀ X

and its partial inverse R_h=P_h^{-1}. Thus +h acts by P_h and -h by R_h. No predecessor pointer is added by this definition: the reverse map must already be a well-defined operation of the source model. Let o:X -> Omega be a selected finite observation, or a finite tuple of such observations.

An exact finite arbitrary-context realization consists of:

  • a finite realized carrier S and a surjection sigma:X -> S;
  • a fixed initialized subset sigma(I);
  • a finite output map lambda:S -> Omega;
  • for every h, a partial bijection U_h:S ⇀ S and its inverse;

such that, for every x and every operation, definedness is preserved and reflected, sigma(P_h(x))=U_h(sigma(x)) when defined, and lambda(sigma(x))=o(x). There is no scan, history oracle, saved source version, or allocation in this finite summary channel.

This is stronger than language equivalence. It preserves the selected output, every operation domain, and the resulting summary graph. It still does not claim identity of the source’s stored graph.

3. The two-way future residual

For a word alpha in A*, write alpha(x) for the corresponding partial execution. Define

x ≡± y

iff for every alpha:

  • alpha(x) is defined exactly when alpha(y) is defined; and
  • when both are defined, o(alpha(x))=o(alpha(y)).

Enabledness is deliberately part of this observation contract. If a model submits only correctly typed operations and does not observe failed operations, the quantification must instead be restricted to that common legal protocol.

Theorem 1: symmetric residual characterization

An exact finite arbitrary-context realization exists if and only if ≡± has finite index.

When it exists, X/≡± is the unique minimal realization up to isomorphism. Its number of classes is the optimum state count, not merely a construction bound. Every generator acts as a partial bijection on this quotient, and the transformations generated by the operations form a finite inverse semigroup.

Proof

Residual equivalence is stable under every operation, and the one-letter experiments make each operation domain a union of residual classes. Hence

[x] |-> [P_h(x)]

is a well-defined partial map on the quotient.

It is injective. If [P_h(x)]=[P_h(y)], prepend the inverse test -h to every future experiment. It first returns to x and y, so the successor equivalence implies x ≡± y. The induced -h map is exactly the inverse on the image. Finite index therefore supplies the required realization.

Conversely, the kernel of any exact finite realization refines ≡±: equal summary states have the same defined executions and outputs under every word. Thus the residual has finite index. Every exact realization maps onto the residual quotient, proving minimality and uniqueness of the minimal quotient.

Partial bijections are closed under composition and inversion. Their generated transformation monoid is therefore an inverse semigroup. On a full cone, each operation has total domain and range, so the partial bijections become permutations and this theorem specializes to the preceding finite-group result.

Metric form

Give the residual quotient its discrete metric and pull it back to X:

d(x,y)=0 when x ≡± y, and d(x,y)=1 otherwise.

Every enabled operation is a partial isometry:

d(P_h(x),P_h(y))=d(x,y)

whenever both sides are defined. The forward inequality says equal futures stay equal. The reverse inequality comes from the inverse operation. This is the epsilon-delta-like core: an update that can later be locally undone may neither create nor collapse an observable distinction inside its domain.

4. Why the forward residual alone is not enough

Let ≡+ quantify only over the controller’s forward traces. It is tempting to claim:

A finite locally restorable realization exists iff ≡+ has finite index and every induced push is injective on its residual classes.

The condition is sufficient, but injectivity of the minimal forward residual is not necessary.

Fork-merge counterexample

Take four configurations x0,x1,y0,y1. The only push has

x0 -> y0 and x1 -> y1,

with the inverse pop returning along those two arrows. Give them observations

o(x0)=0, o(x1)=1, and o(y0)=o(y1)=2.

No forward push is enabled at either y state. Therefore the forward residual has three classes:

[x0], [x1], [y0=y1].

Its push merges two distinct source classes, so the three-state quotient is not reversible. Nevertheless the original four-state carrier is already a finite locally reversible realization. The reverse context distinguishes y0 from y1, and the symmetric residual has four classes.

The finite-index plus residual-injectivity proposal is therefore not a characterization for fixed-controller semantics. It mistakes minimal forward behavior for sufficient restoration memory.

5. The corrected fixed-controller object: a reversible cover

For a fixed forward controller, a finite reversible realization is equivalent to a finite-index equivalence E on reachable boundary configurations with all of the following properties:

  1. E refines the forward behavioral residual ≡+;
  2. operation domains are unions of E-classes;
  3. every forward operation respects E; and
  4. for each operation, P_h(x) E P_h(y) implies x E y whenever both pushes are defined.

The quotient X/E is a finite partial-injection automaton and maps onto the forward residual X/≡+. Conversely, the kernel of every finite reversible summary has these four properties. This is an exact characterization, but it quantifies over a finer congruence and so is not yet an effective synthesis theorem for infinite sources.

Call such a quotient a reversible cover of the forward residual. It stores precisely those predecessor distinctions that forward observation was allowed to merge but later restoration still needs. If the forward residual itself is partial-injective, it is already the unique minimal cover. Otherwise covers can require state splitting, and a minimum cover need not be canonical.

This nonuniqueness is not a new phenomenon in finite automata. Pin characterized reversible regular languages, Lombardy gave an effective reversible-automaton construction, and later work shows that minimal reversible recognizers need not be unique and reduced reversible recognizers need not be minimal. The new claim here is narrower: the same cover phenomenon is forced by the difference between forward observation and restoration in the persistent-summary model.

6. Boundary examples

Restricted alternating parity

Use four boundary states q0,q1,b0,b1. Operation A maps qi to bi; operation X maps bi to q(1-i); each inverse reverses its corresponding edge. Every operation is a partial injection. The finite carrier retains the parity needed after a legal return without requiring a full hidden-stack cone.

Restricted rightmost tag

The seven configurations

epsilon, B0, B1, AB0, AB1, C0AB0, C1AB1

with only their displayed construction and inverse edges form a finite partial-bijection system. This explains why the earlier rightmost-tag repair works on its restricted carrier even though a total “overwrite the tag” operation is noninjective. The restriction changes the operation domains; it does not magically make a merge reversible.

Bounded depth

The path epsilon <-> X <-> XX is a partial-bijection system and exactly remembers emptiness. The full unbounded cone is different: exact emptiness has infinitely many symmetric residual classes because arbitrary pops reveal the depth.

Presence and the X/XX witness

For forward observation “has an X occurred?”, pushing X maps both absent and present to present. The two-state residual is noninjective. On the full cone, no finite exact reversible cover can hide unbounded depth while restoring this observation after arbitrary pops. On a controller-bounded carrier, a larger finite cover may still exist. The resource and reachability hypotheses therefore matter.

Control-carried predecessor bit

If the controller itself retains the branch bit distinguishing y0 from y1, then the fork-merge system’s four-state cover is explicit. Declaring only the data summary and omitting control would incorrectly report an obstruction. The carrier for the theorem must include every finite control component that the proposed realization is allowed to use.

7. Checkability and resource consequences

For a finite partial Moore system, include undefinedness in each transition signature and perform ordinary partition refinement over the chosen alphabet. This computes ≡± when both directions are included, or ≡+ for the selected forward controller. Each quotient operation can then be checked for partial injectivity by inspecting its defined arrows.

For infinite deterministic visibly structured sources, the exact arbitrary- context theorem remains semantic until finite-index residuals can be computed. For fixed-controller semantics, the problem is harder still: one must decide whether the forward residual has a finite reversible cover consistent with the source projection. No general decision or size bound is claimed here.

The summary carrier is finite, initialized from I, and allocates no logical record per operation. If a passing source still has a visible stack with the previously proved bounded-spread property, the existing simultaneous-record compiler supplies degree two, native access distance two, fixed virtual initialization, and one physical node per input. This is a construction bound, not an optimum. The scaffold preserves the same-word language. Transfer to a PEG introduces exactly one reversal: a scaffold for L gives a PEG for L^R.

8. Verification scope

The finite checker exactly minimizes six supplied partial Moore systems with undefinedness observable. It verifies:

  • the fork-merge forward residual has three states and a merge;
  • its two-way residual has four states and partial-injective operations;
  • the alternating-parity, restricted-tag, and bounded-depth systems are partial-reversible; and
  • the presence update merges the absent and present residual states.

The recorded output is an exact certificate for those finite instances only. It does not prove Theorem 1, decide an infinite pushdown source, synthesize a smallest cover, or generate a scaffold.

9. Literature boundary and contribution status

Established ingredients and nearby primary sources include:

Myhill-Nerode residual minimality and partial-bijection/inverse-semigroup algebra are imported. The finite-automata literature already warns that minimal deterministic behavior and minimal reversible realizations are different objects, and that reversible minima need not be unique.

The additional mathematical contribution claimed here is limited to the stated persistent-restoration setting: (i) the exact symmetric residual characterization with enabledness and selected observations, (ii) the proof that restricted operation domains replace the full-cone group by an inverse- semigroup action, (iii) the forward-residual counterexample, and (iv) the identification of reversible covers as the memory between forward reuse and later restoration. Publication novelty has not been established.

10. Next question

The next useful problem is not to add more groupoid terminology. It is to make the reversible-cover condition effective for a natural source class:

For deterministic visibly pushdown or regularly presented reachable boundary systems, when does the forward residual admit a finite reversible cover compatible with the source projection, and can the necessary extra restoration states be computed or bounded?

A satisfactory result must include initialization, visible boundary types, finite control that may carry restoration data, operation domains, the exact observation contract, and an explicit resource bound. It must also distinguish one controller’s legal traces from arbitrary future scaffold contexts.