Correlated word caches that remain valid after updates

Working research note, 30 September 2026.

Understand when future computational behavior admits a representation maintained by finite rules with bounded local access and bounded allocation, and what structural obstructions prevent such a representation.

1. A class of correlations specified independently of a controller

Fix a finite alphabet Sigma with at least two letters, d base roots, and m>=d available word roots. A finite list of formal concatenation expressions C1,…,Cm over Sigma and parameters Z1,…,Zd specifies the interface. Require Ci=Zi for i<=d. A valid root tuple R1,…,Rm satisfies

word(Rj) = Cj(z1,...,zd)

for some tuple of arbitrary finite words z1,…,zd. Thus the base roots supply the parameters and the remaining roots cache declared expressions. All parameter tuples are admitted; additional restrictions are not implicit. For example (Z1,Z2,Z1Z2) specifies two factors and their concatenation. Acyclic definitions of caches in terms of earlier caches can be expanded to this form. Arbitrary cyclic word equations are outside this class.

The heap is an immutable finite acyclic positive rope: E, letter records, and Cat records with two child pointers, interpreted as concatenation. The available old pointers are the m named roots and fixed E/letter constants. Their subgraphs are opaque: no descent, semantic equality test, length query, address arithmetic or search through old versions is allowed. Physical sharing is permitted but does not supply extra observable data or extra named roots. Updating the fixed tuple of root registers is free of record allocation; every fresh Cat, including discarded temporary work, counts toward K. The input operation name selects a rule from a fixed finite table.

This is a specified root interface and resource model, not all representations of the same abstract words. The interface exposes correlations in its contract rather than asking the runtime to discover or verify them by traversing words. A caller must establish the invariant initially. Initialization uses one fixed finite graph, independent of the operation history; its size is not charged to an arbitrary later operation. The example below starts entirely at E.

2. Normalization and simultaneous construction

For an operation, prescribe output words F1,…,Fm, each a formal expression in the base parameters and constants. A construction template may create at most K Cat records and choose m output roots, sharing both old and new records across different outputs. There are finitely many such templates. Expand each old register Rj to Cj in the unfolded output expressions. Call the resulting tuple the template’s normalized output.

Theorem 1. For the specified interface, the following are equivalent:

1. For every admitted parameter tuple there exists a construction template of at most K fresh records producing all prescribed Fj simultaneously.
2. A template of at most K fresh records has normalized output exactly F as a tuple of formal words.
3. One uniform template of at most K fresh records produces F on every admitted tuple, with no descent into old roots.

Proof. Enumerate all bounded templates and normalize their output tuples. This gives a finite collection of formal words, including every target Fj. The finite-separation lemma in the preceding note supplies one assignment to the Zi that distinguishes every unequal word in this collection. Apply (1) at that assignment. The successful template has each normalized coordinate formally equal to the corresponding Fj. Hence (2), which implies (3) by substitution. Statement (3) implies (1). QED.

The test is finite and independent of a proposed controller: normalize each enumerated template and compare its output tuple with the specification. K bounds the joint construction, not a separate budget for each coordinate. Shared intermediate results are included. A symbolic length bound for the finite-separation argument is 2^K times max(1,max_j |Cj|), enlarged to include the lengths of the Fj. Formal lengths count parameter symbols once.

This theorem extends the previous independent-root case by retaining caches as usable old roots. Expanding a cache for the proof does not mean rebuilding it at runtime. For example, with C=(Z1,Z2,Z1Z2), returning the cached product costs zero; ignoring that third root would cost one Cat.

3. An effective preservation test and iteration theorem

The first d target coordinates specify the new base words. The same interface invariant holds after the update exactly when the following formal identities hold for every j>d:

Fj = Cj(F1,...,Fd).

Theorem 2. Given a finite family of such operation specifications and a fixed K, finite template search plus these formal identity checks decides whether there are uniform <=K templates implementing every specified operation and preserving this interface on all admitted states. If they exist and initialization satisfies the invariant, their execution is correct for every finite operation sequence, and each call preserves all old graphs.

Proof. The identity test is sufficient by substitution. It is necessary for preservation on all admitted parameter tuples by finite separation applied to its two sides. Theorem 1 decides the simultaneous implementation of each operation. There are finitely many operations, so choose a successful template for each. Induct on the operation sequence: the initial tuple is valid; the chosen template gives the prescribed next words and the identities put them back in the invariant class. Immutability preserves old records at every step. The same argument allows a call to start from any retained valid tuple. QED.

The updated base words need not range independently over every word tuple as a function of the previous tuple. They only need to be one admissible tuple at the next call. For instance (Z1,Z2) -> (Z1Z2,Z1) creates additional correlations along that history, but remains inside the class admitting all base tuples. Confusing surjectivity with invariant membership would reject valid updates.

This is a characterization of universal operation contracts in the named interface. It is not necessarily optimal for a controller required to handle only a smaller reachable subset. Resources are <=K fresh binary records, zero pointer descent and a fixed number of register assignments depending on the finite templates. No semantic equality oracle or unbounded runtime normalization is used. The finite synthesis procedure need not be efficient.

A negative control: on C=(Z1,Z2,Z1Z2), specifying F=(Z1a,Z2,Z1Z2) cheaply updates the base factor but leaves its product cache stale. The preservation check compares Z1Z2 with Z1aZ2 and rejects it. Correct word production for isolated coordinates is not enough.

4. An allocation lower bound from distinct required roots

Let Old be the set of formal words C1,…,Cm, E and the letter constants. Let New be the set of distinct target words Fj that do not belong to Old.

Proposition. Every implementation correct on all admitted tuples has worst-case allocation at least |New| in this interface.

Proof. Use finite separation on Old union {Fj}. On the resulting input, each member of New denotes a word different from all available old roots and from every other member of New. Each therefore requires its own fresh root record. One record has only one decoded word, so sharing cannot merge these distinct roots. At least |New| fresh records are necessary. QED.

This is a necessary bound, not generally sufficient: intermediate records can also be needed. The proof depends on the specified available-root set. An implementation with additional prepared roots or a different representation has a different problem. It is stronger than counting changed register names, because multiple registers with the same target word can share one root.

5. Persistent prefix caches: exact update cost

Fix d>=1. Store the d base factors X1,…,Xd and the d-1 prefix roots P2,…,Pd, with Pi=X1…Xi. Write P1=X1 as an abbreviation, not an extra required register. There are 2d-1 word registers, plus the fixed constants. This is the interface of Section 1. Initialize every word register to E.

The finite operation alphabet contains append(i,c), for 1<=i<=d and c in Sigma. It replaces Xi by Xi c and updates all prefixes. A prefix query j returns Pj as a handle with zero new records. It does not print or traverse the entire word in constant time. Factor lengths and the number of calls are unbounded; d is fixed for each machine.

Theorem 3. The exact worst-case number of fresh Cat records needed for append(i,c), in this available-root interface, is

d                     if i=1,
d-i+2                 if 2<=i<=d.

Construction. If i=1, create X1’=Cat(X1,c), then for j=2,…,d create Pj’=Cat(P(j-1)‘,Xj). This uses d records. If i>1, create Xi’=Cat(Xi,c) and Pi’=Cat(Pi,c). For j>i, create Pj’=Cat(P(j-1)’,Xj). Keep other factors and earlier prefixes unchanged. This uses 2+(d-i) records. All right-hand-side old factors refer to the pre-call tuple. The current intermediate prefixes are fresh roots.

Preservation. The new Pi is X1…Xi c. Each successive construction appends the next unchanged factor. Earlier prefixes do not include Xi and remain correct. Thus every prefix equation holds after every call. Starting at E and applying induction gives the invariant for arbitrary histories, including calls applied to retained valid versions. Old records are never modified.

Lower bound. If i=1 there are d distinct changed formal outputs: the new X1 and all Pj for j>=2. If i>1 there are d-i+2: the new Xi and all Pj for j>=i. None is an old formal word, because each contains the inserted literal c and the old factors/prefixes contain only parameter symbols. These changed outputs are pairwise distinct as formal words. Apply the proposition. This proves exact worst-case cost. Some particular inputs, especially empty factors, can use fewer records. QED.

Every tuple of factor words is reachable from E by appending its letters factor by factor. Thus the lower-bound witness also occurs in this example’s reachable word states. The claim still restricts usable old pointers to the named roots and constants; it does not grant access to arbitrary accumulated internal nodes or historical tuples during a call.

For d=3, appending to factor 1 or 2 costs three records in the worst case; appending to factor 3 costs two. If only the factors are retained, each append costs one, but a prefix query then has to construct its requested concatenation. This states the actual tradeoff: keeping every prefix already represented makes queries cheap and creates an unavoidable update obligation. It is not a lower bound against every data structure for prefix queries.

6. Established ingredients, verification, and remaining question

Alur and Cerny’s Expressiveness of streaming string transducers (FSTTCS 2010, introduction and model) already studies finite string registers updated simultaneously by concatenation. Its no-copy condition forbids using one old variable multiple times across the right-hand sides. Our immutable DAGs permit sharing and charge fresh binary records, so that paper’s regular- transduction characterization is not imported into this resource model. Word substitution, loop invariants and finite straight-line construction search are established ingredients. The previous uniformization comparison also remains applicable. No novelty claim follows from this source check.

The additional argument here is an exact bounded-allocation criterion with explicit cached correlations, a decidable preservation test, and the matching prefix-cache upper/lower bound. These are written proofs, not proof-assistant certificates. The accompanying finite checker tests normalized template costs on a small correlated example and simulates bounded prefix histories while checking stored old versions. Finite histories do not prove arbitrary iteration.

The working hypothesis now has a proved case: correlations given by explicit concatenation expressions admit a uniform construction and preservation criterion. It does not yet handle destructive observations such as finding and removing the first letter of an opaque factor. A decisive extension is a finite set of structural views exposing a head and tail, with view transitions that preserve the relations among cached words. Determine whether this can be specified independently and checked completely for a natural subclass, or whether a concrete view transition destroys the property. Mere extra concatenation examples will not settle that boundary.

Only decoded word contracts are claimed. Physical graph identity and arbitrary future scaffold-context equivalence are not. The bounded-record compiler may be applied only with its full observation and initialization hypotheses; its own representation overhead is not included in the exact Cat bounds. A scaffold recognizing L still transfers to a PEG for reversed L.