Chomsky Normal Form Grammars

This file contains the definition of a chomsky normal form grammar, which is a context-free grammar with syntactic restriction on the rules. Each rule either rewrites to a single terminal symbol or a pair of nonterminals.

Main definitions

• ChomskyNormalFormGrammar: A chomsky normal form grammar.
• ChomskyNormalFormGrammar.toCFG: simple translation to a context-free grammar.

Main theorems

• Language.toCFG_correct: g.toCFG generates the same language a a context-free grammar g.

inductive ChomskyNormalFormRule (T : Type uT) (N : Type uN) : Type (max uN uT)

Rule that rewrites a single nonterminal to a single terminal or a pair of nonterminals.

• leaf {T : Type uT} {N : Type uN} (n : N) (t : T) : ChomskyNormalFormRule T N

  First kind of rule, rewriting a nonterminal n to a single terminal t.

• node {T : Type uT} {N : Type uN} (n l r : N) : ChomskyNormalFormRule T N

  Second kind of rule, rewriting a nonterminal n to a pair of nonterminal lr.

def instDecidableEqChomskyNormalFormRule.decEq {T✝ : Type u_1} {N✝ : Type u_2} [DecidableEq T✝] [DecidableEq N✝] (x✝ x✝¹ : ChomskyNormalFormRule T✝ N✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• instDecidableEqChomskyNormalFormRule.decEq (ChomskyNormalFormRule.leaf n t) (ChomskyNormalFormRule.node n_1 l r) = isFalse ⋯
• instDecidableEqChomskyNormalFormRule.decEq (ChomskyNormalFormRule.node n l r) (ChomskyNormalFormRule.leaf n_1 t) = isFalse ⋯

@[implicit_reducible]

instance instDecidableEqChomskyNormalFormRule {T✝ : Type u_1} {N✝ : Type u_2} [DecidableEq T✝] [DecidableEq N✝] : DecidableEq (ChomskyNormalFormRule T✝ N✝)

Equations

• instDecidableEqChomskyNormalFormRule = instDecidableEqChomskyNormalFormRule.decEq

structure ChomskyNormalFormGrammar (T : Type uT) : Type (max (uN + 1) uT)

Chomsky normal form grammar that generates words over the alphabet T (a type of terminals).

• NT : Type uN

  Type of nonterminals.

• initial : self.NT

  Initial nonterminal.

• rules : Finset (ChomskyNormalFormRule T self.NT)

  Rewrite rules.

def ChomskyNormalFormRule.input {T : Type uT} {N : Type uN} (r : ChomskyNormalFormRule T N) : N

The input of a CNF rule, similar to ContextFreeRule.input

Equations

• (ChomskyNormalFormRule.leaf n t).input = n
• (ChomskyNormalFormRule.node n l r_2).input = n

def ChomskyNormalFormRule.output {T : Type uT} {N : Type uN} (r : ChomskyNormalFormRule T N) : List (Symbol T N)

The output of a CNF rule, similar to ContextFreeRule.output

Equations

• (ChomskyNormalFormRule.leaf n t).output = [Symbol.terminal t]
• (ChomskyNormalFormRule.node n l r_2).output = [Symbol.nonterminal l, Symbol.nonterminal r_2]

inductive ChomskyNormalFormRule.Rewrites {T : Type uT} {N : Type uN} : ChomskyNormalFormRule T N → List (Symbol T N) → List (Symbol T N) → Prop

Inductive definition of a single application of a given cnf rule r to a string u; r.Rewrites u v means that the r sends u to v (there may be multiple such strings v).

• head_leaf {T : Type uT} {N : Type uN} (n : N) (t : T) (s : List (Symbol T N)) : (leaf n t).Rewrites (Symbol.nonterminal n :: s) (Symbol.terminal t :: s)

  The replacement is at the start of the remaining string and the rule is a leaf rule.

• head_node {T : Type uT} {N : Type uN} (nᵢ n₁ n₂ : N) (s : List (Symbol T N)) : (node nᵢ n₁ n₂).Rewrites (Symbol.nonterminal nᵢ :: s) (Symbol.nonterminal n₁ :: Symbol.nonterminal n₂ :: s)

  The replacement is at the start of the remaining string and the rule is a node rule.

• cons {T : Type uT} {N : Type uN} (r : ChomskyNormalFormRule T N) (s : Symbol T N) {u₁ u₂ : List (Symbol T N)} (hru : r.Rewrites u₁ u₂) : r.Rewrites (s :: u₁) (s :: u₂)

  The replacement is at the start of the remaining string.

theorem ChomskyNormalFormRule.Rewrites.exists_parts {T : Type uT} {N : Type uN} {r : ChomskyNormalFormRule T N} {u v : List (Symbol T N)} (hr : r.Rewrites u v) : ∃ (p : List (Symbol T N)) (q : List (Symbol T N)), u = p ++ [Symbol.nonterminal r.input] ++ q ∧ v = p ++ r.output ++ q

theorem ChomskyNormalFormRule.Rewrites.input_output {T : Type uT} {N : Type uN} {r : ChomskyNormalFormRule T N} : r.Rewrites [Symbol.nonterminal r.input] r.output

theorem ChomskyNormalFormRule.rewrites_of_exists_parts {T : Type uT} {N : Type uN} (r : ChomskyNormalFormRule T N) (p q : List (Symbol T N)) : r.Rewrites (p ++ [Symbol.nonterminal r.input] ++ q) (p ++ r.output ++ q)

theorem ChomskyNormalFormRule.rewrites_iff {T : Type uT} {N : Type uN} {r : ChomskyNormalFormRule T N} (u v : List (Symbol T N)) : r.Rewrites u v ↔ ∃ (p : List (Symbol T N)) (q : List (Symbol T N)), u = p ++ [Symbol.nonterminal r.input] ++ q ∧ v = p ++ r.output ++ q

Rule r rewrites string u to string v iff they share both a prefix p and postfix q such that the remaining middle part of u is the input of r and the remaining middle part of v is the output of r.

theorem ChomskyNormalFormRule.Rewrites.append_left {T : Type uT} {N : Type uN} {r : ChomskyNormalFormRule T N} {u v : List (Symbol T N)} (huv : r.Rewrites u v) (p : List (Symbol T N)) : r.Rewrites (p ++ u) (p ++ v)

Add extra prefix to cnf rewriting.

theorem ChomskyNormalFormRule.Rewrites.append_right {T : Type uT} {N : Type uN} {r : ChomskyNormalFormRule T N} {u v : List (Symbol T N)} (huv : r.Rewrites u v) (p : List (Symbol T N)) : r.Rewrites (u ++ p) (v ++ p)

Add extra postfix to cnf rewriting.

def ChomskyNormalFormRule.toCFGRule {T : Type uT} {N : Type uN} (r : ChomskyNormalFormRule T N) : ContextFreeRule T N

Translation of ChomskyNormalFormRule to ContextFreeRule

Equations

• (ChomskyNormalFormRule.leaf n t).toCFGRule = { input := n, output := [Symbol.terminal t] }
• (ChomskyNormalFormRule.node n l r_2).toCFGRule = { input := n, output := [Symbol.nonterminal l, Symbol.nonterminal r_2] }

theorem ChomskyNormalFormRule.Rewrites.toCFGRule_match {T : Type uT} {N : Type uN} {u v : List (Symbol T N)} {r : ChomskyNormalFormRule T N} (huv : r.Rewrites u v) : r.toCFGRule.Rewrites u v

theorem ChomskyNormalFormRule.Rewrites.match_toCFGRule {T : Type uT} {N : Type uN} {u v : List (Symbol T N)} {r : ChomskyNormalFormRule T N} (huv : r.toCFGRule.Rewrites u v) : r.Rewrites u v

def ChomskyNormalFormGrammar.Produces {T : Type uT} (g : ChomskyNormalFormGrammar T) (u v : List (Symbol T g.NT)) : Prop

Given a cnf grammar g and strings u and v g.Produces u v means that one step of a cnf transformation by a rule from g sends u to v.

Equations

• g.Produces u v = ∃ r ∈ g.rules, r.Rewrites u v

@[reducible, inline]

abbrev ChomskyNormalFormGrammar.Derives {T : Type uT} (g : ChomskyNormalFormGrammar T) : List (Symbol T g.NT) → List (Symbol T g.NT) → Prop

Given a cnf grammar g and strings u and v g.Derives u v means that g can transform u to v in some number of rewriting steps.

Equations

• g.Derives = Relation.ReflTransGen g.Produces

def ChomskyNormalFormGrammar.Generates {T : Type uT} (g : ChomskyNormalFormGrammar T) (u : List (Symbol T g.NT)) : Prop

Given a cnf grammar g and a string s g.Generates s means that g can transform its initial nonterminal c s in some number of rewriting steps.

Equations

• g.Generates u = g.Derives [Symbol.nonterminal g.initial] u

def ChomskyNormalFormGrammar.language {T : Type uT} (g : ChomskyNormalFormGrammar T) : Language T

The language (set of words) that can be generated by a given cnf grammar g.

Equations

• g.language = {w : List T | g.Generates (List.map Symbol.terminal w)}

@[simp]

theorem ChomskyNormalFormGrammar.mem_language_iff {T : Type uT} (g : ChomskyNormalFormGrammar T) (w : List T) : w ∈ g.language ↔ g.Generates (List.map Symbol.terminal w)

A given word w belongs to the language generated by a given cnf grammar g iff g can derive the word w (wrapped as a string) from the initial nonterminal of g in some number of steps.

theorem ChomskyNormalFormGrammar.Derives.refl {T : Type uT} {g : ChomskyNormalFormGrammar T} (u : List (Symbol T g.NT)) : g.Derives u u

theorem ChomskyNormalFormGrammar.Produces.single {T : Type uT} {g : ChomskyNormalFormGrammar T} {u v : List (Symbol T g.NT)} (hvw : g.Produces u v) : g.Derives u v

theorem ChomskyNormalFormGrammar.Derives.trans {T : Type uT} {g : ChomskyNormalFormGrammar T} {u v w : List (Symbol T g.NT)} (huv : g.Derives u v) (hvw : g.Derives v w) : g.Derives u w

theorem ChomskyNormalFormGrammar.Derives.trans_produces {T : Type uT} {g : ChomskyNormalFormGrammar T} {u v w : List (Symbol T g.NT)} (huv : g.Derives u v) (hvw : g.Produces v w) : g.Derives u w

theorem ChomskyNormalFormGrammar.Produces.trans_derives {T : Type uT} {g : ChomskyNormalFormGrammar T} {u v w : List (Symbol T g.NT)} (huv : g.Produces u v) (hvw : g.Derives v w) : g.Derives u w

theorem ChomskyNormalFormGrammar.Derives.eq_or_head {T : Type uT} {g : ChomskyNormalFormGrammar T} {u w : List (Symbol T g.NT)} (huw : g.Derives u w) : u = w ∨ ∃ (v : List (Symbol T g.NT)), g.Produces u v ∧ g.Derives v w

theorem ChomskyNormalFormGrammar.Derives.eq_or_tail {T : Type uT} {g : ChomskyNormalFormGrammar T} {u w : List (Symbol T g.NT)} (huw : g.Derives u w) : u = w ∨ ∃ (v : List (Symbol T g.NT)), g.Derives u v ∧ g.Produces v w

theorem ChomskyNormalFormGrammar.Produces.append_left {T : Type uT} {g : ChomskyNormalFormGrammar T} {u v : List (Symbol T g.NT)} (huv : g.Produces u v) (p : List (Symbol T g.NT)) : g.Produces (p ++ u) (p ++ v)

Add extra prefix to cnf producing.

theorem ChomskyNormalFormGrammar.Produces.append_right {T : Type uT} {g : ChomskyNormalFormGrammar T} {u v : List (Symbol T g.NT)} (huv : g.Produces u v) (p : List (Symbol T g.NT)) : g.Produces (u ++ p) (v ++ p)

Add extra postfix to cnf producing.

theorem ChomskyNormalFormGrammar.Derives.append_left {T : Type uT} {g : ChomskyNormalFormGrammar T} {u v : List (Symbol T g.NT)} (huv : g.Derives u v) (p : List (Symbol T g.NT)) : g.Derives (p ++ u) (p ++ v)

Add extra prefix to cnf deriving.

theorem ChomskyNormalFormGrammar.Derives.append_right {T : Type uT} {g : ChomskyNormalFormGrammar T} {u v : List (Symbol T g.NT)} (huv : g.Derives u v) (p : List (Symbol T g.NT)) : g.Derives (u ++ p) (v ++ p)

Add extra postfix to cnf deriving.

theorem ChomskyNormalFormGrammar.Derives.head_induction_on {T : Type uT} {g : ChomskyNormalFormGrammar T} {v : List (Symbol T g.NT)} {P : (u : List (Symbol T g.NT)) → g.Derives u v → Prop} {u : List (Symbol T g.NT)} (huv : g.Derives u v) (refl : P v ⋯) (head : ∀ {u w : List (Symbol T g.NT)} (huw : g.Produces u w) (hwv : g.Derives w v), P w hwv → P u ⋯) : P u huv

ChomskyNormalFormGrammar to ContextFreeGrammar translation and related properties

noncomputable def ChomskyNormalFormGrammar.toCFG {T : Type uT} [DecidableEq T] (g : ChomskyNormalFormGrammar T) [DecidableEq g.NT] : ContextFreeGrammar T

Translation of ChomskyNormalFormGrammar to ContextFreeGrammar

Equations

• g.toCFG = { NT := g.NT, initial := g.initial, rules := (List.map ChomskyNormalFormRule.toCFGRule g.rules.toList).toFinset }

theorem ChomskyNormalFormGrammar.Produces.toCFG_match {T : Type uT} [DecidableEq T] {g : ChomskyNormalFormGrammar T} [DecidableEq g.NT] {u v : List (Symbol T g.NT)} (huv : g.Produces u v) : g.toCFG.Produces u v

theorem ChomskyNormalFormGrammar.Derives.toCFG_match {T : Type uT} [DecidableEq T] {g : ChomskyNormalFormGrammar T} [DecidableEq g.NT] {u v : List (Symbol T g.NT)} (huv : g.Derives u v) : g.toCFG.Derives u v

theorem ChomskyNormalFormGrammar.Generates.toCFG_match {T : Type uT} [DecidableEq T] {g : ChomskyNormalFormGrammar T} [DecidableEq g.NT] {u : List (Symbol T g.NT)} (hu : g.Generates u) : g.toCFG.Generates u

theorem ChomskyNormalFormGrammar.Produces.match_toCFG {T : Type uT} [DecidableEq T] {g : ChomskyNormalFormGrammar T} [DecidableEq g.NT] {u v : List (Symbol T g.NT)} (huv : g.toCFG.Produces u v) : g.Produces u v

theorem ChomskyNormalFormGrammar.Derives.match_toCFG {T : Type uT} [DecidableEq T] {g : ChomskyNormalFormGrammar T} [DecidableEq g.NT] {u v : List (Symbol T g.NT)} (huv : g.toCFG.Derives u v) : g.Derives u v

theorem ChomskyNormalFormGrammar.Generates.match_toCFG {T : Type uT} [DecidableEq T] {g : ChomskyNormalFormGrammar T} [DecidableEq g.NT] {u : List (Symbol T g.NT)} (hu : g.toCFG.Generates u) : g.Generates u

theorem ChomskyNormalFormGrammar.toCFG_correct {T : Type uT} [DecidableEq T] {g : ChomskyNormalFormGrammar T} [DecidableEq g.NT] {u : List (Symbol T g.NT)} : g.Generates u ↔ g.toCFG.Generates u

Alternative definition of ChomskyNormalFormGrammar.Derives which allows to use well-founded induction on derivations, by explicitely counting the number of steps of the transformation

inductive ChomskyNormalFormGrammar.DerivesIn {T : Type uT} (g : ChomskyNormalFormGrammar T) : List (Symbol T g.NT) → List (Symbol T g.NT) → ℕ → Prop

Given a context-free grammar g, strings u and v, and number n g.DerivesIn u v n means that g can transform u to v in n rewriting steps.

• refl {T : Type uT} {g : ChomskyNormalFormGrammar T} (w : List (Symbol T g.NT)) : g.DerivesIn w w 0

  0 steps entail no transformation

• tail {T : Type uT} {g : ChomskyNormalFormGrammar T} (u v w : List (Symbol T g.NT)) (n : ℕ) : g.DerivesIn u v n → g.Produces v w → g.DerivesIn u w n.succ

  n + 1 steps, if transforms u to v in n steps, and v to w in 1 step

theorem ChomskyNormalFormGrammar.derives_iff_derivesIn {T : Type uT} (g : ChomskyNormalFormGrammar T) (v w : List (Symbol T g.NT)) : g.Derives v w ↔ ∃ (n : ℕ), g.DerivesIn v w n

theorem ChomskyNormalFormGrammar.mem_language_iff_derivesIn {T : Type uT} (g : ChomskyNormalFormGrammar T) (w : List T) : w ∈ g.language ↔ ∃ (n : ℕ), g.DerivesIn [Symbol.nonterminal g.initial] (List.map Symbol.terminal w) n

theorem ChomskyNormalFormGrammar.DerivesIn.zero_steps {T : Type uT} {g : ChomskyNormalFormGrammar T} (w : List (Symbol T g.NT)) : g.DerivesIn w w 0

theorem ChomskyNormalFormGrammar.DerivesIn.zero_steps_eq {T : Type uT} {g : ChomskyNormalFormGrammar T} {u v : List (Symbol T g.NT)} (huv : g.DerivesIn u v 0) : u = v

theorem ChomskyNormalFormGrammar.Produces.single_step {T : Type uT} {g : ChomskyNormalFormGrammar T} {v w : List (Symbol T g.NT)} (hvw : g.Produces v w) : g.DerivesIn v w 1

theorem ChomskyNormalFormGrammar.DerivesIn.trans_produces {T : Type uT} {g : ChomskyNormalFormGrammar T} {n : ℕ} {u v w : List (Symbol T g.NT)} (huv : g.DerivesIn u v n) (hvw : g.Produces v w) : g.DerivesIn u w n.succ

theorem ChomskyNormalFormGrammar.DerivesIn.trans {T : Type uT} {g : ChomskyNormalFormGrammar T} {n : ℕ} {u v w : List (Symbol T g.NT)} {m : ℕ} (huv : g.DerivesIn u v n) (hvw : g.DerivesIn v w m) : g.DerivesIn u w (n + m)

theorem ChomskyNormalFormGrammar.Produces.trans_derivesIn {T : Type uT} {g : ChomskyNormalFormGrammar T} {n : ℕ} {u v w : List (Symbol T g.NT)} (huv : g.Produces u v) (hvw : g.DerivesIn v w n) : g.DerivesIn u w n.succ

theorem ChomskyNormalFormGrammar.DerivesIn.tail_of_succ {T : Type uT} {g : ChomskyNormalFormGrammar T} {n : ℕ} {u w : List (Symbol T g.NT)} (huw : g.DerivesIn u w n.succ) : ∃ (v : List (Symbol T g.NT)), g.DerivesIn u v n ∧ g.Produces v w

theorem ChomskyNormalFormGrammar.DerivesIn.head_of_succ {T : Type uT} {g : ChomskyNormalFormGrammar T} {n : ℕ} {u w : List (Symbol T g.NT)} (huw : g.DerivesIn u w n.succ) : ∃ (v : List (Symbol T g.NT)), g.Produces u v ∧ g.DerivesIn v w n

theorem ChomskyNormalFormGrammar.DerivesIn.append_left {T : Type uT} {g : ChomskyNormalFormGrammar T} {n : ℕ} {v w : List (Symbol T g.NT)} (hvw : g.DerivesIn v w n) (p : List (Symbol T g.NT)) : g.DerivesIn (p ++ v) (p ++ w) n

Add extra prefix to context-free deriving (number of steps unchanged).

theorem ChomskyNormalFormGrammar.DerivesIn.append_right {T : Type uT} {g : ChomskyNormalFormGrammar T} {n : ℕ} {v w : List (Symbol T g.NT)} (hvw : g.DerivesIn v w n) (p : List (Symbol T g.NT)) : g.DerivesIn (v ++ p) (w ++ p) n

Add extra postfix to context-free deriving (number of steps unchanged).

theorem ChomskyNormalFormGrammar.DerivesIn.append_split {T : Type uT} {g : ChomskyNormalFormGrammar T} {p q w : List (Symbol T g.NT)} {n : ℕ} (hpqw : g.DerivesIn (p ++ q) w n) : ∃ (x : List (Symbol T g.NT)) (y : List (Symbol T g.NT)) (m₁ : ℕ) (m₂ : ℕ), w = x ++ y ∧ g.DerivesIn p x m₁ ∧ g.DerivesIn q y m₂ ∧ n = m₁ + m₂

theorem ChomskyNormalFormGrammar.DerivesIn.three_split {T : Type uT} {g : ChomskyNormalFormGrammar T} {p q r w : List (Symbol T g.NT)} {n : ℕ} (hg : g.DerivesIn (p ++ q ++ r) w n) : ∃ (x : List (Symbol T g.NT)) (y : List (Symbol T g.NT)) (z : List (Symbol T g.NT)) (m₁ : ℕ) (m₂ : ℕ) (m₃ : ℕ), w = x ++ y ++ z ∧ g.DerivesIn p x m₁ ∧ g.DerivesIn q y m₂ ∧ g.DerivesIn r z m₃ ∧ n = m₁ + m₂ + m₃

theorem ChomskyNormalFormGrammar.DerivesIn.head_induction_on {T : Type uT} {g : ChomskyNormalFormGrammar T} {n : ℕ} {b : List (Symbol T g.NT)} {P : (n : ℕ) → (a : List (Symbol T g.NT)) → g.DerivesIn a b n → Prop} (refl : P 0 b ⋯) (head : ∀ {n : ℕ} {a c : List (Symbol T g.NT)} (hac : g.Produces a c) (hcb : g.DerivesIn c b n), P n c hcb → P n.succ a ⋯) {a : List (Symbol T g.NT)} (hab : g.DerivesIn a b n) : P n a hab