Left-Regular (Type-3) Grammar Definitions

This file defines left-regular grammars as a restricted variant of the unrestricted (Type-0) grammar framework. A left-regular grammar is a variant of the Type-3 class in the Chomsky hierarchy, generating exactly the regular languages.

Grammar restriction

A left-regular grammar restricts every production rule to one of three forms:

• A → B a (a nonterminal followed by a terminal)
• A → a (a single terminal)
• A → ε (the empty string)

where A, B are nonterminals and a is a terminal symbol.

Main declarations

• LG_rule — A production rule in a left-regular grammar.
• LG_grammar — A left-regular grammar.
• LG_transforms — One-step derivation in a left-regular grammar.
• LG_derives — Reflexive-transitive closure of LG_transforms.
• LG_language — The language generated by a left-regular grammar.
• is_LG — A language is left-regular if it is generated by some left-regular grammar.

References

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

inductive LG_rule (T N : Type) : Type

A production rule in a left-regular grammar.

• cons A a B represents the rule A → B a.
• single A a represents the rule A → a.
• epsilon A represents the rule A → ε.

• cons {T N : Type} : N → T → N → LG_rule T N
• single {T N : Type} : N → T → LG_rule T N
• epsilon {T N : Type} : N → LG_rule T N

def instDecidableEqLG_rule.decEq {T✝ N✝ : Type} [DecidableEq T✝] [DecidableEq N✝] (x✝ x✝¹ : LG_rule T✝ N✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• instDecidableEqLG_rule.decEq (LG_rule.cons a a_1 a_2) (LG_rule.single a_3 a_4) = isFalse ⋯
• instDecidableEqLG_rule.decEq (LG_rule.cons a a_1 a_2) (LG_rule.epsilon a_3) = isFalse ⋯
• instDecidableEqLG_rule.decEq (LG_rule.single a a_1) (LG_rule.cons a_2 a_3 a_4) = isFalse ⋯
• instDecidableEqLG_rule.decEq (LG_rule.single a a_1) (LG_rule.single b b_1) = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯
• instDecidableEqLG_rule.decEq (LG_rule.single a a_1) (LG_rule.epsilon a_2) = isFalse ⋯
• instDecidableEqLG_rule.decEq (LG_rule.epsilon a) (LG_rule.cons a_1 a_2 a_3) = isFalse ⋯
• instDecidableEqLG_rule.decEq (LG_rule.epsilon a) (LG_rule.single a_1 a_2) = isFalse ⋯
• instDecidableEqLG_rule.decEq (LG_rule.epsilon a) (LG_rule.epsilon b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

instance instDecidableEqLG_rule {T✝ N✝ : Type} [DecidableEq T✝] [DecidableEq N✝] : DecidableEq (LG_rule T✝ N✝)

Equations

• instDecidableEqLG_rule = instDecidableEqLG_rule.decEq

structure LG_grammar (T : Type) : Type 1

A left-regular (Type-3) grammar over terminal alphabet T.

This is a variant of the most restricted class in the Chomsky hierarchy. Every production has the form A → Ba, A → a, or A → ε.

• nt : Type

  Type of nonterminals

• initial : self.nt

  Start symbol

• rules : List (LG_rule T self.nt)

  Production rules

def LG_rule.lhs {T N : Type} : LG_rule T N → N

Extract the left-hand-side nonterminal from a left-regular rule.

Equations

• (LG_rule.cons A a a_1).lhs = A
• (LG_rule.single A a).lhs = A
• (LG_rule.epsilon A).lhs = A

def LG_rule.output {T N : Type} : LG_rule T N → List (symbol T N)

Convert an LG rule to its output as a list of symbols.

• A → Ba outputs [B, a]
• A → a outputs [a]
• A → ε outputs []

Equations

• (LG_rule.cons A a a_1).output = [symbol.nonterminal a_1, symbol.terminal a]
• (LG_rule.single A a).output = [symbol.terminal a]
• (LG_rule.epsilon A).output = []

def LG_transforms {T : Type} (g : LG_grammar T) (w₁ w₂ : List (symbol T g.nt)) : Prop

One step of left-regular grammar derivation.

Rewrites a nonterminal A in context u ++ [A] ++ v according to a rule.

Equations

• LG_transforms g w₁ w₂ = ∃ r ∈ g.rules, ∃ (u : List (symbol T g.nt)) (v : List (symbol T g.nt)), w₁ = u ++ [symbol.nonterminal r.lhs] ++ v ∧ w₂ = u ++ r.output ++ v

def LG_derives {T : Type} (g : LG_grammar T) : List (symbol T g.nt) → List (symbol T g.nt) → Prop

Reflexive-transitive closure of LG_transforms.

Equations

• LG_derives g = Relation.ReflTransGen (LG_transforms g)

def LG_generates {T : Type} (g : LG_grammar T) (w : List T) : Prop

A word (list of terminals) is generated by a left-regular grammar.

Equations

• LG_generates g w = LG_derives g [symbol.nonterminal g.initial] (List.map symbol.terminal w)

def LG_language {T : Type} (g : LG_grammar T) : Language T

The language generated by a left-regular grammar.

Equations

• LG_language g = setOf (LG_generates g)

def is_LG {T : Type} (L : Language T) : Prop

A language is left-regular if it is generated by some left-regular grammar.

Equations

• is_LG L = ∃ (g : LG_grammar T), LG_language g = L

def LG {T : Type} : Set (Language T)

The class of left-regular languages.

Equations

• LG = setOf is_LG

theorem LG_deri_self {T : Type} (g : LG_grammar T) {w : List (symbol T g.nt)} : LG_derives g w w

theorem LG_deri_of_tran {T : Type} {g : LG_grammar T} {u v : List (symbol T g.nt)} (h : LG_transforms g u v) : LG_derives g u v

theorem LG_deri_of_deri_tran {T : Type} {g : LG_grammar T} {u v w : List (symbol T g.nt)} (huv : LG_derives g u v) (hvw : LG_transforms g v w) : LG_derives g u w

theorem LG_deri_of_deri_deri {T : Type} {g : LG_grammar T} {u v w : List (symbol T g.nt)} (huv : LG_derives g u v) (hvw : LG_derives g v w) : LG_derives g u w