The Cocke–Younger–Kasami recognizer

14 fully proved

Yields under Chomsky normal form

TheoremNonterminals in outputs have no empty production#✓fully proved

Let \(g\) be a context-free grammar in Chomsky normal form. If a nonterminal \(B\) occurs in the output of some production of \(g\), then \(g\) has no production \(B \to \varepsilon\).

Such a production would have the initial nonterminal on the left, which then occurs in an output while an empty production exists.

theorem no_empty_rule_of_mem_output (hg : IsChomskyNormalForm g) {r : ContextFreeRule T g.NT}
    (hr : r ∈ g.rules) {B : g.NT} (hB : Symbol.nonterminal B ∈ r.output) :
    ¬ ∃ r' ∈ g.rules, r'.input = B ∧ r'.output = []

Uses 1 · Used by 2

Statement usesChomsky normal form

Used byForms yielding the empty word under Chomsky normal form · Shape of yields under Chomsky normal form

TheoremForms yielding the empty word under Chomsky normal form#✓fully proved

If \(g\) is in Chomsky normal form, then every symbol of a sentential form that yields the empty word is a nonterminal \(B\) for which \(g\) has a production \(B \to \varepsilon\).

theorem empty_rule_of_yields_nil (hg : IsChomskyNormalForm g) {u : List (Symbol T g.NT)}
    {w : List T} (h : Yields g u w) (hw : w = []) :
    ∀ s ∈ u, ∃ B, s = .nonterminal B ∧ ∃ r ∈ g.rules, r.input = B ∧ r.output = []

Uses 3 · Used by 2

Statement usesChomsky normal form · Yield of a sentential form

Proof usesNonterminals in outputs have no empty production

Used byCorrectness of the CYK recognizer · Shape of yields under Chomsky normal form

TheoremShape of yields under Chomsky normal form#✓fully proved

Let \(g\) be a context-free grammar in Chomsky normal form, \(A\) a nonterminal and \(w\) a nonempty word. Then \(A\) yields \(w\) if and only if \(g\) has a production \(A \to a\) with \(a\) a terminal and \(w = a\), or a production \(A \to BC\) with nonterminals \(B\) and \(C\) and nonempty words \(w_1\) and \(w_2\) such that \(w = w_1 w_2\), \(B\) yields \(w_1\) and \(C\) yields \(w_2\).

theorem yields_nonterminal_iff_of_ne_nil (hg : IsChomskyNormalForm g) {A : g.NT} {w : List T}
    (hw : w ≠ []) :
    Yields g [.nonterminal A] w ↔ ∃ r ∈ g.rules, r.input = A ∧
      ((∃ a, r.output = [.terminal a] ∧ w = [a]) ∨
        ∃ B C w₁ w₂, r.output = [.nonterminal B, .nonterminal C] ∧ w = w₁ ++ w₂ ∧
          w₁ ≠ [] ∧ w₂ ≠ [] ∧ Yields g [.nonterminal B] w₁ ∧ Yields g [.nonterminal C] w₂)

Uses 7 · Used by 1

Statement usesChomsky normal form · Yield of a sentential form

Proof usesConcatenation of yields · Splitting a yield over a concatenation · Forms yielding the empty word under Chomsky normal form · Nonterminals in outputs have no empty production · Yield through one production

Used byThe CYK step

The recognizer

DefinitionWhen a production output fits a word#✓fully proved

Let \(f\) assign a cell (a finite set of nonterminals) to every word. A production output fits a word \(w\) with respect to \(f\) exactly in two cases: the output is a single terminal \(a\) and \(w\) is the one-letter word \(a\); or the output is a pair of nonterminals \(B C\) and there is some \(i\) with \(0 < i < |w|\) such that \(B\) lies in the cell of the first \(i\) letters of \(w\) and \(C\) lies in the cell of the remaining letters. No other output fits any word.

def cykFits (f : List T → Finset g.NT) (w : List T) : List (Symbol T g.NT) → Bool
  | [.terminal a] => decide (w = [a])
  | [.nonterminal B, .nonterminal C] =>
      (List.range w.length).any fun i =>
        decide (0 < i) && decide (B ∈ f (w.take i)) && decide (C ∈ f (w.drop i))
  | _ => false

Used by 3

Used byCorrectness of one indexed CYK cell · The CYK cell built from given cells · The CYK step

DefinitionThe CYK cell built from given cells#✓fully proved

Given an assignment \(f\) of a cell (a finite set of nonterminals of \(g\)) to every word, the cell of a word \(w\) built from \(f\) is the set of left-hand sides of those productions of \(g\) whose outputs fit \(w\) with respect to \(f\).

def cykCellFrom (f : List T → Finset g.NT) (w : List T) : Finset g.NT :=
  (g.rules.filter fun r => cykFits f w r.output = true).image ContextFreeRule.input

Uses 1 · Used by 4

Statement usesWhen a production output fits a word

Used byThe unshared CYK recurrence · The CYK table · Correctness of the CYK table · The CYK step

TheoremThe CYK step#✓fully proved

Let \(g\) be a context-free grammar in Chomsky normal form, let \(f\) assign to each word over the terminals a finite set of nonterminals, and let \(w\) be a nonempty word. For \(0 < i < |w|\) write \(u_i\) for the prefix of \(w\) of length \(i\) and \(v_i\) for the remaining suffix, so that \(w = u_i v_i\). Suppose that for every such \(i\) and every nonterminal \(B\), \(B \in f(u_i)\) if and only if \(B\) yields \(u_i\), and \(B \in f(v_i)\) if and only if \(B\) yields \(v_i\). Then a nonterminal \(A\) lies in the CYK cell of \(w\) built from \(f\) if and only if \(A\) yields \(w\).

theorem mem_cykCellFrom_iff (hg : IsChomskyNormalForm g) {f : List T → Finset g.NT}
    {w : List T} (hw : w ≠ [])
    (hf : ∀ i, 0 < i → i < w.length → ∀ B,
      (B ∈ f (w.take i) ↔ Yields g [.nonterminal B] (w.take i)) ∧
      (B ∈ f (w.drop i) ↔ Yields g [.nonterminal B] (w.drop i)))
    {A : g.NT} : A ∈ cykCellFrom g f w ↔ Yields g [.nonterminal A] w

Uses 5 · Used by 2

Statement usesChomsky normal form · Yield of a sentential form · The CYK cell built from given cells

Proof usesWhen a production output fits a word · Shape of yields under Chomsky normal form

Used byCorrectness of the CYK table · Correctness of the CYK recurrence

DefinitionThe unshared CYK recurrence#✓fully proved

The depth-\(n\) CYK cell of a word \(w\) is defined by recursion on \(n\): at depth \(0\) every cell is empty, and the depth-\((n + 1)\) cell of \(w\) is the CYK cell of \(w\) built from the depth-\(n\) cells of all words. Cells are recomputed without sharing.

def cykCell : ℕ → List T → Finset g.NT
  | 0, _ => ∅
  | n + 1, w => cykCellFrom g (cykCell n) w

Uses 1 · Used by 2

Statement usesThe CYK cell built from given cells

Used byCorrectness of one indexed CYK cell · Correctness of the CYK recurrence

TheoremCorrectness of the CYK recurrence#✓fully proved

Let \(g\) be a context-free grammar in Chomsky normal form. For every natural number \(n\), every nonterminal \(A\) and every nonempty word \(w\) of length at most \(n\), \(A\) lies in the depth-\(n\) CYK cell of \(w\) if and only if \(A\) yields \(w\).

theorem mem_cykCell_iff (hg : IsChomskyNormalForm g) :
    ∀ (n : ℕ) {A : g.NT} {w : List T}, w ≠ [] → w.length ≤ n →
      (A ∈ cykCell g n w ↔ Yields g [.nonterminal A] w)

Uses 4 · Used by 1

Statement usesChomsky normal form · Yield of a sentential form · The unshared CYK recurrence

Proof usesThe CYK step

Used byCorrectness of one indexed CYK cell

The table

DefinitionLooking up a word in a CYK table#✓fully proved

In a table listing pairs of a word and a cell, the cell recorded for a word \(u\) is the cell of the first entry whose word is \(u\), or the empty set if no entry has word \(u\).

def cykLookup (tbl : List (List T × Finset g.NT)) (u : List T) : Finset g.NT :=
  ((tbl.find? fun e => e.1 = u).map Prod.snd).getD ∅

Used by 5

Used byCorrectness of the indexed CYK recognizer · The CYK recognizer · Correctness of the CYK recognizer · The CYK table · Correctness of the CYK table

DefinitionThe CYK table#✓fully proved

The CYK table of a word \(w\) up to length \(l\) is a list of pairs of a word and a cell, defined by recursion on \(l\). Up to length \(0\) it is empty. The table up to length \(l + 1\) is the table \(t\) up to length \(l\) followed by one entry for each position \(i\) (counted from \(0\)) with \(i + l + 1 \le |w|\), in increasing order of \(i\): the factor \(u\) of \(w\) of length \(l + 1\) starting at position \(i\), together with the CYK cell of \(u\) built from the cells recorded in \(t\).

def cykTable (w : List T) : ℕ → List (List T × Finset g.NT)
  | 0 => []
  | l + 1 =>
      let tbl := cykTable w l
      tbl ++ (List.range (w.length - l)).map fun i =>
        let u := (w.drop i).take (l + 1)
        (u, cykCellFrom g (cykLookup tbl) u)

Uses 2 · Used by 4

Statement usesThe CYK cell built from given cells · Looking up a word in a CYK table

Used byCorrectness of the indexed CYK recognizer · The CYK recognizer · Correctness of the CYK recognizer · Correctness of the CYK table

DefinitionCorrect CYK tables#✓fully proved

A table listing pairs \((u, X)\) of a word \(u\) and a set \(X\) of nonterminals of \(g\) is correct when, for every entry \((u, X)\) with \(u\) nonempty, \(X\) consists exactly of the nonterminals \(B\) such that the one-symbol form \(B\) yields \(u\).

def CykTableCorrect (tbl : List (List T × Finset g.NT)) : Prop :=
  ∀ e ∈ tbl, e.1 ≠ [] → ∀ B, B ∈ e.2 ↔ Yields g [.nonterminal B] e.1

Uses 1 · Used by 2

Statement usesYield of a sentential form

Used byCorrectness of the CYK recognizer · Correctness of the CYK table

TheoremCorrectness of the CYK table#✓fully proved

Let \(g\) be a context-free grammar in Chomsky normal form and \(w\) a word. For every \(l\), the CYK table of \(w\) up to length \(l\) is correct, and for all \(j\) and \(m\) with \(0 < m \le l\) and \(j + m \le |w|\), some entry of the table has as its word the factor of \(w\) of length \(m\) starting at position \(j\) (positions counted from \(0\)).

theorem cykTable_spec (hg : IsChomskyNormalForm g) (w : List T) :
    ∀ l, CykTableCorrect (cykTable g w l) ∧
      ∀ j m, 0 < m → m ≤ l → j + m ≤ w.length →
        ∃ e ∈ cykTable g w l, e.1 = (w.drop j).take m

Uses 7 · Used by 1

Statement usesCorrect CYK tables · Chomsky normal form · The CYK table

Proof usesYield of a sentential form · The CYK cell built from given cells · Looking up a word in a CYK table · The CYK step

Used byCorrectness of the CYK recognizer

DefinitionThe CYK recognizer#✓fully proved

Let \(g\) be a context-free grammar with initial nonterminal \(S\). The CYK recognizer accepts the empty word exactly when \(g\) has a production \(S \to \varepsilon\), and accepts a nonempty word \(w\) exactly when \(S\) lies in the cell recorded for \(w\) in the CYK table of \(w\) up to length \(|w|\).

def cykAccepts (w : List T) : Bool :=
  if w = [] then decide (∃ r ∈ g.rules, r.input = g.initial ∧ r.output = [])
  else decide (g.initial ∈ cykLookup (cykTable g w w.length) w)

Uses 2 · Used by 3

Statement usesLooking up a word in a CYK table · The CYK table

Used byIndexed CYK agrees with the list-table CYK recognizer · Correctness of the indexed CYK recognizer · Correctness of the CYK recognizer

TheoremCorrectness of the CYK recognizer#✓fully proved

Let \(g\) be a context-free grammar in Chomsky normal form. For every word \(w\) over the terminals of \(g\), the CYK recognizer accepts \(w\) if and only if \(w\) belongs to the language of \(g\).

theorem cykAccepts_iff (hg : IsChomskyNormalForm g) {w : List T} :
    cykAccepts g w = true ↔ w ∈ g.language

Uses 10 · Used by 2

Statement usesChomsky normal form · The CYK recognizer

Proof usesCorrect CYK tables · Yield of a sentential form · Looking up a word in a CYK table · The CYK table · Correctness of the CYK table · Forms yielding the empty word under Chomsky normal form · Language membership through yields · Yield through one production

Used byIndexed CYK agrees with the list-table CYK recognizer · Correctness of the indexed CYK recognizer

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.