The finite canonical viable-prefix automaton

Starting from the augmented kernel, scanKernel follows canonical goto edges over a grammar-symbol prefix. Actions are taken from its epsilon closure. The main theorem here is the soundness half of the viable-prefix theorem: every item reached after scanning gamma is semantically valid at gamma.

noncomputable def CF_grammar.LRk.scanKernel {T : Type} [Fintype T] (G : CF_grammar T) (k : ℕ) : List (symbol T G.augment.nt) → Finset (Item G.augment k)

Raw canonical kernel after scanning a grammar-symbol word. Closure is performed by goto before every dot advancement, and once more when the state is inspected.

Equations

• CF_grammar.LRk.scanKernel G k = List.foldl (CF_grammar.LRk.goto G.augment k) (CF_grammar.LRk.startKernel G k)

noncomputable def CF_grammar.LRk.itemState {T : Type} [Fintype T] (G : CF_grammar T) (k : ℕ) (gamma : List (symbol T G.augment.nt)) : Finset (Item G.augment k)

The closed canonical item state after scanning gamma.

Equations

• CF_grammar.LRk.itemState G k gamma = CF_grammar.LRk.closure G.augment k (CF_grammar.LRk.scanKernel G k gamma)

@[simp]

theorem CF_grammar.LRk.scanKernel_nil {T : Type} [Fintype T] (G : CF_grammar T) (k : ℕ) : scanKernel G k [] = startKernel G k

@[simp]

theorem CF_grammar.LRk.scanKernel_append {T : Type} [Fintype T] (G : CF_grammar T) (k : ℕ) (gamma delta : List (symbol T G.augment.nt)) : scanKernel G k (gamma ++ delta) = List.foldl (goto G.augment k) (scanKernel G k gamma) delta

@[simp]

theorem CF_grammar.LRk.scanKernel_append_singleton {T : Type} [Fintype T] (G : CF_grammar T) (k : ℕ) (gamma : List (symbol T G.augment.nt)) (X : symbol T G.augment.nt) : scanKernel G k (gamma ++ [X]) = goto G.augment k (scanKernel G k gamma) X

@[simp]

theorem CF_grammar.LRk.itemState_nil {T : Type} [Fintype T] (G : CF_grammar T) (k : ℕ) : itemState G k [] = closure G.augment k (startKernel G k)

theorem CF_grammar.LRk.itemState_valid {T : Type} [Fintype T] (G : CF_grammar T) (k : ℕ) (gamma : List (symbol T G.augment.nt)) {i : Item G.augment k} (hi : i ∈ itemState G k gamma) : Valid G.augment k gamma i

Every item in a canonical state is semantically valid for the scanned prefix.