Residuals, balanced contexts, and the cost of joining retained words

Working research note, 1 October 2026.

Overview

When a computation stores a word, what must remain accessible so that later operations can use it? A streaming recognizer can often keep exactly the state it needs for the next letter. A stronger interface asks to build two words independently, join their stored representations in bounded local work, and immediately decide whether the concatenation belongs to a language.

That stronger interface has a sharp boundary in the finite-label immutable record model used here: it exists exactly for regular languages. The reason is the Myhill-Nerode idea of a future. If two stored words can be told apart by some continuation, their bounded local views must differ. There are only finitely many such views, so there can be only finitely many distinct futures. Conversely, a finite transition monoid gives a one-record join construction.

Balanced parentheses show why the operation contract matters. A persistent stack recognizes the two-bracket Dyck language while reading a stream, but it does not make arbitrary retained-word joins locally decidable. Restricting all values to balanced words changes the question again: basic join and one-layer wrapping still do not force a finite contextual algebra, while uniform application of stored one-hole contexts does. The later context-application note gives that result.

The semantic ingredients are classical residual and visibly pushdown theory. This note supplies the explicit operational model and its local-view argument. It does not claim a new general theory of automata, a new Dyck algorithm, or established novelty for the operational corollary.

1. A concrete distinction before the general theorem

Let $D_2$ be the language of correctly matched words with two kinds of brackets. An immutable stack supports streaming recognition. An opening bracket creates one stack cell; a closing bracket checks the top kind and follows its tail. A finite error flag handles mismatches. Membership means no error and an empty stack. Earlier configurations remain available.

Now demand a different interface. Independently construct and retain word values x and y. Join them into a value for xy, then immediately ask whether xy belongs to D2. There is no scan, deferred computation or additional stream of internal steps between the join and the answer.

For each n, the 2^n words made of n opening brackets have different futures. If x and x’ are distinct such words, the sequence of closing brackets that exactly closes x accepts after x and rejects after x’. A bounded local view has only finitely many possibilities. It cannot distinguish all these cases. The theorem below turns this observation into a statement about every representation satisfying an explicit standalone-value interface.

This does not prohibit joining two words as a rope in constant work. It prohibits combining bounded local join with bounded local exact membership for D2 in this model. Likewise it does not prohibit the streaming stack.

2. The semantic atoms already exist

For a language L over a finite alphabet Sigma, define its future after w by

$$b_w(u)=\mathbf 1[wu\in L],\qquad u\in\Sigma^*.$$

Equality of these functions is the ordinary right residual equivalence. Appending a letter a acts by the derivative $D_a b(u)=b(au)$. The behavior object is $B=\{0,1\}^{\Sigma^*}$, with observation $b(\epsilon)$. Every deterministic system has a unique behavior map into B, commuting with its transitions and these derivatives. Its reachable behavior quotient is the residual machine; it is finite exactly for regular languages. These are established final-automaton and Myhill-Nerode results, not new definitions whose existence assumes an implementation. See Rutten, Automata and Coinduction, Section 7.

The familiar future metric is also precise:

$$d(b,c)=2^{-\min\{|u|:b(u)\ne c(u)\}},\qquad d(b,b)=0.$$

It is an ultrametric: agreement through an experiment length is transitive, giving $d(b,e)\le\max(d(b,c),d(c,e))$. Derivatives satisfy $d(D_a b,D_a c)\le2d(b,c)$, because a distinguishing u after a is a distinguishing au before it. This organizes finite observations. By itself it gives no effective transition procedure, pointer radius or allocation bound: these statements hold for every language L, without a computability assumption.

A concrete implementation must supply an invariant class I of heaps, a behavior map e, and finite rules U_a with

$$e(U_a(H))=D_a e(H),\qquad U_a(H)\in I.$$

It must additionally bound observation, copied old addresses and fresh records, preserve earlier versions, and start from fixed finite data. The equation alone is correctness of a proposed lift, not a criterion that finds one. Full graph behavior under arbitrary port-testing contexts remains a different observation from a fixed controller’s language residual.

3. An exact operational corollary of Myhill-Nerode

Model and quantifiers

Fix a finite record alphabet, maximum pointer arity q, a fixed number s of root slots per word handle, and finite handle metadata. Heaps are immutable finite acyclic graphs. Missing and fixed initial constants have their own finite observations. A handle may represent a word in many different ways. Its decoded word is denoted alpha(h).

All word-dependent information supplied to an operation belongs to its named handles and their rooted storage. There is no hidden history-dependent global index, address arithmetic, heap-size observation, pointer-identity test, unbounded scalar or externally supplied semantic answer. Control and handle tags are finite. Rules can inspect a fixed-depth labeled rooted unfolding and use old addresses within a fixed radius, or current fresh slots.

Valid handle meanings are invariant under address renaming and heap extension, and handles are independently composable: two independently built valid handles can be used together after disjoint union of their word-dependent storage, identifying only fixed initial data. The operation must work on every such pair, including copies. Ordinary standalone immutable values have this property. An interface with forced cross-handle correlations is outside the theorem.

From fixed finite initialization, finite rules build a valid handle for every word using letters and append or join. Join takes any two valid handles, returns a valid handle for their concatenation, and preserves the old heaps. Query takes any valid handle and returns exactly $\mathbf 1[\alpha(h)\in L]$. Both are total on their admitted inputs. Their fixed observation/address radii and allocation budgets are independent of word length, heap size and operation history. Query is immediate; neither routine defers unbounded computation to a suspension or an uncharged module. Primitive locality includes the old handles it returns, not merely tags read.

No operation promises access to an arbitrarily chosen historical version: the client must already possess the supplied handle. The word interpretation is mathematical, with no requirement to print its letters in constant work.

Theorem

A language L admits this bounded local persistent join-and-membership interface if and only if L is regular.

This characterizes the stated interface across its admitted representations. It is not a characterization of all persistent computations, all scaffold languages, or interfaces consisting only of streaming append and membership.

Necessity

Let rJ and rQ bound the old addresses and observations of join and query. The composition Query(Join(h,k)) depends only on a fixed old rooted view of (h,k). A conservative depth is R=rJ+rQ, with the endpoint-table convention. Join’s selected rule, fresh tags and old links are determined within rJ. A query path through its fresh graph either remains in that determined graph or exits by a join-installed old address of length at most rJ and follows at most rQ more old edges. Returning an old handle obeys the same bound. Thus both decision observations and old targets remain within R. Using the native scaffold view instead requires the established extra frontier layer.

There are finitely many depth-R views of one handle: the number of roots, ports, labels and metadata possibilities is fixed. Choose a valid handle h_w for each word w. If h_x and h_y have the same view, pair each with the same independently constructed handle h_z. Independent composability makes both calls legal. Their combined views agree, and neither routine tests physical identity. Corresponding join plans and query observations therefore give the same bit. Correctness implies

$$\forall z\in\Sigma^*,\quad xz\in L\iff yz\in L.$$

So every view class lies in one right residual class. There can be no more residual classes than handle views. Myhill-Nerode gives regularity. This is an unbounded argument over every word and continuation, not an experiment at a finite maximum depth. It does not give an effective procedure for discovering an arbitrary representation invariant.

Sufficiency and exact preservation guarantee

Given a DFA for L with finite state set Q and initial state q0, let M be its finite monoid of state transformations. Let mu(w) be the transformation induced by w, with multiplication in reading order. Make immutable records E, Letter(a), and Cat(x,y), carrying their mu tags. The initial graph holds E and the finitely many Letter records. Their word meanings are epsilon, a, and alpha(x)alpha(y), respectively.

Join reads the two root tags, multiplies them using a fixed finite table, and allocates one binary Cat record. Query tests whether the stored transformation sends q0 to an accepting state. Append joins with a fixed Letter record. Induction gives the correct word and transformation at every returned root. All old records remain unchanged; joins can use any retained roots and arbitrary sharing. The source bounds are one root per value, maximum record arity 2, old radius 0, and at most one new record per join or append; query allocates zero. These are construction bounds, not optimality claims about a supplied DFA or every implementation.

This proves the converse without assuming a suitable representation in its hypotheses. Finite transition monoids and the residual theorem are classical. The additional exposition here is the explicit operational interface and local-view proof of its boundary; novelty is unestablished.

A control that makes the finite-label hypothesis essential

For one kind of bracket, let b(w) be total opening-minus-closing balance and m(w) its minimum prefix balance, including the empty prefix. Then

$$b(xy)=b(x)+b(y),\qquad m(xy)=\min\{m(x),b(x)+m(y)\}.$$

Dyck1 membership is b=0 and m>=0. Thus a model with unbounded integer fields and unit-cost addition/comparison has constant-operation join and query for a nonregular language. The summaries have an unbounded range; they violate our fixed finite-label/metadata premise. This is a precise positive control outside the theorem, not an exception inside it. Their bit costs and the relation between decoded word length and a shared graph’s size require separate analysis.

For comparison, Amarilli, Jachiet and Paperman, Dynamic Membership for Regular Languages, Sections 1-2, use a fixed-length word, position substitutions, linear preprocessing, and a RAM with growing integer cells. They describe monoid-annotated binary trees as an elementary algorithm. That algebraic ingredient transfers here. Their operation interface and mutable indexed storage differ from ours, so their lower bounds are not imported into this join-only model. No exact prior statement of our operational corollary was established by this focused check; that is not evidence of novelty.

4. Balanced contexts provide the next established baseline

Fix finite disjoint call, return and internal alphabets. WM is the language whose call/return heights never become negative and end at zero. For $L\subseteq WM$, put, on x,y in WM,

$$x\approx_L y\quad\Longleftrightarrow\quad \forall u,v\in\Sigma^*\;(uxv\in L\iff uyv\in L).$$

Alur, Kumar, Madhusudan and Viswanathan, Congruences for Visibly Pushdown Languages, Theorem 1, characterize such visibly pushdown languages by finite index of this relation. Theorem 2 needs additional congruences for languages with unmatched calls or returns. Minimality also requires care: unrestricted VPAs need not have one unique minimal recognizer.

Our direct resource inference is simple. A fixed deterministic VPA uses an immutable cons stack. A call allocates one unary cell, a return inspects the top and reuses its tail, and an internal letter changes finite control. With control in the controller, conservative bounds are A<=1,q=1,r<=1. To make each retained configuration independently resumable, store (control,stack) in a unary immutable header: then A<=2,q=1,r<=2. Initialization is a fixed bottom and initial header. No epsilon steps or final scan are introduced. Each step exactly simulates the VPA, including bottom returns and empty input. Induction preserves its prefix acceptance and all earlier configurations. This supplies a complete streaming persistent baseline, not cheap joining of arbitrary retained words.

The balanced-fragment calculus can be written without inventing new atoms:

$$t ::= \epsilon\mid i\mid tt\mid c\,t\,r.$$

Its operations are concatenation and wrapping a balanced fragment in one call and return. A finite contextual quotient induces finite operation tables. For D2, it has only two classes: internally correct fragments and fragments with a mismatched bracket kind. A mismatch inside a balanced fragment cannot be repaired by outside context; every correct balanced fragment has the same effect as epsilon. Concatenation is Boolean conjunction; wrapping additionally checks that the two bracket kinds agree. Yet unrestricted prefixes have infinitely many ordinary right residuals. The pending calls are precisely what the persistent stack retains. Restricting joins to WM therefore escapes Section 3’s every-word quantifier.

5. Which existing calculi settle which obligations

For the derivative row, Winter, Bonsangue and Rutten, Coalgebraic Characterizations of Context-Free Languages, Theorems 3.8 and 4.4, give the grammar and term-algebra characterizations. The familiar rule is

$$D_a(UV)=D_a(U)V\ \cup\ \begin{cases}D_a(V),&\epsilon\in U,\\\varnothing,&\epsilon\notin U.\end{cases}$$

It is a semantic calculus, without an automatic cost bound on its execution. For Chomsky-Schutzenberger, the formulation $L=h(D_k\cap R)$, with regular R and a possibly erasing alphabetic h, was checked in the introduction of Crespi Reghizzi and San Pietro, Non-erasing Chomsky-Schutzenberger theorem with grammar-independent alphabet. The original historical proof was not inspected. The cost limitation stated in the table is our model comparison, not a theorem imported from that paper.

These selected primary-source checks are a focused comparison, not an exhaustive novelty search. No new proof-assistant verification was performed. The join theorem has a written universal proof; finite example checks only corroborate its sharp streaming-versus-join distinction.

The finite example checker and its recorded scope check transition-monoid rope joins, persistent Dyck streaming, same-view distinct-future examples, and the growing-integer control. They do not establish the theorem over arbitrary representations.

6. What the recent construction work actually contributes

The earlier finite-menu selection theorem is exact within its declared interface, using finite enumeration and separation of free-monoid words. Cache equations and typed-view preservation support verified implementations. They do not find adequate representations or characterize arbitrary behavior. The deque authors’ indexed algorithm remains their construction, with its own stronger formal development.

The accompanying indexed plan checker makes one previously unresolved certificate test executable. It checks an explicit finite straight-line language, including polymorphic Empty, Small and Big. It admits source-relevant repair plans and rejects word-correct ill-typed ones. It also records failure of closure of the narrow nonempty-green-child view. That is useful verification work, with conditional module bounds; it is not the foundational characterization.

The mathematical direction is now explicit: use established residual and context algebras as the semantic foundation, specify the operation interface, and prove or refute its quantitative lift. The join theorem gives a sharp boundary in a natural interface. A next result must explain which restriction or additional resource crosses this boundary, with an independently stated hypothesis and comparison to existing dynamic-language and data-structure results. Adding further deque helper certificates alone does not answer it.

These results concern word membership or a specified controller’s futures, not equivalence of physical graphs under every scaffold context. If used in a fixed scaffold client, the reviewed initialization and native-observation contracts still apply; recognizing L by a scaffold yields a PEG for L reversed.

7. The next implication to test

The balanced-context application note, completed later on 1 October 2026, resolves the test posed in this section. Basic join and primitive wrapping do not imply a finite contextual congruence: that note gives a bounded persistent implementation for a language outside the visibly pushdown class. The stronger interface with uniform application of stored one-hole contexts does have an exact finite-congruence characterization.

Retain Section 3’s finite-label immutable standalone-value model, but admit only balanced word values in WM. Require fixed-local Empty, Join(x,y)=xy, Wrap(c,x,r)=cxr, and immediate exact membership for a fixed L subset WM. The rules must work on every valid supplied balanced value or pair and on all finite term histories, preserving earlier values.

Historical test posed here: must every such bounded realization have a finite $\mathrm{WM}$ contextual congruence, and hence recognize a visibly pushdown language? The later counterexample answers no for this basic interface. The sufficient direction from a finite contextual algebra remains valid, and uniform stored-context application supplies the matching necessary direction in the later note.

The obstruction that prevented copying Section 3’s necessity proof was concrete. A context c^k[-]rk takes k Wrap calls; its combined observation radius may grow with k. Its two unbalanced sides are not separate admitted WM handles. Locality of each operation therefore does not give one fixed-depth view that covers every balanced context. The later result resolves the gap in both directions: its counterexample gives a complete invariant and bounded implementation, and its stronger interface makes arbitrary stored contexts uniformly applicable.