Chomsky Normal Form Grammars

This file defines Chomsky-normal-form grammars and their derivation semantics.

Main declarations

• rewrites_iff
• mem_language_iff
• Derives.head_induction_on

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 ⋯

@[instance_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)

• 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 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 to 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