Useful epsilon cycles in the normalized empty-stack PDA

The final-state-to-empty-stack conversion is almost deterministic. Its only extra branch enters the fresh drain state from a normalized final state. First-final normalization makes that branch harmless for useful computations: a simulation branch which returned to the same cut would be a forbidden nonempty epsilon path from a normalized final state to itself.

theorem DPDA_to_LR.emptyStack_simulation_step_projects {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {q p : Q × Bool} {input input' : List T} {stack stack' : List (EStack M)} (h : PDA.Reaches₁ { state := Sum.inl q, input := input, stack := stack } { state := Sum.inl p, input := input', stack := stack' }) : PDA.Reaches₁ { state := q, input := input, stack := List.filterMap id stack } { state := p, input := input', stack := List.filterMap id stack' }

A simulation-to-simulation FS→ES step projects through arbitrary Option stack context to a step of the normalized DPDA. none symbols in the untouched context are simply erased by filterMap.

theorem DPDA_to_LR.emptyStack_simulation_reaches_classify {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {q : Q × Bool} {input : List T} {stack : List (EStack M)} {d : (emptyStackPDA M).conf} (h : PDA.Reaches { state := Sum.inl q, input := input, stack := stack } d) : (∃ (p : Q × Bool) (output : List T) (result : List (EStack M)), d = { state := Sum.inl p, input := output, stack := result } ∧ PDA.Reaches { state := q, input := input, stack := List.filterMap id stack } { state := p, input := output, stack := List.filterMap id result }) ∨ d.state = Sum.inr 1 ∧ ∃ (p : Q × Bool) (output : List T) (result : List S), p ∈ M.firstFinal.final_states ∧ PDA.Reaches { state := q, input := input, stack := List.filterMap id stack } { state := p, input := output, stack := result }

A run beginning in a simulation state either remains a simulation of the normalized DPDA, or has entered the drain after reaching a normalized final configuration. The statement permits arbitrary Option stack context.

theorem DPDA_to_LR.emptyStack_no_useful_cycle {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {c : (emptyStackPDA M).conf} {final : EState M} (hcycle : Relation.TransGen PDA.Reaches₁ c c) (huseful : PDA.Reaches c { state := final, input := [], stack := [] }) : False

The normalized FS→ES machine has no nonempty cycle with a continuation to empty stack. Boot cannot be re-entered, drain steps strictly shrink the stack, and a simulation cycle projects to the deterministic first-final machine. A useful simulation continuation either itself reaches empty stack, or enters drain from a normalized final state; both projected alternatives contradict determinism and first-final normalization.

theorem DPDA_to_LR.emptyStack_no_useful_stack_growth {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {q final : EState M} {base extra context : List (EStack M)} {input : List T} (hgrowth : PDA.Reaches { state := q, input := [], stack := base } { state := q, input := [], stack := base ++ extra }) (hextra : extra ≠ []) (huseful : PDA.Reaches { state := q, input := input, stack := base ++ extra ++ context } { state := final, input := [], stack := [] }) : False

The same exclusion holds for a useful self-embedding stack-growth segment in the FS→ES machine. In the simulation component the inserted Option block either projects to a nonempty normalized-DPDA block, where the counted stack-growth kernels apply, or projects to the empty block, where the nonempty FS→ES segment becomes an exact normalized-DPDA cycle.