Equivalence of Left-Regular and Right-Regular Grammars

This file proves that the class of languages generated by left-regular grammars coincides with the class of languages generated by right-regular grammars, i.e., both define exactly the regular languages.

Proof strategy

The key observation is that reversing the output of each rule converts a left-regular grammar into a right-regular grammar (and vice versa), and a derivation step in one corresponds to a derivation step on the reversed sentential form in the other.

Concretely, if g is a left-regular grammar, we construct a right-regular grammar RG_of_LG g such that LG_language g = (RG_language (RG_of_LG g)).reverse. Since the class of right-regular languages is closed under reversal (via Mathlib's Language.isRegular_reverse_iff and is_RG_iff_isRegular), this gives is_LG L → is_RG L. The converse direction is symmetric.

Main results

• is_LG_iff_is_RG — A language is left-regular iff it is right-regular.
• LG_eq_RG — The class of left-regular languages equals the class of right-regular languages.

References

• Hopcroft, Motwani, Ullman. Introduction to Automata Theory, Languages, and Computation, 3rd ed. Section 3.3.

def RG_rule_of_LG_rule {T N : Type} : LG_rule T N → RG_rule T N

Convert a left-regular rule to a right-regular rule by reversing the output.

• A → Ba becomes A → aB
• A → a stays A → a
• A → ε stays A → ε

Equations

• RG_rule_of_LG_rule (LG_rule.cons A a B) = RG_rule.cons A a B
• RG_rule_of_LG_rule (LG_rule.single A a) = RG_rule.single A a
• RG_rule_of_LG_rule (LG_rule.epsilon A) = RG_rule.epsilon A

def LG_rule_of_RG_rule {T N : Type} : RG_rule T N → LG_rule T N

Convert a right-regular rule to a left-regular rule by reversing the output.

• A → aB becomes A → Ba
• A → a stays A → a
• A → ε stays A → ε

Equations

• LG_rule_of_RG_rule (RG_rule.cons A a B) = LG_rule.cons A a B
• LG_rule_of_RG_rule (RG_rule.single A a) = LG_rule.single A a
• LG_rule_of_RG_rule (RG_rule.epsilon A) = LG_rule.epsilon A

def RG_of_LG {T : Type} (g : LG_grammar T) : RG_grammar T

Convert a left-regular grammar to a right-regular grammar.

Equations

• RG_of_LG g = { nt := g.nt, initial := g.initial, rules := List.map RG_rule_of_LG_rule g.rules }

def LG_of_RG {T : Type} (g : RG_grammar T) : LG_grammar T

Convert a right-regular grammar to a left-regular grammar.

Equations

• LG_of_RG g = { nt := g.nt, initial := g.initial, rules := List.map LG_rule_of_RG_rule g.rules }

theorem RG_rule_of_LG_rule_lhs {T N : Type} (r : LG_rule T N) : (RG_rule_of_LG_rule r).lhs = r.lhs

theorem LG_rule_of_RG_rule_lhs {T N : Type} (r : RG_rule T N) : (LG_rule_of_RG_rule r).lhs = r.lhs

theorem RG_rule_of_LG_rule_output {T N : Type} (r : LG_rule T N) : (RG_rule_of_LG_rule r).output = r.output.reverse

theorem LG_rule_of_RG_rule_output {T N : Type} (r : RG_rule T N) : (LG_rule_of_RG_rule r).output = r.output.reverse

theorem RG_transforms_reverse_of_LG_transforms {T : Type} {g : LG_grammar T} {w₁ w₂ : List (symbol T g.nt)} (h : LG_transforms g w₁ w₂) : RG_transforms (RG_of_LG g) w₁.reverse w₂.reverse

An LG transformation step corresponds to an RG transformation step on the reversed sentential form.

theorem LG_transforms_of_RG_transforms_reverse {T : Type} {g : LG_grammar T} {w₁ w₂ : List (symbol T g.nt)} (h : RG_transforms (RG_of_LG g) w₁ w₂) : LG_transforms g w₁.reverse w₂.reverse

An RG transformation step on RG_of_LG g corresponds to an LG transformation step on the reversed sentential form.

theorem RG_derives_reverse_of_LG_derives {T : Type} {g : LG_grammar T} {w₁ w₂ : List (symbol T g.nt)} (h : LG_derives g w₁ w₂) : RG_derives (RG_of_LG g) w₁.reverse w₂.reverse

LG derivation corresponds to RG derivation on reversed sentential forms.

theorem LG_derives_of_RG_derives_reverse {T : Type} {g : LG_grammar T} {w₁ w₂ : List (symbol T g.nt)} (h : RG_derives (RG_of_LG g) w₁ w₂) : LG_derives g w₁.reverse w₂.reverse

RG derivation on RG_of_LG g corresponds to LG derivation on reversed sentential forms.

theorem LG_generates_iff_RG_generates_reverse {T : Type} (g : LG_grammar T) (w : List T) : LG_generates g w ↔ RG_generates (RG_of_LG g) w.reverse

theorem LG_language_eq_RG_language_reverse {T : Type} (g : LG_grammar T) : LG_language g = (RG_language (RG_of_LG g)).reverse

theorem LG_transforms_reverse_of_RG_transforms {T : Type} {g : RG_grammar T} {w₁ w₂ : List (symbol T g.nt)} (h : RG_transforms g w₁ w₂) : LG_transforms (LG_of_RG g) w₁.reverse w₂.reverse

An RG transformation step corresponds to an LG transformation step on the reversed sentential form.

theorem RG_transforms_of_LG_transforms_reverse {T : Type} {g : RG_grammar T} {w₁ w₂ : List (symbol T g.nt)} (h : LG_transforms (LG_of_RG g) w₁ w₂) : RG_transforms g w₁.reverse w₂.reverse

theorem LG_derives_reverse_of_RG_derives {T : Type} {g : RG_grammar T} {w₁ w₂ : List (symbol T g.nt)} (h : RG_derives g w₁ w₂) : LG_derives (LG_of_RG g) w₁.reverse w₂.reverse

theorem RG_derives_of_LG_derives_reverse {T : Type} {g : RG_grammar T} {w₁ w₂ : List (symbol T g.nt)} (h : LG_derives (LG_of_RG g) w₁ w₂) : RG_derives g w₁.reverse w₂.reverse

theorem RG_generates_iff_LG_generates_reverse {T : Type} (g : RG_grammar T) (w : List T) : RG_generates g w ↔ LG_generates (LG_of_RG g) w.reverse

theorem RG_language_eq_LG_language_reverse {T : Type} (g : RG_grammar T) : RG_language g = (LG_language (LG_of_RG g)).reverse

theorem is_RG_of_is_LG {T : Type} [Fintype T] {L : Language T} (h : is_LG L) : is_RG L

Every left-regular language is right-regular.

theorem is_LG_of_is_RG {T : Type} [Fintype T] {L : Language T} (h : is_RG L) : is_LG L

Every right-regular language is left-regular.

theorem is_LG_iff_is_RG {T : Type} [Fintype T] {L : Language T} : is_LG L ↔ is_RG L

A language is left-regular if and only if it is right-regular.

theorem LG_eq_RG {T : Type} [Fintype T] : LG = RG

The class of left-regular languages equals the class of right-regular languages.