LanglibPushdown automaton to context-free grammar #
This file proves the automaton-to-grammar direction of the PDA = CFG equivalence.
From a PDA M it builds the grammar G M whose nonterminals (N) are the triples
N.single q Z p and bounded lists N.list q α p, together with a start symbol
N.start. The triple q Z p derives exactly the inputs along which M goes from
state q to state p while net-popping the single stack symbol Z; the bound
max_push M on stack pushes keeps the rule set finite. The main result cfg_of_pda
proves (G M).language = M.acceptsByEmptyStack, via derives_of_reachesIn and
reachesIn_of_derivesLeftmostIn (both by strong induction on the step count).
@[reducible, inline]
abbrev
PDA_to_CFG.AllStackPushes
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
(M : PDA Q T S)
:
Equations
- PDA_to_CFG.AllStackPushes M = (Prod.snd '' ⋃ (q : Q), ⋃ (a : T), ⋃ (Z : S), M.transition_fun q a Z) ∪ Prod.snd '' ⋃ (q : Q), ⋃ (Z : S), M.transition_fun' q Z
Instances For
theorem
PDA_to_CFG.allStackPushes_finite
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
(M : PDA Q T S)
:
(AllStackPushes M).Finite
@[reducible, inline]
Equations
- PDA_to_CFG.N.start.IsAllowed = True
- (PDA_to_CFG.N.single a a_1 a_2).IsAllowed = True
- (PDA_to_CFG.N.list a α a_1).IsAllowed = (↑α.length ≤ PDA_to_CFG.max_push M)
Instances For
@[reducible, inline]
abbrev
PDA_to_CFG.compute_rule
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : PDA Q T S}
(q p : Q)
(a : T)
(Z : S)
:
Set (ContextFreeRule T (N M))
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
abbrev
PDA_to_CFG.compute_rule'
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : PDA Q T S}
(q p : Q)
(Z : S)
:
Set (ContextFreeRule T (N M))
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
abbrev
PDA_to_CFG.split_rule
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : PDA Q T S}
(q₁ : Q)
(n : N M)
:
Set (ContextFreeRule T (N M))
Equations
- One or more equations did not get rendered due to their size.
- PDA_to_CFG.split_rule q₁ PDA_to_CFG.N.start = ∅
- PDA_to_CFG.split_rule q₁ (PDA_to_CFG.N.single a a_1 a_2) = ∅
- PDA_to_CFG.split_rule q₁ (PDA_to_CFG.N.list a [] a_1) = ∅
Instances For
@[reducible, inline]
abbrev
PDA_to_CFG.start_rule
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : PDA Q T S}
(q : Q)
:
Set (ContextFreeRule T (N M))
Equations
- PDA_to_CFG.start_rule q = {{ input := PDA_to_CFG.N.start, output := [Symbol.nonterminal (PDA_to_CFG.N.list M.initial_state [M.start_symbol] q)] }}
Instances For
@[reducible, inline]
abbrev
PDA_to_CFG.RuleSet
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : PDA Q T S}
:
Set (ContextFreeRule T (N M))
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
abbrev
PDA_to_CFG.rules
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : PDA Q T S}
:
Finset (ContextFreeRule T (N M))
Equations
Instances For
@[reducible, inline]
Equations
- PDA_to_CFG.G M = { NT := PDA_to_CFG.N M, initial := PDA_to_CFG.N.start, rules := PDA_to_CFG.rules }
Instances For
theorem
PDA_to_CFG.produces_split
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : PDA Q T S}
(q q₁ p : Q)
{α : List S}
{Z : S}
(h : ↑(Z :: α).length ≤ max_push M)
:
(G M).Produces [Symbol.nonterminal (N.list q (Z :: α) p)]
[Symbol.nonterminal (N.single q Z q₁), Symbol.nonterminal (N.list q₁ α p)]
theorem
PDA_to_CFG.produces_compute
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : PDA Q T S}
{q q₁ p : Q}
{α : List S}
{a : T}
{Z : S}
(h : (q₁, α) ∈ M.transition_fun q a Z)
:
(G M).Produces [Symbol.nonterminal (N.single q Z p)] [Symbol.terminal a, Symbol.nonterminal (N.list q₁ α p)]
theorem
PDA_to_CFG.derives_of_reachesIn
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : PDA Q T S}
{γ : List S}
{q p : Q}
{x : List T}
{n : ℕ}
(hγ : ↑γ.length ≤ max_push M)
(h : PDA.ReachesIn n { state := q, input := x, stack := γ } { state := p, input := [], stack := [] })
:
(G M).Derives [Symbol.nonterminal (N.list q γ p)] (List.map Symbol.terminal x)
theorem
PDA_to_CFG.produces_cons
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : PDA Q T S}
{q p : Q}
{Z : S}
{γ : List S}
{u : List (Symbol T (N M))}
(h : (G M).ProducesLeftmost [Symbol.nonterminal (N.list q (Z :: γ) p)] u)
:
∃ (q₁ : Q), u = [Symbol.nonterminal (N.single q Z q₁), Symbol.nonterminal (N.list q₁ γ p)]
theorem
PDA_to_CFG.produces_single
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : PDA Q T S}
{q p : Q}
{Z : S}
{u v : List (Symbol T (N M))}
(h : (G M).ProducesLeftmost (Symbol.nonterminal (N.single q Z p) :: v) u)
:
(∃ (α : List S) (q₀ : Q) (a : T),
(q₀, α) ∈ M.transition_fun q a Z ∧ u = Symbol.terminal a :: Symbol.nonterminal (N.list q₀ α p) :: v) ∨ ∃ (α : List S) (q₀ : Q), (q₀, α) ∈ M.transition_fun' q Z ∧ u = Symbol.nonterminal (N.list q₀ α p) :: v
theorem
PDA_to_CFG.produces_start
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : PDA Q T S}
{u : List (Symbol T (N M))}
(h : (G M).ProducesLeftmost [Symbol.nonterminal N.start] u)
:
∃ (q : Q), u = [Symbol.nonterminal (N.list M.initial_state [M.start_symbol] q)]
theorem
PDA_to_CFG.reachesIn_of_derivesLeftmostIn
{Q T S : Type}
[Fintype Q]
[Fintype T]
[Fintype S]
{M : PDA Q T S}
{γ : List S}
{q p : Q}
{x : List T}
{n : ℕ}
(hγ : ↑γ.length ≤ max_push M)
(h : (G M).DerivesLeftmostIn [Symbol.nonterminal (N.list q γ p)] (List.map Symbol.terminal x) n)
: