Reading an answer and constructing its residual

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.

The certificate method has proved useful for verifying supplied persistent constructions. Its soundness is an application of simulation, invariants and finite resource accounting. The deque example does not yet turn it into an intrinsic characterization or a method for finding representations. This note isolates a further requirement by comparing it with a simpler word representation: making today’s answer local does not necessarily make the state needed for tomorrow cheap to construct.

1. Model and independent obligations

Fix the alphabet {a,b}. A positive binary rope is a finite immutable acyclic graph with constructors E, A, B and Cat(x,y), interpreted respectively as the empty word, a, b and the concatenation of the two child words. Sharing is allowed. There are no substring, deletion, cancellation, compressed-run or evaluator constructors. Returning a residual means returning one root in this same representation with its ordinary word interpretation.

Records may additionally carry any tags from a fixed finite set. These tags are ignored by the word interpretation and add no child pointers. This allows cached first-letter information. Old records cannot be changed. An update may return an old root or allocate a finite acyclic batch of fresh E/A/B/Cat records, with arbitrary sharing among the fresh and old records. Every allocated record counts, including discarded work.

In the intended bounded model the controller has finite control, finitely many roots, bounded access radius r and allocation budget K per call. The lower bound below is stronger within this representation: it permits unlimited old-graph access and arbitrary knowledge when choosing the fresh batch. Thus no issue about finding the right branch can explain it away. Initialization is a fixed finite graph, independent of the later parameter n.

There are two separate requirements for pop:

1. determine the first letter;
2. construct a root denoting the remaining word.

An earlier note ruled out the first requirement at bounded radius on bare ropes. Caching a first-letter tag repairs that obstruction. The following argument addresses the second requirement even after that repair.

2. A general allocation bound for positive binary ropes

Call a word a-free if it contains no a. For any finite pre-call heap H, put

$$M(H)=\max\bigl(\{1\}\cup \{|\alpha(v)|:v\in H,\ \alpha(v)\text{ is a-free}\}\bigr).$$

This is a mathematical measure of the supplied heap, not a counter that the runtime must compute. It can be calculated independently on any finite input by interpreting its acyclic graph.

Proposition. If a persistent update allocates at most K fresh records and returns an a-free rope with word w, then

$$|w|\leq M(H)2^K.$$

Proof. Positivity is crucial. Every descendant of a returned rope contributes its entire word, possibly repeatedly through sharing, to the root word. Therefore every old node reachable from an a-free result is itself a-free, and has word length at most M(H).

Topologically order the fresh records reachable from the returned root, children before parents. There are at most K. Before any such record is added, all usable old values have length at most M(H). A fresh leaf has length at most one. A fresh Cat sums two already available lengths and therefore at most doubles their previous maximum. Induction on the number of fresh records gives M(H)2^i after i records. An old result already satisfies the i=0 bound. This proves the claim. Shared children are included: Cat(x,x) can double the word length using one record, but cannot exceed the same bound. No access restriction was used. QED.

Consequently any such output of positive length N needs

$$K\geq\max\{0,\lceil\log_2(N/M(H))\rceil\}.$$

This is a necessary condition in the specified positive binary constructor model. It is not sufficient: the lengths available in the old heap need not combine to the exact requested length within K records, and the construction must also be selected using the permitted observations. No optimality claim is made for arbitrary N or H.

3. A family with a local head and an expensive tail

Initialize E, A and B. Let

$$T_0=A,\qquad T_{n+1}=\operatorname{Cat}(T_n,B).$$

The pre-call heap H_n consists of these initial records and T_1,…,T_n. Its current word is ab^n. Every T_i contains a; the only a-free words in the heap are the empty word and b. Hence M(H_n)=1.

Attach the cached tag a to every T_i. More generally, first-letter tags from {empty,a,b} can be maintained for every Cat by taking its left child’s tag unless that tag is empty, in which case take its right child’s tag. This finite rule makes the first-letter query local. In this particular history each append needs only one new Cat and preserves all earlier roots.

Corollary. Any pop operation returning a same-format rope for the tail of T_n needs at least ceil(log2 n) fresh records, for n>=1. No fixed allocation budget handles every n, even with the head cached, unlimited access and permission to rearrange and share output nodes arbitrarily.

Proof. The tail is b^n and is a-free. Apply Section 2 with M(H_n)=1. For a proposed fixed budget K, choose n>2^K. QED.

The quantifier is over all update procedures for these supplied heaps and this output representation. It is not over all representations of words. The input family is generated by the specified append-only rule; a different constructor that also maintains suffix structures is outside that family. Finite metadata tags cannot change the proof because they do not change word interpretation or supply additional reusable subgraphs.

A fixed finite initialization with additional a-free constants changes the bound to M0*2^K for a fixed M0, and cannot remove the unbounded requirement. Initializing a different b^n record for each n would violate fixed initialization. Maintaining such a record during earlier operations is instead a legitimate change of representation and history, discussed next.

4. Positive controls and failed stronger claims

For n=2^k, k fresh Cat records suffice to represent the tail: start at B and repeatedly replace x by Cat(x,x). Thus the lower bound is attained on these lengths when selecting the construction is unrestricted. The naive argument that every old ancestor must be copied would incorrectly claim a linear lower bound. A persistent output need not retain the old shape.

If H also contains a root for b^n, returning that root uses no new records. Then M(H)>=n and the bound allows K=0. Earlier computation can therefore remove the obstruction by preparing a usable residual structure. A linked list representation similarly exposes its tail by an existing pointer. These examples explain why the result cannot exclude bounded pop for all word representations or persistent deque implementations.

A deferred Drop(x) constructor would also defeat the present output-size argument by interpreting a whole old word and deleting its head. It is excluded here because the interpretation is no longer positive concatenation. Adding it requires a separate proof that future observations and updates can be served with bounded work; simply naming the deferred operation does not provide that proof.

The obstruction therefore separates three questions: whether an answer is locally observable, whether its residual can be constructed from reusable pieces with bounded allocation, and whether subsequent operations preserve both capabilities. Our certificates check these obligations for a supplied construction; they do not infer a representation satisfying them.

5. Comparison, verification and research consequence

Boehm, Atkinson and Plass’s Ropes: an Alternative to Strings discusses immutable path copying, eager substring work along boundary paths, and deferred substring nodes (pp. 1317-1319). Those mechanisms are established. Our restricted family permits output reshaping and DAG sharing, so its allocation argument is not merely a cost analysis of the path-copying algorithm. The exponential bound itself is elementary DAG growth; novelty of this exact application has not been established.

The earlier local-certificate theorem uses standard simulation/invariant reasoning, as its comparisons with proof-carrying code, translation validation and resource certification already explain. The strict FIFO construction also illustrates a different way to keep future work ready: distribute rebuilding across prior operations and retain explicit progress structure. Its imported scheduling invariant still carries real content; the generic certificate theorem alone does not discover it.

The proposition and corollary have written proofs for all finite H and all n, respectively. No proof assistant has checked them. The accompanying finite DAG-growth check enumerates small addition DAGs and checks the doubling witnesses; its output is corroboration, not a proof of the unrestricted theorem or a lower bound for arbitrary encodings.

The completed certificate study yields a useful sufficient verification method and concrete conditional applications. It has not yielded a novel general characterization. Continuing to list deque helper identities would not settle that gap. The next mathematical question is narrower: for a specified constructor invariant and fixed budgets, when can each required residual be assembled from locally available old pieces by one uniform finite choice of construction rules? Existence of a construction for each input must be separated from selection by the same bounded observation.

All observations here are decoded words and operations on this rope interface. There is no claim about equivalence under arbitrary future scaffold contexts, language-class separation, or generalized pumping. The positive scaffold compiler and its fixed virtual initialization are unaffected; any scaffold-to-PEG language transfer still reverses the word.