Pumping lemma for context-free languages

InductiveHeight-bounded derivations#✓fully proved

Let \(g\) be a context-free grammar. For a sentential form \(\alpha\) (a list of terminals and nonterminals of \(g\)), a terminal word \(w\) and a natural number \(n\), say that \(\alpha\) yields \(w\) at height \(n\) when this follows from three rules: the empty form yields the empty word at every height \(n\); if \(\alpha\) yields \(w\) at height \(n\), then for every terminal \(a\) the form \(a\alpha\) yields \(aw\) at height \(n\); and if \(A \to \beta\) is a production of \(g\), \(\beta\) yields \(w_1\) at height \(n\) and \(\alpha\) yields \(w_2\) at height \(m\), then \(A\alpha\) yields \(w_1 w_2\) at height \(\max(n + 1, m)\).

Thus \(n\) bounds the height of a derivation forest, the number of nonterminal expansions along its longest path; terminals and empty forests contribute nothing.

inductive YieldsH (g : ContextFreeGrammar T) :
    List (Symbol T g.NT) → List T → ℕ → Prop
  | nil (n : ℕ) : YieldsH g [] [] n
  | terminal (a : T) {u : List (Symbol T g.NT)} {w : List T} {n : ℕ}
      (h : YieldsH g u w n) : YieldsH g (Symbol.terminal a :: u) (a :: w) n
  | nonterminal {r : ContextFreeRule T g.NT} (hr : r ∈ g.rules)
      {u : List (Symbol T g.NT)} {w₁ w₂ : List T} {n m : ℕ}
      (hout : YieldsH g r.output w₁ n) (hrest : YieldsH g u w₂ m) :
      YieldsH g (Symbol.nonterminal r.input :: u) (w₁ ++ w₂) (max (n + 1) m)

Used by 9

Used byOgden's lemma for a grammar, with an explicit bound · Concatenating height-bounded yields · Splitting a height-bounded yield at a concatenation · Minimal-height derivation forests exist · Length bound for height-bounded yields · Raising the height bound of a yield · Every yield has a height bound · Height-bounded yields are yields · Pumping lemma for context-free languages

TheoremRaising the height bound of a yield#✓fully proved

Let \(g\) be a context-free grammar. If a sentential form \(\alpha\) yields the terminal word \(w\) through a derivation forest of height at most \(n\), and \(n \le m\), then \(\alpha\) yields \(w\) through a derivation forest of height at most \(m\).

theorem YieldsH.mono {α : List (Symbol T g.NT)} {w : List T} {n m : ℕ}
    (h : YieldsH g α w n) (hle : n ≤ m) : YieldsH g α w m

Uses 1 · Used by 3

Statement usesHeight-bounded derivations

Used byConcatenating height-bounded yields · Splitting a height-bounded yield at a concatenation · Pumping lemma for context-free languages

TheoremEvery yield has a height bound#✓fully proved

Let \(g\) be a context-free grammar. If a sentential form \(\alpha\) yields the terminal word \(w\), then there is a natural number \(n\) such that \(\alpha\) yields \(w\) through a derivation forest of height at most \(n\).

theorem YieldsH.of_yields {α : List (Symbol T g.NT)} {w : List T}
    (h : Yields g α w) : ∃ n, YieldsH g α w n

Uses 2 · Used by 2

Statement usesYield of a sentential form · Height-bounded derivations

Used byOgden's lemma for a grammar, with an explicit bound · Minimal-height derivation forests exist

TheoremHeight-bounded yields are yields#✓fully proved

Let \(g\) be a context-free grammar. If a sentential form \(\alpha\) yields the terminal word \(w\) through a derivation forest of height at most \(n\), then \(\alpha\) yields \(w\).

theorem Yields.of_yieldsH {α : List (Symbol T g.NT)} {w : List T} {n : ℕ}
    (h : YieldsH g α w n) : Yields g α w

Uses 2 · Used by 2

Statement usesYield of a sentential form · Height-bounded derivations

Used byOgden's lemma for a grammar, with an explicit bound · Pumping lemma for context-free languages

TheoremConcatenating height-bounded yields#✓fully proved

Let \(g\) be a context-free grammar. If a sentential form \(u\) yields the terminal word \(w_1\) through a derivation forest of height at most \(n\), and a sentential form \(v\) yields the terminal word \(w_2\) through one of height at most \(m\), then the concatenation \(uv\) yields \(w_1 w_2\) through a derivation forest of height at most \(\max(n, m)\).

theorem YieldsH.append {u v : List (Symbol T g.NT)} {w₁ w₂ : List T}
    {n m : ℕ} (hu : YieldsH g u w₁ n) (hv : YieldsH g v w₂ m) :
    YieldsH g (u ++ v) (w₁ ++ w₂) (max n m)

Uses 2 · Used by 1

Statement usesHeight-bounded derivations

Proof usesRaising the height bound of a yield

Used byPumping lemma for context-free languages

TheoremSplitting a height-bounded yield at a concatenation#✓fully proved

Let \(g\) be a context-free grammar and \(u\), \(v\) sentential forms of \(g\). If the concatenation \(uv\) yields the terminal word \(w\) through a derivation forest of height at most \(n\), then there are terminal words \(w_1\), \(w_2\) with \(w = w_1 w_2\) such that \(u\) yields \(w_1\) and \(v\) yields \(w_2\), each through a derivation forest of height at most \(n\).

theorem YieldsH.append_inv {u v : List (Symbol T g.NT)} {w : List T}
    {n : ℕ} (h : YieldsH g (u ++ v) w n) :
    ∃ w₁ w₂, w = w₁ ++ w₂ ∧ YieldsH g u w₁ n ∧ YieldsH g v w₂ n

Uses 2 · Used by 2

Statement usesHeight-bounded derivations

Proof usesRaising the height bound of a yield

Used byOgden's lemma for a grammar, with an explicit bound · Pumping lemma for context-free languages

TheoremLength bound for height-bounded yields#✓fully proved

Let \(g\) be a context-free grammar and \(R\) a natural number such that every production of \(g\) has an output of length at most \(R\). If a sentential form \(\alpha\) yields the terminal word \(w\) through a derivation forest of height at most \(n\), then \(|w| \le |\alpha| \cdot \max(2, R)^n\).

theorem List.length_le_of_yieldsH {R : ℕ}
    (hR : ∀ r ∈ g.rules, r.output.length ≤ R) :
    ∀ {α : List (Symbol T g.NT)} {w : List T} {n : ℕ},
      YieldsH g α w n → w.length ≤ α.length * (max 2 R) ^ n

Uses 1 · Used by 1

Statement usesHeight-bounded derivations

Used byPumping lemma for context-free languages

TheoremMinimal-height derivation forests exist#✓fully proved

Let \(g\) be a context-free grammar. If a sentential form \(\alpha\) yields the terminal word \(w\), then there is a natural number \(n\) such that \(\alpha\) yields \(w\) through a derivation forest of height at most \(n\), but through no derivation forest of height at most \(m\) for any \(m < n\).

theorem exists_minimal_yieldsH {α : List (Symbol T g.NT)} {w : List T}
    (h : Yields g α w) :
    ∃ n, YieldsH g α w n ∧ ∀ m < n, ¬ YieldsH g α w m

Uses 3 · Used by 1

Statement usesYield of a sentential form · Height-bounded derivations

Proof usesEvery yield has a height bound

Used byPumping lemma for context-free languages

DefinitionDerivation contexts#✓fully proved

Let \(g\) be a context-free grammar, let \(A\) and \(B\) be nonterminals of \(g\), and let \(l\) and \(r\) be words over the terminal alphabet. Then \((l, r)\) is a derivation context from \(A\) to \(B\) when, for every terminal word \(w\) that the nonterminal \(B\) yields in \(g\), the nonterminal \(A\) yields the word \(l w r\) in \(g\).

This is the language-inclusion form of a one-hole derivation context; it is what pumping iteration uses, and it holds vacuously when \(B\) yields nothing.

def YieldsContext (g : ContextFreeGrammar T) (A B : g.NT) (l r : List T) :
    Prop :=
  ∀ w, Yields g [Symbol.nonterminal B] w →
    Yields g [Symbol.nonterminal A] (l ++ w ++ r)

Uses 1 · Used by 4

Statement usesYield of a sentential form

Used byOgden's lemma for a grammar, with an explicit bound · Pumping through a self-context · A production gives derivation contexts · Pumping lemma for context-free languages

TheoremA production gives derivation contexts#✓fully proved

Let \(g\) be a context-free grammar and \(A \to \alpha_1 B \alpha_2\) a production of \(g\), where \(B\) is a nonterminal and \(\alpha_1\), \(\alpha_2\) are sentential forms. If \(\alpha_1\) yields the terminal word \(l\) and \(\alpha_2\) yields the terminal word \(r\), then for every terminal word \(w\) yielded by \(B\) the word \(l w r\) is yielded by \(A\); that is, \((l, r)\) is a derivation context from \(A\) to \(B\).

theorem YieldsContext.of_rule {r : ContextFreeRule T g.NT}
    (hr : r ∈ g.rules) {α₁ α₂ : List (Symbol T g.NT)} {B : g.NT}
    {l rr : List T} (hα : r.output = α₁ ++ Symbol.nonterminal B :: α₂)
    (hl : Yields g α₁ l) (hrr : Yields g α₂ rr) :
    YieldsContext g r.input B l rr

Uses 4 · Used by 2

Statement usesYield of a sentential form · Derivation contexts

Proof usesConcatenation of yields · Yield through one production

Used byOgden's lemma for a grammar, with an explicit bound · Pumping lemma for context-free languages

TheoremPumping through a self-context#✓fully proved

Let \(g\) be a context-free grammar, \(A\) a nonterminal and \(l\), \(r\), \(x\) terminal words. Suppose that for every terminal word \(w\) yielded by \(A\) the word \(l w r\) is also yielded by \(A\), and that \(A\) yields \(x\). Then for every natural number \(i\) the nonterminal \(A\) yields \(l^i x r^i\), where \(l^i\) and \(r^i\) denote the concatenations of \(i\) copies of \(l\) and of \(r\).

theorem YieldsContext.iterate {A : g.NT} {l r x : List T}
    (h : YieldsContext g A A l r) (hx : Yields g [Symbol.nonterminal A] x)
    (i : ℕ) :
    Yields g [Symbol.nonterminal A]
      ((List.replicate i l).flatten ++ x ++
        (List.replicate i r).flatten)

Uses 2 · Used by 2

Statement usesYield of a sentential form · Derivation contexts

Used byOgden's lemma for a grammar, with an explicit bound · Pumping lemma for context-free languages

TheoremPumping lemma for context-free languages#✓fully proved

For every context-free language \(L\) over an alphabet \(T\) there is a natural number \(n > 0\) such that every word \(w \in L\) with \(|w| \ge n\) can be written as \(w = uvxyz\) with words \(u, v, x, y, z\) over \(T\) such that \(vy\) is nonempty, \(|vxy| \le n\), and \(u v^i x y^i z \in L\) for every natural number \(i\), where \(v^i\) and \(y^i\) denote the concatenations of \(i\) copies of \(v\) and of \(y\).

theorem IsContextFree.pumping {L : Language T} (hL : L.IsContextFree) :
    ∃ n : ℕ, 0 < n ∧ ∀ w ∈ L, n ≤ w.length →
      ∃ u v x y z : List T, w = u ++ v ++ x ++ y ++ z ∧ v ++ y ≠ [] ∧
        (v ++ x ++ y).length ≤ n ∧
        ∀ i : ℕ, u ++ (List.replicate i v).flatten ++ x ++
          (List.replicate i y).flatten ++ z ∈ L

Uses 18 · Used by 1

Proof usesReduced grammars · Unit output · Length bound for height-bounded yields · Yield of a sentential form · No empty words without empty productions · Height-bounded yields are yields · Derivation contexts · Pumping through a self-context · A production gives derivation contexts · Height-bounded derivations · Concatenating height-bounded yields · Splitting a height-bounded yield at a concatenation · Raising the height bound of a yield · Minimal-height derivation forests exist · Existence of reduced grammars · Nonterminals of a sentential form · Set of nonterminals mentioned by a grammar · Language membership through yields

Used byThe language \(a^n b^n c^n\) is not context-free

12 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.