Right-regular and left-regular grammars

Statement

The regular (Chomsky type-3) languages are exactly those generated by right-regular grammars — every rule has the form A → aB, A → a, or A → ε (a terminal optionally followed by a single nonterminal on the right). The mirror notion, left-regular grammars (A → Ba, A → a, A → ε), generates the same class of languages. Langlib defines both and proves their equivalence, and ties the right-regular grammars to deterministic finite automata (see regular grammars = DFA languages).

In Lean

Definitions:

  • RG_grammar / RG_rule — right-regular grammars and their rules.
  • LG_grammar / LG_rule — left-regular grammars and their rules.
  • is_RG — a language is regular iff generated by some right-regular grammar; is_LG is the left-regular analogue.

Equivalence of the two grammar forms:

  • is_LG_iff_is_RG — a language is left-regular iff it is right-regular.
  • LG_eq_RG — the left-regular and right-regular language classes are equal.

Connection to finite automata: is_RG_iff_isRegular and RG_eq_DFA — right-regular grammars generate exactly the DFA-recognizable (Mathlib-regular) languages.

Proof idea

RG_of_LG turns a left-regular grammar into a right-regular one (and LG_of_RG back) by reversing each rule’s output: A → Ba becomes A → aB, while A → a and A → ε are unchanged. One transformation step on a grammar is exactly one step on the reversed sentential form of its converted grammar (RG_transforms_reverse_of_LG_transforms and its inverse), so induction on the derivation gives LG_language g = (RG_language (RG_of_LG g))ᴿ (LG_language_eq_RG_language_reverse). Because the regular languages are closed under reversal (Mathlib’s Language.isRegular_reverse_iff, via is_RG_iff_isRegular), a left-regular L is right-regular and vice versa — is_LG_iff_is_RG, hence LG_eq_RG. The tie to automata is is_RG_iff_isRegular, proved by the NFA/DFA constructions described under regular grammars = DFA languages.

Keywords / also known as

right-regular grammar, left-regular grammar, right-linear and left-linear grammars, type-3 grammars, regular grammar normal form, left-regular equals right-regular, regular languages grammar characterization, Lean formalization.

Formalized in Lean 4 with Mathlib, in Langlib.