Indexed CYK primitives

DefinitionCharged list-membership scan#✓fully proved

Full membership scan, charging equality and list/control operations.

def member (eqCost : ℕ) (a : N) : List N → TimeM ℕ Bool
  | [] => ⟨false, 1⟩
  | b :: bs =>
      let rest := member eqCost a bs
      ⟨decide (a = b) || rest.ret, rest.time + eqCost + 3⟩

Used by 8

Used byCorrectness of the indexed CYK recognizer · Exact cost of a membership scan · Explicit cubic cost bound for indexed CYK · Cost bound for the CYK split scan · Charged membership scan agrees with list membership · Charged indexed CYK recognizer · Charged scan of CYK split positions · Successful CYK split scans find a split in range

TheoremCharged membership scan agrees with list membership#✓fully proved

The charged scan has ordinary list-membership semantics.

@[simp] theorem member_ret (eqCost : ℕ) (a : N) (xs : List N) :
    (member eqCost a xs).ret = true ↔ a ∈ xs

Uses 1 · Used by 2

Statement usesCharged list-membership scan

Used byCorrectness of the indexed CYK recognizer · Successful CYK split scans find a split in range

DefinitionCYK table lookup with empty default cells#✓fully proved

Two bounded array reads; invalid indices denote an empty cell.

def lookup (tbl : Array (Array (List N))) (i len : ℕ) : List N :=
  (tbl[len]?.getD #[])[i]?.getD []

Used by 14

Used byCorrectness of one indexed CYK cell · New CYK table row holds the computed cells · CYK table update leaves other lengths' cells unchanged · Correctness of the indexed CYK recognizer · Correctness of the completed indexed CYK table · Cost bound for computing one CYK cell · Cost bound for the CYK production fit test · Every CYK table lookup is bounded by the rule count · Explicit cubic cost bound for indexed CYK · Cost bound for building one CYK row · Cost bound for the CYK split scan · Charged indexed CYK recognizer · Charged scan of CYK split positions · Successful CYK split scans find a split in range

DefinitionCharged scan of CYK split positions#✓fully proved

Scan split positions 1,...,count, with two table reads per split. The 16 units cover four array reads, bounds/default tests, index arithmetic, Boolean combinations and recursion control.

def splits (eqCost : ℕ) (tbl : Array (Array (List N)))
    (i len : ℕ) (b c : N) : ℕ → TimeM ℕ Bool
  | 0 => ⟨false, 1⟩
  | k + 1 =>
      let rest := splits eqCost tbl i len b c k
      let left := member eqCost b (lookup tbl i (k + 1))
      let right := member eqCost c (lookup tbl (i + (k + 1)) (len - (k + 1)))
      ⟨rest.ret || (left.ret && right.ret),
        rest.time + left.time + right.time + 16⟩

Uses 2 · Used by 5

Statement usesCYK table lookup with empty default cells · Charged list-membership scan

Used byCorrectness of one indexed CYK cell · Cost bound for the CYK production fit test · Cost bound for the CYK split scan · Production-output fit test for indexed CYK · Successful CYK split scans find a split in range

TheoremSuccessful CYK split scans find a split in range#✓fully proved

Every successful scan names a split in exactly the scanned interval.

theorem splits_ret (eqCost : ℕ) (tbl : Array (Array (List N)))
    (i len : ℕ) (b c : N) (count : ℕ) :
    (splits eqCost tbl i len b c count).ret = true ↔
      ∃ k, 0 < k ∧ k ≤ count ∧ b ∈ lookup tbl i k ∧
        c ∈ lookup tbl (i + k) (len - k)

Uses 4 · Used by 1

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

Proof usesCharged list-membership scan · Charged membership scan agrees with list membership

Used byCorrectness of one indexed CYK cell

DefinitionProduction-output fit test for indexed CYK#✓fully proved

Test a production output without constructing or comparing substrings. Pattern inspection is bounded (at most three cons and two symbol tags).

def fits (termCost ntCost : ℕ) (w : Array T)
    (tbl : Array (Array (List N))) (i len : ℕ) :
    List (Symbol T N) → TimeM ℕ Bool
  | [.terminal a] =>
      ⟨decide (len = 1) && decide (w[i]? = some a), termCost + 12⟩
  | [.nonterminal b, .nonterminal c] =>
      let r := splits ntCost tbl i len b c (len - 1)
      ⟨r.ret, r.time + 8⟩
  | _ => ⟨false, 8⟩

Uses 1 · Used by 6

Statement usesCharged scan of CYK split positions

Used byCorrectness of one indexed CYK cell · Computed CYK cell length bounded by the rule count · Cost bound for computing one CYK cell · Cost bound for the CYK production fit test · Charged computation of one CYK cell · CYK cell members come from scanned productions

DefinitionCharged computation of one CYK cell#✓fully proved

Scan every production once, retaining its input exactly when it fits. Duplicates are allowed; no set insertion or uncharged deduplication occurs.

def cell (termCost ntCost : ℕ) (w : Array T)
    (tbl : Array (Array (List N))) (i len : ℕ) :
    List (ContextFreeRule T N) → TimeM ℕ (List N)
  | [] => ⟨[], 1⟩
  | r :: rs =>
      let f := fits termCost ntCost w tbl i len r.output
      let rest := cell termCost ntCost w tbl i len rs
      ⟨if f.ret then r.input :: rest.ret else rest.ret,
        f.time + rest.time + 5⟩

Uses 1 · Used by 10

Statement usesProduction-output fit test for indexed CYK

Used byCorrectness of one indexed CYK cell · New CYK table row holds the computed cells · Indexing of a constructed CYK row · Correctness of the completed indexed CYK table · Computed CYK cell length bounded by the rule count · Cost bound for computing one CYK cell · Every CYK table lookup is bounded by the rule count · Cost bound for building one CYK row · CYK cell members come from scanned productions · Charged construction of one CYK row

TheoremCYK cell members come from scanned productions#✓fully proved

Membership in a computed cell names an actual scanned production.

theorem mem_cell (termCost ntCost : ℕ) (w : Array T)
    (tbl : Array (Array (List N))) (i len : ℕ)
    (rs : List (ContextFreeRule T N)) (a : N) :
    a ∈ (cell termCost ntCost w tbl i len rs).ret ↔
      ∃ r ∈ rs, r.input = a ∧
        (fits termCost ntCost w tbl i len r.output).ret = true

Uses 2 · Used by 1

Statement usesCharged computation of one CYK cell · Production-output fit test for indexed CYK

Used byCorrectness of one indexed CYK cell

DefinitionCharged construction of one CYK row#✓fully proved

Build one row in increasing start-position order. Each cell is evaluated once against the already completed shorter rows.

def row (termCost ntCost : ℕ) (w : Array T)
    (tbl : Array (Array (List N))) (len : ℕ)
    (rs : List (ContextFreeRule T N)) (i : ℕ) :
    ℕ → TimeM ℕ (List (List N))
  | 0 => ⟨[], 1⟩
  | count + 1 =>
      let c := cell termCost ntCost w tbl i len rs
      let rest := row termCost ntCost w tbl len rs (i + 1) count
      ⟨c.ret :: rest.ret, c.time + rest.time + 4⟩

Uses 1 · Used by 9

Statement usesCharged computation of one CYK cell

Used byNew CYK table row holds the computed cells · CYK table update leaves other lengths' cells unchanged · Indexing of a constructed CYK row · Indexed CYK table keeps its allocated size · Every CYK table lookup is bounded by the rule count · Length of a computed CYK row · Cost bound for building one CYK row · Cost bound for filling the indexed CYK table · Charged construction of the indexed CYK table

DefinitionCharged construction of the indexed CYK table#✓fully proved

Fill rows 1,...,depth in a fixed outer array of size w.size + 1. Row conversion is linear; the outer update is an indexed primitive.

def table (termCost ntCost : ℕ) (w : Array T)
    (rs : List (ContextFreeRule T N)) :
    ℕ → TimeM ℕ (Array (Array (List N)))
  | 0 => ⟨Array.replicate (w.size + 1) #[], w.size + 4⟩
  | depth + 1 =>
      let prev := table termCost ntCost w rs depth
      let next := row termCost ntCost w prev.ret (depth + 1) rs 0
        (w.size + 1)
      ⟨prev.ret.set! (depth + 1) next.ret.toArray,
        prev.time + next.time + 2 * (w.size + 1) + 8⟩

Uses 1 · Used by 9

Statement usesCharged construction of one CYK row

Used byNew CYK table row holds the computed cells · CYK table update leaves other lengths' cells unchanged · Correctness of the indexed CYK recognizer · Correctness of the completed indexed CYK table · Indexed CYK table keeps its allocated size · Every CYK table lookup is bounded by the rule count · Explicit cubic cost bound for indexed CYK · Cost bound for filling the indexed CYK table · Charged indexed CYK recognizer

DefinitionCharged scan for start epsilon productions#✓fully proved

Scan start epsilon rules; output emptiness is a single list-tag test.

def epsilon (ntCost : ℕ) (start : N) :
    List (ContextFreeRule T N) → TimeM ℕ Bool
  | [] => ⟨false, 1⟩
  | r :: rs =>
      let rest := epsilon ntCost start rs
      ⟨(decide (r.input = start) && r.output.isEmpty) || rest.ret,
        rest.time + ntCost + 6⟩

Used by 5

Used byCorrectness of the CYK epsilon scan · Correctness of the indexed CYK recognizer · Exact cost of the CYK epsilon scan · Explicit cubic cost bound for indexed CYK · Charged indexed CYK recognizer

DefinitionCharged indexed CYK recognizer#✓fully proved

The charged indexed recognizer. The nonempty branch pays for the input length scan, conversion, completed table, final lookup and membership.

def recognizes (termCost ntCost : ℕ) (start : N)
    (rs : List (ContextFreeRule T N)) (w : List T) : TimeM ℕ Bool :=
  match w with
  | [] =>
      let r := epsilon ntCost start rs
      ⟨r.ret, r.time + 1⟩
  | _ :: _ =>
      let a := w.toArray
      let tbl := table termCost ntCost a rs a.size
      let r := member ntCost start (lookup tbl.ret 0 a.size)
      ⟨r.ret, tbl.time + r.time + 3 * w.length + 12⟩

Uses 4 · Used by 7

Statement usesCharged scan for start epsilon productions · CYK table lookup with empty default cells · Charged list-membership scan · Charged construction of the indexed CYK table

Used byIndexed CYK agrees with the list-table CYK recognizer · Correctness of the indexed CYK recognizer · Explicit cubic cost bound for indexed CYK · Indexed CYK costs a constant times \(n^3\) on nonempty words · Indexed CYK recognizer for encoded grammars · Correctness of indexed CYK on encoded grammars · Cubic cost bound for indexed CYK on encoded grammars

12 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.