Translation to Chomsky Normal Form

This file assembles the elimination passes into a correctness proof for the full CNF translation.

Main declarations

• toCFG_correct
• toCNF_correct

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ᵢ n₁ n₂).toCFGRule = { input := nᵢ, output := [Symbol.nonterminal n₁, Symbol.nonterminal n₂] }

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

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

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

Translation of ContextFreeGrammar to ChomskyNormalFormGrammar, composing the individual translation passes

Equations

• g.toCNF = g.eliminateEmpty.eliminateUnitRules.restrictTerminals.restrictLength

theorem ContextFreeGrammar.newTerminalRules_terminal_output {T : Type} {g : ContextFreeGrammar T} {r : ContextFreeRule T g.NT} (r' : ContextFreeRule T (g.NT ⊕ T)) : r' ∈ newTerminalRules r → ∃ (t : T), r'.output = [Symbol.terminal t]

theorem ContextFreeGrammar.restrictTerminals_nonUnit_output {T : Type} {g : ContextFreeGrammar T} [DecidableEq T] [DecidableEq g.NT] (hrₒ : ∀ r ∈ g.rules, NonUnit r.output) (r' : ContextFreeRule T g.restrictTerminals.NT) : r' ∈ g.restrictTerminals.rules → NonUnit r'.output

theorem ContextFreeGrammar.restrictTerminals_not_empty_output {T : Type} {g : ContextFreeGrammar T} [DecidableEq T] [DecidableEq g.NT] (hne : ∀ r ∈ g.rules, r.output ≠ []) (r' : ContextFreeRule T g.restrictTerminals.NT) : r' ∈ g.restrictTerminals.rules → r'.output ≠ []

theorem ContextFreeGrammar.restrictTerminals_terminal_or_nonterminals {T : Type} {g : ContextFreeGrammar T} [DecidableEq T] [DecidableEq g.NT] (r : ContextFreeRule T g.restrictTerminals.NT) : r ∈ g.restrictTerminals.rules → (∃ (t : T), r.output = [Symbol.terminal t]) ∨ ∀ s ∈ r.output, ∃ (nt : g.restrictTerminals.NT), s = Symbol.nonterminal nt

theorem ContextFreeGrammar.eliminateUnitRules_not_empty_output {T : Type} {g : ContextFreeGrammar T} [DecidableEq T] [DecidableEq g.NT] (hne : ∀ r ∈ g.rules, r.output ≠ []) (r' : ContextFreeRule T g.eliminateUnitRules.NT) : r' ∈ g.eliminateUnitRules.rules → r'.output ≠ []

theorem ContextFreeGrammar.eliminateEmpty_not_empty_output {T : Type} {g : ContextFreeGrammar T} [DecidableEq T] [DecidableEq g.NT] (r : ContextFreeRule T g.eliminateEmpty.NT) : r ∈ g.eliminateEmpty.rules → r.output ≠ []

theorem ContextFreeGrammar.eliminateUnitRules_output_nonUnit {T : Type} {g : ContextFreeGrammar T} [DecidableEq T] [DecidableEq g.NT] (r : ContextFreeRule T g.eliminateUnitRules.NT) : r ∈ g.eliminateUnitRules.rules → NonUnit r.output

theorem ContextFreeGrammar.toCNF_correct {T : Type} {g : ContextFreeGrammar T} [DecidableEq T] [DecidableEq g.NT] : g.language \ {[]} = g.toCNF.language