FPRD-T174: Synchronized stack clocks make causal selection effective

1. Visibility-preserving hidden coordinates

Let the hidden and observed alphabets have call, return, and local partitions:

$$\widehat\Sigma =\widehat\Sigma_c\sqcup\widehat\Sigma_r\sqcup\widehat\Sigma_i, \qquad \Sigma=\Sigma_c\sqcup\Sigma_r\sqcup\Sigma_i.$$

A letter projection

$$\pi:\widehat\Sigma\to\Sigma$$

is action-preserving when it maps calls to calls, returns to returns, and locals to locals.

Let A be accepted by a deterministic visibly pushdown automaton. Every projection-compatible causal selector emits a hidden symbol over the observed input symbol. Under an action-preserving projection, the source lift and every selected lift therefore perform the same kind of stack operation at each position.

Their stack contents may differ, but their stack heights are always equal.

2. The synchronized missed-word automaton

Fix selectors

$$F=(T_1,\ldots,T_m).$$

As in FPRD-T173, a word is missed when it has some accepting hidden lift in A but every lift emitted by F is rejected by A.

Simulate these $m+1$ runs in parallel. The finite control stores:

• the source-automaton state for the nondeterministically chosen lift;
• the control state of every selector;
• the source-automaton state reached by every selected lift.

At a call, zip the $m+1$ pushed stack symbols into one tuple and push that tuple. At a return, pop one tuple and distribute its coordinates to the corresponding return transitions. Local letters leave the product stack unchanged.

This is a single visibly pushdown automaton $P_F$, not a multi-stack machine. It recognizes exactly

$$L(P_F) =\pi(A)\setminus\bigcup_{i=1}^mT_i^{-1}(A).$$

If A has q control states and stack alphabet $\Gamma$, while selector $T_i$ has $s_i$ states, then one direct presentation uses at most

$$q^{m+1}\prod_{i=1}^m s_i$$

control states and stack alphabet $\Gamma^{m+1}$, apart from the fixed bottom convention.

3. FPRD-T174: effective selection under a common stack clock

For a deterministic visibly pushdown source A and an action-preserving letter projection $\pi$:

1. Coverage by any fixed finite causal-selector family is decidable.
2. If coverage fails, a shortest missed word is computable.
3. For every fixed selector-count and selector-state budget $(m,s)$, there is a computable horizon $B_{A,\pi}(m,s)$ such that

$$(m,s)\in\operatorname{Sel}(A,\pi) \quad\Longleftrightarrow\quad (m,s)\in\operatorname{Sel}_{B_{A,\pi}(m,s)}(A,\pi).$$

Proof

The synchronized construction above produces a visibly pushdown automaton for the failure language of each candidate family. Emptiness of visibly pushdown automata is decidable. When the language is nonempty, standard pushdown reachability or a context-free grammar conversion computes a shortest accepted word.

For fixed $(m,s)$, only finitely many labeled selector families exist. Compute the shortest missed-word length for every noncovering family and take their maximum. If no family fails, take zero. This gives the stated horizon.

The same procedure constructs the finite obstruction suites from FPRD-T171 and makes both their radius and their words effective.

4. Why forgotten actions are different

The theorem does not apply when $\pi$ erases the call, return, or local type. Then one compatible hidden lift may push while another pops or remains local at the same observed position. The parallel failure construction has independently moving stacks and no longer folds into one visibly pushdown stack.

This gives a structural explanation for the boundary exposed by FPRD-T164 and FPRD-T168:

• hiding labels while preserving the nesting clock leaves fixed-budget selector coverage effective;
• hiding the nesting clock itself permits unboundedly incompatible histories and includes the hard forgotten-action witness.

The negative result is not caused merely by having a stack. It appears when projection destroys agreement about when the stack is being used.

5. Relation to established theory

Alur and Madhusudan identify synchronized push and pop behavior as the reason nested-word and visibly pushdown products retain finite-automaton-like closure and decision properties. T174 applies that classical mechanism to FPRD’s acceptance-blind selector families and obstruction horizons.

Kopczynski’s invisible-pushdown result supplies broader context: once nesting structure is invisible to an ordinary word observer, even regular separability for visibly pushdown languages becomes undecidable. T174 does not reprove or strengthen that result. It records the positive selector tier on the visibility-preserving side of the boundary.

Sources

• Rajeev Alur and P. Madhusudan, Adding Nesting Structure to Words, Journal of the ACM 56(3), 2009: https://www.cis.upenn.edu/~alur/Jacm09.pdf
• Eryk Kopczynski, Invisible Pushdown Languages, LICS 2016, arXiv:1511.00289: https://arxiv.org/abs/1511.00289

6. Evidence and limits

The checker exhausts 4,096 deterministic two-state visibly pushdown machines from a bounded transition family, all eight one-state action-preserving selectors, their singleton and two-selector families, and every observed word through length three. It compares the direct acceptance definition with the zipped-stack product language.

Limits:

• The computable horizon is obtained algorithmically; this note does not give a closed-form size bound.
• The source automaton is deterministic. Nondeterministic selected runs would require complementing their acceptance conditions before forming the missed-word language.
• Projection must preserve the call, return, and local partition.
• The theorem decides each fixed selector budget, not the existence of some unbounded finite selector family.
• The closure and emptiness ingredients are established visibly pushdown theory. No priority claim is made for them.