FPRD Cross-Area Probe Set 1

Five bounded experiments across automata and formal-language theory

Date: 2026-07-27
FPRD reference point: repository commit b70ff6ccb4d333c825c598bf52f054db72d24cbb

Purpose

This report tests whether FPRD creates mathematical leverage outside its current worked lanes. It does not attempt to axiomatize FPRD or turn five areas into new milestones. Each probe has:

1. a narrowly defined example or question;
2. an FPRD formulation;
3. one mathematical calculation or separation;
4. a comparison with established literature;
5. a decision to promote, retain, or stop.

The five areas are deliberately different:

• finite trees and one-hole contexts;
• infinite alphabets and nominal/register automata;
• infinite words and Büchi acceptance;
• timed words and continuous clock configurations;
• two-way finite automata and crossing sequences.

No novelty claim is made for the results derived here. “Derived result” means that the calculation was completed in this probe. It does not mean that the statement is absent from the literature.

Executive result

The overall outcome is positive. FPRD produced useful structure in three of the five probes and correctly identified one known reformulation that should not be pursued.

Probe 1: Branching inputs and a perfect-tree orbit

Bounded question

Does FPRD reveal anything beyond the standard tree Myhill–Nerode theorem when a finite action presentation generates an infinite family of pairwise distinguishable trees?

Setup

Use the ranked alphabet

$$\Gamma=\{a^{(0)},f^{(2)}\}.$$

Define

$$T_0=a,\qquad T_{n+1}=f(T_n,T_n),$$

and let

$$P=\{T_n:n\ge 0\}.$$

Thus $P$ is the family of perfect binary trees with one member at each height. It has a finite one-action presentation:

$$T_0=a,\qquad D(t)=f(t,t).$$

The orbit of $T_0$ under $D$ is exactly $P$.

This is not an ordinary regular tree grammar: the diagonal action requires both children to be the same previously generated tree. That distinction is part of the probe. The presentation is finite even though the recognized/generated tree family is not finite-state recognizable.

FPRD formulation

• Finite presentation: the initial tree $a$ and the action $D(t)=f(t,t)$.
• Exact dynamic: the orbit $T_0\to T_1\to T_2\to\cdots$.
• Observations: one-hole tree contexts $C[\square]$, with $$o_C(t)=1\quad\Longleftrightarrow\quad C[t]\in P.$$
• Observation cost: $|C|$, the number of non-hole nodes in $C$.
• Finite shadow: two orbit states agree at budget $B$ when no context of cost at most $B$ distinguishes them.

The ordinary tree Myhill–Nerode theorem uses exactly these one-hole contexts. The additional FPRD question is quantitative: how much context is required to expose the difference between two exact states?

Derived result: exact context-access cost

For $n<m$, the minimum cost of a context distinguishing $T_n$ from $T_m$ is

$$\delta(T_n,T_m)=2^{n+1}.$$

Upper bound

Take

$$C_n[\square]=f(\square,T_n).$$

Because $|T_n|=2^{n+1}-1$, the context has cost

$$|C_n|=1+|T_n|=2^{n+1}.$$

It distinguishes the states:

$$C_n[T_n]=T_{n+1}\in P,$$

while $C_n[T_m]=f(T_m,T_n)\notin P$ for $m\ne n$.

Lower bound

Suppose a nontrivial context $C$ makes $C[T_n]$ perfect. At the parent of the hole, the sibling subtree must be exactly $T_n$; otherwise the two children at that node have different heights or shapes. Therefore $C$ contains at least one $f$-node and a complete copy of $T_n$:

$$|C|\ge 1+|T_n|=2^{n+1}.$$

If instead $C[T_m]$ is the perfect result, the corresponding lower bound is $2^{m+1}$, which is larger. Every distinguishing context makes exactly one of the two substituted trees perfect, so the lower bound is $2^{n+1}$.

The formula was also exhaustively checked for $0\le n<m\le 3$ by enumerating all smaller one-hole contexts.

Exact finite-shadow profile

For $B\ge1$, let $q_P(B)$ be the number of equivalence classes of the orbit $\{T_n:n\ge0\}$ under observations of cost at most $B$. Then

$$q_P(B)=1+\lfloor\log_2 B\rfloor.$$

The classes are the individually exposed states

$$T_0,\ldots,T_{\lfloor\log_2B\rfloor-1}$$

and one undifferentiated tail containing all remaining $T_n$.

What is interesting

The exact action dynamic is just the natural-number successor orbit. It is abstractly the same generated action shape as many unary word examples. Nevertheless, the observation-access geometry is exponential because a tree context must reproduce an entire sibling tree before it can test the current height.

This gives a clean separation:

Action conjugacy does not determine observation-access complexity.

The readout and the geometry of admissible contexts are essential parts of the recognition dynamic.

It also suggests a tree-FPRD invariant:

$$\delta_L(s,t) =\min\{|C|:1[C[s]\in L]\ne1[C[t]\in L]\},$$

along with the resulting bounded-context quotient profile.

Literature boundary

The use of one-hole contexts and finite-index congruences is standard tree automata theory. Kozen’s account states the tree Myhill–Nerode theorem in this form and notes its older provenance:

• Dexter Kozen, “On the Myhill–Nerode Theorem for Trees”.

Balanced/perfect binary trees are also a standard source of infinitely many tree-congruence classes. The potentially useful FPRD content is not the nonregularity result; it is the exact observation-cost profile and its comparison with action-conjugate word dynamics.

Decision

Promote, narrowly.

This is suitable for a short theorem/example in FPRD. Before claiming novelty, search specifically for quantitative or metric versions of tree syntactic congruences and context size.

The next bounded task should be to determine whether the same profile can be expressed as:

• a tree Hankel separation radius;
• a bottom-up streaming or communication lower bound;
• or a general formula for diagonal tree-morphism orbits.

Stop if all three are already standard consequences with no cleaner FPRD transfer.

Probe 2: Infinite alphabets and nominal recognition

Bounded question

Can FPRD handle a finite recognition presentation whose concrete residual states and even its fixed-horizon observations are infinite because the input alphabet is infinite?

Setup

Let $\mathbb A$ be a countably infinite set of data values, acted on by all finite permutations. Add a fixed delimiter $\#$, and consider

$$L_{\mathrm{rev}} =\{u\#u^R:u\in\mathbb A^*\}.$$

A nominal pushdown automaton recognizes this language: push the values of $u$, switch mode at $\#$, and pop while comparing the remaining values. This is the infinite-alphabet version of the ordinary delimiter palindrome.

FPRD formulation

• Finite presentation: finite pushdown control with an atom-valued stack.
• Exact dynamic: residual obligations after prefixes.
• Observation: acceptance after a finite data-word continuation.
• Symmetry: simultaneous renaming of all atoms.
• Proposed bounded representation: orbit-finite shadows rather than finite sets of concrete states.
• Resources: number of orbits and maximum support size.

For a word $u=a_1\cdots a_k$, the residual after $u\#$ is

$$(u\#)^{-1}L_{\mathrm{rev}}=\{u^R\}.$$

There are infinitely many concrete residuals at every positive $k$, because there are infinitely many choices of atoms.

Derived result 1: exact orbit count at the midpoint

Two $k$-tuples of atoms lie in the same permutation orbit exactly when they have the same equality pattern. Equality patterns are set partitions of $\{1,\ldots,k\}$. Therefore the midpoint residuals have exactly

$$\operatorname{Bell}(k)$$

orbits, where $\operatorname{Bell}(k)$ is the $k$-th Bell number.

Thus the bounded concrete shadow is infinite, while the bounded symmetry quotient is finite.

Derived result 2: exact maximum support

The residual $\{u^R\}$ is supported by the distinct atoms occurring in $u$. For a tuple of $k$ pairwise distinct atoms, its least support has size $k$. Consequently the maximum support demand at the midpoint is exactly

$$s(k)=k.$$

The lower bound is direct. If a purported residual state after a distinct tuple $a_1\cdots a_k\#$ had support omitting $a_i$, transpose $a_i$ with a fresh atom while fixing the alleged support. The state would be unchanged, so its accepted continuation language would also be unchanged. But the continuation $a_k\cdots a_1$ must be accepted, whereas the continuation with that one atom replaced must be rejected. This is a contradiction.

What is interesting

This gives two nonredundant profiles:

$$\text{orbit count}=\operatorname{Bell}(k), \qquad \text{support demand}=k.$$

Neither ordinary cardinality nor orbit count alone describes the recognition resource. Support records how many distinct data values a state must retain.

For each fixed $k$, a finite-register device can store the needed values. For unbounded $k$, the nominal pushdown presentation retains finite control while the support demand of its residual states grows without bound.

This is closely aligned with the original FPRD distinction:

infinitely many exact states can have a finite structured presentation, and the appropriate finite description may be symmetry-based rather than a finite quotient.

Required extension to the current FPRD core

The present finite-observation doctrine assumes finite bounded behavior algebras over a finite alphabet. That axiom fails literally here. A natural nominal version would replace:

$$\text{finite} \quad\text{with}\quad \text{orbit-finite with an effective support representation}.$$

The reconstruction target would be an inverse system in nominal sets, and its resource profiles would include both orbit count and support.

Literature boundary

This is directly adjacent to established nominal automata theory. Bojańczyk, Klin, and Lasota prove that an equivariant language is recognized by a deterministic orbit-finite nominal automaton exactly when its Myhill–Nerode classes are orbit-finite. They also treat nominal pushdown automata and palindrome languages:

• Mikołaj Bojańczyk, Bartek Klin, and Sławomir Lasota, “Automata Theory in Nominal Sets”.

Register-automaton Myhill–Nerode and minimal-storage questions also have direct prior art:

• Frits Vaandrager and Abhisek Midya, “A Myhill–Nerode Theorem for Register Automata and Symbolic Trace Languages”.

Therefore, orbit-finite residuals or support lower bounds are not themselves safe novelty claims. The FPRD opportunity is the horizon-indexed joint profile, its inverse-system behavior, and transfer to pushdown or other finitely presented recognition dynamics.

Decision

Promote.

This is one of the strongest probes. It identifies a precise extension of the FPRD doctrine and produces an exact calibration family.

The next bounded task should define nominal finite shadows and prove the midpoint profile

$$(\operatorname{Bell}(k),k)$$

inside that definition. It should then test one non-palindrome nominal pushdown language. Stop if the construction adds no result beyond directly restating the nominal Myhill–Nerode theorem.

Probe 3: Infinite words and liveness readout

Bounded question

Does the FPRD residual/readout architecture transfer unchanged from finite words to $\omega$-languages?

Setup

Let

$$L_{\infty a} =\{\alpha\in\{a,b\}^{\omega}:\alpha \text{ contains infinitely many }a\text{s}\}.$$

This is recognized by a deterministic Büchi automaton.

Derived separation

For every finite word $u$,

$$u^{-1}L_{\infty a}=L_{\infty a}.$$

Adding a finite prefix cannot change whether the infinite suffix has infinitely many $a$’s. Therefore the ordinary right congruence has one class.

But no one-state state-based deterministic Büchi automaton recognizes the language:

• if its single state is accepting, it accepts every infinite word;
• if its single state is not accepting, it accepts no infinite word.

A two-state deterministic Büchi automaton recognizes the language by recording whether the most recent symbol is $a$, with the $a$-state accepting.

Equivalently, a one-state transition-based Büchi automaton can recognize it by marking the $a$-transition as accepting. This confirms that the missing resource is not necessarily another residual state; it is acceptance structure on the infinite run.

FPRD consequence

The finite-word pattern

$$\text{residual state}+\text{state readout}$$

is insufficient for general $\omega$-recognition. The readout is a property of an infinite orbit or trace, such as:

• infinitely repeated states or transitions;
• a parity condition;
• a Muller family;
• a topological condition on the run.

An $\omega$-FPRD doctrine would therefore need to distinguish:

1. finite-prefix transition dynamics;
2. residual equivalence of finite prefixes;
3. acceptance structure on infinite generated traces.

A plausible resource field would include:

$$(\text{residual-state demand}, \text{acceptance coloring/index}, \text{topological complexity}).$$

The example proves that the first coordinate can be trivial while the second is not.

Literature boundary

This failure of right congruences to determine $\omega$-automata is known. Angluin and Fisman explicitly study regular $\omega$-languages with trivial or non-informative right congruences:

• Dana Angluin and Dana Fisman, “Regular $\omega$-Languages with an Informative Right Congruence”.

Families of right congruences, $\omega$-semigroups, parity indices, and other acceptance structures already address this problem in established theories.

Decision

Retain as a boundary result; do not promote to a full lane yet.

The probe successfully identifies exactly which FPRD interface breaks: uniform state readout must be replaced or supplemented by trace readout. However, no new invariant or transfer theorem emerged in this bounded pass.

Return only if FPRD can relate finite-shadow growth to an established acceptance invariant, or can transfer a theorem between finite-word and $\omega$-word doctrines.

Probe 4: Exact timed languages and tame continuous dynamics

Bounded question

Does the FPRD distinction between finite presentation, exact state, finite observation, and coordinate realization expose useful structure in timed automata?

Setup

Use timed words whose event times are absolute. Consider

$$L_{\mathrm{time}} =\{(a,t)(b,1):0\le t<1\}.$$

A deterministic timed automaton with finite control and one clock $x$ can recognize this language:

• read $a$ while $x<1$;
• do not reset $x$;
• accept $b$ exactly when $x=1$.

Derived result: continuum residuals at one-event horizon

After reading the prefix $(a,t)$, express the remaining timed input relative to the current time. The required residual is

$$R_t=\{(b,1-t)\}.$$

For $s\ne t$, the continuation “wait $1-t$, then read $b$” is accepted from $R_t$ but rejected from $R_s$. Therefore

$$R_s\ne R_t.$$

There are continuum-many exact residual configurations even though:

• the control graph is finite;
• there is only one clock;
• only one future event is needed to distinguish the residuals.

Thus a word-length-bounded exact observational quotient is not finite.

Derived result: one-dimensional exact realization

Let

$$r=1-t$$

be the remaining time obligation. The entire residual family is represented by the interval $r\in(0,1]$, with:

• delay action $d$: $r\mapsto r-d$ when $0\le d\le r$;
• failure when $d>r$;
• $b$-readout accepting exactly at $r=0$.

These actions and readouts are affine/semialgebraic. Hence the same exact dynamic has:

• continuum-many residual states;
• no finite exact bounded observation quotient at event horizon one;
• a one-dimensional tame coordinate realization.

What is interesting

This example isolates three different observation regimes:

1. Exact timed observation: continuum residual dynamics.
2. Untimed projection: the underlying word language is simply $\{ab\}$, so a finite automaton suffices.
3. Tame coordinate observation: one real coordinate with affine actions gives an exact representation.

This is almost a direct demonstration of the original FPRD motivation. Finite-state quotienting is not the only meaningful form of finite description.

It also shows that a general FPRD theory should not require every doctrine to have finite bounded shadows. There may be at least three legitimate representation regimes:

• finite shadows;
• orbit-finite shadows;
• finitely definable or tame continuous shadows.

Possible quantitative invariants include:

• minimum coordinate dimension;
• definability class of actions and readout;
• number of clocks;
• region/zone complexity after a selected loss of timing information;
• approximation modulus when exact timing is discretized.

Literature boundary

Alur and Dill introduced finite-control timed automata with real-valued clocks and their region construction. The region automaton gives a finite quotient used for untiming and decision procedures; it should not be confused with the continuum of exact timed residual obligations above:

• Rajeev Alur and David Dill, “A Theory of Timed Automata”.

There are also direct machine-independent and Myhill–Nerode-style characterizations of timed languages, including active current work on restricted timed-automaton classes. Any novelty claim must be compared with that literature.

Decision

Promote, as a bounded tame-coordinate direction.

The next task should not attempt a general theory of timed automata. It should:

1. state the continuum-residual/one-dimensional-realization proposition precisely;
2. compare exact timed residual equivalence with Alur–Dill regions;
3. test whether an FPRD coordinate invariant distinguishes two one-clock languages that have the same untimed projection.

Stop if “coordinate dimension” merely becomes “number of clocks” with no presentation-sensitive or observation-sensitive refinement.

Probe 5: Two-way automata and crossing-sequence dynamics

Bounded question

Does treating a two-way automaton as a finite presentation of cut-crossing dynamics produce a useful new FPRD invariant?

FPRD formulation

For a halting two-way finite automaton:

• Finite presentation: its finite control and left/right head actions.
• Generated dynamic: crossing sequences or entry/exit summaries at input boundaries.
• Finite observation: behavior on words through length $N$.
• Readout: acceptance at the endmarkers.
• Candidate profiles: number of reachable boundary summaries, shortest words realizing them, and minimum one-way state demand under a bound on leftward motion.

This formulation is natural and closely resembles the cut systems already developed in FPRD.

What the bounded comparison found

The immediate construction is classical:

• Rabin and Scott and, independently, Shepherdson proved that two-way finite automata recognize only regular languages by converting their two-way behavior into finite one-way summaries.
• Crossing sequences and related boundary summaries are standard mechanisms for that conversion.
• State complexity as the allowed amount of two-way motion increases has already been explicitly studied as a “two-way spectrum.”

Primary comparators include:

• Michael Rabin and Dana Scott, “Finite Automata and Their Decision Problems”;
• J. C. Shepherdson, “The Reduction of Two-Way Automata to One-Way Automata”;
• David Damanik, “Finite Automata with Restricted Two-Way Motion”.

The proposed FPRD resource field is therefore very close to existing descriptional-complexity objects. No new calculation, separation, or transfer appeared in this pass.

Decision

Stop.

Do not open a two-way-automata FPRD milestone merely to rename crossing sequences or two-way spectra.

Return only if one of the following becomes available:

• an exact theorem connecting FPRD’s existing cut fields to crossing-sequence minimization;
• a transfer to two-way transducers, pushdown systems, or pebble automata where the boundary dynamics are no longer finite;
• an instance-sensitive invariant not already present in descriptional complexity.

Cross-probe synthesis

1. FPRD did not behave like one narrow technique

The three successful probes produced different kinds of structure:

• trees: observation-access geometry;
• nominal languages: symmetry and support;
• timed languages: definable continuous coordinates.

That is evidence that the presentation/dynamics/observation separation is portable. The same framework did not force the same invariant onto every model.

2. “Finite shadow” is one case of a broader design choice

The probes suggest three representation regimes:

This is not yet a theorem. It is a useful refinement of the FPRD research question:

What kind of finite description is appropriate for the exact recognition dynamic under the chosen observation doctrine?

3. Readout type must remain explicit

The tree result shows that action dynamics alone do not determine observation cost. The $\omega$-language result shows that state residuals alone do not determine liveness acceptance. The timed result shows that changing from exact timed readout to untimed readout radically changes the quotient.

The FPRD insistence on a uniform readout is therefore substantively useful, but “uniform readout” must be generalized to include trace-level observations.

4. A plausible general resource signature emerged

Across these models, a recognition presentation may need a profile with some subset of:

$$\begin{aligned} &\text{finite state count},\\ &\text{observation-access cost},\\ &\text{orbit count and support},\\ &\text{coordinate dimension and definability},\\ &\text{trace-acceptance index},\\ &\text{presentation size}. \end{aligned}$$

The point is not to combine all coordinates into one universal table. It is to make the representation resource appropriate to the doctrine explicit and then study exact tradeoffs.

5. The stop rule worked

The two-way probe is useful precisely because it was stopped. The FPRD translation was clean, but the candidate objects already had standard names and an established literature. A successful probe program should produce some closures of this kind.

Recommended next move

Do not run five more probes immediately. Take the three promoted results through one additional bounded stage:

1. Tree: literature-check and formalize the exact $2^{\min(n,m)+1}$ distinguishing-context theorem.
2. Nominal: define orbit-finite FPRD shadows and formalize the $(\operatorname{Bell}(k),k)$ midpoint profile.
3. Timed: formalize the continuum-residual/one-dimensional-realization separation and compare it precisely with region equivalence.

Use the same stop condition for each: if the formulation does not produce a new invariant, sharper theorem, or cross-model transfer after the comparator review, retain it as calibration and close it.

The $\omega$-language result should remain a doctrine-design note. The two-way result should be closed.

Overall assessment from this probe set

This first set is evidence that FPRD is not too narrow. It generated meaningful questions in branching, symmetric, and continuous recognition models without requiring those models to be forced into the weighted-automata branch.

It is not yet evidence of a general theorem-producing theory. The strongest next test is whether one of the promoted probes yields either:

• a result not already available in its home literature; or
• a theorem that transfers between two of the three representation regimes.

That is enough to justify continuing the bounded-probe strategy without starting an exhaustive rigor or axiomatization campaign.