The pumping lemma for context-free languages

Every context-free language has the pumping property: beyond the pumping constant of a grammar, every word splits as u ++ v ++ x ++ y ++ z with v ++ x ++ y short, v ++ y nonempty, and every u ++ vⁱ ++ x ++ yⁱ ++ z in the language.

The proof is the textbook one through derivation trees. A word longer than maxBranch ^ (rules.card + 1) has a licensed tree of height above rules.card + 1 (RoseTree.Licensed.length_yield_le); a longest path in a tree of least size passes two nodes with the same nonterminal (RoseTree.Licensed.exists_repeat); replacing the lower by the upper would shrink the tree unless it adds terminals, and grafting the lower into the upper repeatedly pumps them (RoseTree.Licensed.replaceAt, RoseTree.Licensed.derives).

Main definitions

• Language.HasCFLPumpingProperty: the pumping property of a language.
• ContextFreeGrammar.maxBranch, ContextFreeGrammar.pumpingConstant: the branching bound and the pumping constant of a grammar.

Main results

• RoseTree.Licensed.length_yield_le: a licensed tree of height h has at most maxBranch ^ h terminals.
• Language.IsContextFree.hasCFLPumpingProperty: every context-free language has the pumping property.

def Language.HasCFLPumpingProperty {α : Type u_1} (L : Language α) : Prop

A language has the pumping property when, beyond some length, every word splits as u ++ v ++ x ++ y ++ z with v ++ x ++ y no longer than that length, v ++ y nonempty, and every u ++ vⁱ ++ x ++ yⁱ ++ z in the language.

Equations

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

The branching bound

noncomputable def ContextFreeGrammar.maxBranch {T : Type u_1} (g : ContextFreeGrammar T) : ℕ

The branching bound of a grammar is the length of its longest right-hand side, and at least 2.

Equations

• g.maxBranch = max 2 (g.rules.sup fun (r : ContextFreeRule T g.NT) => r.output.length)

noncomputable def ContextFreeGrammar.pumpingConstant {T : Type u_1} (g : ContextFreeGrammar T) : ℕ

The pumping constant is maxBranch ^ (rules.card + 1), so that a licensed tree with more terminals has a path through two nodes with the same nonterminal.

Equations

• g.pumpingConstant = g.maxBranch ^ (g.rules.card + 1)

theorem ContextFreeGrammar.two_le_maxBranch {T : Type u_1} (g : ContextFreeGrammar T) : 2 ≤ g.maxBranch

theorem ContextFreeGrammar.pumpingConstant_pos {T : Type u_1} (g : ContextFreeGrammar T) : 0 < g.pumpingConstant

theorem ContextFreeGrammar.length_output_le_maxBranch {T : Type u_1} (g : ContextFreeGrammar T) {r : ContextFreeRule T g.NT} (hr : r ∈ g.rules) : r.output.length ≤ g.maxBranch

theorem RoseTree.Licensed.length_yield_le {T : Type u_1} {g : ContextFreeGrammar T} {t : RoseTree (Symbol T g.NT)} (ht : Licensed g.Licenses t) : t.yield.length ≤ g.maxBranch ^ (t.height - 1)

A licensed tree of height h has at most maxBranch ^ (h - 1) terminals.

theorem ContextFreeGrammar.pumping_from_tall_tree {T : Type u_1} {g : ContextFreeGrammar T} {t : RoseTree (Symbol T g.NT)} (ht : RoseTree.Licensed g.Licenses t) (hroot : t.value = Symbol.nonterminal g.initial) (hlong : g.pumpingConstant ≤ t.yield.length) : ∃ (u : List T) (v : List T) (x : List T) (y : List T) (z : List T), t.yield = u ++ v ++ x ++ y ++ z ∧ (v ++ x ++ y).length ≤ g.pumpingConstant ∧ 1 ≤ v.length + y.length ∧ ∀ (i : ℕ), u ++ (List.replicate i v).flatten ++ x ++ (List.replicate i y).flatten ++ z ∈ g.language

A licensed tree from the start symbol whose yield reaches the pumping constant pumps.

theorem Language.IsContextFree.hasCFLPumpingProperty {T : Type u_1} {L : Language T} (hcf : L.IsContextFree) : L.HasCFLPumpingProperty

The pumping lemma for context-free languages.