[proofplan]
We reduce language equivalence of two regular grammars to isomorphism of two finite deterministic automata — a problem that admits a brute-force decision procedure. The reduction uses three pre-existing effective procedures: (i) the standard construction of a deterministic finite automaton from a regular grammar, (ii) the restriction to accessible states (decidable by the accessibility algorithm), and (iii) the quotient by indistinguishability (effective because indistinguishability is decidable via table filling). These produce the *irreducible* automaton canonically attached to each grammar. By uniqueness of the irreducible automaton, the two grammars recognise the same language iff the resulting irreducible automata are isomorphic, and isomorphism of two finite labelled graphs is decided by searching through the finitely many candidate bijections between their state sets.
[/proofplan]
[step:Fix notation and outline the reduction]
Let $G$ and $G'$ be regular grammars over a fixed finite alphabet $\Sigma$, with languages $\mathcal{L}(G), \mathcal{L}(G') \subseteq \Sigma^*$. The decision problem is: output "yes" iff $\mathcal{L}(G) = \mathcal{L}(G')$. The reduction has three stages:
1. Construct a deterministic finite automaton $D$ with $\mathcal{L}(D) = \mathcal{L}(G)$, and similarly $D'$ with $\mathcal{L}(D') = \mathcal{L}(G')$.
2. From $D$ and $D'$, effectively construct irreducible deterministic automata $I$ and $I'$ recognising the same languages.
3. Decide whether $I \cong I'$ by exhausting the finite set of bijections between their state sets.
We argue each stage is effective (terminates in a finite number of steps on any input), and that a "yes" for isomorphism is equivalent to a "yes" for language equivalence.
[/step]
[step:Convert each regular grammar into a deterministic finite automaton]
By the standard effective procedure, given a [regular grammar](/pages/???) $G = (V, \Sigma, P, S)$ one first builds a [non-deterministic finite automaton](/pages/???) with states $V \cup \{\text{accept}\}$ whose transitions record the productions of $P$, and then applies the [subset construction](/theorems/???) to obtain a deterministic finite automaton
\begin{align*}
D = (Q, \Sigma, \delta, q_0, F)
\end{align*}
with $\mathcal{L}(D) = \mathcal{L}(G)$ and $|Q| \le 2^{|V| + 1}$. Each step of this construction consists of finitely many elementary operations on finite sets, so the whole procedure is effective; apply it twice to obtain $D$ and $D'$ with $\mathcal{L}(D) = \mathcal{L}(G)$ and $\mathcal{L}(D') = \mathcal{L}(G')$.
[/step]
[step:Restrict to accessible states using the accessibility algorithm]
Define
\begin{align*}
Q_{\mathrm{acc}} := \{q \in Q : q \text{ is accessible from } q_0\}.
\end{align*}
By the [Accessibility is Decidable](/theorems/1799) theorem, membership in $Q_{\mathrm{acc}}$ is decidable state-by-state. Hence $Q_{\mathrm{acc}}$ can be computed by iterating over the finite set $Q$ and testing each state. The transition function $\delta$ preserves $Q_{\mathrm{acc}}$ (if $q \in Q_{\mathrm{acc}}$ witnessed by a word $w$, then $\delta(q, a) \in Q_{\mathrm{acc}}$ via $wa$), so we obtain the *accessible part*
\begin{align*}
D_{\mathrm{acc}} = (Q_{\mathrm{acc}}, \Sigma, \delta|_{Q_{\mathrm{acc}} \times \Sigma}, q_0, F \cap Q_{\mathrm{acc}})
\end{align*}
with $\mathcal{L}(D_{\mathrm{acc}}) = \mathcal{L}(D)$ (starting from $q_0$ no word can leave $Q_{\mathrm{acc}}$). Apply this construction to $D'$ to obtain $D'_{\mathrm{acc}}$.
[/step]
[step:Quotient by indistinguishability using the table-filling algorithm]
On the accessible automaton, the indistinguishability relation
\begin{align*}
q \sim q' \iff \bigl(\forall w \in \Sigma^*\bigr)\bigl[\hat{\delta}(q, w) \in F \cap Q_{\mathrm{acc}} \iff \hat{\delta}(q', w) \in F \cap Q_{\mathrm{acc}}\bigr]
\end{align*}
is an equivalence relation on $Q_{\mathrm{acc}}$. By the [Indistinguishability is Decidable](/theorems/1800) theorem, $\sim$ is decidable; consequently the quotient map $Q_{\mathrm{acc}} \twoheadrightarrow Q_{\mathrm{acc}}/\sim$ can be computed by running the table-filling algorithm and grouping states with empty table entries. The quotient carries a well-defined deterministic automaton structure (indistinguishable states have indistinguishable transitions, so $\delta$ descends to the classes), yielding the *irreducible* automaton
\begin{align*}
I := (Q_{\mathrm{acc}}/\sim,\, \Sigma,\, \bar{\delta},\, [q_0],\, (F \cap Q_{\mathrm{acc}})/\sim)
\end{align*}
with $\mathcal{L}(I) = \mathcal{L}(D_{\mathrm{acc}}) = \mathcal{L}(G)$, and $I$ is accessible (since $D_{\mathrm{acc}}$ is) and has no two distinct indistinguishable states (by construction). Apply the analogous procedure to $D'_{\mathrm{acc}}$ to obtain $I'$ with $\mathcal{L}(I') = \mathcal{L}(G')$. Both $I$ and $I'$ are effectively computable and finite.
[/step]
[step:Reduce language equivalence to isomorphism via uniqueness]
[claim:$\mathcal{L}(G) = \mathcal{L}(G')$ if and only if $I \cong I'$]
$(\Rightarrow)$ Suppose $\mathcal{L}(G) = \mathcal{L}(G')$. Then $\mathcal{L}(I) = \mathcal{L}(G) = \mathcal{L}(G') = \mathcal{L}(I')$. Both $I$ and $I'$ are irreducible deterministic automata, so by the [Uniqueness of the Irreducible Automaton](/theorems/1798) theorem, $I \cong I'$.
$(\Leftarrow)$ Suppose $\varphi: I \to I'$ is an isomorphism of automata. An isomorphism is a bijective homomorphism, so for every $w \in \Sigma^*$,
\begin{align*}
\hat{\bar{\delta}}([q_0], w) \in (F \cap Q_{\mathrm{acc}})/\sim \iff \hat{\bar{\delta}}'(\varphi([q_0]), w) \in (F' \cap Q'_{\mathrm{acc}})/\sim'.
\end{align*}
Homomorphism preservation of start states gives $\varphi([q_0]) = [q_0']$, so the right-hand side is $w \in \mathcal{L}(I')$, and the left-hand side is $w \in \mathcal{L}(I)$. Hence $\mathcal{L}(I) = \mathcal{L}(I')$, which equals $\mathcal{L}(G) = \mathcal{L}(G')$.
[/claim]
[/step]
[step:Decide isomorphism of two finite automata by exhausting bijections]
Write $I = (Q_I, \Sigma, \delta_I, s_I, F_I)$ and $I' = (Q_{I'}, \Sigma, \delta_{I'}, s_{I'}, F_{I'})$ with $|Q_I|, |Q_{I'}|$ finite. Two deterministic automata are isomorphic iff there exists a bijection $\varphi: Q_I \to Q_{I'}$ such that
\begin{align*}
\varphi(s_I) &= s_{I'}, & \varphi(F_I) &= F_{I'}, & \varphi(\delta_I(q, a)) &= \delta_{I'}(\varphi(q), a) \quad \forall q \in Q_I, a \in \Sigma.
\end{align*}
We decide this as follows:
- If $|Q_I| \ne |Q_{I'}|$, output "not isomorphic". (Any bijection requires equal cardinalities.)
- Else enumerate the $|Q_I|!$ bijections $\varphi: Q_I \to Q_{I'}$. For each, check the three conditions by looking up $|Q_I| \cdot |\Sigma| + |F_I| + 1$ table entries.
- Output "isomorphic" iff some enumerated $\varphi$ passes all checks.
*Termination* is immediate: finitely many bijections, each tested by finitely many lookups. *Correctness* is by definition: the enumeration exhausts the set of candidate isomorphisms, so it finds one iff one exists. (The procedure is not efficient, but effectiveness is all that decidability requires.)
[/step]
[step:Combine the stages into the final decision procedure]
On input $(G, G')$, execute in order:
1. Construct $D, D'$ from $G, G'$.
2. Compute the accessible parts $D_{\mathrm{acc}}, D'_{\mathrm{acc}}$ using the accessibility algorithm.
3. Quotient by indistinguishability using the table-filling algorithm to obtain $I, I'$.
4. Run the bijection-exhaustion procedure on $I, I'$ and output its verdict.
Each stage is effective, and by the previous step the output is "isomorphic" iff $\mathcal{L}(G) = \mathcal{L}(G')$. This yields an effective procedure deciding the equivalence problem for regular grammars, completing the proof.
[/step]
