Bounded stack skew can be absorbed into finite control

Research note, 29 September 2026. Proof supplied below; not formally verified or independently reviewed. No priority claim.

Overview

A pushdown machine can do the right stack work at slightly different moments from a visible reference clock. For example, while reading a pair $ac$, it might push on $a$ or delay the push until $c$. If the clock treats $a$ as the call, the two stack heights briefly differ by one and then meet again. The same early-or-late choice can occur for a later pop.

This note asks whether a fixed bound on that timing error is enough for a persistent implementation. The answer is yes for a specified real-time pushdown machine, a supplied visible clock, and a bound $B$ that covers every run and every prefix. The construction keeps the few source-stack symbols near the disagreement in finite control. The deeper, shared tail follows the visible stack. It yields a visibly pushdown automaton for the same language and then, through the reviewed compiler, a degree-two, distance-two scaffold.

The result is a sufficient and effectively checkable certificate, not a characterization or a lower bound. It does not decide whether a different clock, a larger unknown bound, or another presentation would work. The main open question is how to recover a useful clock from a natural source description instead of receiving one as part of the certificate.

1. Model and statement

Fix a finite alphabet with a supplied partition $\Sigma=\Sigma_c\sqcup\Sigma_r\sqcup\Sigma_i$. Its clock starts at $H(\epsilon)=0$, increases by one on a call, decreases by one on a return when positive, and stays fixed on an internal letter or a return at zero.

Let $P$ be a finite, possibly nondeterministic, real-time pushdown machine. It starts with an empty stack over a finite alphabet $\Gamma$. Each input letter consumes exactly one transition. A transition can inspect finite control and the top symbol, or emptiness, and then:

• push one symbol, leaving the old stack unchanged underneath;
• pop one symbol (with an explicitly specified bottom no-op, or no transition);
• leave the stack unchanged.

There are no epsilon moves, bulk rewrites, pointer-identity tests, or hidden work between letters. Transitions may be partial. A finite initial-state set is allowed. Acceptance is existential final-state acceptance; a final top-symbol or emptiness predicate is also allowed.

For a supplied integer $B\geq0$, the corridor condition is

$$\forall w\in\Sigma^*\ \forall \rho\text{ a run of }P\text{ on }w: \quad |h_\rho(w)-H(w)|\leq B. \tag{C}$$

This quantifies over every finite run from an initial configuration, including rejecting runs and prefixes of runs that later get stuck. Checking only accepted words, final heights, or one selected run does not establish (C).

Proposition (bounded-skew normalization). If (C) holds, one can effectively construct a nondeterministic visibly pushdown automaton $V$, for the supplied partition, with $L(V)=L(P)$. It uses a stack of height exactly $H(w)$ and a finite buffer of at most $2B+1$ source symbols. The construction is letter-synchronous and preserves acceptance after every prefix, including the empty prefix.

For fixed $P,\Sigma_c,\Sigma_r,\Sigma_i,B$, condition (C) is decidable. If false, a shortest violating input and a corresponding source run can be computed by finite pushdown reachability.

By classical visibly pushdown determinization, $L(P)$ has a deterministic visibly pushdown recognizer. The Lab’s bounded-record compiler consequently gives a scaffold of degree two and distance two, with finite labels and control, appending exactly one physical node per input letter. Hence $L(P)^R$ has a PEG. The PEG conclusion contains exactly one reversal.

The bounds two and two are sufficient construction bounds. They do not assert optimal degree or count the finite-control cost of buffering and determinization.

2. The buffer invariant

Write a source stack bottom to top as $s$, of length $h$. At clock height $H$, set

$$C=\max(0,H-B-1),\qquad s=vu,\qquad |v|=C. \tag{1}$$

The aligned stack has $H$ frames. Its first $\min(H,B+1)$ frames carry dummy payloads; subsequent frames carry the symbols of $v$, in order. The finite control stores the suffix $u$, the source state, and

$$t=\min(H,B+2).$$

Each frame additionally stores the value of $t$ immediately before that frame was pushed. This finite tag restores the capped height after a return. Below and at $H=B+1$ all source symbols are buffered. Above that threshold, (C) gives

$$1\leq |u|=h-H+B+1\leq2B+1. \tag{2}$$

At smaller heights, $0\leq|u|=h\leq2B+1$. Thus the source top is always in finite control when the source stack is nonempty. In particular, an empty buffer means an empty source stack on every represented configuration.

The one-cell margin matters. Cutting at $H-B$ instead would allow an empty buffer over a nonempty core. Then a source transition inspecting its top on an internal letter could require reading the aligned stack, which a visibly pushdown internal transition cannot do.

A direct finite-control bound for this nondeterministic simulation, before adding any optional acceptance flags, is

$$|Q|(B+3)\sum_{j=0}^{2B+1}|\Gamma|^j.$$

A frame belongs to an alphabet of size at most $(B+3)(|\Gamma|+1)$, excluding the bottom sentinel. These are loose bounds; many combinations are unreachable.

3. One-step simulation

The source transition is chosen using only its state, next letter, and the buffer’s last symbol, or its emptiness. Apply the chosen source operation to the buffer to obtain a temporary word $u_0$. Its length is at most $2B+2$. Let $\delta h\in\{-1,0,1\}$ be the actual source height change, treating a permitted bottom-pop as zero. Let $\delta H$ be the clock’s actual change, also zero for a bottom-return.

The old height difference is available in finite control:

$$h-H=|u|-\min(t,B+1).$$

Consequently the next difference

$$e'=|u|-\min(t,B+1)+\delta h-\delta H \tag{3}$$

can be computed without reading an unbounded counter. A step satisfying $|e'|\leq B$ is normalized as follows.

Call cases are determined by $t$ and do not inspect the aligned stack. Return cases read only the popped frame, which is permitted. Internal steps read no aligned-stack symbol.

On a call that transfers a real symbol, (C) after the step implies $|u_0|\geq2$: the new core needs one symbol and the final buffer retains at least one. On a return that transfers a real symbol, the old frame is exactly the last symbol of $v$. It has not been changed by the source operation, because that operation touched only the buffered top.

These observations prove that the table produces the unique decomposition (1) of the new source stack. The cap is updated on calls and restored from the popped tag on returns. Initialization has empty aligned stack, empty buffer, and $t=0$.

Induction on input length gives both directions of run correspondence: each source run inside the corridor has a simulated run, and each non-error simulated run decodes to a source run. Carrying the source accepting predicate then proves language equality and prefix acceptance preservation.

This correspondence is before determinization. The deterministic recognizer need not choose, expose, or preserve one particular nondeterministic source history.

4. Checking the hypothesis without assuming the conclusion

Build the same finite visibly pushdown transition system without assuming (C). It simulates source runs as long as (3) stays in $[-B,B]$. If a legal source transition first leaves that interval, move to an accepting error state while performing the prescribed visible stack action. An error call can push a dummy, an error return can pop the available frame, and an error internal step leaves it unchanged. In the error state, consume subsequent letters with the same visible discipline.

Before the first error, the invariant is valid by induction. Therefore this automaton accepts exactly those words having a prefix and a source run that first violate (C). It is finite and effectively constructible: all buffers, capped-height tags, states, source rules, and visible letters range over explicit finite sets.

Visibly pushdown emptiness decides whether an error is reachable. Standard pushdown-to-grammar conversion with shortest-derivation computation returns a shortest word if one exists. Retain source-rule identifiers on simulated edges to recover the witnessing run. A shortest accepted word ends at the first error, since every extension of an error is accepted.

Thus checking a supplied clock and bound uses an error-reachability construction, not an assumed deterministic recognizer or an assumed persistent realization.

This does not decide whether some unboundedly searched value of $B$, some other clock, or some different presentation will work.

5. The persistent compilation

Apply the established visibly pushdown determinization theorem to $V$. Use the corrected author-hosted version of Alur and Madhusudan’s Adding Nesting Structure to Words, Theorem 3.3 and its visibly pushdown translation.

Represent the resulting deterministic stack as immutable linked records. There is one root, one pointer field per record, and at most one fresh record per letter. A push allocates one record pointing to the old root; a pop copies its tail; a local step preserves the root. Empty stack is a missing logical root, so no nonempty initialization is needed.

In the reviewed simultaneous-record interface, take $s=A=q=1$ and old address radius $r=1$. This gives

$$d=\max(1,s+Aq)=2,\qquad k=r+1=2.$$

Labels and finite control encode the deterministic automaton and slot tags. No physical identity query is needed. The compiler preserves the decoded deterministic stack and control, with one scaffold step per source letter. The whole route preserves accepted words and all acceptance decisions at input cuts. It does not identify the original nondeterministic stack graph with the target scaffold under arbitrary graph-testing contexts.

LMR’s scaffold-to-PEG theorem applies to the reversal of this same-word language. No epsilon padding or inserted initialization letter is used.

6. A positive example with genuine hidden timing

Use observed alphabet $\{a,c,b,d\}$, with $a$ a call, $b$ a return, and $c,d$ internal. A source uses finite control to allow only prefixes of $(ac)^*(bd)^*$. Within each $ac$ pair it chooses whether to push on the first or second letter; within each $bd$ pair it chooses whether to pop on the first or second letter. It remembers that choice until the pair ends. It starts a return pair only with a nonempty source stack and accepts at pair boundaries exactly when the source stack is empty.

At every pair boundary the source and reference heights agree. Within a pair they differ by at most one. Hence (C) holds with $B=1$, while $B=0$ fails on a delayed first push. The accepted language is

$$\{(ac)^n(bd)^n:n\geq0\},$$

which is nonregular. The proof is by counting pairs; a homomorphism erasing $c,d$ maps it to $\{a^nb^n:n\geq0\}$.

This source can be written as a partial deterministic visibly pushdown machine on hidden tagged letters: the tags specify the early/late choices, and finite control checks their pairing. Forgetting those tags mixes call and internal actions in projection fibres. Arbitrary compatible hidden words can have unbounded skew, as shown by the earlier clock dichotomy, but the source’s legal prefixes cannot. Thus the result extends the applicability of exact synchronization to presentations with source-constrained timing errors. It does not enlarge the visibly pushdown language class for the supplied visible partition.

For a fixed finite family of projection-compatible Mealy selectors, restrict the hidden choices to each selector’s output, carrying its state in control. Every surviving run inherits (C). Normalize the existential projected source and each selected source to VPAs on the same visible partition. Determinize and take the difference

$$\pi(A)\setminus\bigcup_i T_i^{-1}(A).$$

Its emptiness decides coverage, even though the projection need not preserve hidden action types. Undefined selected-source runs reject; they are not completed with arbitrary stack actions before checking (C). As in the exact-synchronization case, enumerating a fixed finite selector budget yields a computable missed-word horizon. This concerns fixed budgets, not whether some finite cover exists.

7. Negative controls and limits

If one input symbol independently allows a push or a no-op at every step, then after $x^n$ there are heights $n$ and zero. Their distance $n$ precludes any common height within $B$ of both once $n>2B$. No supplied clock can certify this presentation with fixed $B$. Nevertheless, if all its states accept, its language is $x^*$. Failure of the certificate is therefore not a language lower bound.

The lower bound in (C) prevents the aligned core from exceeding the source stack. The upper bound makes the buffer finite. Dropping either bound breaks this particular invariant. That is not an impossibility theorem for other encodings.

An amortized allocation theorem does not meet the per-letter compiler contract. Unbounded epsilon work or multi-symbol pushes likewise require separate timing and resource arguments.

No pumping theorem is proposed here. Reusable interfaces and a recurrence theorem would be separate obligations. Nothing here contradicts LMR’s obstruction to unrestricted effective PEG pumping.

8. Established ingredients and contribution

The argument supplied here is the explicit $2B+1$-buffer invariant, its first-exit verifier, and its composition with the reviewed scaffold compiler and fixed-budget selector procedure. This identifies the incremental work relative to the existing Lab notes. Literature priority for bounded-skew normalization has not been established. It may be a standard robustness construction in synchronized-pushdown theory.

9. Verification and next question

The induction above is the unrestricted argument. The accompanying Python audit compares the local algorithm with direct stack operations on bounded configurations, checks first-exit detection, exercises different symbols in deep stack cores, and tests the early/late example. It does not implement or formally verify VPA determinization, pushdown emptiness, the full source compiler, or any imported theorem. No Lean verification is claimed.

The next decisive question is whether the explicit visible clock can be recovered from a natural source description, or replaced by an effective finite-state clock, without assuming the desired synchronized realization. First compare the buffer construction with Caucal and subsequent work. Avoid turning a supplied-clock sufficient condition into an intrinsic language characterization.

Primary sources

• Alur and Madhusudan: https://www.cis.upenn.edu/~alur/Jacm09.pdf
• Nowotka and Srba: https://people.cs.aau.dk/~srba/files/NS:MFCS:07.pdf
• Caucal: https://igm.univ-mlv.fr/~caucal/Sync.pdf
• Driscoll et al.: https://www.cs.cmu.edu/~sleator/papers/making-data-structures-persistent.pdf
• Loff, Moreira and Reis: https://arxiv.org/html/1902.08272v2
• Jecker and Filiot: https://arxiv.org/pdf/1504.03864
• Kim and Park: https://arxiv.org/abs/2608.29592
• Ko: https://arxiv.org/abs/2603.25914

Local dependencies: compiler review, synchronized selectors, clock dichotomy.