Ogden's lemma

DefinitionNumber of marked letters#✓fully proved

A marked word over an alphabet \(T\) is a word whose letters are pairs \((a, b)\) with \(a \in T\) and \(b\) a Boolean; the letter \((a, b)\) is marked when \(b\) is true. The number of marked letters of a marked word \(w\) is the number of letters of \(w\) that are marked, counted with multiplicity.

def marks (w : List (T × Bool)) : ℕ :=
  w.countP (·.2)

Used by 3

Used byOgden's lemma · Ogden's lemma for a grammar, with an explicit bound · The pumping lemma for a grammar, with an explicit bound

TheoremOgden's lemma for a grammar, with an explicit bound#✓fully proved

Let \(g\) be a context-free grammar over an alphabet \(T\) and let \(R\), \(K\), \(n\) be natural numbers with \(R \ge 2\) such that the right-hand side of every production of \(g\) has length at most \(R\), some list of at most \(K\) nonterminals contains the left-hand side of every production of \(g\), and \(R^{K+1} \le n\). A marked word is a word whose letters are pairs \((a, b)\) with \(a \in T\) and \(b\) a Boolean, the letter being marked when \(b\) is true; its underlying word is the word of first components. Then every marked word \(w\) whose underlying word lies in the language of \(g\) and which has at least \(n\) marked letters can be written as \(w = uvxyz\) with marked words \(u, v, x, y, z\) such that \(vy\) has at least one marked letter, \(vxy\) has at most \(n\) marked letters, and for every natural number \(i\) the underlying word of \(u v^i x y^i z\) lies in the language of \(g\), where \(v^i\) is the concatenation of \(i\) copies of \(v\).

theorem ogden_of_bound (g : ContextFreeGrammar T) {R K n : ℕ} (hR2 : 2 ≤ R)
    (hR : ∀ r ∈ g.rules, r.output.length ≤ R)
    (hK : ∃ l : List g.NT, l.length ≤ K ∧ ∀ r ∈ g.rules, r.input ∈ l) (hn : R ^ (K + 1) ≤ n) :
    ∀ w : List (T × Bool), w.map Prod.fst ∈ g.language → n ≤ marks w →
      ∃ u v x y z : List (T × Bool), w = u ++ v ++ x ++ y ++ z ∧ 0 < marks (v ++ y) ∧
        marks (v ++ x ++ y) ≤ n ∧
        ∀ i : ℕ, (u ++ (List.replicate i v).flatten ++ x ++ (List.replicate i y).flatten ++
          z).map Prod.fst ∈ g.language

Uses 11 · Used by 2

Statement usesNumber of marked letters

Proof usesYield of a sentential form · Concatenation of yields · Height-bounded yields are yields · Derivation contexts · Pumping through a self-context · A production gives derivation contexts · Height-bounded derivations · Splitting a height-bounded yield at a concatenation · Every yield has a height bound · Language membership through yields

Used byOgden's lemma · The pumping lemma for a grammar, with an explicit bound

TheoremThe pumping lemma for a grammar, with an explicit bound#✓fully proved

Let \(g\) be a context-free grammar over an alphabet \(T\) and let \(R\), \(K\), \(n\) be natural numbers with \(R \ge 2\) such that the right-hand side of every production of \(g\) has length at most \(R\), some list of at most \(K\) nonterminals contains the left-hand side of every production of \(g\), and \(R^{K+1} \le n\). Then every word \(w\) in the language of \(g\) of length at least \(n\) can be written as \(w = uvxyz\) with words \(u, v, x, y, z\) over \(T\) such that \(vy\) is nonempty, \(vxy\) has length at most \(n\), and \(u v^i x y^i z\) lies in the language of \(g\) for every natural number \(i\), where \(v^i\) is the concatenation of \(i\) copies of \(v\).

It follows from Ogden's lemma with every letter marked.

theorem pumping_of_bound (g : ContextFreeGrammar T) {R K n : ℕ} (hR2 : 2 ≤ R)
    (hR : ∀ r ∈ g.rules, r.output.length ≤ R)
    (hK : ∃ l : List g.NT, l.length ≤ K ∧ ∀ r ∈ g.rules, r.input ∈ l) (hn : R ^ (K + 1) ≤ n) :
    ∀ w ∈ g.language, 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 ∈
        g.language

Uses 2 · Used by 1

Proof usesNumber of marked letters · Ogden's lemma for a grammar, with an explicit bound

Used byPumping lemma for encoded grammars

TheoremOgden's lemma#✓fully proved

Let \(L\) be a context-free language over an alphabet \(T\). A marked word is a word whose letters are pairs \((a, b)\) with \(a \in T\) and \(b\) a Boolean, the letter being marked when \(b\) is true; its underlying word is the word of first components. Then there is a natural number \(n > 0\) such that every marked word \(w\) whose underlying word lies in \(L\) and which has at least \(n\) marked letters can be written as \(w = uvxyz\) with marked words \(u, v, x, y, z\) such that \(vy\) has at least one marked letter, \(vxy\) has at most \(n\) marked letters, and for every natural number \(i\) the underlying word of \(u v^i x y^i z\) lies in \(L\), where \(v^i\) is the concatenation of \(i\) copies of \(v\).

theorem IsContextFree.ogden {L : Language T} (hL : L.IsContextFree) :
    ∃ n : ℕ, 0 < n ∧ ∀ w : List (T × Bool), w.map Prod.fst ∈ L → n ≤ marks w →
      ∃ u v x y z : List (T × Bool), w = u ++ v ++ x ++ y ++ z ∧ 0 < marks (v ++ y) ∧
        marks (v ++ x ++ y) ≤ n ∧
        ∀ i : ℕ, (u ++ (List.replicate i v).flatten ++ x ++ (List.replicate i y).flatten ++
          z).map Prod.fst ∈ L

Uses 2

Statement usesNumber of marked letters

Proof usesOgden's lemma for a grammar, with an explicit bound

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.