FPRD LabShare an approach

← Claims

Theorem · presentation-dynamics decomposition

FPRD-RE-T02

Star quotient as a least fixed point

Exact statement

For languages K,LK,L, the quotient Q(K∗,L)Q(K^*,L) is the least fixed point of ΦK,L(X)=L∪Q(K,X)\Phi_{K,L}(X)=L\cup Q(K,X), hence Q(K∗,L)=⋃n≥0Q(Kn,L)Q(K^*,L)=\bigcup_{n\ge0}Q(K^n,L). On a finite derivative carrier of LL, this becomes finite reachability saturation.

StatusProved directly from left-quotient composition
External reviewNo documented external or specialist review of this FPRD result is recorded.

Context

The theorem identifies the exact place where structural recursion becomes a dynamic closure problem: union and concatenation compose directly, while star asks for the closure of every finite number of returns through the quotienting language.

Definitions

  • Q(K,L)=K−1LQ(K,L)=K^{-1}L.
  • The approximants are X0=∅X_0=\varnothing and Xn+1=L∪Q(K,Xn)X_{n+1}=L\cup Q(K,X_n).

Hypotheses and scope

  • K and L are languages over one alphabet; regularity is needed only for the finite implementation statement.

Proof or evidence

Induction gives each approximant as the union of quotients by K^i through its current depth. Their union is the quotient by K*, and every pre-fixed point contains all approximants. A finite derivative carrier realizes the same closure by finite graph reachability.

Fixed-point theorem and proof →

Verification notes

The order in the concatenation identity was checked explicitly: Q(KH,L)=Q(H,Q(K,L)). The fixed-point statement is language-level and does not depend on a particular derivative implementation.

Limitations

  • The theorem explains the carrier construction but does not prove that every carrier-free formulation is impossible.
  • The finite-round bound depends on the chosen finite residual carrier.

Open work

Determine whether the finite star-orbit closure can be compiled uniformly into the stricter model FPRD-RE-D02.