Correctness of indexed CYK

TheoremCorrectness of one indexed CYK cell#✓fully proved

A cell is correct once all strictly shorter, valid factors are correct. The rule enumeration certificate constrains data only, not computation.

theorem cell_correct {g : ContextFreeGrammar T} [DecidableEq g.NT]
    (hg : IsChomskyNormalForm g) (tc nc : ℕ) (w : List T)
    (rs : List (ContextFreeRule T g.NT))
    (hrs : ∀ r, r ∈ rs ↔ r ∈ g.rules)
    (tbl : Array (Array (List g.NT))) (i len : ℕ)
    (hpos : 0 < len) (hbound : i + len ≤ w.length)
    (htbl : ∀ j m, 0 < m → m < len → j + m ≤ w.length → ∀ a,
      a ∈ lookup tbl j m ↔
        Yields g [.nonterminal a] ((w.drop j).take m)) (a : g.NT) :
    a ∈ (cell tc nc w.toArray tbl i len rs).ret ↔
      Yields g [.nonterminal a] ((w.drop i).take len)

Uses 11 · Used by 1

Statement usesCharged computation of one CYK cell · CYK table lookup with empty default cells · Chomsky normal form · Yield of a sentential form

Proof usesProduction-output fit test for indexed CYK · CYK cell members come from scanned productions · Charged scan of CYK split positions · Successful CYK split scans find a split in range · The unshared CYK recurrence · When a production output fits a word · Correctness of the CYK recurrence

Used byCorrectness of the completed indexed CYK table

TheoremIndexing of a constructed CYK row#✓fully proved

Row construction preserves the exact start-position indexing.

theorem row_get (tc nc : ℕ) (w : Array T)
    (tbl : Array (Array (List N))) (len : ℕ)
    (rs : List (ContextFreeRule T N)) (i count j : ℕ) :
    (row tc nc w tbl len rs i count).ret[j]? =
      if j < count then some (cell tc nc w tbl (i + j) len rs).ret
      else none

Uses 2 · Used by 2

Statement usesCharged computation of one CYK cell · Charged construction of one CYK row

Used byNew CYK table row holds the computed cells · Every CYK table lookup is bounded by the rule count

TheoremIndexed CYK table keeps its allocated size#✓fully proved

The outer table retains its allocated size through every update.

@[simp] theorem table_size (tc nc : ℕ) (w : Array T)
    (rs : List (ContextFreeRule T N)) (depth : ℕ) :
    (table tc nc w rs depth).ret.size = w.size + 1

Uses 2 · Used by 2

Statement usesCharged construction of the indexed CYK table

Proof usesCharged construction of one CYK row

Used byNew CYK table row holds the computed cells · Every CYK table lookup is bounded by the rule count

TheoremCYK table update leaves other lengths' cells unchanged#✓fully proved

Updating one length never changes another length's cells.

theorem lookup_table_other (tc nc : ℕ) (w : Array T)
    (rs : List (ContextFreeRule T N)) (depth i len : ℕ)
    (h : depth + 1 ≠ len) :
    lookup (table tc nc w rs (depth + 1)).ret i len =
      lookup (table tc nc w rs depth).ret i len

Uses 3 · Used by 2

Statement usesCYK table lookup with empty default cells · Charged construction of the indexed CYK table

Proof usesCharged construction of one CYK row

Used byCorrectness of the completed indexed CYK table · Every CYK table lookup is bounded by the rule count

TheoremNew CYK table row holds the computed cells#✓fully proved

The new length's row contains exactly the cells just computed.

theorem lookup_table_new (tc nc : ℕ) (w : Array T)
    (rs : List (ContextFreeRule T N)) (depth i : ℕ)
    (hd : depth < w.size) (hi : i < w.size + 1) :
    lookup (table tc nc w rs (depth + 1)).ret i (depth + 1) =
      (cell tc nc w (table tc nc w rs depth).ret i (depth + 1) rs).ret

Uses 6 · Used by 1

Statement usesCharged computation of one CYK cell · CYK table lookup with empty default cells · Charged construction of the indexed CYK table

Proof usesCharged construction of one CYK row · Indexing of a constructed CYK row · Indexed CYK table keeps its allocated size

Used byCorrectness of the completed indexed CYK table

TheoremCorrectness of the completed indexed CYK table#✓fully proved

Every completed valid cell agrees with canonical grammar derivations.

theorem table_correct {g : ContextFreeGrammar T} [DecidableEq g.NT]
    (hg : IsChomskyNormalForm g) (tc nc : ℕ) (w : List T)
    (rs : List (ContextFreeRule T g.NT))
    (hrs : ∀ r, r ∈ rs ↔ r ∈ g.rules) (depth : ℕ) :
    ∀ i len, 0 < len → len ≤ depth → i + len ≤ w.length → ∀ a,
      a ∈ lookup (table tc nc w.toArray rs depth).ret i len ↔
        Yields g [.nonterminal a] ((w.drop i).take len)

Uses 8 · Used by 1

Statement usesCYK table lookup with empty default cells · Charged construction of the indexed CYK table · Chomsky normal form · Yield of a sentential form

Proof usesCharged computation of one CYK cell · Correctness of one indexed CYK cell · New CYK table row holds the computed cells · CYK table update leaves other lengths' cells unchanged

Used byCorrectness of the indexed CYK recognizer

TheoremCorrectness of the CYK epsilon scan#✓fully proved

Epsilon scanning agrees with existence of a start epsilon production.

@[simp] theorem epsilon_ret (nc : ℕ) (start : N)
    (rs : List (ContextFreeRule T N)) :
    (epsilon nc start rs).ret = true ↔
      ∃ r ∈ rs, r.input = start ∧ r.output = []

Uses 1 · Used by 1

Statement usesCharged scan for start epsilon productions

Used byCorrectness of the indexed CYK recognizer

TheoremCorrectness of the indexed CYK recognizer#✓fully proved

The indexed recognizer decides the existing canonical language.

theorem recognizes_iff {g : ContextFreeGrammar T} [DecidableEq g.NT]
    (hg : IsChomskyNormalForm g) (tc nc : ℕ)
    (rs : List (ContextFreeRule T g.NT))
    (hrs : ∀ r, r ∈ rs ↔ r ∈ g.rules) (w : List T) :
    (recognizes tc nc g.initial rs w).ret = true ↔ w ∈ g.language

Uses 15 · Used by 2

Statement usesCharged indexed CYK recognizer · Chomsky normal form

Proof usesCharged scan for start epsilon productions · Correctness of the CYK epsilon scan · CYK table lookup with empty default cells · Charged list-membership scan · Charged membership scan agrees with list membership · Charged construction of the indexed CYK table · Correctness of the completed indexed CYK table · Yield of a sentential form · The CYK recognizer · Correctness of the CYK recognizer · Looking up a word in a CYK table · The CYK table · Language membership through yields

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

TheoremIndexed CYK agrees with the list-table CYK recognizer#✓fully proved

Exact Boolean correspondence with the existing list-table recognizer.

theorem recognizes_eq_cykAccepts {g : ContextFreeGrammar T}
    [DecidableEq g.NT] (hg : IsChomskyNormalForm g) (tc nc : ℕ)
    (rs : List (ContextFreeRule T g.NT))
    (hrs : ∀ r, r ∈ rs ↔ r ∈ g.rules) (w : List T) :
    (recognizes tc nc g.initial rs w).ret = cykAccepts g w

Uses 5

Statement usesCharged indexed CYK recognizer · Chomsky normal form · The CYK recognizer

Proof usesCorrectness of the indexed CYK recognizer · Correctness of the CYK recognizer

9 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.