Grammar Quotients

Definition. Grammar Quotients

For formal grammars $𝐴$ and $𝐵$ , the quotient of $𝐵$ by $𝐴$ is the grammar of what is left of $𝐵$ once an $𝐴$ has been read off the front:

(𝐷_{𝐴} 𝐵) (𝑣) = Σ_{𝑢} 𝐴 (𝑢) \times 𝐵 (𝑢 \cdot 𝑣)

A parse of the quotient consists of an $𝐴$ -parses at prefix $𝑢$ and a $𝐵$ -parse of the full string $𝑢 \cdot 𝑣$ .

This operation has a right adjoint:

(\sqrt[𝐴]{𝐶}) (𝑤) = Π_{𝑢, 𝑣} (𝑢 \cdot 𝑣 = 𝑤) \to 𝐴 (𝑢) \to 𝐶 (𝑣)

Intuitively, $\sqrt[𝐴]{𝐶}$ parses $𝑤$ if: for all splittings of $𝑤$ into a prefix and suffix, if the prefix matches $𝐴$ then the suffix must match $𝐶$ .

Together, these form the adjunction:

𝐷_{𝐴} 𝐵 ⊢ 𝐶 ⟺ 𝐵 ⊢ \sqrt[𝐴]{𝐶}

This is an instance of the Day quotient over the discrete monoidal category of strings.