Length Restriction

This file contains the algorithm to translate a ContextFreeGrammar.Wellformed grammar to a chomsky normal form grammar while preserving the language of the original grammar. A context-free grammar is wellformed if it has rules that rewrite either to a single terminal or multiple nonterminals.

Main definitions

• ContextFreeGrammar.restrictLength: Transforms a context-free grammar to a chomsky normal form grammar by replacing rules that rewrite to multiple nonterminals to a set of cascading rules.

Main theorems

• ContextFreeGrammar.restrictLength_correct: The transformed grammar's language coincides with the original

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]

inductive ContextFreeRule.Wellformed {T : Type uT} {N : Type u_1} : ContextFreeRule T N → Prop

Wellformed r holds if the rule's output is not a single nonterminal (UnitRule), not empty, or if the output is more than one symbol, it is only nonterminals

• terminal {T : Type uT} {N : Type u_1} {n : N} (t : T) : { input := n, output := [Symbol.terminal t] }.Wellformed

  Rule rewriting to a single terminal is wellformed

• nonterminals {T : Type uT} {N : Type u_1} {n : N} (u : List (Symbol T N)) (h2 : 2 ≤ u.length) (hu : ∀ s ∈ u, match s with | Symbol.nonterminal n => True | x => False) : { input := n, output := u }.Wellformed

  Rule rewriting to mulitple nonterminals is wellformed

theorem ContextFreeRule.only_nonterminals {T : Type uT} {N : Type u_1} {u : List (Symbol T N)} (hu : ∀ s ∈ u, match s with | Symbol.nonterminal n => True | x => False) : ∃ (v : List N), List.map Symbol.nonterminal v = u

theorem ContextFreeRule.Wellformed.mem_nonterminal {T : Type uT} {N : Type u_1} {r : ContextFreeRule T N} (hr : r.Wellformed) (i : Fin r.output.length) (h2 : 2 ≤ r.output.length) : ∃ (n : N), r.output[i] = Symbol.nonterminal n

theorem ContextFreeRule.Wellformed.cases {T : Type uT} {N : Type u_1} {r : ContextFreeRule T N} (hr : r.Wellformed) : (∃ (t : T), r.output = [Symbol.terminal t]) ∨ ∃ (n₁ : N) (n₂ : N) (u : List N), r.output = Symbol.nonterminal n₁ :: Symbol.nonterminal n₂ :: List.map Symbol.nonterminal u

Definition of ContextFreeGrammar.restrictLength, the algorithm to translate a wellformed context-free grammar to a chomsky normal form grammar

@[reducible, inline]

abbrev ContextFreeGrammar.NT' {T : Type uT} {g : ContextFreeGrammar T} : Type uT

Shorthand for the new type of nonterminals.

Equations

• ContextFreeGrammar.NT' = (g.NT ⊕ (r : ContextFreeRule T g.NT) × Fin (r.output.length - 2))

@[irreducible]

def ContextFreeGrammar.computeRulesRec {T : Type uT} {g : ContextFreeGrammar T} (r : ContextFreeRule T g.NT) (i : Fin (r.output.length - 2)) : List (ChomskyNormalFormRule T NT')

Computes a cascade of rules generating r.output if it only contains nonterminals. For a rule r : n -> n₁n₂n₃n₄, generates rules n -> n₁m₂, m₂ -> n₂m₃, and m₃ -> n₃n₄. The type of of NT', encodes the correspondence between rules and the new nonterminals.

Equations

• One or more equations did not get rendered due to their size.

def ContextFreeGrammar.computeRules {T : Type uT} {g : ContextFreeGrammar T} (r : ContextFreeRule T g.NT) : List (ChomskyNormalFormRule T NT')

We assume all rules' output is either a pair of nonterminals, a single terminal or a string of at least 3 nonterminals. In the first two cases we can directly translate them, otherwise we generate new rules using compute_rules_rec.

Equations

• One or more equations did not get rendered due to their size.

def ContextFreeGrammar.restrictLengthRules {T : Type uT} {g : ContextFreeGrammar T} [DecidableEq T] [DecidableEq g.NT] (l : List (ContextFreeRule T g.NT)) : Finset (ChomskyNormalFormRule T NT')

Compute all ChomskyNormalFormRules corresponding to the original ContextFreeRules

Equations

• ContextFreeGrammar.restrictLengthRules l = (List.map ContextFreeGrammar.computeRules l).flatten.toFinset

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

Construct a ChomskyNormalGrammar corresponding to the original ContextFreeGrammar

Equations

• g.restrictLength = { NT := ContextFreeGrammar.NT', initial := Sum.inl g.initial, rules := ContextFreeGrammar.restrictLengthRules g.rules.toList }

def ContextFreeGrammar.Wellformed {T : Type uT} (g : ContextFreeGrammar T) : Prop

A grammar is Wellformed if all rules are ContextFreeRule.Wellformed

Equations

• g.Wellformed = ∀ r ∈ g.rules, r.Wellformed

Definitions of embeding into and projecting to the type of symbols of the new grammar

def ContextFreeGrammar.embedSymbol {T : Type uT} {g : ContextFreeGrammar T} (s : Symbol T g.NT) : Symbol T NT'

Intuitive embedding of symbols of the original grammar into symbols of the new grammar's type

Equations

• ContextFreeGrammar.embedSymbol (Symbol.terminal t) = Symbol.terminal t
• ContextFreeGrammar.embedSymbol (Symbol.nonterminal n) = Symbol.nonterminal (Sum.inl n)

theorem ContextFreeGrammar.embedSymbol_nonterminal {T : Type uT} {g : ContextFreeGrammar T} {n : g.NT} : embedSymbol (Symbol.nonterminal n) = Symbol.nonterminal (Sum.inl n)

theorem ContextFreeGrammar.embedSymbol_terminal {T : Type uT} {g : ContextFreeGrammar T} {t : T} : embedSymbol (Symbol.terminal t) = Symbol.terminal t

@[reducible, inline]

abbrev ContextFreeGrammar.embedString {T : Type uT} {g : ContextFreeGrammar T} (u : List (Symbol T g.NT)) : List (Symbol T NT')

Intuitive embedding of strings of the original grammar into strings of the new grammar's type

Equations

• ContextFreeGrammar.embedString u = List.map ContextFreeGrammar.embedSymbol u

theorem ContextFreeGrammar.embedString_nonterminal {T : Type uT} {g : ContextFreeGrammar T} {n : g.NT} : embedString [Symbol.nonterminal n] = [Symbol.nonterminal (Sum.inl n)]

theorem ContextFreeGrammar.embedString_terminals {T : Type uT} {g : ContextFreeGrammar T} {u : List T} : embedString (List.map Symbol.terminal u) = List.map Symbol.terminal u

theorem ContextFreeGrammar.embedString_append {T : Type uT} {g : ContextFreeGrammar T} {u v : List (Symbol T g.NT)} : embedString (u ++ v) = embedString u ++ embedString v

def ContextFreeGrammar.projectSymbol {T : Type uT} {g : ContextFreeGrammar T} (s : Symbol T NT') : List (Symbol T g.NT)

Projection from symbols of the new grammars type into symbols of the original grammar

Equations

• ContextFreeGrammar.projectSymbol (Symbol.terminal t) = [Symbol.terminal t]
• ContextFreeGrammar.projectSymbol (Symbol.nonterminal (Sum.inl n)) = [Symbol.nonterminal n]
• ContextFreeGrammar.projectSymbol (Symbol.nonterminal (Sum.inr ⟨r, ⟨i, isLt⟩⟩)) = List.drop (r.output.length - 2 - i) r.output

@[reducible, inline]

abbrev ContextFreeGrammar.projectString {T : Type uT} {g : ContextFreeGrammar T} (u : List (Symbol T NT')) : List (Symbol T g.NT)

Projection from strings of the new grammars type into strings of the original grammar

Equations

• ContextFreeGrammar.projectString u = (List.map ContextFreeGrammar.projectSymbol u).flatten

theorem ContextFreeGrammar.projectString_append {T : Type uT} {g : ContextFreeGrammar T} {u v : List (Symbol T NT')} : projectString (u ++ v) = projectString u ++ projectString v

theorem ContextFreeGrammar.projectString_embedString_id {T : Type uT} {g : ContextFreeGrammar T} {u : List (Symbol T g.NT)} : projectString (embedString u) = u

theorem ContextFreeGrammar.projectString_nonterminal {T : Type uT} {g : ContextFreeGrammar T} {n : g.NT} : projectString [Symbol.nonterminal (Sum.inl n)] = [Symbol.nonterminal n]

@[simp]

theorem ContextFreeGrammar.projectSymbol_terminal {T : Type uT} {g : ContextFreeGrammar T} {t : T} : projectSymbol (Symbol.terminal t) = [Symbol.terminal t]

theorem ContextFreeGrammar.projectString_terminals {T : Type uT} {g : ContextFreeGrammar T} {u : List T} : projectString (List.map Symbol.terminal u) = List.map Symbol.terminal u

theorem ContextFreeGrammar.mem_computeRulesRec_projectString_input_eq_output {T : Type uT} {g : ContextFreeGrammar T} {r : ContextFreeRule T g.NT} {i : Fin (r.output.length - 2)} {r' : ChomskyNormalFormRule T NT'} (hrri : r' ∈ computeRulesRec r i) : projectString r'.output = projectString [Symbol.nonterminal r'.input]

theorem ContextFreeGrammar.left_not_mem_computeRulesRec {T : Type uT} {g : ContextFreeGrammar T} {n : g.NT} {r : ContextFreeRule T g.NT} {r' : ChomskyNormalFormRule T NT'} {i : Fin (r.output.length - 2)} (hrn : r'.input = Sum.inl n) : r' ∉ computeRulesRec r i

theorem ContextFreeGrammar.mem_computRules_right_length {T : Type uT} {g : ContextFreeGrammar T} {n : (r : ContextFreeRule T g.NT) × Fin (r.output.length - 2)} {r : ContextFreeRule T g.NT} {r' : ChomskyNormalFormRule T NT'} (hrr : r' ∈ computeRules r) (hrn : r'.input = Sum.inr n) : 3 ≤ r.output.length

theorem ContextFreeGrammar.mem_computeRules_right_mem_computeRulesRec {T : Type uT} {g : ContextFreeGrammar T} {n : (r : ContextFreeRule T g.NT) × Fin (r.output.length - 2)} {r : ContextFreeRule T g.NT} {r' : ChomskyNormalFormRule T NT'} (hrₒ : r.output.length - 3 < r.output.length - 2) (hrr : r' ∈ computeRules r) (hrn : r'.input = Sum.inr n) : r' ∈ computeRulesRec r ⟨r.output.length - 3, hrₒ⟩

theorem ContextFreeGrammar.mem_computeRules_left {T : Type uT} {g : ContextFreeGrammar T} {n : g.NT} {r : ContextFreeRule T g.NT} {r' : ChomskyNormalFormRule T NT'} (hrr : r' ∈ computeRules r) (hrn : r'.input = Sum.inl n) : projectString r'.output = r.output ∧ n = r.input

theorem ContextFreeGrammar.restrictLength_produces_derives_projectString {T : Type uT} {g : ContextFreeGrammar T} {u v : List (Symbol T NT')} [DecidableEq T] [DecidableEq g.NT] (huv : g.restrictLength.Produces u v) : g.Derives (projectString u) (projectString v)

theorem ContextFreeGrammar.restrictLength_derives_derives_projectString {T : Type uT} {g : ContextFreeGrammar T} {u v : List (Symbol T NT')} [DecidableEq T] [DecidableEq g.NT] (huv : g.restrictLength.Derives u v) : g.Derives (projectString u) (projectString v)

theorem ContextFreeGrammar.computeRulesRec_derives {T : Type uT} {g : ContextFreeGrammar T} [DecidableEq T] [DecidableEq g.NT] {r : ContextFreeRule T g.NT} {i : Fin (r.output.length - 2)} {n : NT'} {x : List (ChomskyNormalFormRule T NT')} (hrix : computeRulesRec r i ⊆ x) (hr : r.Wellformed) : { NT := NT', initial := n, rules := x.toFinset }.Derives [Symbol.nonterminal (Sum.inr ⟨r, i⟩)] (embedString (List.drop (r.output.length - 2 - ↑i) r.output))

theorem ContextFreeGrammar.computeRules_derives_embedString {T : Type uT} {g : ContextFreeGrammar T} [DecidableEq T] [DecidableEq g.NT] {r : ContextFreeRule T g.NT} {n : NT'} {x : List (ChomskyNormalFormRule T NT')} (hrx : computeRules r ⊆ x) (hr : r.Wellformed) : { NT := NT', initial := n, rules := x.toFinset }.Derives [Symbol.nonterminal (Sum.inl r.input)] (embedString r.output)

theorem ContextFreeGrammar.produces_restrictLength_derives_embedString {T : Type uT} {g : ContextFreeGrammar T} [DecidableEq T] [DecidableEq g.NT] {u v : List (Symbol T g.NT)} (huv : g.Produces u v) (hg : g.Wellformed) : g.restrictLength.Derives (embedString u) (embedString v)

theorem ContextFreeGrammar.derives_restrictLength_derives_embedString {T : Type uT} {g : ContextFreeGrammar T} [DecidableEq T] [DecidableEq g.NT] {u v : List (Symbol T g.NT)} (huv : g.Derives u v) (hg : g.Wellformed) : g.restrictLength.Derives (embedString u) (embedString v)

theorem ContextFreeGrammar.restrictLength_correct {T : Type uT} {g : ContextFreeGrammar T} [DecidableEq T] [e : DecidableEq g.NT] (hg : g.Wellformed) : g.language = g.restrictLength.language