Correctness of the buffered canonical LR machine

The lemmas in this file relate stable parser controls of the concrete marked DPDA to the grammar-symbol-stack semantics of CanonicalParser.

def CF_grammar.LRk.Buffered.stableConfig {T : Type} [Fintype T] (G : CF_grammar T) (k : ℕ) (hk : 0 < k) (c : CanonicalParser.Config T G) : (machine G k hk).toPDA.conf

Concrete machine configuration corresponding to a stable canonical parser configuration.

Equations

• One or more equations did not get rendered due to their size.

theorem CF_grammar.LRk.Buffered.machine_reaches_of_canonical {T : Type} [Fintype T] (G : CF_grammar T) (k : ℕ) (hk : 0 < k) {c d : CanonicalParser.Config T G} (h : CanonicalParser.Reaches G k c d) : PDA.Reaches (stableConfig G k hk c) (stableConfig G k hk d)

Canonical reachability is simulated by the concrete DPDA.

theorem CF_grammar.LRk.Buffered.marked_machine_accepts_of_canonical {T : Type} [Fintype T] (G : CF_grammar T) (k : ℕ) (hk : 0 < k) {w : List T} (h : CanonicalParser.Accepts G k w) : List.map some w ++ [none] ∈ (machine G k hk).acceptsByFinalState

Canonical acceptance implies acceptance of the explicitly endmarked word by the concrete DPDA.

theorem CF_grammar.LRk.Buffered.canonical_of_marked_machine_accepts {T : Type} [Fintype T] (G : CF_grammar T) (k : ℕ) (hk : 0 < k) {w : List T} (h : List.map some w ++ [none] ∈ (machine G k hk).acceptsByFinalState) : CanonicalParser.Accepts G k w

Acceptance of a properly endmarked word by the concrete machine yields a canonical accepting run.

theorem CF_grammar.LRk.Buffered.marked_machine_correct {T : Type} [Fintype T] (G : CF_grammar T) (k : ℕ) (hk : 0 < k) (hLR : G.IsLRk k) (w : List T) : List.map some w ++ [none] ∈ (machine G k hk).acceptsByFinalState ↔ w ∈ CF_language G

On properly endmarked inputs, the concrete machine recognizes exactly the language of its LR(k) grammar.