Regular grammars recognize exactly the DFA languages

Statement

A language is generated by a regular grammar if and only if it is recognized by a deterministic finite automaton (DFA). The grammar and automaton models agree on the class of regular languages. Langlib also shows left-regular and right-regular grammars are equivalent.

In Lean

Left-regular ⇔ right-regular grammars are proved in LG_eq_RG.

Proof idea

Grammar → DFA. NFA_of_RG builds an NFA over the finite state set Option g.FinNT, where g.FinNT is the (finite) subtype of nonterminals appearing in the grammar and the extra state none is the sole “completed” marker. A rule A → aB becomes a transition A —a→ B, a rule A → a becomes A —a→ none, and the accepting states are none together with every nonterminal carrying an A → ε rule. Forward/backward simulation lemmas (NFA_of_RG_some_forward / NFA_of_RG_some_backward, and the none variants) match runs of the NFA against RG_derives; NFA_of_RG_accepts packages them into (NFA_of_RG g).accepts = RG_language g. Mathlib’s NFA.toDFA (correctness NFA.toDFA_correct, the subset construction) then yields a DFA, giving isRegular_of_is_RG.

DFA → grammar. RG_of_DFA reads the DFA directly as a right-regular grammar: states become nonterminals, each transition M.step q a becomes a rule q → a (M.step q a), and each accepting state q gets q → ε. The invariant RG_of_DFA_derives_inv shows every sentential form reachable from q is map terminal w ++ [nt (M.evalFrom q w)] or a terminal word ending in an accepting state, so RG_of_DFA_language gives RG_language (RG_of_DFA M) = M.accepts, hence is_RG_of_isRegular. The two directions combine into is_RG_iff_isRegular / RG_eq_DFA.

Left ⇔ right. RG_of_LG / LG_of_RG reverse each rule’s output (A → Ba ↦ A → aB). A single transformation step on one grammar is a step on the reversed sentential form of the other (RG_transforms_reverse_of_LG_transforms and its converse), so by induction on the derivation LG_language g = (RG_language (RG_of_LG g))ᴿ (LG_language_eq_RG_language_reverse). Since the regular languages are closed under reversal (Mathlib’s Language.isRegular_reverse_iff), is_LG_iff_is_RG and LG_eq_RG follow.

Keywords / also known as

regular grammars equal finite automata, regular languages DFA equivalence, right-regular grammar to DFA, left-regular equals right-regular, Chomsky type-3 languages, Kleene regular languages, NFA DFA subset construction.

Formalized in Lean 4 with Mathlib, in Langlib.