noncomputable def PDA_FS_to_ES_eps {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : PDA Q T S) : Q ⊕ Fin 2 → Option S → Set ((Q ⊕ Fin 2) × List (Option S))

ε-transition function for the FS→ES PDA conversion. Defined as a top-level function to ensure good definitional reduction.

Equations

• PDA_FS_to_ES_eps M (Sum.inr 0) none = {(Sum.inl M.initial_state, [some M.start_symbol, none])}
• PDA_FS_to_ES_eps M (Sum.inl q) (some s) = (fun (p : Q × List S) => (Sum.inl p.1, List.map some p.2)) '' M.transition_fun' q s ∪ if q ∈ M.final_states then {(Sum.inr 1, [])} else ∅
• PDA_FS_to_ES_eps M (Sum.inl q) none = if q ∈ M.final_states then {(Sum.inr 1, [])} else ∅
• PDA_FS_to_ES_eps M (Sum.inr 1) x✝ = {(Sum.inr 1, [])}
• PDA_FS_to_ES_eps M (Sum.inr 0) (some val) = ∅

noncomputable def PDA_FS_to_ES_trans {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : PDA Q T S) : Q ⊕ Fin 2 → T → Option S → Set ((Q ⊕ Fin 2) × List (Option S))

Input-reading transition function for the FS→ES PDA conversion.

Equations

• PDA_FS_to_ES_trans M (Sum.inl q) x✝ (some s) = (fun (p : Q × List S) => (Sum.inl p.1, List.map some p.2)) '' M.transition_fun q x✝ s
• PDA_FS_to_ES_trans M x✝² x✝¹ x✝ = ∅

noncomputable def PDA_FS_to_ES_pda {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : PDA Q T S) : PDA (Q ⊕ Fin 2) T (Option S)

The PDA that converts final-state acceptance to empty-stack acceptance.

Equations

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

def liftConf {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : PDA Q T S) (c : M.conf) : (PDA_FS_to_ES_pda M).conf

Lifting a configuration from the original PDA to the new PDA.

Equations

• liftConf M c = { state := Sum.inl c.state, input := c.input, stack := List.map some c.stack ++ [none] }

theorem simulation_step {T : Type} [Fintype T] {Q S : Type} [Fintype Q] [Fintype S] (M : PDA Q T S) (r₁ r₂ : M.conf) (h : PDA.Reaches₁ r₁ r₂) : PDA.Reaches₁ (liftConf M r₁) (liftConf M r₂)

theorem simulation_reaches {T : Type} [Fintype T] {Q S : Type} [Fintype Q] [Fintype S] (M : PDA Q T S) (r₁ r₂ : M.conf) (h : PDA.Reaches r₁ r₂) : PDA.Reaches (liftConf M r₁) (liftConf M r₂)

Multi-step simulation: if M reaches r₂ from r₁, then M' reaches lift(r₂) from lift(r₁).

theorem drain_reaches {T : Type} [Fintype T] {Q S : Type} [Fintype Q] [Fintype S] (M : PDA Q T S) (γ : List (Option S)) : PDA.Reaches { state := Sum.inr 1, input := [], stack := γ } { state := Sum.inr 1, input := [], stack := [] }

theorem PDA_FS_to_ES_forward {T : Type} [Fintype T] {Q S : Type} [Fintype Q] [Fintype S] (M : PDA Q T S) (w : List T) (h : w ∈ M.acceptsByFinalState) : w ∈ (PDA_FS_to_ES_pda M).acceptsByEmptyStack

theorem reverse_simulation_step {T : Type} [Fintype T] {Q S : Type} [Fintype Q] [Fintype S] (M : PDA Q T S) (q₁ q₂ : Q) (w₁ w₂ : List T) (γ₁ γ₂ : List S) (h : PDA.Reaches₁ { state := Sum.inl q₁, input := w₁, stack := List.map some γ₁ } { state := Sum.inl q₂, input := w₂, stack := List.map some γ₂ }) : PDA.Reaches₁ { state := q₁, input := w₁, stack := γ₁ } { state := q₂, input := w₂, stack := γ₂ }

def FSES_Inv {T : Type} [Fintype T] {Q S : Type} [Fintype Q] [Fintype S] (M : PDA Q T S) (w : List T) (c : (PDA_FS_to_ES_pda M).conf) : Prop

Invariant for configurations reachable from the initial config of the FS→ES PDA. Every such configuration is either: (1) the initial config (inr 0, w, [none]) (2) a simulation of M: (inl q, w', γ.map some ++ [none]) with M.Reaches ⟨M.initial_state, w, [M.start_symbol]⟩ ⟨q, w', γ⟩ (3) the drain state (inr 1, ...) with a witness that some final state of M was reached on empty input.

Equations

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

theorem FSES_Inv_init {T : Type} [Fintype T] {Q S : Type} [Fintype Q] [Fintype S] (M : PDA Q T S) (w : List T) : FSES_Inv M w { state := Sum.inr 0, input := w, stack := [none] }

The invariant holds for the initial configuration.

theorem FSES_Inv_step {T : Type} [Fintype T] {Q S : Type} [Fintype Q] [Fintype S] (M : PDA Q T S) (w : List T) (c₁ c₂ : (PDA_FS_to_ES_pda M).conf) (h_inv : FSES_Inv M w c₁) (h_step : PDA.Reaches₁ c₁ c₂) : FSES_Inv M w c₂

theorem FSES_Inv_reaches {T : Type} [Fintype T] {Q S : Type} [Fintype Q] [Fintype S] (M : PDA Q T S) (w : List T) (c₁ c₂ : (PDA_FS_to_ES_pda M).conf) (h_inv : FSES_Inv M w c₁) (h_reach : PDA.Reaches c₁ c₂) : FSES_Inv M w c₂

The invariant is preserved by multi-step reachability.

theorem FSES_Inv_terminal {T : Type} [Fintype T] {Q S : Type} [Fintype Q] [Fintype S] (M : PDA Q T S) (w : List T) (q : Q ⊕ Fin 2) (h_inv : FSES_Inv M w { state := q, input := [], stack := [] }) : w ∈ M.acceptsByFinalState

theorem PDA_FS_to_ES_backward {T : Type} [Fintype T] {Q S : Type} [Fintype Q] [Fintype S] (M : PDA Q T S) (w : List T) (h : w ∈ (PDA_FS_to_ES_pda M).acceptsByEmptyStack) : w ∈ M.acceptsByFinalState

Backward direction of PDA_FS_subset_ES.

theorem PDA_FS_subset_ES {T : Type} [Fintype T] {Q S : Type} [Fintype Q] [Fintype S] (M : PDA Q T S) : PDA.is_PDA M.acceptsByFinalState

Any PDA final-state language is also a PDA empty-stack language.

Empty-stack acceptance ⊆ Final-state acceptance

Given a PDA M that accepts by empty stack, we construct a new PDA M' that accepts by final state, recognising the same language.

The construction adds:

• A new initial state Sum.inr 0 that pushes M's start symbol on top of a fresh bottom marker.
• A new accepting state Sum.inr 1 that is entered whenever the simulated M empties its original stack (i.e. the bottom marker is exposed).

noncomputable def PDA_ES_to_FS_eps {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : PDA Q T S) : Q ⊕ Fin 2 → Option S → Set ((Q ⊕ Fin 2) × List (Option S))

ε-transition function for the ES→FS PDA conversion.

Equations

• PDA_ES_to_FS_eps M (Sum.inr 0) none = {(Sum.inl M.initial_state, [some M.start_symbol, none])}
• PDA_ES_to_FS_eps M (Sum.inl q) (some s) = (fun (p : Q × List S) => (Sum.inl p.1, List.map some p.2)) '' M.transition_fun' q s
• PDA_ES_to_FS_eps M (Sum.inl q) none = {(Sum.inr 1, [])}
• PDA_ES_to_FS_eps M (Sum.inr 1) x✝ = ∅
• PDA_ES_to_FS_eps M (Sum.inr 0) (some val) = ∅

noncomputable def PDA_ES_to_FS_trans {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : PDA Q T S) : Q ⊕ Fin 2 → T → Option S → Set ((Q ⊕ Fin 2) × List (Option S))

Input-reading transition function for the ES→FS PDA conversion.

Equations

• PDA_ES_to_FS_trans M (Sum.inl q) x✝ (some s) = (fun (p : Q × List S) => (Sum.inl p.1, List.map some p.2)) '' M.transition_fun q x✝ s
• PDA_ES_to_FS_trans M x✝² x✝¹ x✝ = ∅

noncomputable def PDA_ES_to_FS_pda {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : PDA Q T S) : PDA (Q ⊕ Fin 2) T (Option S)

The PDA that converts empty-stack acceptance to final-state acceptance.

Equations

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

def liftConf_ES {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : PDA Q T S) (c : M.conf) : (PDA_ES_to_FS_pda M).conf

Lifting a configuration from the original PDA to the ES→FS PDA.

Equations

• liftConf_ES M c = { state := Sum.inl c.state, input := c.input, stack := List.map some c.stack ++ [none] }

theorem ES_simulation_step {T : Type} [Fintype T] {Q S : Type} [Fintype Q] [Fintype S] (M : PDA Q T S) (r₁ r₂ : M.conf) (h : PDA.Reaches₁ r₁ r₂) : PDA.Reaches₁ (liftConf_ES M r₁) (liftConf_ES M r₂)

theorem ES_simulation_reaches {T : Type} [Fintype T] {Q S : Type} [Fintype Q] [Fintype S] (M : PDA Q T S) (r₁ r₂ : M.conf) (h : PDA.Reaches r₁ r₂) : PDA.Reaches (liftConf_ES M r₁) (liftConf_ES M r₂)

Multi-step simulation: if M reaches r₂ from r₁, then the ES→FS PDA reaches lift(r₂) from lift(r₁).

theorem PDA_ES_to_FS_forward {T : Type} [Fintype T] {Q S : Type} [Fintype Q] [Fintype S] (M : PDA Q T S) (w : List T) (h : w ∈ M.acceptsByEmptyStack) : w ∈ (PDA_ES_to_FS_pda M).acceptsByFinalState

def ESFS_Inv {T : Type} [Fintype T] {Q S : Type} [Fintype Q] [Fintype S] (M : PDA Q T S) (w : List T) (c : (PDA_ES_to_FS_pda M).conf) : Prop

Invariant for configurations reachable from the initial config of the ES→FS PDA. Every such configuration is either: (1) the initial config (inr 0, w, [none]) (2) a simulation of M: (inl q, w', γ.map some ++ [none]) with M.Reaches ⟨M.initial_state, w, [M.start_symbol]⟩ ⟨q, w', γ⟩ (3) the accepting state (inr 1, w', []) with a witness that M reached empty stack on some suffix.

Equations

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

theorem ESFS_Inv_init {T : Type} [Fintype T] {Q S : Type} [Fintype Q] [Fintype S] (M : PDA Q T S) (w : List T) : ESFS_Inv M w { state := Sum.inr 0, input := w, stack := [none] }

theorem ESFS_Inv_step {T : Type} [Fintype T] {Q S : Type} [Fintype Q] [Fintype S] (M : PDA Q T S) (w : List T) (c₁ c₂ : (PDA_ES_to_FS_pda M).conf) (h_inv : ESFS_Inv M w c₁) (h_step : PDA.Reaches₁ c₁ c₂) : ESFS_Inv M w c₂

theorem ESFS_Inv_reaches {T : Type} [Fintype T] {Q S : Type} [Fintype Q] [Fintype S] (M : PDA Q T S) (w : List T) (c₁ c₂ : (PDA_ES_to_FS_pda M).conf) (h_inv : ESFS_Inv M w c₁) (h_reach : PDA.Reaches c₁ c₂) : ESFS_Inv M w c₂

theorem ESFS_Inv_terminal {T : Type} [Fintype T] {Q S : Type} [Fintype Q] [Fintype S] (M : PDA Q T S) (w : List T) (q : Q ⊕ Fin 2) (γ : List (Option S)) (hq : q ∈ {Sum.inr 1}) (h_inv : ESFS_Inv M w { state := q, input := [], stack := γ }) : w ∈ M.acceptsByEmptyStack

theorem PDA_ES_to_FS_backward {T : Type} [Fintype T] {Q S : Type} [Fintype Q] [Fintype S] (M : PDA Q T S) (w : List T) (h : w ∈ (PDA_ES_to_FS_pda M).acceptsByFinalState) : w ∈ M.acceptsByEmptyStack

theorem PDA_ES_subset_FS {T : Type} [Fintype T] {Q S : Type} [Fintype Q] [Fintype S] (M : PDA Q T S) : ∃ (Q' : Type) (S' : Type) (x : Fintype Q') (x_1 : Fintype S') (M' : PDA Q' T S'), M'.acceptsByFinalState = M.acceptsByEmptyStack

Any PDA empty-stack language is also a PDA final-state language.

theorem is_PDA_finalState_iff_is_PDA_emptyStack {T : Type} [Fintype T] {L : Language T} : PDA.is_PDA_finalState L ↔ PDA.is_PDA_emptyStack L

A language is accepted by some PDA via empty-stack acceptance iff it is accepted by some PDA via final-state acceptance.

@[simp]

theorem is_PDA_finalState_iff_is_PDA {T : Type} [Fintype T] {L : Language T} : PDA.is_PDA_finalState L ↔ PDA.is_PDA L

theorem PDA_FinalStateClass_eq_EmptyStackClass {T : Type} [Fintype T] : PDA.FinalStateClass = PDA.EmptyStackClass

The languages accepted by PDAs via final-state acceptance are exactly the languages accepted by PDAs via empty-stack acceptance.

theorem PDA_FinalStateClass_eq_Class {T : Type} [Fintype T] : PDA.FinalStateClass = PDA.Class