Earley parser

StructureEarley item#✓fully proved

An Earley item: a production with a dot after dot symbols of its output, recognizing input that starts at the end of pre and whose recognized prefix is consumed. The full input is pre ++ consumed ++ rest for some rest.

structure EarleyItem (T : Type*) (N : Type*) where
  /-- The production whose right-hand side is being recognized. -/
  rule : ContextFreeRule T N
  /-- How many symbols of `rule.output` have been recognized so far. -/
  dot : ℕ
  /-- The input consumed before the origin of this item. -/
  pre : List T
  /-- The input consumed by the recognized prefix `rule.output.take dot`. -/
  consumed : List T
Used by 3
Used byAcceptance by the Earley recognizer · Correctness of the Earley recognizer · Earley chart as a predicate on items

InductiveEarley chart#✓fully proved

The Earley chart for input w: the least set of items closed under initialization, prediction, scanning, and completion.

Cslib.Language.EarleyChart · 24 lines 
inductive EarleyChart (g : ContextFreeGrammar T) (w : List T) :
    ContextFreeRule T g.NT → ℕ → List T → List T → Prop
  | init {r : ContextFreeRule T g.NT} (hr : r ∈ g.rules)
      (hinit : r.input = g.initial) :
      EarleyChart g w r 0 [] []
  | predict {r : ContextFreeRule T g.NT} {k : ℕ} {pre consumed : List T}
      (h : EarleyChart g w r k pre consumed) {A : g.NT}
      (hnext : r.output[k]? = some (Symbol.nonterminal A))
      {r' : ContextFreeRule T g.NT} (hr' : r' ∈ g.rules)
      (hinput : r'.input = A) :
      EarleyChart g w r' 0 (pre ++ consumed) []
  | scan {r : ContextFreeRule T g.NT} {k : ℕ} {pre consumed : List T}
      (h : EarleyChart g w r k pre consumed) {a : T}
      (hnext : r.output[k]? = some (Symbol.terminal a)) {rest : List T}
      (hw : w = pre ++ consumed ++ a :: rest) :
      EarleyChart g w r (k + 1) pre (consumed ++ [a])
  | complete {r : ContextFreeRule T g.NT} {k : ℕ} {pre consumed : List T}
      (h : EarleyChart g w r k pre consumed) {A : g.NT}
      (hnext : r.output[k]? = some (Symbol.nonterminal A))
      {r' : ContextFreeRule T g.NT} {consumed' : List T}
      (hr' : r' ∈ g.rules) (hinput : r'.input = A)
      (hcomp : EarleyChart g w r' r'.output.length (pre ++ consumed)
        consumed') :
      EarleyChart g w r (k + 1) pre (consumed ++ consumed')
Sources
  • Earley, "An efficient context-free parsing algorithm", Communications of the ACM 13 (1970), 94-102.
Used by 5
Used byEarley item dot stays within its production · Correctness of the Earley recognizer · Completeness of the Earley chart · Earley chart as a predicate on items · Soundness of the Earley chart

DefinitionEarley chart as a predicate on items#✓fully proved

The chart as a predicate on EarleyItems.

def EarleyChartItem (g : ContextFreeGrammar T) (w : List T)
    (item : EarleyItem T g.NT) : Prop :=
  EarleyChart g w item.rule item.dot item.pre item.consumed
Sources
  • Earley, "An efficient context-free parsing algorithm", Communications of the ACM 13 (1970), 94-102.
Uses 2 · Used by 2
Statement usesEarley chart · Earley item
Used byAcceptance by the Earley recognizer · Correctness of the Earley recognizer

DefinitionAcceptance by the Earley recognizer#✓fully proved

Acceptance by the Earley recognizer: some completed item for a production of the initial nonterminal consumes the whole input.

def earleyAccepts (g : ContextFreeGrammar T) (w : List T) : Prop :=
  ∃ (r : ContextFreeRule T g.NT), r ∈ g.rules ∧ r.input = g.initial ∧
    EarleyChartItem g w ⟨r, r.output.length, [], w⟩
Sources
  • Earley, "An efficient context-free parsing algorithm", Communications of the ACM 13 (1970), 94-102.
Uses 2 · Used by 1
Statement usesEarley chart as a predicate on items · Earley item
Used byCorrectness of the Earley recognizer

TheoremEarley item dot stays within its production#✓fully proved

The dot of a chart item never passes the end of its production.

theorem dot_le_of_earleyChart {w : List T} {r : ContextFreeRule T g.NT}
    {k : ℕ} {pre consumed : List T}
    (h : EarleyChart g w r k pre consumed) : k ≤ r.output.length
Sources
  • Earley, "An efficient context-free parsing algorithm", Communications of the ACM 13 (1970), 94-102.
Uses 1 · Used by 1
Statement usesEarley chart
Used byCompleteness of the Earley chart

TheoremSoundness of the Earley chart#✓fully proved

Soundness: the recognized prefix of a chart item yields the input it consumed.

theorem yields_take_of_earleyChart {w : List T} {r : ContextFreeRule T g.NT}
    {k : ℕ} {pre consumed : List T}
    (h : EarleyChart g w r k pre consumed) :
    Yields g (r.output.take k) consumed
Sources
  • Earley, "An efficient context-free parsing algorithm", Communications of the ACM 13 (1970), 94-102.
Uses 4 · Used by 1
Statement usesEarley chart · Yield of a sentential form
Proof usesConcatenation of yields · Yield through one production
Used byCorrectness of the Earley recognizer

TheoremCompleteness of the Earley chart#✓fully proved

Completeness: if a chart item waits on a sentential form and that form yields a word fitting in the remaining input, the chart contains the item completed by that word.

theorem earleyChart_complete_of_yields {w : List T}
    {α : List (Symbol T g.NT)} {u : List T} (h : Yields g α u) :
    ∀ {ρ : ContextFreeRule T g.NT} {k : ℕ} {pre consumed : List T}
      {rest : List T},
      EarleyChart g w ρ k pre consumed → ρ.output.drop k = α →
      w = pre ++ consumed ++ u ++ rest →
      EarleyChart g w ρ ρ.output.length pre (consumed ++ u)
Sources
  • Earley, "An efficient context-free parsing algorithm", Communications of the ACM 13 (1970), 94-102.
Uses 3 · Used by 1
Statement usesEarley chart · Yield of a sentential form
Proof usesEarley item dot stays within its production
Used byCorrectness of the Earley recognizer

TheoremA yield from one nonterminal starts with one of its productions#✓fully proved

Inversion of a yield from a single nonterminal: it begins with one production of that nonterminal.

theorem exists_rule_of_yields_singleton {A : g.NT} {w : List T}
    (h : Yields g [Symbol.nonterminal A] w) :
    ∃ (r : ContextFreeRule T g.NT), r ∈ g.rules ∧ r.input = A ∧
      Yields g r.output w
Sources
  • Earley, "An efficient context-free parsing algorithm", Communications of the ACM 13 (1970), 94-102.
Uses 1 · Used by 1
Statement usesYield of a sentential form
Used byCorrectness of the Earley recognizer

TheoremCorrectness of the Earley recognizer#✓fully proved

The Earley recognizer accepts exactly the grammar's language.

theorem earleyAccepts_iff {w : List T} :
    earleyAccepts g w ↔ w ∈ g.language
Sources
  • Earley, "An efficient context-free parsing algorithm", Communications of the ACM 13 (1970), 94-102.
Uses 10
Statement usesAcceptance by the Earley recognizer
Proof usesEarley chart · Earley chart as a predicate on items · Earley item · Yield of a sentential form · Completeness of the Earley chart · A yield from one nonterminal starts with one of its productions · Language membership through yields · Yield through one production · Soundness of the Earley chart
9 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.