Indexed CYK for the canonical encoded grammar

DefinitionCharged decoding of encoded grammar symbols#✓fully proved

Decode symbols with a charge for each constructor test and output cons.

def decodeSymbols : List (ℕ ⊕ T) → TimeM ℕ (List (Symbol T ℕ))
  | [] => ⟨[], 1⟩
  | s :: ss =>
      let rest := decodeSymbols ss
      ⟨EncodedCFG.decodeSymbol s :: rest.ret, rest.time + 4⟩

Uses 1 · Used by 5

Statement usesDecoding a grammar symbol

Used byCharged decoding of encoded grammar rules · Charged rule decoding agrees with the decoded grammar · Exact cost of grammar rule decoding · Charged symbol decoding agrees with canonical decoding · Exact cost of grammar symbol decoding

TheoremCharged symbol decoding agrees with canonical decoding#✓fully proved

The charged conversion is exactly the canonical symbol decoding.

@[simp] theorem decodeSymbols_ret (ss : List (ℕ ⊕ T)) :
    (decodeSymbols ss).ret = ss.map EncodedCFG.decodeSymbol

Uses 2 · Used by 3

Statement usesCharged decoding of encoded grammar symbols · Decoding a grammar symbol

Used byCharged rule decoding agrees with the decoded grammar · Exact cost of grammar rule decoding · Exact cost of grammar symbol decoding

DefinitionCharged decoding of encoded grammar rules#✓fully proved

Decode every rule, charging all right-hand-side traversals.

def decodeRules : List (ℕ × List (ℕ ⊕ T)) →
    TimeM ℕ (List (ContextFreeRule T ℕ))
  | [] => ⟨[], 1⟩
  | r :: rs =>
      let out := decodeSymbols r.2
      let rest := decodeRules rs
      ⟨⟨r.1, out.ret⟩ :: rest.ret, out.time + rest.time + 5⟩

Uses 1 · Used by 5

Statement usesCharged decoding of encoded grammar symbols

Used byCharged rule decoding agrees with the decoded grammar · Exact cost of grammar rule decoding · Indexed CYK recognizer for encoded grammars · Correctness of indexed CYK on encoded grammars · Cubic cost bound for indexed CYK on encoded grammars

TheoremCharged rule decoding agrees with the decoded grammar#✓fully proved

The charged rule conversion agrees with the existing decoded grammar.

@[simp] theorem decodeRules_ret (rs : List (ℕ × List (ℕ ⊕ T))) :
    (decodeRules rs).ret = rs.map EncodedCFG.decodeRule

Uses 5 · Used by 3

Statement usesCharged decoding of encoded grammar rules · Decoding a production

Proof usesCharged decoding of encoded grammar symbols · Charged symbol decoding agrees with canonical decoding · Decoding a grammar symbol

Used byExact cost of grammar rule decoding · Correctness of indexed CYK on encoded grammars · Cubic cost bound for indexed CYK on encoded grammars

DefinitionIndexed CYK recognizer for encoded grammars#✓fully proved

Run indexed CYK on the existing encoded grammar, including preparation.

def recognizesEncoded [DecidableEq T] (tc nc : ℕ) (g : EncodedCFG T)
    (w : List T) : TimeM ℕ Bool :=
  let rules := decodeRules g.rules
  let result := recognizes tc nc g.start rules.ret w
  ⟨result.ret, rules.time + result.time + 3⟩

Uses 3 · Used by 2

Statement usesCharged decoding of encoded grammar rules · Charged indexed CYK recognizer · Encoded context-free grammars

Used byCorrectness of indexed CYK on encoded grammars · Cubic cost bound for indexed CYK on encoded grammars

TheoremCorrectness of indexed CYK on encoded grammars#✓fully proved

Correctness for the canonical encoded language, including epsilon.

theorem recognizesEncoded_iff [DecidableEq T] (tc nc : ℕ)
    (g : EncodedCFG T) (hg : IsChomskyNormalForm g.toCFG) (w : List T) :
    (recognizesEncoded tc nc g w).ret = true ↔ w ∈ g.language

Uses 10

Statement usesIndexed CYK recognizer for encoded grammars · Encoded context-free grammars · Language of an encoded grammar · Grammar denoted by an encoding · Chomsky normal form

Proof usesCharged decoding of encoded grammar rules · Charged rule decoding agrees with the decoded grammar · Charged indexed CYK recognizer · Correctness of the indexed CYK recognizer · Decoding a production

TheoremExact cost of grammar symbol decoding#✓fully proved

Exact symbol-decoding traversal cost.

theorem decodeSymbols_time (ss : List (ℕ ⊕ T)) :
    (decodeSymbols ss).time = 1 + 4 * ss.length

Uses 3 · Used by 1

Statement usesCharged decoding of encoded grammar symbols

Proof usesCharged symbol decoding agrees with canonical decoding · Decoding a grammar symbol

Used byExact cost of grammar rule decoding

TheoremExact cost of grammar rule decoding#✓fully proved

Exact grammar-preparation cost, including all production symbols.

theorem decodeRules_time (rs : List (ℕ × List (ℕ ⊕ T))) :
    (decodeRules rs).time =
      1 + 6 * rs.length + 4 * (rs.map (fun r => r.2.length)).sum

Uses 7 · Used by 1

Statement usesCharged decoding of encoded grammar rules

Proof usesCharged rule decoding agrees with the decoded grammar · Charged decoding of encoded grammar symbols · Charged symbol decoding agrees with canonical decoding · Exact cost of grammar symbol decoding · Decoding a production · Decoding a grammar symbol

Used byCubic cost bound for indexed CYK on encoded grammars

TheoremCubic cost bound for indexed CYK on encoded grammars#✓fully proved

Cubic word-length bound including canonical grammar preparation. All dependence on the fixed grammar and symbol-equality model is explicit.

theorem recognizesEncoded_time_le [DecidableEq T] (tc nc : ℕ)
    (g : EncodedCFG T) (w : List T) :
    (recognizesEncoded tc nc g w).time ≤
      (g.rules.length * (tc + nc + 2 * g.rules.length * (nc + 3) + 44) +
        4 * (g.rules.map (fun r => r.2.length)).sum + 44) *
          (w.length + 1) ^ 3

Uses 8

Statement usesIndexed CYK recognizer for encoded grammars · Encoded context-free grammars

Proof usesCharged decoding of encoded grammar rules · Charged rule decoding agrees with the decoded grammar · Exact cost of grammar rule decoding · Charged indexed CYK recognizer · Explicit cubic cost bound for indexed CYK · Decoding a production

9 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.