Chomsky Normal Form Translation

This file contains the algorithm to translate a ContextFreeGrammar. to a ChomskyNormalFormGrammar by using the algorithms ContextFreeGrammar.eliminateEmpty removing rules with an empty right-hand side, ContextFreeGrammar.eliminateUnitRules removing rules with a single nonterminal right-hand side, ContextFreeGrammar.restrictTerminals restricting all terminals to only occur as the single symbol of a rule's right-hand side, and ContextFreeGrammar.restrictLength translating ContextFreeRules with multiple nonterminals to ChomskyNormalFormRules with only two nonterminals on the right-hand side.

Main definitions

• ContextFreeGrammar.toCNF: Transforms a context-free grammar to a chomsky normal form grammar

Main theorems

• ContextFreeGrammar.toCNF_correct: The transformed grammar's language coincides with the original language (except for the empty string)

References

• [John E. Hopcroft, Rajeev Motwani, and Jeffrey D. Ullman. 2006. Introduction to Automata Theory, Languages, and Computation (3rd Edition). Addison-Wesley Longman Publishing Co., Inc., USA.] [Hopcroft et al. 2006]

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