Left quotients from finite partial derivatives

Exact statement

For regular expressions $A,B$ , form the finite set of states $Q\in Q_B$ reachable from $B$ through $\llbracket A\rrbracket_B$ , and let $f(A,B)$ be their union as regular expressions. Then $L(f(A,B))=L(A)^{-1}L(B)=\{v:\exists u\in L(A),\ uv\in L(B)\}$ .

StatusProved under the finite-derivative interpretation of the requested construction

External reviewNo documented external or specialist review of this FPRD result is recorded.

Context

The construction returns an ordinary regular expression and follows the syntax of A, while using a finite derivative carrier computed from B.

Definitions

The union of an empty set of residual expressions is $0$ .

Hypotheses and scope

Regular expressions have their standard language semantics.
Finite auxiliary relations and transitive-closure saturation are permitted by the intended construction model.

Proof or evidence

By the relational lemma, a residual Q is selected exactly when some u in L(A) reaches Q from B. The partial-derivative membership theorem gives v in L(Q) exactly when uv is in L(B). Taking the finite union proves both inclusions. A checker found no mismatch in 12,555 bounded membership comparisons across 405 expression pairs.

Construction and correctness proof →

Verification notes

The written induction and the finite checker were inspected separately. The checker is corroboration, not a substitute for the proof.

Limitations

The construction uses an auxiliary finite carrier and relation closure.
It does not settle the stricter compiler model FPRD-RE-D02; FPRD-RE-X01 shows only that uniformly bounded star unfolding cannot replace saturation.

Open work

Determine whether the finite carrier and relation saturation can be compiled away under the pinned model FPRD-RE-D02.