Head removal with typed word-cache views

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. Why word equations need a structural companion

The preceding cache criterion preserved equations among decoded words, but left all old roots opaque. A pop operation needs more: a root whose head and tail can be exposed, with the tail still supporting the next pop. This note supplies a decidable bounded-template criterion for a specific class: proper lists with correlated rope caches. It does not infer a good representation for arbitrary sequences, or recognize every valid list/rope implementation. The contract is given independently of a controller.

There are two sorts. L is the proper-list sort with constructors E:L and Cons_c:L->L for each c in a fixed finite alphabet Sigma. R is the rope sort; every L root can be used as R, and Cat:R x R->R constructs a concatenation. A Cat record is never an L record, even if its decoded word happens to equal that of a list. Records are finite, immutable and acyclic. Semantics are epsilon for E, c followed by the child’s word for Cons_c, and concatenation for Cat. The alphabet contains distinct letters a,b.

Fix d base roots of sort L and finitely many cache roots of sort R. Each cache has a declared word expression Cj(Z1,…,Zd), using concatenation and fixed letters, in the words of the base lists. All base-word tuples are admitted, including empty words. Aliasing is allowed but is not an observable or a guard. A root declared R cannot be cast to L on the basis of its word alone. Available constants are E and the singleton lists Cons_c(E), built once in a fixed finite initialization.

A valid state has both proper-list base roots and the declared cache word equations. Initial validity must be established; it is not assumed for an arbitrary external graph. Calls may also start from retained valid tuples. Old records are never modified. The example below initializes all roots at E.

2. A finite family of views with explicit residual parameters

At the start of a call inspect each base root’s outer tag. The view is a tuple with entries empty or c in Sigma. For an empty base set Zi=epsilon. For a c branch expose its one tail pointer Ti:L and substitute Zi=c Ti. The Ti are new symbolic word parameters for the proof, not newly allocated records. Inside each branch their values range independently over all finite words. No tag inside a Ti is inspected. All original base and cache roots, the exposed Ti, and the fixed constants are available to construction.

Thus there are (1+|Sigma|)^d branches. The observer needs at most one old pointer edge from each named base root and reads only the base tags. It uses no pointer-identity tests, inverse edges or numerical addresses. This is an explicit restricted observation interface; a machine allowed to inspect deeper labels or additional roots has a different synthesis problem. A native bounded labelled view can supply these observations without alias tests; extra information can be ignored.

For each operation name and branch, prescribe output words F for all base and cache registers as formal expressions in that branch’s Ti and letters. A finite reply, such as the removed head, is specified per branch. On empty pop the example returns an empty status and preserves the tuple.

Allowed templates allocate at most K fresh records, choosing Cons_c on an L child or Cat on R children. Old and fresh L roots are usable as R. Output base registers must have type L; caches need only R. Register reassignment does not itself allocate a record. Every allocated record counts, including unused intermediate work. Type checking uses the declared sorts and branch facts, not inaccessible runtime information.

3. Exact synthesis for this typed template language

Theorem. Given the finite cache declaration, branch specifications and K, it is decidable whether typed <=K templates implement every branch and preserve valid states. The decision procedure is complete for this template language on all admitted states. Successful templates give a bounded local implementation correct for every finite sequence from a valid initialization.

Proof. Fix an operation and branch. List all well-typed acyclic templates of at most K records and all correctly sorted choices of output roots. The list is finite: each new constructor has fixed arity and its children come from finitely many old or earlier fresh pointers.

Normalize old base words by Zi=epsilon or c Ti, and cache words by the same substitution in Cj. The exposed tail root has formal word Ti. Normalize fresh Cons as prefixing its letter and Cat as concatenation. This produces a finite set of tuples of formal words in the independent Ti.

Apply the finite-separation lemma from the uniform-selection note to all these words and the target coordinates simultaneously. If every branch input has some correct well-typed <=K template, a witness at the separating input must have normalized output exactly F. It is therefore a uniform template for that branch. Conversely a matching template is a pointwise witness. The separating words are realizable by proper lists for every Ti, so the structural constraint does not remove the witness.

Check also, for each cache coordinate j,

F_cache,j = Cj(F_base,1,...,F_base,d)

as formal words in the Ti. Finite separation makes this necessary and sufficient for the declared word invariant on the whole branch. Output sort checking makes the base roots proper lists. The two checks together put the result back in the valid-state class. Apply them to every finite branch and operation. Induction from the fixed valid initialization proves all finite histories, including branching calls from retained valid versions. QED.

No semantic equality oracle is used at runtime. Normalization and search happen when constructing the finite rule table. Bounds are K fresh records, maximum constructor arity two, at most one old-pointer edge from a named base, and a fixed finite amount of register work. The result is a characterization of this declared typed template language, not of every radius-one pointer program or every representation of the same words. In particular it does not permit a pointwise witness to use an R root as L just because that particular heap has a helpful hidden shape.

The theorem handles a genuine change of parameters: after a nonempty pop, the exposed Ti becomes a base word. It need not expose Ti’s next head in the same call. The proper-list invariant guarantees that the next call has one of the same finite views, however long the list is.

4. Persistent stacks with prefix caches

Fix d>=1. Base roots X1,…,Xd are proper lists. Store rope roots P2,…,Pd with Pj=X1…Xj; abbreviate P1=X1. Initialize every root to E. Allow push(i,c), pop(i), and prefix-handle queries. These are a fixed finite operation alphabet for each fixed d and Sigma. A query returns a root; it does not print the entire decoded word at unit cost.

For push(i,c), form Xi’=Cons_c(Xi). If i=1 set P1’=Xi’ and rebuild each Pj’=Cat(P(j-1)‘,Xj) for j=2,…,d. This allocates d records. If i>1 form Pi’=Cat(P(i-1),Xi’), then rebuild later prefixes in the same way. This allocates d-i+2 records. Retain all other base and earlier prefix roots.

For nonempty pop(i), the observed tag supplies c and its tail pointer T. Set Xi’=T. If i=1, rebuild Pj’=Cat(P(j-1)‘,Xj) for j=2,…,d, starting with P1’=T. This uses d-1 records. If i>1, form Pi’=Cat(P(i-1),T) and rebuild j>i, using d-i+1 records. Empty pop and prefix queries allocate zero. All source Xj for j!=i refer to the original tuple.

Preservation proof. Push makes the selected factor c Xi; pop makes it T where the old factor was c T. In either case the first affected prefix is the unchanged prefix before i followed by the new factor. Each later Cat appends the next unchanged factor. Earlier prefixes remain correct. Cons and the exposed tail retain sort L; Cat caches have sort R. The empty case changes nothing. This proves both word and shape obligations on every branch, so the theorem applies to every finite history and every retained valid version. No recursive rebuilding depends on factor length: the chain of cache repairs has at most d-1 steps, with d fixed.

These are construction bounds, not claims of optimality for the richer head/tail observation interface. The previous opaque-root optimum should not be silently transferred: this call can use exposed tails that were unavailable there. For d=1 this reduces to the familiar persistent stack; for d>1 the additional obligation is maintaining the correlated caches.

5. A word-correct join can destroy future head access

A useful negative control starts with two proper lists X,Y and a rope cache P with word XY. Consider replacing the first base by the concatenation XY and leaving the second at Y. A word-only template can return old P as the new first base and set the new product cache to Cat(P,Y), using one fresh record. Every requested word equation holds. If P is a Cat root, the new base is not a proper list, so the next head/tail call has no legal list view. The typed test rejects this otherwise word-correct update.

This is not merely a conservative type-check failure. In this representation, proper-list catenation has an unbounded allocation requirement on a concrete family. Take X=a^n and Y=b as ordinary Cons lists, and P=Cat(X,Y), from the same fixed E and singleton constants. There are no additional b-ending lists beyond the singleton b; all old suffixes of X end in a. Even granting access to every old node, a proper-list result for a^n b must allocate at least n fresh Cons records.

Proof. The returned proper list is a chain of fresh Cons records followed by an old proper-list suffix, or by E. An old nonempty suffix ending in a cannot occur, since the output ends in b. The longest usable old b-ending proper-list suffix is b itself. Therefore at least n new letters must be prepended in fresh Cons records. Cat nodes cannot occur in a proper list. Allocating n Cons records in reverse construction order attains this bound for the supplied input family. QED.

Allowing a rope as the output makes concatenation cheap, but requires a separate mechanism for maintaining head/tail views. This is precisely the structural obligation missed by word equations alone. The lower bound does not apply to all catenable sequences, to all persistent representations, or to all scaffold languages. Prepared list suffixes could also change the supplied-heap bound.

6. Status and next boundary

Persistent Cons lists, sharing tails, and the need to copy a left list for ordinary immutable-list concatenation are established ingredients. See Chris Okasaki, Purely Functional Data Structures (1996 thesis, persistence and list discussion). We do not claim a new stack or catenable-list algorithm. The prior Alur-Cerny register comparison and Filiot-Jecker-Loding-Winter uniformization comparison remain relevant; their stronger language/transducer theorems are not imported into this typed model.

The additional argument is finite synthesis with branchwise independent tails, simultaneous cache equations, and a structural condition ensuring that the next operation still has a legal view. The completeness claim is only for the explicit typed templates. Novelty remains unestablished. The proofs are written, unbounded arguments. The accompanying checker tests small typed templates, rejects the ill-sorted word-only join, and checks finite mixed push/pop histories with old versions retained. It is not a proof assistant or a verification of all bounded pointer programs.

The working hypothesis has advanced from opaque concatenation to a class with actual head removal and a preserved structural invariant. Its next hard boundary is a bounded family of views for general concatenation roots: can one regain head/tail access without requiring a proper Cons list and without hiding unbounded normalization? A concrete next candidate is a fixed number of proper-list segments with a bounded descriptor. Test its closure under concatenation and pop before claiming a general theorem. An unbounded segment count or a required unbounded traversal is a failure, not a bounded primitive.

Observations here are the chosen head tags, exposed pointers and decoded word contracts. No physical-alias guard or arbitrary future scaffold-context equivalence is assumed. The existing bounded-record compiler can use the finite equality-free plans with its full virtual-initialization contract; its representation overhead is separate from these record counts. Any scaffold-to-PEG language transfer still reverses the recognized language.