Pumping Lemma via Chomsky Normal Form

This file proves the pumping lemma for context-free languages using parse trees for Chomsky-normal-form grammars.

Main declarations

• pidgeonhole
• subtree_repeat_root_height
• pumping
• Language.IsContextFree.pumping

Pumping Lemma for Context-Free Grammars

This file contains the proof of the pumping lemma for context-free grammars

Main theorems

• Language.IsContextFree.pumping: A language generated by a contextfree grammar can be pumped.

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]

theorem pidgeonhole {α : Type u_1} {β : Type u_2} {A : Finset α} {B : Finset β} {f : ↥A → ↥B} (hf : Function.Injective f) : A.card ≤ B.card

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

generators g is the set of nonterminals that appear in the left hand side of rules of g

Equations

• g.generators = (List.map ChomskyNormalFormRule.input g.rules.toList).toFinset

theorem ChomskyNormalFormGrammar.pumping_string {T : Type uT} {g : ChomskyNormalFormGrammar T} {u v : List (Symbol T g.NT)} {n : g.NT} (hg : g.Derives [Symbol.nonterminal n] (u ++ [Symbol.nonterminal n] ++ v)) (i : ℕ) : g.Derives [Symbol.nonterminal n] (u ^+^ i ++ [Symbol.nonterminal n] ++ v ^+^ i)

theorem ChomskyNormalFormGrammar.subtree_height_le {T : Type uT} {g : ChomskyNormalFormGrammar T} {n₁ n₂ : g.NT} {p₁ : parseTree n₁} {p₂ : parseTree n₂} (hpp : p₂.IsSubtreeOf p₁) : p₂.height ≤ p₁.height

theorem ChomskyNormalFormGrammar.input_mem_generators {T : Type uT} {g : ChomskyNormalFormGrammar T} [DecidableEq g.NT] {r : ChomskyNormalFormRule T g.NT} (hrg : r ∈ g.rules) : r.input ∈ g.generators

theorem ChomskyNormalFormGrammar.subtree_repeat_root_height_ind {T : Type uT} {g : ChomskyNormalFormGrammar T} [DecidableEq g.NT] [DecidableEq ((_n : g.NT) × parseTree _n)] {n : g.NT} {p : parseTree n} (s : Finset ((_n : g.NT) × parseTree _n)) (hs : ∀ e₁ ∈ s, ∀ e₂ ∈ s, e₁.fst = e₂.fst → e₁ = e₂) (hp : g.generators.card.succ ≤ p.height + s.card) (hps : ∀ pₛ ∈ s, p.IsSubtreeOf pₛ.snd) : (∃ (n' : g.NT) (p' : parseTree n') (p'' : parseTree n'), p'.IsSubtreeOf p ∧ p''.IsSubtreeOf p' ∧ p' ≠ p'') ∨ ∃ (n₀ : g.NT) (t : parseTree n₀) (t' : parseTree n₀), ⟨n₀, t⟩ ∈ s ∧ t'.IsSubtreeOf p

theorem ChomskyNormalFormGrammar.subtree_repeat_root_height_aux_aux_aux {T : Type uT} {g : ChomskyNormalFormGrammar T} [DecidableEq g.NT] [DecidableEq ((_n : g.NT) × parseTree _n)] {n : g.NT} {p : parseTree n} (hp : g.generators.card.succ = p.height) : ∃ (n' : g.NT) (p' : parseTree n') (p'' : parseTree n'), p'.IsSubtreeOf p ∧ p''.IsSubtreeOf p' ∧ p' ≠ p''

theorem ChomskyNormalFormGrammar.subtree_repeat_root_height_aux_aux {T : Type uT} {g : ChomskyNormalFormGrammar T} [DecidableEq g.NT] [DecidableEq ((_n : g.NT) × parseTree _n)] {n : g.NT} {p : parseTree n} (hgp : g.generators.card.succ = p.height) : ∃ (n' : g.NT) (p' : parseTree n') (p'' : parseTree n'), p'.IsSubtreeOf p ∧ p''.IsSubtreeOf p' ∧ p'.height ≤ g.generators.card.succ ∧ p' ≠ p''

theorem ChomskyNormalFormGrammar.subtree_repeat_root_height_aux {T : Type uT} {g : ChomskyNormalFormGrammar T} [DecidableEq g.NT] [DecidableEq ((_n : g.NT) × parseTree _n)] {n : g.NT} {p : parseTree n} (hgp : g.generators.card.succ ≤ p.height) : ∃ (n' : g.NT) (p' : parseTree n') (p'' : parseTree n'), p'.IsSubtreeOf p ∧ p''.IsSubtreeOf p' ∧ p'.height ≤ g.generators.card.succ ∧ p' ≠ p''

theorem ChomskyNormalFormGrammar.subtree_repeat_root_height {T : Type uT} {g : ChomskyNormalFormGrammar T} [DecidableEq g.NT] [DecidableEq ((_n : g.NT) × parseTree _n)] {n : g.NT} {p : parseTree n} (hp : p.yield.length ≥ 2 ^ g.generators.card) : ∃ (n' : g.NT) (p' : parseTree n') (p'' : parseTree n'), p'.IsSubtreeOf p ∧ p''.IsSubtreeOf p' ∧ p'.height ≤ g.generators.card.succ ∧ p' ≠ p''

theorem ChomskyNormalFormGrammar.pumping {T : Type uT} {g : ChomskyNormalFormGrammar T} [DecidableEq g.NT] [DecidableEq ((_n : g.NT) × parseTree _n)] {w : List T} (hwg : w ∈ g.language) (hw : w.length ≥ 2 ^ g.generators.card) : ∃ (u : List T) (v : List T) (x : List T) (y : List T) (z : List T), w = u ++ v ++ x ++ y ++ z ∧ (v ++ y).length > 0 ∧ (v ++ x ++ y).length ≤ 2 ^ g.generators.card ∧ ∀ (i : ℕ), u ++ v ^+^ i ++ x ++ y ^+^ i ++ z ∈ g.language

theorem Language.IsContextFree.pumping {T : Type} {L : Language T} (hL : L.IsContextFree) : ∃ (p : ℕ), ∀ w ∈ L, w.length ≥ p → ∃ (u : List T) (v : List T) (x : List T) (y : List T) (z : List T), w = u ++ v ++ x ++ y ++ z ∧ (v ++ y).length > 0 ∧ (v ++ x ++ y).length ≤ p ∧ ∀ (i : ℕ), u ++ v ^+^ i ++ x ++ y ^+^ i ++ z ∈ L