When a finite input clock cannot recover a stored decision
30 September 2026. Working research note. The argument below reduces an established undecidable separation problem to the precise clock model used in this program. It is a written proof, not a proof-assistant development. The reduction’s literature novelty has not been established.
Contents
1. A small decision can require a substantial past
Imagine reading a nested document, then a delimiter, then an arbitrarily long sequence of ticks. Some documents require the stack to grow on every tick. Others require it to stay unchanged. A pushdown reader can determine which case applies while reading the document and retain the answer in one bit. An input clock whose control has only finitely many states might be unable to recover that same bit from the document.
This distinction settles the previously open unrestricted clock-synthesis question in our model. There is no algorithm deciding whether a normalized pushdown source has any finite reflected input clock with uniformly bounded height error. This remains true for deterministic partial sources which already have direct bounded-local persistent implementations. On the reduction family, existence with any bounded error is equivalent to existence with zero error.
The result concerns removal of access to stored information. It is not an impossibility theorem for persistent memory, a language-recognition lower bound, or a PEG pumping obstruction.
2. Model, quantifiers and imported premise
A source P has finite control and stack alphabet, a single initially empty stack, and deterministic possibly partial rules. Each rule consumes exactly one input letter and performs one push, one pop, or no stack change. Guards inspect finite control and the top symbol or emptiness. Returns at empty are explicit no-ops where specified. No epsilon steps or final drain are part of the source. Every finite legal prefix counts, even if rejecting or unable to continue on the next letter.
A clock C has finite control R, one initial state, a total transition map tau:R x Delta -> R, and outputs c:R x Delta -> {-1,0,1}. Initially H=0; on each letter x it updates H to max(0,H+c(r,x)). Its control cannot inspect H, source control, stack symbols, or pointers. We ask whether
exists finite C, exists B in N, forall legal source prefixes w:
|h_P(w)-H_C(w)| <= B. (1)Acceptance does not occur in (1). All source states may be declared rejecting, giving the empty language in every instance of the reduction.
Imported premise. Kopczynski, Invisible pushdown languages, Theorem 2.4, proves undecidability of regular separation for two disjoint binary flattened tree languages. Their structural opening and closing symbols are shared, so the resulting visibly pushdown languages have a common visibility partition. The promise is disjointness, not that their union is every word. Both languages consist of well-matched words. See the definitions preceding Theorem 2.4 and the reduction in Section 3, not only the abstract [1].
We also import effective visibly pushdown determinization, using the corrected Alur-Madhusudan construction [2, Theorems 3.1 and 3.3]. Thus the input to our reduction may be taken as two deterministic visibly pushdown automata A0,A1 over the same partitioned alphabet Sigma, accepting disjoint K0,K1. Acceptance is a finite-control test. Complete them over Sigma, allowing bottom returns as no-ops, and form their synchronous product. One stack holds pairs of their stack symbols: every call pushes once and every nonempty return pops once. This preprocessing is effective and preserves the common visible height.
These are standard imports. Our additional argument is the tail construction and the exact equivalence in Section 4.
3. The deterministic source constructed from K0 and K1
Add fresh letters # and t. Before #, simulate the product of A0 and A1. For w in Sigma, its stack height is the usual reflected visible height V(w). All words in Sigma are legal in this phase, whether accepted or not.
On #:
- if w is in K0, leave the stack unchanged and enter mode 0;
- if w is in K1, leave the stack unchanged and enter mode 1;
- otherwise, the # transition is undefined.
Disjointness makes this deterministic. In mode 0 every t keeps the stack; in mode 1 every t pushes a fixed symbol. No other letters are legal there. The complete legal-prefix domain is exactly
Sigma* union (K0 union K1)#t*.For every w in Ki and every j>=0,
h_P(w#t^j) = V(w) + i*j. (2)All words supplied by the imported undecidability premise are balanced, so V(w)=0 at their delimiters. The proof also works for unbalanced K0,K1. Initialization is an empty paired stack and the product initial state; # is an ordinary input letter, not a hidden initialization or lookahead operation.
Partiality matters. Completing the missing # transitions with a continuing flat sink would impose additional tail requirements on Sigma* minus (K0 union K1). The separator hypothesis imposes no such requirements. That completion is not used, and this note does not claim the same restricted-family theorem for total sources.
4. Exact equivalence with regular separation
Tail-separation theorem. For the source above, the following are equivalent:
- A finite clock satisfies (1) for some B.
- A regular language S contains K1 and is disjoint from K0.
- A finite clock tracks every legal source prefix exactly (B=0).
A bounded-error clock yields a separator
Fix a clock state r and follow t indefinitely. Its state sequence has a finite transient and a cycle. Let mu(r) be the mean of the outputs on that eventual cycle. From any fixed starting height x>=0, reflection gives
lim_{j->infinity} H_r,x(t^j)/j = max(0,mu(r)). (3)For completeness, write S_j for the cumulative signed outputs. Then S_j=mu(r)j+O(1), and
H_r,x(t^j)=x+S_j-min(0,min_{0<=ell<=j}(x+S_ell)).If mu is positive, the minimum is bounded below and the limit is mu; if negative, the reflected height is bounded; if zero, the signed sums and reflected height are bounded. This proves (3). The initial height may depend on w: we fix w before taking the tail limit, so no uniform bound on x is being assumed.
Let G be the finite set of clock states whose eventual t-cycle has mean 1. For w in K1, (1)-(3) force the clock state after w# to lie in G. For w in K0, they force its mean to be nonpositive, so that state is outside G. Therefore
S = {w in Sigma* : tau*(r0,w#) is in G} (4)is a regular separator. A DFA for it uses the clock states and treats r as accepting exactly when tau(r,#) is in G. Output means strictly between 0 and 1 cannot serve either required tail. The argument allows every finite clock, not just an enumerated state budget.
A separator yields an exact clock
While reading Sigma, run a DFA for S and emit +1 on calls, -1 on returns, and 0 on internal letters. Reflection gives H=V on every prefix. On # emit 0 and enter a t-mode selected by the DFA’s acceptance: emit +1 forever in the S case and 0 forever otherwise. Complete the clock arbitrarily on other inputs. For every legal delimiter, the separator selects exactly the source mode. Equation (2) proves exact equality on all legal prefixes, including epsilon, w#, and each finite tail prefix. Thus 2 implies 3; 3 implies 1.
If the supplied separator has s states, this construction uses at most s+3 clock states: the prefix states, two tail modes, and a sink. This is a construction bound, not a minimum. Its outputs are unit operations, and its numerical height is never tested.
5. Decision consequences and their limits
By [1] and the effective reduction, (1) is undecidable already for this deterministic partial family. For every fixed B>=0, asking for some clock with that error bound is also undecidable: within this family any successful bound implies the existence of an exact clock. Thus the unknown numerical error is not responsible for the undecidability.
This is compatible with the earlier result that a given clock’s uniform error is decidable. A fixed observer-state budget still gives finitely many clocks to check. Without that budget, enumerating clocks and using the fixed- clock decider semidecides positive instances but cannot always terminate on negative ones. There is no total computable bound on the number of states needed by successful clocks as a function of the source description: such a bound, finite enumeration and fixed-clock checking would decide (1). This last conclusion also has a proof independent of our fixed-clock theorem. Formula (4) converts any successful s-state clock into a separator with at most s states. A bound would therefore allow enumeration of finitely many separator DFAs; each candidate is checkable by visibly pushdown/regular intersection and emptiness. That would decide the imported separation problem.
These statements exclude an algorithm for this clock-existence property. They do not exclude non-effective characterizations, useful sufficient certificates, or decidability on additional subclasses. They do not assert undecidability of every finite-state synthesis problem.
6. Positive and negative examples
Positive, including nonregular document languages. Let W be all balanced parenthesis words, let x,y be internal letters, and take K1=Wx, K0=Wy. The last letter separates them. A clock tracks nesting in the prefix, then uses that finite-state separator to choose the exact tail. Arbitrarily deep nesting by itself is no obstruction.
Negative with no stack left at the delimiter. Let a,c be calls and b,d returns, and consider
K1 = {a^n b^n c^q d^q : n,q>=1},
K0 = {a^n b^p c^q d^(n-p+q) : n>p>=1, q>=1}. (5)Both languages are balanced, disjoint and visibly pushdown. A deterministic reader checks the four nonempty blocks, rejects unmatched returns, records whether its stack is empty at the b/c boundary, and checks final emptiness. An explicit bottom marker on the first pushed record lets a return update the empty flag using just the popped symbol.
They are not regularly separable. For any DFA with s>=1 states, let N=s and P=s!. For each letter x its transition function satisfies f_xN=f_x(N+P) on every state. Consequently the DFA ends in the same state on
u=a^N b^N c^N d^N in K1,
v=a^(N+P) b^N c^N d^(N+P) in K0.No acceptance choice can separate them. By the theorem there is no finite clock with bounded error for the associated source. At # both source stacks are empty. The useful retained fact is the bit computed at the earlier b/c boundary, not the remaining stack size.
A failed strengthening. Giving the observer the source’s mode bit at # immediately permits exact tracking: use the visible clock before # and that bit afterward. This bit is computed by the actual persistent stack reader; it is not an oracle with uncharged preparation. The negative result depends on forbidding that memory observation.
7. Persistent cost and the meaning of the obstruction
Every constructed source, positive or negative, has one immutable linked stack. A call allocates one labelled cons record pointing to the old root; a return selects the old tail; a keep reuses the root. All decisions inspect finite control, the top label and emptiness. No physical pointer identity is tested. Thus s=1 root, q=1 pointer field, A=1 fresh record and old-address radius r=1 suffice. The reviewed compiler [3] gives degree 2 and native distance 2, with one physical scaffold node per input letter, fixed virtual empty initialization, and no padding step. A stuck input can be represented by a dead flag; the simulated stack/control guarantee concerns legal prefixes.
The compiler preserves the decoded deterministic stack and control, hence same-word prefix acceptance for any declared source acceptance. It does not identify the raw source and target graph vocabularies under arbitrary testing contexts. If acceptance language L is transferred to a PEG, that PEG recognizes L reversed. Declaring all states rejecting makes L empty throughout this reduction, so the clock difficulty cannot be a lower bound for every presentation of the accepted language.
The example exposes a precise difference between two questions: whether a past-dependent decision can be maintained cheaply using stored structure, and whether finite input-only control can reconstruct it. Our original memory question permits the former. A future observer can need only one bit while the process of maintaining that bit uses an unbounded, locally updated stack. This is consistent with the replayable-memory distinction between an answer quotient and the cost of transporting it through updates [4].
8. Status, dependencies and the next constructive question
This settles the unrestricted input-only clock-existence question in the stated partial-source model, conditional only on the explicit established imports. The two-block decision theorem remains a positive subclass result. The extension to more fixed blocks is not decided here. Its language-level motivation is weakened by the classical construction in the companion semilinear baseline.
The useful next question permits a deterministic stack observer to consult its own stored top while producing the clock actions. Given that observer and a candidate skew bound, can the buffer normalization and visibly pushdown determinization be combined into one deterministic persistent stack, with an effective first-exit check? Pairing the observer stack with the determinized summary stack is a concrete route. This note does not prove that extension or decide synthesis of such observers. Its costs must include the observer’s own stack maintenance; adding a free oracle would evade the original question.
The executable companion checks finite tail dynamics, a positive separator construction, and the explicit DFA collision family. It does not implement the BFG reduction, general VPA determinization, unrestricted clock synthesis, or a proof assistant. Infinite statements rest on the proofs above and their named imports. No new pumping or recurrence theorem is asserted.
Primary sources and local dependencies
- Eryk Kopczynski, Invisible pushdown languages, Theorem 2.4 and Section 3. Author manuscript: https://arxiv.org/pdf/1511.00289 . The imported result is regular-separation undecidability for disjoint BFG languages with a common structural alphabet; it is not a new undecidability technique here.
- Rajeev Alur and P. Madhusudan, Adding nesting structure to words, corrected JACM version, Theorems 3.1, 3.3 and 3.5: https://www.cis.upenn.edu/~alur/Jacm09.pdf . These supply effective finite- control acceptance, determinization and the synchronized product.
- Reviewed record compiler and foundational contracts.
- Replayable memory, especially the support/quotient distinction and stationary transport obligation.
- Fixed-clock decision, used for the positive semidecision and no-computable-state-bound corollary, not for the reduction.
- Executable stress checks and recorded scope and output.
Nearby transducer uniformization results concern different relation and observation models. This proof uses a direct regular-separation reduction instead of importing their undecidability by analogy. No claim of originality follows from the targeted literature search.