Local construction and uniform context application

Working research note, 1 October 2026.

The question is whether bounded local persistent operations force a finite algebra of future observations. The answer depends on which operations are bounded. Balanced concatenation and one layer of wrapping do not suffice. Uniform application of an arbitrary retained one-hole context does suffice, and gives an exact operational form of an established visibly pushdown theorem.

1. Model, observations and two interfaces

Use immutable finite acyclic records, a fixed finite tag alphabet, fixed pointer arity and root count, and fixed finite pointer-closed initialization. Every operation has finite rules, uniformly bounded old-address/observation radius and fresh allocation. No mutation, address tests, growing scalar, global history index, uncharged scan or suspended computation is allowed. An old pointer copied into an output counts against the radius, even if its target’s tag is not inspected. Radii use endpoint-table observations, not the native scaffold truncation that needs an extra frontier layer.

Valid values are independently composable after address renaming and disjoint union over fixed constants. Operations work on every admitted tuple, including retained versions, shared operands and independent copies. The client already possesses each supplied handle. Word decoding is mathematical; printing a decoded word is not a constant-work operation.

Fix a finite visibly partitioned alphabet. WM consists of words with nonnegative call-minus-return prefix heights and final height zero; bracket kinds need not match. Fix L subset WM. The basic value interface has Empty, internal-letter constants, Join(x,y)=xy, Wrap(c,x,r)=cxr, and exact Query(x). It generates every WM word. The alphabet used in our counterexample has just one call c and one return r, with no internal letters.

The stronger interface also stores every one-hole context C=(u,v) with uv in WM, meaning C[x]=uxv. It has Hole, left/right attachment of a balanced value, bracket wrapping, context composition, and Apply(C,x). All of these, including Apply, obey the same uniform local resource contract. There is one hole, occurring once. These constructors generate all such contexts: parse a balanced word containing a distinguished internal hole symbol and follow the unique path to that symbol. Composition is C composed with D, meaning C[D[x]]. All observations below are exact membership, not raw-heap equivalence.

2. The counterexample to the basic-interface implication

Let n_k=2^(k+1)+k for k>=0, and define

$$L_* = \{c^{n_k}r^{n_k}:k\ge0\}.$$

The first accepted nesting depths are 2,5,10,19,36. There are arbitrarily large gaps. Nevertheless the basic balanced-value interface has a bounded local persistent implementation for L_*.

The clock

Use a strict persistent FIFO over the two payload symbols A and #. Initially its abstract contents are A#. A tick removes its front symbol. If it was A, append A twice; if it was #, append # once. The returned bit is true exactly when the removed symbol was #. Overwrite this bit each tick; it is not sticky. At most three FIFO calls occur, and the queue is never empty before a tick.

Before the first block the queue is A#. Processing a block A^m# transforms it into A^(2m)# and takes m+1 ticks: each old A is removed once and its two successors are appended behind the old marker; the marker is then removed and appended after them. Induction gives block sizes 1,2,4,… . Hence the k-th marker occurs at

$$\sum_{j=0}^{k}(2^j+1)=2^{k+1}+k.$$

This is an unbounded induction, not an inference from the displayed terms. At the end of event k the queue is A⁽²(k+1))#. Even immediately after a dequeue the queue remains nonempty: it has at least two symbols before a tick. All promised dequeue calls are legal.

Value records and rules

Use an Empty record containing the fixed initial clock root and false bit; Wrap records with one word-child pointer; and Cat records with two word-child pointers. Each nonempty record has a finite classification Chain or Other. A Chain Wrap additionally stores its clock root and last-tick bit. Other records have false membership and need no clock. Maximum word-record arity is two. The decoder uses the constructor tag: Empty is epsilon, Wrap(h) is c alpha(h) r, and Cat(h,k) is alpha(h) alpha(k).

• Empty returns the fixed record.
• Join with an Empty operand returns the other supplied handle.
• Join with two nonempty operands allocates Cat(h,k), classified Other.
• Wrap of Empty or Chain reads its clock, performs one tick, and allocates a Chain Wrap record containing the old word root, returned clock and bit.
• Wrap of Other allocates an Other Wrap record pointing to its input.
• Query returns the stored bit, including false for Empty and Other.

Here is the complete semantic invariant. Empty decodes to epsilon with clock Q_0. A Chain decodes to c^n r^n for n>=1, has a valid FIFO representation of the abstract clock Q_n after n ticks, and stores the n-th tick’s output bit. Other decodes to a nonempty WM word not of the form c^n r^n.

Two nonempty balanced words joined together have an internal height-zero boundary. A nonempty c^n r^n has no such boundary, so the Join classification is exact. Also cxr is a chain exactly when x is Empty or a chain. These facts and the FIFO contract prove preservation under every rule. Every WM word has a balanced term construction, so all admitted values are covered. Induction over any finite history, choosing any previously retained valid handles at each call, proves exact decoding, membership and preservation of all old versions. In particular, empty joins and reassociation cannot change a chain’s clock: its clock is determined by nesting depth. No global clock is shared between branches.

Literal resource composition and the FIFO dependency

The FIFO is the prior counter-free strict queue, an adaptation of Hood-Melville with structural tokens replacing integer fields. Its correctness proof projects to the classical queue invariant. It is a written dependency, not newly proof-assistant verified here.

For this application use the explicit flat queue record Q(front,rear,status,b1,b2). Lists and tokens have one successor. Rev has five pointers, App three, Done one, and Idle is fixed. The two balance cursors are fields of Q, with no intervening pair record. Finite intermediate variables are eliminated when fusing a public queue operation into a transition plan.

We use the conservative FIFO bounds q<=6, A<=12, r<=6. The earlier radius-3 account considered the two execution steps too briefly: dequeue invalidation can pop an old App token before both execution steps pop further tokens. An old pointer copied after those pops need not be within radius 3. That estimate is not used here. This is a quantitative dependency repair, not a change to the queue’s abstract correctness argument.

The address audit is finite by the status cases. Root fields are at depth 1; status fields at depth 2. Budget cursor consumption follows one successor. In an existing App status, invalidation followed by two exec steps traverses at most three token successors, so even the final copied old target is at depth at most 5. The front accumulator traverses at most two successors. Existing Rev list cursors traverse at most two successors; invalidation only changes tokens. A newly started rotation uses the public front (possibly one tail after dequeue) and rear (possibly a fresh enqueue head), and two exec steps again take at most two successors. Done merely returns its stored list. These cases cover tag observations and copied old targets; r=6 is a safe allowance. No numeric radius optimality is claimed.

Each exec step allocates at most two list nodes, one token and one status. Charge both steps, one possible invalidation status, one rotation-start status, one enqueue list node and the final queue record: at most 12 records. This deliberately charges mutually exclusive work together. There is no extra allocated queue tuple for intermediate register assignments.

A Chain Wrap first follows one edge to the FIFO root, reads its front, dequeues, then enqueues once or twice. A composition of three radius-6 plans uses old targets within radius 18 of the original FIFO root: a path through an intermediate fresh graph exits through a previously bounded old target, and the next plan adds at most its radius. From the word root the bound is therefore 19. The three calls allocate at most 36 records; the final Wrap record makes 37. The copied old word-child is at radius zero. Thus the whole basic interface has construction bounds

$$q\le6,\qquad r\le19,\qquad A\le37.$$

Join uses radius zero and at most one record, and Query uses radius zero and none. Initialization contains a fixed valid FIFO for A# and its finite pointer closure, prepared once by two enqueues; it does not depend on input size or nesting depth. All tags are finite, and all old records are immutable.

Why L_* is not visibly pushdown

Alur, Kumar, Madhusudan and Viswanathan’s Theorem 1 says that, for L subset WM, visibly pushdown recognition is equivalent to finite index of the restricted syntactic congruence

$$x\approx_L y\iff\forall u,v\in\Sigma^*: uxv\in L\iff uyv\in L,\qquad x,y\in WM.$$

Wrapping preserves this equivalence: a test of cxr substitutes uc and rv for u and v. If its quotient were finite, the orbit of epsilon under repeated wrapping would eventually cycle. Membership along c^n r^n would then be ultimately periodic. An infinite ultimately periodic set of natural numbers has bounded successive gaps, whereas n_(k+1)-n_k=2^(k+1)+1 is unbounded. Contradiction. Hence L_* has infinite contextual index and is not a VPL.

The mechanism generalizes as a sufficient construction: any given bounded local immutable unary transition system with a returned observation bit can run on single-nesting values, while all other nonempty balanced shapes are rejected. Wrapping adds one word record and one edge of access overhead. This transfers a supplied implementation; it does not discover one or characterize every balanced language.

3. Uniform context application restores an exact characterization

Theorem. For a fixed finite visibly partitioned alphabet and L subset WM, the stronger interface of Section 1 has a bounded local persistent realization if and only if L is visibly pushdown.

For necessity, let r_A,r_Q bound Apply and Query. Query(Apply(C,x)) depends only on the supplied roots’ old views through radius R=r_A+r_Q, by the same fresh/old composition argument as for unrestricted word joining. There are finitely many depth-R value views. Choose a valid handle for each x in WM. Equal-view x,y paired with any independently constructed context C give the same bit, hence agree in every admissible context. If uv is not in WM, then uxv and uyv are outside WM for balanced x,y, so both are outside L anyway. Thus equal views imply x approximately_L y for the full congruence above. It has finite index. The imported theorem gives visibly pushdown recognition. No invariant-discovery algorithm is being inferred from this proof.

For sufficiency, let M be that finite quotient. Concatenation and each bracket wrapper induce well-defined finite operations on M: substitution in either factor or inside a wrapper is itself a context test. Membership is constant on each class. A one-hole context induces a function M->M, so there are finitely many possible context transformations.

Store the M-class at each value root and the entire induced transformation at each context root. Empty, internal letters, Hole and elementary bracket contexts are fixed finite initialization. Cat and Wrap compute their finite class tables. Left/right attachment computes z->m z or z->z m. Context composition composes transformations; Apply evaluates a transformation on a class. Query reads the membership bit. All tables are fixed for L.

Every constructor allocates at most one record with at most two supplied roots: value Cat/Wrap, context Left/Right/Compose, or value Apply(context,value). The last node is decoded by inserting the value word into the context, not by traversing or copying its expanded word. Context wrapping can be a unary record with its fixed wrapper tag. Simultaneous induction on creation order gives the exact word or one-hole-context decoder and the associated class or transformation. Old graphs remain unchanged even with sharing. The construction therefore has q<=2,r=0,A<=1 per constructor or application, and zero allocation for Query. These are existence/construction bounds; computing the quotient from an arbitrary language description is not promised. The premise can instead be supplied as an explicit finite VPA, using the established finite summary construction and finite tables.

4. What separates the two results

For the counterexample, c^k[-]rk is an admissible context, but applying it by k primitive Wrap calls gives k opportunities to advance the clock. The combined observation radius can grow with k. Its sides c^k and r^k are not balanced value arguments for Join. The stronger interface requires the same context, however deep, to be applied in one uniformly bounded operation. The counterexample cannot meet that stronger requirement in any representation within the stated model.

The quantifier distinction is useful: primitive locality gives a finite access bound for each fixed number of future construction steps, with that bound allowed to grow with the number of steps. Uniform context application supplies one access bound for all supplied contexts, independent of their depth. It is this uniformity, together with finite labels and bounded arity, that forces a finite observational quotient. The context itself may still occupy unbounded immutable storage.

This is an operational use of established syntactic-congruence theory and scheduled persistent queues. It does not assert a new VPL characterization independent of that literature. Novelty of the combined formulation and counterexample is unestablished. The two-sort algebra of values and contexts, with context composition acting on values and left/right insertion, is also established: see Bojanczyk and Walukiewicz, Forest Algebras, in its opening account of concatenation, context composition and action. Our well-matched-word presentation uses that familiar pattern; it does not introduce context algebra itself. The additional statements here are the explicit bounded immutable implementation equivalence and the failure when only primitive wrapping is bounded. This focused comparison does not establish originality. The AFP entry verifies a standard Hood-Melville presentation following Okasaki; it does not certify our scalar elimination, radius accounting or balanced-value wrapper.

The companion checker and output test the clock, basic-interface term histories and retained branches against explicit word semantics. The host tuple model is not a constant-time implementation: written record plans establish the claimed bounds. No proof assistant has verified these results.

Neither result is a same-word streaming recognition theorem for flattened input. Each Wrap or Apply is one interface request. Compiling a fixed client requires its own fixed-register and operation-input contract. Word behavior does not imply arbitrary scaffold-context graph equivalence. Any eventual scaffold-to-PEG language transfer must retain its reversal.