FPRD-RE-D01 · finite construction

The partial-derivative carrier

Let $Q_B$ be the finite set of Antimirov partial derivatives reachable from $B$, including $B$ itself. For a letter $c$, put an edge from $P$ to $Q$ when $Q\in\partial_c(P)$.

Antimirov's partial-derivative theorem makes this carrier finite, even though it represents the effect of arbitrarily long words.

FPRD-RE-L01 · lemma

Interpret the first expression as a relation

Define a relation $\llbracket A\rrbracket_B\subseteq Q_B\times Q_B$ by following the syntax of $A$:

• $0$ is the empty relation.
• $1$ is the identity relation.
• A letter is its partial-derivative edge relation.
• Union is relational union.
• Concatenation is relational composition.
• Star is reflexive-transitive closure.

FPRD-RE-T01 · theorem

The quotient expression

Let $R(A,B)$ be the states $Q\in Q_B$ for which $(B,Q)\in\llbracket A\rrbracket_B$, and define the ordinary regular expression

$$f(A,B)=\sum_{Q\in R(A,B)}Q.$$

The structural proof establishes the theorem. The finite audit below checks the implemented construction against a separately implemented product-automaton oracle.

FPRD-RE-D02 · formulation attempt

An informal carrier-free discipline

One proposed strengthening of “purely inductive” calls a quotient compiler carrier-free constructor-only when its clauses recurse on the regular-expression constructors and return ordinary regular expressions, but do not enumerate a residual carrier, saturate a finite relation, or add an explicit least-fixed-point constructor.

This is an FPRD presentation discipline, not a restriction stated by the problem author. It is also not yet a formal compiler model. Phrases such as “enumerate a carrier” can be hidden inside another data representation unless the admissible recursion schemes, auxiliary values, equality tests, and cost model are specified. Consequently, the discipline can classify named proposals, but it cannot yet support a theorem quantifying over every admissible compiler.

FPRD-RE-T02 · exact structural theorem

The star clause is a least fixed point

Write $Q(K,L)=K^{-1}L$. The non-star constructors satisfy

For star, define the monotone language transformer

On the finite derivative carrier of the target expression, this language fixed point becomes ordinary reachability saturation and stabilizes after at most $|Q_B|$ rounds. Thus the carrier in the proved construction is not an unrelated detour: it is a finite presentation of the star orbit.

FPRD-RE-X01 · negative theorem

No fixed number of star unfoldings is enough

The fixed point cannot be replaced by a uniform finite number of unfoldings. For any $k\ge 0$, take $K=\{a\}$ and$L=\{a^{k+1}\}$. After quotient depth $k$, the shortest residual still contains one $a$, so the empty word is absent. The next step adds it, because$a^{k+1}\in K^*$.

This rules out every uniformly bounded-unfolding star clause. It does not rule out a different algebraic compression. A broader lower-bound question must wait until the compiler class is formally defined.

FPRD-RE-C01 · reproducible finite audit

Three automata formulations agree

A new checker uses 27 quotienting expressions, 15 target expressions, and all 31 binary suffixes of length at most four. It therefore compares

membership decisions. The construction interprets the first expression as a finite relation on derivatives of the second. The first oracle instead explores the synchronized derivative product and asks whether some reachable prefix state accepts the quotienting expression while the target state accepts the tested suffix. The two procedures produced zero mismatches.

Agreement alone can be vacuous if the corpus cannot detect likely faults. Four construction-side mutations therefore reverse concatenation order, truncate star closure after one step, reverse letter edges, or forget the distinguished start residual. The same corpus rejects all four, producing respectively 130, 2, 366, and 132 mismatches. The certificate preserves the first witness for each injected fault.

A second checker removes the first audit's largest common-mode dependency. It independently parses the fixed infix corpus, uses Antimirov partial derivatives on an unsimplified binary syntax tree for the construction, and compares that result with Thompson epsilon-NFAs and subset-product reachability. It does not share normalization, nullability, derivative code, or acceptance logic with the first checker. It also produced zero mismatches, and its complete semantic transcript has exactly the same digest.

The review audit keeps the Antimirov construction but replaces the oracle with epsilon-free Glushkov position automata. It again agrees on all $12{,}555$ decisions and reproduces the same transcript digest. Separately, it checks the hostile unary family for every$0\le k\le64$. This third check shares a parser and corpus with its construction side, so it is a cross-formulation audit rather than a fully independent experiment.

This is a replacement audit, not a reconstruction of the earlier unavailable checker. The matching comparison total does not imply that the two checks used the same expression corpus. Finite evidence also does not replace the all-expression proof. These four negative controls test named proof obligations, not every possible bug. The second audit still shares the fixed expression strings, alphabet, and case ordering with the first.

Checker · Certificate · Independent checker · Independent certificate · Review checker · Review certificate · Review method · Method note

FPRD-RE-B01 · formalization boundary

The remaining task is to define the compiler class

The bounded-unfolding family proves that simple truncation cannot work, while the derivative construction proves that finite residual saturation can. It is tempting to ask whether saturation can always be eliminated, but the current exclusion-based discipline does not determine which encodings or auxiliary computations count as an elimination. The next obligation is therefore a grammar or machine model for admissible compilers. Only then is there a well-posed existence or impossibility question.