Syntactic quotients and bounded persistent context application

Working research note, 1 October 2026.

Question: when can exact observations of constructed values be maintained by finite local immutable rules, including uniform application of every stored one-hole context? The following gives one answer for a fixed finite signature. Its algebraic foundation is classical. The added argument makes the operation interface, persistence and resource bounds explicit.

1. Semantic atoms

Fix finitely many sorts S and a finite signature F of total operations f:A_s1 x … x A_sn -> A_t of finite arities. Assume each A_s is nonempty and the algebra A is generated by its nullary operations. Empty generated sorts can instead be removed, with unusable operation instances removed as well. Let d be the maximum arity (zero if all constructors are nullary). The algebra can satisfy equations: its elements need not be free syntax trees. Fix maps o_s:A_s -> O_s, with each O_s finite. An unobserved sort uses a singleton O_s.

A context of type s->t is a finite constructor expression with exactly one hole of sort s, output sort t, and parameters from A in the other positions. It denotes a function A_s->A_t. Let C_st be all these functions; different expressions with the same function denote the same context. Identity contexts, elementary contexts f(a_1,…,[-],…,a_n), and typed composition generate them. All parameters are ground-generated. Define

$$x\sim_s y\quad\Longleftrightarrow\quad \forall t\in S\;\forall C\in C_{st},\quad o_t(C(x))=o_t(C(y)).$$

Proposition 1 (syntactic congruence). This is the largest congruence of A through which all observations factor.

Proof. Identity contexts give observation preservation. To replace one argument of f by an equivalent value, compose any observing context with the elementary f-context holding the other arguments fixed. The definition gives equal observations after that replacement. Replacing finitely many arguments one at a time proves congruence. Conversely, every observation-preserving congruence is preserved by elementary contexts and their compositions, by induction, and thus relates only equivalent values. This proves maximality. Consequently Q_s=A_s/~_s is finite for every s exactly when the observations factor through a finite many-sorted quotient algebra. For the converse, the kernel of any finite recognizing homomorphism refines ~, so ~ has finite index.

Although the contexts here use the hole once, they give the same equivalence as finite terms with a single variable occurring repeatedly: Proposition 1 makes ~ a congruence, hence preserves every such term by induction. We do not extend this elementary argument to infinitary constructors or arbitrary monads.

2. Operational contract

A value handle decodes to an element of A; a context handle decodes to a function in C_st. Use finite immutable acyclic records, finite tags and handle metadata, fixed pointer arity and number of roots, fixed finite pointer-closed initialization, and finite address-blind operation rules. Every operation has uniform bounds on old endpoint-view radius and allocation. Copying an old pointer into an output counts against the radius, whether its tag is read or not. No address equality, arithmetic on addresses, unbounded scalar, mutable global index, suspended scan or uncharged oracle is available.

Handles can be independently constructed and combined by address renaming and disjoint union over the fixed initialization. Validity and decoding are stable under heap extension. Operations must work on all valid typed tuples, including shared arguments and all retained versions; correctness cannot rely on an unrecorded construction history. The finite views include handle tags and endpoint labels/missing markers; they do not test alias identity.

The interface has each f on value handles, each elementary context constructor with its non-hole operands, Identity_s, Compose(D,C)=D after C, Apply(C,x), and Query_s(x)=o_s(x). It represents every generated value and every context. In particular Apply has one bound for all context depths, not a separate bound for each fixed context. Returning a handle preserves exact decoded values/functions, not merely their observational classes. Decoding is a mathematical map, not a promise of bounded printing or semantic equality tests.

3. Operational syntactic-algebra theorem

Theorem 2. The interface in Section 2 has such a realization if and only if each Q_s is finite. When finite, one construction uses one root per handle, record arity at most max(d,2), old endpoint radius zero, and at most one fresh record per constructor, composition or application. Queries allocate none. These are sufficient bounds, not optima; finite tables and tags depend on A and its observations, not just the signature.

Necessity. Let r_A be the maximum Apply radius over the finitely many sort pairs and r_Q the maximum Query radius. Put R=r_A+r_Q. Composing Apply with Query can observe only radius R of each old input handle: any path through a fresh record exits to an old target within r_A of an input, and the remaining query path adds at most r_Q. Fresh-record tags and output metadata are chosen by finite rules from the same old views. This proves dependence on those views even when Apply returns an old root or uses several fresh records.

There are finitely many depth-R views because tags, roots, metadata and arity are fixed and finite. Choose one valid representative h_x for each x. If h_x and h_y have the same view, pair them, separately, with an independently constructed representative of any C:s->t. The combined views are identical, so Query_t(Apply(C,h_x)) and Query_t(Apply(C,h_y)) agree. Independent amalgamation and address blindness justify using the same C without a hidden shared-history constraint. Thus x~_s y. Each class of representative views lies in one ~_s class, proving finite index. No algorithm for choosing these representatives is required for this counting proof.

Sufficiency. Fix the quotient tables of Q and the observation tables. A value root stores its Q-class; a context root stores its entire induced function Q_s->Q_t. There are at most |Q_t|^|Q_s| such tags for a sort pair. Proposition 1 makes these tags well-defined. The record also retains its constructor and supplied operand roots:

• V_f points to its n value operands and decodes by f in A.
• E_f,i points to its n-1 non-hole operands and decodes to the elementary context with hole in position i.
• Identity has no operands and decodes to the identity.
• Compose points to two context roots and decodes to function composition.
• Apply points to a context and a value root and decodes to application.

All edges point to older records. Nullary values and identity records form fixed finite initialization. Tables calculate V_f classes, elementary transformations, transformation composition, transformation evaluation and query answers from root tags alone. Even an elementary context stores the whole transformation, not just its value at one distinguished class.

Simultaneous induction on record creation proves both exact decoding and tag correctness. Equations of A hold in decoded meanings, whether or not two construction DAGs are physically equal. The induction also works for every history selecting arbitrary retained handles; old graphs are never modified. Taking disjoint unions or sharing operands does not change decoding. The listed records give the claimed bounds. The finite control table may be large; no claim about efficient synthesis or description size is included.

The finite-index premise is semantic and does not assume a controller. To establish it constructively one can supply a finite recognizing algebra, a homomorphism from A and a proof that observations factor through it. For an equational presentation, respecting its equations is an additional proof obligation. Ground-term tag evaluation alone need not respect those equations. This theorem does not decide finite index for arbitrary language or program presentations. A finite table cannot certify an arbitrary infinite semantic specification without a connection proof.

4. Instances and controls

Words. Use one sort A=Sigma*, nullary epsilon and letters, and binary concatenation, with o the membership bit of L. Contexts are exactly u[-]v. The quotient is the syntactic monoid; finite index is equivalent to regularity. The previous Join theorem needs no separate Apply operation: two Joins evaluate u x v. Conversely Theorem 2 supplies Join and Query. This recovers the same realization criterion, not a new language class. Right residual index and two-sided syntactic index differ numerically, but their finiteness criteria agree.

Balanced words. Use epsilon, internal letters, binary concatenation and each unary c[-]r over WM. Every context is (u,v) with uv in WM: reading the unique path to the hole in a balanced parse gives its elementary construction. For L subset WM, contexts with uv outside WM reject every balanced insertion, so adding them does not change ~. Alur et al.’s Theorem 1 identifies finite index with VPL. Theorem 2 therefore recovers the stronger balanced Apply theorem, with q<=2,r=0,A<=1. It does not cover arbitrary languages containing unmatched words.

Negative control. The preceding queue-clock language has a bounded basic Empty/Join/Wrap/Query interface but infinite contextual index. It therefore cannot have uniform Apply in any representation satisfying Section 2. This uses the written queue dependency only for the basic-interface positive result; Theorem 2 itself has no queue dependency.

Exact values may remain infinite. With A=N, constructors 0 and successor, and observation parity, the quotient has two classes. The constructor DAG still decodes to the exact integer; it does not replace all even values by 0. With a constant observation the quotient has one class, while exact values and context functions can still be infinite. Neither case promises cheap printing, integer arithmetic primitives, or raw-heap behavioral equivalence.

5. A sufficient condition for primitive operations alone

A finite template cover means there are finitely many fixed typed constructor terms p_j(x,z_1,…,z_kj), with x occurring once, such that every observing one-hole context is extensionally p_j(-,a_1,…,a_kj) for some generated parameters. A weaker cover of a family giving exactly the same contextual equivalence for the chosen observations also suffices.

Corollary 3. Under this cover condition, a bounded primitive constructor and Query realization exists exactly when the contextual quotient is finite.

Proof. Let N be the largest number of constructor occurrences in the fixed templates, and r the largest primitive radius. Each instantiated template is a fixed program using at most N primitive calls on supplied parameter handles. Its final query sees radius at most Nr+r_Q of x. This is uniform over all parameters. The finite-view counting argument proves necessity. Sufficiency is Theorem 2 restricted to primitive operations. Cover existence, not effective recovery of parameters from an arbitrary context, suffices for necessity. There is no claim that every other realization must construct these templates.

For words the single template (z_1 x) z_2 covers all contexts. For the balanced-word algebra, no finite family of once-hole templates covers all contexts extensionally. In a fixed template, the bracket height immediately before the inserted hole equals the number of wrapper ancestors of that hole; balanced parameter values add net height zero. A finite family bounds this number by some H, whereas c^k[-]rk has height k for every k. To see that extensional equality cannot hide the hole location, compare a template uxv with c^k x r^k on x=epsilon and x=cr. The first forces uv=c^k r^k; the second forces the split after exactly k calls (an earlier or later split leaves a return before a later call). Thus its hole height must be k. This rules out full finite covers for this signature, not every observation-specific cover or alternative presentation. The queue example rules out an observation- sufficient finite cover for that particular non-VPL observation as well.

6. Established theory and the remaining gap

Bojanczyk, Recognisable Languages over Monads, Section 3, Theorem 3.1 and its unary-polynomial construction, supplies the established syntactic-algebra framework. Section 11.3 defines observational completeness and finite covers; Theorem 11.4 connects recognition with uniform continuity under stated finitary and finite-generation hypotheses. Our finite signature proof is a direct specialization, not a new calculus. Its one-hole restriction is justified by Proposition 1 rather than assumed for all monads.

Bojanczyk and Walukiewicz’s Forest Algebras already gives the value/context composition-and-action pattern. Alur, Kumar, Madhusudan and Viswanathan’s Congruences for Visibly Pushdown Languages, Theorem 1, supplies precisely the balanced-language equivalence used above.

Our additional work is the explicit local-view necessity and exact immutable DAG realization, plus the operational specialization of a finite cover. These are elementary operational consequences of established algebra. Novelty is unestablished. Uniform continuity by itself is not a resource implementation theorem: one must specify the metric/observations and prove an effective local realization. Conversely our finite-view argument does not identify heap distance with a language-defined metric.

This closes the word/balanced-context consolidation. It gives a substantial restricted characterization, not the broad primitive-only characterization. The remaining question is which weaker interfaces admit infinite semantic quotients with bounded persistent updates. A useful next test is to distinguish failure of a full context cover from failure of an observation-sufficient cover on one fixed algebra, before proposing any necessity claim about finite covers.

All universal arguments here are written proofs; none is proof-assistant verified. No new finite experiment is used to infer an unrestricted result. The earlier finite checkers keep their original scopes. A fixed scaffold client still requires its separate register and request-encoding contract; this is not a flattened-input streaming theorem. Any scaffold-to-PEG transfer retains language reversal. No generalized pumping conclusion follows.