Right-Regular (Type-3) Grammar Definitions

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

Grammar restriction

An unrestricted grammar allows rules of the form α A β → γ where α, β, γ are arbitrary strings of terminals and nonterminals. A right-regular grammar restricts every production rule to one of three forms:

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

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

Main declarations

• RG_rule — A production rule in a right-regular grammar.
• RG_grammar — A right-regular grammar.
• RG_transforms — One-step derivation in a right-regular grammar.
• RG_derives — Reflexive-transitive closure of RG_transforms.
• RG_language — The language generated by a right-regular grammar.

References

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

inductive RG_rule (T N : Type) : Type

A production rule in a right-regular grammar.

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

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

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

Equations

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

instance instDecidableEqRG_rule {T✝ N✝ : Type} [DecidableEq T✝] [DecidableEq N✝] : DecidableEq (RG_rule T✝ N✝)

Equations

• instDecidableEqRG_rule = instDecidableEqRG_rule.decEq

structure RG_grammar (T : Type) : Type 1

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

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

• nt : Type

  Type of nonterminals

• initial : self.nt

  Start symbol

• rules : List (RG_rule T self.nt)

  Production rules

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

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

Equations

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

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

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

Equations

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

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

One step of right-regular grammar derivation.

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

Equations

• RG_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 RG_derives {T : Type} (g : RG_grammar T) : List (symbol T g.nt) → List (symbol T g.nt) → Prop

Reflexive-transitive closure of RG_transforms.

Equations

• RG_derives g = Relation.ReflTransGen (RG_transforms g)

def RG_generates {T : Type} (g : RG_grammar T) (w : List T) : Prop

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

Equations

• RG_generates g w = RG_derives g [symbol.nonterminal g.initial] (List.map symbol.terminal w)

def RG_language {T : Type} (g : RG_grammar T) : Language T

The language generated by a right-regular grammar.

Equations

• RG_language g = setOf (RG_generates g)

theorem RG_deri_self {T : Type} (g : RG_grammar T) {w : List (symbol T g.nt)} : RG_derives g w w

theorem RG_deri_of_tran {T : Type} {g : RG_grammar T} {u v : List (symbol T g.nt)} (h : RG_transforms g u v) : RG_derives g u v

theorem RG_deri_of_deri_tran {T : Type} {g : RG_grammar T} {u v w : List (symbol T g.nt)} (huv : RG_derives g u v) (hvw : RG_transforms g v w) : RG_derives g u w

theorem RG_deri_of_deri_deri {T : Type} {g : RG_grammar T} {u v w : List (symbol T g.nt)} (huv : RG_derives g u v) (hvw : RG_derives g v w) : RG_derives g u w