FPRD LabShare an approach

A classical baseline for bounded-input applications

30 September 2026. A source-to-claim comparison and explicit compiler corollary. The arithmetic recognition principle is classical; no novelty claim is made for it or for the resulting scaffold-language inclusion.

Contents

1. Why compare against counters?

The proposed continuation of two-block clock synthesis sought a uniform result for a1…ak, with distinct letters. Before investing in that extension, ask what its language-recognition consequence would add.

For every fixed finite k, every effectively semilinear set S of exponent vectors already gives a bounded-local persistent recognizer for

L_S = {a1^n1 ... ak^nk : (n1,...,nk) in S}.               (1)

This includes every context-free language restricted to those blocks, and some non-context-free languages. No common clock for the given source’s stacks is required. The construction preserves membership at every prefix; it does not preserve that source’s stack histories.

Fischer, Meyer and Rosenberg’s Counter machines and counter languages, Section 2.2, Theorem 2.2 (credited there to Laing), already relates semilinear count sets to finite Boolean combinations of real-time one-counter languages [1]. Parallel counters and a finite phase check yield the recognition principle. Below we expose the record costs directly, avoiding assumptions about machine-word arithmetic, amortization or post-input processing.

2. Effective theorem and observations

Let Sigma be a finite alphabet, R a supplied regular language over Sigma, and S an effectively given semilinear subset of N^Sigma. Then

{w in R : Parikh(w) in S}                               (2)

has an effective deterministic persistent-record implementation with finite control, fixed finitely many roots, bounded local access and bounded fresh allocation on each input letter. Initial records are one fixed finite immutable graph. Every input prefix has its correct membership bit, including epsilon, with no final scan or extra input letter.

The implementation below uses s integer monitors, s roots, one pointer field per record, at most s fresh records per letter, and old-address radius 1. Here s is the number of nonmodular linear forms retained after effective Presburger quantifier elimination. The reviewed compiler gives

degree max(1,2s), native distance at most 2,
one physical scaffold node per input letter.            (3)

These are construction bounds, not optimal degree, control size or total storage. If s=0, the entire computation is finite-state. Formula conversion is offline and may be expensive; no complexity bound is claimed.

The preservation guarantee is the chosen arithmetic monitor state and fixed- controller prefix acceptance. It is neither arbitrary-context raw graph equivalence nor a simulation of every original pushdown run. A PEG obtained from this scaffold recognizes the reverse of (2).

3. Arithmetic without unbounded numerical primitives

An explicit union of linear sets gives an existential Presburger formula for S. Effective quantifier elimination in Presburger arithmetic with constant divisibility predicates gives a Boolean combination of atoms

b + sum_a c_a n_a >= 0,        b + sum_a c_a n_a = 0,
b + sum_a c_a n_a congruent r modulo m.                 (4)

All coefficients, moduli and the number of atoms are fixed constants of the constructed machine. This is a classical imported algorithm [2]. Congruence atoms are maintained in finite control. For each other form Z, reading a changes Z by the fixed integer c_a.

Choose M=max(1, max |c_a| over these forms and letters). Represent each Z as

Z = M*q + r,             0<=r<M, q in Z.                (5)

Keep r and the sign of q in finite control, and store |q| as the length of an immutable unary list. When Z changes by d, compute in finite control

kappa=floor((r+d)/M),   r'=(r+d)-M*kappa.

Because |d|<=M, kappa is -1,0 or 1, and q’=q+kappa. Thus only one unit change of a signed unary counter is required per form and input letter.

  • If q=0 and kappa is nonzero, push one record and set its sign to kappa.
  • If q and kappa have the same nonzero sign, push one record.
  • If their signs oppose, pop one record, setting the sign to zero if it was the last record.
  • If kappa=0, keep the root and sign.

Every cons record has a finite label indicating whether it was pushed onto an empty list. This lets a pop recognize the last record by the old top label, without inspecting an unbounded number or testing physical identity. Its tail is an old address one pointer hop away. A push points to the old root and sets the last-record label from the maintained zero flag. All parallel updates form one simultaneous batch with at most s fresh records.

Initially q=floor(b/M), r=b-M*q. The finitely many initial unary chains are fixed virtual records, so even large constants impose no first-letter charge. The numerical invariant (5) follows by induction. The sign of Z is determined by the sign of q, except that q=0 uses r; specifically Z>=0 iff q>=0 and Z=0 iff q=0 and r=0. Hence every atom and the full Boolean formula are available immediately in finite control. Track the DFA for R in parallel.

All rule choices are finite and directly generated from (4). They factor through control and the current top labels. Source parameters in (3) satisfy the reviewed native-view contract; no boundary-layer shortcut or alias test is being assumed.

4. All distinct-letter block counts, at once

For (1), choose R=a1…ak. Every word in R is uniquely determined by its Parikh vector. If L is context-free, effectively intersect L with R and compute its Parikh set S by constructive Parikh theory [3]. Then

L intersect R = {w in R : Parikh(w) in S}.

The equality uses injectivity on this distinct-letter block protocol. An arbitrary bounded expression w1…wk need not have this property; the argument does not silently extend to overlapping or repeated-word factors. For general inputs, a Parikh vector does not encode order either.

Examples. Two difference monitors recognize a^n b^n c^n, using the forms #a-#b and #b-#c and the three-block phase guard. This is a semilinear example beyond context-free languages. A Boolean formula handles unions such as #b=#a or #b=2#a without requiring a deterministic choice of stack timing in an earlier nondeterministic presentation. Parity conditions alone need only finite control. Nonsemilinear sets are outside this theorem, not thereby proved impossible for persistent machines.

5. An effective native-distance dichotomy on this testbed

For an explicitly semilinear S in (1), the least allowed native distance in the convention k>=1 is decidably either 1 or 2, with finite degree unrestricted:

distance 1 iff L_S is regular iff S is recognizable in N^k;
otherwise the least distance is 2.                     (6)

A recognizable subset here means membership is determined by finitely many coordinate thresholds and residues, equivalently a finite union of products of unary ultimately periodic sets. To verify the equivalence with regularity, take any s-state DFA. Each letter’s transformation has a transient at most s and eventual period dividing s!, uniformly over starting states. Therefore coordinatewise threshold/residue data determine its answer on the block word. Conversely that data can be maintained by finite control while a DFA checks the block order.

Decidability of recognizable separation for semilinear sets is established in the literature [4]. Compute the semilinear complement of S and apply that result to S and its complement. A separator must then be S itself. This decides recognizability without presupposing a finite representation. On a positive instance an equivalent DFA can be found by enumeration and effective semilinear equality checks on the block protocol. On a negative instance the distance-one regularity boundary rules out every finite- degree distance-one scaffold, while (3) supplies distance two.

The imported regularity/separation decision, our existing native-distance boundary and the explicit counter compiler account for the entire corollary. It is a useful exact baseline, not evidence for a new automata-theoretic regularity discovery. Degree and state minima remain unspecified.

6. Consequence for the research direction

Further fixed-block clock synthesis could give a finer theorem about the height relation of a particular source, or a useful implementation bound. It cannot expand the language-realizability conclusion on this semilinear testbed: the classical baseline already covers every instance, including those without a finite input clock. That is a substantive reason to stop treating additional block counts as the program’s main destination.

The companion clock obstruction separates finite input prediction from cheap use of an actually stored decision and settles unrestricted clock existence in the partial-source model. Together these arguments support investigating controllers which can consult their own persistent summaries, with the cost of producing those summaries charged. They do not supply a universal characterization of persistent computation.

Sources and verification

  1. Fischer, Meyer and Rosenberg, Counter machines and counter languages, Section 2.2 and Theorem 2.2, including its attribution to Laing: https://people.csail.mit.edu/meyer/counter-machines-and-counter-languages-theoryofcomputingsystems.pdf .
  2. Haase, Krishna, Madnani, Mishra and Zetzsche, An efficient quantifier elimination procedure for Presburger arithmetic, introduction and preliminaries: https://arxiv.org/html/2405.01183v1 . We use effective quantifier elimination, not their new complexity bound.
  3. Esparza, Ganty, Kiefer and Luttenberger, Parikh’s Theorem: A simple and direct automaton construction, IPL 2011: https://archive.model.in.tum.de/um/bibdb/esparza/IPL11.pdf .
  4. Rojas Collins, Kocher and Zetzsche, The Complexity of Separability for Semilinear Sets and Parikh Automata, MFCS 2025, Theorem 3.1 and Corollary 3.4: https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2025.38 . The paper credits earlier decidability to Choffrut and Grigorieff. Only decidability is used here, with no composed complexity assertion.
  5. Foundational contracts, Sections 3-4, for the reviewed simultaneous-record compiler and distance-one boundary.

The accompanying checker tests the signed quotient update at sign changes and selected monitor examples with immutable lists. It does not implement quantifier elimination, semilinear extraction, recognizable separation or the general scaffold compiler. Its finite results corroborate the local construction; the unrestricted statements use the argument and imports above.