Context-free grammar to pushdown automaton

This file proves the grammar-to-automaton direction of the PDA = CFG equivalence. From a grammar G it builds the single-state PDA M G (state Q.loop, stack alphabet Symbol T G.NT, start symbol nonterminal G.initial) that simulates leftmost derivations: ε-moves replace a nonterminal by a rule right-hand side (M_consumes_nonterminal) and input-moves pop a matching terminal (M_consumes_terminal). The main result pda_of_cfg proves G.language = (M G).acceptsByEmptyStack, with the two inclusions given by M_reaches_off_G_derives and G_derives_of_M_reaches.

structure CFG_to_PDA.Q : Type

• loop :: (
• )

instance CFG_to_PDA.instFintypeQ : Fintype Q

Equations

• CFG_to_PDA.instFintypeQ = { elems := {{ }}, complete := ⋯ }

@[reducible, inline]

abbrev CFG_to_PDA.S {T : Type} (G : ContextFreeGrammar T) [Fintype G.NT] : Type

Equations

• CFG_to_PDA.S G = Symbol T G.NT

@[reducible, inline]

abbrev CFG_to_PDA.PDA' {T : Type} [Fintype T] (G : ContextFreeGrammar T) [Fintype G.NT] : Type

Equations

• CFG_to_PDA.PDA' G = PDA CFG_to_PDA.Q T (CFG_to_PDA.S G)

@[reducible, inline]

abbrev CFG_to_PDA.transition_fun {T : Type} [DecidableEq T] (G : ContextFreeGrammar T) [Fintype G.NT] : Q → (a : T) → (Z : S G) → Set (Q × List (S G))

Equations

• CFG_to_PDA.transition_fun G x✝ a (Symbol.terminal b) = if a = b then {({ }, [])} else ∅
• CFG_to_PDA.transition_fun G x✝ a Z = ∅

@[reducible, inline]

abbrev CFG_to_PDA.transition_fun' {T : Type} (G : ContextFreeGrammar T) [Fintype G.NT] : Q → (Z : S G) → Set (Q × List (S G))

Equations

• CFG_to_PDA.transition_fun' G x✝ (Symbol.nonterminal N) = {x : CFG_to_PDA.Q × List (CFG_to_PDA.S G) | ∃ (α : List (CFG_to_PDA.S G)) (_ : { input := N, output := α } ∈ G.rules), ({ }, α) = x}
• CFG_to_PDA.transition_fun' G x✝ Z = ∅

@[reducible, inline]

abbrev CFG_to_PDA.M {T : Type} [DecidableEq T] [Fintype T] (G : ContextFreeGrammar T) [Fintype G.NT] : PDA' G

Equations

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

theorem CFG_to_PDA.M_consumes_terminal {T : Type} [DecidableEq T] [Fintype T] {G : ContextFreeGrammar T} [Fintype G.NT] (a : T) (w : List T) (α : List (S G)) : PDA.ReachesIn 1 { state := { }, input := a :: w, stack := Symbol.terminal a :: α } { state := { }, input := w, stack := α }

theorem CFG_to_PDA.M_consumes_nonterminal {T : Type} [DecidableEq T] [Fintype T] {G : ContextFreeGrammar T} [Fintype G.NT] {r : ContextFreeRule T G.NT} (h : r ∈ G.rules) (w : List T) (α : List (S G)) : PDA.ReachesIn 1 { state := { }, input := w, stack := Symbol.nonterminal r.input :: α } { state := { }, input := w, stack := r.output ++ α }

theorem CFG_to_PDA.M_consumes_terminal_string {T : Type} [DecidableEq T] [Fintype T] {G : ContextFreeGrammar T} [Fintype G.NT] (w w' : List T) (α : List (S G)) : PDA.Reaches { state := { }, input := w ++ w', stack := List.map Symbol.terminal w ++ α } { state := { }, input := w', stack := α }

theorem CFG_to_PDA.G_rule_of_M_consumes_nonterminal {T : Type} [DecidableEq T] [Fintype T] {G : ContextFreeGrammar T} [Fintype G.NT] {w w' : List T} {α β : List (S G)} {N : G.NT} : PDA.ReachesIn 1 { state := { }, input := w, stack := Symbol.nonterminal N :: α } { state := { }, input := w', stack := β } → ∃ (γ : List (S G)), { input := N, output := γ } ∈ G.rules ∧ β = γ ++ α ∧ w = w'

theorem CFG_to_PDA.M_terminal_stack_of_read {T : Type} [DecidableEq T] [Fintype T] {G : ContextFreeGrammar T} [Fintype G.NT] (a : T) (w : List T) (α β : List (S G)) : PDA.ReachesIn 1 { state := { }, input := a :: w, stack := α } { state := { }, input := w, stack := β } → α = Symbol.terminal a :: β

theorem CFG_to_PDA.M_deterministic_step_of_terminal_stack_cons {T : Type} [DecidableEq T] [Fintype T] {G : ContextFreeGrammar T} [Fintype G.NT] (a : T) (w v : List T) (β β' : List (S G)) : PDA.ReachesIn 1 { state := { }, input := w, stack := Symbol.terminal a :: β } { state := { }, input := v, stack := β' } → w = a :: v ∧ β = β'

theorem CFG_to_PDA.M_deterministic_of_terminal_stack_cons {T : Type} [DecidableEq T] [Fintype T] {G : ContextFreeGrammar T} [Fintype G.NT] (a : T) (w : List T) (β : List (S G)) : PDA.Reaches { state := { }, input := w, stack := Symbol.terminal a :: β } { state := { }, input := [], stack := [] } → ∃ (w' : List T), w = a :: w' ∧ PDA.Reaches { state := { }, input := w', stack := β } { state := { }, input := [], stack := [] }

theorem CFG_to_PDA.M_deterministic_of_terminal_stack {T : Type} [DecidableEq T] [Fintype T] {G : ContextFreeGrammar T} [Fintype G.NT] (w v : List T) (β : List (S G)) : PDA.Reaches { state := { }, input := w, stack := List.map Symbol.terminal v ++ β } { state := { }, input := [], stack := [] } → ∃ (w' : List T), w = v ++ w' ∧ PDA.Reaches { state := { }, input := w', stack := β } { state := { }, input := [], stack := [] }

theorem CFG_to_PDA.M_reaches_off_G_derives {T : Type} [DecidableEq T] [Fintype T] {G : ContextFreeGrammar T} [Fintype G.NT] (α : List (Symbol T G.NT)) (w : List T) (h : G.DerivesLeftmost α (List.map Symbol.terminal w)) : PDA.Reaches { state := { }, input := w, stack := α } { state := { }, input := [], stack := [] }

theorem CFG_to_PDA.G_derives_of_M_reaches {T : Type} [DecidableEq T] [Fintype T] {G : ContextFreeGrammar T} [Fintype G.NT] {α : List (Symbol T G.NT)} {w : List T} (h : PDA.Reaches { state := { }, input := w, stack := α } { state := { }, input := [], stack := [] }) : G.Derives α (List.map Symbol.terminal w)

theorem CFG_to_PDA.pda_of_cfg {T : Type} [DecidableEq T] [Fintype T] (G : ContextFreeGrammar T) [Fintype G.NT] : G.language = PDA.acceptsByEmptyStack (M G)