Cubic cost of indexed CYK

TheoremExact cost of a membership scan#✓fully proved

Exact charge for a full membership scan, including a failed scan.

theorem member_time (nc : ℕ) (a : N) (xs : List N) :
    (member nc a xs).time = 1 + xs.length * (nc + 3)

Uses 1 · Used by 2

Statement usesCharged list-membership scan

Used byExplicit cubic cost bound for indexed CYK · Cost bound for the CYK split scan

TheoremComputed CYK cell length bounded by the rule count#✓fully proved

Even with duplicates, a cell never exceeds the rule enumeration length.

theorem cell_length (tc nc : ℕ) (w : Array T)
    (tbl : Array (Array (List N))) (i len : ℕ)
    (rs : List (ContextFreeRule T N)) :
    (cell tc nc w tbl i len rs).ret.length ≤ rs.length

Uses 2 · Used by 1

Statement usesCharged computation of one CYK cell

Proof usesProduction-output fit test for indexed CYK

Used byEvery CYK table lookup is bounded by the rule count

TheoremEvery CYK table lookup is bounded by the rule count#✓fully proved

All table cells, including invalid/default positions, have bounded membership-scan length. This invariant is proved from construction.

theorem lookup_length (tc nc : ℕ) (w : Array T)
    (rs : List (ContextFreeRule T N)) (depth i len : ℕ) :
    (lookup (table tc nc w rs depth).ret i len).length ≤ rs.length

Uses 8 · Used by 2

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

Proof usesCharged computation of one CYK cell · Computed CYK cell length bounded by the rule count · CYK table update leaves other lengths' cells unchanged · Charged construction of one CYK row · Indexing of a constructed CYK row · Indexed CYK table keeps its allocated size

Used byExplicit cubic cost bound for indexed CYK · Cost bound for filling the indexed CYK table

TheoremCost bound for the CYK split scan#✓fully proved

Each split pays for both indexed cell reads and both membership scans.

theorem splits_time_le (nc : ℕ) (tbl : Array (Array (List N)))
    (r : ℕ) (htbl : ∀ i len, (lookup tbl i len).length ≤ r)
    (i len : ℕ) (b c : N) (count : ℕ) :
    (splits nc tbl i len b c count).time ≤
      1 + count * (2 * r * (nc + 3) + 18)

Uses 4 · Used by 1

Statement usesCYK table lookup with empty default cells · Charged scan of CYK split positions

Proof usesCharged list-membership scan · Exact cost of a membership scan

Used byCost bound for the CYK production fit test

TheoremCost bound for the CYK production fit test#✓fully proved

Output inspection is bounded; only binary productions scan splits.

theorem fits_time_le (tc nc : ℕ) (w : Array T)
    (tbl : Array (Array (List N))) (r : ℕ)
    (htbl : ∀ i len, (lookup tbl i len).length ≤ r)
    (i len : ℕ) (out : List (Symbol T N)) :
    (fits tc nc w tbl i len out).time ≤
      tc + 12 + len * (2 * r * (nc + 3) + 18)

Uses 4 · Used by 1

Statement usesProduction-output fit test for indexed CYK · CYK table lookup with empty default cells

Proof usesCharged scan of CYK split positions · Cost bound for the CYK split scan

Used byCost bound for computing one CYK cell

TheoremCost bound for computing one CYK cell#✓fully proved

A cell charges every rule, its test, and its possible output cons.

theorem cell_time_le (tc nc : ℕ) (w : Array T)
    (tbl : Array (Array (List N))) (r : ℕ)
    (htbl : ∀ i len, (lookup tbl i len).length ≤ r)
    (i len : ℕ) (rs : List (ContextFreeRule T N)) :
    (cell tc nc w tbl i len rs).time ≤
      1 + rs.length * (tc + 17 + len * (2 * r * (nc + 3) + 18))

Uses 4 · Used by 1

Statement usesCharged computation of one CYK cell · CYK table lookup with empty default cells

Proof usesProduction-output fit test for indexed CYK · Cost bound for the CYK production fit test

Used byCost bound for building one CYK row

TheoremCost bound for building one CYK row#✓fully proved

Row cost counts all starts, not only successful or distinct factors.

theorem row_time_le (tc nc : ℕ) (w : Array T)
    (tbl : Array (Array (List N))) (r : ℕ)
    (htbl : ∀ i len, (lookup tbl i len).length ≤ r)
    (len : ℕ) (rs : List (ContextFreeRule T N)) (i count : ℕ) :
    (row tc nc w tbl len rs i count).time ≤
      1 + count * (5 + rs.length *
        (tc + 17 + len * (2 * r * (nc + 3) + 18)))

Uses 4 · Used by 1

Statement usesCYK table lookup with empty default cells · Charged construction of one CYK row

Proof usesCharged computation of one CYK cell · Cost bound for computing one CYK cell

Used byCost bound for filling the indexed CYK table

TheoremCost bound for filling the indexed CYK table#✓fully proved

Table cost includes allocation, every row conversion and every update. The memory-size hypothesis needed for split costs is discharged internally.

theorem table_time_le (tc nc : ℕ) (w : Array T)
    (rs : List (ContextFreeRule T N)) (depth : ℕ) (hd : depth ≤ w.size) :
    (table tc nc w rs depth).time ≤ w.size + 4 + depth *
      (9 + (w.size + 1) * (7 + rs.length *
        (tc + 17 + w.size * (2 * rs.length * (nc + 3) + 18))))

Uses 4 · Used by 1

Statement usesCharged construction of the indexed CYK table

Proof usesEvery CYK table lookup is bounded by the rule count · Charged construction of one CYK row · Cost bound for building one CYK row

Used byExplicit cubic cost bound for indexed CYK

TheoremLength of a computed CYK row#✓fully proved

The linear row-conversion charge uses the actual number of entries.

theorem row_length (tc nc : ℕ) (w : Array T)
    (tbl : Array (Array (List N))) (len : ℕ)
    (rs : List (ContextFreeRule T N)) (i count : ℕ) :
    (row tc nc w tbl len rs i count).ret.length = count

Uses 1

Statement usesCharged construction of one CYK row

TheoremExact cost of the CYK epsilon scan#✓fully proved

Exact cost of the empty-input production scan.

theorem epsilon_time (nc : ℕ) (start : N)
    (rs : List (ContextFreeRule T N)) :
    (epsilon nc start rs).time = 1 + rs.length * (nc + 6)

Uses 1 · Used by 1

Statement usesCharged scan for start epsilon productions

Used byExplicit cubic cost bound for indexed CYK

TheoremExplicit cubic cost bound for indexed CYK#✓fully proved

Explicit cubic bound, for every word including the empty word. The coefficient depends only on the rule enumeration and equality costs; no semantic or assumed recurrence hypothesis occurs in this cost theorem.

theorem recognizes_time_le (tc nc : ℕ) (start : N)
    (rs : List (ContextFreeRule T N)) (w : List T) :
    (recognizes tc nc start rs w).time ≤
      (rs.length * (tc + nc + 2 * rs.length * (nc + 3) + 38) + 40) *
        (w.length + 1) ^ 3

Uses 9 · Used by 2

Statement usesCharged indexed CYK recognizer

Proof usesCharged scan for start epsilon productions · Exact cost of the CYK epsilon scan · CYK table lookup with empty default cells · Every CYK table lookup is bounded by the rule count · Charged list-membership scan · Exact cost of a membership scan · Charged construction of the indexed CYK table · Cost bound for filling the indexed CYK table

Used byIndexed CYK costs a constant times \(n^3\) on nonempty words · Cubic cost bound for indexed CYK on encoded grammars

TheoremIndexed CYK costs a constant times \(n^3\) on nonempty words#✓fully proved

In the usual nonempty-input form, the bound is a constant times n³.

theorem recognizes_time_le_cubic (tc nc : ℕ) (start : N)
    (rs : List (ContextFreeRule T N)) (w : List T) (hw : w ≠ []) :
    (recognizes tc nc start rs w).time ≤
      8 * (rs.length *
        (tc + nc + 2 * rs.length * (nc + 3) + 38) + 40) * w.length ^ 3

Uses 2

Statement usesCharged indexed CYK recognizer

Proof usesExplicit cubic cost bound for indexed CYK

12 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.