Epsilon Phases of a DPDA

Before a DPDA can safely be complemented by flipping final states, its forced epsilon-only phases must be accounted for. This file records the semantic objects used by the totalization construction: epsilon-only one-step motion, epsilon-only reachability, stable configurations, and divergence.

@[reducible, inline]

abbrev DPDA.EpsilonConf (Q S : Type) : Type

The stack/control part of a DPDA configuration, ignoring the unchanged input.

Equations

• DPDA.EpsilonConf Q S = (Q × List S)

def DPDA.EpsilonStep {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) : EpsilonConf Q S → EpsilonConf Q S → Prop

One forced epsilon step on the control/stack part of a configuration.

Equations

• M.EpsilonStep (q, Z :: γ) (p, γ') = ∃ (β : List S), M.epsilon_transition q Z = some (p, β) ∧ γ' = β ++ γ
• M.EpsilonStep (fst, []) x✝ = False

def DPDA.epsilonNext? {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) : EpsilonConf Q S → Option (EpsilonConf Q S)

The deterministic successor function for one epsilon step, if one exists.

Equations

• M.epsilonNext? (q, Z :: γ) = match M.epsilon_transition q Z with | some (p, β) => some (p, β ++ γ) | none => none
• M.epsilonNext? (fst, []) = none

def DPDA.EpsilonReaches {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) : EpsilonConf Q S → EpsilonConf Q S → Prop

Epsilon-only reachability on the control/stack part of a configuration.

Equations

• M.EpsilonReaches = Relation.ReflTransGen M.EpsilonStep

def DPDA.EpsilonStable {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) : EpsilonConf Q S → Prop

A control/stack configuration is stable when no epsilon transition is forced.

Equations

• M.EpsilonStable (fst, []) = True
• M.EpsilonStable (q, Z :: tail) = (M.epsilon_transition q Z = none)

def DPDA.EpsilonStopsAt {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (c c' : EpsilonConf Q S) : Prop

An epsilon phase stops at a stable control/stack configuration.

Equations

• M.EpsilonStopsAt c c' = (M.EpsilonReaches c c' ∧ M.EpsilonStable c')

def DPDA.EpsilonDiverges {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (c : EpsilonConf Q S) : Prop

An infinite epsilon-only computation from a control/stack configuration.

Equations

• M.EpsilonDiverges c = ∃ (run : ℕ → DPDA.EpsilonConf Q S), run 0 = c ∧ ∀ (n : ℕ), M.EpsilonStep (run n) (run (n + 1))

@[simp]

theorem DPDA.epsilonNext?_nil {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (q : Q) : M.epsilonNext? (q, []) = none

theorem DPDA.epsilonStep_iff_next?_eq_some {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (c c' : EpsilonConf Q S) : M.EpsilonStep c c' ↔ M.epsilonNext? c = some c'

theorem DPDA.epsilonStable_iff_next?_eq_none {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (c : EpsilonConf Q S) : M.EpsilonStable c ↔ M.epsilonNext? c = none

theorem DPDA.exists_epsilonStep_of_not_stable {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {c : EpsilonConf Q S} (h : ¬M.EpsilonStable c) : ∃ (c' : EpsilonConf Q S), M.EpsilonStep c c'

theorem DPDA.not_epsilonStep_of_stable {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {c c' : EpsilonConf Q S} (hstable : M.EpsilonStable c) : ¬M.EpsilonStep c c'

theorem DPDA.epsilonStep_deterministic {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {c c₁ c₂ : EpsilonConf Q S} (h₁ : M.EpsilonStep c c₁) (h₂ : M.EpsilonStep c c₂) : c₁ = c₂

theorem DPDA.epsilonStep_suffix_of_stops {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} {c c₁ cfinal : EpsilonConf Q S} (hstep : M.EpsilonStep c c₁) (hstops : M.EpsilonStopsAt c cfinal) : M.EpsilonStopsAt c₁ cfinal

theorem DPDA.epsilonReaches_suffix_of_stops {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} {c c₁ cfinal : EpsilonConf Q S} (hreach : M.EpsilonReaches c c₁) (hstops : M.EpsilonStopsAt c cfinal) : M.EpsilonStopsAt c₁ cfinal

theorem DPDA.epsilonStopsAt_of_step {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} {c c₁ : EpsilonConf Q S} (hstep : M.EpsilonStep c c₁) (hstops : ∃ (cfinal : EpsilonConf Q S), M.EpsilonStopsAt c₁ cfinal) : ∃ (cfinal : EpsilonConf Q S), M.EpsilonStopsAt c cfinal

noncomputable def DPDA.epsilonRun {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (c : EpsilonConf Q S) : ℕ → EpsilonConf Q S

The canonical epsilon run that follows the deterministic epsilon successor while it exists.

Equations

• M.epsilonRun c 0 = c
• M.epsilonRun c n.succ = (M.epsilonNext? (M.epsilonRun c n)).getD (M.epsilonRun c n)

theorem DPDA.epsilonRun_zero {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (c : EpsilonConf Q S) : M.epsilonRun c 0 = c

theorem DPDA.epsilonRun_succ {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (c : EpsilonConf Q S) (n : ℕ) : M.epsilonRun c (n + 1) = (M.epsilonNext? (M.epsilonRun c n)).getD (M.epsilonRun c n)

theorem DPDA.epsilonReaches_epsilonRun_of_all_steps {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} {c : EpsilonConf Q S} (hstep : ∀ (n : ℕ), M.EpsilonStep (M.epsilonRun c n) (M.epsilonRun c (n + 1))) (n : ℕ) : M.EpsilonReaches c (M.epsilonRun c n)

theorem DPDA.epsilonPhase_stops_or_diverges {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (c : EpsilonConf Q S) : (∃ (c' : EpsilonConf Q S), M.EpsilonStopsAt c c') ∨ M.EpsilonDiverges c

Semantically, a deterministic epsilon phase either reaches a stable configuration or has an infinite epsilon-only run. The later finite-state totalizer must implement this split using regular stack lookahead.

theorem DPDA.epsilonStep_toPDA {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} {c c' : EpsilonConf Q S} {w : List T} (h : M.EpsilonStep c c') : PDA.Reaches₁ { state := c.1, input := w, stack := c.2 } { state := c'.1, input := w, stack := c'.2 }

Lift one semantic epsilon step to the underlying PDA step relation, for any fixed input.

theorem DPDA.epsilonReaches_toPDA {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} {c c' : EpsilonConf Q S} {w : List T} (h : M.EpsilonReaches c c') : PDA.Reaches { state := c.1, input := w, stack := c.2 } { state := c'.1, input := w, stack := c'.2 }

Lift epsilon-only reachability to ordinary PDA reachability, preserving the input.

theorem DPDA.epsilonStep_of_toPDA_empty_step {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} {q p : Q} {γ γ' : List S} (h : PDA.Reaches₁ { state := q, input := [], stack := γ } { state := p, input := [], stack := γ' }) : M.EpsilonStep (q, γ) (p, γ')

theorem DPDA.epsilonReaches_of_toPDA_empty_reaches {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} {q p : Q} {γ γ' : List S} (h : PDA.Reaches { state := q, input := [], stack := γ } { state := p, input := [], stack := γ' }) : M.EpsilonReaches (q, γ) (p, γ')

theorem DPDA.stable_reaches_nonempty_decompose {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} {q qf : Q} {a : T} {w : List T} {Z : S} {γ γf : List S} (hstable : M.epsilon_transition q Z = none) (hreach : PDA.Reaches { state := q, input := a :: w, stack := Z :: γ } { state := qf, input := [], stack := γf }) : ∃ (p : Q) (β : List S), M.transition q a Z = some (p, β) ∧ PDA.Reaches { state := p, input := w, stack := β ++ γ } { state := qf, input := [], stack := γf }

theorem DPDA.toPDA_reaches_suffix_of_epsilonStep_nonempty {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} {c c' : EpsilonConf Q S} {qf : Q} {a : T} {w : List T} {γf : List S} (hstep : M.EpsilonStep c c') (hreach : PDA.Reaches { state := c.1, input := a :: w, stack := c.2 } { state := qf, input := [], stack := γf }) : PDA.Reaches { state := c'.1, input := a :: w, stack := c'.2 } { state := qf, input := [], stack := γf }

theorem DPDA.toPDA_reaches_suffix_of_epsilonReaches_nonempty {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} {c c' : EpsilonConf Q S} {qf : Q} {a : T} {w : List T} {γf : List S} (heps : M.EpsilonReaches c c') (hreach : PDA.Reaches { state := c.1, input := a :: w, stack := c.2 } { state := qf, input := [], stack := γf }) : PDA.Reaches { state := c'.1, input := a :: w, stack := c'.2 } { state := qf, input := [], stack := γf }

theorem DPDA.epsilonStopsAt_of_toPDA_reaches_nonempty {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} {q qf : Q} {a : T} {w : List T} {γ γf : List S} (hreach : PDA.Reaches { state := q, input := a :: w, stack := γ } { state := qf, input := [], stack := γf }) : ∃ (cstable : EpsilonConf Q S), M.EpsilonStopsAt (q, γ) cstable